Metamath Proof Explorer

Theorem pcdvdstr

Description: The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion pcdvdstr 
|- ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) -> ( P pCnt A ) <_ ( P pCnt B ) )

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 zq 
 |-  ( 0 e. ZZ -> 0 e. QQ )
3 1 2 ax-mp 
 |-  0 e. QQ
4 pcxcl 
 |-  ( ( P e. Prime /\ 0 e. QQ ) -> ( P pCnt 0 ) e. RR* )
5 3 4 mpan2 
 |-  ( P e. Prime -> ( P pCnt 0 ) e. RR* )
6 5 xrleidd 
 |-  ( P e. Prime -> ( P pCnt 0 ) <_ ( P pCnt 0 ) )
7 6 ad2antrr 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> ( P pCnt 0 ) <_ ( P pCnt 0 ) )
8 simpr 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> A = 0 )
9 8 oveq2d 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> ( P pCnt A ) = ( P pCnt 0 ) )
10 simplr3 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> A || B )
11 8 10 eqbrtrrd 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> 0 || B )
12 simplr2 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> B e. ZZ )
13 0dvds 
 |-  ( B e. ZZ -> ( 0 || B <-> B = 0 ) )
14 12 13 syl 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> ( 0 || B <-> B = 0 ) )
15 11 14 mpbid 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> B = 0 )
16 15 oveq2d 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> ( P pCnt B ) = ( P pCnt 0 ) )
17 7 9 16 3brtr4d 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A = 0 ) -> ( P pCnt A ) <_ ( P pCnt B ) )
18 prmnn 
 |-  ( P e. Prime -> P e. NN )
19 18 ad2antrr 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> P e. NN )
20 simpll 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> P e. Prime )
21 simplr1 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> A e. ZZ )
22 simpr 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> A =/= 0 )
23 pczcl 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) ) -> ( P pCnt A ) e. NN0 )
24 20 21 22 23 syl12anc 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> ( P pCnt A ) e. NN0 )
25 19 24 nnexpcld 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> ( P ^ ( P pCnt A ) ) e. NN )
26 25 nnzd 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> ( P ^ ( P pCnt A ) ) e. ZZ )
27 simplr2 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> B e. ZZ )
28 pczdvds 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ A =/= 0 ) ) -> ( P ^ ( P pCnt A ) ) || A )
29 20 21 22 28 syl12anc 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> ( P ^ ( P pCnt A ) ) || A )
30 simplr3 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> A || B )
31 26 21 27 29 30 dvdstrd 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> ( P ^ ( P pCnt A ) ) || B )
32 pcdvdsb 
 |-  ( ( P e. Prime /\ B e. ZZ /\ ( P pCnt A ) e. NN0 ) -> ( ( P pCnt A ) <_ ( P pCnt B ) <-> ( P ^ ( P pCnt A ) ) || B ) )
33 20 27 24 32 syl3anc 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> ( ( P pCnt A ) <_ ( P pCnt B ) <-> ( P ^ ( P pCnt A ) ) || B ) )
34 31 33 mpbird 
 |-  ( ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) /\ A =/= 0 ) -> ( P pCnt A ) <_ ( P pCnt B ) )
35 17 34 pm2.61dane 
 |-  ( ( P e. Prime /\ ( A e. ZZ /\ B e. ZZ /\ A || B ) ) -> ( P pCnt A ) <_ ( P pCnt B ) )