let p, q, a, b be Real; :: thesis:
assume that
A1: 1 < p and
A2: (1 / p) + (1 / q) = 1 and
A3: 0 < a and
A4: 0 < b ; :: thesis:
reconsider pp = 1 / p as Real ;
1 - pp <> 0 by A1, XREAL_1:191;
then A5: (q " ) " <> 0 by A2;
then (((1 * q) + (1 * p)) / (p * q)) * (p * q) = 1 * (p * q) by A1, A2, XCMPLX_1:117;
then A6: q + p = p * q by A1, A5, XCMPLX_1:6, XCMPLX_1:88;
then A7: ((1 - q) * p) + q = 0 ;
A8: (q - 1) * p = q by A6;
A9: ex g being PartFunc of REAL ,REAL st
( dom g = REAL & ( for x being Real holds
( g . x = (1 / q) - x & ( for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 ) ) ) ) )

proof

defpred S₁[ set ] means $1 in REAL ;
deffunc H₁( Real) -> Element of REAL = (1 / q) - $1;
consider g being PartFunc of REAL ,REAL such that
A10: for d being Element of REAL holds
( d in dom g iff S₁[d] ) and
A11: for d being Element of REAL st d in dom g holds
g /. d = H₁(d) from PARTFUN2:sch 2();
take g ; :: thesis:
A12: dom g = [#] REAL

proof

A13: dom g c= REAL by RELAT_1:def 18;
for x being set st x in REAL holds
x in dom g by A10;
then REAL c= dom g by TARSKI:def 3;
hence dom g = [#] REAL by A13, XBOOLE_0:def 10; :: thesis:

end;

A14: for d being Element of REAL holds g . d = (1 / q) - d

proof

let d be Element of REAL ; :: thesis:
g /. d = (1 / q) - d by A11, A12;
hence g . d = (1 / q) - d by A12, PARTFUN1:def 8; :: thesis:

end;

A15: for d being Real st d in REAL holds
g . d = ((- 1) * d) + (1 / q)

proof

let d be Real; :: thesis:
assume d in REAL ; :: thesis:
thus g . d = (1 / q) - d by A14
.= ((- 1) * d) + (1 / q) ; :: thesis:

end;

then A16: g is_differentiable_on dom g by A12, FDIFF_1:31;
for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 )

proof

let d be Real; :: thesis:
thus g is_differentiable_in d by A12, A16, FDIFF_1:16; :: thesis:
thus diff g,d = (g `| (dom g)) . d by A12, A16, FDIFF_1:def 8
.= - 1 by A12, A15, FDIFF_1:31 ; :: thesis:

end;

hence ( dom g = REAL & ( for x being Real holds
( g . x = (1 / q) - x & ( for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 ) ) ) ) ) by A12, A14; :: thesis:

end;

A17: ex h being PartFunc of REAL ,REAL st
( dom h = right_open_halfline 0 & ( for x being Real st x > 0 holds
( h . x = (x #R p) / p & h is_differentiable_in x & diff h,x = x #R (p - 1) ) ) )

proof

set h = (1 / p) (#) (#R p);
take (1 / p) (#) (#R p) ; :: thesis:
dom (#R p) = right_open_halfline 0 by TAYLOR_1:def 4;
hence A18: dom ((1 / p) (#) (#R p)) = right_open_halfline 0 by VALUED_1:def 5; :: thesis:

now

let x be Real; :: thesis:
assume A19: x > 0 ; :: thesis:
A20: x in right_open_halfline 0

proof

x in { g where g is Real : 0 < g } by A19;
hence x in right_open_halfline 0 by XXREAL_1:230; :: thesis:

end;

hence ((1 / p) (#) (#R p)) . x = (1 / p) * ((#R p) . x) by A18, VALUED_1:def 5
.= (1 / p) * (x #R p) by A20, TAYLOR_1:def 4
.= (x #R p) / p by XCMPLX_1:100 ;
:: thesis:
A21: #R p is_differentiable_in x by A19, TAYLOR_1:21;
hence (1 / p) (#) (#R p) is_differentiable_in x by FDIFF_1:23; :: thesis:
thus diff ((1 / p) (#) (#R p)),x = (1 / p) * (diff (#R p),x) by A21, FDIFF_1:23
.= (1 / p) * (p * (x #R (p - 1))) by A19, TAYLOR_1:21
.= ((1 / p) * p) * (x #R (p - 1))
.= 1 * (x #R (p - 1)) by A1, XCMPLX_1:107
.= x #R (p - 1) ; :: thesis:

end;

hence for x being Real st x > 0 holds
( ((1 / p) (#) (#R p)) . x = (x #R p) / p & (1 / p) (#) (#R p) is_differentiable_in x & diff ((1 / p) (#) (#R p)),x = x #R (p - 1) ) ; :: thesis:

end;

consider g being PartFunc of REAL ,REAL such that
A22: dom g = REAL and
A23: for x being Real holds g . x = (1 / q) - x and
A24: for x being Real holds
( g is_differentiable_in x & diff g,x = - 1 ) by A9;
consider h being PartFunc of REAL ,REAL such that
A25: dom h = right_open_halfline 0 and
A26: for x being Real st x > 0 holds
( h . x = (x #R p) / p & h is_differentiable_in x & diff h,x = x #R (p - 1) ) by A17;
set f = h + g;
A27: dom (h + g) = (right_open_halfline 0 ) /\ REAL by A22, A25, VALUED_1:def 1
.= right_open_halfline 0 by XBOOLE_1:28 ;
A28: for x being Real st x in right_open_halfline 0 holds
( (h + g) . x = (((x #R p) / p) + (1 / q)) - x & h + g is_differentiable_in x & diff (h + g),x = (x #R (p - 1)) - 1 )

proof

let x be Real; :: thesis:
assume A29: x in right_open_halfline 0 ; :: thesis:
x in { y where y is Real : 0 < y } by A29, XXREAL_1:230;
then A30: ex y being Real st
( x = y & 0 < y ) ;
A31: g is_differentiable_in x by A24;
A32: diff g,x = - 1 by A24;
A33: h is_differentiable_in x by A26, A30;
A34: diff h,x = x #R (p - 1) by A26, A30;
thus (h + g) . x = (h . x) + (g . x) by A27, A29, VALUED_1:def 1
.= ((x #R p) / p) + (g . x) by A26, A30
.= ((x #R p) / p) + ((1 / q) - x) by A23
.= (((x #R p) / p) + (1 / q)) - x ; :: thesis:
thus h + g is_differentiable_in x by A31, A33, FDIFF_1:21; :: thesis:
thus diff (h + g),x = (diff h,x) + (diff g,x) by A31, A33, FDIFF_1:21
.= (x #R (p - 1)) - 1 by A32, A34 ; :: thesis:

end;

A35: for x being Real st 0 < x & x <> 1 holds
x < ((x #R p) / p) + (1 / q)

proof

let x be Real; :: thesis:
assume A36: ( 0 < x & x <> 1 ) ; :: thesis:
x in { y where y is Real : 0 < y } by A36;
then A37: x in right_open_halfline 0 by XXREAL_1:230;
for x being Real st x in right_open_halfline 0 holds
h + g is_differentiable_in x by A28;
then A39: h + g is_differentiable_on right_open_halfline 0 by A27, FDIFF_1:16;
1 in { y where y is Real : 0 < y } ;
then 1 in right_open_halfline 0 by XXREAL_1:230;
then A40: (h + g) . 1 = (((1 #R p) / p) + (1 / q)) - 1 by A28
.= ((1 / p) + (1 / q)) - 1 by PREPOWER:87
.= 0 by A2 ;

now

per cases by A36, XXREAL_0:1;

case A41: x < 1 ; :: thesis:

set t = 1 - x;
A42: 1 - 1 < 1 - x by A41, XREAL_1:17;
A43: [.x,(x + (1 - x)).] c= right_open_halfline 0

proof

now

let z be set ; :: thesis:
assume A44: z in [.x,(x + (1 - x)).] ; :: thesis:
z in { r where r is Real : ( x <= r & r <= x + (1 - x) ) } by A44, RCOMP_1:def 1;
then consider r being Real such that
A45: ( r = z & x <= r & r <= x + (1 - x) ) ;
z in { y where y is Real : 0 < y } by A36, A45;
hence z in right_open_halfline 0 by XXREAL_1:230; :: thesis:

end;

hence [.x,(x + (1 - x)).] c= right_open_halfline 0 by TARSKI:def 3; :: thesis:

end;

A46: ].x,(x + (1 - x)).[ c= [.x,(x + (1 - x)).] by XXREAL_1:25;
X: right_open_halfline 0 c= dom (h + g) by A27;
(h + g) | (right_open_halfline 0 ) is continuous by A39, FDIFF_1:33;
then A47: (h + g) | [.x,(x + (1 - x)).] is continuous by A43, FCONT_1:17;
Y: [.x,(x + (1 - x)).] c= dom (h + g) by X, A43, XBOOLE_1:1;
h + g is_differentiable_on ].x,(x + (1 - x)).[ by A39, A43, A46, FDIFF_1:34, XBOOLE_1:1;
then consider s being Real such that
A48: 0 < s and
A49: s < 1 and
A50: (h + g) . (x + (1 - x)) = ((h + g) . x) + ((1 - x) * (diff (h + g),(x + (s * (1 - x))))) by A42, A47, Y, ROLLE:4;
0 * (1 - x) < s * (1 - x) by A42, A48, XREAL_1:70;
then A51: 0 + 0 < x + (s * (1 - x)) by A36;
s * (1 - x) < 1 * (1 - x) by A42, A49, XREAL_1:70;
then A52: x + (s * (1 - x)) < x + (1 - x) by XREAL_1:10;
x + (s * (1 - x)) in right_open_halfline 0

proof

x + (s * (1 - x)) in { y where y is Real : 0 < y } by A51;
hence x + (s * (1 - x)) in right_open_halfline 0 by XXREAL_1:230; :: thesis:

end;

then A53: diff (h + g),(x + (s * (1 - x))) = ((x + (s * (1 - x))) #R (p - 1)) - 1 by A28;
1 - 1 < p - 1 by A1, XREAL_1:16;
then (x + (s * (1 - x))) to_power (p - 1) < (x + (s * (1 - x))) to_power 0 by A51, A52, POWER:45;
then (x + (s * (1 - x))) #R (p - 1) < (x + (s * (1 - x))) to_power 0 by A51, POWER:def 2;
then (x + (s * (1 - x))) #R (p - 1) < (x + (s * (1 - x))) #R 0 by A51, POWER:def 2;
then (x + (s * (1 - x))) #R (p - 1) < 1 by A51, PREPOWER:85;
then ((x + (s * (1 - x))) #R (p - 1)) - 1 < 1 - 1 by XREAL_1:16;
then (1 - x) * (diff (h + g),(x + (s * (1 - x)))) < (1 - x) * 0 by A42, A53, XREAL_1:70;
then ((h + g) . x) + ((1 - x) * (diff (h + g),(x + (s * (1 - x))))) < ((h + g) . x) + 0 by XREAL_1:10;
then 0 < (((x #R p) / p) + (1 / q)) - x by A28, A37, A40, A50;
then 0 + x < ((((x #R p) / p) + (1 / q)) - x) + x by XREAL_1:10;
hence x < ((x #R p) / p) + (1 / q) ; :: thesis:

end;

case A54: x > 1 ; :: thesis:

set t = x - 1;
A55: 1 - 1 < x - 1 by A54, XREAL_1:16;
A56: [.1,(1 + (x - 1)).] c= right_open_halfline 0

proof

now

let z be set ; :: thesis:
assume A57: z in [.1,(1 + (x - 1)).] ; :: thesis:
z in { r where r is Real : ( 1 <= r & r <= 1 + (x - 1) ) } by A57, RCOMP_1:def 1;
then consider r being Real such that
A58: ( r = z & 1 <= r & r <= 1 + (x - 1) ) ;
z in { y where y is Real : 0 < y } by A58;
hence z in right_open_halfline 0 by XXREAL_1:230; :: thesis:

end;

hence [.1,(1 + (x - 1)).] c= right_open_halfline 0 by TARSKI:def 3; :: thesis:

end;

A59: ].1,(1 + (x - 1)).[ c= [.1,(1 + (x - 1)).] by XXREAL_1:25;
X: right_open_halfline 0 c= dom (h + g) by A27;
(h + g) | (right_open_halfline 0 ) is continuous by A39, FDIFF_1:33;
then A60: (h + g) | [.1,(1 + (x - 1)).] is continuous by A56, FCONT_1:17;
Y: [.1,(1 + (x - 1)).] c= dom (h + g) by X, A56, XBOOLE_1:1;
h + g is_differentiable_on ].1,(1 + (x - 1)).[ by A39, A56, A59, FDIFF_1:34, XBOOLE_1:1;
then consider s being Real such that
A61: 0 < s and
s < 1 and
A62: (h + g) . (1 + (x - 1)) = ((h + g) . 1) + ((x - 1) * (diff (h + g),(1 + (s * (x - 1))))) by A55, A60, Y, ROLLE:4;
A63: 0 * (x - 1) < s * (x - 1) by A55, A61, XREAL_1:70;
then A64: 0 + 0 < 1 + (s * (x - 1)) ;
A65: 1 + (s * (x - 1)) in right_open_halfline 0

proof

1 + (s * (x - 1)) in { y where y is Real : 0 < y } by A64;
hence 1 + (s * (x - 1)) in right_open_halfline 0 by XXREAL_1:230; :: thesis:

end;

A66: 1 + 0 < 1 + (s * (x - 1)) by A63, XREAL_1:10;
A67: diff (h + g),(1 + (s * (x - 1))) = ((1 + (s * (x - 1))) #R (p - 1)) - 1 by A28, A65;
1 - 1 < p - 1 by A1, XREAL_1:16;
then 1 < (1 + (s * (x - 1))) #R (p - 1) by A66, PREPOWER:100;
then 1 - 1 < ((1 + (s * (x - 1))) #R (p - 1)) - 1 by XREAL_1:16;
then (x - 1) * 0 < (x - 1) * (diff (h + g),(1 + (s * (x - 1)))) by A55, A67, XREAL_1:70;
then 0 < (((x #R p) / p) + (1 / q)) - x by A28, A37, A40, A62;
then 0 + x < ((((x #R p) / p) + (1 / q)) - x) + x by XREAL_1:10;
hence x < ((x #R p) / p) + (1 / q) ; :: thesis:

end;

hence x < ((x #R p) / p) + (1 / q) ; :: thesis:

end;

A68: 0 < b #R (1 - q) by A4, PREPOWER:95;
then A69: 0 * (b #R (1 - q)) < a * (b #R (1 - q)) by A3, XREAL_1:70;
A70: 0 < b #R q by A4, PREPOWER:95;
a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q)

proof

now

per cases ;

case a * (b #R (1 - q)) = 1 ; :: thesis:

hence a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A2, PREPOWER:87; :: thesis:

end;

case a * (b #R (1 - q)) <> 1 ; :: thesis:

hence a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A35, A69; :: thesis:

end;

hence a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q) ; :: thesis:

end;

then (a * (b #R (1 - q))) * (b #R q) <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A70, XREAL_1:66;
then a * ((b #R (1 - q)) * (b #R q)) <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) ;
then a * (b #R ((1 - q) + q)) <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:89;
then a * b <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:86;
then a * b <= ((((a #R p) * ((b #R (1 - q)) #R p)) / p) + (1 / q)) * (b #R q) by A3, A68, PREPOWER:92;
then a * b <= ((((a #R p) * (b #R ((1 - q) * p))) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:105;
then a * b <= ((((a #R p) * (b #R ((1 - q) * p))) / p) * (b #R q)) + ((1 / q) * (b #R q)) ;
then a * b <= (((a #R p) * ((b #R ((1 - q) * p)) / p)) * (b #R q)) + ((1 / q) * (b #R q)) by XCMPLX_1:75;
then a * b <= ((a #R p) * (((b #R ((1 - q) * p)) / p) * (b #R q))) + ((1 / q) * (b #R q)) ;
then a * b <= ((a #R p) * (((b #R ((1 - q) * p)) * (b #R q)) / p)) + ((1 / q) * (b #R q)) by XCMPLX_1:75;
then a * b <= ((a #R p) * ((b #R (((1 - q) * p) + q)) / p)) + ((1 / q) * (b #R q)) by A4, PREPOWER:89;
then a * b <= ((a #R p) * (1 / p)) + ((1 / q) * (b #R q)) by A4, A6, PREPOWER:85;
then A71: a * b <= ((a #R p) / p) + ((1 / q) * (b #R q)) by XCMPLX_1:100;
( a * b = ((a #R p) / p) + ((b #R q) / q) iff a #R p = b #R q )

proof

A72: now

assume a * b = ((a #R p) / p) + ((b #R q) / q) ; :: thesis:
then a * b = ((a #R p) / p) + ((1 / q) * (b #R q)) by XCMPLX_1:100;
then a * b = ((a #R p) * (1 / p)) + ((1 / q) * (b #R q)) by XCMPLX_1:100;
then a * b = ((a #R p) * ((b #R 0 ) / p)) + ((1 / q) * (b #R q)) by A4, PREPOWER:85;
then a * b = ((a #R p) * (((b #R ((1 - q) * p)) * (b #R q)) / p)) + ((1 / q) * (b #R q)) by A4, A7, PREPOWER:89;
then a * b = ((a #R p) * (((b #R ((1 - q) * p)) / p) * (b #R q))) + ((1 / q) * (b #R q)) by XCMPLX_1:75;
then a * b = (((a #R p) * ((b #R ((1 - q) * p)) / p)) * (b #R q)) + ((1 / q) * (b #R q)) ;
then a * b = ((((a #R p) * (b #R ((1 - q) * p))) / p) * (b #R q)) + ((1 / q) * (b #R q)) by XCMPLX_1:75;
then a * b = ((((a #R p) * (b #R ((1 - q) * p))) / p) + (1 / q)) * (b #R q) ;
then a * b = ((((a #R p) * ((b #R (1 - q)) #R p)) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:105;
then a * b = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A3, A68, PREPOWER:92;
then a * (b #R ((1 - q) + q)) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:86;
then a * ((b #R (1 - q)) * (b #R q)) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:89;
then (a * (b #R (1 - q))) * (b #R q) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) ;
then A73: a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A70, XCMPLX_1:5;
a * ((b #R (1 - q)) * (b #R (q - 1))) = (a * (b #R (1 - q))) * (b #R (q - 1))
.= 1 * (b #R (q - 1)) by A35, A69, A73 ;
then a * (b #R ((1 - q) + (q - 1))) = b #R (q - 1) by A4, PREPOWER:89;
then a * 1 = b #R (q - 1) by A4, PREPOWER:85;
hence a #R p = b #R q by A4, A8, PREPOWER:105; :: thesis:

end;

A74: 0 < b #R (q - 1) by A4, PREPOWER:95;

now

assume A75: a #R p = b #R q ; :: thesis:
then A76: a #R p = (b #R (q - 1)) #R p by A4, A8, PREPOWER:105;
a = a #R 1 by A3, PREPOWER:86
.= a #R (p * (1 / p)) by A1, XCMPLX_1:107
.= (a #R p) #R (1 / p) by A3, PREPOWER:105
.= (b #R (q - 1)) #R (p * (1 / p)) by A4, A76, PREPOWER:95, PREPOWER:105
.= (b #R (q - 1)) #R 1 by A1, XCMPLX_1:107
.= b #R (q - 1) by A4, PREPOWER:86, PREPOWER:95 ;
then a * 1 = b #R (q - 1) ;
then a * (b #R ((1 - q) + (q - 1))) = b #R (q - 1) by A4, PREPOWER:85;
then a * ((b #R (1 - q)) * (b #R (q - 1))) = 1 * (b #R (q - 1)) by A4, PREPOWER:89;
then A77: (a * (b #R (1 - q))) * (b #R (q - 1)) = 1 * (b #R (q - 1)) ;
thus ((a #R p) / p) + ((b #R q) / q) = ((b #R q) * (1 / p)) + ((b #R q) / q) by A75, XCMPLX_1:100
.= ((b #R q) * (1 / p)) + ((b #R q) * (1 / q)) by XCMPLX_1:100
.= (b #R q) * ((1 / p) + (1 / q))
.= (b #R q) * (a * (b #R (1 - q))) by A2, A74, A77, XCMPLX_1:5
.= a * ((b #R (1 - q)) * (b #R q))
.= a * (b #R ((1 - q) + q)) by A4, PREPOWER:89
.= a * b by A4, PREPOWER:86 ; :: thesis:

end;

hence ( a * b = ((a #R p) / p) + ((b #R q) / q) iff a #R p = b #R q ) by A72; :: thesis:

end;

hence ( a * b <= ((a #R p) / p) + ((b #R q) / q) & ( a * b = ((a #R p) / p) + ((b #R q) / q) implies a #R p = b #R q ) & ( a #R p = b #R q implies a * b = ((a #R p) / p) + ((b #R q) / q) ) ) by A71, XCMPLX_1:100; :: thesis: