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

Metamath Proof Explorer

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	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		rlimconst	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐵 )
2		rlimo1	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝_𝑟 𝐵 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )
3	1 2	syl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )