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 \mathrm{-\infty }\le A$$

Proof

Step	Hyp	Ref	Expression
1		nltmnf	$$⊢A\in {ℝ}^{*}\to \neg A<\mathrm{-\infty }$$
2		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
3		xrlenlt	$$⊢\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty }\le A\leftrightarrow \neg A<\mathrm{-\infty }\right)$$
4	2 3	mpan	$$⊢A\in {ℝ}^{*}\to \left(\mathrm{-\infty }\le A\leftrightarrow \neg A<\mathrm{-\infty }\right)$$
5	1 4	mpbird	$$⊢A\in {ℝ}^{*}\to \mathrm{-\infty }\le A$$