Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Signum (sgn or sign) function - misc. additions
sgnclre
Next ⟩
sgnneg
Metamath Proof Explorer
Ascii
Unicode
Theorem
sgnclre
Description:
Closure of the signum.
(Contributed by
Thierry Arnoux
, 28-Sep-2018)
Ref
Expression
Assertion
sgnclre
⊢
A
∈
ℝ
→
sgn
⁡
A
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
neg1rr
⊢
−
1
∈
ℝ
2
0re
⊢
0
∈
ℝ
3
1re
⊢
1
∈
ℝ
4
tpssi
⊢
−
1
∈
ℝ
∧
0
∈
ℝ
∧
1
∈
ℝ
→
−
1
0
1
⊆
ℝ
5
1
2
3
4
mp3an
⊢
−
1
0
1
⊆
ℝ
6
rexr
⊢
A
∈
ℝ
→
A
∈
ℝ
*
7
sgncl
⊢
A
∈
ℝ
*
→
sgn
⁡
A
∈
−
1
0
1
8
6
7
syl
⊢
A
∈
ℝ
→
sgn
⁡
A
∈
−
1
0
1
9
5
8
sseldi
⊢
A
∈
ℝ
→
sgn
⁡
A
∈
ℝ