Metamath Proof Explorer


Theorem mnfled

Description: Minus infinity is less than or equal to any extended real. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis mnfled.1
|- ( ph -> A e. RR* )
Assertion mnfled
|- ( ph -> -oo <_ A )

Proof

Step Hyp Ref Expression
1 mnfled.1
 |-  ( ph -> A e. RR* )
2 mnfle
 |-  ( A e. RR* -> -oo <_ A )
3 1 2 syl
 |-  ( ph -> -oo <_ A )