Metamath Proof Explorer

Theorem geo2sum2

Description: The value of the finite geometric series 1 + 2 + 4 + 8 + ... + 2 ^ ( N - 1 ) . (Contributed by Mario Carneiro, 7-Sep-2016)

Ref Expression
Assertion geo2sum2 
|- ( N e. NN0 -> sum_ k e. ( 0 ..^ N ) ( 2 ^ k ) = ( ( 2 ^ N ) - 1 ) )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
2 fzoval 
 |-  ( N e. ZZ -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
3 1 2 syl 
 |-  ( N e. NN0 -> ( 0 ..^ N ) = ( 0 ... ( N - 1 ) ) )
4 3 sumeq1d 
 |-  ( N e. NN0 -> sum_ k e. ( 0 ..^ N ) ( 2 ^ k ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( 2 ^ k ) )
5 2cn 
 |-  2 e. CC
6 5 a1i 
 |-  ( N e. NN0 -> 2 e. CC )
7 1ne2 
 |-  1 =/= 2
8 7 necomi 
 |-  2 =/= 1
9 8 a1i 
 |-  ( N e. NN0 -> 2 =/= 1 )
10 id 
 |-  ( N e. NN0 -> N e. NN0 )
11 6 9 10 geoser 
 |-  ( N e. NN0 -> sum_ k e. ( 0 ... ( N - 1 ) ) ( 2 ^ k ) = ( ( 1 - ( 2 ^ N ) ) / ( 1 - 2 ) ) )
12 6 10 expcld 
 |-  ( N e. NN0 -> ( 2 ^ N ) e. CC )
13 ax-1cn 
 |-  1 e. CC
14 13 a1i 
 |-  ( N e. NN0 -> 1 e. CC )
15 12 14 subcld 
 |-  ( N e. NN0 -> ( ( 2 ^ N ) - 1 ) e. CC )
16 ax-1ne0 
 |-  1 =/= 0
17 16 a1i 
 |-  ( N e. NN0 -> 1 =/= 0 )
18 15 14 17 div2negd 
 |-  ( N e. NN0 -> ( -u ( ( 2 ^ N ) - 1 ) / -u 1 ) = ( ( ( 2 ^ N ) - 1 ) / 1 ) )
19 12 14 negsubdi2d 
 |-  ( N e. NN0 -> -u ( ( 2 ^ N ) - 1 ) = ( 1 - ( 2 ^ N ) ) )
20 2m1e1 
 |-  ( 2 - 1 ) = 1
21 20 negeqi 
 |-  -u ( 2 - 1 ) = -u 1
22 5 13 negsubdi2i 
 |-  -u ( 2 - 1 ) = ( 1 - 2 )
23 21 22 eqtr3i 
 |-  -u 1 = ( 1 - 2 )
24 23 a1i 
 |-  ( N e. NN0 -> -u 1 = ( 1 - 2 ) )
25 19 24 oveq12d 
 |-  ( N e. NN0 -> ( -u ( ( 2 ^ N ) - 1 ) / -u 1 ) = ( ( 1 - ( 2 ^ N ) ) / ( 1 - 2 ) ) )
26 15 div1d 
 |-  ( N e. NN0 -> ( ( ( 2 ^ N ) - 1 ) / 1 ) = ( ( 2 ^ N ) - 1 ) )
27 18 25 26 3eqtr3d 
 |-  ( N e. NN0 -> ( ( 1 - ( 2 ^ N ) ) / ( 1 - 2 ) ) = ( ( 2 ^ N ) - 1 ) )
28 4 11 27 3eqtrd 
 |-  ( N e. NN0 -> sum_ k e. ( 0 ..^ N ) ( 2 ^ k ) = ( ( 2 ^ N ) - 1 ) )