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 )
4 3 adantr
 |-  ( ( 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 )
9 8 ad2antll
 |-  ( ( 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 )
21 20 adantr
 |-  ( ( 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 )