let a, b be positive Real; :: thesis: ( a + b > a * b iff (1 / a) + (1 / b) > 1 )
A1: ( (1 * a) / (a * b) = 1 / b & (1 * b) / (a * b) = 1 / a ) by XCMPLX_1:91;
A2: ( a + b > a * b implies (1 / a) + (1 / b) > 1 )
proof
assume a + b > a * b ; :: thesis: (1 / a) + (1 / b) > 1
then (a + b) / (a * b) > (a * b) / (a * b) by XREAL_1:74;
hence (1 / a) + (1 / b) > 1 by XCMPLX_1:60, A1; :: thesis: verum
end;
( (1 / a) + (1 / b) > 1 implies a + b > a * b )
proof
assume (1 / a) + (1 / b) > 1 ; :: thesis: a + b > a * b
then (a + b) / (a * b) > (a * b) / (a * b) by A1, XCMPLX_1:60;
hence a + b > a * b by XREAL_1:72; :: thesis: verum
end;
hence ( a + b > a * b iff (1 / a) + (1 / b) > 1 ) by A2; :: thesis: verum