Theorem sgnclre

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

	Ref	Expression
Assertion	sgnclre	|- ( A e. RR -> ( sgn ` A ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		neg1rr	|- -u 1 e. RR
2		0re	|- 0 e. RR
3		1re	|- 1 e. RR
4		tpssi	|- ( ( -u 1 e. RR /\ 0 e. RR /\ 1 e. RR ) -> { -u 1 , 0 , 1 } C_ RR )
5	1 2 3 4	mp3an	|- { -u 1 , 0 , 1 } C_ RR
6		rexr	|- ( A e. RR -> A e. RR* )
7		sgncl	|- ( A e. RR* -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )
8	6 7	syl	|- ( A e. RR -> ( sgn ` A ) e. { -u 1 , 0 , 1 } )
9	5 8	sselid	|- ( A e. RR -> ( sgn ` A ) e. RR )