Theorem sgnrn

Description: The range of the signum function. (Contributed by AV, 16-Jun-2026) (Proof shortened by TA, 21-Jun-2026)

	Ref	Expression
Assertion	sgnrn	|- ran sgn = { -u 1 , 0 , 1 }

Proof

Step	Hyp	Ref	Expression
1		df-sgn	|- sgn = ( x e. RR* |-> if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) )
2	1	fnmpt	|- ( A. x e. RR* if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) e. { -u 1 , 0 , 1 } -> sgn Fn RR* )
3		sgnval	|- ( x e. RR* -> ( sgn ` x ) = if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) )
4		sgncl	|- ( x e. RR* -> ( sgn ` x ) e. { -u 1 , 0 , 1 } )
5	3 4	eqeltrrd	|- ( x e. RR* -> if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) e. { -u 1 , 0 , 1 } )
6	2 5	mprg	|- sgn Fn RR*
7	4	rgen	|- A. x e. RR* ( sgn ` x ) e. { -u 1 , 0 , 1 }
8		fnfvrnss	|- ( ( sgn Fn RR* /\ A. x e. RR* ( sgn ` x ) e. { -u 1 , 0 , 1 } ) -> ran sgn C_ { -u 1 , 0 , 1 } )
9	6 7 8	mp2an	|- ran sgn C_ { -u 1 , 0 , 1 }
10		sgnmnf	|- ( sgn ` -oo ) = -u 1
11		mnfxr	|- -oo e. RR*
12		fnfvelrn	|- ( ( sgn Fn RR* /\ -oo e. RR* ) -> ( sgn ` -oo ) e. ran sgn )
13	6 11 12	mp2an	|- ( sgn ` -oo ) e. ran sgn
14	10 13	eqeltrri	|- -u 1 e. ran sgn
15		sgn0	|- ( sgn ` 0 ) = 0
16		0xr	|- 0 e. RR*
17		fnfvelrn	|- ( ( sgn Fn RR* /\ 0 e. RR* ) -> ( sgn ` 0 ) e. ran sgn )
18	6 16 17	mp2an	|- ( sgn ` 0 ) e. ran sgn
19	15 18	eqeltrri	|- 0 e. ran sgn
20		sgn1	|- ( sgn ` 1 ) = 1
21		1xr	|- 1 e. RR*
22		fnfvelrn	|- ( ( sgn Fn RR* /\ 1 e. RR* ) -> ( sgn ` 1 ) e. ran sgn )
23	6 21 22	mp2an	|- ( sgn ` 1 ) e. ran sgn
24	20 23	eqeltrri	|- 1 e. ran sgn
25		tpssi	|- ( ( -u 1 e. ran sgn /\ 0 e. ran sgn /\ 1 e. ran sgn ) -> { -u 1 , 0 , 1 } C_ ran sgn )
26	14 19 24 25	mp3an	|- { -u 1 , 0 , 1 } C_ ran sgn
27	9 26	eqssi	|- ran sgn = { -u 1 , 0 , 1 }