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

Metamath Proof Explorer

Theorem rlimdmo1

Description: A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016)

		Ref	Expression
	Assertion	rlimdmo1	$⊢ F \in dom \underset{ℝ}{⇝} \to F \in 𝑂 (1)$

Step	Hyp	Ref	Expression
1		eldmg	$⊢ F \in dom \underset{ℝ}{⇝} \to (F \in dom \underset{ℝ}{⇝} \leftrightarrow \exists x F \underset{ℝ}{⇝} x)$
2	1	ibi	$⊢ F \in dom \underset{ℝ}{⇝} \to \exists x F \underset{ℝ}{⇝} x$
3		rlimo1	$⊢ F \underset{ℝ}{⇝} x \to F \in 𝑂 (1)$
4	3	exlimiv	$⊢ \exists x F \underset{ℝ}{⇝} x \to F \in 𝑂 (1)$
5	2 4	syl	$⊢ F \in dom \underset{ℝ}{⇝} \to F \in 𝑂 (1)$