chto1lb

Description: The theta function is lower bounded by a linear term. Corollary of chebbnd1 . (Contributed by Mario Carneiro, 8-Apr-2016)

		Ref	Expression
	Assertion	chto1lb	$⊢ (x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		ovexd	$⊢ ⊤ \to [2, +∞) \in V$
2		2re	$⊢ 2 \in ℝ$
3		elicopnf	$⊢ 2 \in ℝ \to (x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x))$
4	2 3	ax-mp	$⊢ x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x)$
5	4	biimpi	$⊢ x \in [2, +∞) \to (x \in ℝ \land 2 \leq x)$
6	5	simpld	$⊢ x \in [2, +∞) \to x \in ℝ$
7		0red	$⊢ x \in [2, +∞) \to 0 \in ℝ$
8	2	a1i	$⊢ x \in [2, +∞) \to 2 \in ℝ$
9		2pos	$⊢ 0 < 2$
10	9	a1i	$⊢ x \in [2, +∞) \to 0 < 2$
11	5	simprd	$⊢ x \in [2, +∞) \to 2 \leq x$
12	7 8 6 10 11	ltletrd	$⊢ x \in [2, +∞) \to 0 < x$
13	6 12	elrpd	$⊢ x \in [2, +∞) \to x \in ℝ^{+}$
14		ppinncl	$⊢ (x \in ℝ \land 2 \leq x) \to \underline{π} (x) \in ℕ$
15	14	nnrpd	$⊢ (x \in ℝ \land 2 \leq x) \to \underline{π} (x) \in ℝ^{+}$
16	5 15	syl	$⊢ x \in [2, +∞) \to \underline{π} (x) \in ℝ^{+}$
17		1red	$⊢ x \in [2, +∞) \to 1 \in ℝ$
18		1lt2	$⊢ 1 < 2$
19	18	a1i	$⊢ x \in [2, +∞) \to 1 < 2$
20	17 8 6 19 11	ltletrd	$⊢ x \in [2, +∞) \to 1 < x$
21	6 20	rplogcld	$⊢ x \in [2, +∞) \to \log x \in ℝ^{+}$
22	16 21	rpmulcld	$⊢ x \in [2, +∞) \to \underline{π} (x) \log x \in ℝ^{+}$
23	13 22	rpdivcld	$⊢ x \in [2, +∞) \to \frac{x}{\underline{π} (x) \log x} \in ℝ^{+}$
24	23	rpcnd	$⊢ x \in [2, +∞) \to \frac{x}{\underline{π} (x) \log x} \in ℂ$
25	24	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{x}{\underline{π} (x) \log x} \in ℂ$
26		chtrpcl	$⊢ (x \in ℝ \land 2 \leq x) \to θ (x) \in ℝ^{+}$
27	5 26	syl	$⊢ x \in [2, +∞) \to θ (x) \in ℝ^{+}$
28	22 27	rpdivcld	$⊢ x \in [2, +∞) \to \frac{\underline{π} (x) \log x}{θ (x)} \in ℝ^{+}$
29	28	rpcnd	$⊢ x \in [2, +∞) \to \frac{\underline{π} (x) \log x}{θ (x)} \in ℂ$
30	29	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{\underline{π} (x) \log x}{θ (x)} \in ℂ$
31	6	recnd	$⊢ x \in [2, +∞) \to x \in ℂ$
32	21	rpcnd	$⊢ x \in [2, +∞) \to \log x \in ℂ$
33	16	rpcnd	$⊢ x \in [2, +∞) \to \underline{π} (x) \in ℂ$
34	21	rpne0d	$⊢ x \in [2, +∞) \to \log x \neq 0$
35	16	rpne0d	$⊢ x \in [2, +∞) \to \underline{π} (x) \neq 0$
36	31 32 33 34 35	divdiv1d	$⊢ x \in [2, +∞) \to \frac{\frac{x}{\log x}}{\underline{π} (x)} = \frac{x}{\log x \underline{π} (x)}$
37	32 33	mulcomd	$⊢ x \in [2, +∞) \to \log x \underline{π} (x) = \underline{π} (x) \log x$
38	37	oveq2d	$⊢ x \in [2, +∞) \to \frac{x}{\log x \underline{π} (x)} = \frac{x}{\underline{π} (x) \log x}$
39	36 38	eqtrd	$⊢ x \in [2, +∞) \to \frac{\frac{x}{\log x}}{\underline{π} (x)} = \frac{x}{\underline{π} (x) \log x}$
40	39	mpteq2ia	$⊢ (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) = (x \in [2, +∞) ⟼ \frac{x}{\underline{π} (x) \log x})$
41	40	a1i	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) = (x \in [2, +∞) ⟼ \frac{x}{\underline{π} (x) \log x})$
42	27	rpcnd	$⊢ x \in [2, +∞) \to θ (x) \in ℂ$
43	22	rpcnd	$⊢ x \in [2, +∞) \to \underline{π} (x) \log x \in ℂ$
44	27	rpne0d	$⊢ x \in [2, +∞) \to θ (x) \neq 0$
45	22	rpne0d	$⊢ x \in [2, +∞) \to \underline{π} (x) \log x \neq 0$
46	42 43 44 45	recdivd	$⊢ x \in [2, +∞) \to \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}} = \frac{\underline{π} (x) \log x}{θ (x)}$
47	46	mpteq2ia	$⊢ (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) = (x \in [2, +∞) ⟼ \frac{\underline{π} (x) \log x}{θ (x)})$
48	47	a1i	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) = (x \in [2, +∞) ⟼ \frac{\underline{π} (x) \log x}{θ (x)})$
49	1 25 30 41 48	offval2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) = (x \in [2, +∞) ⟼ (\frac{x}{\underline{π} (x) \log x}) (\frac{\underline{π} (x) \log x}{θ (x)}))$
50	31 43 42 45 44	dmdcan2d	$⊢ x \in [2, +∞) \to (\frac{x}{\underline{π} (x) \log x}) (\frac{\underline{π} (x) \log x}{θ (x)}) = \frac{x}{θ (x)}$
51	50	mpteq2ia	$⊢ (x \in [2, +∞) ⟼ (\frac{x}{\underline{π} (x) \log x}) (\frac{\underline{π} (x) \log x}{θ (x)})) = (x \in [2, +∞) ⟼ \frac{x}{θ (x)})$
52	49 51	eqtrdi	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) = (x \in [2, +∞) ⟼ \frac{x}{θ (x)})$
53		chebbnd1	$⊢ (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \in 𝑂 (1)$
54		ax-1cn	$⊢ 1 \in ℂ$
55	54	a1i	$⊢ (⊤ \land x \in [2, +∞)) \to 1 \in ℂ$
56	27 22	rpdivcld	$⊢ x \in [2, +∞) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℝ^{+}$
57	56	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℝ^{+}$
58	57	rpcnd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{\underline{π} (x) \log x} \in ℂ$
59	6	ssriv	$⊢ [2, +∞) \subseteq ℝ$
60		rlimconst	$⊢ ([2, +∞) \subseteq ℝ \land 1 \in ℂ) \to (x \in [2, +∞) ⟼ 1) \underset{ℝ}{⇝} 1$
61	59 54 60	mp2an	$⊢ (x \in [2, +∞) ⟼ 1) \underset{ℝ}{⇝} 1$
62	61	a1i	$⊢ ⊤ \to (x \in [2, +∞) ⟼ 1) \underset{ℝ}{⇝} 1$
63		chtppilim	$⊢ (x \in [2, +∞) ⟼ \frac{θ (x)}{\underline{π} (x) \log x}) \underset{ℝ}{⇝} 1$
64	63	a1i	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{\underline{π} (x) \log x}) \underset{ℝ}{⇝} 1$
65		ax-1ne0	$⊢ 1 \neq 0$
66	65	a1i	$⊢ ⊤ \to 1 \neq 0$
67	56	rpne0d	$⊢ x \in [2, +∞) \to \frac{θ (x)}{\underline{π} (x) \log x} \neq 0$
68	67	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{\underline{π} (x) \log x} \neq 0$
69	55 58 62 64 66 68	rlimdiv	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \underset{ℝ}{⇝} (\frac{1}{1})$
70		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)$
71	69 70	syl	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)$
72		o1mul	$⊢ ((x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \in 𝑂 (1) \land (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)) \to (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)$
73	53 71 72	sylancr	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{\frac{x}{\log x}}{\underline{π} (x)}) \times_{f} (x \in [2, +∞) ⟼ \frac{1}{\frac{θ (x)}{\underline{π} (x) \log x}}) \in 𝑂 (1)$
74	52 73	eqeltrrd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \in 𝑂 (1)$
75	74	mptru	$⊢ (x \in [2, +∞) ⟼ \frac{x}{θ (x)}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem chto1lb

Proof