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

Metamath Proof Explorer

Theorem ge0nemnf

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

		Ref	Expression
	Assertion	ge0nemnf	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to A \neq −∞$

Step	Hyp	Ref	Expression
1		ge0gtmnf	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to −∞ < A$
2		ngtmnft	$⊢ A \in ℝ^{*} \to (A = −∞ \leftrightarrow \neg −∞ < A)$
3	2	adantr	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to (A = −∞ \leftrightarrow \neg −∞ < A)$
4	3	necon2abid	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to (−∞ < A \leftrightarrow A \neq −∞)$
5	1 4	mpbid	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to A \neq −∞$