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

Metamath Proof Explorer

Theorem mnfle

Description: Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006)

		Ref	Expression
	Assertion	mnfle	$⊢ A \in ℝ^{*} \to −∞ \leq A$

Step	Hyp	Ref	Expression
1		nltmnf	$⊢ A \in ℝ^{*} \to \neg A < −∞$
2		mnfxr	$⊢ −∞ \in ℝ^{*}$
3		xrlenlt	$⊢ (−∞ \in ℝ^{} \land A \in ℝ^{}) \to (−∞ \leq A \leftrightarrow \neg A < −∞)$
4	2 3	mpan	$⊢ A \in ℝ^{*} \to (−∞ \leq A \leftrightarrow \neg A < −∞)$
5	1 4	mpbird	$⊢ A \in ℝ^{*} \to −∞ \leq A$