Step | Hyp | Ref
| Expression |
1 | | nnuz 11599 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11285 |
. . 3
⊢ (𝐴 ∈ ℂ → 1 ∈
ℤ) |
3 | | halfcn 11124 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
4 | 3 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (1 / 2)
∈ ℂ) |
5 | | halfre 11123 |
. . . . . . . . 9
⊢ (1 / 2)
∈ ℝ |
6 | | 0re 9919 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ |
7 | | halfgt0 11125 |
. . . . . . . . . 10
⊢ 0 < (1
/ 2) |
8 | 6, 5, 7 | ltleii 10039 |
. . . . . . . . 9
⊢ 0 ≤ (1
/ 2) |
9 | | absid 13884 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℝ ∧ 0 ≤ (1 / 2)) → (abs‘(1 / 2)) = (1 /
2)) |
10 | 5, 8, 9 | mp2an 704 |
. . . . . . . 8
⊢
(abs‘(1 / 2)) = (1 / 2) |
11 | | halflt1 11127 |
. . . . . . . 8
⊢ (1 / 2)
< 1 |
12 | 10, 11 | eqbrtri 4604 |
. . . . . . 7
⊢
(abs‘(1 / 2)) < 1 |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(abs‘(1 / 2)) < 1) |
14 | 4, 13 | expcnv 14435 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))
⇝ 0) |
15 | | id 22 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐴 ∈
ℂ) |
16 | | geo2lim.1 |
. . . . . . 7
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) |
17 | | nnex 10903 |
. . . . . . . 8
⊢ ℕ
∈ V |
18 | 17 | mptex 6390 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ ↦ (𝐴 / (2↑𝑘))) ∈ V |
19 | 16, 18 | eqeltri 2684 |
. . . . . 6
⊢ 𝐹 ∈ V |
20 | 19 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ ℂ → 𝐹 ∈ V) |
21 | | nnnn0 11176 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℕ0) |
22 | 21 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ0) |
23 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → ((1 / 2)↑𝑘) = ((1 / 2)↑𝑗)) |
24 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘)) =
(𝑘 ∈
ℕ0 ↦ ((1 / 2)↑𝑘)) |
25 | | ovex 6577 |
. . . . . . . . 9
⊢ ((1 /
2)↑𝑗) ∈
V |
26 | 23, 24, 25 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ ((𝑘 ∈
ℕ0 ↦ ((1 / 2)↑𝑘))‘𝑗) = ((1 / 2)↑𝑗)) |
27 | 22, 26 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) = ((1 / 2)↑𝑗)) |
28 | | nnz 11276 |
. . . . . . . . 9
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
29 | 28 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℤ) |
30 | | 2cn 10968 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
31 | | 2ne0 10990 |
. . . . . . . . 9
⊢ 2 ≠
0 |
32 | | exprec 12763 |
. . . . . . . . 9
⊢ ((2
∈ ℂ ∧ 2 ≠ 0 ∧ 𝑗 ∈ ℤ) → ((1 / 2)↑𝑗) = (1 / (2↑𝑗))) |
33 | 30, 31, 32 | mp3an12 1406 |
. . . . . . . 8
⊢ (𝑗 ∈ ℤ → ((1 /
2)↑𝑗) = (1 /
(2↑𝑗))) |
34 | 29, 33 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((1 /
2)↑𝑗) = (1 /
(2↑𝑗))) |
35 | 27, 34 | eqtrd 2644 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) = (1 / (2↑𝑗))) |
36 | | 2nn 11062 |
. . . . . . . . 9
⊢ 2 ∈
ℕ |
37 | | nnexpcl 12735 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑗
∈ ℕ0) → (2↑𝑗) ∈ ℕ) |
38 | 36, 22, 37 | sylancr 694 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
ℕ) |
39 | 38 | nnrecred 10943 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (1 /
(2↑𝑗)) ∈
ℝ) |
40 | 39 | recnd 9947 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (1 /
(2↑𝑗)) ∈
ℂ) |
41 | 35, 40 | eqeltrd 2688 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → ((𝑘 ∈ ℕ0
↦ ((1 / 2)↑𝑘))‘𝑗) ∈ ℂ) |
42 | | simpl 472 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝐴 ∈
ℂ) |
43 | 38 | nncnd 10913 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ∈
ℂ) |
44 | 38 | nnne0d 10942 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
(2↑𝑗) ≠
0) |
45 | 42, 43, 44 | divrecd 10683 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 / (2↑𝑗)) = (𝐴 · (1 / (2↑𝑗)))) |
46 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑘 = 𝑗 → (2↑𝑘) = (2↑𝑗)) |
47 | 46 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑘 = 𝑗 → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑𝑗))) |
48 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐴 / (2↑𝑗)) ∈ V |
49 | 47, 16, 48 | fvmpt 6191 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = (𝐴 / (2↑𝑗))) |
50 | 49 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐴 / (2↑𝑗))) |
51 | 35 | oveq2d 6565 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 · ((𝑘 ∈ ℕ0 ↦ ((1 /
2)↑𝑘))‘𝑗)) = (𝐴 · (1 / (2↑𝑗)))) |
52 | 45, 50, 51 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = (𝐴 · ((𝑘 ∈ ℕ0 ↦ ((1 /
2)↑𝑘))‘𝑗))) |
53 | 1, 2, 14, 15, 20, 41, 52 | climmulc2 14215 |
. . . 4
⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ (𝐴 · 0)) |
54 | | mul01 10094 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐴 · 0) =
0) |
55 | 53, 54 | breqtrd 4609 |
. . 3
⊢ (𝐴 ∈ ℂ → 𝐹 ⇝ 0) |
56 | | seqex 12665 |
. . . 4
⊢ seq1( + ,
𝐹) ∈
V |
57 | 56 | a1i 11 |
. . 3
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ∈
V) |
58 | 42, 43, 44 | divcld 10680 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 / (2↑𝑗)) ∈ ℂ) |
59 | 50, 58 | eqeltrd 2688 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ) |
60 | 50 | oveq2d 6565 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (𝐴 − (𝐹‘𝑗)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
61 | | geo2sum 14443 |
. . . . 5
⊢ ((𝑗 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
62 | 61 | ancoms 468 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (𝐴 − (𝐴 / (2↑𝑗)))) |
63 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑛 ∈ (1...𝑗) → 𝑛 ∈ ℕ) |
64 | 63 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝑛 ∈ ℕ) |
65 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑘 = 𝑛 → (2↑𝑘) = (2↑𝑛)) |
66 | 65 | oveq2d 6565 |
. . . . . . 7
⊢ (𝑘 = 𝑛 → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑𝑛))) |
67 | | ovex 6577 |
. . . . . . 7
⊢ (𝐴 / (2↑𝑛)) ∈ V |
68 | 66, 16, 67 | fvmpt 6191 |
. . . . . 6
⊢ (𝑛 ∈ ℕ → (𝐹‘𝑛) = (𝐴 / (2↑𝑛))) |
69 | 64, 68 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐹‘𝑛) = (𝐴 / (2↑𝑛))) |
70 | | simpr 476 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
ℕ) |
71 | 70, 1 | syl6eleq 2698 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈
(ℤ≥‘1)) |
72 | | simpll 786 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → 𝐴 ∈ ℂ) |
73 | | nnnn0 11176 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → 𝑛 ∈
ℕ0) |
74 | | nnexpcl 12735 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ 𝑛
∈ ℕ0) → (2↑𝑛) ∈ ℕ) |
75 | 36, 73, 74 | sylancr 694 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ →
(2↑𝑛) ∈
ℕ) |
76 | 64, 75 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ∈ ℕ) |
77 | 76 | nncnd 10913 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ∈ ℂ) |
78 | 76 | nnne0d 10942 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (2↑𝑛) ≠ 0) |
79 | 72, 77, 78 | divcld 10680 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) ∧ 𝑛 ∈ (1...𝑗)) → (𝐴 / (2↑𝑛)) ∈ ℂ) |
80 | 69, 71, 79 | fsumser 14308 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) →
Σ𝑛 ∈ (1...𝑗)(𝐴 / (2↑𝑛)) = (seq1( + , 𝐹)‘𝑗)) |
81 | 60, 62, 80 | 3eqtr2rd 2651 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ) → (seq1( +
, 𝐹)‘𝑗) = (𝐴 − (𝐹‘𝑗))) |
82 | 1, 2, 55, 15, 57, 59, 81 | climsubc2 14217 |
. 2
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ⇝ (𝐴 − 0)) |
83 | | subid1 10180 |
. 2
⊢ (𝐴 ∈ ℂ → (𝐴 − 0) = 𝐴) |
84 | 82, 83 | breqtrd 4609 |
1
⊢ (𝐴 ∈ ℂ → seq1( + ,
𝐹) ⇝ 𝐴) |