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	ffvelcdmd	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℕ )
12	11	nnzd	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ∈ ℤ )
13	11	nnne0d	⊢ ( 𝜑 → ( seq 1 ( · , 𝐹 ) ‘ 𝑀 ) ≠ 0 )
14	8 3	ffvelcdmd	⊢ ( 𝜑 → ( 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 ) )