Metamath Proof Explorer

Theorem dyadmaxlem

Description: Lemma for dyadmax . (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypotheses dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
dyadmax.2 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
dyadmax.3 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
dyadmax.4 ⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
dyadmax.5 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
dyadmax.6 ⊢ ( 𝜑 → ¬ 𝐷 < 𝐶 )
dyadmax.7 ⊢ ( 𝜑 → ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) )
Assertion dyadmaxlem ( 𝜑 → ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 dyadmax.2 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3 dyadmax.3 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
4 dyadmax.4 ⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
5 dyadmax.5 ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
6 dyadmax.6 ⊢ ( 𝜑 → ¬ 𝐷 < 𝐶 )
7 dyadmax.7 ⊢ ( 𝜑 → ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) )
8 1 dyadval ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 𝐹 𝐶 ) = ⟨ ( 𝐴 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ )
9 2 4 8 syl2anc ⊢ ( 𝜑 → ( 𝐴 𝐹 𝐶 ) = ⟨ ( 𝐴 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ )
10 9 fveq2d ⊢ ( 𝜑 → ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) = ( [,] ‘ ⟨ ( 𝐴 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ ) )
11 df-ov ⊢ ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) = ( [,] ‘ ⟨ ( 𝐴 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ )
12 10 11 eqtr4di ⊢ ( 𝜑 → ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) = ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
13 1 dyadss ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) ) → ( ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) → 𝐷 ≤ 𝐶 ) )
14 2 3 4 5 13 syl22anc ⊢ ( 𝜑 → ( ( [,] ‘ ( 𝐴 𝐹 𝐶 ) ) ⊆ ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) → 𝐷 ≤ 𝐶 ) )
15 7 14 mpd ⊢ ( 𝜑 → 𝐷 ≤ 𝐶 )
16 5 nn0red ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
17 4 nn0red ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
18 16 17 eqleltd ⊢ ( 𝜑 → ( 𝐷 = 𝐶 ↔ ( 𝐷 ≤ 𝐶 ∧ ¬ 𝐷 < 𝐶 ) ) )
19 15 6 18 mpbir2and ⊢ ( 𝜑 → 𝐷 = 𝐶 )
20 19 oveq2d ⊢ ( 𝜑 → ( 𝐵 𝐹 𝐷 ) = ( 𝐵 𝐹 𝐶 ) )
21 1 dyadval ⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐵 𝐹 𝐶 ) = ⟨ ( 𝐵 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ )
22 3 4 21 syl2anc ⊢ ( 𝜑 → ( 𝐵 𝐹 𝐶 ) = ⟨ ( 𝐵 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ )
23 20 22 eqtrd ⊢ ( 𝜑 → ( 𝐵 𝐹 𝐷 ) = ⟨ ( 𝐵 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ )
24 23 fveq2d ⊢ ( 𝜑 → ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) = ( [,] ‘ ⟨ ( 𝐵 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ ) )
25 df-ov ⊢ ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) = ( [,] ‘ ⟨ ( 𝐵 / ( 2 ↑ 𝐶 ) ) , ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ⟩ )
26 24 25 eqtr4di ⊢ ( 𝜑 → ( [,] ‘ ( 𝐵 𝐹 𝐷 ) ) = ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
27 7 12 26 3sstr3d ⊢ ( 𝜑 → ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ⊆ ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
28 2 zred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
29 2nn ⊢ 2 ∈ ℕ
30 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ 𝐶 ∈ ℕ0 ) → ( 2 ↑ 𝐶 ) ∈ ℕ )
31 29 4 30 sylancr ⊢ ( 𝜑 → ( 2 ↑ 𝐶 ) ∈ ℕ )
32 28 31 nndivred ⊢ ( 𝜑 → ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ℝ )
33 32 rexrd ⊢ ( 𝜑 → ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ℝ* )
34 peano2re ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) ∈ ℝ )
35 28 34 syl ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ )
36 35 31 nndivred ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ )
37 36 rexrd ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ* )
38 28 lep1d ⊢ ( 𝜑 → 𝐴 ≤ ( 𝐴 + 1 ) )
39 31 nnred ⊢ ( 𝜑 → ( 2 ↑ 𝐶 ) ∈ ℝ )
40 31 nngt0d ⊢ ( 𝜑 → 0 < ( 2 ↑ 𝐶 ) )
41 lediv1 ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐴 + 1 ) ∈ ℝ ∧ ( ( 2 ↑ 𝐶 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐶 ) ) ) → ( 𝐴 ≤ ( 𝐴 + 1 ) ↔ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
42 28 35 39 40 41 syl112anc ⊢ ( 𝜑 → ( 𝐴 ≤ ( 𝐴 + 1 ) ↔ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
43 38 42 mpbid ⊢ ( 𝜑 → ( 𝐴 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) )
44 ubicc2 ⊢ ( ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ℝ* ∧ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ* ∧ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) → ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
45 33 37 43 44 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
46 27 45 sseldd ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
47 3 zred ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
48 47 31 nndivred ⊢ ( 𝜑 → ( 𝐵 / ( 2 ↑ 𝐶 ) ) ∈ ℝ )
49 peano2re ⊢ ( 𝐵 ∈ ℝ → ( 𝐵 + 1 ) ∈ ℝ )
50 47 49 syl ⊢ ( 𝜑 → ( 𝐵 + 1 ) ∈ ℝ )
51 50 31 nndivred ⊢ ( 𝜑 → ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ )
52 elicc2 ⊢ ( ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) ∈ ℝ ∧ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ ) → ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ↔ ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ ∧ ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∧ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ) )
53 48 51 52 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ↔ ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ ∧ ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∧ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ) )
54 46 53 mpbid ⊢ ( 𝜑 → ( ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ ∧ ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∧ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
55 54 simp3d ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) )
56 lediv1 ⊢ ( ( ( 𝐴 + 1 ) ∈ ℝ ∧ ( 𝐵 + 1 ) ∈ ℝ ∧ ( ( 2 ↑ 𝐶 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐶 ) ) ) → ( ( 𝐴 + 1 ) ≤ ( 𝐵 + 1 ) ↔ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
57 35 50 39 40 56 syl112anc ⊢ ( 𝜑 → ( ( 𝐴 + 1 ) ≤ ( 𝐵 + 1 ) ↔ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
58 55 57 mpbird ⊢ ( 𝜑 → ( 𝐴 + 1 ) ≤ ( 𝐵 + 1 ) )
59 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
60 28 47 59 leadd1d ⊢ ( 𝜑 → ( 𝐴 ≤ 𝐵 ↔ ( 𝐴 + 1 ) ≤ ( 𝐵 + 1 ) ) )
61 58 60 mpbird ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
62 lbicc2 ⊢ ( ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ℝ* ∧ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ* ∧ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) → ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
63 33 37 43 62 syl3anc ⊢ ( 𝜑 → ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐴 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
64 27 63 sseldd ⊢ ( 𝜑 → ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
65 elicc2 ⊢ ( ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) ∈ ℝ ∧ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ∈ ℝ ) → ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ↔ ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ℝ ∧ ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∧ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ) )
66 48 51 65 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ( ( 𝐵 / ( 2 ↑ 𝐶 ) ) [,] ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ↔ ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ℝ ∧ ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∧ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) ) )
67 64 66 mpbid ⊢ ( 𝜑 → ( ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∈ ℝ ∧ ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ∧ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ≤ ( ( 𝐵 + 1 ) / ( 2 ↑ 𝐶 ) ) ) )
68 67 simp2d ⊢ ( 𝜑 → ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( 𝐴 / ( 2 ↑ 𝐶 ) ) )
69 lediv1 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( ( 2 ↑ 𝐶 ) ∈ ℝ ∧ 0 < ( 2 ↑ 𝐶 ) ) ) → ( 𝐵 ≤ 𝐴 ↔ ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ) )
70 47 28 39 40 69 syl112anc ⊢ ( 𝜑 → ( 𝐵 ≤ 𝐴 ↔ ( 𝐵 / ( 2 ↑ 𝐶 ) ) ≤ ( 𝐴 / ( 2 ↑ 𝐶 ) ) ) )
71 68 70 mpbird ⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
72 28 47 letri3d ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴 ) ) )
73 61 71 72 mpbir2and ⊢ ( 𝜑 → 𝐴 = 𝐵 )
74 19 eqcomd ⊢ ( 𝜑 → 𝐶 = 𝐷 )
75 73 74 jca ⊢ ( 𝜑 → ( 𝐴 = 𝐵 ∧ 𝐶 = 𝐷 ) )