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

Metamath Proof Explorer

Theorem 0sgmppw

Description: A prime power P ^ K has K + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016)

Ref Expression
Assertion 0sgmppw 
|- ( ( P e. Prime /\ K e. NN0 ) -> ( 0 sigma ( P ^ K ) ) = ( K + 1 ) )

Proof

Step Hyp Ref Expression
1 prmnn 
 |-  ( P e. Prime -> P e. NN )
2 nnexpcl 
 |-  ( ( P e. NN /\ K e. NN0 ) -> ( P ^ K ) e. NN )
3 1 2 sylan 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( P ^ K ) e. NN )
4 0sgm 
 |-  ( ( P ^ K ) e. NN -> ( 0 sigma ( P ^ K ) ) = ( # ` { x e. NN | x || ( P ^ K ) } ) )
5 3 4 syl 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( 0 sigma ( P ^ K ) ) = ( # ` { x e. NN | x || ( P ^ K ) } ) )
6 fzfid 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( 0 ... K ) e. Fin )
7 eqid 
 |-  ( n e. ( 0 ... K ) |-> ( P ^ n ) ) = ( n e. ( 0 ... K ) |-> ( P ^ n ) )
8 7 dvdsppwf1o 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( n e. ( 0 ... K ) |-> ( P ^ n ) ) : ( 0 ... K ) -1-1-onto-> { x e. NN | x || ( P ^ K ) } )
9 6 8 hasheqf1od 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( # ` ( 0 ... K ) ) = ( # ` { x e. NN | x || ( P ^ K ) } ) )
10 5 9 eqtr4d 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( 0 sigma ( P ^ K ) ) = ( # ` ( 0 ... K ) ) )
11 simpr 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> K e. NN0 )
12 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
13 11 12 eleqtrdi 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> K e. ( ZZ>= ` 0 ) )
14 hashfz 
 |-  ( K e. ( ZZ>= ` 0 ) -> ( # ` ( 0 ... K ) ) = ( ( K - 0 ) + 1 ) )
15 13 14 syl 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( # ` ( 0 ... K ) ) = ( ( K - 0 ) + 1 ) )
16 nn0cn 
 |-  ( K e. NN0 -> K e. CC )
17 16 adantl 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> K e. CC )
18 17 subid1d 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( K - 0 ) = K )
19 18 oveq1d 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( ( K - 0 ) + 1 ) = ( K + 1 ) )
20 10 15 19 3eqtrd 
 |-  ( ( P e. Prime /\ K e. NN0 ) -> ( 0 sigma ( P ^ K ) ) = ( K + 1 ) )