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

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