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=\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},n^A,1\right)\right)$$
	pcmpt.2	$$⊢\phi \to \forall n\in \mathbb{P}A\in {\mathbb{N}}_0$$
	pcmpt.3	$$⊢\phi \to N\in \mathbb{N}$$
	pcmpt.4	$$⊢\phi \to P\in \mathbb{P}$$
	pcmpt.5	$$⊢n=P\to A=B$$
	pcmpt2.6	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge N}$$
Assertion	pcmpt2	$$⊢\phi \to P\mathrm{pCnt}\left(\frac{seq1\left(\times ,F\right)\left(M\right)}{seq1\left(\times ,F\right)\left(N\right)}\right)=if\left(\left(P\le M\wedge \neg P\le N\right),B,0\right)$$

Proof

Step	Hyp	Ref	Expression
1		pcmpt.1	$$⊢F=\left(n\in \mathbb{N}⟼if\left(n\in \mathbb{P},n^A,1\right)\right)$$
2		pcmpt.2	$$⊢\phi \to \forall n\in \mathbb{P}A\in {\mathbb{N}}_0$$
3		pcmpt.3	$$⊢\phi \to N\in \mathbb{N}$$
4		pcmpt.4	$$⊢\phi \to P\in \mathbb{P}$$
5		pcmpt.5	$$⊢n=P\to A=B$$
6		pcmpt2.6	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge N}$$
7	1 2	pcmptcl	$$⊢\phi \to \left(F:\mathbb{N}⟶\mathbb{N}\wedge seq1\left(\times ,F\right):\mathbb{N}⟶\mathbb{N}\right)$$
8	7	simprd	$$⊢\phi \to seq1\left(\times ,F\right):\mathbb{N}⟶\mathbb{N}$$
9		eluznn	$$⊢\left(N\in \mathbb{N}\wedge M\in {\mathbb{Z}}_{\ge N}\right)\to M\in \mathbb{N}$$
10	3 6 9	syl2anc	$$⊢\phi \to M\in \mathbb{N}$$
11	8 10	ffvelcdmd	$$⊢\phi \to seq1\left(\times ,F\right)\left(M\right)\in \mathbb{N}$$
12	11	nnzd	$$⊢\phi \to seq1\left(\times ,F\right)\left(M\right)\in \mathbb{Z}$$
13	11	nnne0d	$$⊢\phi \to seq1\left(\times ,F\right)\left(M\right)\ne 0$$
14	8 3	ffvelcdmd	$$⊢\phi \to seq1\left(\times ,F\right)\left(N\right)\in \mathbb{N}$$
15		pcdiv	$$⊢\left(P\in \mathbb{P}\wedge \left(seq1\left(\times ,F\right)\left(M\right)\in \mathbb{Z}\wedge seq1\left(\times ,F\right)\left(M\right)\ne 0\right)\wedge seq1\left(\times ,F\right)\left(N\right)\in \mathbb{N}\right)\to P\mathrm{pCnt}\left(\frac{seq1\left(\times ,F\right)\left(M\right)}{seq1\left(\times ,F\right)\left(N\right)}\right)=\left(P\mathrm{pCnt}seq1\left(\times ,F\right)\left(M\right)\right)-\left(P\mathrm{pCnt}seq1\left(\times ,F\right)\left(N\right)\right)$$
16	4 12 13 14 15	syl121anc	$$⊢\phi \to P\mathrm{pCnt}\left(\frac{seq1\left(\times ,F\right)\left(M\right)}{seq1\left(\times ,F\right)\left(N\right)}\right)=\left(P\mathrm{pCnt}seq1\left(\times ,F\right)\left(M\right)\right)-\left(P\mathrm{pCnt}seq1\left(\times ,F\right)\left(N\right)\right)$$
17	1 2 10 4 5	pcmpt	$$⊢\phi \to P\mathrm{pCnt}seq1\left(\times ,F\right)\left(M\right)=if\left(P\le M,B,0\right)$$
18	1 2 3 4 5	pcmpt	$$⊢\phi \to P\mathrm{pCnt}seq1\left(\times ,F\right)\left(N\right)=if\left(P\le N,B,0\right)$$
19	17 18	oveq12d	$$⊢\phi \to \left(P\mathrm{pCnt}seq1\left(\times ,F\right)\left(M\right)\right)-\left(P\mathrm{pCnt}seq1\left(\times ,F\right)\left(N\right)\right)=if\left(P\le M,B,0\right)-if\left(P\le N,B,0\right)$$
20	5	eleq1d	$$⊢n=P\to \left(A\in {\mathbb{N}}_0\leftrightarrow B\in {\mathbb{N}}_0\right)$$
21	20 2 4	rspcdva	$$⊢\phi \to B\in {\mathbb{N}}_0$$
22	21	nn0cnd	$$⊢\phi \to B\in ℂ$$
23	22	subidd	$$⊢\phi \to B-B=0$$
24	23	adantr	$$⊢\left(\phi \wedge P\le N\right)\to B-B=0$$
25		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
26	4 25	syl	$$⊢\phi \to P\in \mathbb{N}$$
27	26	nnred	$$⊢\phi \to P\in ℝ$$
28	27	adantr	$$⊢\left(\phi \wedge P\le N\right)\to P\in ℝ$$
29	3	nnred	$$⊢\phi \to N\in ℝ$$
30	29	adantr	$$⊢\left(\phi \wedge P\le N\right)\to N\in ℝ$$
31	10	nnred	$$⊢\phi \to M\in ℝ$$
32	31	adantr	$$⊢\left(\phi \wedge P\le N\right)\to M\in ℝ$$
33		simpr	$$⊢\left(\phi \wedge P\le N\right)\to P\le N$$
34		eluzle	$$⊢M\in {\mathbb{Z}}_{\ge N}\to N\le M$$
35	6 34	syl	$$⊢\phi \to N\le M$$
36	35	adantr	$$⊢\left(\phi \wedge P\le N\right)\to N\le M$$
37	28 30 32 33 36	letrd	$$⊢\left(\phi \wedge P\le N\right)\to P\le M$$
38	37	iftrued	$$⊢\left(\phi \wedge P\le N\right)\to if\left(P\le M,B,0\right)=B$$
39		iftrue	$$⊢P\le N\to if\left(P\le N,B,0\right)=B$$
40	39	adantl	$$⊢\left(\phi \wedge P\le N\right)\to if\left(P\le N,B,0\right)=B$$
41	38 40	oveq12d	$$⊢\left(\phi \wedge P\le N\right)\to if\left(P\le M,B,0\right)-if\left(P\le N,B,0\right)=B-B$$
42		simpr	$$⊢\left(P\le M\wedge \neg P\le N\right)\to \neg P\le N$$
43	42 33	nsyl3	$$⊢\left(\phi \wedge P\le N\right)\to \neg \left(P\le M\wedge \neg P\le N\right)$$
44	43	iffalsed	$$⊢\left(\phi \wedge P\le N\right)\to if\left(\left(P\le M\wedge \neg P\le N\right),B,0\right)=0$$
45	24 41 44	3eqtr4d	$$⊢\left(\phi \wedge P\le N\right)\to if\left(P\le M,B,0\right)-if\left(P\le N,B,0\right)=if\left(\left(P\le M\wedge \neg P\le N\right),B,0\right)$$
46		iffalse	$$⊢\neg P\le N\to if\left(P\le N,B,0\right)=0$$
47	46	oveq2d	$$⊢\neg P\le N\to if\left(P\le M,B,0\right)-if\left(P\le N,B,0\right)=if\left(P\le M,B,0\right)-0$$
48		0cn	$$⊢0\in ℂ$$
49		ifcl	$$⊢\left(B\in ℂ\wedge 0\in ℂ\right)\to if\left(P\le M,B,0\right)\in ℂ$$
50	22 48 49	sylancl	$$⊢\phi \to if\left(P\le M,B,0\right)\in ℂ$$
51	50	subid1d	$$⊢\phi \to if\left(P\le M,B,0\right)-0=if\left(P\le M,B,0\right)$$
52	47 51	sylan9eqr	$$⊢\left(\phi \wedge \neg P\le N\right)\to if\left(P\le M,B,0\right)-if\left(P\le N,B,0\right)=if\left(P\le M,B,0\right)$$
53		simpr	$$⊢\left(\phi \wedge \neg P\le N\right)\to \neg P\le N$$
54	53	biantrud	$$⊢\left(\phi \wedge \neg P\le N\right)\to \left(P\le M\leftrightarrow \left(P\le M\wedge \neg P\le N\right)\right)$$
55	54	ifbid	$$⊢\left(\phi \wedge \neg P\le N\right)\to if\left(P\le M,B,0\right)=if\left(\left(P\le M\wedge \neg P\le N\right),B,0\right)$$
56	52 55	eqtrd	$$⊢\left(\phi \wedge \neg P\le N\right)\to if\left(P\le M,B,0\right)-if\left(P\le N,B,0\right)=if\left(\left(P\le M\wedge \neg P\le N\right),B,0\right)$$
57	45 56	pm2.61dan	$$⊢\phi \to if\left(P\le M,B,0\right)-if\left(P\le N,B,0\right)=if\left(\left(P\le M\wedge \neg P\le N\right),B,0\right)$$
58	16 19 57	3eqtrd	$$⊢\phi \to P\mathrm{pCnt}\left(\frac{seq1\left(\times ,F\right)\left(M\right)}{seq1\left(\times ,F\right)\left(N\right)}\right)=if\left(\left(P\le M\wedge \neg P\le N\right),B,0\right)$$