let a, b be real positive number ; :: 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:117
.= ((a * b) * 1) / (b + a) by XCMPLX_1:78
.= (a * b) / (b + a) ;
then (2 * 1) / ((1 / a) + (1 / b)) = 2 * ((a * b) / (b + a)) by XCMPLX_1:75;
hence 2 / ((1 / a) + (1 / b)) = (2 * (a * b)) / (a + b) by XCMPLX_1:75; :: thesis: verum