let x, y be Real; :: thesis: ( 0 <= x * y implies |.(x + y).| = |.x.| + |.y.| )
assume A1: 0 <= x * y ; :: thesis: |.(x + y).| = |.x.| + |.y.|
per cases ( x * y = 0 or 0 < x * y ) by A1;
suppose x * y = 0 ; :: thesis: |.(x + y).| = |.x.| + |.y.|
then ( x = 0 or y = 0 ) by XCMPLX_1:6;
hence |.(x + y).| = |.x.| + |.y.| ; :: thesis: verum
end;
suppose A5: 0 < x * y ; :: thesis: |.(x + y).| = |.x.| + |.y.|
then A6: ( x <> 0 & y <> 0 ) ;
per cases ( ( 0 < x & 0 < y ) or ( x < 0 & y < 0 ) ) by A5, A6;
suppose A7: ( 0 < x & 0 < y ) ; :: thesis: |.(x + y).| = |.x.| + |.y.|
( |.x.| = x & |.y.| = y ) by A7, Def1;
hence |.(x + y).| = |.x.| + |.y.| by A7, Def1; :: thesis: verum
end;
suppose that A8: x < 0 and
A9: y < 0 ; :: thesis: |.(x + y).| = |.x.| + |.y.|
|.x.| = - x by A8, Def1;
then |.x.| + |.y.| = ((- 1) * x) + (- (1 * y)) by A9, Def1
.= - (x + y) ;
hence |.(x + y).| = |.x.| + |.y.| by A8, A9, Def1; :: thesis: verum
end;
end;
end;
end;