Theorem sgnmnf

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

	Ref	Expression
Assertion	sgnmnf	⊢ ( sgn ‘ -∞ ) = - 1

Proof

Step	Hyp	Ref	Expression
1		mnfxr	⊢ -∞ ∈ ℝ*
2		mnflt0	⊢ -∞ < 0
3		sgnn	⊢ ( ( -∞ ∈ ℝ* ∧ -∞ < 0 ) → ( sgn ‘ -∞ ) = - 1 )
4	1 2 3	mp2an	⊢ ( sgn ‘ -∞ ) = - 1