let x, y be real number ; :: thesis: ( abs (x + y) = (abs x) + (abs 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 abs (x + y) <> (abs x) + (abs y) )

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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