Theorem xlemnf

Description: An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018)

	Ref	Expression
Assertion	xlemnf	$$⊢A\in {ℝ}^{*}\to \left(A\le \mathrm{-\infty }\leftrightarrow A=\mathrm{-\infty }\right)$$

Proof

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