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	$⊢ (x \in (1, +∞) ⟼ \frac{\underline{π} (x)}{\frac{x}{\log x}}) \underset{ℝ}{⇝} 1$

Proof

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

Metamath Proof Explorer

Theorem pnt

Proof