Proof of Theorem dyadmaxlem
Step | Hyp | Ref
| Expression |
1 | | dyadmax.7 |
. . . . . . . . 9
⊢ (𝜑 → ([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷))) |
2 | | dyadmax.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℤ) |
3 | | dyadmax.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐶 ∈
ℕ0) |
4 | | dyadmbl.1 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) |
5 | 4 | dyadval 24754 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℕ0)
→ (𝐴𝐹𝐶) = 〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉) |
6 | 2, 3, 5 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴𝐹𝐶) = 〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉) |
7 | 6 | fveq2d 6775 |
. . . . . . . . . 10
⊢ (𝜑 → ([,]‘(𝐴𝐹𝐶)) = ([,]‘〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉)) |
8 | | df-ov 7274 |
. . . . . . . . . 10
⊢ ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶))) = ([,]‘〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉) |
9 | 7, 8 | eqtr4di 2798 |
. . . . . . . . 9
⊢ (𝜑 → ([,]‘(𝐴𝐹𝐶)) = ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
10 | | dyadmax.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ∈ ℤ) |
11 | | dyadmax.5 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
12 | 4 | dyadss 24756 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) → 𝐷 ≤ 𝐶)) |
13 | 2, 10, 3, 11, 12 | syl22anc 836 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) → 𝐷 ≤ 𝐶)) |
14 | 1, 13 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ≤ 𝐶) |
15 | | dyadmax.6 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ¬ 𝐷 < 𝐶) |
16 | 11 | nn0red 12294 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ ℝ) |
17 | 3 | nn0red 12294 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ ℝ) |
18 | 16, 17 | eqleltd 11119 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 = 𝐶 ↔ (𝐷 ≤ 𝐶 ∧ ¬ 𝐷 < 𝐶))) |
19 | 14, 15, 18 | mpbir2and 710 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 = 𝐶) |
20 | 19 | oveq2d 7287 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵𝐹𝐷) = (𝐵𝐹𝐶)) |
21 | 4 | dyadval 24754 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0)
→ (𝐵𝐹𝐶) = 〈(𝐵 / (2↑𝐶)), ((𝐵 + 1) / (2↑𝐶))〉) |
22 | 10, 3, 21 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐵𝐹𝐶) = 〈(𝐵 / (2↑𝐶)), ((𝐵 + 1) / (2↑𝐶))〉) |
23 | 20, 22 | eqtrd 2780 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵𝐹𝐷) = 〈(𝐵 / (2↑𝐶)), ((𝐵 + 1) / (2↑𝐶))〉) |
24 | 23 | fveq2d 6775 |
. . . . . . . . . 10
⊢ (𝜑 → ([,]‘(𝐵𝐹𝐷)) = ([,]‘〈(𝐵 / (2↑𝐶)), ((𝐵 + 1) / (2↑𝐶))〉)) |
25 | | df-ov 7274 |
. . . . . . . . . 10
⊢ ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶))) = ([,]‘〈(𝐵 / (2↑𝐶)), ((𝐵 + 1) / (2↑𝐶))〉) |
26 | 24, 25 | eqtr4di 2798 |
. . . . . . . . 9
⊢ (𝜑 → ([,]‘(𝐵𝐹𝐷)) = ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶)))) |
27 | 1, 9, 26 | 3sstr3d 3972 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶))) ⊆ ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶)))) |
28 | 2 | zred 12425 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
29 | | 2nn 12046 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
30 | | nnexpcl 13793 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝐶
∈ ℕ0) → (2↑𝐶) ∈ ℕ) |
31 | 29, 3, 30 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (2↑𝐶) ∈ ℕ) |
32 | 28, 31 | nndivred 12027 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 / (2↑𝐶)) ∈ ℝ) |
33 | 32 | rexrd 11026 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (2↑𝐶)) ∈
ℝ*) |
34 | | peano2re 11148 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
35 | 28, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + 1) ∈ ℝ) |
36 | 35, 31 | nndivred 12027 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ) |
37 | 36 | rexrd 11026 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 + 1) / (2↑𝐶)) ∈
ℝ*) |
38 | 28 | lep1d 11906 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≤ (𝐴 + 1)) |
39 | 31 | nnred 11988 |
. . . . . . . . . . 11
⊢ (𝜑 → (2↑𝐶) ∈ ℝ) |
40 | 31 | nngt0d 12022 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (2↑𝐶)) |
41 | | lediv1 11840 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 + 1) ∈ ℝ ∧
((2↑𝐶) ∈ ℝ
∧ 0 < (2↑𝐶)))
→ (𝐴 ≤ (𝐴 + 1) ↔ (𝐴 / (2↑𝐶)) ≤ ((𝐴 + 1) / (2↑𝐶)))) |
42 | 28, 35, 39, 40, 41 | syl112anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ≤ (𝐴 + 1) ↔ (𝐴 / (2↑𝐶)) ≤ ((𝐴 + 1) / (2↑𝐶)))) |
43 | 38, 42 | mpbid 231 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / (2↑𝐶)) ≤ ((𝐴 + 1) / (2↑𝐶))) |
44 | | ubicc2 13196 |
. . . . . . . . 9
⊢ (((𝐴 / (2↑𝐶)) ∈ ℝ* ∧ ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ*
∧ (𝐴 / (2↑𝐶)) ≤ ((𝐴 + 1) / (2↑𝐶))) → ((𝐴 + 1) / (2↑𝐶)) ∈ ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
45 | 33, 37, 43, 44 | syl3anc 1370 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + 1) / (2↑𝐶)) ∈ ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
46 | 27, 45 | sseldd 3927 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + 1) / (2↑𝐶)) ∈ ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶)))) |
47 | 10 | zred 12425 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℝ) |
48 | 47, 31 | nndivred 12027 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 / (2↑𝐶)) ∈ ℝ) |
49 | | peano2re 11148 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℝ) |
50 | 47, 49 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 + 1) ∈ ℝ) |
51 | 50, 31 | nndivred 12027 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 + 1) / (2↑𝐶)) ∈ ℝ) |
52 | | elicc2 13143 |
. . . . . . . 8
⊢ (((𝐵 / (2↑𝐶)) ∈ ℝ ∧ ((𝐵 + 1) / (2↑𝐶)) ∈ ℝ) → (((𝐴 + 1) / (2↑𝐶)) ∈ ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶))) ↔ (((𝐴 + 1) / (2↑𝐶)) ∈ ℝ ∧ (𝐵 / (2↑𝐶)) ≤ ((𝐴 + 1) / (2↑𝐶)) ∧ ((𝐴 + 1) / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶))))) |
53 | 48, 51, 52 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 + 1) / (2↑𝐶)) ∈ ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶))) ↔ (((𝐴 + 1) / (2↑𝐶)) ∈ ℝ ∧ (𝐵 / (2↑𝐶)) ≤ ((𝐴 + 1) / (2↑𝐶)) ∧ ((𝐴 + 1) / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶))))) |
54 | 46, 53 | mpbid 231 |
. . . . . 6
⊢ (𝜑 → (((𝐴 + 1) / (2↑𝐶)) ∈ ℝ ∧ (𝐵 / (2↑𝐶)) ≤ ((𝐴 + 1) / (2↑𝐶)) ∧ ((𝐴 + 1) / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶)))) |
55 | 54 | simp3d 1143 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 1) / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶))) |
56 | | lediv1 11840 |
. . . . . 6
⊢ (((𝐴 + 1) ∈ ℝ ∧
(𝐵 + 1) ∈ ℝ
∧ ((2↑𝐶) ∈
ℝ ∧ 0 < (2↑𝐶))) → ((𝐴 + 1) ≤ (𝐵 + 1) ↔ ((𝐴 + 1) / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶)))) |
57 | 35, 50, 39, 40, 56 | syl112anc 1373 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 1) ≤ (𝐵 + 1) ↔ ((𝐴 + 1) / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶)))) |
58 | 55, 57 | mpbird 256 |
. . . 4
⊢ (𝜑 → (𝐴 + 1) ≤ (𝐵 + 1)) |
59 | | 1red 10977 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
60 | 28, 47, 59 | leadd1d 11569 |
. . . 4
⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 + 1) ≤ (𝐵 + 1))) |
61 | 58, 60 | mpbird 256 |
. . 3
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
62 | | lbicc2 13195 |
. . . . . . . 8
⊢ (((𝐴 / (2↑𝐶)) ∈ ℝ* ∧ ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ*
∧ (𝐴 / (2↑𝐶)) ≤ ((𝐴 + 1) / (2↑𝐶))) → (𝐴 / (2↑𝐶)) ∈ ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
63 | 33, 37, 43, 62 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜑 → (𝐴 / (2↑𝐶)) ∈ ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
64 | 27, 63 | sseldd 3927 |
. . . . . 6
⊢ (𝜑 → (𝐴 / (2↑𝐶)) ∈ ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶)))) |
65 | | elicc2 13143 |
. . . . . . 7
⊢ (((𝐵 / (2↑𝐶)) ∈ ℝ ∧ ((𝐵 + 1) / (2↑𝐶)) ∈ ℝ) → ((𝐴 / (2↑𝐶)) ∈ ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶))) ↔ ((𝐴 / (2↑𝐶)) ∈ ℝ ∧ (𝐵 / (2↑𝐶)) ≤ (𝐴 / (2↑𝐶)) ∧ (𝐴 / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶))))) |
66 | 48, 51, 65 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝐴 / (2↑𝐶)) ∈ ((𝐵 / (2↑𝐶))[,]((𝐵 + 1) / (2↑𝐶))) ↔ ((𝐴 / (2↑𝐶)) ∈ ℝ ∧ (𝐵 / (2↑𝐶)) ≤ (𝐴 / (2↑𝐶)) ∧ (𝐴 / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶))))) |
67 | 64, 66 | mpbid 231 |
. . . . 5
⊢ (𝜑 → ((𝐴 / (2↑𝐶)) ∈ ℝ ∧ (𝐵 / (2↑𝐶)) ≤ (𝐴 / (2↑𝐶)) ∧ (𝐴 / (2↑𝐶)) ≤ ((𝐵 + 1) / (2↑𝐶)))) |
68 | 67 | simp2d 1142 |
. . . 4
⊢ (𝜑 → (𝐵 / (2↑𝐶)) ≤ (𝐴 / (2↑𝐶))) |
69 | | lediv1 11840 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧
((2↑𝐶) ∈ ℝ
∧ 0 < (2↑𝐶)))
→ (𝐵 ≤ 𝐴 ↔ (𝐵 / (2↑𝐶)) ≤ (𝐴 / (2↑𝐶)))) |
70 | 47, 28, 39, 40, 69 | syl112anc 1373 |
. . . 4
⊢ (𝜑 → (𝐵 ≤ 𝐴 ↔ (𝐵 / (2↑𝐶)) ≤ (𝐴 / (2↑𝐶)))) |
71 | 68, 70 | mpbird 256 |
. . 3
⊢ (𝜑 → 𝐵 ≤ 𝐴) |
72 | 28, 47 | letri3d 11117 |
. . 3
⊢ (𝜑 → (𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴))) |
73 | 61, 71, 72 | mpbir2and 710 |
. 2
⊢ (𝜑 → 𝐴 = 𝐵) |
74 | 19 | eqcomd 2746 |
. 2
⊢ (𝜑 → 𝐶 = 𝐷) |
75 | 73, 74 | jca 512 |
1
⊢ (𝜑 → (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) |