Theorem mnfle

Description: Minus infinity is less than or equal to any extended real. (Contributed by NM, 19-Jan-2006)

	Ref	Expression
Assertion	mnfle	⊢ ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nltmnf	⊢ ( 𝐴 ∈ ℝ* → ¬ 𝐴 < -∞ )
2		mnfxr	⊢ -∞ ∈ ℝ*
3		xrlenlt	⊢ ( ( -∞ ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( -∞ ≤ 𝐴 ↔ ¬ 𝐴 < -∞ ) )
4	2 3	mpan	⊢ ( 𝐴 ∈ ℝ* → ( -∞ ≤ 𝐴 ↔ ¬ 𝐴 < -∞ ) )
5	1 4	mpbird	⊢ ( 𝐴 ∈ ℝ* → -∞ ≤ 𝐴 )