mnflt

Description: Minus infinity is less than any (finite) real. (Contributed by NM, 14-Oct-2005)

		Ref	Expression
	Assertion	mnflt	$⊢ A \in ℝ \to −∞ < A$

Step	Hyp	Ref	Expression
1		eqid	$⊢ −∞ = −∞$
2		olc	$⊢ (−∞ = −∞ \land A \in ℝ) \to ((−∞ \in ℝ \land A = +∞) \lor (−∞ = −∞ \land A \in ℝ))$
3	1 2	mpan	$⊢ A \in ℝ \to ((−∞ \in ℝ \land A = +∞) \lor (−∞ = −∞ \land A \in ℝ))$
4	3	olcd	$⊢ A \in ℝ \to ((((−∞ \in ℝ \land A \in ℝ) \land −∞ <_{ℝ} A) \lor (−∞ = −∞ \land A = +∞)) \lor ((−∞ \in ℝ \land A = +∞) \lor (−∞ = −∞ \land A \in ℝ)))$
5		mnfxr	$⊢ −∞ \in ℝ^{*}$
6		rexr	$⊢ A \in ℝ \to A \in ℝ^{*}$
7		ltxr	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to (−∞ < A \leftrightarrow ((((−∞ \in ℝ \land A \in ℝ) \land −∞ <_{ℝ} A) \lor (−∞ = −∞ \land A = +∞)) \lor ((−∞ \in ℝ \land A = +∞) \lor (−∞ = −∞ \land A \in ℝ))))$
8	5 6 7	sylancr	$⊢ A \in ℝ \to (−∞ < A \leftrightarrow ((((−∞ \in ℝ \land A \in ℝ) \land −∞ <_{ℝ} A) \lor (−∞ = −∞ \land A = +∞)) \lor ((−∞ \in ℝ \land A = +∞) \lor (−∞ = −∞ \land A \in ℝ))))$
9	4 8	mpbird	$⊢ A \in ℝ \to −∞ < A$

Metamath Proof Explorer