Theorem ppiwordi

Description: The prime-counting function ppi is weakly increasing. (Contributed by Mario Carneiro, 19-Sep-2014)

	Ref	Expression
Assertion	ppiwordi	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \underset{\_}{\pi }\left(A\right)\le \underset{\_}{\pi }\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simp2	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to B\in ℝ$$
2		ppifi	$$⊢B\in ℝ\to \left[0,B\right]\cap \mathbb{P}\in \mathrm{Fin}$$
3	1 2	syl	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left[0,B\right]\cap \mathbb{P}\in \mathrm{Fin}$$
4		0red	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to 0\in ℝ$$
5		0le0	$$⊢0\le 0$$
6	5	a1i	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to 0\le 0$$
7		simp3	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to A\le B$$
8		iccss	$$⊢\left(\left(0\in ℝ\wedge B\in ℝ\right)\wedge \left(0\le 0\wedge A\le B\right)\right)\to \left[0,A\right]\subseteq \left[0,B\right]$$
9	4 1 6 7 8	syl22anc	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left[0,A\right]\subseteq \left[0,B\right]$$
10	9	ssrind	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left[0,A\right]\cap \mathbb{P}\subseteq \left[0,B\right]\cap \mathbb{P}$$
11		ssdomg	$$⊢\left[0,B\right]\cap \mathbb{P}\in \mathrm{Fin}\to \left(\left[0,A\right]\cap \mathbb{P}\subseteq \left[0,B\right]\cap \mathbb{P}\to \left(\left[0,A\right]\cap \mathbb{P}\right)\preccurlyeq \left(\left[0,B\right]\cap \mathbb{P}\right)\right)$$
12	3 10 11	sylc	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left(\left[0,A\right]\cap \mathbb{P}\right)\preccurlyeq \left(\left[0,B\right]\cap \mathbb{P}\right)$$
13		ppifi	$$⊢A\in ℝ\to \left[0,A\right]\cap \mathbb{P}\in \mathrm{Fin}$$
14	13	3ad2ant1	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left[0,A\right]\cap \mathbb{P}\in \mathrm{Fin}$$
15		hashdom	$$⊢\left(\left[0,A\right]\cap \mathbb{P}\in \mathrm{Fin}\wedge \left[0,B\right]\cap \mathbb{P}\in \mathrm{Fin}\right)\to \left(\left|\left[0,A\right]\cap \mathbb{P}\right|\le \left|\left[0,B\right]\cap \mathbb{P}\right|\leftrightarrow \left(\left[0,A\right]\cap \mathbb{P}\right)\preccurlyeq \left(\left[0,B\right]\cap \mathbb{P}\right)\right)$$
16	14 3 15	syl2anc	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left(\left|\left[0,A\right]\cap \mathbb{P}\right|\le \left|\left[0,B\right]\cap \mathbb{P}\right|\leftrightarrow \left(\left[0,A\right]\cap \mathbb{P}\right)\preccurlyeq \left(\left[0,B\right]\cap \mathbb{P}\right)\right)$$
17	12 16	mpbird	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \left|\left[0,A\right]\cap \mathbb{P}\right|\le \left|\left[0,B\right]\cap \mathbb{P}\right|$$
18		ppival	$$⊢A\in ℝ\to \underset{\_}{\pi }\left(A\right)=\left|\left[0,A\right]\cap \mathbb{P}\right|$$
19	18	3ad2ant1	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \underset{\_}{\pi }\left(A\right)=\left|\left[0,A\right]\cap \mathbb{P}\right|$$
20		ppival	$$⊢B\in ℝ\to \underset{\_}{\pi }\left(B\right)=\left|\left[0,B\right]\cap \mathbb{P}\right|$$
21	1 20	syl	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \underset{\_}{\pi }\left(B\right)=\left|\left[0,B\right]\cap \mathbb{P}\right|$$
22	17 19 21	3brtr4d	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge A\le B\right)\to \underset{\_}{\pi }\left(A\right)\le \underset{\_}{\pi }\left(B\right)$$