Metamath Proof Explorer

Theorem pnt

Description: The Prime Number Theorem: the number of prime numbers less than x tends asymptotically to x / log ( x ) as x goes to infinity. This is Metamath 100 proof #5. (Contributed by Mario Carneiro, 1-Jun-2016)

Ref Expression
Assertion pnt ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1

Proof

Step Hyp Ref Expression
1 1xr ⊢ 1 ∈ ℝ*
2 1lt2 ⊢ 1 < 2
3 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
4 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦 ) } )
5 xrltletr ⊢ ( ( 1 ∈ ℝ* ∧ 2 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 1 < 2 ∧ 2 ≤ 𝑤 ) → 1 < 𝑤 ) )
6 3 4 5 ixxss1 ⊢ ( ( 1 ∈ ℝ* ∧ 1 < 2 ) → ( 2 [,) +∞ ) ⊆ ( 1 (,) +∞ ) )
7 1 2 6 mp2an ⊢ ( 2 [,) +∞ ) ⊆ ( 1 (,) +∞ )
8 resmpt ⊢ ( ( 2 [,) +∞ ) ⊆ ( 1 (,) +∞ ) → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ↾ ( 2 [,) +∞ ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
9 7 8 mp1i ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ↾ ( 2 [,) +∞ ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
10 7 sseli ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ( 1 (,) +∞ ) )
11 ioossre ⊢ ( 1 (,) +∞ ) ⊆ ℝ
12 11 sseli ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
13 10 12 syl ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ )
14 2re ⊢ 2 ∈ ℝ
15 pnfxr ⊢ +∞ ∈ ℝ*
16 elico2 ⊢ ( ( 2 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ∧ 𝑥 < +∞ ) ) )
17 14 15 16 mp2an ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ∧ 𝑥 < +∞ ) )
18 17 simp2bi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑥 )
19 chtrpcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
20 13 18 19 syl2anc ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
21 0red ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 0 ∈ ℝ )
22 1red ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 1 ∈ ℝ )
23 0lt1 ⊢ 0 < 1
24 23 a1i ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 0 < 1 )
25 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
26 25 simpld ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 1 < 𝑥 )
27 21 22 12 24 26 lttrd ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 0 < 𝑥 )
28 12 27 elrpd ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ )
29 10 28 syl ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ )
30 20 29 rpdivcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ+ )
31 30 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ+ )
32 ppinncl ⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( π ‘ 𝑥 ) ∈ ℕ )
33 13 18 32 syl2anc ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℕ )
34 33 nnrpd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℝ+ )
35 12 26 rplogcld ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
36 10 35 syl ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
37 34 36 rpmulcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
38 20 37 rpdivcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ+ )
39 38 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ+ )
40 29 ssriv ⊢ ( 2 [,) +∞ ) ⊆ ℝ+
41 resmpt ⊢ ( ( 2 [,) +∞ ) ⊆ ℝ+ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) )
42 40 41 ax-mp ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) )
43 pnt2 ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1
44 rlimres ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 → ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) ⇝𝑟 1 )
45 43 44 mp1i ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) ⇝𝑟 1 )
46 42 45 eqbrtrrid ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ⇝𝑟 1 )
47 chtppilim ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1
48 47 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 )
49 ax-1ne0 ⊢ 1 ≠ 0
50 49 a1i ⊢ ( ⊤ → 1 ≠ 0 )
51 38 rpne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ≠ 0 )
52 51 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ≠ 0 )
53 31 39 46 48 50 52 rlimdiv ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( θ ‘ 𝑥 ) / 𝑥 ) / ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ⇝𝑟 ( 1 / 1 ) )
54 13 recnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℂ )
55 chtcl ⊢ ( 𝑥 ∈ ℝ → ( θ ‘ 𝑥 ) ∈ ℝ )
56 12 55 syl ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℝ )
57 56 recnd ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℂ )
58 10 57 syl ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℂ )
59 54 58 mulcomd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 · ( θ ‘ 𝑥 ) ) = ( ( θ ‘ 𝑥 ) · 𝑥 ) )
60 59 oveq2d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( θ ‘ 𝑥 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( θ ‘ 𝑥 ) ) ) = ( ( ( θ ‘ 𝑥 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( ( θ ‘ 𝑥 ) · 𝑥 ) ) )
61 37 rpcnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
62 29 rpne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ≠ 0 )
63 20 rpne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ≠ 0 )
64 61 54 58 62 63 divcan5d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( θ ‘ 𝑥 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( ( θ ‘ 𝑥 ) · 𝑥 ) ) = ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
65 60 64 eqtrd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( θ ‘ 𝑥 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( θ ‘ 𝑥 ) ) ) = ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
66 37 rpne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ≠ 0 )
67 58 54 58 61 62 66 63 divdivdivd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( θ ‘ 𝑥 ) / 𝑥 ) / ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) = ( ( ( θ ‘ 𝑥 ) · ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( θ ‘ 𝑥 ) ) ) )
68 33 nncnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℂ )
69 36 rpcnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℂ )
70 36 rpne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ≠ 0 )
71 68 54 69 62 70 divdiv2d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / 𝑥 ) )
72 65 67 71 3eqtr4d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( θ ‘ 𝑥 ) / 𝑥 ) / ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) = ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) )
73 72 mpteq2ia ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( θ ‘ 𝑥 ) / 𝑥 ) / ( ( θ ‘ 𝑥 ) / ( ( π ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) )
74 1div1e1 ⊢ ( 1 / 1 ) = 1
75 53 73 74 3brtr3g ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 )
76 9 75 eqbrtrd ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ↾ ( 2 [,) +∞ ) ) ⇝𝑟 1 )
77 ppicl ⊢ ( 𝑥 ∈ ℝ → ( π ‘ 𝑥 ) ∈ ℕ0 )
78 12 77 syl ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℕ0 )
79 78 nn0red ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℝ )
80 28 35 rpdivcld ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 𝑥 / ( log ‘ 𝑥 ) ) ∈ ℝ+ )
81 79 80 rerpdivcld ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
82 81 recnd ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ∈ ℂ )
83 82 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ∈ ℂ )
84 83 fmpttd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) : ( 1 (,) +∞ ) ⟶ ℂ )
85 11 a1i ⊢ ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ )
86 14 a1i ⊢ ( ⊤ → 2 ∈ ℝ )
87 84 85 86 rlimresb ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 ↔ ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ↾ ( 2 [,) +∞ ) ) ⇝𝑟 1 ) )
88 76 87 mpbird ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 )
89 88 mptru ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1