Metamath Proof Explorer

Theorem sgndm

Description: The domain of the signum function. (Contributed by AV, 16-Jun-2026)

Ref Expression
Assertion sgndm 
|- dom sgn = RR*

Proof

Step Hyp Ref Expression
1 c0ex 
 |-  0 e. _V
2 negex 
 |-  -u 1 e. _V
3 1ex 
 |-  1 e. _V
4 2 3 ifex 
 |-  if ( x < 0 , -u 1 , 1 ) e. _V
5 1 4 ifex 
 |-  if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) e. _V
6 df-sgn 
 |-  sgn = ( x e. RR* |-> if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) )
7 5 6 dmmpti 
 |-  dom sgn = RR*