let x, y be Real; :: thesis: ( |.(x + y).| = |.x.| + |.y.| implies 0 <= x * y )
A1: ( not x * y < 0 or ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) )

proof

assume A2: x * y < 0 ; :: thesis: ( ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) )
then ( x <> 0 & y <> 0 ) ;
hence ( ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) ) by A2; :: thesis: verum

end;

A3: ( x < 0 & 0 < y & x + y < 0 implies |.(x + y).| <> |.x.| + |.y.| )

proof

assume that
A4: x < 0 and
A5: 0 < y and
A6: x + y < 0 ; :: thesis: |.(x + y).| <> |.x.| + |.y.|
(- (1 * x)) + (- y) < (- x) + y by A5, XREAL_1:6;
then A7: - (1 * (x + y)) < (- x) + y ;
( |.x.| = - x & |.y.| = y ) by A4, A5, Def1;
hence |.(x + y).| <> |.x.| + |.y.| by A6, A7, Def1; :: thesis: verum

end;

A8: ( 0 < x & y < 0 & x + y < 0 implies |.(x + y).| <> |.x.| + |.y.| )

proof

assume that
A9: 0 < x and
A10: y < 0 and
A11: x + y < 0 ; :: thesis: |.(x + y).| <> |.x.| + |.y.|
(- (1 * x)) + (- y) < x + (- y) by A9, XREAL_1:6;
then A12: - (1 * (x + y)) < x + (- y) ;
( |.x.| = x & |.y.| = - y ) by A9, A10, Def1;
hence |.(x + y).| <> |.x.| + |.y.| by A11, A12, Def1; :: thesis: verum

end;

A13: ( 0 < x & y < 0 & 0 <= x + y implies |.(x + y).| <> |.x.| + |.y.| )

proof

assume that
A14: 0 < x and
A15: y < 0 and
A16: 0 <= x + y ; :: thesis: |.(x + y).| <> |.x.| + |.y.|
A17: |.y.| = - y by A15, Def1;
( x + y < x + (- y) & |.x.| = x ) by A14, A15, Def1, XREAL_1:6;
hence |.(x + y).| <> |.x.| + |.y.| by A16, A17, Def1; :: thesis: verum

end;

A18: ( x < 0 & 0 < y & 0 <= x + y implies |.(x + y).| <> |.x.| + |.y.| )

proof

assume that
A19: x < 0 and
A20: 0 < y and
A21: 0 <= x + y ; :: thesis: |.(x + y).| <> |.x.| + |.y.|
A22: |.y.| = y by A20, Def1;
( x + y < (- x) + y & |.x.| = - x ) by A19, Def1, XREAL_1:6;
hence |.(x + y).| <> |.x.| + |.y.| by A21, A22, Def1; :: thesis: verum

end;

assume ( |.(x + y).| = |.x.| + |.y.| & 0 > x * y ) ; :: thesis: contradiction
hence contradiction by A1, A3, A18, A8, A13; :: thesis: verum