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 eqtr3id 
 |-  ( ( 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 )