let x be Real; :: thesis: |.x.| = (sgn x) * x
A1: ( 0 < x implies |.x.| = (sgn x) * x )

proof

assume A2: 0 < x ; :: thesis: |.x.| = (sgn x) * x
then (sgn x) * x = 1 * x by ABSVALUE:def 2
.= x ;
hence |.x.| = (sgn x) * x by A2, ABSVALUE:def 1; :: thesis: verum

end;

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

proof

assume A5: x < 0 ; :: thesis: |.x.| = (sgn x) * x
then (sgn x) * x = (- 1) * x by ABSVALUE:def 2
.= - x ;
hence |.x.| = (sgn x) * x by A5, ABSVALUE:def 1; :: thesis: verum

end;

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