Theorem ge0gtmnf

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

	Ref	Expression
Assertion	ge0gtmnf	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → -∞ < 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mnflt0	⊢ -∞ < 0
2		mnfxr	⊢ -∞ ∈ ℝ*
3		0xr	⊢ 0 ∈ ℝ*
4		xrltletr	⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 ≤ 𝐴 ) → -∞ < 𝐴 ) )
5	2 3 4	mp3an12	⊢ ( 𝐴 ∈ ℝ* → ( ( -∞ < 0 ∧ 0 ≤ 𝐴 ) → -∞ < 𝐴 ) )
6	5	imp	⊢ ( ( 𝐴 ∈ ℝ* ∧ ( -∞ < 0 ∧ 0 ≤ 𝐴 ) ) → -∞ < 𝐴 )
7	1 6	mpanr1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → -∞ < 𝐴 )