# Metamath Proof Explorer

## 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 ℙ\in \mathrm{Fin}$
3 1 2 syl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to \left[0,{B}\right]\cap ℙ\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 ℙ\subseteq \left[0,{B}\right]\cap ℙ$
11 ssdomg ${⊢}\left[0,{B}\right]\cap ℙ\in \mathrm{Fin}\to \left(\left[0,{A}\right]\cap ℙ\subseteq \left[0,{B}\right]\cap ℙ\to \left(\left[0,{A}\right]\cap ℙ\right)\preccurlyeq \left(\left[0,{B}\right]\cap ℙ\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 ℙ\right)\preccurlyeq \left(\left[0,{B}\right]\cap ℙ\right)$
13 ppifi ${⊢}{A}\in ℝ\to \left[0,{A}\right]\cap ℙ\in \mathrm{Fin}$
14 13 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to \left[0,{A}\right]\cap ℙ\in \mathrm{Fin}$
15 hashdom ${⊢}\left(\left[0,{A}\right]\cap ℙ\in \mathrm{Fin}\wedge \left[0,{B}\right]\cap ℙ\in \mathrm{Fin}\right)\to \left(\left|\left[0,{A}\right]\cap ℙ\right|\le \left|\left[0,{B}\right]\cap ℙ\right|↔\left(\left[0,{A}\right]\cap ℙ\right)\preccurlyeq \left(\left[0,{B}\right]\cap ℙ\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 ℙ\right|\le \left|\left[0,{B}\right]\cap ℙ\right|↔\left(\left[0,{A}\right]\cap ℙ\right)\preccurlyeq \left(\left[0,{B}\right]\cap ℙ\right)\right)$
17 12 16 mpbird ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to \left|\left[0,{A}\right]\cap ℙ\right|\le \left|\left[0,{B}\right]\cap ℙ\right|$
18 ppival ${⊢}{A}\in ℝ\to \underset{_}{\pi }\left({A}\right)=\left|\left[0,{A}\right]\cap ℙ\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 ℙ\right|$
20 ppival ${⊢}{B}\in ℝ\to \underset{_}{\pi }\left({B}\right)=\left|\left[0,{B}\right]\cap ℙ\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 ℙ\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)$