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 ) )