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

Theorem pnt 27648
Description: The Prime Number Theorem: the number of prime numbers less than 𝑥 tends asymptotically to 𝑥 / log(𝑥) as 𝑥 goes to infinity. This is Metamath 100 proof #5. (Contributed by Mario Carneiro, 1-Jun-2016.)
Assertion
Ref Expression
pnt (𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ⇝𝑟 1

Proof of Theorem pnt
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1xr 11316 . . . . . 6 1 ∈ ℝ*
2 1lt2 12433 . . . . . 6 1 < 2
3 df-ioo 13387 . . . . . . 7 (,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧𝑧 < 𝑦)})
4 df-ico 13389 . . . . . . 7 [,) = (𝑥 ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥𝑧𝑧 < 𝑦)})
5 xrltletr 13195 . . . . . . 7 ((1 ∈ ℝ* ∧ 2 ∈ ℝ*𝑤 ∈ ℝ*) → ((1 < 2 ∧ 2 ≤ 𝑤) → 1 < 𝑤))
63, 4, 5ixxss1 13401 . . . . . 6 ((1 ∈ ℝ* ∧ 1 < 2) → (2[,)+∞) ⊆ (1(,)+∞))
71, 2, 6mp2an 692 . . . . 5 (2[,)+∞) ⊆ (1(,)+∞)
8 resmpt 6053 . . . . 5 ((2[,)+∞) ⊆ (1(,)+∞) → ((𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ↾ (2[,)+∞)) = (𝑥 ∈ (2[,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))))
97, 8mp1i 13 . . . 4 (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ↾ (2[,)+∞)) = (𝑥 ∈ (2[,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))))
107sseli 3978 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ (1(,)+∞))
11 ioossre 13444 . . . . . . . . . . 11 (1(,)+∞) ⊆ ℝ
1211sseli 3978 . . . . . . . . . 10 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ)
1310, 12syl 17 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ)
14 2re 12336 . . . . . . . . . . 11 2 ∈ ℝ
15 pnfxr 11311 . . . . . . . . . . 11 +∞ ∈ ℝ*
16 elico2 13447 . . . . . . . . . . 11 ((2 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥𝑥 < +∞)))
1714, 15, 16mp2an 692 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥𝑥 < +∞))
1817simp2bi 1147 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → 2 ≤ 𝑥)
19 chtrpcl 27208 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 2 ≤ 𝑥) → (θ‘𝑥) ∈ ℝ+)
2013, 18, 19syl2anc 584 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → (θ‘𝑥) ∈ ℝ+)
21 0red 11260 . . . . . . . . . . 11 (𝑥 ∈ (1(,)+∞) → 0 ∈ ℝ)
22 1red 11258 . . . . . . . . . . 11 (𝑥 ∈ (1(,)+∞) → 1 ∈ ℝ)
23 0lt1 11781 . . . . . . . . . . . 12 0 < 1
2423a1i 11 . . . . . . . . . . 11 (𝑥 ∈ (1(,)+∞) → 0 < 1)
25 eliooord 13442 . . . . . . . . . . . 12 (𝑥 ∈ (1(,)+∞) → (1 < 𝑥𝑥 < +∞))
2625simpld 494 . . . . . . . . . . 11 (𝑥 ∈ (1(,)+∞) → 1 < 𝑥)
2721, 22, 12, 24, 26lttrd 11418 . . . . . . . . . 10 (𝑥 ∈ (1(,)+∞) → 0 < 𝑥)
2812, 27elrpd 13070 . . . . . . . . 9 (𝑥 ∈ (1(,)+∞) → 𝑥 ∈ ℝ+)
2910, 28syl 17 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ+)
3020, 29rpdivcld 13090 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → ((θ‘𝑥) / 𝑥) ∈ ℝ+)
3130adantl 481 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (2[,)+∞)) → ((θ‘𝑥) / 𝑥) ∈ ℝ+)
32 ppinncl 27207 . . . . . . . . . . 11 ((𝑥 ∈ ℝ ∧ 2 ≤ 𝑥) → (π𝑥) ∈ ℕ)
3313, 18, 32syl2anc 584 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → (π𝑥) ∈ ℕ)
3433nnrpd 13071 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → (π𝑥) ∈ ℝ+)
3512, 26rplogcld 26661 . . . . . . . . . 10 (𝑥 ∈ (1(,)+∞) → (log‘𝑥) ∈ ℝ+)
3610, 35syl 17 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → (log‘𝑥) ∈ ℝ+)
3734, 36rpmulcld 13089 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → ((π𝑥) · (log‘𝑥)) ∈ ℝ+)
3820, 37rpdivcld 13090 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → ((θ‘𝑥) / ((π𝑥) · (log‘𝑥))) ∈ ℝ+)
3938adantl 481 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (2[,)+∞)) → ((θ‘𝑥) / ((π𝑥) · (log‘𝑥))) ∈ ℝ+)
4029ssriv 3986 . . . . . . . 8 (2[,)+∞) ⊆ ℝ+
41 resmpt 6053 . . . . . . . 8 ((2[,)+∞) ⊆ ℝ+ → ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) = (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)))
4240, 41ax-mp 5 . . . . . . 7 ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) = (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / 𝑥))
43 pnt2 27647 . . . . . . . 8 (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1
44 rlimres 15590 . . . . . . . 8 ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1 → ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) ⇝𝑟 1)
4543, 44mp1i 13 . . . . . . 7 (⊤ → ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) ⇝𝑟 1)
4642, 45eqbrtrrid 5177 . . . . . 6 (⊤ → (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1)
47 chtppilim 27509 . . . . . . 7 (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π𝑥) · (log‘𝑥)))) ⇝𝑟 1
4847a1i 11 . . . . . 6 (⊤ → (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π𝑥) · (log‘𝑥)))) ⇝𝑟 1)
49 ax-1ne0 11220 . . . . . . 7 1 ≠ 0
5049a1i 11 . . . . . 6 (⊤ → 1 ≠ 0)
5138rpne0d 13078 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → ((θ‘𝑥) / ((π𝑥) · (log‘𝑥))) ≠ 0)
5251adantl 481 . . . . . 6 ((⊤ ∧ 𝑥 ∈ (2[,)+∞)) → ((θ‘𝑥) / ((π𝑥) · (log‘𝑥))) ≠ 0)
5331, 39, 46, 48, 50, 52rlimdiv 15678 . . . . 5 (⊤ → (𝑥 ∈ (2[,)+∞) ↦ (((θ‘𝑥) / 𝑥) / ((θ‘𝑥) / ((π𝑥) · (log‘𝑥))))) ⇝𝑟 (1 / 1))
5413recnd 11285 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℂ)
55 chtcl 27142 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (θ‘𝑥) ∈ ℝ)
5612, 55syl 17 . . . . . . . . . . . 12 (𝑥 ∈ (1(,)+∞) → (θ‘𝑥) ∈ ℝ)
5756recnd 11285 . . . . . . . . . . 11 (𝑥 ∈ (1(,)+∞) → (θ‘𝑥) ∈ ℂ)
5810, 57syl 17 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → (θ‘𝑥) ∈ ℂ)
5954, 58mulcomd 11278 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → (𝑥 · (θ‘𝑥)) = ((θ‘𝑥) · 𝑥))
6059oveq2d 7445 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → (((θ‘𝑥) · ((π𝑥) · (log‘𝑥))) / (𝑥 · (θ‘𝑥))) = (((θ‘𝑥) · ((π𝑥) · (log‘𝑥))) / ((θ‘𝑥) · 𝑥)))
6137rpcnd 13075 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → ((π𝑥) · (log‘𝑥)) ∈ ℂ)
6229rpne0d 13078 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → 𝑥 ≠ 0)
6320rpne0d 13078 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → (θ‘𝑥) ≠ 0)
6461, 54, 58, 62, 63divcan5d 12065 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → (((θ‘𝑥) · ((π𝑥) · (log‘𝑥))) / ((θ‘𝑥) · 𝑥)) = (((π𝑥) · (log‘𝑥)) / 𝑥))
6560, 64eqtrd 2776 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → (((θ‘𝑥) · ((π𝑥) · (log‘𝑥))) / (𝑥 · (θ‘𝑥))) = (((π𝑥) · (log‘𝑥)) / 𝑥))
6637rpne0d 13078 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → ((π𝑥) · (log‘𝑥)) ≠ 0)
6758, 54, 58, 61, 62, 66, 63divdivdivd 12086 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → (((θ‘𝑥) / 𝑥) / ((θ‘𝑥) / ((π𝑥) · (log‘𝑥)))) = (((θ‘𝑥) · ((π𝑥) · (log‘𝑥))) / (𝑥 · (θ‘𝑥))))
6833nncnd 12278 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → (π𝑥) ∈ ℂ)
6936rpcnd 13075 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → (log‘𝑥) ∈ ℂ)
7036rpne0d 13078 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → (log‘𝑥) ≠ 0)
7168, 54, 69, 62, 70divdiv2d 12071 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → ((π𝑥) / (𝑥 / (log‘𝑥))) = (((π𝑥) · (log‘𝑥)) / 𝑥))
7265, 67, 713eqtr4d 2786 . . . . . 6 (𝑥 ∈ (2[,)+∞) → (((θ‘𝑥) / 𝑥) / ((θ‘𝑥) / ((π𝑥) · (log‘𝑥)))) = ((π𝑥) / (𝑥 / (log‘𝑥))))
7372mpteq2ia 5243 . . . . 5 (𝑥 ∈ (2[,)+∞) ↦ (((θ‘𝑥) / 𝑥) / ((θ‘𝑥) / ((π𝑥) · (log‘𝑥))))) = (𝑥 ∈ (2[,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥))))
74 1div1e1 11954 . . . . 5 (1 / 1) = 1
7553, 73, 743brtr3g 5174 . . . 4 (⊤ → (𝑥 ∈ (2[,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ⇝𝑟 1)
769, 75eqbrtrd 5163 . . 3 (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ↾ (2[,)+∞)) ⇝𝑟 1)
77 ppicl 27164 . . . . . . . . . 10 (𝑥 ∈ ℝ → (π𝑥) ∈ ℕ0)
7812, 77syl 17 . . . . . . . . 9 (𝑥 ∈ (1(,)+∞) → (π𝑥) ∈ ℕ0)
7978nn0red 12584 . . . . . . . 8 (𝑥 ∈ (1(,)+∞) → (π𝑥) ∈ ℝ)
8028, 35rpdivcld 13090 . . . . . . . 8 (𝑥 ∈ (1(,)+∞) → (𝑥 / (log‘𝑥)) ∈ ℝ+)
8179, 80rerpdivcld 13104 . . . . . . 7 (𝑥 ∈ (1(,)+∞) → ((π𝑥) / (𝑥 / (log‘𝑥))) ∈ ℝ)
8281recnd 11285 . . . . . 6 (𝑥 ∈ (1(,)+∞) → ((π𝑥) / (𝑥 / (log‘𝑥))) ∈ ℂ)
8382adantl 481 . . . . 5 ((⊤ ∧ 𝑥 ∈ (1(,)+∞)) → ((π𝑥) / (𝑥 / (log‘𝑥))) ∈ ℂ)
8483fmpttd 7133 . . . 4 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))):(1(,)+∞)⟶ℂ)
8511a1i 11 . . . 4 (⊤ → (1(,)+∞) ⊆ ℝ)
8614a1i 11 . . . 4 (⊤ → 2 ∈ ℝ)
8784, 85, 86rlimresb 15597 . . 3 (⊤ → ((𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ⇝𝑟 1 ↔ ((𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ↾ (2[,)+∞)) ⇝𝑟 1))
8876, 87mpbird 257 . 2 (⊤ → (𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ⇝𝑟 1)
8988mptru 1547 1 (𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ⇝𝑟 1
Colors of variables: wff setvar class
Syntax hints:  wb 206  w3a 1087   = wceq 1540  wtru 1541  wcel 2108  wne 2939  wss 3950   class class class wbr 5141  cmpt 5223  cres 5685  cfv 6559  (class class class)co 7429  cc 11149  cr 11150  0cc0 11151  1c1 11152   · cmul 11156  +∞cpnf 11288  *cxr 11290   < clt 11291  cle 11292   / cdiv 11916  cn 12262  2c2 12317  0cn0 12522  +crp 13030  (,)cioo 13383  [,)cico 13385  𝑟 crli 15517  logclog 26586  θccht 27124  πcppi 27127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751  ax-inf2 9677  ax-cnex 11207  ax-resscn 11208  ax-1cn 11209  ax-icn 11210  ax-addcl 11211  ax-addrcl 11212  ax-mulcl 11213  ax-mulrcl 11214  ax-mulcom 11215  ax-addass 11216  ax-mulass 11217  ax-distr 11218  ax-i2m1 11219  ax-1ne0 11220  ax-1rid 11221  ax-rnegex 11222  ax-rrecex 11223  ax-cnre 11224  ax-pre-lttri 11225  ax-pre-lttrn 11226  ax-pre-ltadd 11227  ax-pre-mulgt0 11228  ax-pre-sup 11229  ax-addf 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4906  df-int 4945  df-iun 4991  df-iin 4992  df-disj 5109  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-se 5636  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-isom 6568  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-of 7694  df-om 7884  df-1st 8010  df-2nd 8011  df-supp 8182  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-1o 8502  df-2o 8503  df-oadd 8506  df-er 8741  df-map 8864  df-pm 8865  df-ixp 8934  df-en 8982  df-dom 8983  df-sdom 8984  df-fin 8985  df-fsupp 9398  df-fi 9447  df-sup 9478  df-inf 9479  df-oi 9546  df-dju 9937  df-card 9975  df-pnf 11293  df-mnf 11294  df-xr 11295  df-ltxr 11296  df-le 11297  df-sub 11490  df-neg 11491  df-div 11917  df-nn 12263  df-2 12325  df-3 12326  df-4 12327  df-5 12328  df-6 12329  df-7 12330  df-8 12331  df-9 12332  df-n0 12523  df-xnn0 12596  df-z 12610  df-dec 12730  df-uz 12875  df-q 12987  df-rp 13031  df-xneg 13150  df-xadd 13151  df-xmul 13152  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-o1 15522  df-lo1 15523  df-sum 15719  df-ef 16099  df-e 16100  df-sin 16101  df-cos 16102  df-tan 16103  df-pi 16104  df-dvds 16287  df-gcd 16528  df-prm 16705  df-pc 16871  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17244  df-ress 17271  df-plusg 17306  df-mulr 17307  df-starv 17308  df-sca 17309  df-vsca 17310  df-ip 17311  df-tset 17312  df-ple 17313  df-ds 17315  df-unif 17316  df-hom 17317  df-cco 17318  df-rest 17463  df-topn 17464  df-0g 17482  df-gsum 17483  df-topgen 17484  df-pt 17485  df-prds 17488  df-xrs 17543  df-qtop 17548  df-imas 17549  df-xps 17551  df-mre 17625  df-mrc 17626  df-acs 17628  df-mgm 18649  df-sgrp 18728  df-mnd 18744  df-submnd 18793  df-mulg 19082  df-cntz 19331  df-cmn 19796  df-psmet 21348  df-xmet 21349  df-met 21350  df-bl 21351  df-mopn 21352  df-fbas 21353  df-fg 21354  df-cnfld 21357  df-top 22890  df-topon 22907  df-topsp 22929  df-bases 22943  df-cld 23017  df-ntr 23018  df-cls 23019  df-nei 23096  df-lp 23134  df-perf 23135  df-cn 23225  df-cnp 23226  df-haus 23313  df-cmp 23385  df-tx 23560  df-hmeo 23753  df-fil 23844  df-fm 23936  df-flim 23937  df-flf 23938  df-xms 24320  df-ms 24321  df-tms 24322  df-cncf 24894  df-limc 25891  df-dv 25892  df-ulm 26410  df-log 26588  df-cxp 26589  df-atan 26900  df-em 27026  df-cht 27130  df-vma 27131  df-chp 27132  df-ppi 27133  df-mu 27134
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator