let a, b be positive Real; :: thesis: 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b)
1 / ((1 / a) + (1 / b)) = 1 / (((1 * b) + (1 * a)) / (a * b)) by XCMPLX_1:116
.= ((a * b) * 1) / (b + a) by XCMPLX_1:77
.= (a * b) / (b + a) ;
then (2 * 1) / ((1 / a) + (1 / b)) = 2 * ((a * b) / (b + a)) by XCMPLX_1:74;
hence 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b) by XCMPLX_1:74; :: thesis: verum