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	$⊢ (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \in 𝑂 (1)$

Proof

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

Metamath Proof Explorer

Theorem chebbnd1

Proof