let a, b, p, q be Real; :: thesis: ( 1 < p & (1 / p) + (1 / q) = 1 & 0 <= a & 0 <= b implies ( 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) ) ) )
assume that
A1: 1 < p and
A2: (1 / p) + (1 / q) = 1 and
A3: 0 <= a and
A4: 0 <= b ; :: thesis: ( 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) ) )
A5: 0 <= (a to_power p) / p
proof
now :: thesis: ( ( 0 < a & 0 <= (a to_power p) / p ) or ( 0 = a & 0 <= (a to_power p) / p ) )
per cases ( 0 < a or 0 = a ) by A3;
case 0 < a ; :: thesis: 0 <= (a to_power p) / p
then 0 < a to_power p by POWER:34;
hence 0 <= (a to_power p) / p by A1; :: thesis: verum
end;
case 0 = a ; :: thesis: 0 <= (a to_power p) / p
then 0 = a to_power p by A1, POWER:def 2;
hence 0 <= (a to_power p) / p ; :: thesis: verum
end;
end;
end;
hence 0 <= (a to_power p) / p ; :: thesis: verum
end;
reconsider pp = 1 / p as Real ;
1 / p < 1 by A1, XREAL_1:189;
then A6: 1 - 1 < 1 - pp by XREAL_1:15;
then A7: 0 < q by A2;
A8: 0 <= (b to_power q) / q
proof
now :: thesis: ( ( 0 < b & 0 <= (b to_power q) / q ) or ( 0 = b & 0 <= (b to_power q) / q ) )
per cases ( 0 < b or 0 = b ) by A4;
case 0 < b ; :: thesis: 0 <= (b to_power q) / q
then 0 < b to_power q by POWER:34;
hence 0 <= (b to_power q) / q by A7; :: thesis: verum
end;
case 0 = b ; :: thesis: 0 <= (b to_power q) / q
then 0 = b to_power q by A7, POWER:def 2;
hence 0 <= (b to_power q) / q ; :: thesis: verum
end;
end;
end;
hence 0 <= (b to_power q) / q ; :: thesis: verum
end;
now :: thesis: ( ( a * b = 0 & 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) ) ) or ( a * b <> 0 & 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) ) ) )
per cases ( a * b = 0 or a * b <> 0 ) ;
case A9: a * b = 0 ; :: thesis: ( 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) ) )
now :: thesis: ( ( a = 0 & ( 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) ) ) or ( b = 0 & ( 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) ) ) )
per cases ( a = 0 or b = 0 ) by A9, XCMPLX_1:6;
case A10: a = 0 ; :: thesis: ( a * b = ((a to_power p) / p) + ((b to_power q) / q) iff a to_power p = b to_power q )
A11: now :: thesis: ( a * b = ((a to_power p) / p) + ((b to_power q) / q) implies a to_power p = b to_power q )
assume a * b = ((a to_power p) / p) + ((b to_power q) / q) ; :: thesis: a to_power p = b to_power q
then 0 = (0 / p) + ((b to_power q) / q) by A1, A10, POWER:def 2;
then 0 * q = ((b to_power q) / q) * q ;
then 0 = b to_power q by A7, XCMPLX_1:87;
then A12: 0 = (b to_power q) to_power (1 / q) by A2, A6, POWER:def 2;
A13: 0 = b
proof
assume A14: b <> 0 ; :: thesis: contradiction
then 0 = b to_power (q * (1 / q)) by A4, A12, POWER:33;
then 0 = b to_power 1 by A7, XCMPLX_1:106;
hence contradiction by A14, POWER:25; :: thesis: verum
end;
thus a to_power p = 0 by A1, A10, POWER:def 2
.= b to_power q by A7, A13, POWER:def 2 ; :: thesis: verum
end;
now :: thesis: ( a to_power p = b to_power q implies a * b = ((a to_power p) / p) + ((b to_power q) / q) )
assume a to_power p = b to_power q ; :: thesis: a * b = ((a to_power p) / p) + ((b to_power q) / q)
then A15: (b to_power q) / q = 0 / q by A1, A10, POWER:def 2
.= 0 ;
(a to_power p) / p = 0 / p by A1, A10, POWER:def 2
.= 0 ;
hence a * b = ((a to_power p) / p) + ((b to_power q) / q) by A9, A15; :: thesis: verum
end;
hence ( a * b = ((a to_power p) / p) + ((b to_power q) / q) iff a to_power p = b to_power q ) by A11; :: thesis: verum
end;
case A16: b = 0 ; :: thesis: ( a * b = ((a to_power p) / p) + ((b to_power q) / q) iff a to_power p = b to_power q )
A17: 1 / p > 0 by A1, XREAL_1:139;
A18: now :: thesis: ( a * b = ((a to_power p) / p) + ((b to_power q) / q) implies b to_power q = a to_power p )
assume a * b = ((a to_power p) / p) + ((b to_power q) / q) ; :: thesis: b to_power q = a to_power p
then 0 = (0 / q) + ((a to_power p) / p) by A7, A16, POWER:def 2;
then 0 * p = ((a to_power p) / p) * p ;
then 0 = a to_power p by A1, XCMPLX_1:87;
then A19: 0 = (a to_power p) to_power (1 / p) by A17, POWER:def 2;
A20: 0 = a
proof
assume A21: a <> 0 ; :: thesis: contradiction
then 0 = a to_power (p * (1 / p)) by A3, A19, POWER:33;
then 0 = a to_power 1 by A1, XCMPLX_1:106;
hence contradiction by A21, POWER:25; :: thesis: verum
end;
thus b to_power q = 0 by A7, A16, POWER:def 2
.= a to_power p by A1, A20, POWER:def 2 ; :: thesis: verum
end;
now :: thesis: ( a to_power p = b to_power q implies a * b = ((a to_power p) / p) + ((b to_power q) / q) )
assume a to_power p = b to_power q ; :: thesis: a * b = ((a to_power p) / p) + ((b to_power q) / q)
then A22: (a to_power p) / p = 0 / p by A7, A16, POWER:def 2
.= 0 ;
(b to_power q) / q = 0 / q by A7, A16, POWER:def 2
.= 0 ;
hence a * b = ((a to_power p) / p) + ((b to_power q) / q) by A9, A22; :: thesis: verum
end;
hence ( a * b = ((a to_power p) / p) + ((b to_power q) / q) iff a to_power p = b to_power q ) by A18; :: thesis: verum
end;
end;
end;
hence ( 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) ) ) by A5, A8; :: thesis: verum
end;
case A23: a * b <> 0 ; :: thesis: ( 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) ) )
then A24: a <> 0 ;
A25: b <> 0 by A23;
then ( a * b = ((a #R p) / p) + ((b #R q) / q) iff a #R p = b #R q ) by A1, A2, A3, A4, A24, Th4;
then A26: ( a * b = ((a to_power p) / p) + ((b #R q) / q) iff a to_power p = b #R q ) by A3, A24, POWER:def 2;
a * b <= ((a #R p) / p) + ((b #R q) / q) by A1, A2, A3, A4, A24, A25, Th4;
then a * b <= ((a to_power p) / p) + ((b #R q) / q) by A3, A24, POWER:def 2;
hence ( 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) ) ) by A4, A25, A26, POWER:def 2; :: thesis: verum
end;
end;
end;
hence ( 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) ) ) ; :: thesis: verum