Metamath Proof Explorer


Theorem nemnftgtmnft

Description: An extended real that is not minus infinity, is larger than minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion nemnftgtmnft ( ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) → -∞ < 𝐴 )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) → 𝐴 ≠ -∞ )
2 1 neneqd ( ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) → ¬ 𝐴 = -∞ )
3 ngtmnft ( 𝐴 ∈ ℝ* → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )
4 3 adantr ( ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )
5 2 4 mtbid ( ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) → ¬ ¬ -∞ < 𝐴 )
6 notnotb ( -∞ < 𝐴 ↔ ¬ ¬ -∞ < 𝐴 )
7 5 6 sylibr ( ( 𝐴 ∈ ℝ*𝐴 ≠ -∞ ) → -∞ < 𝐴 )