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

Metamath Proof Explorer

Theorem xlemnf

Description: An extended real which is less than minus infinity is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018)

Ref Expression
Assertion xlemnf ⊢ A ∈ ℝ * → A ≤ −∞ ↔ A = −∞

Proof

Step Hyp Ref Expression
1 mnfxr ⊢ −∞ ∈ ℝ *
2 xrlenlt ⊢ A ∈ ℝ * ∧ −∞ ∈ ℝ * → A ≤ −∞ ↔ ¬ −∞ < A
3 1 2 mpan2 ⊢ A ∈ ℝ * → A ≤ −∞ ↔ ¬ −∞ < A
4 ngtmnft ⊢ A ∈ ℝ * → A = −∞ ↔ ¬ −∞ < A
5 3 4 bitr4d ⊢ A ∈ ℝ * → A ≤ −∞ ↔ A = −∞