Description: A prime power P ^ K has K + 1 divisors. (Contributed by Mario Carneiro, 17-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | 0sgmppw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prmnn | |
|
2 | nnexpcl | |
|
3 | 1 2 | sylan | |
4 | 0sgm | |
|
5 | 3 4 | syl | |
6 | fzfid | |
|
7 | eqid | |
|
8 | 7 | dvdsppwf1o | |
9 | 6 8 | hasheqf1od | |
10 | 5 9 | eqtr4d | |
11 | simpr | |
|
12 | nn0uz | |
|
13 | 11 12 | eleqtrdi | |
14 | hashfz | |
|
15 | 13 14 | syl | |
16 | nn0cn | |
|
17 | 16 | adantl | |
18 | 17 | subid1d | |
19 | 18 | oveq1d | |
20 | 10 15 19 | 3eqtrd | |