let a, b be positive Real; :: thesis: 2 / ((1 / a) + (1 / b)) <= sqrt (a * b)
A1: sqrt (a * b) > 0 by SQUARE_1:25;
then (2 * (sqrt (a * b))) / (a + b) <= 1 by SIN_COS2:1, XREAL_1:183;
then ((2 * (sqrt (a * b))) / (a + b)) * (sqrt (a * b)) <= 1 * (sqrt (a * b)) by A1, XREAL_1:64;
then (2 * (sqrt (a * b))) / ((a + b) / (sqrt (a * b))) <= sqrt (a * b) by XCMPLX_1:82;
then ((2 * (sqrt (a * b))) * (sqrt (a * b))) / (a + b) <= sqrt (a * b) by XCMPLX_1:77;
then (2 * ((sqrt (a * b)) ^2)) / (a + b) <= sqrt (a * b) ;
then (2 * (a * b)) / (a + b) <= sqrt (a * b) by SQUARE_1:def 2;
hence 2 / ((1 / a) + (1 / b)) <= sqrt (a * b) by Lm2; :: thesis: verum