This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 elicopnf ⊢ ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
3 1 2 ax-mp ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
4 chtrpcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
5 3 4 sylbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
6 5 rpcnne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) )
7 3 simplbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ )
8 0red ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 ∈ ℝ )
9 1 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ )
10 2pos ⊢ 0 < 2
11 10 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 2 )
12 3 simprbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑥 )
13 8 9 7 11 12 ltletrd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 𝑥 )
14 7 13 elrpd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ )
15 14 rpcnne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
16 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
17 chpcl ⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
18 16 17 syl ⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℝ )
19 18 recnd ⊢ ( 𝑥 ∈ ℝ+ → ( ψ ‘ 𝑥 ) ∈ ℂ )
20 14 19 syl ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ψ ‘ 𝑥 ) ∈ ℂ )
21 dmdcan ⊢ ( ( ( ( θ ‘ 𝑥 ) ∈ ℂ ∧ ( θ ‘ 𝑥 ) ≠ 0 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( ψ ‘ 𝑥 ) ∈ ℂ ) → ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) = ( ( ψ ‘ 𝑥 ) / 𝑥 ) )
22 6 15 20 21 syl3anc ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) = ( ( ψ ‘ 𝑥 ) / 𝑥 ) )
23 22 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) = ( ( ψ ‘ 𝑥 ) / 𝑥 ) )
24 23 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
25 ovexd ⊢ ( ⊤ → ( 2 [,) +∞ ) ∈ V )
26 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / 𝑥 ) ∈ V )
27 ovexd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ∈ V )
28 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) )
29 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) )
30 25 26 27 28 29 offval2 ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( θ ‘ 𝑥 ) / 𝑥 ) · ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) )
31 14 ssriv ⊢ ( 2 [,) +∞ ) ⊆ ℝ+
32 resmpt ⊢ ( ( 2 [,) +∞ ) ⊆ ℝ+ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
33 31 32 mp1i ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
34 24 30 33 3eqtr4rd ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) = ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) )
35 31 a1i ⊢ ( ⊤ → ( 2 [,) +∞ ) ⊆ ℝ+ )
36 chto1ub ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)
37 36 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
38 35 37 o1res2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
39 chpchtlim ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ⇝𝑟 1
40 rlimo1 ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ⇝𝑟 1 → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
41 39 40 ax-mp ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ∈ 𝑂(1)
42 o1mul ⊢ ( ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
43 38 41 42 sylancl ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( θ ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
44 34 43 eqeltrd ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) ∈ 𝑂(1) )
45 rerpdivcl ⊢ ( ( ( ψ ‘ 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
46 18 45 mpancom ⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
47 46 recnd ⊢ ( 𝑥 ∈ ℝ+ → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
48 47 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
49 48 fmpttd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) : ℝ+ ⟶ ℂ )
50 rpssre ⊢ ℝ+ ⊆ ℝ
51 50 a1i ⊢ ( ⊤ → ℝ+ ⊆ ℝ )
52 1 a1i ⊢ ( ⊤ → 2 ∈ ℝ )
53 49 51 52 o1resb ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ↾ ( 2 [,) +∞ ) ) ∈ 𝑂(1) ) )
54 44 53 mpbird ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
55 54 mptru ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)