chpo1ub

Description: The psi function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016)

		Ref	Expression
	Assertion	chpo1ub	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2		elicopnf	$⊢ 2 \in ℝ \to (x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x))$
3	1 2	ax-mp	$⊢ x \in [2, +∞) \leftrightarrow (x \in ℝ \land 2 \leq x)$
4		chtrpcl	$⊢ (x \in ℝ \land 2 \leq x) \to θ (x) \in ℝ^{+}$
5	3 4	sylbi	$⊢ x \in [2, +∞) \to θ (x) \in ℝ^{+}$
6	5	rpcnne0d	$⊢ x \in [2, +∞) \to (θ (x) \in ℂ \land θ (x) \neq 0)$
7	3	simplbi	$⊢ x \in [2, +∞) \to x \in ℝ$
8		0red	$⊢ x \in [2, +∞) \to 0 \in ℝ$
9	1	a1i	$⊢ x \in [2, +∞) \to 2 \in ℝ$
10		2pos	$⊢ 0 < 2$
11	10	a1i	$⊢ x \in [2, +∞) \to 0 < 2$
12	3	simprbi	$⊢ x \in [2, +∞) \to 2 \leq x$
13	8 9 7 11 12	ltletrd	$⊢ x \in [2, +∞) \to 0 < x$
14	7 13	elrpd	$⊢ x \in [2, +∞) \to x \in ℝ^{+}$
15	14	rpcnne0d	$⊢ x \in [2, +∞) \to (x \in ℂ \land x \neq 0)$
16		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
17		chpcl	$⊢ x \in ℝ \to ψ (x) \in ℝ$
18	16 17	syl	$⊢ x \in ℝ^{+} \to ψ (x) \in ℝ$
19	18	recnd	$⊢ x \in ℝ^{+} \to ψ (x) \in ℂ$
20	14 19	syl	$⊢ x \in [2, +∞) \to ψ (x) \in ℂ$
21		dmdcan	$⊢ ((θ (x) \in ℂ \land θ (x) \neq 0) \land (x \in ℂ \land x \neq 0) \land ψ (x) \in ℂ) \to (\frac{θ (x)}{x}) (\frac{ψ (x)}{θ (x)}) = \frac{ψ (x)}{x}$
22	6 15 20 21	syl3anc	$⊢ x \in [2, +∞) \to (\frac{θ (x)}{x}) (\frac{ψ (x)}{θ (x)}) = \frac{ψ (x)}{x}$
23	22	adantl	$⊢ (⊤ \land x \in [2, +∞)) \to (\frac{θ (x)}{x}) (\frac{ψ (x)}{θ (x)}) = \frac{ψ (x)}{x}$
24	23	mpteq2dva	$⊢ ⊤ \to (x \in [2, +∞) ⟼ (\frac{θ (x)}{x}) (\frac{ψ (x)}{θ (x)})) = (x \in [2, +∞) ⟼ \frac{ψ (x)}{x})$
25		ovexd	$⊢ ⊤ \to [2, +∞) \in V$
26		ovexd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{θ (x)}{x} \in V$
27		ovexd	$⊢ (⊤ \land x \in [2, +∞)) \to \frac{ψ (x)}{θ (x)} \in V$
28		eqidd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) = (x \in [2, +∞) ⟼ \frac{θ (x)}{x})$
29		eqidd	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) = (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)})$
30	25 26 27 28 29	offval2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \times_{f} (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) = (x \in [2, +∞) ⟼ (\frac{θ (x)}{x}) (\frac{ψ (x)}{θ (x)}))$
31	14	ssriv	$⊢ [2, +∞) \subseteq ℝ^{+}$
32		resmpt	$⊢ [2, +∞) \subseteq ℝ^{+} \to {(x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) ↾}_{[2, +∞)} = (x \in [2, +∞) ⟼ \frac{ψ (x)}{x})$
33	31 32	mp1i	$⊢ ⊤ \to {(x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) ↾}_{[2, +∞)} = (x \in [2, +∞) ⟼ \frac{ψ (x)}{x})$
34	24 30 33	3eqtr4rd	$⊢ ⊤ \to {(x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) ↾}_{[2, +∞)} = (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \times_{f} (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)})$
35	31	a1i	$⊢ ⊤ \to [2, +∞) \subseteq ℝ^{+}$
36		chto1ub	$⊢ (x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) \in 𝑂 (1)$
37	36	a1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{θ (x)}{x}) \in 𝑂 (1)$
38	35 37	o1res2	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \in 𝑂 (1)$
39		chpchtlim	$⊢ (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \underset{ℝ}{⇝} 1$
40		rlimo1	$⊢ (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \underset{ℝ}{⇝} 1 \to (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \in 𝑂 (1)$
41	39 40	ax-mp	$⊢ (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \in 𝑂 (1)$
42		o1mul	$⊢ ((x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \in 𝑂 (1) \land (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \in 𝑂 (1)) \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \times_{f} (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \in 𝑂 (1)$
43	38 41 42	sylancl	$⊢ ⊤ \to (x \in [2, +∞) ⟼ \frac{θ (x)}{x}) \times_{f} (x \in [2, +∞) ⟼ \frac{ψ (x)}{θ (x)}) \in 𝑂 (1)$
44	34 43	eqeltrd	$⊢ ⊤ \to {(x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) ↾}_{[2, +∞)} \in 𝑂 (1)$
45		rerpdivcl	$⊢ (ψ (x) \in ℝ \land x \in ℝ^{+}) \to \frac{ψ (x)}{x} \in ℝ$
46	18 45	mpancom	$⊢ x \in ℝ^{+} \to \frac{ψ (x)}{x} \in ℝ$
47	46	recnd	$⊢ x \in ℝ^{+} \to \frac{ψ (x)}{x} \in ℂ$
48	47	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{ψ (x)}{x} \in ℂ$
49	48	fmpttd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) : ℝ^{+} ⟶ ℂ$
50		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
51	50	a1i	$⊢ ⊤ \to ℝ^{+} \subseteq ℝ$
52	1	a1i	$⊢ ⊤ \to 2 \in ℝ$
53	49 51 52	o1resb	$⊢ ⊤ \to ((x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1) \leftrightarrow {(x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) ↾}_{[2, +∞)} \in 𝑂 (1))$
54	44 53	mpbird	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$
55	54	mptru	$⊢ (x \in ℝ^{+} ⟼ \frac{ψ (x)}{x}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem chpo1ub

Proof