let x, y be real number ; :: thesis: ( 0 <= x * y implies abs (x + y) = (abs x) + (abs y) )
assume A1: 0 <= x * y ; :: thesis: abs (x + y) = (abs x) + (abs y)

per cases ( x * y = 0 or 0 < x * y ) by A1;

suppose A2: x * y = 0 ; :: thesis: abs (x + y) = (abs x) + (abs y)

per cases ( x = 0 or y = 0 ) by A2, XCMPLX_1:6;

suppose A3: x = 0 ; :: thesis: abs (x + y) = (abs x) + (abs y)

then (abs x) + (abs y) = 0 + (abs y) by Def1
.= abs y ;
hence abs (x + y) = (abs x) + (abs y) by A3; :: thesis: verum

end;

suppose A4: y = 0 ; :: thesis: abs (x + y) = (abs x) + (abs y)

then (abs x) + (abs y) = (abs x) + 0 by Def1
.= abs x ;
hence abs (x + y) = (abs x) + (abs y) by A4; :: thesis: verum

end;

end;

end;

suppose A5: 0 < x * y ; :: thesis: abs (x + y) = (abs x) + (abs y)

A6: ( ( x < 0 & y < 0 ) or ( 0 < x & 0 < y ) )

proof

A7: ( x <> 0 & y <> 0 ) by A5;
thus ( ( x < 0 & y < 0 ) or ( 0 < x & 0 < y ) ) by A5, A7; :: thesis: verum

end;

per cases ( ( 0 < x & 0 < y ) or ( x < 0 & y < 0 ) ) by A6;

suppose that A9: 0 < x and
A10: 0 < y ; :: thesis: abs (x + y) = (abs x) + (abs y)

A11: 0 + 0 < x + y by A9, A10;
( abs x = x & abs y = y ) by A9, A10, Def1;
hence abs (x + y) = (abs x) + (abs y) by A11, Def1; :: thesis: verum

end;

suppose that A12: x < 0 and
A13: y < 0 ; :: thesis: abs (x + y) = (abs x) + (abs y)

A14: x + y < 0 + 0 by A12, A13;
abs x = - x by A12, Def1;
then (abs x) + (abs y) = ((- 1) * x) + (- (1 * y)) by A13, Def1
.= - (x + y) ;
hence abs (x + y) = (abs x) + (abs y) by A14, Def1; :: thesis: verum

end;

end;

end;

end;