let a, b, c, d be positive Real; :: thesis: ( a + b = c + d implies ( (1 / a) + (1 / b) = (1 / c) + (1 / d) iff a * b = c * d ) )
assume A1: a + b = c + d ; :: thesis: ( (1 / a) + (1 / b) = (1 / c) + (1 / d) iff a * b = c * d )
( ((1 / a) * a) * b = 1 * b & ((1 / b) * b) * a = 1 * a & ((1 / c) * c) * d = 1 * d & ((1 / d) * d) * c = 1 * c ) by XCMPLX_1:87;
then ( a + b = ((1 / a) + (1 / b)) * (a * b) & c + d = ((1 / c) + (1 / d)) * (c * d) ) ;
hence ( (1 / a) + (1 / b) = (1 / c) + (1 / d) iff a * b = c * d ) by A1, XCMPLX_1:5; :: thesis: verum