Metamath Proof Explorer

Theorem sgnmnf

Description: The signum of -oo is -1. (Contributed by David A. Wheeler, 26-Jun-2016)

Ref Expression
Assertion sgnmnf 
|- ( sgn ` -oo ) = -u 1

Proof

Step Hyp Ref Expression
1 mnfxr 
 |-  -oo e. RR*
2 mnflt0 
 |-  -oo < 0
3 sgnn 
 |-  ( ( -oo e. RR* /\ -oo < 0 ) -> ( sgn ` -oo ) = -u 1 )
4 1 2 3 mp2an 
 |-  ( sgn ` -oo ) = -u 1