let a, b be positive Real; :: thesis: ( a + b < a * b iff (1 / a) + (1 / b) < 1 )
thus ( a + b < a * b implies (1 / a) + (1 / b) < 1 ) :: thesis: ( (1 / a) + (1 / b) < 1 implies a + b < a * b )
proof
( a + b < a * b implies ( (1 / a) + (1 / b) <= 1 & (1 / a) + (1 / b) <> 1 ) ) by SIO, SIL;
hence ( a + b < a * b implies (1 / a) + (1 / b) < 1 ) by XXREAL_0:1; :: thesis: verum
end;
( (1 / a) + (1 / b) < 1 implies ( a + b <= a * b & a + b <> a * b ) ) by SIO, SIL;
hence ( (1 / a) + (1 / b) < 1 implies a + b < a * b ) by XXREAL_0:1; :: thesis: verum