Metamath Proof Explorer

Theorem pceq0

Description: There are zero powers of a prime P in N iff P does not divide N . (Contributed by Mario Carneiro, 23-Feb-2014)

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

Proof

Step Hyp Ref Expression
1 pcelnn 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) e. NN <-> P || N ) )
2 pccl 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( P pCnt N ) e. NN0 )
3 nnne0 
 |-  ( ( P pCnt N ) e. NN -> ( P pCnt N ) =/= 0 )
4 elnn0 
 |-  ( ( P pCnt N ) e. NN0 <-> ( ( P pCnt N ) e. NN \/ ( P pCnt N ) = 0 ) )
5 4 biimpi 
 |-  ( ( P pCnt N ) e. NN0 -> ( ( P pCnt N ) e. NN \/ ( P pCnt N ) = 0 ) )
6 5 ord 
 |-  ( ( P pCnt N ) e. NN0 -> ( -. ( P pCnt N ) e. NN -> ( P pCnt N ) = 0 ) )
7 6 necon1ad 
 |-  ( ( P pCnt N ) e. NN0 -> ( ( P pCnt N ) =/= 0 -> ( P pCnt N ) e. NN ) )
8 3 7 impbid2 
 |-  ( ( P pCnt N ) e. NN0 -> ( ( P pCnt N ) e. NN <-> ( P pCnt N ) =/= 0 ) )
9 2 8 syl 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) e. NN <-> ( P pCnt N ) =/= 0 ) )
10 1 9 bitr3d 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( P || N <-> ( P pCnt N ) =/= 0 ) )
11 10 necon2bbid 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) = 0 <-> -. P || N ) )