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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) )
pcmpt.2 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ 𝐴 ∈ ℕ0 )
pcmpt.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
pcmpt.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
pcmpt.5 ⊢ ( 𝑛 = 𝑃 → 𝐴 = 𝐵 )
pcmpt2.6 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
Assertion pcmpt2 ( 𝜑 → ( 𝑃 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) ) = if ( ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) , 𝐵 , 0 ) )

Proof

Step Hyp Ref Expression
1 pcmpt.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 𝑛 ↑ 𝐴 ) , 1 ) )
2 pcmpt.2 ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℙ 𝐴 ∈ ℕ0 )
3 pcmpt.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 pcmpt.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 pcmpt.5 ⊢ ( 𝑛 = 𝑃 → 𝐴 = 𝐵 )
6 pcmpt2.6 ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) )
7 1 2 pcmptcl ⊢ ( 𝜑 → ( 𝐹 : ℕ ⟶ ℕ ∧ seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ ) )
8 7 simprd ⊢ ( 𝜑 → seq 1 ( · , 𝐹 ) : ℕ ⟶ ℕ )
9 eluznn ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑀 ∈ ℕ )
10 3 6 9 syl2anc ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
11 8 10 ffvelrnd ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ )
12 11 nnzd ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℤ )
13 11 nnne0d ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 )
14 8 3 ffvelrnd ⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℕ )
15 pcdiv ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℤ ∧ ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 ) ∧ ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ∈ ℕ ) → ( 𝑃 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) ) = ( ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) − ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) ) )
16 4 12 13 14 15 syl121anc ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) ) = ( ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) − ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) ) )
17 1 2 10 4 5 pcmpt ⊢ ( 𝜑 → ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) = if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) )
18 1 2 3 4 5 pcmpt ⊢ ( 𝜑 → ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) = if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) )
19 17 18 oveq12d ⊢ ( 𝜑 → ( ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ) − ( 𝑃 pCnt ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) ) = ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) ) )
20 5 eleq1d ⊢ ( 𝑛 = 𝑃 → ( 𝐴 ∈ ℕ0 ↔ 𝐵 ∈ ℕ0 ) )
21 20 2 4 rspcdva ⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
22 21 nn0cnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
23 22 subidd ⊢ ( 𝜑 → ( 𝐵 − 𝐵 ) = 0 )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → ( 𝐵 − 𝐵 ) = 0 )
25 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
26 4 25 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
27 26 nnred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → 𝑃 ∈ ℝ )
29 3 nnred ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
31 10 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → 𝑀 ∈ ℝ )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → 𝑃 ≤ 𝑁 )
34 eluzle ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝑀 )
35 6 34 syl ⊢ ( 𝜑 → 𝑁 ≤ 𝑀 )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → 𝑁 ≤ 𝑀 )
37 28 30 32 33 36 letrd ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → 𝑃 ≤ 𝑀 )
38 37 iftrued ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) = 𝐵 )
39 iftrue ⊢ ( 𝑃 ≤ 𝑁 → if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) = 𝐵 )
40 39 adantl ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) = 𝐵 )
41 38 40 oveq12d ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) ) = ( 𝐵 − 𝐵 ) )
42 simpr ⊢ ( ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) → ¬ 𝑃 ≤ 𝑁 )
43 42 33 nsyl3 ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → ¬ ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) )
44 43 iffalsed ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → if ( ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) , 𝐵 , 0 ) = 0 )
45 24 41 44 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑃 ≤ 𝑁 ) → ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) ) = if ( ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) , 𝐵 , 0 ) )
46 iffalse ⊢ ( ¬ 𝑃 ≤ 𝑁 → if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) = 0 )
47 46 oveq2d ⊢ ( ¬ 𝑃 ≤ 𝑁 → ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) ) = ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − 0 ) )
48 0cn ⊢ 0 ∈ ℂ
49 ifcl ⊢ ( ( 𝐵 ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) ∈ ℂ )
50 22 48 49 sylancl ⊢ ( 𝜑 → if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) ∈ ℂ )
51 50 subid1d ⊢ ( 𝜑 → ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − 0 ) = if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) )
52 47 51 sylan9eqr ⊢ ( ( 𝜑 ∧ ¬ 𝑃 ≤ 𝑁 ) → ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) ) = if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) )
53 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝑃 ≤ 𝑁 ) → ¬ 𝑃 ≤ 𝑁 )
54 53 biantrud ⊢ ( ( 𝜑 ∧ ¬ 𝑃 ≤ 𝑁 ) → ( 𝑃 ≤ 𝑀 ↔ ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) ) )
55 54 ifbid ⊢ ( ( 𝜑 ∧ ¬ 𝑃 ≤ 𝑁 ) → if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) = if ( ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) , 𝐵 , 0 ) )
56 52 55 eqtrd ⊢ ( ( 𝜑 ∧ ¬ 𝑃 ≤ 𝑁 ) → ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) ) = if ( ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) , 𝐵 , 0 ) )
57 45 56 pm2.61dan ⊢ ( 𝜑 → ( if ( 𝑃 ≤ 𝑀 , 𝐵 , 0 ) − if ( 𝑃 ≤ 𝑁 , 𝐵 , 0 ) ) = if ( ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) , 𝐵 , 0 ) )
58 16 19 57 3eqtrd ⊢ ( 𝜑 → ( 𝑃 pCnt ( ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) / ( seq 1 ( · , 𝐹 ) ‘ 𝑁 ) ) ) = if ( ( 𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁 ) , 𝐵 , 0 ) )