Proof of Theorem dyaddisjlem
| Step | Hyp | Ref
| Expression |
| 1 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐴 ∈ ℤ) |
| 2 | | simplrl 777 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈
ℕ0) |
| 3 | | dyadmbl.1 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑥 ∈ ℤ, 𝑦 ∈ ℕ0 ↦
〈(𝑥 / (2↑𝑦)), ((𝑥 + 1) / (2↑𝑦))〉) |
| 4 | 3 | dyadval 25627 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℕ0)
→ (𝐴𝐹𝐶) = 〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉) |
| 5 | 1, 2, 4 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐴𝐹𝐶) = 〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉) |
| 6 | 5 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((,)‘(𝐴𝐹𝐶)) = ((,)‘〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉)) |
| 7 | | df-ov 7434 |
. . . . . . . 8
⊢ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))) = ((,)‘〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((,)‘(𝐴𝐹𝐶)) = ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶)))) |
| 9 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐵 ∈ ℤ) |
| 10 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈
ℕ0) |
| 11 | 3 | dyadval 25627 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℕ0)
→ (𝐵𝐹𝐷) = 〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉) |
| 12 | 9, 10, 11 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐵𝐹𝐷) = 〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉) |
| 13 | 12 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((,)‘(𝐵𝐹𝐷)) = ((,)‘〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉)) |
| 14 | | df-ov 7434 |
. . . . . . . 8
⊢ ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) = ((,)‘〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉) |
| 15 | 13, 14 | eqtr4di 2795 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((,)‘(𝐵𝐹𝐷)) = ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷)))) |
| 16 | 8, 15 | ineq12d 4221 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = (((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))) ∩ ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))))) |
| 17 | | incom 4209 |
. . . . . 6
⊢ (((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))) ∩ ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷)))) = (((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) ∩ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶)))) |
| 18 | 16, 17 | eqtrdi 2793 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = (((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) ∩ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))))) |
| 19 | 18 | adantr 480 |
. . . 4
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐵 / (2↑𝐷)) < (𝐴 / (2↑𝐶))) → (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = (((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) ∩ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))))) |
| 20 | 1 | zred 12722 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐴 ∈ ℝ) |
| 21 | 20 | recnd 11289 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐴 ∈ ℂ) |
| 22 | | 2nn 12339 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℕ |
| 23 | | nnexpcl 14115 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝐶
∈ ℕ0) → (2↑𝐶) ∈ ℕ) |
| 24 | 22, 2, 23 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (2↑𝐶) ∈ ℕ) |
| 25 | 24 | nncnd 12282 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (2↑𝐶) ∈ ℂ) |
| 26 | | nnexpcl 14115 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℕ ∧ 𝐷
∈ ℕ0) → (2↑𝐷) ∈ ℕ) |
| 27 | 22, 10, 26 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (2↑𝐷) ∈ ℕ) |
| 28 | 27 | nncnd 12282 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (2↑𝐷) ∈ ℂ) |
| 29 | 24 | nnne0d 12316 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (2↑𝐶) ≠ 0) |
| 30 | 21, 25, 28, 29 | div13d 12067 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐴 / (2↑𝐶)) · (2↑𝐷)) = (((2↑𝐷) / (2↑𝐶)) · 𝐴)) |
| 31 | | 2cnd 12344 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 2 ∈ ℂ) |
| 32 | | 2ne0 12370 |
. . . . . . . . . . . . 13
⊢ 2 ≠
0 |
| 33 | 32 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 2 ≠ 0) |
| 34 | 2 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐶 ∈ ℤ) |
| 35 | 10 | nn0zd 12639 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐷 ∈ ℤ) |
| 36 | 31, 33, 34, 35 | expsubd 14197 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (2↑(𝐷 − 𝐶)) = ((2↑𝐷) / (2↑𝐶))) |
| 37 | | 2z 12649 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℤ |
| 38 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐶 ≤ 𝐷) |
| 39 | | znn0sub 12664 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ) → (𝐶 ≤ 𝐷 ↔ (𝐷 − 𝐶) ∈
ℕ0)) |
| 40 | 34, 35, 39 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐶 ≤ 𝐷 ↔ (𝐷 − 𝐶) ∈
ℕ0)) |
| 41 | 38, 40 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐷 − 𝐶) ∈
ℕ0) |
| 42 | | zexpcl 14117 |
. . . . . . . . . . . 12
⊢ ((2
∈ ℤ ∧ (𝐷
− 𝐶) ∈
ℕ0) → (2↑(𝐷 − 𝐶)) ∈ ℤ) |
| 43 | 37, 41, 42 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (2↑(𝐷 − 𝐶)) ∈ ℤ) |
| 44 | 36, 43 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((2↑𝐷) / (2↑𝐶)) ∈ ℤ) |
| 45 | 44, 1 | zmulcld 12728 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((2↑𝐷) / (2↑𝐶)) · 𝐴) ∈ ℤ) |
| 46 | 30, 45 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐴 / (2↑𝐶)) · (2↑𝐷)) ∈ ℤ) |
| 47 | | zltp1le 12667 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℤ ∧ ((𝐴 / (2↑𝐶)) · (2↑𝐷)) ∈ ℤ) → (𝐵 < ((𝐴 / (2↑𝐶)) · (2↑𝐷)) ↔ (𝐵 + 1) ≤ ((𝐴 / (2↑𝐶)) · (2↑𝐷)))) |
| 48 | 9, 46, 47 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐵 < ((𝐴 / (2↑𝐶)) · (2↑𝐷)) ↔ (𝐵 + 1) ≤ ((𝐴 / (2↑𝐶)) · (2↑𝐷)))) |
| 49 | 9 | zred 12722 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 𝐵 ∈ ℝ) |
| 50 | 20, 24 | nndivred 12320 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐴 / (2↑𝐶)) ∈ ℝ) |
| 51 | 27 | nnred 12281 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (2↑𝐷) ∈ ℝ) |
| 52 | 27 | nngt0d 12315 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → 0 < (2↑𝐷)) |
| 53 | | ltdivmul2 12145 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ ∧ (𝐴 / (2↑𝐶)) ∈ ℝ ∧ ((2↑𝐷) ∈ ℝ ∧ 0 <
(2↑𝐷))) → ((𝐵 / (2↑𝐷)) < (𝐴 / (2↑𝐶)) ↔ 𝐵 < ((𝐴 / (2↑𝐶)) · (2↑𝐷)))) |
| 54 | 49, 50, 51, 52, 53 | syl112anc 1376 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐵 / (2↑𝐷)) < (𝐴 / (2↑𝐶)) ↔ 𝐵 < ((𝐴 / (2↑𝐶)) · (2↑𝐷)))) |
| 55 | | peano2re 11434 |
. . . . . . . . 9
⊢ (𝐵 ∈ ℝ → (𝐵 + 1) ∈
ℝ) |
| 56 | 49, 55 | syl 17 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐵 + 1) ∈ ℝ) |
| 57 | | ledivmul2 12147 |
. . . . . . . 8
⊢ (((𝐵 + 1) ∈ ℝ ∧
(𝐴 / (2↑𝐶)) ∈ ℝ ∧
((2↑𝐷) ∈ ℝ
∧ 0 < (2↑𝐷)))
→ (((𝐵 + 1) /
(2↑𝐷)) ≤ (𝐴 / (2↑𝐶)) ↔ (𝐵 + 1) ≤ ((𝐴 / (2↑𝐶)) · (2↑𝐷)))) |
| 58 | 56, 50, 51, 52, 57 | syl112anc 1376 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((𝐵 + 1) / (2↑𝐷)) ≤ (𝐴 / (2↑𝐶)) ↔ (𝐵 + 1) ≤ ((𝐴 / (2↑𝐶)) · (2↑𝐷)))) |
| 59 | 48, 54, 58 | 3bitr4d 311 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐵 / (2↑𝐷)) < (𝐴 / (2↑𝐶)) ↔ ((𝐵 + 1) / (2↑𝐷)) ≤ (𝐴 / (2↑𝐶)))) |
| 60 | 49, 27 | nndivred 12320 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐵 / (2↑𝐷)) ∈ ℝ) |
| 61 | 60 | rexrd 11311 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐵 / (2↑𝐷)) ∈
ℝ*) |
| 62 | 56, 27 | nndivred 12320 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐵 + 1) / (2↑𝐷)) ∈ ℝ) |
| 63 | 62 | rexrd 11311 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐵 + 1) / (2↑𝐷)) ∈
ℝ*) |
| 64 | 50 | rexrd 11311 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐴 / (2↑𝐶)) ∈
ℝ*) |
| 65 | | peano2re 11434 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ℝ → (𝐴 + 1) ∈
ℝ) |
| 66 | 20, 65 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐴 + 1) ∈ ℝ) |
| 67 | 66, 24 | nndivred 12320 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ) |
| 68 | 67 | rexrd 11311 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐴 + 1) / (2↑𝐶)) ∈
ℝ*) |
| 69 | | ioodisj 13522 |
. . . . . . . 8
⊢
(((((𝐵 /
(2↑𝐷)) ∈
ℝ* ∧ ((𝐵 + 1) / (2↑𝐷)) ∈ ℝ*) ∧ ((𝐴 / (2↑𝐶)) ∈ ℝ* ∧ ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ*))
∧ ((𝐵 + 1) /
(2↑𝐷)) ≤ (𝐴 / (2↑𝐶))) → (((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) ∩ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶)))) = ∅) |
| 70 | 69 | ex 412 |
. . . . . . 7
⊢ ((((𝐵 / (2↑𝐷)) ∈ ℝ* ∧ ((𝐵 + 1) / (2↑𝐷)) ∈ ℝ*)
∧ ((𝐴 / (2↑𝐶)) ∈ ℝ*
∧ ((𝐴 + 1) /
(2↑𝐶)) ∈
ℝ*)) → (((𝐵 + 1) / (2↑𝐷)) ≤ (𝐴 / (2↑𝐶)) → (((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) ∩ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶)))) = ∅)) |
| 71 | 61, 63, 64, 68, 70 | syl22anc 839 |
. . . . . 6
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((𝐵 + 1) / (2↑𝐷)) ≤ (𝐴 / (2↑𝐶)) → (((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) ∩ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶)))) = ∅)) |
| 72 | 59, 71 | sylbid 240 |
. . . . 5
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐵 / (2↑𝐷)) < (𝐴 / (2↑𝐶)) → (((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) ∩ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶)))) = ∅)) |
| 73 | 72 | imp 406 |
. . . 4
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐵 / (2↑𝐷)) < (𝐴 / (2↑𝐶))) → (((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))) ∩ ((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶)))) = ∅) |
| 74 | 19, 73 | eqtrd 2777 |
. . 3
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐵 / (2↑𝐷)) < (𝐴 / (2↑𝐶))) → (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅) |
| 75 | 74 | 3mix3d 1339 |
. 2
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐵 / (2↑𝐷)) < (𝐴 / (2↑𝐶))) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) |
| 76 | 50 | adantr 480 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → (𝐴 / (2↑𝐶)) ∈ ℝ) |
| 77 | 67 | adantr 480 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ) |
| 78 | | simprl 771 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → (𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) |
| 79 | 66 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐴 + 1) ∈ ℂ) |
| 80 | 79, 25, 28, 29 | div13d 12067 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)) = (((2↑𝐷) / (2↑𝐶)) · (𝐴 + 1))) |
| 81 | 1 | peano2zd 12725 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐴 + 1) ∈ ℤ) |
| 82 | 44, 81 | zmulcld 12728 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((2↑𝐷) / (2↑𝐶)) · (𝐴 + 1)) ∈ ℤ) |
| 83 | 80, 82 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)) ∈ ℤ) |
| 84 | | zltp1le 12667 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℤ ∧ (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)) ∈ ℤ) → (𝐵 < (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)) ↔ (𝐵 + 1) ≤ (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)))) |
| 85 | 9, 83, 84 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (𝐵 < (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)) ↔ (𝐵 + 1) ≤ (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)))) |
| 86 | | ltdivmul2 12145 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ ℝ ∧ ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ ∧
((2↑𝐷) ∈ ℝ
∧ 0 < (2↑𝐷)))
→ ((𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)) ↔ 𝐵 < (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)))) |
| 87 | 49, 67, 51, 52, 86 | syl112anc 1376 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)) ↔ 𝐵 < (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)))) |
| 88 | | ledivmul2 12147 |
. . . . . . . . . . 11
⊢ (((𝐵 + 1) ∈ ℝ ∧
((𝐴 + 1) / (2↑𝐶)) ∈ ℝ ∧
((2↑𝐷) ∈ ℝ
∧ 0 < (2↑𝐷)))
→ (((𝐵 + 1) /
(2↑𝐷)) ≤ ((𝐴 + 1) / (2↑𝐶)) ↔ (𝐵 + 1) ≤ (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)))) |
| 89 | 56, 67, 51, 52, 88 | syl112anc 1376 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((𝐵 + 1) / (2↑𝐷)) ≤ ((𝐴 + 1) / (2↑𝐶)) ↔ (𝐵 + 1) ≤ (((𝐴 + 1) / (2↑𝐶)) · (2↑𝐷)))) |
| 90 | 85, 87, 89 | 3bitr4d 311 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ((𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)) ↔ ((𝐵 + 1) / (2↑𝐷)) ≤ ((𝐴 + 1) / (2↑𝐶)))) |
| 91 | 90 | biimpa 476 |
. . . . . . . 8
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶))) → ((𝐵 + 1) / (2↑𝐷)) ≤ ((𝐴 + 1) / (2↑𝐶))) |
| 92 | 91 | adantrl 716 |
. . . . . . 7
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → ((𝐵 + 1) / (2↑𝐷)) ≤ ((𝐴 + 1) / (2↑𝐶))) |
| 93 | | iccss 13455 |
. . . . . . 7
⊢ ((((𝐴 / (2↑𝐶)) ∈ ℝ ∧ ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ ((𝐵 + 1) / (2↑𝐷)) ≤ ((𝐴 + 1) / (2↑𝐶)))) → ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷))) ⊆ ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
| 94 | 76, 77, 78, 92, 93 | syl22anc 839 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷))) ⊆ ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
| 95 | 12 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ([,]‘(𝐵𝐹𝐷)) = ([,]‘〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉)) |
| 96 | | df-ov 7434 |
. . . . . . . 8
⊢ ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷))) = ([,]‘〈(𝐵 / (2↑𝐷)), ((𝐵 + 1) / (2↑𝐷))〉) |
| 97 | 95, 96 | eqtr4di 2795 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ([,]‘(𝐵𝐹𝐷)) = ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷)))) |
| 98 | 97 | adantr 480 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → ([,]‘(𝐵𝐹𝐷)) = ((𝐵 / (2↑𝐷))[,]((𝐵 + 1) / (2↑𝐷)))) |
| 99 | 5 | fveq2d 6910 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ([,]‘(𝐴𝐹𝐶)) = ([,]‘〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉)) |
| 100 | | df-ov 7434 |
. . . . . . . 8
⊢ ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶))) = ([,]‘〈(𝐴 / (2↑𝐶)), ((𝐴 + 1) / (2↑𝐶))〉) |
| 101 | 99, 100 | eqtr4di 2795 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → ([,]‘(𝐴𝐹𝐶)) = ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
| 102 | 101 | adantr 480 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → ([,]‘(𝐴𝐹𝐶)) = ((𝐴 / (2↑𝐶))[,]((𝐴 + 1) / (2↑𝐶)))) |
| 103 | 94, 98, 102 | 3sstr4d 4039 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶))) |
| 104 | 103 | 3mix2d 1338 |
. . . 4
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶)))) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) |
| 105 | 104 | anassrs 467 |
. . 3
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) ∧ (𝐵 / (2↑𝐷)) < ((𝐴 + 1) / (2↑𝐶))) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) |
| 106 | 16 | adantr 480 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 + 1) / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = (((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))) ∩ ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷))))) |
| 107 | | ioodisj 13522 |
. . . . . . . . 9
⊢
(((((𝐴 /
(2↑𝐶)) ∈
ℝ* ∧ ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ*) ∧ ((𝐵 / (2↑𝐷)) ∈ ℝ* ∧ ((𝐵 + 1) / (2↑𝐷)) ∈ ℝ*))
∧ ((𝐴 + 1) /
(2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → (((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))) ∩ ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷)))) = ∅) |
| 108 | 107 | ex 412 |
. . . . . . . 8
⊢ ((((𝐴 / (2↑𝐶)) ∈ ℝ* ∧ ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ*)
∧ ((𝐵 / (2↑𝐷)) ∈ ℝ*
∧ ((𝐵 + 1) /
(2↑𝐷)) ∈
ℝ*)) → (((𝐴 + 1) / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) → (((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))) ∩ ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷)))) = ∅)) |
| 109 | 64, 68, 61, 63, 108 | syl22anc 839 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (((𝐴 + 1) / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷)) → (((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))) ∩ ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷)))) = ∅)) |
| 110 | 109 | imp 406 |
. . . . . 6
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 + 1) / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → (((𝐴 / (2↑𝐶))(,)((𝐴 + 1) / (2↑𝐶))) ∩ ((𝐵 / (2↑𝐷))(,)((𝐵 + 1) / (2↑𝐷)))) = ∅) |
| 111 | 106, 110 | eqtrd 2777 |
. . . . 5
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 + 1) / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅) |
| 112 | 111 | 3mix3d 1339 |
. . . 4
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ ((𝐴 + 1) / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) |
| 113 | 112 | adantlr 715 |
. . 3
⊢
((((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) ∧ ((𝐴 + 1) / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) |
| 114 | 60 | adantr 480 |
. . 3
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → (𝐵 / (2↑𝐷)) ∈ ℝ) |
| 115 | 67 | adantr 480 |
. . 3
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → ((𝐴 + 1) / (2↑𝐶)) ∈ ℝ) |
| 116 | 105, 113,
114, 115 | ltlecasei 11369 |
. 2
⊢
(((((𝐴 ∈
ℤ ∧ 𝐵 ∈
ℤ) ∧ (𝐶 ∈
ℕ0 ∧ 𝐷
∈ ℕ0)) ∧ 𝐶 ≤ 𝐷) ∧ (𝐴 / (2↑𝐶)) ≤ (𝐵 / (2↑𝐷))) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) |
| 117 | 75, 116, 60, 50 | ltlecasei 11369 |
1
⊢ ((((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℕ0
∧ 𝐷 ∈
ℕ0)) ∧ 𝐶 ≤ 𝐷) → (([,]‘(𝐴𝐹𝐶)) ⊆ ([,]‘(𝐵𝐹𝐷)) ∨ ([,]‘(𝐵𝐹𝐷)) ⊆ ([,]‘(𝐴𝐹𝐶)) ∨ (((,)‘(𝐴𝐹𝐶)) ∩ ((,)‘(𝐵𝐹𝐷))) = ∅)) |