let a, b be real positive number ; :: thesis: (a + b) / 2 <= sqrt (((a ^2 ) + (b ^2 )) / 2)
A2: sqrt 2 > 0 by SQUARE_1:93;
(a ^2 ) + (b ^2 ) >= (2 * a) * b by SERIES_3:6;
then ((a ^2 ) + (b ^2 )) + ((a ^2 ) + (b ^2 )) >= ((2 * a) * b) + ((a ^2 ) + (b ^2 )) by XREAL_1:9;
then sqrt (2 * ((a ^2 ) + (b ^2 ))) >= sqrt ((a + b) ^2 ) by SQUARE_1:94;
then sqrt (2 * ((a ^2 ) + (b ^2 ))) >= a + b by SQUARE_1:89;
then (sqrt (2 * ((a ^2 ) + (b ^2 )))) / (sqrt (2 * 2)) >= (a + b) / 2 by SQUARE_1:85, XREAL_1:74;
then (sqrt (2 * ((a ^2 ) + (b ^2 )))) / ((sqrt 2) * (sqrt 2)) >= (a + b) / 2 by SQUARE_1:97;
then ((sqrt 2) * (sqrt ((a ^2 ) + (b ^2 )))) / ((sqrt 2) * (sqrt 2)) >= (a + b) / 2 by SQUARE_1:97;
then (((sqrt 2) / (sqrt 2)) * (sqrt ((a ^2 ) + (b ^2 )))) / (sqrt 2) >= (a + b) / 2 by XCMPLX_1:84;
then (1 * (sqrt ((a ^2 ) + (b ^2 )))) / (sqrt 2) >= (a + b) / 2 by A2, XCMPLX_1:60;
hence (a + b) / 2 <= sqrt (((a ^2 ) + (b ^2 )) / 2) by SQUARE_1:99; :: thesis: verum