let x, y be Complex; :: thesis: |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|)
A2: ( |.(x * x).| = |.x.| * |.x.| & |.(y * y).| = |.y.| * |.y.| ) by COMPLEX1:65;
|.((((x * x) + (x * y)) + (x * y)) + (y * y)).| <= |.(((x * x) + (x * y)) + (x * y)).| + |.(y * y).| by COMPLEX1:56;
then A3: |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| - |.(y * y).| <= |.(((x * x) + (x * y)) + (x * y)).| by XREAL_1:20;
|.(((x * x) + (x * y)) + (x * y)).| <= |.((x * x) + (x * y)).| + |.(x * y).| by COMPLEX1:56;
then ( |.((x * x) + (x * y)).| <= |.(x * x).| + |.(x * y).| & |.(((x * x) + (x * y)) + (x * y)).| - |.(x * y).| <= |.((x * x) + (x * y)).| ) by COMPLEX1:56, XREAL_1:20;
then |.(((x * x) + (x * y)) + (x * y)).| - |.(x * y).| <= |.(x * x).| + |.(x * y).| by XXREAL_0:2;
then A4: |.(((x * x) + (x * y)) + (x * y)).| <= (|.(x * x).| + |.(x * y).|) + |.(x * y).| by XREAL_1:20;
|.(x + y).| * |.(x + y).| = |.((x + y) * (x + y)).| by COMPLEX1:65
.= |.((((x * x) + (x * y)) + (x * y)) + (y * y)).| ;
then (|.(x + y).| * |.(x + y).|) - |.(y * y).| <= |.(x * x).| + (2 * |.(x * y).|) by A3, A4, XXREAL_0:2;
then A5: ((|.(x + y).| * |.(x + y).|) - |.(y * y).|) - |.(x * x).| <= 2 * |.(x * y).| by XREAL_1:20;
2 * |.(x * y).| <= (|.x.| ^2) + (|.y.| ^2) by Lm20;
then ((|.(x + y).| * |.(x + y).|) - |.(y * y).|) - |.(x * x).| <= (|.x.| ^2) + (|.y.| ^2) by A5, XXREAL_0:2;
then (|.(x + y).| * |.(x + y).|) - (|.y.| * |.y.|) <= ((|.x.| * |.x.|) + (|.y.| * |.y.|)) + (|.x.| * |.x.|) by A2, XREAL_1:20;
then |.(x + y).| * |.(x + y).| <= ((2 * (|.x.| * |.x.|)) + (|.y.| * |.y.|)) + (|.y.| * |.y.|) by XREAL_1:20;
hence |.(x + y).| * |.(x + y).| <= ((2 * |.x.|) * |.x.|) + ((2 * |.y.|) * |.y.|) ; :: thesis: verum

let x, y be Complex; :: thesis: |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|)
|.((x - y) + y).| = |.x.| ;
hence |.x.| * |.x.| <= ((2 * |.(x - y).|) * |.(x - y).|) + ((2 * |.y.|) * |.y.|) by A1; :: thesis: verum