Theorem sgnclre

Description: Closure of the signum. (Contributed by Thierry Arnoux, 28-Sep-2018)

	Ref	Expression
Assertion	sgnclre	⊢ ( 𝐴 ∈ ℝ → ( sgn ‘ 𝐴 ) ∈ ℝ )

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	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ* )
7		sgncl	⊢ ( 𝐴 ∈ ℝ* → ( sgn ‘ 𝐴 ) ∈ { - 1 , 0 , 1 } )
8	6 7	syl	⊢ ( 𝐴 ∈ ℝ → ( sgn ‘ 𝐴 ) ∈ { - 1 , 0 , 1 } )
9	5 8	sselid	⊢ ( 𝐴 ∈ ℝ → ( sgn ‘ 𝐴 ) ∈ ℝ )