chtppilim

Description: The theta function is asymptotic to ppi ( x ) log ( x ) , so it is sufficient to prove theta ( x ) / x ~>r 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		halfre	$⊢ \frac{1}{2} \in ℝ$
2		1re	$⊢ 1 \in ℝ$
3		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
4		resubcl	$⊢ (1 \in ℝ \land y \in ℝ) \to 1 - y \in ℝ$
5	2 3 4	sylancr	$⊢ y \in ℝ^{+} \to 1 - y \in ℝ$
6		ifcl	$⊢ (\frac{1}{2} \in ℝ \land 1 - y \in ℝ) \to if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \in ℝ$
7	1 5 6	sylancr	$⊢ y \in ℝ^{+} \to if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \in ℝ$
8		0red	$⊢ y \in ℝ^{+} \to 0 \in ℝ$
9	1	a1i	$⊢ y \in ℝ^{+} \to \frac{1}{2} \in ℝ$
10		halfgt0	$⊢ 0 < \frac{1}{2}$
11	10	a1i	$⊢ y \in ℝ^{+} \to 0 < \frac{1}{2}$
12		max2	$⊢ (1 - y \in ℝ \land \frac{1}{2} \in ℝ) \to \frac{1}{2} \leq if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)$
13	5 1 12	sylancl	$⊢ y \in ℝ^{+} \to \frac{1}{2} \leq if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)$
14	8 9 7 11 13	ltletrd	$⊢ y \in ℝ^{+} \to 0 < if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)$
15	7 14	elrpd	$⊢ y \in ℝ^{+} \to if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \in ℝ^{+}$
16	15	rpsqrtcld	$⊢ y \in ℝ^{+} \to \sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)} \in ℝ^{+}$
17		halflt1	$⊢ \frac{1}{2} < 1$
18		ltsubrp	$⊢ (1 \in ℝ \land y \in ℝ^{+}) \to 1 - y < 1$
19	2 18	mpan	$⊢ y \in ℝ^{+} \to 1 - y < 1$
20		breq1	$⊢ \frac{1}{2} = if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \to (\frac{1}{2} < 1 \leftrightarrow if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < 1)$
21		breq1	$⊢ 1 - y = if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \to (1 - y < 1 \leftrightarrow if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < 1)$
22	20 21	ifboth	$⊢ (\frac{1}{2} < 1 \land 1 - y < 1) \to if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < 1$
23	17 19 22	sylancr	$⊢ y \in ℝ^{+} \to if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < 1$
24	15	rpge0d	$⊢ y \in ℝ^{+} \to 0 \leq if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)$
25	2	a1i	$⊢ y \in ℝ^{+} \to 1 \in ℝ$
26		0le1	$⊢ 0 \leq 1$
27	26	a1i	$⊢ y \in ℝ^{+} \to 0 \leq 1$
28	7 24 25 27	sqrtltd	$⊢ y \in ℝ^{+} \to (if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < 1 \leftrightarrow \sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)} < \sqrt{1})$
29	23 28	mpbid	$⊢ y \in ℝ^{+} \to \sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)} < \sqrt{1}$
30		sqrt1	$⊢ \sqrt{1} = 1$
31	29 30	breqtrdi	$⊢ y \in ℝ^{+} \to \sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)} < 1$
32	16 31	chtppilimlem2	$⊢ y \in ℝ^{+} \to \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to {\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} \underline{π} (x) \log x < θ (x))$
33	5	adantr	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to 1 - y \in ℝ$
34		max1	$⊢ (1 - y \in ℝ \land \frac{1}{2} \in ℝ) \to 1 - y \leq if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)$
35	33 1 34	sylancl	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to 1 - y \leq if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)$
36	7	adantr	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \in ℝ$
37		2re	$⊢ 2 \in ℝ$
38		elicopnf	$⊢ 2 \in ℝ \to (x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x))$
39	37 38	ax-mp	$⊢ x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x)$
40	39	simplbi	$⊢ x \in [2, +∞) \to x \in ℝ$
41		chtcl	$⊢ x \in ℝ \to θ (x) \in ℝ$
42	40 41	syl	$⊢ x \in [2, +∞) \to θ (x) \in ℝ$
43		ppinncl	$⊢ (x \in ℝ \land 2 \leq x) \to \underline{π} (x) \in ℕ$
44	39 43	sylbi	$⊢ x \in [2, +∞) \to \underline{π} (x) \in ℕ$
45	44	nnrpd	$⊢ x \in [2, +∞) \to \underline{π} (x) \in ℝ^{+}$
46	2	a1i	$⊢ x \in [2, +∞) \to 1 \in ℝ$
47	37	a1i	$⊢ x \in [2, +∞) \to 2 \in ℝ$
48		1lt2	$⊢ 1 < 2$
49	48	a1i	$⊢ x \in [2, +∞) \to 1 < 2$
50	39	simprbi	$⊢ x \in [2, +∞) \to 2 \leq x$
51	46 47 40 49 50	ltletrd	$⊢ x \in [2, +∞) \to 1 < x$
52	40 51	rplogcld	$⊢ x \in [2, +∞) \to \log x \in ℝ^{+}$
53	45 52	rpmulcld	$⊢ x \in [2, +∞) \to \underline{π} (x) \log x \in ℝ^{+}$
54	42 53	rerpdivcld	$⊢ x \in [2, +∞) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℝ$
55	54	adantl	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℝ$
56		lelttr	$⊢ (1 - y \in ℝ \land if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \in ℝ \land \frac{θ (x)}{\underline{π} (x) \log x} \in ℝ) \to ((1 - y \leq if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \land if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < \frac{θ (x)}{\underline{π} (x) \log x}) \to 1 - y < \frac{θ (x)}{\underline{π} (x) \log x})$
57	33 36 55 56	syl3anc	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to ((1 - y \leq if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \land if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < \frac{θ (x)}{\underline{π} (x) \log x}) \to 1 - y < \frac{θ (x)}{\underline{π} (x) \log x})$
58	35 57	mpand	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to (if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < \frac{θ (x)}{\underline{π} (x) \log x} \to 1 - y < \frac{θ (x)}{\underline{π} (x) \log x})$
59	7	recnd	$⊢ y \in ℝ^{+} \to if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \in ℂ$
60	59	sqsqrtd	$⊢ y \in ℝ^{+} \to {\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} = if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)$
61	60	adantr	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to {\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} = if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)$
62	61	oveq1d	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to {\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} \underline{π} (x) \log x = if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \underline{π} (x) \log x$
63	62	breq1d	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to ({\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} \underline{π} (x) \log x < θ (x) \leftrightarrow if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \underline{π} (x) \log x < θ (x))$
64	42	adantl	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to θ (x) \in ℝ$
65	53	rpregt0d	$⊢ x \in [2, +∞) \to (\underline{π} (x) \log x \in ℝ \land 0 < \underline{π} (x) \log x)$
66	65	adantl	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to (\underline{π} (x) \log x \in ℝ \land 0 < \underline{π} (x) \log x)$
67		ltmuldiv	$⊢ (if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \in ℝ \land θ (x) \in ℝ \land (\underline{π} (x) \log x \in ℝ \land 0 < \underline{π} (x) \log x)) \to (if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \underline{π} (x) \log x < θ (x) \leftrightarrow if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < \frac{θ (x)}{\underline{π} (x) \log x})$
68	36 64 66 67	syl3anc	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to (if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) \underline{π} (x) \log x < θ (x) \leftrightarrow if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < \frac{θ (x)}{\underline{π} (x) \log x})$
69	63 68	bitrd	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to ({\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} \underline{π} (x) \log x < θ (x) \leftrightarrow if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y) < \frac{θ (x)}{\underline{π} (x) \log x})$
70		0red	$⊢ x \in [2, +∞) \to 0 \in ℝ$
71		2pos	$⊢ 0 < 2$
72	71	a1i	$⊢ x \in [2, +∞) \to 0 < 2$
73	70 47 40 72 50	ltletrd	$⊢ x \in [2, +∞) \to 0 < x$
74	40 73	elrpd	$⊢ x \in [2, +∞) \to x \in ℝ^{+}$
75		chtleppi	$⊢ x \in ℝ^{+} \to θ (x) \leq \underline{π} (x) \log x$
76	74 75	syl	$⊢ x \in [2, +∞) \to θ (x) \leq \underline{π} (x) \log x$
77	53	rpcnd	$⊢ x \in [2, +∞) \to \underline{π} (x) \log x \in ℂ$
78	77	mulridd	$⊢ x \in [2, +∞) \to \underline{π} (x) \log x \cdot 1 = \underline{π} (x) \log x$
79	76 78	breqtrrd	$⊢ x \in [2, +∞) \to θ (x) \leq \underline{π} (x) \log x \cdot 1$
80	42 46 53	ledivmuld	$⊢ x \in [2, +∞) \to (\frac{θ (x)}{\underline{π} (x) \log x} \leq 1 \leftrightarrow θ (x) \leq \underline{π} (x) \log x \cdot 1)$
81	79 80	mpbird	$⊢ x \in [2, +∞) \to \frac{θ (x)}{\underline{π} (x) \log x} \leq 1$
82	54 46 81	abssuble0d	$⊢ x \in [2, +∞) \to \|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| = 1 - (\frac{θ (x)}{\underline{π} (x) \log x})$
83	82	breq1d	$⊢ x \in [2, +∞) \to (\|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y \leftrightarrow 1 - (\frac{θ (x)}{\underline{π} (x) \log x}) < y)$
84	83	adantl	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to (\|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y \leftrightarrow 1 - (\frac{θ (x)}{\underline{π} (x) \log x}) < y)$
85	2	a1i	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to 1 \in ℝ$
86	3	adantr	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to y \in ℝ$
87		ltsub23	$⊢ (1 \in ℝ \land \frac{θ (x)}{\underline{π} (x) \log x} \in ℝ \land y \in ℝ) \to (1 - (\frac{θ (x)}{\underline{π} (x) \log x}) < y \leftrightarrow 1 - y < \frac{θ (x)}{\underline{π} (x) \log x})$
88	85 55 86 87	syl3anc	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to (1 - (\frac{θ (x)}{\underline{π} (x) \log x}) < y \leftrightarrow 1 - y < \frac{θ (x)}{\underline{π} (x) \log x})$
89	84 88	bitrd	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to (\|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y \leftrightarrow 1 - y < \frac{θ (x)}{\underline{π} (x) \log x})$
90	58 69 89	3imtr4d	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to ({\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} \underline{π} (x) \log x < θ (x) \to \|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y)$
91	90	imim2d	$⊢ (y \in ℝ^{+} \land x \in [2, +∞)) \to ((z \leq x \to {\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} \underline{π} (x) \log x < θ (x)) \to (z \leq x \to \|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y))$
92	91	ralimdva	$⊢ y \in ℝ^{+} \to (\forall x \in [2, +∞) (z \leq x \to {\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} \underline{π} (x) \log x < θ (x)) \to \forall x \in [2, +∞) (z \leq x \to \|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y))$
93	92	reximdv	$⊢ y \in ℝ^{+} \to (\exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to {\sqrt{if (1 - y \leq \frac{1}{2}, \frac{1}{2}, 1 - y)}}^{2} \underline{π} (x) \log x < θ (x)) \to \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to \|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y))$
94	32 93	mpd	$⊢ y \in ℝ^{+} \to \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to \|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y)$
95	94	rgen	$⊢ \forall y \in ℝ^{+} \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to \|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y)$
96	54	recnd	$⊢ x \in [2, +∞) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℂ$
97	96	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℂ$
98	97	ralrimiva	$⊢ ⊤ \to \forall x \in [2, +∞) \frac{θ (x)}{\underline{π} (x) \log x} \in ℂ$
99	40	ssriv	$⊢ [2, +∞) \subseteq ℝ$
100	99	a1i	$⊢ ⊤ \to [2, +∞) \subseteq ℝ$
101		1cnd	$⊢ ⊤ \to 1 \in ℂ$
102	98 100 101	rlim2	$⊢ ⊤ \to ((x \in [2, +∞) ⟼ \frac{θ (x)}{\underline{π} (x) \log x}) \underset{ℝ}{⇝} 1 \leftrightarrow \forall y \in ℝ^{+} \exists z \in ℝ \forall x \in [2, +∞) (z \leq x \to \|(\frac{θ (x)}{\underline{π} (x) \log x}) - 1\| < y))$
103	95 102	mpbiri	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{\underline{π} (x) \log x}) \underset{ℝ}{⇝} 1$
104	103	mptru	$⊢ (x \in [2, +∞) ⟼ \frac{θ (x)}{\underline{π} (x) \log x}) \underset{ℝ}{⇝} 1$

Metamath Proof Explorer

Theorem chtppilim

Proof