Description: The signum of 1 is 1. (Contributed by David A. Wheeler, 26-Jun-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | sgn1 | ⊢ ( sgn ‘ 1 ) = 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1xr | ⊢ 1 ∈ ℝ* | |
2 | 0lt1 | ⊢ 0 < 1 | |
3 | sgnp | ⊢ ( ( 1 ∈ ℝ* ∧ 0 < 1 ) → ( sgn ‘ 1 ) = 1 ) | |
4 | 1 2 3 | mp2an | ⊢ ( sgn ‘ 1 ) = 1 |