Step | Hyp | Ref
| Expression |
1 | | nnuz 9522 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 9239 |
. . 3
⊢ (𝐴 ∈ ℂ → 1 ∈
ℤ) |
3 | | halfcn 9092 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
4 | 3 | a1i 9 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (1 / 2)
∈ ℂ) |
5 | | halfre 9091 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
6 | | halfge0 9094 |
. . . . . . . . 9
⊢ 0 ≤ (1
/ 2) |
7 | | absid 11035 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
8 | 5, 6, 7 | mp2an 424 |
. . . . . . . 8
⊢
(abs‘(1 / 2)) = (1 / 2) |
9 | | halflt1 9095 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
10 | 8, 9 | eqbrtri 4010 |
. . . . . . 7
⊢
(abs‘(1 / 2)) < 1 |
11 | 10 | a1i 9 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(1 / 2)) < 1) |
12 | 4, 11 | expcnv 11467 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))
⇝ 0) |
13 | | id 19 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
14 | | geo2lim.1 |
. . . . . . 7
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) |
15 | | nnex 8884 |
. . . . . . . 8
⊢ ℕ
∈ V |
16 | 15 | mptex 5722 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) ∈ V |
17 | 14, 16 | eqeltri 2243 |
. . . . . 6
⊢ 𝐹 ∈ V |
18 | 17 | a1i 9 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐹 ∈ V) |
19 | | nnnn0 9142 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
20 | 19 | adantl 275 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
21 | 3 | a1i 9 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (1 / 2)
∈ ℂ) |
22 | 21, 20 | expcld 10609 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((1 /
2)↑𝑗) ∈
ℂ) |
23 | | oveq2 5861 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → ((1 / 2)↑𝑘) = ((1 / 2)↑𝑗)) |
24 | | eqid 2170 |
. . . . . . . 8
⊢ (𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘)) =
(𝑘 ∈
ℕ0 ↦ ((1 / 2)↑𝑘)) |
25 | 23, 24 | fvmptg 5572 |
. . . . . . 7
⊢ ((𝑗 ∈ ℕ0
∧ ((1 / 2)↑𝑗)
∈ ℂ) → ((𝑘
∈ ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗) = ((1 / 2)↑𝑗)) |
26 | 20, 22, 25 | syl2anc 409 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) = ((1 / 2)↑𝑗)) |
27 | 26, 22 | eqeltrd 2247 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) ∈ ℂ) |
28 | | simpl 108 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝐴 ∈
ℂ) |
29 | | 2nn 9039 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
30 | | nnexpcl 10489 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
31 | 29, 20, 30 | sylancr 412 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
ℕ) |
32 | 31 | nncnd 8892 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
ℂ) |
33 | 31 | nnap0d 8924 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) #
0) |
34 | 28, 32, 33 | divrecapd 8710 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 / (2↑𝑗)) = (𝐴 · (1 / (2↑𝑗)))) |
35 | | simpr 109 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ) |
36 | 28, 32, 33 | divclapd 8707 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 / (2↑𝑗)) ∈ ℂ) |
37 | | oveq2 5861 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (2↑𝑘) = (2↑𝑗)) |
38 | 37 | oveq2d 5869 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑𝑗))) |
39 | 38, 14 | fvmptg 5572 |
. . . . . . 7
⊢ ((𝑗 ∈ ℕ ∧ (𝐴 / (2↑𝑗)) ∈ ℂ) → (𝐹‘𝑗) = (𝐴 / (2↑𝑗))) |
40 | 35, 36, 39 | syl2anc 409 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐴 / (2↑𝑗))) |
41 | | 2cn 8949 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
42 | | 2ap0 8971 |
. . . . . . . . 9
⊢ 2 #
0 |
43 | | nnz 9231 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
44 | 43 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℤ) |
45 | | exprecap 10517 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 2 # 0 ∧ 𝑗 ∈ ℤ) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗))) |
46 | 41, 42, 44, 45 | mp3an12i 1336 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((1 /
2)↑𝑗) = (1 /
(2↑𝑗))) |
47 | 26, 46 | eqtrd 2203 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) = (1 / (2↑𝑗))) |
48 | 47 | oveq2d 5869 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 · ((𝑘 ∈ ℕ0 ↦ ((1 /
2)↑𝑘))‘𝑗)) = (𝐴 · (1 / (2↑𝑗)))) |
49 | 34, 40, 48 | 3eqtr4d 2213 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐴 · ((𝑘 ∈ ℕ0 ↦ ((1 /
2)↑𝑘))‘𝑗))) |
50 | 1, 2, 12, 13, 18, 27, 49 | climmulc2 11294 |
. . . 4
⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ (𝐴 · 0)) |
51 | | mul01 8308 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) =
0) |
52 | 50, 51 | breqtrd 4015 |
. . 3
⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0) |
53 | | seqex 10403 |
. . . 4
⊢ seq1( + ,
𝐹) ∈
V |
54 | 53 | a1i 9 |
. . 3
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ∈
V) |
55 | 40, 36 | eqeltrd 2247 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ) |
56 | 40 | oveq2d 5869 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 − (𝐹‘𝑗)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
57 | | geo2sum 11477 |
. . . . 5
⊢ ((𝑗 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
58 | 57 | ancoms 266 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
59 | | elnnuz 9523 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↔ 𝑛 ∈
(ℤ≥‘1)) |
60 | 59 | biimpri 132 |
. . . . . . 7
⊢ (𝑛 ∈
(ℤ≥‘1) → 𝑛 ∈ ℕ) |
61 | 60 | adantl 275 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → 𝑛 ∈ ℕ) |
62 | | simpll 524 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → 𝐴 ∈ ℂ) |
63 | 41 | a1i 9 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → 2 ∈ ℂ) |
64 | 61 | nnnn0d 9188 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → 𝑛 ∈ ℕ0) |
65 | 63, 64 | expcld 10609 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → (2↑𝑛) ∈ ℂ) |
66 | 42 | a1i 9 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → 2 # 0) |
67 | 61 | nnzd 9333 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → 𝑛 ∈ ℤ) |
68 | 63, 66, 67 | expap0d 10615 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → (2↑𝑛) # 0) |
69 | 62, 65, 68 | divclapd 8707 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → (𝐴 / (2↑𝑛)) ∈ ℂ) |
70 | | oveq2 5861 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛)) |
71 | 70 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑𝑛))) |
72 | 71, 14 | fvmptg 5572 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ∧ (𝐴 / (2↑𝑛)) ∈ ℂ) → (𝐹‘𝑛) = (𝐴 / (2↑𝑛))) |
73 | 61, 69, 72 | syl2anc 409 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈
(ℤ≥‘1)) → (𝐹‘𝑛) = (𝐴 / (2↑𝑛))) |
74 | 35, 1 | eleqtrdi 2263 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
75 | 73, 74, 69 | fsum3ser 11360 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (seq1( + , 𝐹)‘𝑗)) |
76 | 56, 58, 75 | 3eqtr2rd 2210 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) = (𝐴 − (𝐹‘𝑗))) |
77 | 1, 2, 52, 13, 54, 55, 76 | climsubc2 11296 |
. 2
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ⇝ (𝐴 − 0)) |
78 | | subid1 8139 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) |
79 | 77, 78 | breqtrd 4015 |
1
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ⇝ 𝐴) |