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 K 0 0 σ P K = K + 1

Proof

Step Hyp Ref Expression
1 prmnn P P
2 nnexpcl P K 0 P K
3 1 2 sylan P K 0 P K
4 0sgm P K 0 σ P K = x | x P K
5 3 4 syl P K 0 0 σ P K = x | x P K
6 fzfid P K 0 0 K Fin
7 eqid n 0 K P n = n 0 K P n
8 7 dvdsppwf1o P K 0 n 0 K P n : 0 K 1-1 onto x | x P K
9 6 8 hasheqf1od P K 0 0 K = x | x P K
10 5 9 eqtr4d P K 0 0 σ P K = 0 K
11 simpr P K 0 K 0
12 nn0uz 0 = 0
13 11 12 eleqtrdi P K 0 K 0
14 hashfz K 0 0 K = K - 0 + 1
15 13 14 syl P K 0 0 K = K - 0 + 1
16 nn0cn K 0 K
17 16 adantl P K 0 K
18 17 subid1d P K 0 K 0 = K
19 18 oveq1d P K 0 K - 0 + 1 = K + 1
20 10 15 19 3eqtrd P K 0 0 σ P K = K + 1