let x, y be Real; :: thesis: (x ^2) + (y ^2) >= (2 * |.x.|) * |.y.|
A1: ( x ^2 >= 0 & y ^2 >= 0 ) by XREAL_1:63;
then (x ^2) + (y ^2) >= 2 * (sqrt ((x ^2) * (y ^2))) by SIN_COS2:1;
then (x ^2) + (y ^2) >= 2 * ((sqrt (x ^2)) * (sqrt (y ^2))) by A1, SQUARE_1:29;
then (x ^2) + (y ^2) >= 2 * ((sqrt (|.x.| ^2)) * (sqrt (y ^2))) by COMPLEX1:75;
then (x ^2) + (y ^2) >= 2 * ((sqrt (|.x.| ^2)) * (sqrt (|.y.| ^2))) by COMPLEX1:75;
then (x ^2) + (y ^2) >= 2 * (|.x.| * (sqrt (|.y.| ^2))) by SQUARE_1:22;
then (x ^2) + (y ^2) >= 2 * (|.x.| * |.y.|) by SQUARE_1:22;
hence (x ^2) + (y ^2) >= (2 * |.x.|) * |.y.| ; :: thesis: verum