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