Theorem sgnn

Description: The signum of a negative extended real is -1. (Contributed by David A. Wheeler, 15-May-2015)

	Ref	Expression
Assertion	sgnn	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( sgn ‘ 𝐴 ) = - 1 )

Proof

Step	Hyp	Ref	Expression
1		sgnval	⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
3		0xr	⊢ 0 ∈ ℝ*
4		xrltne	⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 𝐴 < 0 ) → 0 ≠ 𝐴 )
5	3 4	mp3an2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → 0 ≠ 𝐴 )
6		nesym	⊢ ( 0 ≠ 𝐴 ↔ ¬ 𝐴 = 0 )
7	5 6	sylib	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ¬ 𝐴 = 0 )
8	7	iffalsed	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) = if ( 𝐴 < 0 , - 1 , 1 ) )
9		iftrue	⊢ ( 𝐴 < 0 → if ( 𝐴 < 0 , - 1 , 1 ) = - 1 )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → if ( 𝐴 < 0 , - 1 , 1 ) = - 1 )
11	2 8 10	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 < 0 ) → ( sgn ‘ 𝐴 ) = - 1 )