This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 = -∞ ↔ ¬ -∞ < 𝐴 ) )