ge0gtmnf

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

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

Step	Hyp	Ref	Expression
1		mnflt0	$⊢ −∞ < 0$
2		mnfxr	$⊢ −∞ \in ℝ^{*}$
3		0xr	$⊢ 0 \in ℝ^{*}$
4		xrltletr	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land A \in ℝ^{*}) \to ((−∞ < 0 \land 0 \leq A) \to −∞ < A)$
5	2 3 4	mp3an12	$⊢ A \in ℝ^{*} \to ((−∞ < 0 \land 0 \leq A) \to −∞ < A)$
6	5	imp	$⊢ (A \in ℝ^{*} \land (−∞ < 0 \land 0 \leq A)) \to −∞ < A$
7	1 6	mpanr1	$⊢ (A \in ℝ^{*} \land 0 \leq A) \to −∞ < A$

Metamath Proof Explorer