theorem Th5: :: HOLDER_1:5

for a, b, p, q being Real st 1 < p & (1 / p) + (1 / q) = 1 & 0 <= a & 0 <= b holds
( a * b <= ((a to_power p) / p) + ((b to_power q) / q) & ( a * b = ((a to_power p) / p) + ((b to_power q) / q) implies a to_power p = b to_power q ) & ( a to_power p = b to_power q implies a * b = ((a to_power p) / p) + ((b to_power q) / q) ) )