Theorem o1const

Description: A constant function is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

	Ref	Expression
Assertion	o1const	$$⊢\left(A\subseteq ℝ\wedge B\in ℂ\right)\to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$

Proof

Step	Hyp	Ref	Expression
1		rlimconst	$$⊢\left(A\subseteq ℝ\wedge B\in ℂ\right)\to \left(x\in A⟼B\right)\underset{ℝ}{⇝}B$$
2		rlimo1	$$⊢\left(x\in A⟼B\right)\underset{ℝ}{⇝}B\to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$
3	1 2	syl	$$⊢\left(A\subseteq ℝ\wedge B\in ℂ\right)\to \left(x\in A⟼B\right)\in 𝑂\left(1\right)$$