![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pnt2 | Structured version Visualization version GIF version |
Description: The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.) |
Ref | Expression |
---|---|
pnt2 | ⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2re 11699 | . . . . . . . . 9 ⊢ 2 ∈ ℝ | |
2 | elicopnf 12823 | . . . . . . . . 9 ⊢ (2 ∈ ℝ → (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥))) | |
3 | 1, 2 | ax-mp 5 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥)) |
4 | chprpcl 25791 | . . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ∧ 2 ≤ 𝑥) → (ψ‘𝑥) ∈ ℝ+) | |
5 | 3, 4 | sylbi 220 | . . . . . . 7 ⊢ (𝑥 ∈ (2[,)+∞) → (ψ‘𝑥) ∈ ℝ+) |
6 | 3 | simplbi 501 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ) |
7 | 0red 10633 | . . . . . . . . 9 ⊢ (𝑥 ∈ (2[,)+∞) → 0 ∈ ℝ) | |
8 | 1 | a1i 11 | . . . . . . . . 9 ⊢ (𝑥 ∈ (2[,)+∞) → 2 ∈ ℝ) |
9 | 2pos 11728 | . . . . . . . . . 10 ⊢ 0 < 2 | |
10 | 9 | a1i 11 | . . . . . . . . 9 ⊢ (𝑥 ∈ (2[,)+∞) → 0 < 2) |
11 | 3 | simprbi 500 | . . . . . . . . 9 ⊢ (𝑥 ∈ (2[,)+∞) → 2 ≤ 𝑥) |
12 | 7, 8, 6, 10, 11 | ltletrd 10789 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) → 0 < 𝑥) |
13 | 6, 12 | elrpd 12416 | . . . . . . 7 ⊢ (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ+) |
14 | 5, 13 | rpdivcld 12436 | . . . . . 6 ⊢ (𝑥 ∈ (2[,)+∞) → ((ψ‘𝑥) / 𝑥) ∈ ℝ+) |
15 | 14 | adantl 485 | . . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (2[,)+∞)) → ((ψ‘𝑥) / 𝑥) ∈ ℝ+) |
16 | chtrpcl 25760 | . . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ∧ 2 ≤ 𝑥) → (θ‘𝑥) ∈ ℝ+) | |
17 | 3, 16 | sylbi 220 | . . . . . . 7 ⊢ (𝑥 ∈ (2[,)+∞) → (θ‘𝑥) ∈ ℝ+) |
18 | 5, 17 | rpdivcld 12436 | . . . . . 6 ⊢ (𝑥 ∈ (2[,)+∞) → ((ψ‘𝑥) / (θ‘𝑥)) ∈ ℝ+) |
19 | 18 | adantl 485 | . . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (2[,)+∞)) → ((ψ‘𝑥) / (θ‘𝑥)) ∈ ℝ+) |
20 | 13 | ssriv 3919 | . . . . . . 7 ⊢ (2[,)+∞) ⊆ ℝ+ |
21 | 20 | a1i 11 | . . . . . 6 ⊢ (⊤ → (2[,)+∞) ⊆ ℝ+) |
22 | pnt3 26196 | . . . . . . 7 ⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1 | |
23 | 22 | a1i 11 | . . . . . 6 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1) |
24 | 21, 23 | rlimres2 14910 | . . . . 5 ⊢ (⊤ → (𝑥 ∈ (2[,)+∞) ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1) |
25 | chpchtlim 26063 | . . . . . 6 ⊢ (𝑥 ∈ (2[,)+∞) ↦ ((ψ‘𝑥) / (θ‘𝑥))) ⇝𝑟 1 | |
26 | 25 | a1i 11 | . . . . 5 ⊢ (⊤ → (𝑥 ∈ (2[,)+∞) ↦ ((ψ‘𝑥) / (θ‘𝑥))) ⇝𝑟 1) |
27 | ax-1ne0 10595 | . . . . . 6 ⊢ 1 ≠ 0 | |
28 | 27 | a1i 11 | . . . . 5 ⊢ (⊤ → 1 ≠ 0) |
29 | 19 | rpne0d 12424 | . . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (2[,)+∞)) → ((ψ‘𝑥) / (θ‘𝑥)) ≠ 0) |
30 | 15, 19, 24, 26, 28, 29 | rlimdiv 14994 | . . . 4 ⊢ (⊤ → (𝑥 ∈ (2[,)+∞) ↦ (((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥)))) ⇝𝑟 (1 / 1)) |
31 | rpre 12385 | . . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ) | |
32 | chpcl 25709 | . . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (ψ‘𝑥) ∈ ℝ) | |
33 | 31, 32 | syl 17 | . . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (ψ‘𝑥) ∈ ℝ) |
34 | 33 | recnd 10658 | . . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → (ψ‘𝑥) ∈ ℂ) |
35 | 13, 34 | syl 17 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) → (ψ‘𝑥) ∈ ℂ) |
36 | 13 | rpcnne0d 12428 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
37 | 5 | rpcnne0d 12428 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) → ((ψ‘𝑥) ∈ ℂ ∧ (ψ‘𝑥) ≠ 0)) |
38 | 17 | rpcnne0d 12428 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) → ((θ‘𝑥) ∈ ℂ ∧ (θ‘𝑥) ≠ 0)) |
39 | divdivdiv 11330 | . . . . . . . 8 ⊢ ((((ψ‘𝑥) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) ∧ (((ψ‘𝑥) ∈ ℂ ∧ (ψ‘𝑥) ≠ 0) ∧ ((θ‘𝑥) ∈ ℂ ∧ (θ‘𝑥) ≠ 0))) → (((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥))) = (((ψ‘𝑥) · (θ‘𝑥)) / (𝑥 · (ψ‘𝑥)))) | |
40 | 35, 36, 37, 38, 39 | syl22anc 837 | . . . . . . 7 ⊢ (𝑥 ∈ (2[,)+∞) → (((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥))) = (((ψ‘𝑥) · (θ‘𝑥)) / (𝑥 · (ψ‘𝑥)))) |
41 | 6 | recnd 10658 | . . . . . . . . 9 ⊢ (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℂ) |
42 | 41, 35 | mulcomd 10651 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) → (𝑥 · (ψ‘𝑥)) = ((ψ‘𝑥) · 𝑥)) |
43 | 42 | oveq2d 7151 | . . . . . . 7 ⊢ (𝑥 ∈ (2[,)+∞) → (((ψ‘𝑥) · (θ‘𝑥)) / (𝑥 · (ψ‘𝑥))) = (((ψ‘𝑥) · (θ‘𝑥)) / ((ψ‘𝑥) · 𝑥))) |
44 | chtcl 25694 | . . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → (θ‘𝑥) ∈ ℝ) | |
45 | 31, 44 | syl 17 | . . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ+ → (θ‘𝑥) ∈ ℝ) |
46 | 45 | recnd 10658 | . . . . . . . . 9 ⊢ (𝑥 ∈ ℝ+ → (θ‘𝑥) ∈ ℂ) |
47 | 13, 46 | syl 17 | . . . . . . . 8 ⊢ (𝑥 ∈ (2[,)+∞) → (θ‘𝑥) ∈ ℂ) |
48 | divcan5 11331 | . . . . . . . 8 ⊢ (((θ‘𝑥) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ ((ψ‘𝑥) ∈ ℂ ∧ (ψ‘𝑥) ≠ 0)) → (((ψ‘𝑥) · (θ‘𝑥)) / ((ψ‘𝑥) · 𝑥)) = ((θ‘𝑥) / 𝑥)) | |
49 | 47, 36, 37, 48 | syl3anc 1368 | . . . . . . 7 ⊢ (𝑥 ∈ (2[,)+∞) → (((ψ‘𝑥) · (θ‘𝑥)) / ((ψ‘𝑥) · 𝑥)) = ((θ‘𝑥) / 𝑥)) |
50 | 40, 43, 49 | 3eqtrd 2837 | . . . . . 6 ⊢ (𝑥 ∈ (2[,)+∞) → (((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥))) = ((θ‘𝑥) / 𝑥)) |
51 | 50 | mpteq2ia 5121 | . . . . 5 ⊢ (𝑥 ∈ (2[,)+∞) ↦ (((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥)))) = (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) |
52 | resmpt 5872 | . . . . . 6 ⊢ ((2[,)+∞) ⊆ ℝ+ → ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) = (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / 𝑥))) | |
53 | 20, 52 | ax-mp 5 | . . . . 5 ⊢ ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) = (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) |
54 | 51, 53 | eqtr4i 2824 | . . . 4 ⊢ (𝑥 ∈ (2[,)+∞) ↦ (((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥)))) = ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) |
55 | 1div1e1 11319 | . . . 4 ⊢ (1 / 1) = 1 | |
56 | 30, 54, 55 | 3brtr3g 5063 | . . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) ⇝𝑟 1) |
57 | rerpdivcl 12407 | . . . . . . . 8 ⊢ (((θ‘𝑥) ∈ ℝ ∧ 𝑥 ∈ ℝ+) → ((θ‘𝑥) / 𝑥) ∈ ℝ) | |
58 | 45, 57 | mpancom 687 | . . . . . . 7 ⊢ (𝑥 ∈ ℝ+ → ((θ‘𝑥) / 𝑥) ∈ ℝ) |
59 | 58 | adantl 485 | . . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → ((θ‘𝑥) / 𝑥) ∈ ℝ) |
60 | 59 | recnd 10658 | . . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ ℝ+) → ((θ‘𝑥) / 𝑥) ∈ ℂ) |
61 | 60 | fmpttd 6856 | . . . 4 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)):ℝ+⟶ℂ) |
62 | rpssre 12384 | . . . . 5 ⊢ ℝ+ ⊆ ℝ | |
63 | 62 | a1i 11 | . . . 4 ⊢ (⊤ → ℝ+ ⊆ ℝ) |
64 | 1 | a1i 11 | . . . 4 ⊢ (⊤ → 2 ∈ ℝ) |
65 | 61, 63, 64 | rlimresb 14914 | . . 3 ⊢ (⊤ → ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1 ↔ ((𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) ⇝𝑟 1)) |
66 | 56, 65 | mpbird 260 | . 2 ⊢ (⊤ → (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1) |
67 | 66 | mptru 1545 | 1 ⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1 |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 = wceq 1538 ⊤wtru 1539 ∈ wcel 2111 ≠ wne 2987 ⊆ wss 3881 class class class wbr 5030 ↦ cmpt 5110 ↾ cres 5521 ‘cfv 6324 (class class class)co 7135 ℂcc 10524 ℝcr 10525 0cc0 10526 1c1 10527 · cmul 10531 +∞cpnf 10661 < clt 10664 ≤ cle 10665 / cdiv 11286 2c2 11680 ℝ+crp 12377 [,)cico 12728 ⇝𝑟 crli 14834 θccht 25676 ψcchp 25678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-inf2 9088 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-icn 10585 ax-addcl 10586 ax-addrcl 10587 ax-mulcl 10588 ax-mulrcl 10589 ax-mulcom 10590 ax-addass 10591 ax-mulass 10592 ax-distr 10593 ax-i2m1 10594 ax-1ne0 10595 ax-1rid 10596 ax-rnegex 10597 ax-rrecex 10598 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 ax-pre-ltadd 10602 ax-pre-mulgt0 10603 ax-pre-sup 10604 ax-addf 10605 ax-mulf 10606 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-reu 3113 df-rmo 3114 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-int 4839 df-iun 4883 df-iin 4884 df-disj 4996 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5425 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-se 5479 df-we 5480 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-pred 6116 df-ord 6162 df-on 6163 df-lim 6164 df-suc 6165 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-isom 6333 df-riota 7093 df-ov 7138 df-oprab 7139 df-mpo 7140 df-of 7389 df-om 7561 df-1st 7671 df-2nd 7672 df-supp 7814 df-wrecs 7930 df-recs 7991 df-rdg 8029 df-1o 8085 df-2o 8086 df-oadd 8089 df-er 8272 df-map 8391 df-pm 8392 df-ixp 8445 df-en 8493 df-dom 8494 df-sdom 8495 df-fin 8496 df-fsupp 8818 df-fi 8859 df-sup 8890 df-inf 8891 df-oi 8958 df-dju 9314 df-card 9352 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-sub 10861 df-neg 10862 df-div 11287 df-nn 11626 df-2 11688 df-3 11689 df-4 11690 df-5 11691 df-6 11692 df-7 11693 df-8 11694 df-9 11695 df-n0 11886 df-xnn0 11956 df-z 11970 df-dec 12087 df-uz 12232 df-q 12337 df-rp 12378 df-xneg 12495 df-xadd 12496 df-xmul 12497 df-ioo 12730 df-ioc 12731 df-ico 12732 df-icc 12733 df-fz 12886 df-fzo 13029 df-fl 13157 df-mod 13233 df-seq 13365 df-exp 13426 df-fac 13630 df-bc 13659 df-hash 13687 df-shft 14418 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-limsup 14820 df-clim 14837 df-rlim 14838 df-o1 14839 df-lo1 14840 df-sum 15035 df-ef 15413 df-e 15414 df-sin 15415 df-cos 15416 df-tan 15417 df-pi 15418 df-dvds 15600 df-gcd 15834 df-prm 16006 df-pc 16164 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-mulr 16571 df-starv 16572 df-sca 16573 df-vsca 16574 df-ip 16575 df-tset 16576 df-ple 16577 df-ds 16579 df-unif 16580 df-hom 16581 df-cco 16582 df-rest 16688 df-topn 16689 df-0g 16707 df-gsum 16708 df-topgen 16709 df-pt 16710 df-prds 16713 df-xrs 16767 df-qtop 16772 df-imas 16773 df-xps 16775 df-mre 16849 df-mrc 16850 df-acs 16852 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-submnd 17949 df-mulg 18217 df-cntz 18439 df-cmn 18900 df-psmet 20083 df-xmet 20084 df-met 20085 df-bl 20086 df-mopn 20087 df-fbas 20088 df-fg 20089 df-cnfld 20092 df-top 21499 df-topon 21516 df-topsp 21538 df-bases 21551 df-cld 21624 df-ntr 21625 df-cls 21626 df-nei 21703 df-lp 21741 df-perf 21742 df-cn 21832 df-cnp 21833 df-haus 21920 df-cmp 21992 df-tx 22167 df-hmeo 22360 df-fil 22451 df-fm 22543 df-flim 22544 df-flf 22545 df-xms 22927 df-ms 22928 df-tms 22929 df-cncf 23483 df-limc 24469 df-dv 24470 df-ulm 24972 df-log 25148 df-cxp 25149 df-atan 25453 df-em 25578 df-cht 25682 df-vma 25683 df-chp 25684 df-ppi 25685 df-mu 25686 |
This theorem is referenced by: pnt 26198 |
Copyright terms: Public domain | W3C validator |