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

Metamath Proof Explorer

Theorem mnfltxr

Description: Minus infinity is less than an extended real that is either real or plus infinity. (Contributed by NM, 2-Feb-2006)

		Ref	Expression
	Assertion	mnfltxr	$⊢ (A \in ℝ \lor A = +∞) \to −∞ < A$

Step	Hyp	Ref	Expression
1		mnflt	$⊢ A \in ℝ \to −∞ < A$
2		mnfltpnf	$⊢ −∞ < +∞$
3		breq2	$⊢ A = +∞ \to (−∞ < A \leftrightarrow −∞ < +∞)$
4	2 3	mpbiri	$⊢ A = +∞ \to −∞ < A$
5	1 4	jaoi	$⊢ (A \in ℝ \lor A = +∞) \to −∞ < A$