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)