This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1sgm2ppw

Description: The sum of the divisors of 2 ^ ( N - 1 ) . (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion 1sgm2ppw 
|- ( N e. NN -> ( 1 sigma ( 2 ^ ( N - 1 ) ) ) = ( ( 2 ^ N ) - 1 ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 2prm 
 |-  2 e. Prime
3 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
4 sgmppw 
 |-  ( ( 1 e. CC /\ 2 e. Prime /\ ( N - 1 ) e. NN0 ) -> ( 1 sigma ( 2 ^ ( N - 1 ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( 2 ^c 1 ) ^ k ) )
5 1 2 3 4 mp3an12i 
 |-  ( N e. NN -> ( 1 sigma ( 2 ^ ( N - 1 ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( 2 ^c 1 ) ^ k ) )
6 2cn 
 |-  2 e. CC
7 cxp1 
 |-  ( 2 e. CC -> ( 2 ^c 1 ) = 2 )
8 6 7 mp1i 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> ( 2 ^c 1 ) = 2 )
9 8 oveq1d 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> ( ( 2 ^c 1 ) ^ k ) = ( 2 ^ k ) )
10 9 sumeq2i 
 |-  sum_ k e. ( 0 ... ( N - 1 ) ) ( ( 2 ^c 1 ) ^ k ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( 2 ^ k )
11 6 a1i 
 |-  ( N e. NN -> 2 e. CC )
12 1ne2 
 |-  1 =/= 2
13 12 necomi 
 |-  2 =/= 1
14 13 a1i 
 |-  ( N e. NN -> 2 =/= 1 )
15 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
16 11 14 15 geoser 
 |-  ( N e. NN -> sum_ k e. ( 0 ... ( N - 1 ) ) ( 2 ^ k ) = ( ( 1 - ( 2 ^ N ) ) / ( 1 - 2 ) ) )
17 10 16 eqtrid 
 |-  ( N e. NN -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( 2 ^c 1 ) ^ k ) = ( ( 1 - ( 2 ^ N ) ) / ( 1 - 2 ) ) )
18 2nn 
 |-  2 e. NN
19 nnexpcl 
 |-  ( ( 2 e. NN /\ N e. NN0 ) -> ( 2 ^ N ) e. NN )
20 18 15 19 sylancr 
 |-  ( N e. NN -> ( 2 ^ N ) e. NN )
21 20 nncnd 
 |-  ( N e. NN -> ( 2 ^ N ) e. CC )
22 subcl 
 |-  ( ( ( 2 ^ N ) e. CC /\ 1 e. CC ) -> ( ( 2 ^ N ) - 1 ) e. CC )
23 21 1 22 sylancl 
 |-  ( N e. NN -> ( ( 2 ^ N ) - 1 ) e. CC )
24 1 a1i 
 |-  ( N e. NN -> 1 e. CC )
25 ax-1ne0 
 |-  1 =/= 0
26 25 a1i 
 |-  ( N e. NN -> 1 =/= 0 )
27 23 24 26 div2negd 
 |-  ( N e. NN -> ( -u ( ( 2 ^ N ) - 1 ) / -u 1 ) = ( ( ( 2 ^ N ) - 1 ) / 1 ) )
28 negsubdi2 
 |-  ( ( ( 2 ^ N ) e. CC /\ 1 e. CC ) -> -u ( ( 2 ^ N ) - 1 ) = ( 1 - ( 2 ^ N ) ) )
29 21 1 28 sylancl 
 |-  ( N e. NN -> -u ( ( 2 ^ N ) - 1 ) = ( 1 - ( 2 ^ N ) ) )
30 df-neg 
 |-  -u 1 = ( 0 - 1 )
31 0cn 
 |-  0 e. CC
32 pnpcan 
 |-  ( ( 1 e. CC /\ 0 e. CC /\ 1 e. CC ) -> ( ( 1 + 0 ) - ( 1 + 1 ) ) = ( 0 - 1 ) )
33 1 31 1 32 mp3an 
 |-  ( ( 1 + 0 ) - ( 1 + 1 ) ) = ( 0 - 1 )
34 1p0e1 
 |-  ( 1 + 0 ) = 1
35 1p1e2 
 |-  ( 1 + 1 ) = 2
36 34 35 oveq12i 
 |-  ( ( 1 + 0 ) - ( 1 + 1 ) ) = ( 1 - 2 )
37 30 33 36 3eqtr2i 
 |-  -u 1 = ( 1 - 2 )
38 37 a1i 
 |-  ( N e. NN -> -u 1 = ( 1 - 2 ) )
39 29 38 oveq12d 
 |-  ( N e. NN -> ( -u ( ( 2 ^ N ) - 1 ) / -u 1 ) = ( ( 1 - ( 2 ^ N ) ) / ( 1 - 2 ) ) )
40 23 div1d 
 |-  ( N e. NN -> ( ( ( 2 ^ N ) - 1 ) / 1 ) = ( ( 2 ^ N ) - 1 ) )
41 27 39 40 3eqtr3d 
 |-  ( N e. NN -> ( ( 1 - ( 2 ^ N ) ) / ( 1 - 2 ) ) = ( ( 2 ^ N ) - 1 ) )
42 5 17 41 3eqtrd 
 |-  ( N e. NN -> ( 1 sigma ( 2 ^ ( N - 1 ) ) ) = ( ( 2 ^ N ) - 1 ) )