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 eqtrid ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℂ ) → Σ 𝑗 ∈ ( ( 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 mullid ⊢ ( 𝐴 ∈ ℂ → ( 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 ↑ 𝑁 ) ) ) )