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 {\mathbb{N}}_0$$
3	1 2	syl	$$⊢A\in {ℝ}^{+}\to \underset{\_}{\pi }\left(A\right)\in {\mathbb{N}}_0$$
4	3	nn0red	$$⊢A\in {ℝ}^{+}\to \underset{\_}{\pi }\left(A\right)\in ℝ$$
5	4	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\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 \mathbb{N}\right)\to ⌊A⌋\in ℝ$$
9	1	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\right)\to A\in ℝ$$
10		fzfi	$$⊢\left(1\dots ⌊A⌋\right)\in \mathrm{Fin}$$
11		inss1	$$⊢\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\subseteq \left(2\dots ⌊A⌋\right)$$
12		2eluzge1	$$⊢2\in {\mathbb{Z}}_{\ge 1}$$
13		fzss1	$$⊢2\in {\mathbb{Z}}_{\ge 1}\to \left(2\dots ⌊A⌋\right)\subseteq \left(1\dots ⌊A⌋\right)$$
14	12 13	mp1i	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\right)\to \left(2\dots ⌊A⌋\right)\subseteq \left(1\dots ⌊A⌋\right)$$
15		simpr	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\right)\to ⌊A⌋\in \mathbb{N}$$
16		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
17	15 16	eleqtrdi	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\right)\to ⌊A⌋\in {\mathbb{Z}}_{\ge 1}$$
18		eluzfz1	$$⊢⌊A⌋\in {\mathbb{Z}}_{\ge 1}\to 1\in \left(1\dots ⌊A⌋\right)$$
19	17 18	syl	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\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\leftrightarrow \neg 2\le 1$$
24	20 23	mpbi	$$⊢\neg 2\le 1$$
25		elfzle1	$$⊢1\in \left(2\dots ⌊A⌋\right)\to 2\le 1$$
26	24 25	mto	$$⊢\neg 1\in \left(2\dots ⌊A⌋\right)$$
27		nelne1	$$⊢\left(1\in \left(1\dots ⌊A⌋\right)\wedge \neg 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 \mathbb{N}\right)\to \left(1\dots ⌊A⌋\right)\ne \left(2\dots ⌊A⌋\right)$$
29	28	necomd	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\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)\leftrightarrow \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 \mathbb{N}\right)\to \left(2\dots ⌊A⌋\right)\subset \left(1\dots ⌊A⌋\right)$$
32		sspsstr	$$⊢\left(\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\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 \mathbb{P}\subset \left(1\dots ⌊A⌋\right)$$
33	11 31 32	sylancr	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\right)\to \left(2\dots ⌊A⌋\right)\cap \mathbb{P}\subset \left(1\dots ⌊A⌋\right)$$
34		php3	$$⊢\left(\left(1\dots ⌊A⌋\right)\in \mathrm{Fin}\wedge \left(2\dots ⌊A⌋\right)\cap \mathbb{P}\subset \left(1\dots ⌊A⌋\right)\right)\to \left(\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right)\prec \left(1\dots ⌊A⌋\right)$$
35	10 33 34	sylancr	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\right)\to \left(\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\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 \mathbb{P}\subseteq \left(2\dots ⌊A⌋\right)\right)\to \left(2\dots ⌊A⌋\right)\cap \mathbb{P}\in \mathrm{Fin}$$
38	36 11 37	mp2an	$$⊢\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\in \mathrm{Fin}$$
39		hashsdom	$$⊢\left(\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\in \mathrm{Fin}\wedge \left(1\dots ⌊A⌋\right)\in \mathrm{Fin}\right)\to \left(\left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right|<\left|\left(1\dots ⌊A⌋\right)\right|\leftrightarrow \left(\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right)\prec \left(1\dots ⌊A⌋\right)\right)$$
40	38 10 39	mp2an	$$⊢\left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right|<\left|\left(1\dots ⌊A⌋\right)\right|\leftrightarrow \left(\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right)\prec \left(1\dots ⌊A⌋\right)$$
41	35 40	sylibr	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\right)\to \left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right|<\left|\left(1\dots ⌊A⌋\right)\right|$$
42	1	flcld	$$⊢A\in {ℝ}^{+}\to ⌊A⌋\in \mathbb{Z}$$
43		ppival2	$$⊢⌊A⌋\in \mathbb{Z}\to \underset{\_}{\pi }\left(⌊A⌋\right)=\left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\right|$$
44	42 43	syl	$$⊢A\in {ℝ}^{+}\to \underset{\_}{\pi }\left(⌊A⌋\right)=\left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\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 \mathbb{P}\right|=\underset{\_}{\pi }\left(A\right)$$
48	47	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\right)\to \left|\left(2\dots ⌊A⌋\right)\cap \mathbb{P}\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 {\mathbb{N}}_0$$
51	1 49 50	syl2anc	$$⊢A\in {ℝ}^{+}\to ⌊A⌋\in {\mathbb{N}}_0$$
52		hashfz1	$$⊢⌊A⌋\in {\mathbb{N}}_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 \mathbb{N}\right)\to \left|\left(1\dots ⌊A⌋\right)\right|=⌊A⌋$$
55	41 48 54	3brtr3d	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\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 \mathbb{N}\right)\to ⌊A⌋\le A$$
58	5 8 9 55 57	ltletrd	$$⊢\left(A\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{N}\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\leftrightarrow 0<2\right)$$
65	63 64	ax-mp	$$⊢\underset{\_}{\pi }\left(0\right)=0\leftrightarrow 0<2$$
66	62 65	mpbir	$$⊢\underset{\_}{\pi }\left(0\right)=0$$
67	61 66	eqtrdi	$$⊢\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 {\mathbb{N}}_0\leftrightarrow \left(⌊A⌋\in \mathbb{N}\vee ⌊A⌋=0\right)$$
73	51 72	sylib	$$⊢A\in {ℝ}^{+}\to \left(⌊A⌋\in \mathbb{N}\vee ⌊A⌋=0\right)$$
74	58 71 73	mpjaodan	$$⊢A\in {ℝ}^{+}\to \underset{\_}{\pi }\left(A\right)<A$$