pnt2

Description: The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to x . (Contributed by Mario Carneiro, 1-Jun-2016)

		Ref	Expression
	Assertion	pnt2	$⊢ (x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) \underset{ℝ}{⇝} 1$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2		elicopnf	$⊢ 2 \in ℝ \to (x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x))$
3	1 2	ax-mp	$⊢ x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x)$
4		chprpcl	$⊢ (x \in ℝ \land 2 \leq x) \to ψ (x) \in ℝ^{+}$
5	3 4	sylbi	$⊢ x \in [2, +∞) \to ψ (x) \in ℝ^{+}$
6	3	simplbi	$⊢ x \in [2, +∞) \to x \in ℝ$
7		0red	$⊢ x \in [2, +∞) \to 0 \in ℝ$
8	1	a1i	$⊢ x \in [2, +∞) \to 2 \in ℝ$
9		2pos	$⊢ 0 < 2$
10	9	a1i	$⊢ x \in [2, +∞) \to 0 < 2$
11	3	simprbi	$⊢ x \in [2, +∞) \to 2 \leq x$
12	7 8 6 10 11	ltletrd	$⊢ x \in [2, +∞) \to 0 < x$
13	6 12	elrpd	$⊢ x \in [2, +∞) \to x \in ℝ^{+}$
14	5 13	rpdivcld	$⊢ x \in [2, +∞) \to \frac{ψ (x)}{x} \in ℝ^{+}$
15	14	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{ψ (x)}{x} \in ℝ^{+}$
16		chtrpcl	$⊢ (x \in ℝ \land 2 \leq x) \to θ (x) \in ℝ^{+}$
17	3 16	sylbi	$⊢ x \in [2, +∞) \to θ (x) \in ℝ^{+}$
18	5 17	rpdivcld	$⊢ x \in [2, +∞) \to \frac{ψ (x)}{θ (x)} \in ℝ^{+}$
19	18	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{ψ (x)}{θ (x)} \in ℝ^{+}$
20	13	ssriv	$⊢ [2, +∞) \subseteq ℝ^{+}$
21	20	a1i	$⊢ ⊤ \to [2, +∞) \subseteq ℝ^{+}$
22		pnt3	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$
23	22	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$
24	21 23	rlimres2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{ψ (x)}{x}) \underset{ℝ}{⇝} 1$
25		chpchtlim	$⊢ (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \underset{ℝ}{⇝} 1$
26	25	a1i	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \underset{ℝ}{⇝} 1$
27		ax-1ne0	$⊢ 1 \neq 0$
28	27	a1i	$⊢ ⊤ \to 1 \neq 0$
29	19	rpne0d	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{ψ (x)}{θ (x)} \neq 0$
30	15 19 24 26 28 29	rlimdiv	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\frac{ψ (x)}{x}}{\frac{ψ (x)}{θ (x)}}) \underset{ℝ}{⇝} (\frac{1}{1})$
31		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
32		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
33	31 32	syl	$⊢ x \in ℝ^{+} \to ψ (x) \in ℝ$
34	33	recnd	$⊢ x \in ℝ^{+} \to ψ (x) \in ℂ$
35	13 34	syl	$⊢ x \in [2, +∞) \to ψ (x) \in ℂ$
36	13	rpcnne0d	$⊢ x \in [2, +∞) \to (x \in ℂ \land x \neq 0)$
37	5	rpcnne0d	$⊢ x \in [2, +∞) \to (ψ (x) \in ℂ \land ψ (x) \neq 0)$
38	17	rpcnne0d	$⊢ x \in [2, +∞) \to (θ (x) \in ℂ \land θ (x) \neq 0)$
39		divdivdiv	$⊢ ((ψ (x) \in ℂ \land (x \in ℂ \land x \neq 0)) \land ((ψ (x) \in ℂ \land ψ (x) \neq 0) \land (θ (x) \in ℂ \land θ (x) \neq 0))) \to \frac{\frac{ψ (x)}{x}}{\frac{ψ (x)}{θ (x)}} = \frac{ψ (x) θ (x)}{x ψ (x)}$
40	35 36 37 38 39	syl22anc	$⊢ x \in [2, +∞) \to \frac{\frac{ψ (x)}{x}}{\frac{ψ (x)}{θ (x)}} = \frac{ψ (x) θ (x)}{x ψ (x)}$
41	6	recnd	$⊢ x \in [2, +∞) \to x \in ℂ$
42	41 35	mulcomd	$⊢ x \in [2, +∞) \to x ψ (x) = ψ (x) x$
43	42	oveq2d	$⊢ x \in [2, +∞) \to \frac{ψ (x) θ (x)}{x ψ (x)} = \frac{ψ (x) θ (x)}{ψ (x) x}$
44		chtcl	$⊢ x \in ℝ \to θ (x) \in ℝ$
45	31 44	syl	$⊢ x \in ℝ^{+} \to θ (x) \in ℝ$
46	45	recnd	$⊢ x \in ℝ^{+} \to θ (x) \in ℂ$
47	13 46	syl	$⊢ x \in [2, +∞) \to θ (x) \in ℂ$
48		divcan5	$⊢ (θ (x) \in ℂ \land (x \in ℂ \land x \neq 0) \land (ψ (x) \in ℂ \land ψ (x) \neq 0)) \to \frac{ψ (x) θ (x)}{ψ (x) x} = \frac{θ (x)}{x}$
49	47 36 37 48	syl3anc	$⊢ x \in [2, +∞) \to \frac{ψ (x) θ (x)}{ψ (x) x} = \frac{θ (x)}{x}$
50	40 43 49	3eqtrd	$⊢ x \in [2, +∞) \to \frac{\frac{ψ (x)}{x}}{\frac{ψ (x)}{θ (x)}} = \frac{θ (x)}{x}$
51	50	mpteq2ia	$⊢ (x \in [2, +∞) ⟼ \frac{\frac{ψ (x)}{x}}{\frac{ψ (x)}{θ (x)}}) = (x \in [2, +∞) ⟼ \frac{θ (x)}{x})$
52		resmpt	$⊢ [2, +∞) \subseteq ℝ^{+} \to {(x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) ↾}_{[2, +∞)} = (x \in [2, +∞) ⟼ \frac{θ (x)}{x})$
53	20 52	ax-mp	$⊢ {(x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) ↾}_{[2, +∞)} = (x \in [2, +∞) ⟼ \frac{θ (x)}{x})$
54	51 53	eqtr4i	$⊢ (x \in [2, +∞) ⟼ \frac{\frac{ψ (x)}{x}}{\frac{ψ (x)}{θ (x)}}) = {(x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) ↾}_{[2, +∞)}$
55		1div1e1	$⊢ \frac{1}{1} = 1$
56	30 54 55	3brtr3g	$⊢ ⊤ \to ({(x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) ↾}_{[2, +∞)}) \underset{ℝ}{⇝} 1$
57		rerpdivcl	$⊢ (θ (x) \in ℝ \land x \in ℝ^{+}) \to \frac{θ (x)}{x} \in ℝ$
58	45 57	mpancom	$⊢ x \in ℝ^{+} \to \frac{θ (x)}{x} \in ℝ$
59	58	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{θ (x)}{x} \in ℝ$
60	59	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{θ (x)}{x} \in ℂ$
61	60	fmpttd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) : ℝ^{+} ⟶ ℂ$
62		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
63	62	a1i	$⊢ ⊤ \to ℝ^{+} \subseteq ℝ$
64	1	a1i	$⊢ ⊤ \to 2 \in ℝ$
65	61 63 64	rlimresb	$⊢ ⊤ \to ((x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) \underset{ℝ}{⇝} 1 \leftrightarrow ({(x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) ↾}_{[2, +∞)}) \underset{ℝ}{⇝} 1)$
66	56 65	mpbird	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) \underset{ℝ}{⇝} 1$
67	66	mptru	$⊢ (x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) \underset{ℝ}{⇝} 1$

Metamath Proof Explorer

Theorem pnt2

Proof