# Metamath Proof Explorer

## Theorem ppiltx

Description: The prime-counting function ppi is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion ppiltx ${⊢}{A}\in {ℝ}^{+}\to \underset{_}{\pi }\left({A}\right)<{A}$

### Proof

Step Hyp Ref Expression
1 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
2 ppicl ${⊢}{A}\in ℝ\to \underset{_}{\pi }\left({A}\right)\in {ℕ}_{0}$
3 1 2 syl ${⊢}{A}\in {ℝ}^{+}\to \underset{_}{\pi }\left({A}\right)\in {ℕ}_{0}$
4 3 nn0red ${⊢}{A}\in {ℝ}^{+}\to \underset{_}{\pi }\left({A}\right)\in ℝ$
5 4 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \underset{_}{\pi }\left({A}\right)\in ℝ$
6 reflcl ${⊢}{A}\in ℝ\to ⌊{A}⌋\in ℝ$
7 1 6 syl ${⊢}{A}\in {ℝ}^{+}\to ⌊{A}⌋\in ℝ$
8 7 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to ⌊{A}⌋\in ℝ$
9 1 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to {A}\in ℝ$
10 fzfi ${⊢}\left(1\dots ⌊{A}⌋\right)\in \mathrm{Fin}$
11 inss1 ${⊢}\left(2\dots ⌊{A}⌋\right)\cap ℙ\subseteq \left(2\dots ⌊{A}⌋\right)$
12 2eluzge1 ${⊢}2\in {ℤ}_{\ge 1}$
13 fzss1 ${⊢}2\in {ℤ}_{\ge 1}\to \left(2\dots ⌊{A}⌋\right)\subseteq \left(1\dots ⌊{A}⌋\right)$
14 12 13 mp1i ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left(2\dots ⌊{A}⌋\right)\subseteq \left(1\dots ⌊{A}⌋\right)$
15 simpr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to ⌊{A}⌋\in ℕ$
16 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
17 15 16 eleqtrdi ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to ⌊{A}⌋\in {ℤ}_{\ge 1}$
18 eluzfz1 ${⊢}⌊{A}⌋\in {ℤ}_{\ge 1}\to 1\in \left(1\dots ⌊{A}⌋\right)$
19 17 18 syl ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to 1\in \left(1\dots ⌊{A}⌋\right)$
20 1lt2 ${⊢}1<2$
21 1re ${⊢}1\in ℝ$
22 2re ${⊢}2\in ℝ$
23 21 22 ltnlei ${⊢}1<2↔¬2\le 1$
24 20 23 mpbi ${⊢}¬2\le 1$
25 elfzle1 ${⊢}1\in \left(2\dots ⌊{A}⌋\right)\to 2\le 1$
26 24 25 mto ${⊢}¬1\in \left(2\dots ⌊{A}⌋\right)$
27 nelne1 ${⊢}\left(1\in \left(1\dots ⌊{A}⌋\right)\wedge ¬1\in \left(2\dots ⌊{A}⌋\right)\right)\to \left(1\dots ⌊{A}⌋\right)\ne \left(2\dots ⌊{A}⌋\right)$
28 19 26 27 sylancl ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left(1\dots ⌊{A}⌋\right)\ne \left(2\dots ⌊{A}⌋\right)$
29 28 necomd ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left(2\dots ⌊{A}⌋\right)\ne \left(1\dots ⌊{A}⌋\right)$
30 df-pss ${⊢}\left(2\dots ⌊{A}⌋\right)\subset \left(1\dots ⌊{A}⌋\right)↔\left(\left(2\dots ⌊{A}⌋\right)\subseteq \left(1\dots ⌊{A}⌋\right)\wedge \left(2\dots ⌊{A}⌋\right)\ne \left(1\dots ⌊{A}⌋\right)\right)$
31 14 29 30 sylanbrc ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left(2\dots ⌊{A}⌋\right)\subset \left(1\dots ⌊{A}⌋\right)$
32 sspsstr ${⊢}\left(\left(2\dots ⌊{A}⌋\right)\cap ℙ\subseteq \left(2\dots ⌊{A}⌋\right)\wedge \left(2\dots ⌊{A}⌋\right)\subset \left(1\dots ⌊{A}⌋\right)\right)\to \left(2\dots ⌊{A}⌋\right)\cap ℙ\subset \left(1\dots ⌊{A}⌋\right)$
33 11 31 32 sylancr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left(2\dots ⌊{A}⌋\right)\cap ℙ\subset \left(1\dots ⌊{A}⌋\right)$
34 php3 ${⊢}\left(\left(1\dots ⌊{A}⌋\right)\in \mathrm{Fin}\wedge \left(2\dots ⌊{A}⌋\right)\cap ℙ\subset \left(1\dots ⌊{A}⌋\right)\right)\to \left(\left(2\dots ⌊{A}⌋\right)\cap ℙ\right)\prec \left(1\dots ⌊{A}⌋\right)$
35 10 33 34 sylancr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left(\left(2\dots ⌊{A}⌋\right)\cap ℙ\right)\prec \left(1\dots ⌊{A}⌋\right)$
36 fzfi ${⊢}\left(2\dots ⌊{A}⌋\right)\in \mathrm{Fin}$
37 ssfi ${⊢}\left(\left(2\dots ⌊{A}⌋\right)\in \mathrm{Fin}\wedge \left(2\dots ⌊{A}⌋\right)\cap ℙ\subseteq \left(2\dots ⌊{A}⌋\right)\right)\to \left(2\dots ⌊{A}⌋\right)\cap ℙ\in \mathrm{Fin}$
38 36 11 37 mp2an ${⊢}\left(2\dots ⌊{A}⌋\right)\cap ℙ\in \mathrm{Fin}$
39 hashsdom ${⊢}\left(\left(2\dots ⌊{A}⌋\right)\cap ℙ\in \mathrm{Fin}\wedge \left(1\dots ⌊{A}⌋\right)\in \mathrm{Fin}\right)\to \left(\left|\left(2\dots ⌊{A}⌋\right)\cap ℙ\right|<\left|\left(1\dots ⌊{A}⌋\right)\right|↔\left(\left(2\dots ⌊{A}⌋\right)\cap ℙ\right)\prec \left(1\dots ⌊{A}⌋\right)\right)$
40 38 10 39 mp2an ${⊢}\left|\left(2\dots ⌊{A}⌋\right)\cap ℙ\right|<\left|\left(1\dots ⌊{A}⌋\right)\right|↔\left(\left(2\dots ⌊{A}⌋\right)\cap ℙ\right)\prec \left(1\dots ⌊{A}⌋\right)$
41 35 40 sylibr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left|\left(2\dots ⌊{A}⌋\right)\cap ℙ\right|<\left|\left(1\dots ⌊{A}⌋\right)\right|$
42 1 flcld ${⊢}{A}\in {ℝ}^{+}\to ⌊{A}⌋\in ℤ$
43 ppival2 ${⊢}⌊{A}⌋\in ℤ\to \underset{_}{\pi }\left(⌊{A}⌋\right)=\left|\left(2\dots ⌊{A}⌋\right)\cap ℙ\right|$
44 42 43 syl ${⊢}{A}\in {ℝ}^{+}\to \underset{_}{\pi }\left(⌊{A}⌋\right)=\left|\left(2\dots ⌊{A}⌋\right)\cap ℙ\right|$
45 ppifl ${⊢}{A}\in ℝ\to \underset{_}{\pi }\left(⌊{A}⌋\right)=\underset{_}{\pi }\left({A}\right)$
46 1 45 syl ${⊢}{A}\in {ℝ}^{+}\to \underset{_}{\pi }\left(⌊{A}⌋\right)=\underset{_}{\pi }\left({A}\right)$
47 44 46 eqtr3d ${⊢}{A}\in {ℝ}^{+}\to \left|\left(2\dots ⌊{A}⌋\right)\cap ℙ\right|=\underset{_}{\pi }\left({A}\right)$
48 47 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left|\left(2\dots ⌊{A}⌋\right)\cap ℙ\right|=\underset{_}{\pi }\left({A}\right)$
49 rpge0 ${⊢}{A}\in {ℝ}^{+}\to 0\le {A}$
50 flge0nn0 ${⊢}\left({A}\in ℝ\wedge 0\le {A}\right)\to ⌊{A}⌋\in {ℕ}_{0}$
51 1 49 50 syl2anc ${⊢}{A}\in {ℝ}^{+}\to ⌊{A}⌋\in {ℕ}_{0}$
52 hashfz1 ${⊢}⌊{A}⌋\in {ℕ}_{0}\to \left|\left(1\dots ⌊{A}⌋\right)\right|=⌊{A}⌋$
53 51 52 syl ${⊢}{A}\in {ℝ}^{+}\to \left|\left(1\dots ⌊{A}⌋\right)\right|=⌊{A}⌋$
54 53 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \left|\left(1\dots ⌊{A}⌋\right)\right|=⌊{A}⌋$
55 41 48 54 3brtr3d ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \underset{_}{\pi }\left({A}\right)<⌊{A}⌋$
56 flle ${⊢}{A}\in ℝ\to ⌊{A}⌋\le {A}$
57 9 56 syl ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to ⌊{A}⌋\le {A}$
58 5 8 9 55 57 ltletrd ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋\in ℕ\right)\to \underset{_}{\pi }\left({A}\right)<{A}$
59 46 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋=0\right)\to \underset{_}{\pi }\left(⌊{A}⌋\right)=\underset{_}{\pi }\left({A}\right)$
60 simpr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋=0\right)\to ⌊{A}⌋=0$
61 60 fveq2d ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋=0\right)\to \underset{_}{\pi }\left(⌊{A}⌋\right)=\underset{_}{\pi }\left(0\right)$
62 2pos ${⊢}0<2$
63 0re ${⊢}0\in ℝ$
64 ppieq0 ${⊢}0\in ℝ\to \left(\underset{_}{\pi }\left(0\right)=0↔0<2\right)$
65 63 64 ax-mp ${⊢}\underset{_}{\pi }\left(0\right)=0↔0<2$
66 62 65 mpbir ${⊢}\underset{_}{\pi }\left(0\right)=0$
67 61 66 syl6eq ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋=0\right)\to \underset{_}{\pi }\left(⌊{A}⌋\right)=0$
68 59 67 eqtr3d ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋=0\right)\to \underset{_}{\pi }\left({A}\right)=0$
69 rpgt0 ${⊢}{A}\in {ℝ}^{+}\to 0<{A}$
70 69 adantr ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋=0\right)\to 0<{A}$
71 68 70 eqbrtrd ${⊢}\left({A}\in {ℝ}^{+}\wedge ⌊{A}⌋=0\right)\to \underset{_}{\pi }\left({A}\right)<{A}$
72 elnn0 ${⊢}⌊{A}⌋\in {ℕ}_{0}↔\left(⌊{A}⌋\in ℕ\vee ⌊{A}⌋=0\right)$
73 51 72 sylib ${⊢}{A}\in {ℝ}^{+}\to \left(⌊{A}⌋\in ℕ\vee ⌊{A}⌋=0\right)$
74 58 71 73 mpjaodan ${⊢}{A}\in {ℝ}^{+}\to \underset{_}{\pi }\left({A}\right)<{A}$