let a, b, p, q be Real; :: thesis: ( 1 < p & (1 / p) + (1 / q) = 1 & 0 < a & 0 < b implies ( 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) ) ) )
assume that
A1: 1 < p and
A2: (1 / p) + (1 / q) = 1 and
A3: 0 < a and
A4: 0 < b ; :: thesis: ( 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) ) )
A5: 0 < b #R q by A4, PREPOWER:81;
reconsider pp = 1 / p as Real ;
1 - pp <> 0 by A1, XREAL_1:189;
then A6: (q ") " <> 0 by A2;
then (((1 * q) + (1 * p)) / (p * q)) * (p * q) = 1 * (p * q) by A1, A2, XCMPLX_1:116;
then A7: q + p = p * q by A1, A6, XCMPLX_1:6, XCMPLX_1:87;
then A8: (q - 1) * p = q ;
A9: 0 < b #R (q - 1) by A4, PREPOWER:81;
A10: now :: thesis: ( a #R p = b #R q implies ((a #R p) / p) + ((b #R q) / q) = a * b )
assume A11: a #R p = b #R q ; :: thesis: ((a #R p) / p) + ((b #R q) / q) = a * b
then A12: a #R p = (b #R (q - 1)) #R p by A4, A8, PREPOWER:91;
a = a #R 1 by A3, PREPOWER:72
.= a #R (p * (1 / p)) by A1, XCMPLX_1:106
.= (a #R p) #R (1 / p) by A3, PREPOWER:91
.= (b #R (q - 1)) #R (p * (1 / p)) by A4, A12, PREPOWER:81, PREPOWER:91
.= (b #R (q - 1)) #R 1 by A1, XCMPLX_1:106
.= b #R (q - 1) by A4, PREPOWER:72, PREPOWER:81 ;
then a * 1 = b #R (q - 1) ;
then a * (b #R ((1 - q) + (q - 1))) = b #R (q - 1) by A4, PREPOWER:71;
then a * ((b #R (1 - q)) * (b #R (q - 1))) = 1 * (b #R (q - 1)) by A4, PREPOWER:75;
then A13: (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 A11, XCMPLX_1:99
.= ((b #R q) * (1 / p)) + ((b #R q) * (1 / q)) by XCMPLX_1:99
.= (b #R q) * ((1 / p) + (1 / q))
.= (b #R q) * (a * (b #R (1 - q))) by A2, A9, A13, XCMPLX_1:5
.= a * ((b #R (1 - q)) * (b #R q))
.= a * (b #R ((1 - q) + q)) by A4, PREPOWER:75
.= a * b by A4, PREPOWER:72 ; :: thesis: verum
end;
A14: 0 < b #R (1 - q) by A4, PREPOWER:81;
then A15: 0 * (b #R (1 - q)) < a * (b #R (1 - q)) by A3, XREAL_1:68;
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 ((1 / p) (#) (#R p)) = right_open_halfline 0 & ( 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) ) ) )
dom (#R p) = right_open_halfline 0 by TAYLOR_1:def 4;
hence A16: dom ((1 / p) (#) (#R p)) = right_open_halfline 0 by VALUED_1:def 5; :: thesis: 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) )
now :: thesis: 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) )
let x be Real; :: thesis: ( x > 0 implies ( ((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) ) )
assume A17: x > 0 ; :: thesis: ( ((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) )
x in { g where g is Real : 0 < g } by A17;
then A18: x in right_open_halfline 0 by XXREAL_1:230;
hence ((1 / p) (#) (#R p)) . x = (1 / p) * ((#R p) . x) by A16, VALUED_1:def 5
.= (1 / p) * (x #R p) by A18, TAYLOR_1:def 4
.= (x #R p) / p by XCMPLX_1:99 ;
:: thesis: ( (1 / p) (#) (#R p) is_differentiable_in x & diff (((1 / p) (#) (#R p)),x) = x #R (p - 1) )
A19: #R p is_differentiable_in x by A17, TAYLOR_1:21;
hence (1 / p) (#) (#R p) is_differentiable_in x by FDIFF_1:15; :: thesis: diff (((1 / p) (#) (#R p)),x) = x #R (p - 1)
thus diff (((1 / p) (#) (#R p)),x) = (1 / p) * (diff ((#R p),x)) by A19, FDIFF_1:15
.= (1 / p) * (p * (x #R (p - 1))) by A17, TAYLOR_1:21
.= ((1 / p) * p) * (x #R (p - 1))
.= 1 * (x #R (p - 1)) by A1, XCMPLX_1:106
.= x #R (p - 1) ; :: thesis: verum
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: verum
end;
then consider h being PartFunc of REAL,REAL such that
A20: dom h = right_open_halfline 0 and
A21: 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) ) ;
ex g being PartFunc of REAL,REAL st
( dom g = REAL & ( for x being Element of REAL holds
( g . x = (1 / q) - x & g is_differentiable_in x & diff (g,x) = - 1 ) ) )
proof
deffunc H1( Real) -> Element of REAL = In (((1 / q) - $1),REAL);
defpred S1[ set ] means $1 in REAL ;
consider g being PartFunc of REAL,REAL such that
A22: for d being Element of REAL holds
( d in dom g iff S1[d] ) and
A23: for d being Element of REAL st d in dom g holds
g /. d = H1(d) from PARTFUN2:sch 2();
 take g ; :: thesis: ( dom g = REAL & ( for x being Element of REAL holds
( g . x = (1 / q) - x & g is_differentiable_in x & diff (g,x) = - 1 ) ) )
for x being object st x in REAL holds
x in dom g by A22;
then A24: ( dom g c= REAL & REAL c= dom g ) by RELAT_1:def 18;
then A25: dom g = [#] REAL by XBOOLE_0:def 10;
A26: 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
g /. d = H1(d) by A23, A25;
hence g . d = (1 / q) - d by A25, PARTFUN1:def 6; :: thesis: verum
end;
A27: for d being Real st d in REAL holds
g . d = ((- 1) * d) + (1 / q)
proof
let d be Real; :: thesis: ( d in REAL implies g . d = ((- 1) * d) + (1 / q) )
assume A28: d in REAL ; :: thesis: g . d = ((- 1) * d) + (1 / q)
thus g . d = (1 / q) - d by A26, A28
.= ((- 1) * d) + (1 / q) ; :: thesis: verum
end;
then A29: g is_differentiable_on dom g by A25, FDIFF_1:23;
for x being Element of REAL holds
( g is_differentiable_in x & diff (g,x) = - 1 )
proof
let d be Element of REAL ; :: thesis: ( g is_differentiable_in d & diff (g,d) = - 1 )
thus g is_differentiable_in d by A25, A29, FDIFF_1:9; :: thesis: diff (g,d) = - 1
thus diff (g,d) = (g `| (dom g)) . d by A25, A29, FDIFF_1:def 7
.= - 1 by A25, A27, FDIFF_1:23 ; :: thesis: verum
end;
hence ( dom g = REAL & ( for x being Element of REAL holds
( g . x = (1 / q) - x & g is_differentiable_in x & diff (g,x) = - 1 ) ) ) by A24, A26, XBOOLE_0:def 10; :: thesis: verum
end;
then consider g being PartFunc of REAL,REAL such that
A30: dom g = REAL and
A31: for x being Element of REAL holds g . x = (1 / q) - x and
A32: for x being Element of REAL holds
( g is_differentiable_in x & diff (g,x) = - 1 ) ;
set f = h + g;
A33: dom (h + g) = (right_open_halfline 0) /\ REAL by A30, A20, VALUED_1:def 1
.= right_open_halfline 0 by XBOOLE_1:28 ;
A34: 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: ( x in right_open_halfline 0 implies ( (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 ) )
assume A35: x in right_open_halfline 0 ; :: thesis: ( (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 )
reconsider xx = x as Element of REAL by XREAL_0:def 1;
x in { y where y is Real : 0 < y } by A35, XXREAL_1:230;
then A36: ex y being Real st
( x = y & 0 < y ) ;
then A37: diff (h,x) = x #R (p - 1) by A21;
thus (h + g) . x = (h . x) + (g . x) by A33, A35, VALUED_1:def 1
.= ((x #R p) / p) + (g . xx) by A21, A36
.= ((x #R p) / p) + ((1 / q) - x) by A31
.= (((x #R p) / p) + (1 / q)) - x ; :: thesis: ( h + g is_differentiable_in x & diff ((h + g),x) = (x #R (p - 1)) - 1 )
A38: g is_differentiable_in xx by A32;
A39: h is_differentiable_in x by A21, A36;
hence h + g is_differentiable_in x by A38, FDIFF_1:13; :: thesis: diff ((h + g),x) = (x #R (p - 1)) - 1
A40: diff (g,xx) = - 1 by A32;
thus diff ((h + g),x) = (diff (h,x)) + (diff (g,x)) by A38, A39, FDIFF_1:13
.= (x #R (p - 1)) - 1 by A40, A37 ; :: thesis: verum
end;
A41: for x being Real st 0 < x & x <> 1 holds
x < ((x #R p) / p) + (1 / q)
proof
1 in { y where y is Real : 0 < y } ;
then 1 in right_open_halfline 0 by XXREAL_1:230;
then A42: (h + g) . 1 = (((1 #R p) / p) + (1 / q)) - 1 by A34
.= ((1 / p) + (1 / q)) - 1 by PREPOWER:73
.= 0 by A2 ;
for x being Real st x in right_open_halfline 0 holds
h + g is_differentiable_in x by A34;
then A43: h + g is_differentiable_on right_open_halfline 0 by A33, FDIFF_1:9;
let x be Real; :: thesis: ( 0 < x & x <> 1 implies x < ((x #R p) / p) + (1 / q) )
assume that
A44: 0 < x and
A45: x <> 1 ; :: thesis: x < ((x #R p) / p) + (1 / q)
x in { y where y is Real : 0 < y } by A44;
then A46: x in right_open_halfline 0 by XXREAL_1:230;
now :: thesis: ( ( x < 1 & x < ((x #R p) / p) + (1 / q) ) or ( x > 1 & x < ((x #R p) / p) + (1 / q) ) )
per cases ( x < 1 or x > 1 ) by A45, XXREAL_0:1;
case x < 1 ; :: thesis: x < ((x #R p) / p) + (1 / q)
then A47: 1 - 1 < 1 - x by XREAL_1:15;
set t = 1 - x;
A48: 1 - 1 < p - 1 by A1, XREAL_1:14;
now :: thesis: for z being object st z in [.x,(x + (1 - x)).] holds
z in right_open_halfline 0
let z be object ; :: thesis: ( z in [.x,(x + (1 - x)).] implies z in right_open_halfline 0 )
assume z in [.x,(x + (1 - x)).] ; :: thesis: z in right_open_halfline 0
then z in { r where r is Real : ( x <= r & r <= x + (1 - x) ) } by RCOMP_1:def 1;
then ex r being Real st
( r = z & x <= r & r <= x + (1 - x) ) ;
then z in { y where y is Real : 0 < y } by A44;
hence z in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum
end;
then A49: [.x,(x + (1 - x)).] c= right_open_halfline 0 ;
(h + g) | (right_open_halfline 0) is continuous by A43, FDIFF_1:25;
then A50: (h + g) | [.x,(x + (1 - x)).] is continuous by A49, FCONT_1:16;
].x,(x + (1 - x)).[ c= [.x,(x + (1 - x)).] by XXREAL_1:25;
then h + g is_differentiable_on ].x,(x + (1 - x)).[ by A43, A49, FDIFF_1:26, XBOOLE_1:1;
then consider s being Real such that
A51: 0 < s and
A52: s < 1 and
A53: (h + g) . (x + (1 - x)) = ((h + g) . x) + ((1 - x) * (diff ((h + g),(x + (s * (1 - x)))))) by A33, A47, A49, A50, ROLLE:4;
s * (1 - x) < 1 * (1 - x) by A47, A52, XREAL_1:68;
then x + (s * (1 - x)) < x + (1 - x) by XREAL_1:8;
then (x + (s * (1 - x))) to_power (p - 1) < (x + (s * (1 - x))) to_power 0 by A44, A47, A51, A48, POWER:40;
then (x + (s * (1 - x))) #R (p - 1) < (x + (s * (1 - x))) to_power 0 by A44, A47, A51, POWER:def 2;
then (x + (s * (1 - x))) #R (p - 1) < (x + (s * (1 - x))) #R 0 by A44, A47, A51, POWER:def 2;
then (x + (s * (1 - x))) #R (p - 1) < 1 by A44, A47, A51, PREPOWER:71;
then A54: ((x + (s * (1 - x))) #R (p - 1)) - 1 < 1 - 1 by XREAL_1:14;
x + (s * (1 - x)) in { y where y is Real : 0 < y } by A44, A47, A51;
then x + (s * (1 - x)) in right_open_halfline 0 by XXREAL_1:230;
then diff ((h + g),(x + (s * (1 - x)))) = ((x + (s * (1 - x))) #R (p - 1)) - 1 by A34;
then (1 - x) * (diff ((h + g),(x + (s * (1 - x))))) < (1 - x) * 0 by A47, A54, XREAL_1:68;
then ((h + g) . x) + ((1 - x) * (diff ((h + g),(x + (s * (1 - x)))))) < ((h + g) . x) + 0 by XREAL_1:8;
then 0 < (((x #R p) / p) + (1 / q)) - x by A34, A46, A42, A53;
then 0 + x < ((((x #R p) / p) + (1 / q)) - x) + x by XREAL_1:8;
hence x < ((x #R p) / p) + (1 / q) ; :: thesis: verum
end;
case x > 1 ; :: thesis: x < ((x #R p) / p) + (1 / q)
then A55: 1 - 1 < x - 1 by XREAL_1:14;
set t = x - 1;
now :: thesis: for z being object st z in [.1,(1 + (x - 1)).] holds
z in right_open_halfline 0
let z be object ; :: thesis: ( z in [.1,(1 + (x - 1)).] implies z in right_open_halfline 0 )
assume z in [.1,(1 + (x - 1)).] ; :: thesis: z in right_open_halfline 0
then z in { r where r is Real : ( 1 <= r & r <= 1 + (x - 1) ) } by RCOMP_1:def 1;
then ex r being Real st
( r = z & 1 <= r & r <= 1 + (x - 1) ) ;
then z in { y where y is Real : 0 < y } ;
hence z in right_open_halfline 0 by XXREAL_1:230; :: thesis: verum
end;
then A56: [.1,(1 + (x - 1)).] c= right_open_halfline 0 ;
A57: 1 - 1 < p - 1 by A1, XREAL_1:14;
(h + g) | (right_open_halfline 0) is continuous by A43, FDIFF_1:25;
then A58: (h + g) | [.1,(1 + (x - 1)).] is continuous by A56, FCONT_1:16;
].1,(1 + (x - 1)).[ c= [.1,(1 + (x - 1)).] by XXREAL_1:25;
then h + g is_differentiable_on ].1,(1 + (x - 1)).[ by A43, A56, FDIFF_1:26, XBOOLE_1:1;
then consider s being Real such that
A59: 0 < s and
s < 1 and
A60: (h + g) . (1 + (x - 1)) = ((h + g) . 1) + ((x - 1) * (diff ((h + g),(1 + (s * (x - 1)))))) by A33, A55, A56, A58, ROLLE:4;
0 * (x - 1) < s * (x - 1) by A55, A59, XREAL_1:68;
then 1 + 0 < 1 + (s * (x - 1)) by XREAL_1:8;
then 1 < (1 + (s * (x - 1))) #R (p - 1) by A57, PREPOWER:86;
then A61: 1 - 1 < ((1 + (s * (x - 1))) #R (p - 1)) - 1 by XREAL_1:14;
1 + (s * (x - 1)) in { y where y is Real : 0 < y } by A55, A59;
then 1 + (s * (x - 1)) in right_open_halfline 0 by XXREAL_1:230;
then diff ((h + g),(1 + (s * (x - 1)))) = ((1 + (s * (x - 1))) #R (p - 1)) - 1 by A34;
then (x - 1) * 0 < (x - 1) * (diff ((h + g),(1 + (s * (x - 1))))) by A55, A61, XREAL_1:68;
then 0 < (((x #R p) / p) + (1 / q)) - x by A34, A46, A42, A60;
then 0 + x < ((((x #R p) / p) + (1 / q)) - x) + x by XREAL_1:8;
hence x < ((x #R p) / p) + (1 / q) ; :: thesis: verum
end;
end;
end;
hence x < ((x #R p) / p) + (1 / q) ; :: thesis: verum
end;
A62: ((1 - q) * p) + q = 0 by A7;
A63: now :: thesis: ( a * b = ((a #R p) / p) + ((b #R q) / q) implies a #R p = b #R q )
assume a * b = ((a #R p) / p) + ((b #R q) / q) ; :: thesis: a #R p = b #R q
then a * b = ((a #R p) / p) + ((1 / q) * (b #R q)) by XCMPLX_1:99;
then a * b = ((a #R p) * (1 / p)) + ((1 / q) * (b #R q)) by XCMPLX_1:99;
then a * b = ((a #R p) * ((b #R 0) / p)) + ((1 / q) * (b #R q)) by A4, PREPOWER:71;
then a * b = ((a #R p) * (((b #R ((1 - q) * p)) * (b #R q)) / p)) + ((1 / q) * (b #R q)) by A4, A62, PREPOWER:75;
then a * b = ((a #R p) * (((b #R ((1 - q) * p)) / p) * (b #R q))) + ((1 / q) * (b #R q)) by XCMPLX_1:74;
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:74;
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:91;
then a * b = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A3, A14, PREPOWER:78;
then a * (b #R ((1 - q) + q)) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:72;
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:75;
then (a * (b #R (1 - q))) * (b #R q) = ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) ;
then A64: a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A5, 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 A41, A15, A64 ;
then a * (b #R ((1 - q) + (q - 1))) = b #R (q - 1) by A4, PREPOWER:75;
then a * 1 = b #R (q - 1) by A4, PREPOWER:71;
hence a #R p = b #R q by A4, A8, PREPOWER:91; :: thesis: verum
end;
a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q)
proof
now :: thesis: ( ( a * (b #R (1 - q)) = 1 & a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q) ) or ( a * (b #R (1 - q)) <> 1 & a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q) ) )
per cases ( a * (b #R (1 - q)) = 1 or a * (b #R (1 - q)) <> 1 ) ;
case a * (b #R (1 - q)) = 1 ; :: thesis: a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q)
hence a * (b #R (1 - q)) = (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A2, PREPOWER:73; :: thesis: verum
end;
case a * (b #R (1 - q)) <> 1 ; :: thesis: a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q)
hence a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q) by A41, A15; :: thesis: verum
end;
end;
end;
hence a * (b #R (1 - q)) <= (((a * (b #R (1 - q))) #R p) / p) + (1 / q) ; :: thesis: verum
end;
then (a * (b #R (1 - q))) * (b #R q) <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A5, XREAL_1:64;
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:75;
then a * b <= ((((a * (b #R (1 - q))) #R p) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:72;
then a * b <= ((((a #R p) * ((b #R (1 - q)) #R p)) / p) + (1 / q)) * (b #R q) by A3, A14, PREPOWER:78;
then a * b <= ((((a #R p) * (b #R ((1 - q) * p))) / p) + (1 / q)) * (b #R q) by A4, PREPOWER:91;
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:74;
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:74;
then a * b <= ((a #R p) * ((b #R (((1 - q) * p) + q)) / p)) + ((1 / q) * (b #R q)) by A4, PREPOWER:75;
then a * b <= ((a #R p) * (1 / p)) + ((1 / q) * (b #R q)) by A4, A7, PREPOWER:71;
then a * b <= ((a #R p) / p) + ((1 / q) * (b #R q)) by XCMPLX_1:99;
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 A63, A10, XCMPLX_1:99; :: thesis: verum