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 
|- ( ( N e. NN /\ A e. CC ) -> sum_ k e. ( 1 ... N ) ( A / ( 2 ^ k ) ) = ( A - ( A / ( 2 ^ N ) ) ) )

Proof

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