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	⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ 𝐴 ) < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2		ppicl	⊢ ( 𝐴 ∈ ℝ → ( π ‘ 𝐴 ) ∈ ℕ0 )
3	1 2	syl	⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ 𝐴 ) ∈ ℕ0 )
4	3	nn0red	⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ 𝐴 ) ∈ ℝ )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( π ‘ 𝐴 ) ∈ ℝ )
6		reflcl	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
7	1 6	syl	⊢ ( 𝐴 ∈ ℝ+ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
8	7	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
9	1	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → 𝐴 ∈ ℝ )
10		fzfi	⊢ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin
11		inss1	⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) )
12		2eluzge1	⊢ 2 ∈ ( ℤ≥ ‘ 1 )
13		fzss1	⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
14	12 13	mp1i	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
15		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ )
16		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
17	15 16	eleqtrdi	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) )
18		eluzfz1	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
19	17 18	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
20		1lt2	⊢ 1 < 2
21		1re	⊢ 1 ∈ ℝ
22		2re	⊢ 2 ∈ ℝ
23	21 22	ltnlei	⊢ ( 1 < 2 ↔ ¬ 2 ≤ 1 )
24	20 23	mpbi	⊢ ¬ 2 ≤ 1
25		elfzle1	⊢ ( 1 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) → 2 ≤ 1 )
26	24 25	mto	⊢ ¬ 1 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) )
27		nelne1	⊢ ( ( 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ¬ 1 ∈ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ≠ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
28	19 26 27	sylancl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ≠ ( 2 ... ( ⌊ ‘ 𝐴 ) ) )
29	28	necomd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ≠ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
30		df-pss	⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ≠ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) )
31	14 29 30	sylanbrc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
32		sspsstr	⊢ ( ( ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
33	11 31 32	sylancr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
34		php3	⊢ ( ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊊ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ≺ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
35	10 33 34	sylancr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ≺ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
36		fzfi	⊢ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin
37		ssfi	⊢ ( ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin )
38	36 11 37	mp2an	⊢ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin
39		hashsdom	⊢ ( ( ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ∧ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ) → ( ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) < ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ↔ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ≺ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) )
40	38 10 39	mp2an	⊢ ( ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) < ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ↔ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ≺ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
41	35 40	sylibr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) < ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) )
42	1	flcld	⊢ ( 𝐴 ∈ ℝ+ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
43		ppival2	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) )
44	42 43	syl	⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) )
45		ppifl	⊢ ( 𝐴 ∈ ℝ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 𝐴 ) )
46	1 45	syl	⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 𝐴 ) )
47	44 46	eqtr3d	⊢ ( 𝐴 ∈ ℝ+ → ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) = ( π ‘ 𝐴 ) )
48	47	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( ( 2 ... ( ⌊ ‘ 𝐴 ) ) ∩ ℙ ) ) = ( π ‘ 𝐴 ) )
49		rpge0	⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 )
50		flge0nn0	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 )
51	1 49 50	syl2anc	⊢ ( 𝐴 ∈ ℝ+ → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 )
52		hashfz1	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ⌊ ‘ 𝐴 ) )
53	51 52	syl	⊢ ( 𝐴 ∈ ℝ+ → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ⌊ ‘ 𝐴 ) )
54	53	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) = ( ⌊ ‘ 𝐴 ) )
55	41 48 54	3brtr3d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( π ‘ 𝐴 ) < ( ⌊ ‘ 𝐴 ) )
56		flle	⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
57	9 56	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( ⌊ ‘ 𝐴 ) ≤ 𝐴 )
58	5 8 9 55 57	ltletrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) ∈ ℕ ) → ( π ‘ 𝐴 ) < 𝐴 )
59	46	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 𝐴 ) )
60		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( ⌊ ‘ 𝐴 ) = 0 )
61	60	fveq2d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = ( π ‘ 0 ) )
62		2pos	⊢ 0 < 2
63		0re	⊢ 0 ∈ ℝ
64		ppieq0	⊢ ( 0 ∈ ℝ → ( ( π ‘ 0 ) = 0 ↔ 0 < 2 ) )
65	63 64	ax-mp	⊢ ( ( π ‘ 0 ) = 0 ↔ 0 < 2 )
66	62 65	mpbir	⊢ ( π ‘ 0 ) = 0
67	61 66	eqtrdi	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ ( ⌊ ‘ 𝐴 ) ) = 0 )
68	59 67	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ 𝐴 ) = 0 )
69		rpgt0	⊢ ( 𝐴 ∈ ℝ+ → 0 < 𝐴 )
70	69	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → 0 < 𝐴 )
71	68 70	eqbrtrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( ⌊ ‘ 𝐴 ) = 0 ) → ( π ‘ 𝐴 ) < 𝐴 )
72		elnn0	⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ ∨ ( ⌊ ‘ 𝐴 ) = 0 ) )
73	51 72	sylib	⊢ ( 𝐴 ∈ ℝ+ → ( ( ⌊ ‘ 𝐴 ) ∈ ℕ ∨ ( ⌊ ‘ 𝐴 ) = 0 ) )
74	58 71 73	mpjaodan	⊢ ( 𝐴 ∈ ℝ+ → ( π ‘ 𝐴 ) < 𝐴 )