let a, b, c, d be positive Real; :: thesis: ( a + b >= c + d & a * b < c * d implies (1 / a) + (1 / b) > (1 / c) + (1 / d) )
assume A1: a + b >= c + d ; :: thesis: ( not a * b < c * d or (1 / a) + (1 / b) > (1 / c) + (1 / 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 ( not a * b < c * d or (1 / a) + (1 / b) > (1 / c) + (1 / d) ) by A1, XREAL_1:98; :: thesis: verum