# 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 e. Prime /\ A e. ZZ ) -> ( P pCnt ( P ^ A ) ) = A )`

### Proof

Step Hyp Ref Expression
1 elznn0nn
` |-  ( A e. ZZ <-> ( A e. NN0 \/ ( A e. RR /\ -u A e. NN ) ) )`
2 pcidlem
` |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) = A )`
3 prmnn
` |-  ( P e. Prime -> P e. NN )`
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> P e. NN )`
5 4 nncnd
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> P e. CC )`
6 simprl
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> A e. RR )`
7 6 recnd
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> A e. CC )`
8 nnnn0
` |-  ( -u A e. NN -> -u A e. NN0 )`
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> -u A e. NN0 )`
10 expneg2
` |-  ( ( P e. CC /\ A e. CC /\ -u A e. NN0 ) -> ( P ^ A ) = ( 1 / ( P ^ -u A ) ) )`
11 5 7 9 10 syl3anc
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( P ^ A ) = ( 1 / ( P ^ -u A ) ) )`
12 11 oveq2d
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( P pCnt ( P ^ A ) ) = ( P pCnt ( 1 / ( P ^ -u A ) ) ) )`
13 simpl
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> P e. Prime )`
14 1zzd
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> 1 e. ZZ )`
15 ax-1ne0
` |-  1 =/= 0`
16 15 a1i
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> 1 =/= 0 )`
17 4 9 nnexpcld
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( P ^ -u A ) e. NN )`
18 pcdiv
` |-  ( ( P e. Prime /\ ( 1 e. ZZ /\ 1 =/= 0 ) /\ ( P ^ -u A ) e. NN ) -> ( P pCnt ( 1 / ( P ^ -u A ) ) ) = ( ( P pCnt 1 ) - ( P pCnt ( P ^ -u A ) ) ) )`
19 13 14 16 17 18 syl121anc
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( P pCnt ( 1 / ( P ^ -u A ) ) ) = ( ( P pCnt 1 ) - ( P pCnt ( P ^ -u A ) ) ) )`
20 pc1
` |-  ( P e. Prime -> ( P pCnt 1 ) = 0 )`
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( P pCnt 1 ) = 0 )`
22 pcidlem
` |-  ( ( P e. Prime /\ -u A e. NN0 ) -> ( P pCnt ( P ^ -u A ) ) = -u A )`
23 9 22 syldan
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( P pCnt ( P ^ -u A ) ) = -u A )`
24 21 23 oveq12d
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( ( P pCnt 1 ) - ( P pCnt ( P ^ -u A ) ) ) = ( 0 - -u A ) )`
25 df-neg
` |-  -u -u A = ( 0 - -u A )`
26 7 negnegd
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> -u -u A = A )`
27 25 26 syl5eqr
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( 0 - -u A ) = A )`
28 24 27 eqtrd
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( ( P pCnt 1 ) - ( P pCnt ( P ^ -u A ) ) ) = A )`
29 19 28 eqtrd
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( P pCnt ( 1 / ( P ^ -u A ) ) ) = A )`
30 12 29 eqtrd
` |-  ( ( P e. Prime /\ ( A e. RR /\ -u A e. NN ) ) -> ( P pCnt ( P ^ A ) ) = A )`
31 2 30 jaodan
` |-  ( ( P e. Prime /\ ( A e. NN0 \/ ( A e. RR /\ -u A e. NN ) ) ) -> ( P pCnt ( P ^ A ) ) = A )`
32 1 31 sylan2b
` |-  ( ( P e. Prime /\ A e. ZZ ) -> ( P pCnt ( P ^ A ) ) = A )`