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	|- ( ( A C_ RR /\ B e. CC ) -> ( x e. A |-> B ) e. O(1) )

Proof

Step	Hyp	Ref	Expression
1		rlimconst	|- ( ( A C_ RR /\ B e. CC ) -> ( x e. A |-> B ) ~~>r B )
2		rlimo1	|- ( ( x e. A |-> B ) ~~>r B -> ( x e. A |-> B ) e. O(1) )
3	1 2	syl	|- ( ( A C_ RR /\ B e. CC ) -> ( x e. A |-> B ) e. O(1) )