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

Metamath Proof Explorer

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