Metamath Proof Explorer

Theorem mnfltd

Description: Minus infinity is less than any (finite) real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis mnfltd.a 
|- ( ph -> A e. RR )
Assertion mnfltd 
|- ( ph -> -oo < A )

Proof

Step Hyp Ref Expression
1 mnfltd.a 
 |-  ( ph -> A e. RR )
2 mnflt 
 |-  ( A e. RR -> -oo < A )
3 1 2 syl 
 |-  ( ph -> -oo < A )