| Step | Hyp | Ref
| Expression |
| 1 | | nnuz 12921 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
| 2 | | 1zzd 12648 |
. . 3
⊢ (𝐴 ∈ ℂ → 1 ∈
ℤ) |
| 3 | | halfcn 12481 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
| 4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (1 / 2)
∈ ℂ) |
| 5 | | halfre 12480 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
| 6 | | halfge0 12483 |
. . . . . . . . 9
⊢ 0 ≤ (1
/ 2) |
| 7 | | absid 15335 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
| 8 | 5, 6, 7 | mp2an 692 |
. . . . . . . 8
⊢
(abs‘(1 / 2)) = (1 / 2) |
| 9 | | halflt1 12484 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
| 10 | 8, 9 | eqbrtri 5164 |
. . . . . . 7
⊢
(abs‘(1 / 2)) < 1 |
| 11 | 10 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(1 / 2)) < 1) |
| 12 | 4, 11 | expcnv 15900 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))
⇝ 0) |
| 13 | | id 22 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
| 14 | | geo2lim.1 |
. . . . . . 7
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) |
| 15 | | nnex 12272 |
. . . . . . . 8
⊢ ℕ
∈ V |
| 16 | 15 | mptex 7243 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) ∈ V |
| 17 | 14, 16 | eqeltri 2837 |
. . . . . 6
⊢ 𝐹 ∈ V |
| 18 | 17 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐹 ∈ V) |
| 19 | | nnnn0 12533 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
| 20 | 19 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
| 21 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((1 / 2)↑𝑘) = ((1 / 2)↑𝑗)) |
| 22 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘)) =
(𝑘 ∈
ℕ0 ↦ ((1 / 2)↑𝑘)) |
| 23 | | ovex 7464 |
. . . . . . . . 9
⊢ ((1 /
2)↑𝑗) ∈
V |
| 24 | 21, 22, 23 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗) = ((1 / 2)↑𝑗)) |
| 25 | 20, 24 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) = ((1 / 2)↑𝑗)) |
| 26 | | 2cn 12341 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
| 27 | | 2ne0 12370 |
. . . . . . . 8
⊢ 2 ≠
0 |
| 28 | | nnz 12634 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
| 29 | 28 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℤ) |
| 30 | | exprec 14144 |
. . . . . . . 8
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 𝑗 ∈ ℤ) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗))) |
| 31 | 26, 27, 29, 30 | mp3an12i 1467 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((1 /
2)↑𝑗) = (1 /
(2↑𝑗))) |
| 32 | 25, 31 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) = (1 / (2↑𝑗))) |
| 33 | | 2nn 12339 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
| 34 | | nnexpcl 14115 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
| 35 | 33, 20, 34 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
ℕ) |
| 36 | 35 | nnrecred 12317 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (1 /
(2↑𝑗)) ∈
ℝ) |
| 37 | 36 | recnd 11289 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (1 /
(2↑𝑗)) ∈
ℂ) |
| 38 | 32, 37 | eqeltrd 2841 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) ∈ ℂ) |
| 39 | | simpl 482 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝐴 ∈
ℂ) |
| 40 | 35 | nncnd 12282 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
ℂ) |
| 41 | 35 | nnne0d 12316 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ≠
0) |
| 42 | 39, 40, 41 | divrecd 12046 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 / (2↑𝑗)) = (𝐴 · (1 / (2↑𝑗)))) |
| 43 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (2↑𝑘) = (2↑𝑗)) |
| 44 | 43 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑𝑗))) |
| 45 | | ovex 7464 |
. . . . . . . 8
⊢ (𝐴 / (2↑𝑗)) ∈ V |
| 46 | 44, 14, 45 | fvmpt 7016 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = (𝐴 / (2↑𝑗))) |
| 47 | 46 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐴 / (2↑𝑗))) |
| 48 | 32 | oveq2d 7447 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 · ((𝑘 ∈ ℕ0 ↦ ((1 /
2)↑𝑘))‘𝑗)) = (𝐴 · (1 / (2↑𝑗)))) |
| 49 | 42, 47, 48 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐴 · ((𝑘 ∈ ℕ0 ↦ ((1 /
2)↑𝑘))‘𝑗))) |
| 50 | 1, 2, 12, 13, 18, 38, 49 | climmulc2 15673 |
. . . 4
⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ (𝐴 · 0)) |
| 51 | | mul01 11440 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) =
0) |
| 52 | 50, 51 | breqtrd 5169 |
. . 3
⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0) |
| 53 | | seqex 14044 |
. . . 4
⊢ seq1( + ,
𝐹) ∈
V |
| 54 | 53 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ∈
V) |
| 55 | 39, 40, 41 | divcld 12043 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 / (2↑𝑗)) ∈ ℂ) |
| 56 | 47, 55 | eqeltrd 2841 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ) |
| 57 | 47 | oveq2d 7447 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 − (𝐹‘𝑗)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
| 58 | | geo2sum 15909 |
. . . . 5
⊢ ((𝑗 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
| 59 | 58 | ancoms 458 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
| 60 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ) |
| 61 | 60 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ) |
| 62 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛)) |
| 63 | 62 | oveq2d 7447 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑𝑛))) |
| 64 | | ovex 7464 |
. . . . . . 7
⊢ (𝐴 / (2↑𝑛)) ∈ V |
| 65 | 63, 14, 64 | fvmpt 7016 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = (𝐴 / (2↑𝑛))) |
| 66 | 61, 65 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐹‘𝑛) = (𝐴 / (2↑𝑛))) |
| 67 | | simpr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ) |
| 68 | 67, 1 | eleqtrdi 2851 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
| 69 | | simpll 767 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝐴 ∈ ℂ) |
| 70 | | nnnn0 12533 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
| 71 | | nnexpcl 14115 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
| 72 | 33, 70, 71 | sylancr 587 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) |
| 73 | 61, 72 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ∈ ℕ) |
| 74 | 73 | nncnd 12282 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ∈ ℂ) |
| 75 | 73 | nnne0d 12316 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ≠ 0) |
| 76 | 69, 74, 75 | divcld 12043 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐴 / (2↑𝑛)) ∈ ℂ) |
| 77 | 66, 68, 76 | fsumser 15766 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (seq1( + , 𝐹)‘𝑗)) |
| 78 | 57, 59, 77 | 3eqtr2rd 2784 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) = (𝐴 − (𝐹‘𝑗))) |
| 79 | 1, 2, 52, 13, 54, 56, 78 | climsubc2 15675 |
. 2
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ⇝ (𝐴 − 0)) |
| 80 | | subid1 11529 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) |
| 81 | 79, 80 | breqtrd 5169 |
1
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ⇝ 𝐴) |