per cases ( a = 0 or a > 0 or a < 0 ) ;
suppose a = 0 ; :: thesis: rsgn a = sgn a
thus rsgn a = sgn a by COMPLEX1:def 1; :: thesis: verum
end;
suppose a > 0 ; :: thesis: rsgn a = sgn a
then reconsider a = a as positive Real ;
Re (director a) = Re ((1 * |.a.|) / |.a.|)
.= Re 1 by XCMPLX_1:89
.= 1 by COMPLEX1:def 1 ;
hence rsgn a = sgn a by ABSVALUE:def 2; :: thesis: verum
end;
suppose a < 0 ; :: thesis: rsgn a = sgn a
then reconsider a = a as negative Real ;
- a = |.a.| by ABSVALUE:def 1;
then Re (director a) = Re (((- 1) * |.a.|) / |.a.|)
.= Re (- 1) by XCMPLX_1:89
.= - 1 by COMPLEX1:def 1
.= sgn a by ABSVALUE:def 2 ;
hence rsgn a = sgn a ; :: thesis: verum
end;
end;