let x, y be real number ; :: thesis: (x ^2) + (y ^2) >= (2 * (abs x)) * (abs 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 ((abs x) ^2)) * (sqrt (y ^2))) by COMPLEX1:75;
then (x ^2) + (y ^2) >= 2 * ((sqrt ((abs x) ^2)) * (sqrt ((abs y) ^2))) by COMPLEX1:75;
then (x ^2) + (y ^2) >= 2 * ((abs x) * (sqrt ((abs y) ^2))) by SQUARE_1:22;
then (x ^2) + (y ^2) >= 2 * ((abs x) * (abs y)) by SQUARE_1:22;
hence (x ^2) + (y ^2) >= (2 * (abs x)) * (abs y) ; :: thesis: verum