Description: Signum function. We do not call it "sign", which is homophonic with "sine" ( df-sin ). Defined as "sgn" in ISO 80000-2:2009(E) operation 2-9.13. It is named "sign" (with the same definition) in the "NIST Digital Library of Mathematical Functions" , front introduction, "Common Notations and Definitions" section at http://dlmf.nist.gov/front/introduction#Sx4 . We define this over RR* ( df-xr ) instead of RR so that it can accept +oo and -oo . Note that df-psgn defines the sign of a permutation, which is different. Value shown in sgnval . (Contributed by David A. Wheeler, 15-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-sgn | ⊢ sgn = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | csgn | ⊢ sgn | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | cxr | ⊢ ℝ* | |
| 3 | 1 | cv | ⊢ 𝑥 |
| 4 | cc0 | ⊢ 0 | |
| 5 | 3 4 | wceq | ⊢ 𝑥 = 0 |
| 6 | clt | ⊢ < | |
| 7 | 3 4 6 | wbr | ⊢ 𝑥 < 0 |
| 8 | c1 | ⊢ 1 | |
| 9 | 8 | cneg | ⊢ - 1 |
| 10 | 7 9 8 | cif | ⊢ if ( 𝑥 < 0 , - 1 , 1 ) |
| 11 | 5 4 10 | cif | ⊢ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) |
| 12 | 1 2 11 | cmpt | ⊢ ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) ) |
| 13 | 0 12 | wceq | ⊢ sgn = ( 𝑥 ∈ ℝ* ↦ if ( 𝑥 = 0 , 0 , if ( 𝑥 < 0 , - 1 , 1 ) ) ) |