Theorem ge0nemnf

Description: A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	ge0nemnf	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\right)\to A\ne \mathrm{-\infty }$$

Proof

Step	Hyp	Ref	Expression
1		ge0gtmnf	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\right)\to \mathrm{-\infty }<A$$
2		ngtmnft	$$⊢A\in {ℝ}^{*}\to \left(A=\mathrm{-\infty }\leftrightarrow \neg \mathrm{-\infty }<A\right)$$
3	2	adantr	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\right)\to \left(A=\mathrm{-\infty }\leftrightarrow \neg \mathrm{-\infty }<A\right)$$
4	3	necon2abid	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\right)\to \left(\mathrm{-\infty }<A\leftrightarrow A\ne \mathrm{-\infty }\right)$$
5	1 4	mpbid	$$⊢\left(A\in {ℝ}^{*}\wedge 0\le A\right)\to A\ne \mathrm{-\infty }$$