# Metamath Proof Explorer

## Theorem chpo1ub

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

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

### Proof

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