let x be Real; :: thesis: x = |.x.| * (sgn x)

A1: ( 0 < x implies x = |.x.| * (sgn x) )

hence x = |.x.| * (sgn x) by A1, A3; :: thesis: verum

A1: ( 0 < x implies x = |.x.| * (sgn x) )

proof

A3:
( x < 0 implies x = |.x.| * (sgn x) )
assume A2:
0 < x
; :: thesis: x = |.x.| * (sgn x)

then |.x.| = x by Def1;

then |.x.| * (sgn x) = x * 1 by A2, Def2;

hence x = |.x.| * (sgn x) ; :: thesis: verum

end;then |.x.| = x by Def1;

then |.x.| * (sgn x) = x * 1 by A2, Def2;

hence x = |.x.| * (sgn x) ; :: thesis: verum

proof

( x = 0 implies x = |.x.| * (sgn x) )
;
assume A4:
x < 0
; :: thesis: x = |.x.| * (sgn x)

then |.x.| = - x by Def1;

then |.x.| * (sgn x) = (- x) * (- 1) by A4, Def2

.= x ;

hence x = |.x.| * (sgn x) ; :: thesis: verum

end;then |.x.| = - x by Def1;

then |.x.| * (sgn x) = (- x) * (- 1) by A4, Def2

.= x ;

hence x = |.x.| * (sgn x) ; :: thesis: verum

hence x = |.x.| * (sgn x) by A1, A3; :: thesis: verum