Metamath Proof Explorer

Theorem mnflt0

Description: Minus infinity is less than 0. (Contributed by David A. Wheeler, 8-Dec-2018)

Ref Expression
Assertion mnflt0 
|- -oo < 0

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 mnflt 
 |-  ( 0 e. RR -> -oo < 0 )
3 1 2 ax-mp 
 |-  -oo < 0