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:65;
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:97;
then (x ^2 ) + (y ^2 ) >= 2 * ((sqrt ((abs x) ^2 )) * (sqrt (y ^2 ))) by COMPLEX1:161;
then (x ^2 ) + (y ^2 ) >= 2 * ((sqrt ((abs x) ^2 )) * (sqrt ((abs y) ^2 ))) by COMPLEX1:161;
then (x ^2 ) + (y ^2 ) >= 2 * ((abs x) * (sqrt ((abs y) ^2 ))) by SQUARE_1:89;
then (x ^2 ) + (y ^2 ) >= 2 * ((abs x) * (abs y)) by SQUARE_1:89;
hence (x ^2 ) + (y ^2 ) >= (2 * (abs x)) * (abs y) ; :: thesis: verum