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 PK00σPK=K+1

Proof

Step Hyp Ref Expression
1 prmnn PP
2 nnexpcl PK0PK
3 1 2 sylan PK0PK
4 0sgm PK0σPK=x|xPK
5 3 4 syl PK00σPK=x|xPK
6 fzfid PK00KFin
7 eqid n0KPn=n0KPn
8 7 dvdsppwf1o PK0n0KPn:0K1-1 ontox|xPK
9 6 8 hasheqf1od PK00K=x|xPK
10 5 9 eqtr4d PK00σPK=0K
11 simpr PK0K0
12 nn0uz 0=0
13 11 12 eleqtrdi PK0K0
14 hashfz K00K=K-0+1
15 13 14 syl PK00K=K-0+1
16 nn0cn K0K
17 16 adantl PK0K
18 17 subid1d PK0K0=K
19 18 oveq1d PK0K-0+1=K+1
20 10 15 19 3eqtrd PK00σPK=K+1