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 ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ≠ -∞ )

Proof

Step Hyp Ref Expression
1 ge0gtmnf ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → -∞ < 𝐴 )
2 ngtmnft ( 𝐴 ∈ ℝ* → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )
3 2 adantr ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )
4 3 necon2abid ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → ( -∞ < 𝐴𝐴 ≠ -∞ ) )
5 1 4 mpbid ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → 𝐴 ≠ -∞ )