Metamath Proof Explorer

Theorem pcidlem

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

Ref Expression
Assertion pcidlem 
|- ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) = A )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> P e. Prime )
2 prmnn 
 |-  ( P e. Prime -> P e. NN )
3 1 2 syl 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> P e. NN )
4 simpr 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> A e. NN0 )
5 3 4 nnexpcld 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P ^ A ) e. NN )
6 1 5 pccld 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) e. NN0 )
7 6 nn0red 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) e. RR )
8 7 leidd 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) <_ ( P pCnt ( P ^ A ) ) )
9 5 nnzd 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P ^ A ) e. ZZ )
10 pcdvdsb 
 |-  ( ( P e. Prime /\ ( P ^ A ) e. ZZ /\ ( P pCnt ( P ^ A ) ) e. NN0 ) -> ( ( P pCnt ( P ^ A ) ) <_ ( P pCnt ( P ^ A ) ) <-> ( P ^ ( P pCnt ( P ^ A ) ) ) || ( P ^ A ) ) )
11 1 9 6 10 syl3anc 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( ( P pCnt ( P ^ A ) ) <_ ( P pCnt ( P ^ A ) ) <-> ( P ^ ( P pCnt ( P ^ A ) ) ) || ( P ^ A ) ) )
12 8 11 mpbid 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P ^ ( P pCnt ( P ^ A ) ) ) || ( P ^ A ) )
13 3 6 nnexpcld 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P ^ ( P pCnt ( P ^ A ) ) ) e. NN )
14 13 nnzd 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P ^ ( P pCnt ( P ^ A ) ) ) e. ZZ )
15 dvdsle 
 |-  ( ( ( P ^ ( P pCnt ( P ^ A ) ) ) e. ZZ /\ ( P ^ A ) e. NN ) -> ( ( P ^ ( P pCnt ( P ^ A ) ) ) || ( P ^ A ) -> ( P ^ ( P pCnt ( P ^ A ) ) ) <_ ( P ^ A ) ) )
16 14 5 15 syl2anc 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( ( P ^ ( P pCnt ( P ^ A ) ) ) || ( P ^ A ) -> ( P ^ ( P pCnt ( P ^ A ) ) ) <_ ( P ^ A ) ) )
17 12 16 mpd 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P ^ ( P pCnt ( P ^ A ) ) ) <_ ( P ^ A ) )
18 3 nnred 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> P e. RR )
19 6 nn0zd 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) e. ZZ )
20 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
21 20 adantl 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> A e. ZZ )
22 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
23 eluz2gt1 
 |-  ( P e. ( ZZ>= ` 2 ) -> 1 < P )
24 1 22 23 3syl 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> 1 < P )
25 18 19 21 24 leexp2d 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( ( P pCnt ( P ^ A ) ) <_ A <-> ( P ^ ( P pCnt ( P ^ A ) ) ) <_ ( P ^ A ) ) )
26 17 25 mpbird 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) <_ A )
27 iddvds 
 |-  ( ( P ^ A ) e. ZZ -> ( P ^ A ) || ( P ^ A ) )
28 9 27 syl 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P ^ A ) || ( P ^ A ) )
29 pcdvdsb 
 |-  ( ( P e. Prime /\ ( P ^ A ) e. ZZ /\ A e. NN0 ) -> ( A <_ ( P pCnt ( P ^ A ) ) <-> ( P ^ A ) || ( P ^ A ) ) )
30 1 9 4 29 syl3anc 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( A <_ ( P pCnt ( P ^ A ) ) <-> ( P ^ A ) || ( P ^ A ) ) )
31 28 30 mpbird 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> A <_ ( P pCnt ( P ^ A ) ) )
32 nn0re 
 |-  ( A e. NN0 -> A e. RR )
33 32 adantl 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> A e. RR )
34 7 33 letri3d 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( ( P pCnt ( P ^ A ) ) = A <-> ( ( P pCnt ( P ^ A ) ) <_ A /\ A <_ ( P pCnt ( P ^ A ) ) ) ) )
35 26 31 34 mpbir2and 
 |-  ( ( P e. Prime /\ A e. NN0 ) -> ( P pCnt ( P ^ A ) ) = A )