Metamath Proof Explorer

Theorem 1sgmprm

Description: The sum of divisors for a prime is P + 1 because the only divisors are 1 and P . (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion 1sgmprm 
|- ( P e. Prime -> ( 1 sigma P ) = ( P + 1 ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 1nn0 
 |-  1 e. NN0
3 sgmppw 
 |-  ( ( 1 e. CC /\ P e. Prime /\ 1 e. NN0 ) -> ( 1 sigma ( P ^ 1 ) ) = sum_ k e. ( 0 ... 1 ) ( ( P ^c 1 ) ^ k ) )
4 1 2 3 mp3an13 
 |-  ( P e. Prime -> ( 1 sigma ( P ^ 1 ) ) = sum_ k e. ( 0 ... 1 ) ( ( P ^c 1 ) ^ k ) )
5 prmnn 
 |-  ( P e. Prime -> P e. NN )
6 5 nncnd 
 |-  ( P e. Prime -> P e. CC )
7 6 exp1d 
 |-  ( P e. Prime -> ( P ^ 1 ) = P )
8 7 oveq2d 
 |-  ( P e. Prime -> ( 1 sigma ( P ^ 1 ) ) = ( 1 sigma P ) )
9 6 adantr 
 |-  ( ( P e. Prime /\ k e. ( 0 ... 1 ) ) -> P e. CC )
10 9 cxp1d 
 |-  ( ( P e. Prime /\ k e. ( 0 ... 1 ) ) -> ( P ^c 1 ) = P )
11 10 oveq1d 
 |-  ( ( P e. Prime /\ k e. ( 0 ... 1 ) ) -> ( ( P ^c 1 ) ^ k ) = ( P ^ k ) )
12 11 sumeq2dv 
 |-  ( P e. Prime -> sum_ k e. ( 0 ... 1 ) ( ( P ^c 1 ) ^ k ) = sum_ k e. ( 0 ... 1 ) ( P ^ k ) )
13 1m1e0 
 |-  ( 1 - 1 ) = 0
14 13 oveq2i 
 |-  ( 0 ... ( 1 - 1 ) ) = ( 0 ... 0 )
15 14 sumeq1i 
 |-  sum_ k e. ( 0 ... ( 1 - 1 ) ) ( P ^ k ) = sum_ k e. ( 0 ... 0 ) ( P ^ k )
16 0z 
 |-  0 e. ZZ
17 6 exp0d 
 |-  ( P e. Prime -> ( P ^ 0 ) = 1 )
18 17 1 eqeltrdi 
 |-  ( P e. Prime -> ( P ^ 0 ) e. CC )
19 oveq2 
 |-  ( k = 0 -> ( P ^ k ) = ( P ^ 0 ) )
20 19 fsum1 
 |-  ( ( 0 e. ZZ /\ ( P ^ 0 ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( P ^ k ) = ( P ^ 0 ) )
21 16 18 20 sylancr 
 |-  ( P e. Prime -> sum_ k e. ( 0 ... 0 ) ( P ^ k ) = ( P ^ 0 ) )
22 21 17 eqtrd 
 |-  ( P e. Prime -> sum_ k e. ( 0 ... 0 ) ( P ^ k ) = 1 )
23 15 22 eqtrid 
 |-  ( P e. Prime -> sum_ k e. ( 0 ... ( 1 - 1 ) ) ( P ^ k ) = 1 )
24 23 7 oveq12d 
 |-  ( P e. Prime -> ( sum_ k e. ( 0 ... ( 1 - 1 ) ) ( P ^ k ) + ( P ^ 1 ) ) = ( 1 + P ) )
25 2 a1i 
 |-  ( P e. Prime -> 1 e. NN0 )
26 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
27 25 26 eleqtrdi 
 |-  ( P e. Prime -> 1 e. ( ZZ>= ` 0 ) )
28 elfznn0 
 |-  ( k e. ( 0 ... 1 ) -> k e. NN0 )
29 expcl 
 |-  ( ( P e. CC /\ k e. NN0 ) -> ( P ^ k ) e. CC )
30 6 28 29 syl2an 
 |-  ( ( P e. Prime /\ k e. ( 0 ... 1 ) ) -> ( P ^ k ) e. CC )
31 oveq2 
 |-  ( k = 1 -> ( P ^ k ) = ( P ^ 1 ) )
32 27 30 31 fsumm1 
 |-  ( P e. Prime -> sum_ k e. ( 0 ... 1 ) ( P ^ k ) = ( sum_ k e. ( 0 ... ( 1 - 1 ) ) ( P ^ k ) + ( P ^ 1 ) ) )
33 addcom 
 |-  ( ( P e. CC /\ 1 e. CC ) -> ( P + 1 ) = ( 1 + P ) )
34 6 1 33 sylancl 
 |-  ( P e. Prime -> ( P + 1 ) = ( 1 + P ) )
35 24 32 34 3eqtr4d 
 |-  ( P e. Prime -> sum_ k e. ( 0 ... 1 ) ( P ^ k ) = ( P + 1 ) )
36 12 35 eqtrd 
 |-  ( P e. Prime -> sum_ k e. ( 0 ... 1 ) ( ( P ^c 1 ) ^ k ) = ( P + 1 ) )
37 4 8 36 3eqtr3d 
 |-  ( P e. Prime -> ( 1 sigma P ) = ( P + 1 ) )