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