This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pcqcl

Description: Closure of the general prime count function. (Contributed by Mario Carneiro, 23-Feb-2014)

Ref Expression
Assertion pcqcl 
|- ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( P pCnt N ) e. ZZ )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> N e. QQ )
2 elq 
 |-  ( N e. QQ <-> E. x e. ZZ E. y e. NN N = ( x / y ) )
3 1 2 sylib 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> E. x e. ZZ E. y e. NN N = ( x / y ) )
4 nncn 
 |-  ( y e. NN -> y e. CC )
5 nnne0 
 |-  ( y e. NN -> y =/= 0 )
6 4 5 div0d 
 |-  ( y e. NN -> ( 0 / y ) = 0 )
7 6 ad2antll 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( 0 / y ) = 0 )
8 oveq1 
 |-  ( x = 0 -> ( x / y ) = ( 0 / y ) )
9 8 eqeq1d 
 |-  ( x = 0 -> ( ( x / y ) = 0 <-> ( 0 / y ) = 0 ) )
10 7 9 syl5ibrcom 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( x = 0 -> ( x / y ) = 0 ) )
11 10 necon3d 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( ( x / y ) =/= 0 -> x =/= 0 ) )
12 an32 
 |-  ( ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) <-> ( ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) )
13 pcdiv 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) -> ( P pCnt ( x / y ) ) = ( ( P pCnt x ) - ( P pCnt y ) ) )
14 pczcl 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( P pCnt x ) e. NN0 )
15 14 nn0zd 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) ) -> ( P pCnt x ) e. ZZ )
16 15 3adant3 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) -> ( P pCnt x ) e. ZZ )
17 nnz 
 |-  ( y e. NN -> y e. ZZ )
18 17 5 jca 
 |-  ( y e. NN -> ( y e. ZZ /\ y =/= 0 ) )
19 pczcl 
 |-  ( ( P e. Prime /\ ( y e. ZZ /\ y =/= 0 ) ) -> ( P pCnt y ) e. NN0 )
20 19 nn0zd 
 |-  ( ( P e. Prime /\ ( y e. ZZ /\ y =/= 0 ) ) -> ( P pCnt y ) e. ZZ )
21 18 20 sylan2 
 |-  ( ( P e. Prime /\ y e. NN ) -> ( P pCnt y ) e. ZZ )
22 21 3adant2 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) -> ( P pCnt y ) e. ZZ )
23 16 22 zsubcld 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) -> ( ( P pCnt x ) - ( P pCnt y ) ) e. ZZ )
24 13 23 eqeltrd 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) -> ( P pCnt ( x / y ) ) e. ZZ )
25 24 3expb 
 |-  ( ( P e. Prime /\ ( ( x e. ZZ /\ x =/= 0 ) /\ y e. NN ) ) -> ( P pCnt ( x / y ) ) e. ZZ )
26 12 25 sylan2b 
 |-  ( ( P e. Prime /\ ( ( x e. ZZ /\ y e. NN ) /\ x =/= 0 ) ) -> ( P pCnt ( x / y ) ) e. ZZ )
27 26 expr 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( x =/= 0 -> ( P pCnt ( x / y ) ) e. ZZ ) )
28 11 27 syld 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( ( x / y ) =/= 0 -> ( P pCnt ( x / y ) ) e. ZZ ) )
29 neeq1 
 |-  ( N = ( x / y ) -> ( N =/= 0 <-> ( x / y ) =/= 0 ) )
30 oveq2 
 |-  ( N = ( x / y ) -> ( P pCnt N ) = ( P pCnt ( x / y ) ) )
31 30 eleq1d 
 |-  ( N = ( x / y ) -> ( ( P pCnt N ) e. ZZ <-> ( P pCnt ( x / y ) ) e. ZZ ) )
32 29 31 imbi12d 
 |-  ( N = ( x / y ) -> ( ( N =/= 0 -> ( P pCnt N ) e. ZZ ) <-> ( ( x / y ) =/= 0 -> ( P pCnt ( x / y ) ) e. ZZ ) ) )
33 28 32 syl5ibrcom 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( N = ( x / y ) -> ( N =/= 0 -> ( P pCnt N ) e. ZZ ) ) )
34 33 com23 
 |-  ( ( P e. Prime /\ ( x e. ZZ /\ y e. NN ) ) -> ( N =/= 0 -> ( N = ( x / y ) -> ( P pCnt N ) e. ZZ ) ) )
35 34 impancom 
 |-  ( ( P e. Prime /\ N =/= 0 ) -> ( ( x e. ZZ /\ y e. NN ) -> ( N = ( x / y ) -> ( P pCnt N ) e. ZZ ) ) )
36 35 adantrl 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( ( x e. ZZ /\ y e. NN ) -> ( N = ( x / y ) -> ( P pCnt N ) e. ZZ ) ) )
37 36 rexlimdvv 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( E. x e. ZZ E. y e. NN N = ( x / y ) -> ( P pCnt N ) e. ZZ ) )
38 3 37 mpd 
 |-  ( ( P e. Prime /\ ( N e. QQ /\ N =/= 0 ) ) -> ( P pCnt N ) e. ZZ )