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