Theorem chebbnd1

Description: The Chebyshev bound: The function ppi ( x ) is eventually lower bounded by a positive constant times x / log ( x ) . Alternatively stated, the function ( x / log ( x ) ) / ppi ( x ) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014)

	Ref	Expression
Assertion	chebbnd1	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)⟼\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
3		icossre	$$⊢\left(2\in ℝ\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left[2,\mathrm{+\infty }\right)\subseteq ℝ$$
4	1 2 3	mp2an	$$⊢\left[2,\mathrm{+\infty }\right)\subseteq ℝ$$
5	4	a1i	$$⊢\top \to \left[2,\mathrm{+\infty }\right)\subseteq ℝ$$
6		elicopnf	$$⊢2\in ℝ\to \left(x\in \left[2,\mathrm{+\infty }\right)\leftrightarrow \left(x\in ℝ\wedge 2\le x\right)\right)$$
7	1 6	ax-mp	$$⊢x\in \left[2,\mathrm{+\infty }\right)\leftrightarrow \left(x\in ℝ\wedge 2\le x\right)$$
8	7	simplbi	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to x\in ℝ$$
9		0red	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to 0\in ℝ$$
10		1re	$$⊢1\in ℝ$$
11	10	a1i	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to 1\in ℝ$$
12		0lt1	$$⊢0<1$$
13	12	a1i	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to 0<1$$
14	1	a1i	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to 2\in ℝ$$
15		1lt2	$$⊢1<2$$
16	15	a1i	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to 1<2$$
17	7	simprbi	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to 2\le x$$
18	11 14 8 16 17	ltletrd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to 1<x$$
19	9 11 8 13 18	lttrd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to 0<x$$
20	8 19	elrpd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to x\in {ℝ}^{+}$$
21	8 18	rplogcld	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \log x\in {ℝ}^{+}$$
22	20 21	rpdivcld	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{x}{\log x}\in {ℝ}^{+}$$
23		ppinncl	$$⊢\left(x\in ℝ\wedge 2\le x\right)\to \underset{\_}{\pi }\left(x\right)\in \mathbb{N}$$
24	7 23	sylbi	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \underset{\_}{\pi }\left(x\right)\in \mathbb{N}$$
25	24	nnrpd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \underset{\_}{\pi }\left(x\right)\in {ℝ}^{+}$$
26	22 25	rpdivcld	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in {ℝ}^{+}$$
27	26	rpcnd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in ℂ$$
28	27	adantl	$$⊢\left(\top \wedge x\in \left[2,\mathrm{+\infty }\right)\right)\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in ℂ$$
29		8re	$$⊢8\in ℝ$$
30	29	a1i	$$⊢\top \to 8\in ℝ$$
31		2rp	$$⊢2\in {ℝ}^{+}$$
32		relogcl	$$⊢2\in {ℝ}^{+}\to \log 2\in ℝ$$
33	31 32	ax-mp	$$⊢\log 2\in ℝ$$
34		ere	$$⊢\mathrm{e}\in ℝ$$
35	1 34	remulcli	$$⊢2\mathrm{e}\in ℝ$$
36		2pos	$$⊢0<2$$
37		epos	$$⊢0<\mathrm{e}$$
38	1 34 36 37	mulgt0ii	$$⊢0<2\mathrm{e}$$
39	35 38	gt0ne0ii	$$⊢2\mathrm{e}\ne 0$$
40	35 39	rereccli	$$⊢\frac{1}{2\mathrm{e}}\in ℝ$$
41	33 40	resubcli	$$⊢\log 2-\left(\frac{1}{2\mathrm{e}}\right)\in ℝ$$
42		2t1e2	$$⊢2\cdot 1=2$$
43		egt2lt3	$$⊢\left(2<\mathrm{e}\wedge \mathrm{e}<3\right)$$
44	43	simpli	$$⊢2<\mathrm{e}$$
45	10 1 34	lttri	$$⊢\left(1<2\wedge 2<\mathrm{e}\right)\to 1<\mathrm{e}$$
46	15 44 45	mp2an	$$⊢1<\mathrm{e}$$
47	10 34 1	ltmul2i	$$⊢0<2\to \left(1<\mathrm{e}\leftrightarrow 2\cdot 1<2\mathrm{e}\right)$$
48	36 47	ax-mp	$$⊢1<\mathrm{e}\leftrightarrow 2\cdot 1<2\mathrm{e}$$
49	46 48	mpbi	$$⊢2\cdot 1<2\mathrm{e}$$
50	42 49	eqbrtrri	$$⊢2<2\mathrm{e}$$
51	1 35 36 38	ltrecii	$$⊢2<2\mathrm{e}\leftrightarrow \frac{1}{2\mathrm{e}}<\frac{1}{2}$$
52	50 51	mpbi	$$⊢\frac{1}{2\mathrm{e}}<\frac{1}{2}$$
53	43	simpri	$$⊢\mathrm{e}<3$$
54		3lt4	$$⊢3<4$$
55		3re	$$⊢3\in ℝ$$
56		4re	$$⊢4\in ℝ$$
57	34 55 56	lttri	$$⊢\left(\mathrm{e}<3\wedge 3<4\right)\to \mathrm{e}<4$$
58	53 54 57	mp2an	$$⊢\mathrm{e}<4$$
59		epr	$$⊢\mathrm{e}\in {ℝ}^{+}$$
60		4pos	$$⊢0<4$$
61	56 60	elrpii	$$⊢4\in {ℝ}^{+}$$
62		logltb	$$⊢\left(\mathrm{e}\in {ℝ}^{+}\wedge 4\in {ℝ}^{+}\right)\to \left(\mathrm{e}<4\leftrightarrow \log \mathrm{e}<\log 4\right)$$
63	59 61 62	mp2an	$$⊢\mathrm{e}<4\leftrightarrow \log \mathrm{e}<\log 4$$
64	58 63	mpbi	$$⊢\log \mathrm{e}<\log 4$$
65		loge	$$⊢\log \mathrm{e}=1$$
66		sq2	$$⊢2^2=4$$
67	66	fveq2i	$$⊢\log 2^2=\log 4$$
68		2z	$$⊢2\in \mathbb{Z}$$
69		relogexp	$$⊢\left(2\in {ℝ}^{+}\wedge 2\in \mathbb{Z}\right)\to \log 2^2=2\log 2$$
70	31 68 69	mp2an	$$⊢\log 2^2=2\log 2$$
71	67 70	eqtr3i	$$⊢\log 4=2\log 2$$
72	64 65 71	3brtr3i	$$⊢1<2\log 2$$
73	1 36	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
74		ltdivmul	$$⊢\left(1\in ℝ\wedge \log 2\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\frac{1}{2}<\log 2\leftrightarrow 1<2\log 2\right)$$
75	10 33 73 74	mp3an	$$⊢\frac{1}{2}<\log 2\leftrightarrow 1<2\log 2$$
76	72 75	mpbir	$$⊢\frac{1}{2}<\log 2$$
77		halfre	$$⊢\frac{1}{2}\in ℝ$$
78	40 77 33	lttri	$$⊢\left(\frac{1}{2\mathrm{e}}<\frac{1}{2}\wedge \frac{1}{2}<\log 2\right)\to \frac{1}{2\mathrm{e}}<\log 2$$
79	52 76 78	mp2an	$$⊢\frac{1}{2\mathrm{e}}<\log 2$$
80	40 33	posdifi	$$⊢\frac{1}{2\mathrm{e}}<\log 2\leftrightarrow 0<\log 2-\left(\frac{1}{2\mathrm{e}}\right)$$
81	79 80	mpbi	$$⊢0<\log 2-\left(\frac{1}{2\mathrm{e}}\right)$$
82	41 81	elrpii	$$⊢\log 2-\left(\frac{1}{2\mathrm{e}}\right)\in {ℝ}^{+}$$
83		rerpdivcl	$$⊢\left(2\in ℝ\wedge \log 2-\left(\frac{1}{2\mathrm{e}}\right)\in {ℝ}^{+}\right)\to \frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\in ℝ$$
84	1 82 83	mp2an	$$⊢\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\in ℝ$$
85	84	a1i	$$⊢\top \to \frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\in ℝ$$
86		rpre	$$⊢\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in {ℝ}^{+}\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in ℝ$$
87		rpge0	$$⊢\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in {ℝ}^{+}\to 0\le \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}$$
88	86 87	absidd	$$⊢\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in {ℝ}^{+}\to \left|\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right|=\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}$$
89	26 88	syl	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \left|\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right|=\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}$$
90	89	adantr	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \left|\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right|=\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}$$
91		eqid	$$⊢⌊\frac{x}{2}⌋=⌊\frac{x}{2}⌋$$
92	91	chebbnd1lem3	$$⊢\left(x\in ℝ\wedge 8\le x\right)\to \frac{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}{2}<\underset{\_}{\pi }\left(x\right)\left(\frac{\log x}{x}\right)$$
93	8 92	sylan	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \frac{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}{2}<\underset{\_}{\pi }\left(x\right)\left(\frac{\log x}{x}\right)$$
94	1	recni	$$⊢2\in ℂ$$
95		2ne0	$$⊢2\ne 0$$
96	41	recni	$$⊢\log 2-\left(\frac{1}{2\mathrm{e}}\right)\in ℂ$$
97	41 81	gt0ne0ii	$$⊢\log 2-\left(\frac{1}{2\mathrm{e}}\right)\ne 0$$
98		recdiv	$$⊢\left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(\log 2-\left(\frac{1}{2\mathrm{e}}\right)\in ℂ\wedge \log 2-\left(\frac{1}{2\mathrm{e}}\right)\ne 0\right)\right)\to \frac{1}{\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}}=\frac{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}{2}$$
99	94 95 96 97 98	mp4an	$$⊢\frac{1}{\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}}=\frac{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}{2}$$
100	99	a1i	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \frac{1}{\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}}=\frac{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}{2}$$
101	22	rpcnd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{x}{\log x}\in ℂ$$
102	24	nncnd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \underset{\_}{\pi }\left(x\right)\in ℂ$$
103	22	rpne0d	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{x}{\log x}\ne 0$$
104	24	nnne0d	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \underset{\_}{\pi }\left(x\right)\ne 0$$
105	101 102 103 104	recdivd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{1}{\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}}=\frac{\underset{\_}{\pi }\left(x\right)}{\frac{x}{\log x}}$$
106	102 101 103	divrecd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{\underset{\_}{\pi }\left(x\right)}{\frac{x}{\log x}}=\underset{\_}{\pi }\left(x\right)\left(\frac{1}{\frac{x}{\log x}}\right)$$
107	20	rpcnne0d	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \left(x\in ℂ\wedge x\ne 0\right)$$
108	21	rpcnne0d	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \left(\log x\in ℂ\wedge \log x\ne 0\right)$$
109		recdiv	$$⊢\left(\left(x\in ℂ\wedge x\ne 0\right)\wedge \left(\log x\in ℂ\wedge \log x\ne 0\right)\right)\to \frac{1}{\frac{x}{\log x}}=\frac{\log x}{x}$$
110	107 108 109	syl2anc	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{1}{\frac{x}{\log x}}=\frac{\log x}{x}$$
111	110	oveq2d	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \underset{\_}{\pi }\left(x\right)\left(\frac{1}{\frac{x}{\log x}}\right)=\underset{\_}{\pi }\left(x\right)\left(\frac{\log x}{x}\right)$$
112	105 106 111	3eqtrd	$$⊢x\in \left[2,\mathrm{+\infty }\right)\to \frac{1}{\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}}=\underset{\_}{\pi }\left(x\right)\left(\frac{\log x}{x}\right)$$
113	112	adantr	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \frac{1}{\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}}=\underset{\_}{\pi }\left(x\right)\left(\frac{\log x}{x}\right)$$
114	93 100 113	3brtr4d	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \frac{1}{\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}}<\frac{1}{\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}}$$
115	26	adantr	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in {ℝ}^{+}$$
116		elrp	$$⊢\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in {ℝ}^{+}\leftrightarrow \left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in ℝ\wedge 0<\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right)$$
117	1 41 36 81	divgt0ii	$$⊢0<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}$$
118		ltrec	$$⊢\left(\left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in ℝ\wedge 0<\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right)\wedge \left(\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\in ℝ\wedge 0<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\right)\right)\to \left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\leftrightarrow \frac{1}{\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}}<\frac{1}{\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}}\right)$$
119	84 117 118	mpanr12	$$⊢\left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in ℝ\wedge 0<\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right)\to \left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\leftrightarrow \frac{1}{\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}}<\frac{1}{\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}}\right)$$
120	116 119	sylbi	$$⊢\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in {ℝ}^{+}\to \left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\leftrightarrow \frac{1}{\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}}<\frac{1}{\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}}\right)$$
121	115 120	syl	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\leftrightarrow \frac{1}{\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}}<\frac{1}{\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}}\right)$$
122	114 121	mpbird	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}$$
123	115	rpred	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in ℝ$$
124		ltle	$$⊢\left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\in ℝ\wedge \frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\in ℝ\right)\to \left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\le \frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\right)$$
125	123 84 124	sylancl	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \left(\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}<\frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\le \frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}\right)$$
126	122 125	mpd	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\le \frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}$$
127	90 126	eqbrtrd	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\to \left|\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right|\le \frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}$$
128	127	adantl	$$⊢\left(\top \wedge \left(x\in \left[2,\mathrm{+\infty }\right)\wedge 8\le x\right)\right)\to \left|\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right|\le \frac{2}{\log 2-\left(\frac{1}{2\mathrm{e}}\right)}$$
129	5 28 30 85 128	elo1d	$$⊢\top \to \left(x\in \left[2,\mathrm{+\infty }\right)⟼\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right)\in 𝑂\left(1\right)$$
130	129	mptru	$$⊢\left(x\in \left[2,\mathrm{+\infty }\right)⟼\frac{\frac{x}{\log x}}{\underset{\_}{\pi }\left(x\right)}\right)\in 𝑂\left(1\right)$$