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

Metamath Proof Explorer

Theorem chebbnd2

Proof