Theorem ppidif

Description: The difference of the prime-counting function ppi at two points counts the number of primes in an interval. (Contributed by Mario Carneiro, 21-Sep-2014)

	Ref	Expression
Assertion	ppidif	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\_}{\pi }\left(N\right)-\underset{\_}{\pi }\left(M\right)=\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|$$

Proof

Step	Hyp	Ref	Expression
1		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
2		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
3		2z	$$⊢2\in \mathbb{Z}$$
4		ifcl	$$⊢\left(M\in \mathbb{Z}\wedge 2\in \mathbb{Z}\right)\to if\left(M\le 2,M,2\right)\in \mathbb{Z}$$
5	2 3 4	sylancl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to if\left(M\le 2,M,2\right)\in \mathbb{Z}$$
6	3	a1i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to 2\in \mathbb{Z}$$
7	2	zred	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in ℝ$$
8		2re	$$⊢2\in ℝ$$
9		min2	$$⊢\left(M\in ℝ\wedge 2\in ℝ\right)\to if\left(M\le 2,M,2\right)\le 2$$
10	7 8 9	sylancl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to if\left(M\le 2,M,2\right)\le 2$$
11		eluz2	$$⊢2\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\leftrightarrow \left(if\left(M\le 2,M,2\right)\in \mathbb{Z}\wedge 2\in \mathbb{Z}\wedge if\left(M\le 2,M,2\right)\le 2\right)$$
12	5 6 10 11	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to 2\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}$$
13		ppival2g	$$⊢\left(N\in \mathbb{Z}\wedge 2\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\right)\to \underset{\_}{\pi }\left(N\right)=\left|\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right|$$
14	1 12 13	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\_}{\pi }\left(N\right)=\left|\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right|$$
15		min1	$$⊢\left(M\in ℝ\wedge 2\in ℝ\right)\to if\left(M\le 2,M,2\right)\le M$$
16	7 8 15	sylancl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to if\left(M\le 2,M,2\right)\le M$$
17		eluz2	$$⊢M\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\leftrightarrow \left(if\left(M\le 2,M,2\right)\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge if\left(M\le 2,M,2\right)\le M\right)$$
18	5 2 16 17	syl3anbrc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}$$
19		id	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in {\mathbb{Z}}_{\ge M}$$
20		elfzuzb	$$⊢M\in \left(if\left(M\le 2,M,2\right)\dots N\right)\leftrightarrow \left(M\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\wedge N\in {\mathbb{Z}}_{\ge M}\right)$$
21	18 19 20	sylanbrc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(if\left(M\le 2,M,2\right)\dots N\right)$$
22		fzsplit	$$⊢M\in \left(if\left(M\le 2,M,2\right)\dots N\right)\to \left(if\left(M\le 2,M,2\right)\dots N\right)=\left(if\left(M\le 2,M,2\right)\dots M\right)\cup \left(M+1\dots N\right)$$
23	21 22	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots N\right)=\left(if\left(M\le 2,M,2\right)\dots M\right)\cup \left(M+1\dots N\right)$$
24	23	ineq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}=\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cup \left(M+1\dots N\right)\right)\cap \mathbb{P}$$
25		indir	$$⊢\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cup \left(M+1\dots N\right)\right)\cap \mathbb{P}=\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)$$
26	24 25	eqtrdi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}=\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)$$
27	26	fveq2d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left|\left(if\left(M\le 2,M,2\right)\dots N\right)\cap \mathbb{P}\right|=\left|\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)\right|$$
28		fzfi	$$⊢\left(if\left(M\le 2,M,2\right)\dots M\right)\in \mathrm{Fin}$$
29		inss1	$$⊢\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\subseteq \left(if\left(M\le 2,M,2\right)\dots M\right)$$
30		ssfi	$$⊢\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\in \mathrm{Fin}\wedge \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\subseteq \left(if\left(M\le 2,M,2\right)\dots M\right)\right)\to \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\in \mathrm{Fin}$$
31	28 29 30	mp2an	$$⊢\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\in \mathrm{Fin}$$
32		fzfi	$$⊢\left(M+1\dots N\right)\in \mathrm{Fin}$$
33		inss1	$$⊢\left(M+1\dots N\right)\cap \mathbb{P}\subseteq \left(M+1\dots N\right)$$
34		ssfi	$$⊢\left(\left(M+1\dots N\right)\in \mathrm{Fin}\wedge \left(M+1\dots N\right)\cap \mathbb{P}\subseteq \left(M+1\dots N\right)\right)\to \left(M+1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
35	32 33 34	mp2an	$$⊢\left(M+1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}$$
36	7	ltp1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M<M+1$$
37		fzdisj	$$⊢M<M+1\to \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \left(M+1\dots N\right)=\varnothing$$
38	36 37	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(if\left(M\le 2,M,2\right)\dots M\right)\cap \left(M+1\dots N\right)=\varnothing$$
39	38	ineq1d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \left(M+1\dots N\right)\right)\cap \mathbb{P}=\varnothing \cap \mathbb{P}$$
40		inindir	$$⊢\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \left(M+1\dots N\right)\right)\cap \mathbb{P}=\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cap \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)$$
41		0in	$$⊢\varnothing \cap \mathbb{P}=\varnothing$$
42	39 40 41	3eqtr3g	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cap \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)=\varnothing$$
43		hashun	$$⊢\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\in \mathrm{Fin}\wedge \left(M+1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}\wedge \left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cap \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)=\varnothing \right)\to \left|\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)\right|=\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|+\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|$$
44	31 35 42 43	mp3an12i	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left|\left(\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right)\cup \left(\left(M+1\dots N\right)\cap \mathbb{P}\right)\right|=\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|+\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|$$
45	14 27 44	3eqtrd	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\_}{\pi }\left(N\right)=\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|+\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|$$
46		ppival2g	$$⊢\left(M\in \mathbb{Z}\wedge 2\in {\mathbb{Z}}_{\ge if\left(M\le 2,M,2\right)}\right)\to \underset{\_}{\pi }\left(M\right)=\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|$$
47	2 12 46	syl2anc	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\_}{\pi }\left(M\right)=\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|$$
48	45 47	oveq12d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\_}{\pi }\left(N\right)-\underset{\_}{\pi }\left(M\right)=\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|+\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|-\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|$$
49		hashcl	$$⊢\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\in \mathrm{Fin}\to \left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|\in {\mathbb{N}}_0$$
50	31 49	ax-mp	$$⊢\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|\in {\mathbb{N}}_0$$
51	50	nn0cni	$$⊢\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|\in ℂ$$
52		hashcl	$$⊢\left(M+1\dots N\right)\cap \mathbb{P}\in \mathrm{Fin}\to \left|\left(M+1\dots N\right)\cap \mathbb{P}\right|\in {\mathbb{N}}_0$$
53	35 52	ax-mp	$$⊢\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|\in {\mathbb{N}}_0$$
54	53	nn0cni	$$⊢\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|\in ℂ$$
55		pncan2	$$⊢\left(\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|\in ℂ\wedge \left|\left(M+1\dots N\right)\cap \mathbb{P}\right|\in ℂ\right)\to \left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|+\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|-\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|=\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|$$
56	51 54 55	mp2an	$$⊢\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|+\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|-\left|\left(if\left(M\le 2,M,2\right)\dots M\right)\cap \mathbb{P}\right|=\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|$$
57	48 56	eqtrdi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \underset{\_}{\pi }\left(N\right)-\underset{\_}{\pi }\left(M\right)=\left|\left(M+1\dots N\right)\cap \mathbb{P}\right|$$