Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq1 |
|- ( x = A -> ( x = 0 <-> A = 0 ) ) |
2 |
|
breq1 |
|- ( x = A -> ( x < 0 <-> A < 0 ) ) |
3 |
2
|
ifbid |
|- ( x = A -> if ( x < 0 , -u 1 , 1 ) = if ( A < 0 , -u 1 , 1 ) ) |
4 |
1 3
|
ifbieq2d |
|- ( x = A -> if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) ) |
5 |
|
df-sgn |
|- sgn = ( x e. RR* |-> if ( x = 0 , 0 , if ( x < 0 , -u 1 , 1 ) ) ) |
6 |
|
c0ex |
|- 0 e. _V |
7 |
|
negex |
|- -u 1 e. _V |
8 |
|
1ex |
|- 1 e. _V |
9 |
7 8
|
ifex |
|- if ( A < 0 , -u 1 , 1 ) e. _V |
10 |
6 9
|
ifex |
|- if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) e. _V |
11 |
4 5 10
|
fvmpt |
|- ( A e. RR* -> ( sgn ` A ) = if ( A = 0 , 0 , if ( A < 0 , -u 1 , 1 ) ) ) |