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 )