Theorem sgnclre

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

	Ref	Expression
Assertion	sgnclre	$$⊢A\in ℝ\to \mathrm{sgn}\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		neg1rr	$$⊢-1\in ℝ$$
2		0re	$$⊢0\in ℝ$$
3		1re	$$⊢1\in ℝ$$
4		tpssi	$$⊢\left(-1\in ℝ\wedge 0\in ℝ\wedge 1\in ℝ\right)\to \left\{-1,0,1\right\}\subseteq ℝ$$
5	1 2 3 4	mp3an	$$⊢\left\{-1,0,1\right\}\subseteq ℝ$$
6		rexr	$$⊢A\in ℝ\to A\in {ℝ}^{*}$$
7		sgncl	$$⊢A\in {ℝ}^{*}\to \mathrm{sgn}\left(A\right)\in \left\{-1,0,1\right\}$$
8	6 7	syl	$$⊢A\in ℝ\to \mathrm{sgn}\left(A\right)\in \left\{-1,0,1\right\}$$
9	5 8	sselid	$$⊢A\in ℝ\to \mathrm{sgn}\left(A\right)\in ℝ$$