Metamath Proof Explorer

Theorem pcz

Description: The prime count function can be used as an indicator that a given rational number is an integer. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pcz 
|- ( A e. QQ -> ( A e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt A ) ) )

Proof

Step Hyp Ref Expression
1 pcge0 
 |-  ( ( p e. Prime /\ A e. ZZ ) -> 0 <_ ( p pCnt A ) )
2 1 ancoms 
 |-  ( ( A e. ZZ /\ p e. Prime ) -> 0 <_ ( p pCnt A ) )
3 2 ralrimiva 
 |-  ( A e. ZZ -> A. p e. Prime 0 <_ ( p pCnt A ) )
4 elq 
 |-  ( A e. QQ <-> E. x e. ZZ E. y e. NN A = ( x / y ) )
5 nnz 
 |-  ( y e. NN -> y e. ZZ )
6 dvds0 
 |-  ( y e. ZZ -> y || 0 )
7 5 6 syl 
 |-  ( y e. NN -> y || 0 )
8 7 ad2antlr 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x = 0 ) -> y || 0 )
9 simpr 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x = 0 ) -> x = 0 )
10 8 9 breqtrrd 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x = 0 ) -> y || x )
11 10 a1d 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x = 0 ) -> ( A. p e. Prime 0 <_ ( p pCnt ( x / y ) ) -> y || x ) )
12 simpr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> p e. Prime )
13 simplll 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> x e. ZZ )
14 simplr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> x =/= 0 )
15 simpllr 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> y e. NN )
16 pcdiv 
 |-  ( ( p e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) -> ( p pCnt ( x / y ) ) = ( ( p pCnt x ) - ( p pCnt y ) ) )
17 12 13 14 15 16 syl121anc 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> ( p pCnt ( x / y ) ) = ( ( p pCnt x ) - ( p pCnt y ) ) )
18 17 breq2d 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> ( 0 <_ ( p pCnt ( x / y ) ) <-> 0 <_ ( ( p pCnt x ) - ( p pCnt y ) ) ) )
19 pczcl 
 |-  ( ( p e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( p pCnt x ) e. NN0 )
20 12 13 14 19 syl12anc 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> ( p pCnt x ) e. NN0 )
21 20 nn0red 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> ( p pCnt x ) e. RR )
22 12 15 pccld 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> ( p pCnt y ) e. NN0 )
23 22 nn0red 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> ( p pCnt y ) e. RR )
24 21 23 subge0d 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> ( 0 <_ ( ( p pCnt x ) - ( p pCnt y ) ) <-> ( p pCnt y ) <_ ( p pCnt x ) ) )
25 18 24 bitrd 
 |-  ( ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) /\ p e. Prime ) -> ( 0 <_ ( p pCnt ( x / y ) ) <-> ( p pCnt y ) <_ ( p pCnt x ) ) )
26 25 ralbidva 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) -> ( A. p e. Prime 0 <_ ( p pCnt ( x / y ) ) <-> A. p e. Prime ( p pCnt y ) <_ ( p pCnt x ) ) )
27 id 
 |-  ( x e. ZZ -> x e. ZZ )
28 pc2dvds 
 |-  ( ( y e. ZZ /\ x e. ZZ ) -> ( y || x <-> A. p e. Prime ( p pCnt y ) <_ ( p pCnt x ) ) )
29 5 27 28 syl2anr 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( y || x <-> A. p e. Prime ( p pCnt y ) <_ ( p pCnt x ) ) )
30 29 adantr 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) -> ( y || x <-> A. p e. Prime ( p pCnt y ) <_ ( p pCnt x ) ) )
31 26 30 bitr4d 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) -> ( A. p e. Prime 0 <_ ( p pCnt ( x / y ) ) <-> y || x ) )
32 31 biimpd 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) -> ( A. p e. Prime 0 <_ ( p pCnt ( x / y ) ) -> y || x ) )
33 11 32 pm2.61dane 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( A. p e. Prime 0 <_ ( p pCnt ( x / y ) ) -> y || x ) )
34 nnne0 
 |-  ( y e. NN -> y =/= 0 )
35 simpl 
 |-  ( ( x e. ZZ /\ y e. NN ) -> x e. ZZ )
36 dvdsval2 
 |-  ( ( y e. ZZ /\ y =/= 0 /\ x e. ZZ ) -> ( y || x <-> ( x / y ) e. ZZ ) )
37 5 34 35 36 syl2an23an 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( y || x <-> ( x / y ) e. ZZ ) )
38 33 37 sylibd 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( A. p e. Prime 0 <_ ( p pCnt ( x / y ) ) -> ( x / y ) e. ZZ ) )
39 oveq2 
 |-  ( A = ( x / y ) -> ( p pCnt A ) = ( p pCnt ( x / y ) ) )
40 39 breq2d 
 |-  ( A = ( x / y ) -> ( 0 <_ ( p pCnt A ) <-> 0 <_ ( p pCnt ( x / y ) ) ) )
41 40 ralbidv 
 |-  ( A = ( x / y ) -> ( A. p e. Prime 0 <_ ( p pCnt A ) <-> A. p e. Prime 0 <_ ( p pCnt ( x / y ) ) ) )
42 eleq1 
 |-  ( A = ( x / y ) -> ( A e. ZZ <-> ( x / y ) e. ZZ ) )
43 41 42 imbi12d 
 |-  ( A = ( x / y ) -> ( ( A. p e. Prime 0 <_ ( p pCnt A ) -> A e. ZZ ) <-> ( A. p e. Prime 0 <_ ( p pCnt ( x / y ) ) -> ( x / y ) e. ZZ ) ) )
44 38 43 syl5ibrcom 
 |-  ( ( x e. ZZ /\ y e. NN ) -> ( A = ( x / y ) -> ( A. p e. Prime 0 <_ ( p pCnt A ) -> A e. ZZ ) ) )
45 44 rexlimivv 
 |-  ( E. x e. ZZ E. y e. NN A = ( x / y ) -> ( A. p e. Prime 0 <_ ( p pCnt A ) -> A e. ZZ ) )
46 4 45 sylbi 
 |-  ( A e. QQ -> ( A. p e. Prime 0 <_ ( p pCnt A ) -> A e. ZZ ) )
47 3 46 impbid2 
 |-  ( A e. QQ -> ( A e. ZZ <-> A. p e. Prime 0 <_ ( p pCnt A ) ) )