chpchtlim

Description: The psi and theta functions are asymptotic to each other, so is sufficient to prove either theta ( x ) / x ~>r 1 or psi ( x ) / x ~>r 1 to establish the PNT. (Contributed by Mario Carneiro, 8-Apr-2016)

		Ref	Expression
	Assertion	chpchtlim	$⊢ (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \underset{ℝ}{⇝} 1$

Proof

Step	Hyp	Ref	Expression
1		1red	$⊢ ⊤ \to 1 \in ℝ$
2		1red	$⊢ (⊤ \land x \in [2, +∞)) \to 1 \in ℝ$
3		2re	$⊢ 2 \in ℝ$
4		elicopnf	$⊢ 2 \in ℝ \to (x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x))$
5	3 4	ax-mp	$⊢ x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x)$
6	5	simplbi	$⊢ x \in [2, +∞) \to x \in ℝ$
7	6	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to x \in ℝ$
8		0red	$⊢ x \in [2, +∞) \to 0 \in ℝ$
9	3	a1i	$⊢ x \in [2, +∞) \to 2 \in ℝ$
10		2pos	$⊢ 0 < 2$
11	10	a1i	$⊢ x \in [2, +∞) \to 0 < 2$
12	5	simprbi	$⊢ x \in [2, +∞) \to 2 \leq x$
13	8 9 6 11 12	ltletrd	$⊢ x \in [2, +∞) \to 0 < x$
14	6 13	elrpd	$⊢ x \in [2, +∞) \to x \in ℝ^{+}$
15	14	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to x \in ℝ^{+}$
16	15	rpge0d	$⊢ (⊤ \land x \in [2, +∞)) \to 0 \leq x$
17	7 16	resqrtcld	$⊢ (⊤ \land x \in [2, +∞)) \to \sqrt{x} \in ℝ$
18	15	relogcld	$⊢ (⊤ \land x \in [2, +∞)) \to \log x \in ℝ$
19	17 18	remulcld	$⊢ (⊤ \land x \in [2, +∞)) \to \sqrt{x} \log x \in ℝ$
20	12	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to 2 \leq x$
21		chtrpcl	$⊢ (x \in ℝ \land 2 \leq x) \to θ (x) \in ℝ^{+}$
22	7 20 21	syl2anc	$⊢ (⊤ \land x \in [2, +∞)) \to θ (x) \in ℝ^{+}$
23	19 22	rerpdivcld	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\sqrt{x} \log x}{θ (x)} \in ℝ$
24	6	ssriv	$⊢ [2, +∞) \subseteq ℝ$
25	1	recnd	$⊢ ⊤ \to 1 \in ℂ$
26		rlimconst	$⊢ ([2, +∞) \subseteq ℝ \land 1 \in ℂ) \to (x \in [2, +∞) ⟼ 1) \underset{ℝ}{⇝} 1$
27	24 25 26	sylancr	$⊢ ⊤ \to (x \in [2, +∞) ⟼ 1) \underset{ℝ}{⇝} 1$
28		ovexd	$⊢ ⊤ \to [2, +∞) \in V$
29	7 22	rerpdivcld	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{x}{θ (x)} \in ℝ$
30		ovexd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\sqrt{x} \log x}{x} \in V$
31		eqidd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{x}{θ (x)}) = (x \in [2, +∞) ⟼ \frac{x}{θ (x)})$
32	7	recnd	$⊢ (⊤ \land x \in [2, +∞)) \to x \in ℂ$
33		cxpsqrt	$⊢ x \in ℂ \to x^{\frac{1}{2}} = \sqrt{x}$
34	32 33	syl	$⊢ (⊤ \land x \in [2, +∞)) \to x^{\frac{1}{2}} = \sqrt{x}$
35	34	oveq2d	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\log x}{x^{\frac{1}{2}}} = \frac{\log x}{\sqrt{x}}$
36	18	recnd	$⊢ (⊤ \land x \in [2, +∞)) \to \log x \in ℂ$
37	15	rpsqrtcld	$⊢ (⊤ \land x \in [2, +∞)) \to \sqrt{x} \in ℝ^{+}$
38	37	rpcnne0d	$⊢ (⊤ \land x \in [2, +∞)) \to (\sqrt{x} \in ℂ \land \sqrt{x} \neq 0)$
39		divcan5	$⊢ (\log x \in ℂ \land (\sqrt{x} \in ℂ \land \sqrt{x} \neq 0) \land (\sqrt{x} \in ℂ \land \sqrt{x} \neq 0)) \to \frac{\sqrt{x} \log x}{\sqrt{x} \sqrt{x}} = \frac{\log x}{\sqrt{x}}$
40	36 38 38 39	syl3anc	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\sqrt{x} \log x}{\sqrt{x} \sqrt{x}} = \frac{\log x}{\sqrt{x}}$
41		remsqsqrt	$⊢ (x \in ℝ \land 0 \leq x) \to \sqrt{x} \sqrt{x} = x$
42	7 16 41	syl2anc	$⊢ (⊤ \land x \in [2, +∞)) \to \sqrt{x} \sqrt{x} = x$
43	42	oveq2d	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\sqrt{x} \log x}{\sqrt{x} \sqrt{x}} = \frac{\sqrt{x} \log x}{x}$
44	35 40 43	3eqtr2d	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\log x}{x^{\frac{1}{2}}} = \frac{\sqrt{x} \log x}{x}$
45	44	mpteq2dva	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\log x}{x^{\frac{1}{2}}}) = (x \in [2, +∞) ⟼ \frac{\sqrt{x} \log x}{x})$
46	28 29 30 31 45	offval2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{\log x}{x^{\frac{1}{2}}}) = (x \in [2, +∞) ⟼ (\frac{x}{θ (x)}) (\frac{\sqrt{x} \log x}{x}))$
47	15	rpne0d	$⊢ (⊤ \land x \in [2, +∞)) \to x \neq 0$
48	22	rpcnne0d	$⊢ (⊤ \land x \in [2, +∞)) \to (θ (x) \in ℂ \land θ (x) \neq 0)$
49	19	recnd	$⊢ (⊤ \land x \in [2, +∞)) \to \sqrt{x} \log x \in ℂ$
50		dmdcan	$⊢ ((x \in ℂ \land x \neq 0) \land (θ (x) \in ℂ \land θ (x) \neq 0) \land \sqrt{x} \log x \in ℂ) \to (\frac{x}{θ (x)}) (\frac{\sqrt{x} \log x}{x}) = \frac{\sqrt{x} \log x}{θ (x)}$
51	32 47 48 49 50	syl211anc	$⊢ (⊤ \land x \in [2, +∞)) \to (\frac{x}{θ (x)}) (\frac{\sqrt{x} \log x}{x}) = \frac{\sqrt{x} \log x}{θ (x)}$
52	51	mpteq2dva	$⊢ ⊤ \to (x \in [2, +∞) ⟼ (\frac{x}{θ (x)}) (\frac{\sqrt{x} \log x}{x})) = (x \in [2, +∞) ⟼ \frac{\sqrt{x} \log x}{θ (x)})$
53	46 52	eqtrd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{\log x}{x^{\frac{1}{2}}}) = (x \in [2, +∞) ⟼ \frac{\sqrt{x} \log x}{θ (x)})$
54		chto1lb	$⊢ (x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \in 𝑂 (1)$
55	14	ssriv	$⊢ [2, +∞) \subseteq ℝ^{+}$
56	55	a1i	$⊢ ⊤ \to [2, +∞) \subseteq ℝ^{+}$
57		1rp	$⊢ 1 \in ℝ^{+}$
58		rphalfcl	$⊢ 1 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
59	57 58	ax-mp	$⊢ \frac{1}{2} \in ℝ^{+}$
60		cxploglim	$⊢ \frac{1}{2} \in ℝ^{+} \to (x \in ℝ^{+} ⟼ \frac{\log x}{x^{\frac{1}{2}}}) \underset{ℝ}{⇝} 0$
61	59 60	ax-mp	$⊢ (x \in ℝ^{+} ⟼ \frac{\log x}{x^{\frac{1}{2}}}) \underset{ℝ}{⇝} 0$
62	61	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\log x}{x^{\frac{1}{2}}}) \underset{ℝ}{⇝} 0$
63	56 62	rlimres2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\log x}{x^{\frac{1}{2}}}) \underset{ℝ}{⇝} 0$
64		o1rlimmul	$⊢ ((x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \in 𝑂 (1) \land (x \in [2, +∞) ⟼ \frac{\log x}{x^{\frac{1}{2}}}) \underset{ℝ}{⇝} 0) \to ((x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{\log x}{x^{\frac{1}{2}}})) \underset{ℝ}{⇝} 0$
65	54 63 64	sylancr	$⊢ ⊤ \to ((x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{\log x}{x^{\frac{1}{2}}})) \underset{ℝ}{⇝} 0$
66	53 65	eqbrtrrd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\sqrt{x} \log x}{θ (x)}) \underset{ℝ}{⇝} 0$
67	2 23 27 66	rlimadd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ 1 + (\frac{\sqrt{x} \log x}{θ (x)})) \underset{ℝ}{⇝} (1 + 0)$
68		1p0e1	$⊢ 1 + 0 = 1$
69	67 68	breqtrdi	$⊢ ⊤ \to (x \in [2, +∞) ⟼ 1 + (\frac{\sqrt{x} \log x}{θ (x)})) \underset{ℝ}{⇝} 1$
70		1re	$⊢ 1 \in ℝ$
71		readdcl	$⊢ (1 \in ℝ \land \frac{\sqrt{x} \log x}{θ (x)} \in ℝ) \to 1 + (\frac{\sqrt{x} \log x}{θ (x)}) \in ℝ$
72	70 23 71	sylancr	$⊢ (⊤ \land x \in [2, +∞)) \to 1 + (\frac{\sqrt{x} \log x}{θ (x)}) \in ℝ$
73		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
74	7 73	syl	$⊢ (⊤ \land x \in [2, +∞)) \to ψ (x) \in ℝ$
75	74 22	rerpdivcld	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{ψ (x)}{θ (x)} \in ℝ$
76		chtcl	$⊢ x \in ℝ \to θ (x) \in ℝ$
77	7 76	syl	$⊢ (⊤ \land x \in [2, +∞)) \to θ (x) \in ℝ$
78	77 19	readdcld	$⊢ (⊤ \land x \in [2, +∞)) \to θ (x) + \sqrt{x} \log x \in ℝ$
79	3	a1i	$⊢ (⊤ \land x \in [2, +∞)) \to 2 \in ℝ$
80		1le2	$⊢ 1 \leq 2$
81	80	a1i	$⊢ (⊤ \land x \in [2, +∞)) \to 1 \leq 2$
82	2 79 7 81 20	letrd	$⊢ (⊤ \land x \in [2, +∞)) \to 1 \leq x$
83		chpub	$⊢ (x \in ℝ \land 1 \leq x) \to ψ (x) \leq θ (x) + \sqrt{x} \log x$
84	7 82 83	syl2anc	$⊢ (⊤ \land x \in [2, +∞)) \to ψ (x) \leq θ (x) + \sqrt{x} \log x$
85	74 78 22 84	lediv1dd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{ψ (x)}{θ (x)} \leq \frac{θ (x) + \sqrt{x} \log x}{θ (x)}$
86	22	rpcnd	$⊢ (⊤ \land x \in [2, +∞)) \to θ (x) \in ℂ$
87		divdir	$⊢ (θ (x) \in ℂ \land \sqrt{x} \log x \in ℂ \land (θ (x) \in ℂ \land θ (x) \neq 0)) \to \frac{θ (x) + \sqrt{x} \log x}{θ (x)} = (\frac{θ (x)}{θ (x)}) + (\frac{\sqrt{x} \log x}{θ (x)})$
88	86 49 48 87	syl3anc	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x) + \sqrt{x} \log x}{θ (x)} = (\frac{θ (x)}{θ (x)}) + (\frac{\sqrt{x} \log x}{θ (x)})$
89		divid	$⊢ (θ (x) \in ℂ \land θ (x) \neq 0) \to \frac{θ (x)}{θ (x)} = 1$
90	48 89	syl	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{θ (x)} = 1$
91	90	oveq1d	$⊢ (⊤ \land x \in [2, +∞)) \to (\frac{θ (x)}{θ (x)}) + (\frac{\sqrt{x} \log x}{θ (x)}) = 1 + (\frac{\sqrt{x} \log x}{θ (x)})$
92	88 91	eqtrd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x) + \sqrt{x} \log x}{θ (x)} = 1 + (\frac{\sqrt{x} \log x}{θ (x)})$
93	85 92	breqtrd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{ψ (x)}{θ (x)} \leq 1 + (\frac{\sqrt{x} \log x}{θ (x)})$
94	93	adantrr	$⊢ (⊤ \land (x \in [2, +∞) \land 1 \leq x)) \to \frac{ψ (x)}{θ (x)} \leq 1 + (\frac{\sqrt{x} \log x}{θ (x)})$
95	86	mullidd	$⊢ (⊤ \land x \in [2, +∞)) \to 1 θ (x) = θ (x)$
96		chtlepsi	$⊢ x \in ℝ \to θ (x) \leq ψ (x)$
97	7 96	syl	$⊢ (⊤ \land x \in [2, +∞)) \to θ (x) \leq ψ (x)$
98	95 97	eqbrtrd	$⊢ (⊤ \land x \in [2, +∞)) \to 1 θ (x) \leq ψ (x)$
99	2 74 22	lemuldivd	$⊢ (⊤ \land x \in [2, +∞)) \to (1 θ (x) \leq ψ (x) \leftrightarrow 1 \leq \frac{ψ (x)}{θ (x)})$
100	98 99	mpbid	$⊢ (⊤ \land x \in [2, +∞)) \to 1 \leq \frac{ψ (x)}{θ (x)}$
101	100	adantrr	$⊢ (⊤ \land (x \in [2, +∞) \land 1 \leq x)) \to 1 \leq \frac{ψ (x)}{θ (x)}$
102	1 1 69 72 75 94 101	rlimsqz2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \underset{ℝ}{⇝} 1$
103	102	mptru	$⊢ (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \underset{ℝ}{⇝} 1$

Metamath Proof Explorer

Theorem chpchtlim

Proof