Theorem sgnval

Description: Value of the signum function. (Contributed by David A. Wheeler, 15-May-2015)

	Ref	Expression
Assertion	sgnval	⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 0 ↔ 𝐴 = 0 ) )
2		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 < 0 ↔ 𝐴 < 0 ) )
3	2	ifbid	⊢ ( 𝑥 = 𝐴 → if ( 𝑥 < 0 , - 1 , 1 ) = if ( 𝐴 < 0 , - 1 , 1 ) )
4	1 3	ifbieq2d	⊢ ( 𝑥 = 𝐴 → if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )
5		df-sgn	⊢ sgn = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) )
6		c0ex	⊢ 0 ∈ V
7		negex	⊢ - 1 ∈ V
8		1ex	⊢ 1 ∈ V
9	7 8	ifex	⊢ if ( 𝐴 < 0 , - 1 , 1 ) ∈ V
10	6 9	ifex	⊢ if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) ∈ V
11	4 5 10	fvmpt	⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ 𝐴 ) = if ( 𝐴 = 0 , 0 , if ( 𝐴 < 0 , - 1 , 1 ) ) )