Theorem ngtmnft

Description: An extended real is not greater than minus infinity iff they are equal. (Contributed by NM, 2-Feb-2006)

	Ref	Expression
Assertion	ngtmnft	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		mnfxr	⊢ -∞ ∈ ℝ*
2		xrltnr	⊢ ( -∞ ∈ ℝ* → ¬ -∞ < -∞ )
3	1 2	ax-mp	⊢ ¬ -∞ < -∞
4		breq2	⊢ ( 𝐴 = -∞ → ( -∞ < 𝐴 ↔ -∞ < -∞ ) )
5	3 4	mtbiri	⊢ ( 𝐴 = -∞ → ¬ -∞ < 𝐴 )
6		mnfle	⊢ ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )
7		xrleloe	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ ≤ 𝐴 ↔ ( -∞ < 𝐴 ∨ -∞ = 𝐴 ) ) )
8	1 7	mpan	⊢ ( 𝐴 ∈ ℝ* → ( -∞ ≤ 𝐴 ↔ ( -∞ < 𝐴 ∨ -∞ = 𝐴 ) ) )
9	6 8	mpbid	⊢ ( 𝐴 ∈ ℝ* → ( -∞ < 𝐴 ∨ -∞ = 𝐴 ) )
10	9	ord	⊢ ( 𝐴 ∈ ℝ* → ( ¬ -∞ < 𝐴 → -∞ = 𝐴 ) )
11		eqcom	⊢ ( -∞ = 𝐴 ↔ 𝐴 = -∞ )
12	10 11	imbitrdi	⊢ ( 𝐴 ∈ ℝ* → ( ¬ -∞ < 𝐴 → 𝐴 = -∞ ) )
13	5 12	impbid2	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )