chebbnd2

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

		Ref	Expression
	Assertion	chebbnd2	$⊢ (x \in [2, +∞) ⟼ \frac{\underline{π} (x)}{\frac{x}{\log x}}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		ovexd	$⊢ ⊤ \to [2, +∞) \in V$
2		ovexd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{x} \in V$
3		ovexd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\underline{π} (x) \log x}{θ (x)} \in V$
4		eqidd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) = (x \in [2, +∞) ⟼ \frac{θ (x)}{x})$
5		simpr	$⊢ (⊤ \land x \in [2, +∞)) \to x \in [2, +∞)$
6		2re	$⊢ 2 \in ℝ$
7		elicopnf	$⊢ 2 \in ℝ \to (x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x))$
8	6 7	ax-mp	$⊢ x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x)$
9	5 8	sylib	$⊢ (⊤ \land x \in [2, +∞)) \to (x \in ℝ \land 2 \leq x)$
10		chtrpcl	$⊢ (x \in ℝ \land 2 \leq x) \to θ (x) \in ℝ^{+}$
11	9 10	syl	$⊢ (⊤ \land x \in [2, +∞)) \to θ (x) \in ℝ^{+}$
12	11	rpcnne0d	$⊢ (⊤ \land x \in [2, +∞)) \to (θ (x) \in ℂ \land θ (x) \neq 0)$
13		ppinncl	$⊢ (x \in ℝ \land 2 \leq x) \to \underline{π} (x) \in ℕ$
14	9 13	syl	$⊢ (⊤ \land x \in [2, +∞)) \to \underline{π} (x) \in ℕ$
15	14	nnrpd	$⊢ (⊤ \land x \in [2, +∞)) \to \underline{π} (x) \in ℝ^{+}$
16	9	simpld	$⊢ (⊤ \land x \in [2, +∞)) \to x \in ℝ$
17		1red	$⊢ (⊤ \land x \in [2, +∞)) \to 1 \in ℝ$
18	6	a1i	$⊢ (⊤ \land x \in [2, +∞)) \to 2 \in ℝ$
19		1lt2	$⊢ 1 < 2$
20	19	a1i	$⊢ (⊤ \land x \in [2, +∞)) \to 1 < 2$
21	9	simprd	$⊢ (⊤ \land x \in [2, +∞)) \to 2 \leq x$
22	17 18 16 20 21	ltletrd	$⊢ (⊤ \land x \in [2, +∞)) \to 1 < x$
23	16 22	rplogcld	$⊢ (⊤ \land x \in [2, +∞)) \to \log x \in ℝ^{+}$
24	15 23	rpmulcld	$⊢ (⊤ \land x \in [2, +∞)) \to \underline{π} (x) \log x \in ℝ^{+}$
25	24	rpcnne0d	$⊢ (⊤ \land x \in [2, +∞)) \to (\underline{π} (x) \log x \in ℂ \land \underline{π} (x) \log x \neq 0)$
26		recdiv	$⊢ ((θ (x) \in ℂ \land θ (x) \neq 0) \land (\underline{π} (x) \log x \in ℂ \land \underline{π} (x) \log x \neq 0)) \to \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}} = \frac{\underline{π} (x) \log x}{θ (x)}$
27	12 25 26	syl2anc	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}} = \frac{\underline{π} (x) \log x}{θ (x)}$
28	27	mpteq2dva	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) = (x \in [2, +∞) ⟼ \frac{\underline{π} (x) \log x}{θ (x)})$
29	1 2 3 4 28	offval2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \times_{f} (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) = (x \in [2, +∞) ⟼ (\frac{θ (x)}{x}) (\frac{\underline{π} (x) \log x}{θ (x)}))$
30		0red	$⊢ (⊤ \land x \in [2, +∞)) \to 0 \in ℝ$
31		2pos	$⊢ 0 < 2$
32	31	a1i	$⊢ (⊤ \land x \in [2, +∞)) \to 0 < 2$
33	30 18 16 32 21	ltletrd	$⊢ (⊤ \land x \in [2, +∞)) \to 0 < x$
34	16 33	elrpd	$⊢ (⊤ \land x \in [2, +∞)) \to x \in ℝ^{+}$
35	34	rpcnne0d	$⊢ (⊤ \land x \in [2, +∞)) \to (x \in ℂ \land x \neq 0)$
36	24	rpcnd	$⊢ (⊤ \land x \in [2, +∞)) \to \underline{π} (x) \log x \in ℂ$
37		dmdcan	$⊢ ((θ (x) \in ℂ \land θ (x) \neq 0) \land (x \in ℂ \land x \neq 0) \land \underline{π} (x) \log x \in ℂ) \to (\frac{θ (x)}{x}) (\frac{\underline{π} (x) \log x}{θ (x)}) = \frac{\underline{π} (x) \log x}{x}$
38	12 35 36 37	syl3anc	$⊢ (⊤ \land x \in [2, +∞)) \to (\frac{θ (x)}{x}) (\frac{\underline{π} (x) \log x}{θ (x)}) = \frac{\underline{π} (x) \log x}{x}$
39	15	rpcnd	$⊢ (⊤ \land x \in [2, +∞)) \to \underline{π} (x) \in ℂ$
40	23	rpcnne0d	$⊢ (⊤ \land x \in [2, +∞)) \to (\log x \in ℂ \land \log x \neq 0)$
41		divdiv2	$⊢ (\underline{π} (x) \in ℂ \land (x \in ℂ \land x \neq 0) \land (\log x \in ℂ \land \log x \neq 0)) \to \frac{\underline{π} (x)}{\frac{x}{\log x}} = \frac{\underline{π} (x) \log x}{x}$
42	39 35 40 41	syl3anc	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\underline{π} (x)}{\frac{x}{\log x}} = \frac{\underline{π} (x) \log x}{x}$
43	38 42	eqtr4d	$⊢ (⊤ \land x \in [2, +∞)) \to (\frac{θ (x)}{x}) (\frac{\underline{π} (x) \log x}{θ (x)}) = \frac{\underline{π} (x)}{\frac{x}{\log x}}$
44	43	mpteq2dva	$⊢ ⊤ \to (x \in [2, +∞) ⟼ (\frac{θ (x)}{x}) (\frac{\underline{π} (x) \log x}{θ (x)})) = (x \in [2, +∞) ⟼ \frac{\underline{π} (x)}{\frac{x}{\log x}})$
45	29 44	eqtrd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \times_{f} (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) = (x \in [2, +∞) ⟼ \frac{\underline{π} (x)}{\frac{x}{\log x}})$
46	34	ex	$⊢ ⊤ \to (x \in [2, +∞) \to x \in ℝ^{+})$
47	46	ssrdv	$⊢ ⊤ \to [2, +∞) \subseteq ℝ^{+}$
48		chto1ub	$⊢ (x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) \in 𝑂 (1)$
49	48	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) \in 𝑂 (1)$
50	47 49	o1res2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \in 𝑂 (1)$
51		ax-1cn	$⊢ 1 \in ℂ$
52	51	a1i	$⊢ (⊤ \land x \in [2, +∞)) \to 1 \in ℂ$
53	11 24	rpdivcld	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℝ^{+}$
54	53	rpcnd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℂ$
55		pnfxr	$⊢ +∞ \in ℝ^{*}$
56		icossre	$⊢ (2 \in ℝ \land +∞ \in ℝ^{*}) \to [2, +∞) \subseteq ℝ$
57	6 55 56	mp2an	$⊢ [2, +∞) \subseteq ℝ$
58		rlimconst	$⊢ ([2, +∞) \subseteq ℝ \land 1 \in ℂ) \to (x \in [2, +∞) ⟼ 1) \underset{ℝ}{⇝} 1$
59	57 51 58	mp2an	$⊢ (x \in [2, +∞) ⟼ 1) \underset{ℝ}{⇝} 1$
60	59	a1i	$⊢ ⊤ \to (x \in [2, +∞) ⟼ 1) \underset{ℝ}{⇝} 1$
61		chtppilim	$⊢ (x \in [2, +∞) ⟼ \frac{θ (x)}{\underline{π} (x) \log x}) \underset{ℝ}{⇝} 1$
62	61	a1i	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{\underline{π} (x) \log x}) \underset{ℝ}{⇝} 1$
63		ax-1ne0	$⊢ 1 \neq 0$
64	63	a1i	$⊢ ⊤ \to 1 \neq 0$
65	53	rpne0d	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{\underline{π} (x) \log x} \neq 0$
66	52 54 60 62 64 65	rlimdiv	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \underset{ℝ}{⇝} (\frac{1}{1})$
67		rlimo1	$⊢ (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \underset{ℝ}{⇝} (\frac{1}{1}) \to (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)$
68	66 67	syl	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)$
69		o1mul	$⊢ ((x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \in 𝑂 (1) \land (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)) \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \times_{f} (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)$
70	50 68 69	syl2anc	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \times_{f} (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)$
71	45 70	eqeltrrd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\underline{π} (x)}{\frac{x}{\log x}}) \in 𝑂 (1)$
72	71	mptru	$⊢ (x \in [2, +∞) ⟼ \frac{\underline{π} (x)}{\frac{x}{\log x}}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem chebbnd2

Proof