Theorem ngtmnft

Description: An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006)

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

Proof

Step	Hyp	Ref	Expression
1		mnfxr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}$$
2		xrltnr	$$⊢\mathrm{-\infty }\in {ℝ}^{*}\to \neg \mathrm{-\infty }<\mathrm{-\infty }$$
3	1 2	ax-mp	$$⊢\neg \mathrm{-\infty }<\mathrm{-\infty }$$
4		breq2	$$⊢A=\mathrm{-\infty }\to \left(\mathrm{-\infty }<A\leftrightarrow \mathrm{-\infty }<\mathrm{-\infty }\right)$$
5	3 4	mtbiri	$$⊢A=\mathrm{-\infty }\to \neg \mathrm{-\infty }<A$$
6		mnfle	$$⊢A\in {ℝ}^{*}\to \mathrm{-\infty }\le A$$
7		xrleloe	$$⊢\left(\mathrm{-\infty }\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(\mathrm{-\infty }\le A\leftrightarrow \left(\mathrm{-\infty }<A\vee \mathrm{-\infty }=A\right)\right)$$
8	1 7	mpan	$$⊢A\in {ℝ}^{*}\to \left(\mathrm{-\infty }\le A\leftrightarrow \left(\mathrm{-\infty }<A\vee \mathrm{-\infty }=A\right)\right)$$
9	6 8	mpbid	$$⊢A\in {ℝ}^{*}\to \left(\mathrm{-\infty }<A\vee \mathrm{-\infty }=A\right)$$
10	9	ord	$$⊢A\in {ℝ}^{*}\to \left(\neg \mathrm{-\infty }<A\to \mathrm{-\infty }=A\right)$$
11		eqcom	$$⊢\mathrm{-\infty }=A\leftrightarrow A=\mathrm{-\infty }$$
12	10 11	imbitrdi	$$⊢A\in {ℝ}^{*}\to \left(\neg \mathrm{-\infty }<A\to A=\mathrm{-\infty }\right)$$
13	5 12	impbid2	$$⊢A\in {ℝ}^{*}\to \left(A=\mathrm{-\infty }\leftrightarrow \neg \mathrm{-\infty }<A\right)$$