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)

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: abs (x + y) = (abs x) + (abs y)

( abs x = x & abs y = y ) by A7, Def1;
hence abs (x + y) = (abs x) + (abs y) by A7, Def1; :: thesis: verum

end;

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

abs x = - x by A8, Def1;
then (abs x) + (abs y) = ((- 1) * x) + (- (1 * y)) by A9, Def1
.= - (x + y) ;
hence abs (x + y) = (abs x) + (abs y) by A8, A9, Def1; :: thesis: verum

end;

end;

end;

end;