Metamath Proof Explorer

Theorem pcmpt2

Description: Dividing two prime count maps yields a number with all dividing primes confined to an interval. (Contributed by Mario Carneiro, 14-Mar-2014)

Ref Expression
Hypotheses pcmpt.1 
|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )
pcmpt.2 
|- ( ph -> A. n e. Prime A e. NN0 )
pcmpt.3 
|- ( ph -> N e. NN )
pcmpt.4 
|- ( ph -> P e. Prime )
pcmpt.5 
|- ( n = P -> A = B )
pcmpt2.6 
|- ( ph -> M e. ( ZZ>= ` N ) )
Assertion pcmpt2 
|- ( ph -> ( P pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) = if ( ( P <_ M /\ -. P <_ N ) , B , 0 ) )

Proof

Step Hyp Ref Expression
1 pcmpt.1 
 |-  F = ( n e. NN |-> if ( n e. Prime , ( n ^ A ) , 1 ) )
2 pcmpt.2 
 |-  ( ph -> A. n e. Prime A e. NN0 )
3 pcmpt.3 
 |-  ( ph -> N e. NN )
4 pcmpt.4 
 |-  ( ph -> P e. Prime )
5 pcmpt.5 
 |-  ( n = P -> A = B )
6 pcmpt2.6 
 |-  ( ph -> M e. ( ZZ>= ` N ) )
7 1 2 pcmptcl 
 |-  ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
8 7 simprd 
 |-  ( ph -> seq 1 ( x. , F ) : NN --> NN )
9 eluznn 
 |-  ( ( N e. NN /\ M e. ( ZZ>= ` N ) ) -> M e. NN )
10 3 6 9 syl2anc 
 |-  ( ph -> M e. NN )
11 8 10 ffvelrnd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) e. NN )
12 11 nnzd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) e. ZZ )
13 11 nnne0d 
 |-  ( ph -> ( seq 1 ( x. , F ) ` M ) =/= 0 )
14 8 3 ffvelrnd 
 |-  ( ph -> ( seq 1 ( x. , F ) ` N ) e. NN )
15 pcdiv 
 |-  ( ( P e. Prime /\ ( ( seq 1 ( x. , F ) ` M ) e. ZZ /\ ( seq 1 ( x. , F ) ` M ) =/= 0 ) /\ ( seq 1 ( x. , F ) ` N ) e. NN ) -> ( P pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) = ( ( P pCnt ( seq 1 ( x. , F ) ` M ) ) - ( P pCnt ( seq 1 ( x. , F ) ` N ) ) ) )
16 4 12 13 14 15 syl121anc 
 |-  ( ph -> ( P pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) = ( ( P pCnt ( seq 1 ( x. , F ) ` M ) ) - ( P pCnt ( seq 1 ( x. , F ) ` N ) ) ) )
17 1 2 10 4 5 pcmpt 
 |-  ( ph -> ( P pCnt ( seq 1 ( x. , F ) ` M ) ) = if ( P <_ M , B , 0 ) )
18 1 2 3 4 5 pcmpt 
 |-  ( ph -> ( P pCnt ( seq 1 ( x. , F ) ` N ) ) = if ( P <_ N , B , 0 ) )
19 17 18 oveq12d 
 |-  ( ph -> ( ( P pCnt ( seq 1 ( x. , F ) ` M ) ) - ( P pCnt ( seq 1 ( x. , F ) ` N ) ) ) = ( if ( P <_ M , B , 0 ) - if ( P <_ N , B , 0 ) ) )
20 5 eleq1d 
 |-  ( n = P -> ( A e. NN0 <-> B e. NN0 ) )
21 20 2 4 rspcdva 
 |-  ( ph -> B e. NN0 )
22 21 nn0cnd 
 |-  ( ph -> B e. CC )
23 22 subidd 
 |-  ( ph -> ( B - B ) = 0 )
24 23 adantr 
 |-  ( ( ph /\ P <_ N ) -> ( B - B ) = 0 )
25 prmnn 
 |-  ( P e. Prime -> P e. NN )
26 4 25 syl 
 |-  ( ph -> P e. NN )
27 26 nnred 
 |-  ( ph -> P e. RR )
28 27 adantr 
 |-  ( ( ph /\ P <_ N ) -> P e. RR )
29 3 nnred 
 |-  ( ph -> N e. RR )
30 29 adantr 
 |-  ( ( ph /\ P <_ N ) -> N e. RR )
31 10 nnred 
 |-  ( ph -> M e. RR )
32 31 adantr 
 |-  ( ( ph /\ P <_ N ) -> M e. RR )
33 simpr 
 |-  ( ( ph /\ P <_ N ) -> P <_ N )
34 eluzle 
 |-  ( M e. ( ZZ>= ` N ) -> N <_ M )
35 6 34 syl 
 |-  ( ph -> N <_ M )
36 35 adantr 
 |-  ( ( ph /\ P <_ N ) -> N <_ M )
37 28 30 32 33 36 letrd 
 |-  ( ( ph /\ P <_ N ) -> P <_ M )
38 37 iftrued 
 |-  ( ( ph /\ P <_ N ) -> if ( P <_ M , B , 0 ) = B )
39 iftrue 
 |-  ( P <_ N -> if ( P <_ N , B , 0 ) = B )
40 39 adantl 
 |-  ( ( ph /\ P <_ N ) -> if ( P <_ N , B , 0 ) = B )
41 38 40 oveq12d 
 |-  ( ( ph /\ P <_ N ) -> ( if ( P <_ M , B , 0 ) - if ( P <_ N , B , 0 ) ) = ( B - B ) )
42 simpr 
 |-  ( ( P <_ M /\ -. P <_ N ) -> -. P <_ N )
43 42 33 nsyl3 
 |-  ( ( ph /\ P <_ N ) -> -. ( P <_ M /\ -. P <_ N ) )
44 43 iffalsed 
 |-  ( ( ph /\ P <_ N ) -> if ( ( P <_ M /\ -. P <_ N ) , B , 0 ) = 0 )
45 24 41 44 3eqtr4d 
 |-  ( ( ph /\ P <_ N ) -> ( if ( P <_ M , B , 0 ) - if ( P <_ N , B , 0 ) ) = if ( ( P <_ M /\ -. P <_ N ) , B , 0 ) )
46 iffalse 
 |-  ( -. P <_ N -> if ( P <_ N , B , 0 ) = 0 )
47 46 oveq2d 
 |-  ( -. P <_ N -> ( if ( P <_ M , B , 0 ) - if ( P <_ N , B , 0 ) ) = ( if ( P <_ M , B , 0 ) - 0 ) )
48 0cn 
 |-  0 e. CC
49 ifcl 
 |-  ( ( B e. CC /\ 0 e. CC ) -> if ( P <_ M , B , 0 ) e. CC )
50 22 48 49 sylancl 
 |-  ( ph -> if ( P <_ M , B , 0 ) e. CC )
51 50 subid1d 
 |-  ( ph -> ( if ( P <_ M , B , 0 ) - 0 ) = if ( P <_ M , B , 0 ) )
52 47 51 sylan9eqr 
 |-  ( ( ph /\ -. P <_ N ) -> ( if ( P <_ M , B , 0 ) - if ( P <_ N , B , 0 ) ) = if ( P <_ M , B , 0 ) )
53 simpr 
 |-  ( ( ph /\ -. P <_ N ) -> -. P <_ N )
54 53 biantrud 
 |-  ( ( ph /\ -. P <_ N ) -> ( P <_ M <-> ( P <_ M /\ -. P <_ N ) ) )
55 54 ifbid 
 |-  ( ( ph /\ -. P <_ N ) -> if ( P <_ M , B , 0 ) = if ( ( P <_ M /\ -. P <_ N ) , B , 0 ) )
56 52 55 eqtrd 
 |-  ( ( ph /\ -. P <_ N ) -> ( if ( P <_ M , B , 0 ) - if ( P <_ N , B , 0 ) ) = if ( ( P <_ M /\ -. P <_ N ) , B , 0 ) )
57 45 56 pm2.61dan 
 |-  ( ph -> ( if ( P <_ M , B , 0 ) - if ( P <_ N , B , 0 ) ) = if ( ( P <_ M /\ -. P <_ N ) , B , 0 ) )
58 16 19 57 3eqtrd 
 |-  ( ph -> ( P pCnt ( ( seq 1 ( x. , F ) ` M ) / ( seq 1 ( x. , F ) ` N ) ) ) = if ( ( P <_ M /\ -. P <_ N ) , B , 0 ) )