Metamath Proof Explorer

Theorem pcelnn

Description: There are a positive number of powers of a prime P in N iff P divides N . (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pcelnn 
|- ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) e. NN <-> P || N ) )

Proof

Step Hyp Ref Expression
1 nnz 
 |-  ( N e. NN -> N e. ZZ )
2 1nn0 
 |-  1 e. NN0
3 pcdvdsb 
 |-  ( ( P e. Prime /\ N e. ZZ /\ 1 e. NN0 ) -> ( 1 <_ ( P pCnt N ) <-> ( P ^ 1 ) || N ) )
4 2 3 mp3an3 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( 1 <_ ( P pCnt N ) <-> ( P ^ 1 ) || N ) )
5 1 4 sylan2 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( 1 <_ ( P pCnt N ) <-> ( P ^ 1 ) || N ) )
6 pccl 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( P pCnt N ) e. NN0 )
7 elnnnn0c 
 |-  ( ( P pCnt N ) e. NN <-> ( ( P pCnt N ) e. NN0 /\ 1 <_ ( P pCnt N ) ) )
8 7 baibr 
 |-  ( ( P pCnt N ) e. NN0 -> ( 1 <_ ( P pCnt N ) <-> ( P pCnt N ) e. NN ) )
9 6 8 syl 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( 1 <_ ( P pCnt N ) <-> ( P pCnt N ) e. NN ) )
10 prmnn 
 |-  ( P e. Prime -> P e. NN )
11 10 nncnd 
 |-  ( P e. Prime -> P e. CC )
12 11 exp1d 
 |-  ( P e. Prime -> ( P ^ 1 ) = P )
13 12 adantr 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( P ^ 1 ) = P )
14 13 breq1d 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( ( P ^ 1 ) || N <-> P || N ) )
15 5 9 14 3bitr3d 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) e. NN <-> P || N ) )