Proof of Theorem aaliou3lem3
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . 3
⊢
(ℤ≥‘𝐴) = (ℤ≥‘𝐴) | 
| 2 |  | nnz 12634 | . . . 4
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℤ) | 
| 3 |  | uzid 12893 | . . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) | 
| 4 | 2, 3 | syl 17 | . . 3
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
(ℤ≥‘𝐴)) | 
| 5 |  | aaliou3lem.a | . . . 4
⊢ 𝐺 = (𝑐 ∈ (ℤ≥‘𝐴) ↦
((2↑-(!‘𝐴))
· ((1 / 2)↑(𝑐
− 𝐴)))) | 
| 6 | 5 | aaliou3lem1 26384 | . . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) ∈ ℝ) | 
| 7 |  | aaliou3lem.b | . . . . . 6
⊢ 𝐹 = (𝑎 ∈ ℕ ↦
(2↑-(!‘𝑎))) | 
| 8 | 5, 7 | aaliou3lem2 26385 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏))) | 
| 9 |  | 0xr 11308 | . . . . . 6
⊢ 0 ∈
ℝ* | 
| 10 |  | elioc2 13450 | . . . . . 6
⊢ ((0
∈ ℝ* ∧ (𝐺‘𝑏) ∈ ℝ) → ((𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏)) ↔ ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏)))) | 
| 11 | 9, 6, 10 | sylancr 587 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝑏) ∈ (0(,](𝐺‘𝑏)) ↔ ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏)))) | 
| 12 | 8, 11 | mpbid 232 | . . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → ((𝐹‘𝑏) ∈ ℝ ∧ 0 < (𝐹‘𝑏) ∧ (𝐹‘𝑏) ≤ (𝐺‘𝑏))) | 
| 13 | 12 | simp1d 1143 | . . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈ ℝ) | 
| 14 |  | halfcn 12481 | . . . . . 6
⊢ (1 / 2)
∈ ℂ | 
| 15 | 14 | a1i 11 | . . . . 5
⊢ (𝐴 ∈ ℕ → (1 / 2)
∈ ℂ) | 
| 16 |  | halfre 12480 | . . . . . . . . 9
⊢ (1 / 2)
∈ ℝ | 
| 17 |  | halfgt0 12482 | . . . . . . . . 9
⊢ 0 < (1
/ 2) | 
| 18 | 16, 17 | elrpii 13037 | . . . . . . . 8
⊢ (1 / 2)
∈ ℝ+ | 
| 19 |  | rprege0 13050 | . . . . . . . 8
⊢ ((1 / 2)
∈ ℝ+ → ((1 / 2) ∈ ℝ ∧ 0 ≤ (1 /
2))) | 
| 20 |  | absid 15335 | . . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) | 
| 21 | 18, 19, 20 | mp2b 10 | . . . . . . 7
⊢
(abs‘(1 / 2)) = (1 / 2) | 
| 22 |  | halflt1 12484 | . . . . . . 7
⊢ (1 / 2)
< 1 | 
| 23 | 21, 22 | eqbrtri 5164 | . . . . . 6
⊢
(abs‘(1 / 2)) < 1 | 
| 24 | 23 | a1i 11 | . . . . 5
⊢ (𝐴 ∈ ℕ →
(abs‘(1 / 2)) < 1) | 
| 25 |  | 2rp 13039 | . . . . . . 7
⊢ 2 ∈
ℝ+ | 
| 26 |  | nnnn0 12533 | . . . . . . . . . 10
⊢ (𝐴 ∈ ℕ → 𝐴 ∈
ℕ0) | 
| 27 | 26 | faccld 14323 | . . . . . . . . 9
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℕ) | 
| 28 | 27 | nnzd 12640 | . . . . . . . 8
⊢ (𝐴 ∈ ℕ →
(!‘𝐴) ∈
ℤ) | 
| 29 | 28 | znegcld 12724 | . . . . . . 7
⊢ (𝐴 ∈ ℕ →
-(!‘𝐴) ∈
ℤ) | 
| 30 |  | rpexpcl 14121 | . . . . . . 7
⊢ ((2
∈ ℝ+ ∧ -(!‘𝐴) ∈ ℤ) →
(2↑-(!‘𝐴))
∈ ℝ+) | 
| 31 | 25, 29, 30 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℝ+) | 
| 32 | 31 | rpcnd 13079 | . . . . 5
⊢ (𝐴 ∈ ℕ →
(2↑-(!‘𝐴))
∈ ℂ) | 
| 33 | 2, 15, 24, 32, 5 | geolim3 26381 | . . . 4
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐺) ⇝ ((2↑-(!‘𝐴)) / (1 − (1 /
2)))) | 
| 34 |  | seqex 14044 | . . . . 5
⊢ seq𝐴( + , 𝐺) ∈ V | 
| 35 |  | ovex 7464 | . . . . 5
⊢
((2↑-(!‘𝐴)) / (1 − (1 / 2))) ∈
V | 
| 36 | 34, 35 | breldm 5919 | . . . 4
⊢ (seq𝐴( + , 𝐺) ⇝ ((2↑-(!‘𝐴)) / (1 − (1 / 2))) →
seq𝐴( + , 𝐺) ∈ dom ⇝ ) | 
| 37 | 33, 36 | syl 17 | . . 3
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐺) ∈ dom ⇝ ) | 
| 38 | 12 | simp2d 1144 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → 0 < (𝐹‘𝑏)) | 
| 39 | 13, 38 | elrpd 13074 | . . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ∈
ℝ+) | 
| 40 | 39 | rpge0d 13081 | . . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → 0 ≤ (𝐹‘𝑏)) | 
| 41 | 12 | simp3d 1145 | . . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) ≤ (𝐺‘𝑏)) | 
| 42 | 1, 4, 6, 13, 37, 40, 41 | cvgcmp 15852 | . 2
⊢ (𝐴 ∈ ℕ → seq𝐴( + , 𝐹) ∈ dom ⇝ ) | 
| 43 |  | eqidd 2738 | . . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝑏) = (𝐹‘𝑏)) | 
| 44 | 1, 1, 4, 43, 39, 42 | isumrpcl 15879 | . 2
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ∈
ℝ+) | 
| 45 |  | eqidd 2738 | . . . 4
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) = (𝐺‘𝑏)) | 
| 46 | 1, 2, 43, 13, 45, 6, 41, 42, 37 | isumle 15880 | . . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ Σ𝑏 ∈ (ℤ≥‘𝐴)(𝐺‘𝑏)) | 
| 47 | 6 | recnd 11289 | . . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝑏 ∈
(ℤ≥‘𝐴)) → (𝐺‘𝑏) ∈ ℂ) | 
| 48 | 1, 2, 45, 47, 33 | isumclim 15793 | . . . 4
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐺‘𝑏) = ((2↑-(!‘𝐴)) / (1 − (1 / 2)))) | 
| 49 |  | 1mhlfehlf 12485 | . . . . . 6
⊢ (1
− (1 / 2)) = (1 / 2) | 
| 50 | 49 | oveq2i 7442 | . . . . 5
⊢
((2↑-(!‘𝐴)) / (1 − (1 / 2))) =
((2↑-(!‘𝐴)) / (1
/ 2)) | 
| 51 |  | 2cn 12341 | . . . . . . . 8
⊢ 2 ∈
ℂ | 
| 52 |  | mulcl 11239 | . . . . . . . 8
⊢
(((2↑-(!‘𝐴)) ∈ ℂ ∧ 2 ∈ ℂ)
→ ((2↑-(!‘𝐴)) · 2) ∈
ℂ) | 
| 53 | 32, 51, 52 | sylancl 586 | . . . . . . 7
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴))
· 2) ∈ ℂ) | 
| 54 | 53 | div1d 12035 | . . . . . 6
⊢ (𝐴 ∈ ℕ →
(((2↑-(!‘𝐴))
· 2) / 1) = ((2↑-(!‘𝐴)) · 2)) | 
| 55 |  | 1rp 13038 | . . . . . . . . 9
⊢ 1 ∈
ℝ+ | 
| 56 |  | rpcnne0 13053 | . . . . . . . . 9
⊢ (1 ∈
ℝ+ → (1 ∈ ℂ ∧ 1 ≠ 0)) | 
| 57 | 55, 56 | ax-mp 5 | . . . . . . . 8
⊢ (1 ∈
ℂ ∧ 1 ≠ 0) | 
| 58 |  | 2cnne0 12476 | . . . . . . . 8
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) | 
| 59 |  | divdiv2 11979 | . . . . . . . 8
⊢
(((2↑-(!‘𝐴)) ∈ ℂ ∧ (1 ∈ ℂ
∧ 1 ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) | 
| 60 | 57, 58, 59 | mp3an23 1455 | . . . . . . 7
⊢
((2↑-(!‘𝐴)) ∈ ℂ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) | 
| 61 | 32, 60 | syl 17 | . . . . . 6
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (((2↑-(!‘𝐴)) · 2) / 1)) | 
| 62 |  | mulcom 11241 | . . . . . . 7
⊢ ((2
∈ ℂ ∧ (2↑-(!‘𝐴)) ∈ ℂ) → (2 ·
(2↑-(!‘𝐴))) =
((2↑-(!‘𝐴))
· 2)) | 
| 63 | 51, 32, 62 | sylancr 587 | . . . . . 6
⊢ (𝐴 ∈ ℕ → (2
· (2↑-(!‘𝐴))) = ((2↑-(!‘𝐴)) · 2)) | 
| 64 | 54, 61, 63 | 3eqtr4d 2787 | . . . . 5
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
/ 2)) = (2 · (2↑-(!‘𝐴)))) | 
| 65 | 50, 64 | eqtrid 2789 | . . . 4
⊢ (𝐴 ∈ ℕ →
((2↑-(!‘𝐴)) / (1
− (1 / 2))) = (2 · (2↑-(!‘𝐴)))) | 
| 66 | 48, 65 | eqtrd 2777 | . . 3
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐺‘𝑏) = (2 · (2↑-(!‘𝐴)))) | 
| 67 | 46, 66 | breqtrd 5169 | . 2
⊢ (𝐴 ∈ ℕ →
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴)))) | 
| 68 | 42, 44, 67 | 3jca 1129 | 1
⊢ (𝐴 ∈ ℕ → (seq𝐴( + , 𝐹) ∈ dom ⇝ ∧ Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ∈ ℝ+ ∧
Σ𝑏 ∈
(ℤ≥‘𝐴)(𝐹‘𝑏) ≤ (2 · (2↑-(!‘𝐴))))) |