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

Proof

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