Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ppiltx Structured version   Visualization version   GIF version

Theorem ppiltx 24948
 Description: The prime-counting function π is strictly less than the identity. (Contributed by Mario Carneiro, 22-Sep-2014.)
Assertion
Ref Expression
ppiltx (𝐴 ∈ ℝ+ → (π𝐴) < 𝐴)

Proof of Theorem ppiltx
StepHypRef Expression
1 rpre 11877 . . . . . 6 (𝐴 ∈ ℝ+𝐴 ∈ ℝ)
2 ppicl 24902 . . . . . 6 (𝐴 ∈ ℝ → (π𝐴) ∈ ℕ0)
31, 2syl 17 . . . . 5 (𝐴 ∈ ℝ+ → (π𝐴) ∈ ℕ0)
43nn0red 11390 . . . 4 (𝐴 ∈ ℝ+ → (π𝐴) ∈ ℝ)
54adantr 480 . . 3 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (π𝐴) ∈ ℝ)
6 reflcl 12637 . . . . 5 (𝐴 ∈ ℝ → (⌊‘𝐴) ∈ ℝ)
71, 6syl 17 . . . 4 (𝐴 ∈ ℝ+ → (⌊‘𝐴) ∈ ℝ)
87adantr 480 . . 3 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (⌊‘𝐴) ∈ ℝ)
91adantr 480 . . 3 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → 𝐴 ∈ ℝ)
10 fzfi 12811 . . . . . 6 (1...(⌊‘𝐴)) ∈ Fin
11 inss1 3866 . . . . . . 7 ((2...(⌊‘𝐴)) ∩ ℙ) ⊆ (2...(⌊‘𝐴))
12 2eluzge1 11772 . . . . . . . . 9 2 ∈ (ℤ‘1)
13 fzss1 12418 . . . . . . . . 9 (2 ∈ (ℤ‘1) → (2...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴)))
1412, 13mp1i 13 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (2...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴)))
15 simpr 476 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (⌊‘𝐴) ∈ ℕ)
16 nnuz 11761 . . . . . . . . . . . 12 ℕ = (ℤ‘1)
1715, 16syl6eleq 2740 . . . . . . . . . . 11 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (⌊‘𝐴) ∈ (ℤ‘1))
18 eluzfz1 12386 . . . . . . . . . . 11 ((⌊‘𝐴) ∈ (ℤ‘1) → 1 ∈ (1...(⌊‘𝐴)))
1917, 18syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → 1 ∈ (1...(⌊‘𝐴)))
20 1lt2 11232 . . . . . . . . . . . 12 1 < 2
21 1re 10077 . . . . . . . . . . . . 13 1 ∈ ℝ
22 2re 11128 . . . . . . . . . . . . 13 2 ∈ ℝ
2321, 22ltnlei 10196 . . . . . . . . . . . 12 (1 < 2 ↔ ¬ 2 ≤ 1)
2420, 23mpbi 220 . . . . . . . . . . 11 ¬ 2 ≤ 1
25 elfzle1 12382 . . . . . . . . . . 11 (1 ∈ (2...(⌊‘𝐴)) → 2 ≤ 1)
2624, 25mto 188 . . . . . . . . . 10 ¬ 1 ∈ (2...(⌊‘𝐴))
27 nelne1 2919 . . . . . . . . . 10 ((1 ∈ (1...(⌊‘𝐴)) ∧ ¬ 1 ∈ (2...(⌊‘𝐴))) → (1...(⌊‘𝐴)) ≠ (2...(⌊‘𝐴)))
2819, 26, 27sylancl 695 . . . . . . . . 9 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (1...(⌊‘𝐴)) ≠ (2...(⌊‘𝐴)))
2928necomd 2878 . . . . . . . 8 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (2...(⌊‘𝐴)) ≠ (1...(⌊‘𝐴)))
30 df-pss 3623 . . . . . . . 8 ((2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴)) ↔ ((2...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴)) ∧ (2...(⌊‘𝐴)) ≠ (1...(⌊‘𝐴))))
3114, 29, 30sylanbrc 699 . . . . . . 7 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴)))
32 sspsstr 3745 . . . . . . 7 ((((2...(⌊‘𝐴)) ∩ ℙ) ⊆ (2...(⌊‘𝐴)) ∧ (2...(⌊‘𝐴)) ⊊ (1...(⌊‘𝐴))) → ((2...(⌊‘𝐴)) ∩ ℙ) ⊊ (1...(⌊‘𝐴)))
3311, 31, 32sylancr 696 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → ((2...(⌊‘𝐴)) ∩ ℙ) ⊊ (1...(⌊‘𝐴)))
34 php3 8187 . . . . . 6 (((1...(⌊‘𝐴)) ∈ Fin ∧ ((2...(⌊‘𝐴)) ∩ ℙ) ⊊ (1...(⌊‘𝐴))) → ((2...(⌊‘𝐴)) ∩ ℙ) ≺ (1...(⌊‘𝐴)))
3510, 33, 34sylancr 696 . . . . 5 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → ((2...(⌊‘𝐴)) ∩ ℙ) ≺ (1...(⌊‘𝐴)))
36 fzfi 12811 . . . . . . 7 (2...(⌊‘𝐴)) ∈ Fin
37 ssfi 8221 . . . . . . 7 (((2...(⌊‘𝐴)) ∈ Fin ∧ ((2...(⌊‘𝐴)) ∩ ℙ) ⊆ (2...(⌊‘𝐴))) → ((2...(⌊‘𝐴)) ∩ ℙ) ∈ Fin)
3836, 11, 37mp2an 708 . . . . . 6 ((2...(⌊‘𝐴)) ∩ ℙ) ∈ Fin
39 hashsdom 13208 . . . . . 6 ((((2...(⌊‘𝐴)) ∩ ℙ) ∈ Fin ∧ (1...(⌊‘𝐴)) ∈ Fin) → ((#‘((2...(⌊‘𝐴)) ∩ ℙ)) < (#‘(1...(⌊‘𝐴))) ↔ ((2...(⌊‘𝐴)) ∩ ℙ) ≺ (1...(⌊‘𝐴))))
4038, 10, 39mp2an 708 . . . . 5 ((#‘((2...(⌊‘𝐴)) ∩ ℙ)) < (#‘(1...(⌊‘𝐴))) ↔ ((2...(⌊‘𝐴)) ∩ ℙ) ≺ (1...(⌊‘𝐴)))
4135, 40sylibr 224 . . . 4 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (#‘((2...(⌊‘𝐴)) ∩ ℙ)) < (#‘(1...(⌊‘𝐴))))
421flcld 12639 . . . . . . 7 (𝐴 ∈ ℝ+ → (⌊‘𝐴) ∈ ℤ)
43 ppival2 24899 . . . . . . 7 ((⌊‘𝐴) ∈ ℤ → (π‘(⌊‘𝐴)) = (#‘((2...(⌊‘𝐴)) ∩ ℙ)))
4442, 43syl 17 . . . . . 6 (𝐴 ∈ ℝ+ → (π‘(⌊‘𝐴)) = (#‘((2...(⌊‘𝐴)) ∩ ℙ)))
45 ppifl 24931 . . . . . . 7 (𝐴 ∈ ℝ → (π‘(⌊‘𝐴)) = (π𝐴))
461, 45syl 17 . . . . . 6 (𝐴 ∈ ℝ+ → (π‘(⌊‘𝐴)) = (π𝐴))
4744, 46eqtr3d 2687 . . . . 5 (𝐴 ∈ ℝ+ → (#‘((2...(⌊‘𝐴)) ∩ ℙ)) = (π𝐴))
4847adantr 480 . . . 4 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (#‘((2...(⌊‘𝐴)) ∩ ℙ)) = (π𝐴))
49 rpge0 11883 . . . . . . 7 (𝐴 ∈ ℝ+ → 0 ≤ 𝐴)
50 flge0nn0 12661 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) → (⌊‘𝐴) ∈ ℕ0)
511, 49, 50syl2anc 694 . . . . . 6 (𝐴 ∈ ℝ+ → (⌊‘𝐴) ∈ ℕ0)
52 hashfz1 13174 . . . . . 6 ((⌊‘𝐴) ∈ ℕ0 → (#‘(1...(⌊‘𝐴))) = (⌊‘𝐴))
5351, 52syl 17 . . . . 5 (𝐴 ∈ ℝ+ → (#‘(1...(⌊‘𝐴))) = (⌊‘𝐴))
5453adantr 480 . . . 4 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (#‘(1...(⌊‘𝐴))) = (⌊‘𝐴))
5541, 48, 543brtr3d 4716 . . 3 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (π𝐴) < (⌊‘𝐴))
56 flle 12640 . . . 4 (𝐴 ∈ ℝ → (⌊‘𝐴) ≤ 𝐴)
579, 56syl 17 . . 3 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (⌊‘𝐴) ≤ 𝐴)
585, 8, 9, 55, 57ltletrd 10235 . 2 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) ∈ ℕ) → (π𝐴) < 𝐴)
5946adantr 480 . . . 4 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) = 0) → (π‘(⌊‘𝐴)) = (π𝐴))
60 simpr 476 . . . . . 6 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) = 0) → (⌊‘𝐴) = 0)
6160fveq2d 6233 . . . . 5 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) = 0) → (π‘(⌊‘𝐴)) = (π‘0))
62 2pos 11150 . . . . . 6 0 < 2
63 0re 10078 . . . . . . 7 0 ∈ ℝ
64 ppieq0 24947 . . . . . . 7 (0 ∈ ℝ → ((π‘0) = 0 ↔ 0 < 2))
6563, 64ax-mp 5 . . . . . 6 ((π‘0) = 0 ↔ 0 < 2)
6662, 65mpbir 221 . . . . 5 (π‘0) = 0
6761, 66syl6eq 2701 . . . 4 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) = 0) → (π‘(⌊‘𝐴)) = 0)
6859, 67eqtr3d 2687 . . 3 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) = 0) → (π𝐴) = 0)
69 rpgt0 11882 . . . 4 (𝐴 ∈ ℝ+ → 0 < 𝐴)
7069adantr 480 . . 3 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) = 0) → 0 < 𝐴)
7168, 70eqbrtrd 4707 . 2 ((𝐴 ∈ ℝ+ ∧ (⌊‘𝐴) = 0) → (π𝐴) < 𝐴)
72 elnn0 11332 . . 3 ((⌊‘𝐴) ∈ ℕ0 ↔ ((⌊‘𝐴) ∈ ℕ ∨ (⌊‘𝐴) = 0))
7351, 72sylib 208 . 2 (𝐴 ∈ ℝ+ → ((⌊‘𝐴) ∈ ℕ ∨ (⌊‘𝐴) = 0))
7458, 71, 73mpjaodan 844 1 (𝐴 ∈ ℝ+ → (π𝐴) < 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   = wceq 1523   ∈ wcel 2030   ≠ wne 2823   ∩ cin 3606   ⊆ wss 3607   ⊊ wpss 3608   class class class wbr 4685  ‘cfv 5926  (class class class)co 6690   ≺ csdm 7996  Fincfn 7997  ℝcr 9973  0cc0 9974  1c1 9975   < clt 10112   ≤ cle 10113  ℕcn 11058  2c2 11108  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ℝ+crp 11870  ...cfz 12364  ⌊cfl 12631  #chash 13157  ℙcprime 15432  πcppi 24865 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-rp 11871  df-icc 12220  df-fz 12365  df-fl 12633  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-dvds 15028  df-prm 15433  df-ppi 24871 This theorem is referenced by:  chtppilimlem1  25207
 Copyright terms: Public domain W3C validator