# Metamath Proof Explorer

## Theorem geo2sum

Description: The value of the finite geometric series 2 ^ -u 1 + 2 ^ -u 2 + ... + 2 ^ -u N , multiplied by a constant. (Contributed by Mario Carneiro, 17-Mar-2014) (Revised by Mario Carneiro, 26-Apr-2014)

Ref Expression
Assertion geo2sum ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 / ( 2 ↑ 𝑘 ) ) = ( 𝐴 − ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) )

### Proof

Step Hyp Ref Expression
1 1zzd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → 1 ∈ ℤ )
2 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
3 2 adantr ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → 𝑁 ∈ ℤ )
4 simplr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 2nn 2 ∈ ℕ
6 elfznn ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
7 6 adantl ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
8 7 nnnn0d ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
9 nnexpcl ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ0 ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
10 5 8 9 sylancr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 ↑ 𝑘 ) ∈ ℕ )
11 10 nncnd ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 ↑ 𝑘 ) ∈ ℂ )
12 10 nnne0d ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 2 ↑ 𝑘 ) ≠ 0 )
13 4 11 12 divcld ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( 𝐴 / ( 2 ↑ 𝑘 ) ) ∈ ℂ )
14 oveq2 ( 𝑘 = ( 𝑗 + 1 ) → ( 2 ↑ 𝑘 ) = ( 2 ↑ ( 𝑗 + 1 ) ) )
15 14 oveq2d ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 / ( 2 ↑ 𝑘 ) ) = ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) ) )
16 1 1 3 13 15 fsumshftm ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 / ( 2 ↑ 𝑘 ) ) = Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) ) )
17 1m1e0 ( 1 − 1 ) = 0
18 17 oveq1i ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) = ( 0 ... ( 𝑁 − 1 ) )
19 18 sumeq1i Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) )
20 halfcn ( 1 / 2 ) ∈ ℂ
21 elfznn0 ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℕ0 )
22 21 adantl ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝑗 ∈ ℕ0 )
23 expcl ( ( ( 1 / 2 ) ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / 2 ) ↑ 𝑗 ) ∈ ℂ )
24 20 22 23 sylancr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 1 / 2 ) ↑ 𝑗 ) ∈ ℂ )
25 2cnd ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 2 ∈ ℂ )
26 2ne0 2 ≠ 0
27 26 a1i ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 2 ≠ 0 )
28 24 25 27 divrecd ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 1 / 2 ) ↑ 𝑗 ) / 2 ) = ( ( ( 1 / 2 ) ↑ 𝑗 ) · ( 1 / 2 ) ) )
29 expp1 ( ( ( 1 / 2 ) ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( ( 1 / 2 ) ↑ ( 𝑗 + 1 ) ) = ( ( ( 1 / 2 ) ↑ 𝑗 ) · ( 1 / 2 ) ) )
30 20 22 29 sylancr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 1 / 2 ) ↑ ( 𝑗 + 1 ) ) = ( ( ( 1 / 2 ) ↑ 𝑗 ) · ( 1 / 2 ) ) )
31 elfzelz ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑗 ∈ ℤ )
32 31 peano2zd ( 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( 𝑗 + 1 ) ∈ ℤ )
33 32 adantl ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℤ )
34 25 27 33 exprecd ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( 1 / 2 ) ↑ ( 𝑗 + 1 ) ) = ( 1 / ( 2 ↑ ( 𝑗 + 1 ) ) ) )
35 28 30 34 3eqtr2rd ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 1 / ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( ( ( 1 / 2 ) ↑ 𝑗 ) / 2 ) )
36 35 oveq2d ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 · ( 1 / ( 2 ↑ ( 𝑗 + 1 ) ) ) ) = ( 𝐴 · ( ( ( 1 / 2 ) ↑ 𝑗 ) / 2 ) ) )
37 simplr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
38 peano2nn0 ( 𝑗 ∈ ℕ0 → ( 𝑗 + 1 ) ∈ ℕ0 )
39 22 38 syl ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝑗 + 1 ) ∈ ℕ0 )
40 nnexpcl ( ( 2 ∈ ℕ ∧ ( 𝑗 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℕ )
41 5 39 40 sylancr ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℕ )
42 41 nncnd ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2 ↑ ( 𝑗 + 1 ) ) ∈ ℂ )
43 41 nnne0d ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 2 ↑ ( 𝑗 + 1 ) ) ≠ 0 )
44 37 42 43 divrecd ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( 𝐴 · ( 1 / ( 2 ↑ ( 𝑗 + 1 ) ) ) ) )
45 24 37 25 27 div12d ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) = ( 𝐴 · ( ( ( 1 / 2 ) ↑ 𝑗 ) / 2 ) ) )
46 36 44 45 3eqtr4d ( ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) )
47 46 sumeq2dv ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) )
48 fzfid ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
49 halfcl ( 𝐴 ∈ ℂ → ( 𝐴 / 2 ) ∈ ℂ )
50 49 adantl ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 / 2 ) ∈ ℂ )
51 48 50 24 fsummulc1 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) )
52 47 51 eqtr4d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) )
53 19 52 syl5eq ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑗 ∈ ( ( 1 − 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 / ( 2 ↑ ( 𝑗 + 1 ) ) ) = ( Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) )
54 2cnd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → 2 ∈ ℂ )
55 26 a1i ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → 2 ≠ 0 )
56 54 55 3 exprecd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( 1 / 2 ) ↑ 𝑁 ) = ( 1 / ( 2 ↑ 𝑁 ) ) )
57 56 oveq2d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 − ( ( 1 / 2 ) ↑ 𝑁 ) ) = ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) )
58 1mhlfehlf ( 1 − ( 1 / 2 ) ) = ( 1 / 2 )
59 58 a1i ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 − ( 1 / 2 ) ) = ( 1 / 2 ) )
60 57 59 oveq12d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − ( ( 1 / 2 ) ↑ 𝑁 ) ) / ( 1 − ( 1 / 2 ) ) ) = ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) / ( 1 / 2 ) ) )
61 simpr ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → 𝐴 ∈ ℂ )
62 61 54 55 divrec2d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 / 2 ) = ( ( 1 / 2 ) · 𝐴 ) )
63 60 62 oveq12d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( ( 1 − ( ( 1 / 2 ) ↑ 𝑁 ) ) / ( 1 − ( 1 / 2 ) ) ) · ( 𝐴 / 2 ) ) = ( ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) / ( 1 / 2 ) ) · ( ( 1 / 2 ) · 𝐴 ) ) )
64 ax-1cn 1 ∈ ℂ
65 nnnn0 ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ0 )
66 65 adantr ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
67 nnexpcl ( ( 2 ∈ ℕ ∧ 𝑁 ∈ ℕ0 ) → ( 2 ↑ 𝑁 ) ∈ ℕ )
68 5 66 67 sylancr ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 2 ↑ 𝑁 ) ∈ ℕ )
69 68 nnrecred ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 / ( 2 ↑ 𝑁 ) ) ∈ ℝ )
70 69 recnd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 / ( 2 ↑ 𝑁 ) ) ∈ ℂ )
71 subcl ( ( 1 ∈ ℂ ∧ ( 1 / ( 2 ↑ 𝑁 ) ) ∈ ℂ ) → ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) ∈ ℂ )
72 64 70 71 sylancr ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) ∈ ℂ )
73 20 a1i ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 / 2 ) ∈ ℂ )
74 0re 0 ∈ ℝ
75 halfgt0 0 < ( 1 / 2 )
76 74 75 gtneii ( 1 / 2 ) ≠ 0
77 76 a1i ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 / 2 ) ≠ 0 )
78 72 73 77 divcld ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) / ( 1 / 2 ) ) ∈ ℂ )
79 78 73 61 mulassd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) / ( 1 / 2 ) ) · ( 1 / 2 ) ) · 𝐴 ) = ( ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) / ( 1 / 2 ) ) · ( ( 1 / 2 ) · 𝐴 ) ) )
80 72 73 77 divcan1d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) / ( 1 / 2 ) ) · ( 1 / 2 ) ) = ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) )
81 80 oveq1d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) / ( 1 / 2 ) ) · ( 1 / 2 ) ) · 𝐴 ) = ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) · 𝐴 ) )
82 63 79 81 3eqtr2d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( ( 1 − ( ( 1 / 2 ) ↑ 𝑁 ) ) / ( 1 − ( 1 / 2 ) ) ) · ( 𝐴 / 2 ) ) = ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) · 𝐴 ) )
83 halfre ( 1 / 2 ) ∈ ℝ
84 halflt1 ( 1 / 2 ) < 1
85 83 84 ltneii ( 1 / 2 ) ≠ 1
86 85 a1i ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 / 2 ) ≠ 1 )
87 73 86 66 geoser ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 / 2 ) ↑ 𝑗 ) = ( ( 1 − ( ( 1 / 2 ) ↑ 𝑁 ) ) / ( 1 − ( 1 / 2 ) ) ) )
88 87 oveq1d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) = ( ( ( 1 − ( ( 1 / 2 ) ↑ 𝑁 ) ) / ( 1 − ( 1 / 2 ) ) ) · ( 𝐴 / 2 ) ) )
89 mulid2 ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
90 89 adantl ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 1 · 𝐴 ) = 𝐴 )
91 90 eqcomd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → 𝐴 = ( 1 · 𝐴 ) )
92 68 nncnd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 2 ↑ 𝑁 ) ∈ ℂ )
93 68 nnne0d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 2 ↑ 𝑁 ) ≠ 0 )
94 61 92 93 divrec2d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 / ( 2 ↑ 𝑁 ) ) = ( ( 1 / ( 2 ↑ 𝑁 ) ) · 𝐴 ) )
95 91 94 oveq12d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 − ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( ( 1 · 𝐴 ) − ( ( 1 / ( 2 ↑ 𝑁 ) ) · 𝐴 ) ) )
96 64 a1i ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → 1 ∈ ℂ )
97 96 70 61 subdird ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) · 𝐴 ) = ( ( 1 · 𝐴 ) − ( ( 1 / ( 2 ↑ 𝑁 ) ) · 𝐴 ) ) )
98 95 97 eqtr4d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( 𝐴 − ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) = ( ( 1 − ( 1 / ( 2 ↑ 𝑁 ) ) ) · 𝐴 ) )
99 82 88 98 3eqtr4d ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → ( Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( 1 / 2 ) ↑ 𝑗 ) · ( 𝐴 / 2 ) ) = ( 𝐴 − ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) )
100 16 53 99 3eqtrd ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐴 / ( 2 ↑ 𝑘 ) ) = ( 𝐴 − ( 𝐴 / ( 2 ↑ 𝑁 ) ) ) )