Metamath Proof Explorer


Theorem pcid

Description: The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014)

Ref Expression
Assertion pcid P A P pCnt P A = A

Proof

Step Hyp Ref Expression
1 elznn0nn A A 0 A A
2 pcidlem P A 0 P pCnt P A = A
3 prmnn P P
4 3 adantr P A A P
5 4 nncnd P A A P
6 simprl P A A A
7 6 recnd P A A A
8 nnnn0 A A 0
9 8 ad2antll P A A A 0
10 expneg2 P A A 0 P A = 1 P A
11 5 7 9 10 syl3anc P A A P A = 1 P A
12 11 oveq2d P A A P pCnt P A = P pCnt 1 P A
13 simpl P A A P
14 1zzd P A A 1
15 ax-1ne0 1 0
16 15 a1i P A A 1 0
17 4 9 nnexpcld P A A P A
18 pcdiv P 1 1 0 P A P pCnt 1 P A = P pCnt 1 P pCnt P A
19 13 14 16 17 18 syl121anc P A A P pCnt 1 P A = P pCnt 1 P pCnt P A
20 pc1 P P pCnt 1 = 0
21 20 adantr P A A P pCnt 1 = 0
22 pcidlem P A 0 P pCnt P A = A
23 9 22 syldan P A A P pCnt P A = A
24 21 23 oveq12d P A A P pCnt 1 P pCnt P A = 0 A
25 df-neg A = 0 A
26 7 negnegd P A A A = A
27 25 26 eqtr3id P A A 0 A = A
28 24 27 eqtrd P A A P pCnt 1 P pCnt P A = A
29 19 28 eqtrd P A A P pCnt 1 P A = A
30 12 29 eqtrd P A A P pCnt P A = A
31 2 30 jaodan P A 0 A A P pCnt P A = A
32 1 31 sylan2b P A P pCnt P A = A