theorem :: COMPLEX3:34

for a, b being positive Real holds
( a + b < a * b iff (1 / a) + (1 / b) < 1 )