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