Step | Hyp | Ref
| Expression |
1 | | 1zzd 9189 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 1 ∈
ℤ) |
2 | | nnz 9181 |
. . . 4
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
3 | 2 | adantr 274 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 𝑁 ∈
ℤ) |
4 | | simplr 520 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝐴 ∈ ℂ) |
5 | | 2nn 8989 |
. . . . . 6
⊢ 2 ∈
ℕ |
6 | | elfznn 9951 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
7 | 6 | adantl 275 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ) |
8 | 7 | nnnn0d 9138 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ0) |
9 | | nnexpcl 10427 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ 𝑘
∈ ℕ0) → (2↑𝑘) ∈ ℕ) |
10 | 5, 8, 9 | sylancr 411 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (2↑𝑘) ∈ ℕ) |
11 | 10 | nncnd 8842 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (2↑𝑘) ∈ ℂ) |
12 | 10 | nnap0d 8874 |
. . . 4
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (2↑𝑘) # 0) |
13 | 4, 11, 12 | divclapd 8658 |
. . 3
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑘 ∈ (1...𝑁)) → (𝐴 / (2↑𝑘)) ∈ ℂ) |
14 | | oveq2 5829 |
. . . 4
⊢ (𝑘 = (𝑗 + 1) → (2↑𝑘) = (2↑(𝑗 + 1))) |
15 | 14 | oveq2d 5837 |
. . 3
⊢ (𝑘 = (𝑗 + 1) → (𝐴 / (2↑𝑘)) = (𝐴 / (2↑(𝑗 + 1)))) |
16 | 1, 1, 3, 13, 15 | fsumshftm 11337 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑘 ∈ (1...𝑁)(𝐴 / (2↑𝑘)) = Σ𝑗 ∈ ((1 − 1)...(𝑁 − 1))(𝐴 / (2↑(𝑗 + 1)))) |
17 | | 1m1e0 8897 |
. . . . 5
⊢ (1
− 1) = 0 |
18 | 17 | oveq1i 5831 |
. . . 4
⊢ ((1
− 1)...(𝑁 − 1))
= (0...(𝑁 −
1)) |
19 | 18 | sumeq1i 11255 |
. . 3
⊢
Σ𝑗 ∈ ((1
− 1)...(𝑁 −
1))(𝐴 / (2↑(𝑗 + 1))) = Σ𝑗 ∈ (0...(𝑁 − 1))(𝐴 / (2↑(𝑗 + 1))) |
20 | | halfcn 9042 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℂ |
21 | | elfznn0 10011 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℕ0) |
22 | 21 | adantl 275 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝑗 ∈ ℕ0) |
23 | | expcl 10432 |
. . . . . . . . . 10
⊢ (((1 / 2)
∈ ℂ ∧ 𝑗
∈ ℕ0) → ((1 / 2)↑𝑗) ∈ ℂ) |
24 | 20, 22, 23 | sylancr 411 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((1 / 2)↑𝑗) ∈
ℂ) |
25 | | 2cnd 8901 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 2 ∈
ℂ) |
26 | | 2ap0 8921 |
. . . . . . . . . 10
⊢ 2 #
0 |
27 | 26 | a1i 9 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 2 # 0) |
28 | 24, 25, 27 | divrecapd 8661 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((1 / 2)↑𝑗) / 2) = (((1 / 2)↑𝑗) · (1 /
2))) |
29 | | expp1 10421 |
. . . . . . . . 9
⊢ (((1 / 2)
∈ ℂ ∧ 𝑗
∈ ℕ0) → ((1 / 2)↑(𝑗 + 1)) = (((1 / 2)↑𝑗) · (1 / 2))) |
30 | 20, 22, 29 | sylancr 411 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((1 / 2)↑(𝑗 + 1)) = (((1 / 2)↑𝑗) · (1 /
2))) |
31 | | elfzelz 9923 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → 𝑗 ∈ ℤ) |
32 | 31 | peano2zd 9284 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (0...(𝑁 − 1)) → (𝑗 + 1) ∈ ℤ) |
33 | 32 | adantl 275 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈ ℤ) |
34 | 25, 27, 33 | exprecapd 10554 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → ((1 / 2)↑(𝑗 + 1)) = (1 / (2↑(𝑗 + 1)))) |
35 | 28, 30, 34 | 3eqtr2rd 2197 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (1 / (2↑(𝑗 + 1))) = (((1 / 2)↑𝑗) / 2)) |
36 | 35 | oveq2d 5837 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝐴 · (1 / (2↑(𝑗 + 1)))) = (𝐴 · (((1 / 2)↑𝑗) / 2))) |
37 | | simplr 520 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
38 | | peano2nn0 9125 |
. . . . . . . . . 10
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
39 | 22, 38 | syl 14 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝑗 + 1) ∈
ℕ0) |
40 | | nnexpcl 10427 |
. . . . . . . . 9
⊢ ((2
∈ ℕ ∧ (𝑗 +
1) ∈ ℕ0) → (2↑(𝑗 + 1)) ∈ ℕ) |
41 | 5, 39, 40 | sylancr 411 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (2↑(𝑗 + 1)) ∈
ℕ) |
42 | 41 | nncnd 8842 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (2↑(𝑗 + 1)) ∈
ℂ) |
43 | 41 | nnap0d 8874 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (2↑(𝑗 + 1)) # 0) |
44 | 37, 42, 43 | divrecapd 8661 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝐴 / (2↑(𝑗 + 1))) = (𝐴 · (1 / (2↑(𝑗 + 1))))) |
45 | 24, 37, 25, 27 | div12apd 8695 |
. . . . . 6
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (((1 / 2)↑𝑗) · (𝐴 / 2)) = (𝐴 · (((1 / 2)↑𝑗) / 2))) |
46 | 36, 44, 45 | 3eqtr4d 2200 |
. . . . 5
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) ∧ 𝑗 ∈ (0...(𝑁 − 1))) → (𝐴 / (2↑(𝑗 + 1))) = (((1 / 2)↑𝑗) · (𝐴 / 2))) |
47 | 46 | sumeq2dv 11260 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑗 ∈ (0...(𝑁 − 1))(𝐴 / (2↑(𝑗 + 1))) = Σ𝑗 ∈ (0...(𝑁 − 1))(((1 / 2)↑𝑗) · (𝐴 / 2))) |
48 | | 0zd 9174 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 0 ∈
ℤ) |
49 | 3, 1 | zsubcld 9286 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (𝑁 − 1) ∈
ℤ) |
50 | 48, 49 | fzfigd 10325 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
(0...(𝑁 − 1)) ∈
Fin) |
51 | | halfcl 9054 |
. . . . . 6
⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈
ℂ) |
52 | 51 | adantl 275 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (𝐴 / 2) ∈
ℂ) |
53 | 50, 52, 24 | fsummulc1 11341 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
(Σ𝑗 ∈
(0...(𝑁 − 1))((1 /
2)↑𝑗) · (𝐴 / 2)) = Σ𝑗 ∈ (0...(𝑁 − 1))(((1 / 2)↑𝑗) · (𝐴 / 2))) |
54 | 47, 53 | eqtr4d 2193 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑗 ∈ (0...(𝑁 − 1))(𝐴 / (2↑(𝑗 + 1))) = (Σ𝑗 ∈ (0...(𝑁 − 1))((1 / 2)↑𝑗) · (𝐴 / 2))) |
55 | 19, 54 | syl5eq 2202 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑗 ∈ ((1 −
1)...(𝑁 − 1))(𝐴 / (2↑(𝑗 + 1))) = (Σ𝑗 ∈ (0...(𝑁 − 1))((1 / 2)↑𝑗) · (𝐴 / 2))) |
56 | | 2cnd 8901 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 2 ∈
ℂ) |
57 | 26 | a1i 9 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 2 #
0) |
58 | 56, 57, 3 | exprecapd 10554 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → ((1 /
2)↑𝑁) = (1 /
(2↑𝑁))) |
59 | 58 | oveq2d 5837 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1
− ((1 / 2)↑𝑁)) =
(1 − (1 / (2↑𝑁)))) |
60 | | 1mhlfehlf 9046 |
. . . . . . 7
⊢ (1
− (1 / 2)) = (1 / 2) |
61 | 60 | a1i 9 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1
− (1 / 2)) = (1 / 2)) |
62 | 59, 61 | oveq12d 5839 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → ((1
− ((1 / 2)↑𝑁)) /
(1 − (1 / 2))) = ((1 − (1 / (2↑𝑁))) / (1 / 2))) |
63 | | simpr 109 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 𝐴 ∈
ℂ) |
64 | 63, 56, 57 | divrecap2d 8662 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (𝐴 / 2) = ((1 / 2) · 𝐴)) |
65 | 62, 64 | oveq12d 5839 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (((1
− ((1 / 2)↑𝑁)) /
(1 − (1 / 2))) · (𝐴 / 2)) = (((1 − (1 / (2↑𝑁))) / (1 / 2)) · ((1 / 2)
· 𝐴))) |
66 | | ax-1cn 7820 |
. . . . . . 7
⊢ 1 ∈
ℂ |
67 | | nnnn0 9092 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
68 | 67 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 𝑁 ∈
ℕ0) |
69 | | nnexpcl 10427 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ0) → (2↑𝑁) ∈ ℕ) |
70 | 5, 68, 69 | sylancr 411 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
(2↑𝑁) ∈
ℕ) |
71 | 70 | nnrecred 8875 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1 /
(2↑𝑁)) ∈
ℝ) |
72 | 71 | recnd 7901 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1 /
(2↑𝑁)) ∈
ℂ) |
73 | | subcl 8069 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ (1 / (2↑𝑁)) ∈ ℂ) → (1 − (1 /
(2↑𝑁))) ∈
ℂ) |
74 | 66, 72, 73 | sylancr 411 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1
− (1 / (2↑𝑁)))
∈ ℂ) |
75 | 20 | a1i 9 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1 / 2)
∈ ℂ) |
76 | 56, 57 | recap0d 8650 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1 / 2)
# 0) |
77 | 74, 75, 76 | divclapd 8658 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → ((1
− (1 / (2↑𝑁))) /
(1 / 2)) ∈ ℂ) |
78 | 77, 75, 63 | mulassd 7896 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → ((((1
− (1 / (2↑𝑁))) /
(1 / 2)) · (1 / 2)) · 𝐴) = (((1 − (1 / (2↑𝑁))) / (1 / 2)) · ((1 / 2)
· 𝐴))) |
79 | 74, 75, 76 | divcanap1d 8659 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (((1
− (1 / (2↑𝑁))) /
(1 / 2)) · (1 / 2)) = (1 − (1 / (2↑𝑁)))) |
80 | 79 | oveq1d 5836 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → ((((1
− (1 / (2↑𝑁))) /
(1 / 2)) · (1 / 2)) · 𝐴) = ((1 − (1 / (2↑𝑁))) · 𝐴)) |
81 | 65, 78, 80 | 3eqtr2d 2196 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (((1
− ((1 / 2)↑𝑁)) /
(1 − (1 / 2))) · (𝐴 / 2)) = ((1 − (1 / (2↑𝑁))) · 𝐴)) |
82 | | halfre 9041 |
. . . . . . 7
⊢ (1 / 2)
∈ ℝ |
83 | | 1re 7872 |
. . . . . . 7
⊢ 1 ∈
ℝ |
84 | | halflt1 9045 |
. . . . . . 7
⊢ (1 / 2)
< 1 |
85 | 82, 83, 84 | ltapii 8505 |
. . . . . 6
⊢ (1 / 2) #
1 |
86 | 85 | a1i 9 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1 / 2)
# 1) |
87 | 75, 86, 68 | geoserap 11399 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑗 ∈ (0...(𝑁 − 1))((1 / 2)↑𝑗) = ((1 − ((1 /
2)↑𝑁)) / (1 − (1
/ 2)))) |
88 | 87 | oveq1d 5836 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
(Σ𝑗 ∈
(0...(𝑁 − 1))((1 /
2)↑𝑗) · (𝐴 / 2)) = (((1 − ((1 /
2)↑𝑁)) / (1 − (1
/ 2))) · (𝐴 /
2))) |
89 | | mulid2 7871 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (1
· 𝐴) = 𝐴) |
90 | 89 | adantl 275 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (1
· 𝐴) = 𝐴) |
91 | 90 | eqcomd 2163 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 𝐴 = (1 · 𝐴)) |
92 | 70 | nncnd 8842 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
(2↑𝑁) ∈
ℂ) |
93 | 70 | nnap0d 8874 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
(2↑𝑁) #
0) |
94 | 63, 92, 93 | divrecap2d 8662 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (𝐴 / (2↑𝑁)) = ((1 / (2↑𝑁)) · 𝐴)) |
95 | 91, 94 | oveq12d 5839 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (𝐴 − (𝐴 / (2↑𝑁))) = ((1 · 𝐴) − ((1 / (2↑𝑁)) · 𝐴))) |
96 | 66 | a1i 9 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → 1 ∈
ℂ) |
97 | 96, 72, 63 | subdird 8285 |
. . . 4
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → ((1
− (1 / (2↑𝑁)))
· 𝐴) = ((1 ·
𝐴) − ((1 /
(2↑𝑁)) · 𝐴))) |
98 | 95, 97 | eqtr4d 2193 |
. . 3
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) → (𝐴 − (𝐴 / (2↑𝑁))) = ((1 − (1 / (2↑𝑁))) · 𝐴)) |
99 | 81, 88, 98 | 3eqtr4d 2200 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
(Σ𝑗 ∈
(0...(𝑁 − 1))((1 /
2)↑𝑗) · (𝐴 / 2)) = (𝐴 − (𝐴 / (2↑𝑁)))) |
100 | 16, 55, 99 | 3eqtrd 2194 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ) →
Σ𝑘 ∈ (1...𝑁)(𝐴 / (2↑𝑘)) = (𝐴 − (𝐴 / (2↑𝑁)))) |