let x, y be real number ; :: thesis: ( abs (x + y) = (abs x) + (abs y) implies 0 <= x * y )
assume that
A1: abs (x + y) = (abs x) + (abs y) and
A2: 0 > x * y ; :: thesis: contradiction
A3: ( not x * y < 0 or ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) )

proof

assume A4: x * y < 0 ; :: thesis: ( ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) )
then A5: ( x <> 0 & y <> 0 ) ;
thus ( ( x < 0 & 0 < y ) or ( 0 < x & y < 0 ) ) by A4, A5; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;

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

proof

assume that
A20: 0 < x and
A21: y < 0 and
A22: x + y < 0 ; :: thesis: abs (x + y) <> (abs x) + (abs y)
(- (1 * x)) + (- y) < x + (- y) by A20, XREAL_1:8;
then A23: - (1 * (x + y)) < x + (- y) ;
A24: abs x = x by A20, Def1;
abs y = - y by A21, Def1;
hence abs (x + y) <> (abs x) + (abs y) by A22, A23, A24, Def1; :: thesis: verum

end;

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

proof

assume that
A25: 0 < x and
A26: y < 0 and
A27: 0 <= x + y ; :: thesis: abs (x + y) <> (abs x) + (abs y)
0 + y < (- y) + 0 by A26;
then A28: x + y < x + (- y) by XREAL_1:8;
A29: abs x = x by A25, Def1;
abs y = - y by A26, Def1;
hence abs (x + y) <> (abs x) + (abs y) by A27, A28, A29, Def1; :: thesis: verum

end;

hence contradiction by A1, A2, A3, A7, A13, A19; :: thesis: verum