:: HOLDER_1 semantic presentation begin registration let x be real number ; cluster right_closed_halfline x -> non empty ; coherence not right_closed_halfline x is empty proof reconsider x = x as Real by XREAL_0:def_1; x in { g where g is Real : x <= g } ; hence not right_closed_halfline x is empty by XXREAL_1:232; ::_thesis: verum end; end; theorem :: HOLDER_1:1 for p, q being Real st 0 < p & 0 < q holds for a being Real st 0 <= a holds (a to_power p) * (a to_power q) = a to_power (p + q) proof let p, q be Real; ::_thesis: ( 0 < p & 0 < q implies for a being Real st 0 <= a holds (a to_power p) * (a to_power q) = a to_power (p + q) ) assume that A1: 0 < p and A2: 0 < q ; ::_thesis: for a being Real st 0 <= a holds (a to_power p) * (a to_power q) = a to_power (p + q) let a be Real; ::_thesis: ( 0 <= a implies (a to_power p) * (a to_power q) = a to_power (p + q) ) assume A3: 0 <= a ; ::_thesis: (a to_power p) * (a to_power q) = a to_power (p + q) now__::_thesis:_(_(_a_=_0_&_(a_to_power_p)_*_(a_to_power_q)_=_a_to_power_(p_+_q)_)_or_(_a_<>_0_&_(a_to_power_p)_*_(a_to_power_q)_=_a_to_power_(p_+_q)_)_) percases ( a = 0 or a <> 0 ) ; caseA4: a = 0 ; ::_thesis: (a to_power p) * (a to_power q) = a to_power (p + q) then (a to_power p) * (a to_power q) = 0 * (0 to_power q) by A1, POWER:def_2 .= 0 ; hence (a to_power p) * (a to_power q) = a to_power (p + q) by A1, A2, A4, POWER:def_2; ::_thesis: verum end; case a <> 0 ; ::_thesis: (a to_power p) * (a to_power q) = a to_power (p + q) hence (a to_power p) * (a to_power q) = a to_power (p + q) by A3, POWER:27; ::_thesis: verum end; end; end; hence (a to_power p) * (a to_power q) = a to_power (p + q) ; ::_thesis: verum end; theorem :: HOLDER_1:2 for p, q being Real st 0 < p & 0 < q holds for a being Real st 0 <= a holds (a to_power p) to_power q = a to_power (p * q) proof let p, q be Real; ::_thesis: ( 0 < p & 0 < q implies for a being Real st 0 <= a holds (a to_power p) to_power q = a to_power (p * q) ) assume that A1: 0 < p and A2: 0 < q ; ::_thesis: for a being Real st 0 <= a holds (a to_power p) to_power q = a to_power (p * q) A3: 0 < p * q by A1, A2, XREAL_1:129; let a be Real; ::_thesis: ( 0 <= a implies (a to_power p) to_power q = a to_power (p * q) ) assume A4: 0 <= a ; ::_thesis: (a to_power p) to_power q = a to_power (p * q) now__::_thesis:_(_(_a_=_0_&_(a_to_power_p)_to_power_q_=_a_to_power_(p_*_q)_)_or_(_a_<>_0_&_(a_to_power_p)_to_power_q_=_a_to_power_(p_*_q)_)_) percases ( a = 0 or a <> 0 ) ; caseA5: a = 0 ; ::_thesis: (a to_power p) to_power q = a to_power (p * q) then (a to_power p) to_power q = 0 to_power q by A1, POWER:def_2 .= 0 by A2, POWER:def_2 ; hence (a to_power p) to_power q = a to_power (p * q) by A3, A5, POWER:def_2; ::_thesis: verum end; case a <> 0 ; ::_thesis: (a to_power p) to_power q = a to_power (p * q) hence (a to_power p) to_power q = a to_power (p * q) by A4, POWER:33; ::_thesis: verum end; end; end; hence (a to_power p) to_power q = a to_power (p * q) ; ::_thesis: verum end; theorem Th3: :: HOLDER_1:3 for p being Real st 0 < p holds for a, b being Real st 0 <= a & a <= b holds a to_power p <= b to_power p proof let p be Real; ::_thesis: ( 0 < p implies for a, b being Real st 0 <= a & a <= b holds a to_power p <= b to_power p ) assume A1: 0 < p ; ::_thesis: for a, b being Real st 0 <= a & a <= b holds a to_power p <= b to_power p let a, b be Real; ::_thesis: ( 0 <= a & a <= b implies a to_power p <= b to_power p ) assume that A2: 0 <= a and A3: a <= b ; ::_thesis: a to_power p <= b to_power p percases ( a = b or a <> b ) ; suppose a = b ; ::_thesis: a to_power p <= b to_power p hence a to_power p <= b to_power p ; ::_thesis: verum end; supposeA4: a <> b ; ::_thesis: a to_power p <= b to_power p thus a to_power p <= b to_power p ::_thesis: verum proof A5: a < b by A3, A4, XXREAL_0:1; now__::_thesis:_(_(_a_=_0_&_a_to_power_p_<=_b_to_power_p_)_or_(_a_<>_0_&_a_to_power_p_<=_b_to_power_p_)_) percases ( a = 0 or a <> 0 ) ; caseA6: a = 0 ; ::_thesis: a to_power p <= b to_power p then a to_power p = 0 by A1, POWER:def_2; hence a to_power p <= b to_power p by A3, A4, A6, POWER:34; ::_thesis: verum end; case a <> 0 ; ::_thesis: a to_power p <= b to_power p hence a to_power p <= b to_power p by A1, A2, A5, POWER:37; ::_thesis: verum end; end; end; hence a to_power p <= b to_power p ; ::_thesis: verum end; end; end; end; theorem Th4: :: HOLDER_1:4 for p, q, a, b being Real st 1 < p & (1 / p) + (1 / q) = 1 & 0 < a & 0 < b holds ( 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) ) ) proof let p, q, a, b 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 Real holds ( g . x = (1 / q) - x & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) ) proof deffunc H1( Real) -> Element of REAL = (1 / q) - $1; 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 Real holds ( g . x = (1 / q) - x & ( for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) ) ) ) ) for x being set 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, TARSKI:def_3; 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 = (1 / q) - 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 d in REAL ; ::_thesis: g . d = ((- 1) * d) + (1 / q) thus g . d = (1 / q) - d by A26 .= ((- 1) * d) + (1 / q) ; ::_thesis: verum end; then A28: g is_differentiable_on dom g by A25, FDIFF_1:23; for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) proof let d be Real; ::_thesis: ( g is_differentiable_in d & diff (g,d) = - 1 ) thus g is_differentiable_in d by A25, A28, FDIFF_1:9; ::_thesis: diff (g,d) = - 1 thus diff (g,d) = (g `| (dom g)) . d by A25, A28, FDIFF_1:def_7 .= - 1 by A25, A27, FDIFF_1:23 ; ::_thesis: verum 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 A24, A26, XBOOLE_0:def_10; ::_thesis: verum end; then consider g being PartFunc of REAL,REAL such that A29: dom g = REAL and A30: for x being Real holds g . x = (1 / q) - x and A31: for x being Real holds ( g is_differentiable_in x & diff (g,x) = - 1 ) ; set f = h + g; A32: dom (h + g) = (right_open_halfline 0) /\ REAL by A29, A20, VALUED_1:def_1 .= right_open_halfline 0 by XBOOLE_1:28 ; A33: 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 A34: 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 ) x in { y where y is Real : 0 < y } by A34, XXREAL_1:230; then A35: ex y being Real st ( x = y & 0 < y ) ; then A36: diff (h,x) = x #R (p - 1) by A21; thus (h + g) . x = (h . x) + (g . x) by A32, A34, VALUED_1:def_1 .= ((x #R p) / p) + (g . x) by A21, A35 .= ((x #R p) / p) + ((1 / q) - x) by A30 .= (((x #R p) / p) + (1 / q)) - x ; ::_thesis: ( h + g is_differentiable_in x & diff ((h + g),x) = (x #R (p - 1)) - 1 ) A37: g is_differentiable_in x by A31; A38: h is_differentiable_in x by A21, A35; hence h + g is_differentiable_in x by A37, FDIFF_1:13; ::_thesis: diff ((h + g),x) = (x #R (p - 1)) - 1 A39: diff (g,x) = - 1 by A31; thus diff ((h + g),x) = (diff (h,x)) + (diff (g,x)) by A37, A38, FDIFF_1:13 .= (x #R (p - 1)) - 1 by A39, A36 ; ::_thesis: verum end; A40: 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 A41: (h + g) . 1 = (((1 #R p) / p) + (1 / q)) - 1 by A33 .= ((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 A33; then A42: h + g is_differentiable_on right_open_halfline 0 by A32, FDIFF_1:9; let x be Real; ::_thesis: ( 0 < x & x <> 1 implies x < ((x #R p) / p) + (1 / q) ) assume that A43: 0 < x and A44: x <> 1 ; ::_thesis: x < ((x #R p) / p) + (1 / q) x in { y where y is Real : 0 < y } by A43; then A45: 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)_)_) percases ( x < 1 or x > 1 ) by A44, XXREAL_0:1; case x < 1 ; ::_thesis: x < ((x #R p) / p) + (1 / q) then A46: 1 - 1 < 1 - x by XREAL_1:15; set t = 1 - x; A47: 1 - 1 < p - 1 by A1, XREAL_1:14; now__::_thesis:_for_z_being_set_st_z_in_[.x,(x_+_(1_-_x)).]_holds_ z_in_right_open_halfline_0 let z be set ; ::_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 A43; hence z in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum end; then A48: [.x,(x + (1 - x)).] c= right_open_halfline 0 by TARSKI:def_3; (h + g) | (right_open_halfline 0) is continuous by A42, FDIFF_1:25; then A49: (h + g) | [.x,(x + (1 - x)).] is continuous by A48, 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 A42, A48, FDIFF_1:26, XBOOLE_1:1; then consider s being Real such that A50: 0 < s and A51: s < 1 and A52: (h + g) . (x + (1 - x)) = ((h + g) . x) + ((1 - x) * (diff ((h + g),(x + (s * (1 - x)))))) by A32, A46, A48, A49, ROLLE:4; s * (1 - x) < 1 * (1 - x) by A46, A51, 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 A43, A46, A50, A47, POWER:40; then (x + (s * (1 - x))) #R (p - 1) < (x + (s * (1 - x))) to_power 0 by A43, A46, A50, POWER:def_2; then (x + (s * (1 - x))) #R (p - 1) < (x + (s * (1 - x))) #R 0 by A43, A46, A50, POWER:def_2; then (x + (s * (1 - x))) #R (p - 1) < 1 by A43, A46, A50, PREPOWER:71; then A53: ((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 A43, A46, A50; 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 A33; then (1 - x) * (diff ((h + g),(x + (s * (1 - x))))) < (1 - x) * 0 by A46, A53, 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 A33, A45, A41, A52; 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 A54: 1 - 1 < x - 1 by XREAL_1:14; set t = x - 1; now__::_thesis:_for_z_being_set_st_z_in_[.1,(1_+_(x_-_1)).]_holds_ z_in_right_open_halfline_0 let z be set ; ::_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 A55: [.1,(1 + (x - 1)).] c= right_open_halfline 0 by TARSKI:def_3; A56: 1 - 1 < p - 1 by A1, XREAL_1:14; (h + g) | (right_open_halfline 0) is continuous by A42, FDIFF_1:25; then A57: (h + g) | [.1,(1 + (x - 1)).] is continuous by A55, 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 A42, A55, FDIFF_1:26, XBOOLE_1:1; then consider s being Real such that A58: 0 < s and s < 1 and A59: (h + g) . (1 + (x - 1)) = ((h + g) . 1) + ((x - 1) * (diff ((h + g),(1 + (s * (x - 1)))))) by A32, A54, A55, A57, ROLLE:4; 0 * (x - 1) < s * (x - 1) by A54, A58, XREAL_1:68; then 1 + 0 < 1 + (s * (x - 1)) by XREAL_1:8; then 1 < (1 + (s * (x - 1))) #R (p - 1) by A56, PREPOWER:86; then A60: 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 A54, A58; 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 A33; then (x - 1) * 0 < (x - 1) * (diff ((h + g),(1 + (s * (x - 1))))) by A54, A60, XREAL_1:68; then 0 < (((x #R p) / p) + (1 / q)) - x by A33, A45, A41, A59; 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; A61: ((1 - q) * p) + q = 0 by A7; A62: 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, A61, 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 A63: 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 A40, A15, A63 ; 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)_)_) percases ( 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 A40, 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 A62, A10, XCMPLX_1:99; ::_thesis: verum end; theorem Th5: :: HOLDER_1:5 for p, q, a, b 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) ) ) proof let p, q, a, b 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_)_) percases ( 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_)_) percases ( 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)_)_)_) percases ( a * b = 0 or a * b <> 0 ) ; caseA9: 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)_)_)_) percases ( a = 0 or b = 0 ) by A9, XCMPLX_1:6; caseA10: 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; caseA16: 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; caseA23: 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 end; Lm1: for a being Real_Sequence st ( for n being Element of NAT holds 0 <= a . n ) holds for n being Element of NAT holds a . n <= (Partial_Sums a) . n proof let a be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= a . n ) implies for n being Element of NAT holds a . n <= (Partial_Sums a) . n ) assume A1: for n being Element of NAT holds 0 <= a . n ; ::_thesis: for n being Element of NAT holds a . n <= (Partial_Sums a) . n defpred S1[ Element of NAT ] means a . $1 <= (Partial_Sums a) . $1; A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then A3: ( (Partial_Sums a) . (n + 1) = ((Partial_Sums a) . n) + (a . (n + 1)) & (a . n) + (a . (n + 1)) <= ((Partial_Sums a) . n) + (a . (n + 1)) ) by SERIES_1:def_1, XREAL_1:6; 0 <= a . n by A1; then 0 + (a . (n + 1)) <= (a . n) + (a . (n + 1)) by XREAL_1:6; hence S1[n + 1] by A3, XXREAL_0:2; ::_thesis: verum end; A4: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence for n being Element of NAT holds a . n <= (Partial_Sums a) . n ; ::_thesis: verum end; Lm2: for a being Real_Sequence st ( for n being Element of NAT holds 0 <= a . n ) holds for n being Element of NAT holds 0 <= (Partial_Sums a) . n proof let a be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= a . n ) implies for n being Element of NAT holds 0 <= (Partial_Sums a) . n ) assume A1: for n being Element of NAT holds 0 <= a . n ; ::_thesis: for n being Element of NAT holds 0 <= (Partial_Sums a) . n let n be Element of NAT ; ::_thesis: 0 <= (Partial_Sums a) . n a . n <= (Partial_Sums a) . n by A1, Lm1; hence 0 <= (Partial_Sums a) . n by A1; ::_thesis: verum end; Lm3: for a being Real_Sequence st ( for n being Element of NAT holds 0 <= a . n ) holds for n being Element of NAT st (Partial_Sums a) . n = 0 holds for k being Element of NAT st k <= n holds a . k = 0 proof let a be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= a . n ) implies for n being Element of NAT st (Partial_Sums a) . n = 0 holds for k being Element of NAT st k <= n holds a . k = 0 ) assume A1: for n being Element of NAT holds 0 <= a . n ; ::_thesis: for n being Element of NAT st (Partial_Sums a) . n = 0 holds for k being Element of NAT st k <= n holds a . k = 0 let n be Element of NAT ; ::_thesis: ( (Partial_Sums a) . n = 0 implies for k being Element of NAT st k <= n holds a . k = 0 ) assume A2: (Partial_Sums a) . n = 0 ; ::_thesis: for k being Element of NAT st k <= n holds a . k = 0 now__::_thesis:_for_k_being_Element_of_NAT_st_k_<=_n_holds_ a_._k_=_0 A3: Partial_Sums a is V41() by A1, SERIES_1:16; let k be Element of NAT ; ::_thesis: ( k <= n implies a . k = 0 ) assume k <= n ; ::_thesis: a . k = 0 then A4: (Partial_Sums a) . k <= (Partial_Sums a) . n by A3, SEQM_3:6; a . k <= (Partial_Sums a) . k by A1, Lm1; hence a . k = 0 by A1, A2, A4; ::_thesis: verum end; hence for k being Element of NAT st k <= n holds a . k = 0 ; ::_thesis: verum end; Lm4: for a being Real_Sequence for n being Element of NAT st ( for k being Element of NAT st k <= n holds a . k = 0 ) holds (Partial_Sums a) . n = 0 proof let a be Real_Sequence; ::_thesis: for n being Element of NAT st ( for k being Element of NAT st k <= n holds a . k = 0 ) holds (Partial_Sums a) . n = 0 defpred S1[ Element of NAT ] means ( ( for k being Element of NAT st k <= $1 holds a . k = 0 ) implies (Partial_Sums a) . $1 = 0 ); A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_(_(_for_k_being_Element_of_NAT_st_k_<=_n_+_1_holds_ a_._k_=_0_)_implies_(Partial_Sums_a)_._(n_+_1)_=_0_) assume A3: for k being Element of NAT st k <= n + 1 holds a . k = 0 ; ::_thesis: (Partial_Sums a) . (n + 1) = 0 A4: now__::_thesis:_for_k_being_Element_of_NAT_st_k_<=_n_holds_ a_._k_=_0 A5: n <= n + 1 by NAT_1:11; let k be Element of NAT ; ::_thesis: ( k <= n implies a . k = 0 ) assume k <= n ; ::_thesis: a . k = 0 hence a . k = 0 by A3, A5, XXREAL_0:2; ::_thesis: verum end; thus (Partial_Sums a) . (n + 1) = ((Partial_Sums a) . n) + (a . (n + 1)) by SERIES_1:def_1 .= 0 by A2, A3, A4 ; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A6: S1[ 0 ] proof assume for k being Element of NAT st k <= 0 holds a . k = 0 ; ::_thesis: (Partial_Sums a) . 0 = 0 then a . 0 = 0 ; hence (Partial_Sums a) . 0 = 0 by SERIES_1:def_1; ::_thesis: verum end; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A1); ::_thesis: verum end; begin theorem Th6: :: HOLDER_1:6 for p, q being Real st 1 < p & (1 / p) + (1 / q) = 1 holds for a, b, ap, bq, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) holds for n being Element of NAT holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) proof let p, q be Real; ::_thesis: ( 1 < p & (1 / p) + (1 / q) = 1 implies for a, b, ap, bq, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) holds for n being Element of NAT holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ) assume that A1: 1 < p and A2: (1 / p) + (1 / q) = 1 ; ::_thesis: for a, b, ap, bq, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) holds for n being Element of NAT holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) reconsider pp = 1 / p as Real ; let a, b, ap, bq, ab be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) implies for n being Element of NAT holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ) assume A3: for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ; ::_thesis: for n being Element of NAT holds (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) let n be Element of NAT ; ::_thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) set B = (Partial_Sums bq) . n; 1 / p < 1 by A1, XREAL_1:189; then A4: 1 - 1 < 1 - pp by XREAL_1:15; then A5: 0 < q by A2; A6: for n being Element of NAT holds 0 <= bq . n proof let n be Element of NAT ; ::_thesis: 0 <= bq . n A7: bq . n = (abs (b . n)) to_power q by A3; now__::_thesis:_(_(_abs_(b_._n)_=_0_&_0_<=_bq_._n_)_or_(_abs_(b_._n)_>_0_&_0_<=_bq_._n_)_) percases ( abs (b . n) = 0 or abs (b . n) > 0 ) by COMPLEX1:46; case abs (b . n) = 0 ; ::_thesis: 0 <= bq . n hence 0 <= bq . n by A5, A7, POWER:def_2; ::_thesis: verum end; case abs (b . n) > 0 ; ::_thesis: 0 <= bq . n hence 0 <= bq . n by A7, POWER:34; ::_thesis: verum end; end; end; hence 0 <= bq . n ; ::_thesis: verum end; then A8: 0 <= (Partial_Sums bq) . n by Lm2; set A = (Partial_Sums ap) . n; A9: for n being Element of NAT holds 0 <= ap . n proof let n be Element of NAT ; ::_thesis: 0 <= ap . n A10: ap . n = (abs (a . n)) to_power p by A3; now__::_thesis:_(_(_abs_(a_._n)_=_0_&_0_<=_ap_._n_)_or_(_abs_(a_._n)_>_0_&_0_<=_ap_._n_)_) percases ( abs (a . n) = 0 or abs (a . n) > 0 ) by COMPLEX1:46; case abs (a . n) = 0 ; ::_thesis: 0 <= ap . n hence 0 <= ap . n by A1, A10, POWER:def_2; ::_thesis: verum end; case abs (a . n) > 0 ; ::_thesis: 0 <= ap . n hence 0 <= ap . n by A10, POWER:34; ::_thesis: verum end; end; end; hence 0 <= ap . n ; ::_thesis: verum end; then A11: 0 <= (Partial_Sums ap) . n by Lm2; set Bq = ((Partial_Sums bq) . n) to_power (1 / q); set Ap = ((Partial_Sums ap) . n) to_power (1 / p); A12: 1 / p > 0 by A1, XREAL_1:139; now__::_thesis:_(_(_((Partial_Sums_ap)_._n)_*_((Partial_Sums_bq)_._n)_=_0_&_(Partial_Sums_ab)_._n_<=_(((Partial_Sums_ap)_._n)_to_power_(1_/_p))_*_(((Partial_Sums_bq)_._n)_to_power_(1_/_q))_)_or_(_((Partial_Sums_ap)_._n)_*_((Partial_Sums_bq)_._n)_<>_0_&_(Partial_Sums_ab)_._n_<=_(((Partial_Sums_ap)_._n)_to_power_(1_/_p))_*_(((Partial_Sums_bq)_._n)_to_power_(1_/_q))_)_) percases ( ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) = 0 or ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) <> 0 ) ; caseA13: ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) = 0 ; ::_thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) A14: 0 <= ((Partial_Sums ap) . n) to_power (1 / p) proof now__::_thesis:_(_(_0_<_(Partial_Sums_ap)_._n_&_0_<=_((Partial_Sums_ap)_._n)_to_power_(1_/_p)_)_or_(_0_=_(Partial_Sums_ap)_._n_&_0_<=_((Partial_Sums_ap)_._n)_to_power_(1_/_p)_)_) percases ( 0 < (Partial_Sums ap) . n or 0 = (Partial_Sums ap) . n ) by A9, Lm2; case 0 < (Partial_Sums ap) . n ; ::_thesis: 0 <= ((Partial_Sums ap) . n) to_power (1 / p) hence 0 <= ((Partial_Sums ap) . n) to_power (1 / p) by POWER:34; ::_thesis: verum end; case 0 = (Partial_Sums ap) . n ; ::_thesis: 0 <= ((Partial_Sums ap) . n) to_power (1 / p) hence 0 <= ((Partial_Sums ap) . n) to_power (1 / p) by A12, POWER:def_2; ::_thesis: verum end; end; end; hence 0 <= ((Partial_Sums ap) . n) to_power (1 / p) ; ::_thesis: verum end; 0 <= ((Partial_Sums bq) . n) to_power (1 / q) proof now__::_thesis:_(_(_0_<_(Partial_Sums_bq)_._n_&_0_<=_((Partial_Sums_bq)_._n)_to_power_(1_/_q)_)_or_(_0_=_(Partial_Sums_bq)_._n_&_0_<=_((Partial_Sums_bq)_._n)_to_power_(1_/_q)_)_) percases ( 0 < (Partial_Sums bq) . n or 0 = (Partial_Sums bq) . n ) by A6, Lm2; case 0 < (Partial_Sums bq) . n ; ::_thesis: 0 <= ((Partial_Sums bq) . n) to_power (1 / q) hence 0 <= ((Partial_Sums bq) . n) to_power (1 / q) by POWER:34; ::_thesis: verum end; case 0 = (Partial_Sums bq) . n ; ::_thesis: 0 <= ((Partial_Sums bq) . n) to_power (1 / q) hence 0 <= ((Partial_Sums bq) . n) to_power (1 / q) by A2, A4, POWER:def_2; ::_thesis: verum end; end; end; hence 0 <= ((Partial_Sums bq) . n) to_power (1 / q) ; ::_thesis: verum end; then A15: 0 <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) by A14; now__::_thesis:_(_(_(Partial_Sums_ap)_._n_=_0_&_(Partial_Sums_ab)_._n_<=_(((Partial_Sums_ap)_._n)_to_power_(1_/_p))_*_(((Partial_Sums_bq)_._n)_to_power_(1_/_q))_)_or_(_(Partial_Sums_bq)_._n_=_0_&_(Partial_Sums_ab)_._n_<=_(((Partial_Sums_ap)_._n)_to_power_(1_/_p))_*_(((Partial_Sums_bq)_._n)_to_power_(1_/_q))_)_) percases ( (Partial_Sums ap) . n = 0 or (Partial_Sums bq) . n = 0 ) by A13, XCMPLX_1:6; caseA16: (Partial_Sums ap) . n = 0 ; ::_thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) A17: for k being Element of NAT st k <= n holds a . k = 0 proof let k be Element of NAT ; ::_thesis: ( k <= n implies a . k = 0 ) assume k <= n ; ::_thesis: a . k = 0 then ap . k = 0 by A9, A16, Lm3; then A18: (abs (a . k)) to_power p = 0 by A3; abs (a . k) = 0 proof assume abs (a . k) <> 0 ; ::_thesis: contradiction then abs (a . k) > 0 by COMPLEX1:46; hence contradiction by A18, POWER:34; ::_thesis: verum end; hence a . k = 0 by ABSVALUE:2; ::_thesis: verum end; for k being Element of NAT st k <= n holds ab . k = 0 proof let k be Element of NAT ; ::_thesis: ( k <= n implies ab . k = 0 ) assume A19: k <= n ; ::_thesis: ab . k = 0 thus ab . k = abs ((a . k) * (b . k)) by A3 .= abs (0 * (b . k)) by A17, A19 .= 0 by ABSVALUE:2 ; ::_thesis: verum end; hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) by A15, Lm4; ::_thesis: verum end; caseA20: (Partial_Sums bq) . n = 0 ; ::_thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) A21: for k being Element of NAT st k <= n holds b . k = 0 proof let k be Element of NAT ; ::_thesis: ( k <= n implies b . k = 0 ) assume k <= n ; ::_thesis: b . k = 0 then bq . k = 0 by A6, A20, Lm3; then A22: (abs (b . k)) to_power q = 0 by A3; abs (b . k) = 0 proof assume abs (b . k) <> 0 ; ::_thesis: contradiction then abs (b . k) > 0 by COMPLEX1:46; hence contradiction by A22, POWER:34; ::_thesis: verum end; hence b . k = 0 by ABSVALUE:2; ::_thesis: verum end; for k being Element of NAT st k <= n holds ab . k = 0 proof let k be Element of NAT ; ::_thesis: ( k <= n implies ab . k = 0 ) assume A23: k <= n ; ::_thesis: ab . k = 0 thus ab . k = abs ((a . k) * (b . k)) by A3 .= abs ((a . k) * 0) by A21, A23 .= 0 by ABSVALUE:2 ; ::_thesis: verum end; hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) by A15, Lm4; ::_thesis: verum end; end; end; hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ; ::_thesis: verum end; caseA24: ((Partial_Sums ap) . n) * ((Partial_Sums bq) . n) <> 0 ; ::_thesis: (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) deffunc H1( Element of NAT ) -> Element of REAL = (abs (b . $1)) / (((Partial_Sums bq) . n) to_power (1 / q)); consider y being Real_Sequence such that A25: for n being Element of NAT holds y . n = H1(n) from SEQ_1:sch_1(); A26: (Partial_Sums bq) . n <> 0 by A24; then A27: ((Partial_Sums bq) . n) to_power (1 / q) > 0 by A8, POWER:34; A28: for n being Element of NAT holds 0 <= y . n proof let n be Element of NAT ; ::_thesis: 0 <= y . n 0 <= abs (b . n) by COMPLEX1:46; then 0 <= (abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q)) by A27; hence 0 <= y . n by A25; ::_thesis: verum end; deffunc H2( Element of NAT ) -> Element of REAL = (abs (a . $1)) / (((Partial_Sums ap) . n) to_power (1 / p)); consider x being Real_Sequence such that A29: for n being Element of NAT holds x . n = H2(n) from SEQ_1:sch_1(); A30: for n being Element of NAT holds ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n = (x . n) * (y . n) proof let n be Element of NAT ; ::_thesis: ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n = (x . n) * (y . n) ( x . n = (abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p)) & y . n = (abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q)) ) by A29, A25; hence (x . n) * (y . n) = ((abs (a . n)) * (abs (b . n))) / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))) by XCMPLX_1:76 .= (abs ((a . n) * (b . n))) / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))) by COMPLEX1:65 .= (ab . n) / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))) by A3 .= (1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) * (ab . n) by XCMPLX_1:99 .= ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n by SEQ_1:9 ; ::_thesis: verum end; A31: (Partial_Sums ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab)) . n = ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) (Partial_Sums ab)) . n by SERIES_1:9 .= (1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) * ((Partial_Sums ab) . n) by SEQ_1:9 ; A32: (Partial_Sums ap) . n <> 0 by A24; then A33: ((Partial_Sums ap) . n) to_power (1 / p) > 0 by A11, POWER:34; then A34: (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) > 0 by A27, XREAL_1:129; A35: for n being Element of NAT holds (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) proof let n be Element of NAT ; ::_thesis: (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) A36: ((abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = ((abs (a . n)) to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) proof now__::_thesis:_(_(_abs_(a_._n)_=_0_&_((abs_(a_._n))_/_(((Partial_Sums_ap)_._n)_to_power_(1_/_p)))_to_power_p_=_((abs_(a_._n))_to_power_p)_/_((((Partial_Sums_ap)_._n)_to_power_(1_/_p))_to_power_p)_)_or_(_abs_(a_._n)_<>_0_&_((abs_(a_._n))_/_(((Partial_Sums_ap)_._n)_to_power_(1_/_p)))_to_power_p_=_((abs_(a_._n))_to_power_p)_/_((((Partial_Sums_ap)_._n)_to_power_(1_/_p))_to_power_p)_)_) percases ( abs (a . n) = 0 or abs (a . n) <> 0 ) ; caseA37: abs (a . n) = 0 ; ::_thesis: ((abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = ((abs (a . n)) to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) hence ((abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = 0 / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) by A1, POWER:def_2 .= ((abs (a . n)) to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) by A1, A37, POWER:def_2 ; ::_thesis: verum end; case abs (a . n) <> 0 ; ::_thesis: ((abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = ((abs (a . n)) to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) then abs (a . n) > 0 by COMPLEX1:46; hence ((abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = ((abs (a . n)) to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) by A33, POWER:31; ::_thesis: verum end; end; end; hence ((abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p))) to_power p = ((abs (a . n)) to_power p) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p) ; ::_thesis: verum end; A38: ((abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = ((abs (b . n)) to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) proof now__::_thesis:_(_(_abs_(b_._n)_=_0_&_((abs_(b_._n))_/_(((Partial_Sums_bq)_._n)_to_power_(1_/_q)))_to_power_q_=_((abs_(b_._n))_to_power_q)_/_((((Partial_Sums_bq)_._n)_to_power_(1_/_q))_to_power_q)_)_or_(_abs_(b_._n)_<>_0_&_((abs_(b_._n))_/_(((Partial_Sums_bq)_._n)_to_power_(1_/_q)))_to_power_q_=_((abs_(b_._n))_to_power_q)_/_((((Partial_Sums_bq)_._n)_to_power_(1_/_q))_to_power_q)_)_) percases ( abs (b . n) = 0 or abs (b . n) <> 0 ) ; caseA39: abs (b . n) = 0 ; ::_thesis: ((abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = ((abs (b . n)) to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) hence ((abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = 0 / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) by A5, POWER:def_2 .= ((abs (b . n)) to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) by A5, A39, POWER:def_2 ; ::_thesis: verum end; case abs (b . n) <> 0 ; ::_thesis: ((abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = ((abs (b . n)) to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) then abs (b . n) > 0 by COMPLEX1:46; hence ((abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = ((abs (b . n)) to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) by A27, POWER:31; ::_thesis: verum end; end; end; hence ((abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q))) to_power q = ((abs (b . n)) to_power q) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q) ; ::_thesis: verum end; y . n = (abs (b . n)) / (((Partial_Sums bq) . n) to_power (1 / q)) by A25; then A40: ((y . n) to_power q) / q = ((bq . n) / ((((Partial_Sums bq) . n) to_power (1 / q)) to_power q)) / q by A3, A38 .= ((bq . n) / (((Partial_Sums bq) . n) to_power ((1 / q) * q))) / q by A8, A26, POWER:33 .= ((bq . n) / (((Partial_Sums bq) . n) to_power 1)) / q by A5, XCMPLX_1:87 .= ((bq . n) / ((Partial_Sums bq) . n)) / q by POWER:25 .= (1 / q) * ((bq . n) / ((Partial_Sums bq) . n)) by XCMPLX_1:99 .= (1 / q) * ((1 / ((Partial_Sums bq) . n)) * (bq . n)) by XCMPLX_1:99 .= (1 / q) * (((1 / ((Partial_Sums bq) . n)) (#) bq) . n) by SEQ_1:9 .= ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq)) . n by SEQ_1:9 ; x . n = (abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p)) by A29; then ((x . n) to_power p) / p = ((ap . n) / ((((Partial_Sums ap) . n) to_power (1 / p)) to_power p)) / p by A3, A36 .= ((ap . n) / (((Partial_Sums ap) . n) to_power ((1 / p) * p))) / p by A11, A32, POWER:33 .= ((ap . n) / (((Partial_Sums ap) . n) to_power 1)) / p by A1, XCMPLX_1:87 .= ((ap . n) / ((Partial_Sums ap) . n)) / p by POWER:25 .= (1 / p) * ((ap . n) / ((Partial_Sums ap) . n)) by XCMPLX_1:99 .= (1 / p) * ((1 / ((Partial_Sums ap) . n)) * (ap . n)) by XCMPLX_1:99 .= (1 / p) * (((1 / ((Partial_Sums ap) . n)) (#) ap) . n) by SEQ_1:9 .= ((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) . n by SEQ_1:9 ; hence (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) by A40, SEQ_1:7; ::_thesis: verum end; A41: for n being Element of NAT holds 0 <= x . n proof let n be Element of NAT ; ::_thesis: 0 <= x . n 0 <= abs (a . n) by COMPLEX1:46; then 0 <= (abs (a . n)) / (((Partial_Sums ap) . n) to_power (1 / p)) by A33; hence 0 <= x . n by A29; ::_thesis: verum end; A42: for n being Element of NAT holds ( (x . n) * (y . n) <= (((x . n) to_power p) / p) + (((y . n) to_power q) / q) & ( (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) implies (x . n) to_power p = (y . n) to_power q ) & ( (x . n) to_power p = (y . n) to_power q implies (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) ) ) proof let n be Element of NAT ; ::_thesis: ( (x . n) * (y . n) <= (((x . n) to_power p) / p) + (((y . n) to_power q) / q) & ( (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) implies (x . n) to_power p = (y . n) to_power q ) & ( (x . n) to_power p = (y . n) to_power q implies (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) ) ) ( 0 <= x . n & 0 <= y . n ) by A41, A28; hence ( (x . n) * (y . n) <= (((x . n) to_power p) / p) + (((y . n) to_power q) / q) & ( (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) implies (x . n) to_power p = (y . n) to_power q ) & ( (x . n) to_power p = (y . n) to_power q implies (x . n) * (y . n) = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) ) ) by A1, A2, Th5; ::_thesis: verum end; for n being Element of NAT holds ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n <= (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n proof let n be Element of NAT ; ::_thesis: ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n <= (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n ( (x . n) * (y . n) <= (((x . n) to_power p) / p) + (((y . n) to_power q) / q) & (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n = (((x . n) to_power p) / p) + (((y . n) to_power q) / q) ) by A42, A35; hence ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab) . n <= (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n by A30; ::_thesis: verum end; then A43: (Partial_Sums ((1 / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)))) (#) ab)) . n <= (Partial_Sums (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq)))) . n by SERIES_1:14; (Partial_Sums (((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap)) + ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq)))) . n = ((Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap))) + (Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq)))) . n by SERIES_1:5 .= ((Partial_Sums ((1 / p) (#) ((1 / ((Partial_Sums ap) . n)) (#) ap))) . n) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SEQ_1:7 .= (((1 / p) (#) (Partial_Sums ((1 / ((Partial_Sums ap) . n)) (#) ap))) . n) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SERIES_1:9 .= ((1 / p) * ((Partial_Sums ((1 / ((Partial_Sums ap) . n)) (#) ap)) . n)) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SEQ_1:9 .= ((1 / p) * (((1 / ((Partial_Sums ap) . n)) (#) (Partial_Sums ap)) . n)) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SERIES_1:9 .= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + ((Partial_Sums ((1 / q) (#) ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SEQ_1:9 .= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + (((1 / q) (#) (Partial_Sums ((1 / ((Partial_Sums bq) . n)) (#) bq))) . n) by SERIES_1:9 .= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + ((1 / q) * ((Partial_Sums ((1 / ((Partial_Sums bq) . n)) (#) bq)) . n)) by SEQ_1:9 .= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + ((1 / q) * (((1 / ((Partial_Sums bq) . n)) (#) (Partial_Sums bq)) . n)) by SERIES_1:9 .= ((1 / p) * ((1 / ((Partial_Sums ap) . n)) * ((Partial_Sums ap) . n))) + ((1 / q) * ((1 / ((Partial_Sums bq) . n)) * ((Partial_Sums bq) . n))) by SEQ_1:9 .= ((1 / p) * 1) + ((1 / q) * ((1 / ((Partial_Sums bq) . n)) * ((Partial_Sums bq) . n))) by A32, XCMPLX_1:87 .= ((1 / p) * 1) + ((1 / q) * 1) by A26, XCMPLX_1:87 .= 1 by A2 ; then ((Partial_Sums ab) . n) / ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q))) <= 1 by A43, A31, XCMPLX_1:99; hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) by A34, XREAL_1:187; ::_thesis: verum end; end; end; hence (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) ; ::_thesis: verum end; theorem Th7: :: HOLDER_1:7 for p being Real st 1 < p holds for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) holds for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) proof let p be Real; ::_thesis: ( 1 < p implies for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) holds for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) ) assume A1: 1 < p ; ::_thesis: for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) holds for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) A2: 1 / p > 0 by A1, XREAL_1:139; let a, b, ap, bp, ab be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) implies for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) ) assume A3: for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ; ::_thesis: for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) A4: for n being Element of NAT holds 0 <= ap . n proof let n be Element of NAT ; ::_thesis: 0 <= ap . n A5: ap . n = (abs (a . n)) to_power p by A3; now__::_thesis:_(_(_abs_(a_._n)_=_0_&_0_<=_ap_._n_)_or_(_abs_(a_._n)_>_0_&_0_<=_ap_._n_)_) percases ( abs (a . n) = 0 or abs (a . n) > 0 ) by COMPLEX1:46; case abs (a . n) = 0 ; ::_thesis: 0 <= ap . n hence 0 <= ap . n by A1, A5, POWER:def_2; ::_thesis: verum end; case abs (a . n) > 0 ; ::_thesis: 0 <= ap . n hence 0 <= ap . n by A5, POWER:34; ::_thesis: verum end; end; end; hence 0 <= ap . n ; ::_thesis: verum end; A6: for n being Element of NAT holds 0 <= bp . n proof let n be Element of NAT ; ::_thesis: 0 <= bp . n A7: bp . n = (abs (b . n)) to_power p by A3; now__::_thesis:_(_(_abs_(b_._n)_=_0_&_0_<=_bp_._n_)_or_(_abs_(b_._n)_>_0_&_0_<=_bp_._n_)_) percases ( abs (b . n) = 0 or abs (b . n) > 0 ) by COMPLEX1:46; case abs (b . n) = 0 ; ::_thesis: 0 <= bp . n hence 0 <= bp . n by A1, A7, POWER:def_2; ::_thesis: verum end; case abs (b . n) > 0 ; ::_thesis: 0 <= bp . n hence 0 <= bp . n by A7, POWER:34; ::_thesis: verum end; end; end; hence 0 <= bp . n ; ::_thesis: verum end; deffunc H1( Element of NAT ) -> Element of REAL = (abs ((a . $1) + (b . $1))) to_power (p - 1); consider x being Real_Sequence such that A8: for n being Element of NAT holds x . n = H1(n) from SEQ_1:sch_1(); A9: 1 - 1 < p - 1 by A1, XREAL_1:14; A10: for n being Element of NAT holds 0 <= x . n proof let n be Element of NAT ; ::_thesis: 0 <= x . n A11: x . n = (abs ((a . n) + (b . n))) to_power (p - 1) by A8; now__::_thesis:_(_(_abs_((a_._n)_+_(b_._n))_=_0_&_0_<=_x_._n_)_or_(_abs_((a_._n)_+_(b_._n))_>_0_&_0_<=_x_._n_)_) percases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) > 0 ) by COMPLEX1:46; case abs ((a . n) + (b . n)) = 0 ; ::_thesis: 0 <= x . n hence 0 <= x . n by A9, A11, POWER:def_2; ::_thesis: verum end; case abs ((a . n) + (b . n)) > 0 ; ::_thesis: 0 <= x . n hence 0 <= x . n by A11, POWER:34; ::_thesis: verum end; end; end; hence 0 <= x . n ; ::_thesis: verum end; A12: for n being Element of NAT holds (x (#) (abs b)) . n = abs ((b . n) * (x . n)) proof let n be Element of NAT ; ::_thesis: (x (#) (abs b)) . n = abs ((b . n) * (x . n)) 0 <= x . n by A10; then A13: abs (x . n) = x . n by ABSVALUE:def_1; thus (x (#) (abs b)) . n = (x . n) * ((abs b) . n) by SEQ_1:8 .= (x . n) * (abs (b . n)) by SEQ_1:12 .= abs ((b . n) * (x . n)) by A13, COMPLEX1:65 ; ::_thesis: verum end; reconsider pp = 1 / p as Real ; reconsider qq = 1 - pp as Real ; reconsider q = 1 / qq as Real ; A14: qq = 1 / q by XCMPLX_1:56; then A15: (1 / p) + (1 / q) = 1 ; 1 / p < 1 by A1, XREAL_1:189; then A16: 1 - 1 < 1 - pp by XREAL_1:15; then A17: q <> 0 by A14; then (((1 * q) + (1 * p)) / (p * q)) * (p * q) = 1 * (p * q) by A1, A15, XCMPLX_1:116; then A18: q + p = p * q by A1, A17, XCMPLX_1:6, XCMPLX_1:87; A19: for n being Element of NAT holds ab . n = (x . n) * (abs ((a . n) + (b . n))) proof let n be Element of NAT ; ::_thesis: ab . n = (x . n) * (abs ((a . n) + (b . n))) now__::_thesis:_(_(_abs_((a_._n)_+_(b_._n))_=_0_&_ab_._n_=_(x_._n)_*_(abs_((a_._n)_+_(b_._n)))_)_or_(_abs_((a_._n)_+_(b_._n))_<>_0_&_ab_._n_=_(x_._n)_*_(abs_((a_._n)_+_(b_._n)))_)_) percases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) <> 0 ) ; caseA20: abs ((a . n) + (b . n)) = 0 ; ::_thesis: ab . n = (x . n) * (abs ((a . n) + (b . n))) thus ab . n = (abs ((a . n) + (b . n))) to_power p by A3 .= (x . n) * (abs ((a . n) + (b . n))) by A1, A20, POWER:def_2 ; ::_thesis: verum end; caseA21: abs ((a . n) + (b . n)) <> 0 ; ::_thesis: ab . n = (x . n) * (abs ((a . n) + (b . n))) A22: 0 <= abs ((a . n) + (b . n)) by COMPLEX1:46; thus ab . n = (abs ((a . n) + (b . n))) to_power ((p - 1) + 1) by A3 .= ((abs ((a . n) + (b . n))) to_power (p - 1)) * ((abs ((a . n) + (b . n))) to_power 1) by A21, A22, POWER:27 .= ((abs ((a . n) + (b . n))) to_power (p - 1)) * (abs ((a . n) + (b . n))) by POWER:25 .= (x . n) * (abs ((a . n) + (b . n))) by A8 ; ::_thesis: verum end; end; end; hence ab . n = (x . n) * (abs ((a . n) + (b . n))) ; ::_thesis: verum end; A23: for n being Element of NAT holds ab . n <= ((x (#) (abs a)) + (x (#) (abs b))) . n proof let n be Element of NAT ; ::_thesis: ab . n <= ((x (#) (abs a)) + (x (#) (abs b))) . n A24: (x . n) * ((abs (a . n)) + (abs (b . n))) = ((x . n) * (abs (a . n))) + ((x . n) * (abs (b . n))) .= ((x . n) * ((abs a) . n)) + ((x . n) * (abs (b . n))) by SEQ_1:12 .= ((x . n) * ((abs a) . n)) + ((x . n) * ((abs b) . n)) by SEQ_1:12 .= ((x (#) (abs a)) . n) + ((x . n) * ((abs b) . n)) by SEQ_1:8 .= ((x (#) (abs a)) . n) + ((x (#) (abs b)) . n) by SEQ_1:8 .= ((x (#) (abs a)) + (x (#) (abs b))) . n by SEQ_1:7 ; ( 0 <= x . n & ab . n = (x . n) * (abs ((a . n) + (b . n))) ) by A10, A19; hence ab . n <= ((x (#) (abs a)) + (x (#) (abs b))) . n by A24, COMPLEX1:56, XREAL_1:64; ::_thesis: verum end; A25: 0 < q by A16, A14; A26: for n being Element of NAT holds (abs (x . n)) to_power q = ab . n proof let n be Element of NAT ; ::_thesis: (abs (x . n)) to_power q = ab . n 0 <= x . n by A10; then abs (x . n) = x . n by ABSVALUE:def_1; then A27: (abs (x . n)) to_power q = ((abs ((a . n) + (b . n))) to_power (p - 1)) to_power q by A8; now__::_thesis:_(_(_abs_((a_._n)_+_(b_._n))_=_0_&_(abs_(x_._n))_to_power_q_=_ab_._n_)_or_(_abs_((a_._n)_+_(b_._n))_<>_0_&_(abs_(x_._n))_to_power_q_=_ab_._n_)_) percases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) <> 0 ) ; caseA28: abs ((a . n) + (b . n)) = 0 ; ::_thesis: (abs (x . n)) to_power q = ab . n then A29: ab . n = 0 to_power p by A3 .= 0 by A1, POWER:def_2 ; (abs (x . n)) to_power q = 0 to_power q by A9, A27, A28, POWER:def_2 .= 0 by A25, POWER:def_2 ; hence (abs (x . n)) to_power q = ab . n by A29; ::_thesis: verum end; case abs ((a . n) + (b . n)) <> 0 ; ::_thesis: (abs (x . n)) to_power q = ab . n then 0 < abs ((a . n) + (b . n)) by COMPLEX1:46; hence (abs (x . n)) to_power q = (abs ((a . n) + (b . n))) to_power ((p - 1) * q) by A27, POWER:33 .= ab . n by A3, A18 ; ::_thesis: verum end; end; end; hence (abs (x . n)) to_power q = ab . n ; ::_thesis: verum end; A30: for n being Element of NAT holds (x (#) (abs a)) . n = abs ((a . n) * (x . n)) proof let n be Element of NAT ; ::_thesis: (x (#) (abs a)) . n = abs ((a . n) * (x . n)) 0 <= x . n by A10; then A31: abs (x . n) = x . n by ABSVALUE:def_1; thus (x (#) (abs a)) . n = (x . n) * ((abs a) . n) by SEQ_1:8 .= (x . n) * (abs (a . n)) by SEQ_1:12 .= abs ((a . n) * (x . n)) by A31, COMPLEX1:65 ; ::_thesis: verum end; A32: for n being Element of NAT holds (Partial_Sums ab) . n <= ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / q)) proof let n be Element of NAT ; ::_thesis: (Partial_Sums ab) . n <= ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / q)) A33: (Partial_Sums ((x (#) (abs a)) + (x (#) (abs b)))) . n = ((Partial_Sums (x (#) (abs a))) + (Partial_Sums (x (#) (abs b)))) . n by SERIES_1:5 .= ((Partial_Sums (x (#) (abs a))) . n) + ((Partial_Sums (x (#) (abs b))) . n) by SEQ_1:7 ; ( (Partial_Sums (x (#) (abs a))) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q)) & (Partial_Sums (x (#) (abs b))) . n <= (((Partial_Sums bp) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q)) ) by A1, A3, A15, A30, A12, A26, Th6; then A34: ((Partial_Sums (x (#) (abs a))) . n) + ((Partial_Sums (x (#) (abs b))) . n) <= ((((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q))) + ((((Partial_Sums bp) . n) to_power (1 / p)) * (((Partial_Sums ab) . n) to_power (1 / q))) by XREAL_1:7; (Partial_Sums ab) . n <= (Partial_Sums ((x (#) (abs a)) + (x (#) (abs b)))) . n by A23, SERIES_1:14; hence (Partial_Sums ab) . n <= ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / q)) by A33, A34, XXREAL_0:2; ::_thesis: verum end; A35: for n being Element of NAT holds 0 <= ab . n proof let n be Element of NAT ; ::_thesis: 0 <= ab . n 0 <= abs ((a . n) + (b . n)) by COMPLEX1:46; then A36: 0 to_power p <= (abs ((a . n) + (b . n))) to_power p by A1, Th3; ab . n = (abs ((a . n) + (b . n))) to_power p by A3; hence 0 <= ab . n by A1, A36, POWER:def_2; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_ab)_._n)_to_power_(1_/_p)_<=_(((Partial_Sums_ap)_._n)_to_power_(1_/_p))_+_(((Partial_Sums_bp)_._n)_to_power_(1_/_p)) let n be Element of NAT ; ::_thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) set A = (Partial_Sums ab) . n; set C = (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)); set D = ((Partial_Sums ab) . n) to_power (1 / q); A37: 0 <= (Partial_Sums ab) . n by A35, Lm2; 0 <= (Partial_Sums bp) . n by A6, Lm2; then 0 to_power (1 / p) <= ((Partial_Sums bp) . n) to_power (1 / p) by A2, Th3; then A38: 0 <= ((Partial_Sums bp) . n) to_power (1 / p) by A2, POWER:def_2; 0 <= (Partial_Sums ap) . n by A4, Lm2; then 0 to_power (1 / p) <= ((Partial_Sums ap) . n) to_power (1 / p) by A2, Th3; then 0 <= ((Partial_Sums ap) . n) to_power (1 / p) by A2, POWER:def_2; then A39: 0 + 0 <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) by A38; now__::_thesis:_(_(_(Partial_Sums_ab)_._n_=_0_&_((Partial_Sums_ab)_._n)_to_power_(1_/_p)_<=_(((Partial_Sums_ap)_._n)_to_power_(1_/_p))_+_(((Partial_Sums_bp)_._n)_to_power_(1_/_p))_)_or_(_(Partial_Sums_ab)_._n_<>_0_&_((Partial_Sums_ab)_._n)_to_power_(1_/_p)_<=_(((Partial_Sums_ap)_._n)_to_power_(1_/_p))_+_(((Partial_Sums_bp)_._n)_to_power_(1_/_p))_)_) percases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n <> 0 ) ; case (Partial_Sums ab) . n = 0 ; ::_thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) hence ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) by A2, A39, POWER:def_2; ::_thesis: verum end; caseA40: (Partial_Sums ab) . n <> 0 ; ::_thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) set B = 1 / (((Partial_Sums ab) . n) to_power (1 / q)); A41: 0 < ((Partial_Sums ab) . n) to_power (1 / q) by A37, A40, POWER:34; then A42: 0 < 1 / (((Partial_Sums ab) . n) to_power (1 / q)) by XREAL_1:139; A43: (((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * (((Partial_Sums ab) . n) to_power (1 / q))) * (1 / (((Partial_Sums ab) . n) to_power (1 / q))) = ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * ((((Partial_Sums ab) . n) to_power (1 / q)) * (1 / (((Partial_Sums ab) . n) to_power (1 / q)))) .= ((((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p))) * 1 by A41, XCMPLX_1:87 .= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) ; ((Partial_Sums ab) . n) * (1 / (((Partial_Sums ab) . n) to_power (1 / q))) = ((Partial_Sums ab) . n) / (((Partial_Sums ab) . n) to_power (1 / q)) by XCMPLX_1:99 .= (((Partial_Sums ab) . n) to_power 1) / (((Partial_Sums ab) . n) to_power (1 / q)) by POWER:25 .= ((Partial_Sums ab) . n) to_power (1 - (1 / q)) by A37, A40, POWER:29 .= ((Partial_Sums ab) . n) to_power (1 / p) by A14 ; hence ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) by A32, A42, A43, XREAL_1:64; ::_thesis: verum end; end; end; hence ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) ; ::_thesis: verum end; hence for n being Element of NAT holds ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) ; ::_thesis: verum end; theorem Th8: :: HOLDER_1:8 for a, b being Real_Sequence st ( for n being Element of NAT holds a . n <= b . n ) & b is convergent & a is V41() holds ( a is convergent & lim a <= lim b ) proof let a, b be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds a . n <= b . n ) & b is convergent & a is V41() implies ( a is convergent & lim a <= lim b ) ) assume that A1: for n being Element of NAT holds a . n <= b . n and A2: b is convergent and A3: a is V41() ; ::_thesis: ( a is convergent & lim a <= lim b ) A4: b is bounded by A2; A5: a is bounded_above proof consider r being real number such that A6: for n being Element of NAT holds b . n < r by A4, SEQ_2:def_3; now__::_thesis:_for_n_being_Element_of_NAT_holds_a_._n_<_r_+_1 let n be Element of NAT ; ::_thesis: a . n < r + 1 a . n <= b . n by A1; then a . n <= r by A6, XXREAL_0:2; then (a . n) + 0 < r + 1 by XREAL_1:8; hence a . n < r + 1 ; ::_thesis: verum end; hence a is bounded_above by SEQ_2:def_3; ::_thesis: verum end; hence a is convergent by A3; ::_thesis: lim a <= lim b thus lim a <= lim b by A1, A2, A3, A5, SEQ_2:18; ::_thesis: verum end; theorem Th9: :: HOLDER_1:9 for a, b, c being Real_Sequence st ( for n being Element of NAT holds a . n <= (b . n) + (c . n) ) & b is convergent & c is convergent & a is V41() holds ( a is convergent & lim a <= (lim b) + (lim c) ) proof let a, b, c be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds a . n <= (b . n) + (c . n) ) & b is convergent & c is convergent & a is V41() implies ( a is convergent & lim a <= (lim b) + (lim c) ) ) assume that A1: for n being Element of NAT holds a . n <= (b . n) + (c . n) and A2: ( b is convergent & c is convergent ) and A3: a is V41() ; ::_thesis: ( a is convergent & lim a <= (lim b) + (lim c) ) A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_a_._n_<=_(b_+_c)_._n let n be Element of NAT ; ::_thesis: a . n <= (b + c) . n a . n <= (b . n) + (c . n) by A1; hence a . n <= (b + c) . n by SEQ_1:7; ::_thesis: verum end; A5: b + c is convergent by A2; hence a is convergent by A3, A4, Th8; ::_thesis: lim a <= (lim b) + (lim c) lim (b + c) = (lim b) + (lim c) by A2, SEQ_2:6; hence lim a <= (lim b) + (lim c) by A3, A5, A4, Th8; ::_thesis: verum end; theorem Th10: :: HOLDER_1:10 for p being Real st 0 < p holds for a, ap being Real_Sequence st a is convergent & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = (a . n) to_power p ) holds ( ap is convergent & lim ap = (lim a) to_power p ) proof let p be Real; ::_thesis: ( 0 < p implies for a, ap being Real_Sequence st a is convergent & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = (a . n) to_power p ) holds ( ap is convergent & lim ap = (lim a) to_power p ) ) assume A1: 0 < p ; ::_thesis: for a, ap being Real_Sequence st a is convergent & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = (a . n) to_power p ) holds ( ap is convergent & lim ap = (lim a) to_power p ) let a, ap be Real_Sequence; ::_thesis: ( a is convergent & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = (a . n) to_power p ) implies ( ap is convergent & lim ap = (lim a) to_power p ) ) assume that A2: a is convergent and A3: for n being Element of NAT holds 0 <= a . n and A4: for n being Element of NAT holds ap . n = (a . n) to_power p ; ::_thesis: ( ap is convergent & lim ap = (lim a) to_power p ) now__::_thesis:_(_(_lim_a_=_0_&_ap_is_convergent_&_lim_ap_=_(lim_a)_to_power_p_)_or_(_lim_a_<>_0_&_ap_is_convergent_&_lim_ap_=_(lim_a)_to_power_p_)_) percases ( lim a = 0 or lim a <> 0 ) ; caseA5: lim a = 0 ; ::_thesis: ( ap is convergent & lim ap = (lim a) to_power p ) now__::_thesis:_(_(_ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ a_._m_=_0_&_ap_is_convergent_&_lim_ap_=_(lim_a)_to_power_p_)_or_(_(_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_ (_n_<=_m_&_a_._m_<>_0_)_)_&_ap_is_convergent_&_lim_ap_=_(lim_a)_to_power_p_)_) percases ( ex n being Element of NAT st for m being Element of NAT st n <= m holds a . m = 0 or for n being Element of NAT ex m being Element of NAT st ( n <= m & a . m <> 0 ) ) ; case ex n being Element of NAT st for m being Element of NAT st n <= m holds a . m = 0 ; ::_thesis: ( ap is convergent & lim ap = (lim a) to_power p ) then consider N being Element of NAT such that A6: for m being Element of NAT st N <= m holds a . m = 0 ; A7: for n being Element of NAT holds (a ^\ N) . n = 0 proof let n be Element of NAT ; ::_thesis: (a ^\ N) . n = 0 a . (n + N) = 0 by A6, NAT_1:12; hence (a ^\ N) . n = 0 by NAT_1:def_3; ::_thesis: verum end; A8: now__::_thesis:_for_e_being_real_number_st_e_>_0_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_(((ap_^\_N)_._m)_-_((lim_a)_to_power_p))_<_e let e be real number ; ::_thesis: ( e > 0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((ap ^\ N) . m) - ((lim a) to_power p)) < e ) assume A9: e > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((ap ^\ N) . m) - ((lim a) to_power p)) < e take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds abs (((ap ^\ N) . m) - ((lim a) to_power p)) < e let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((ap ^\ N) . m) - ((lim a) to_power p)) < e ) assume n <= m ; ::_thesis: abs (((ap ^\ N) . m) - ((lim a) to_power p)) < e A10: (lim a) to_power p = 0 by A1, A5, POWER:def_2; (ap ^\ N) . m = ap . (m + N) by NAT_1:def_3 .= (a . (m + N)) to_power p by A4 .= ((a ^\ N) . m) to_power p by NAT_1:def_3 .= 0 to_power p by A7 .= 0 by A1, POWER:def_2 ; hence abs (((ap ^\ N) . m) - ((lim a) to_power p)) < e by A9, A10, ABSVALUE:2; ::_thesis: verum end; then A11: ap ^\ N is convergent by SEQ_2:def_6; then (lim a) to_power p = lim (ap ^\ N) by A8, SEQ_2:def_7; hence ( ap is convergent & lim ap = (lim a) to_power p ) by A11, SEQ_4:20, SEQ_4:21; ::_thesis: verum end; caseA12: for n being Element of NAT ex m being Element of NAT st ( n <= m & a . m <> 0 ) ; ::_thesis: ( ap is convergent & lim ap = (lim a) to_power p ) defpred S1[ set ] means a . $1 <> 0 ; ex m1 being Element of NAT st ( 0 <= m1 & a . m1 <> 0 ) by A12; then A13: ex m being Nat st S1[m] ; consider M being Nat such that A14: ( S1[M] & ( for n being Nat st S1[n] holds M <= n ) ) from NAT_1:sch_5(A13); defpred S2[ set , set , set ] means for n, m being Element of NAT st $2 = n & $3 = m holds ( n < m & a . m <> 0 & ( for k being Element of NAT st n < k & a . k <> 0 holds m <= k ) ); A15: (lim a) to_power p = 0 by A1, A5, POWER:def_2; reconsider M = M as Element of NAT by ORDINAL1:def_12; A16: now__::_thesis:_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_ (_n_<_m_&_a_._m_<>_0_) let n be Element of NAT ; ::_thesis: ex m being Element of NAT st ( n < m & a . m <> 0 ) consider m being Element of NAT such that A17: ( n + 1 <= m & a . m <> 0 ) by A12; take m = m; ::_thesis: ( n < m & a . m <> 0 ) thus ( n < m & a . m <> 0 ) by A17, NAT_1:13; ::_thesis: verum end; A18: for n, x being Element of NAT ex y being Element of NAT st S2[n,x,y] proof let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S2[n,x,y] defpred S3[ Nat] means ( x < $1 & a . $1 <> 0 ); ex m being Element of NAT st S3[m] by A16; then A19: ex m being Nat st S3[m] ; consider l being Nat such that A20: ( S3[l] & ( for k being Nat st S3[k] holds l <= k ) ) from NAT_1:sch_5(A19); take l ; ::_thesis: ( l is Element of REAL & l is Element of NAT & S2[n,x,l] ) l in NAT by ORDINAL1:def_12; hence ( l is Element of REAL & l is Element of NAT & S2[n,x,l] ) by A20; ::_thesis: verum end; consider F being Function of NAT,NAT such that A21: ( F . 0 = M & ( for n being Element of NAT holds S2[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A18); A22: rng F c= NAT by RELAT_1:def_19; then A23: rng F c= REAL by XBOOLE_1:1; A24: dom F = NAT by FUNCT_2:def_1; then reconsider F = F as Real_Sequence by A23, RELSET_1:4; A25: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_Element_of_NAT let n be Element of NAT ; ::_thesis: F . n is Element of NAT F . n in rng F by A24, FUNCT_1:def_3; hence F . n is Element of NAT by A22; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_<_F_._(n_+_1) let n be Element of NAT ; ::_thesis: F . n < F . (n + 1) ( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A25; hence F . n < F . (n + 1) by A21; ::_thesis: verum end; then reconsider F = F as V39() sequence of NAT by SEQM_3:def_6; A26: for n being Element of NAT st a . n <> 0 holds ex m being Element of NAT st F . m = n proof defpred S3[ set ] means ( a . $1 <> 0 & ( for m being Element of NAT holds F . m <> $1 ) ); assume ex n being Element of NAT st S3[n] ; ::_thesis: contradiction then A27: ex n being Nat st S3[n] ; consider M1 being Nat such that A28: ( S3[M1] & ( for n being Nat st S3[n] holds M1 <= n ) ) from NAT_1:sch_5(A27); defpred S4[ Nat] means ( $1 < M1 & a . $1 <> 0 & ex m being Element of NAT st F . m = $1 ); A29: ex n being Nat st S4[n] proof take M ; ::_thesis: S4[M] ( M <= M1 & M <> M1 ) by A14, A21, A28; hence M < M1 by XXREAL_0:1; ::_thesis: ( a . M <> 0 & ex m being Element of NAT st F . m = M ) thus a . M <> 0 by A14; ::_thesis: ex m being Element of NAT st F . m = M take 0 ; ::_thesis: F . 0 = M thus F . 0 = M by A21; ::_thesis: verum end; A30: for n being Nat st S4[n] holds n <= M1 ; consider MX being Nat such that A31: ( S4[MX] & ( for n being Nat st S4[n] holds n <= MX ) ) from NAT_1:sch_6(A30, A29); A32: for k being Element of NAT st MX < k & k < M1 holds a . k = 0 proof given k being Element of NAT such that A33: MX < k and A34: ( k < M1 & a . k <> 0 ) ; ::_thesis: contradiction now__::_thesis:_(_(_ex_m_being_Element_of_NAT_st_F_._m_=_k_&_contradiction_)_or_(_(_for_m_being_Element_of_NAT_holds_F_._m_<>_k_)_&_contradiction_)_) percases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ; case ex m being Element of NAT st F . m = k ; ::_thesis: contradiction hence contradiction by A31, A33, A34; ::_thesis: verum end; case for m being Element of NAT holds F . m <> k ; ::_thesis: contradiction hence contradiction by A28, A34; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; consider m being Element of NAT such that A35: F . m = MX by A31; A36: ( MX < F . (m + 1) & a . (F . (m + 1)) <> 0 ) by A21, A35; M1 in NAT by ORDINAL1:def_12; then A37: F . (m + 1) <= M1 by A21, A28, A31, A35; now__::_thesis:_not_F_._(m_+_1)_<>_M1 assume F . (m + 1) <> M1 ; ::_thesis: contradiction then F . (m + 1) < M1 by A37, XXREAL_0:1; hence contradiction by A32, A36; ::_thesis: verum end; hence contradiction by A28; ::_thesis: verum end; A38: ( a * F is convergent & lim (a * F) = 0 ) by A2, A5, SEQ_4:16, SEQ_4:17; A39: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ abs_((ap_._m)_-_((lim_a)_to_power_p))_<_e let e be real number ; ::_thesis: ( 0 < e implies ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((ap . m) - ((lim a) to_power p)) < e ) assume A40: 0 < e ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds abs ((ap . m) - ((lim a) to_power p)) < e then 0 < e to_power (1 / p) by POWER:34; then consider n being Element of NAT such that A41: for m being Element of NAT st n <= m holds abs (((a * F) . m) - 0) < e to_power (1 / p) by A38, SEQ_2:def_7; take k = F . n; ::_thesis: for m being Element of NAT st k <= m holds abs ((ap . m) - ((lim a) to_power p)) < e let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((ap . m) - ((lim a) to_power p)) < e ) assume A42: k <= m ; ::_thesis: abs ((ap . m) - ((lim a) to_power p)) < e now__::_thesis:_(_(_a_._m_=_0_&_abs_((ap_._m)_-_((lim_a)_to_power_p))_<_e_)_or_(_a_._m_<>_0_&_abs_((ap_._m)_-_((lim_a)_to_power_p))_<_e_)_) percases ( a . m = 0 or a . m <> 0 ) ; case a . m = 0 ; ::_thesis: abs ((ap . m) - ((lim a) to_power p)) < e then ap . m = 0 to_power p by A4 .= 0 by A1, POWER:def_2 ; hence abs ((ap . m) - ((lim a) to_power p)) < e by A15, A40, ABSVALUE:2; ::_thesis: verum end; caseA43: a . m <> 0 ; ::_thesis: abs ((ap . m) - ((lim a) to_power p)) < e then consider l being Element of NAT such that A44: m = F . l by A26; n <= l by A42, A44, SEQM_3:1; then abs (((a * F) . l) - 0) < e to_power (1 / p) by A41; then A45: abs (a . (F . l)) < e to_power (1 / p) by FUNCT_2:15; A46: (a . m) to_power p = ap . m by A4; A47: a . m > 0 by A3, A43; then A48: 0 < ap . m by A46, POWER:34; abs (a . m) > 0 by A43, COMPLEX1:47; then (abs (a . m)) to_power p < (e to_power (1 / p)) to_power p by A1, A44, A45, POWER:37; then (abs (a . m)) to_power p < e to_power ((1 / p) * p) by A40, POWER:33; then (abs (a . m)) to_power p < e to_power 1 by A1, XCMPLX_1:106; then (abs (a . m)) to_power p < e by POWER:25; then ap . m < e by A47, A46, ABSVALUE:def_1; hence abs ((ap . m) - ((lim a) to_power p)) < e by A15, A48, ABSVALUE:def_1; ::_thesis: verum end; end; end; hence abs ((ap . m) - ((lim a) to_power p)) < e ; ::_thesis: verum end; hence ap is convergent by SEQ_2:def_6; ::_thesis: lim ap = (lim a) to_power p hence lim ap = (lim a) to_power p by A39, SEQ_2:def_7; ::_thesis: verum end; end; end; hence ( ap is convergent & lim ap = (lim a) to_power p ) ; ::_thesis: verum end; caseA49: lim a <> 0 ; ::_thesis: ( ap is convergent & lim ap = (lim a) to_power p ) A50: 0 <= lim a by A2, A3, SEQ_2:17; ex k being Element of NAT st rng (a ^\ k) c= dom (#R p) proof set e0 = lim a; A51: (lim a) / 2 > 0 by A49, A50, XREAL_1:215; then consider k being Element of NAT such that A52: for m being Element of NAT st k <= m holds abs ((a . m) - (lim a)) < (lim a) / 2 by A2, SEQ_2:def_7; take k ; ::_thesis: rng (a ^\ k) c= dom (#R p) A53: now__::_thesis:_for_m_being_Element_of_NAT_holds_0_<_(a_^\_k)_._m let m be Element of NAT ; ::_thesis: 0 < (a ^\ k) . m abs ((a . (k + m)) - (lim a)) < (lim a) / 2 by A52, NAT_1:12; then - ((lim a) / 2) <= (a . (k + m)) - (lim a) by ABSVALUE:5; then (- ((lim a) / 2)) + (lim a) <= ((a . (k + m)) - (lim a)) + (lim a) by XREAL_1:7; hence 0 < (a ^\ k) . m by A51, NAT_1:def_3; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_rng_(a_^\_k)_holds_ x_in_dom_(#R_p) let x be set ; ::_thesis: ( x in rng (a ^\ k) implies x in dom (#R p) ) assume x in rng (a ^\ k) ; ::_thesis: x in dom (#R p) then consider n being Element of NAT such that A54: x = (a ^\ k) . n by FUNCT_2:113; 0 < (a ^\ k) . n by A53; then (a ^\ k) . n in { g where g is Real : 0 < g } ; then (a ^\ k) . n in right_open_halfline 0 by XXREAL_1:230; hence x in dom (#R p) by A54, TAYLOR_1:def_4; ::_thesis: verum end; hence rng (a ^\ k) c= dom (#R p) by TARSKI:def_3; ::_thesis: verum end; then consider k being Element of NAT such that A55: rng (a ^\ k) c= dom (#R p) ; now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ ((#R_p)_/*_(a_^\_k))_._x_=_(ap_^\_k)_._x let x be set ; ::_thesis: ( x in NAT implies ((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x ) assume x in NAT ; ::_thesis: ((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x then reconsider n = x as Element of NAT ; (a ^\ k) . n in rng (a ^\ k) by VALUED_0:28; then (a ^\ k) . n in dom (#R p) by A55; then A56: (a ^\ k) . n in right_open_halfline 0 by TAYLOR_1:def_4; then a . (k + n) in right_open_halfline 0 by NAT_1:def_3; then a . (k + n) in { g where g is Real : 0 < g } by XXREAL_1:230; then A57: ex g being Real st ( a . (k + n) = g & g > 0 ) ; thus ((#R p) /* (a ^\ k)) . x = (#R p) . ((a ^\ k) . n) by A55, FUNCT_2:108 .= ((a ^\ k) . n) #R p by A56, TAYLOR_1:def_4 .= (a . (k + n)) #R p by NAT_1:def_3 .= (a . (k + n)) to_power p by A57, POWER:def_2 .= ap . (k + n) by A4 .= (ap ^\ k) . x by NAT_1:def_3 ; ::_thesis: verum end; then A58: (#R p) /* (a ^\ k) = ap ^\ k by FUNCT_2:12; A59: lim (a ^\ k) = lim a by A2, SEQ_4:20; lim a > 0 by A2, A3, A49, SEQ_2:17; then #R p is_continuous_in lim (a ^\ k) by A59, FDIFF_1:24, TAYLOR_1:21; then A60: ( (#R p) /* (a ^\ k) is convergent & (#R p) . (lim (a ^\ k)) = lim ((#R p) /* (a ^\ k)) ) by A2, A55, FCONT_1:def_1; lim a in { g where g is Real : 0 < g } by A49, A50; then lim a in right_open_halfline 0 by XXREAL_1:230; then (#R p) . (lim (a ^\ k)) = (lim a) #R p by A59, TAYLOR_1:def_4 .= (lim a) to_power p by A49, A50, POWER:def_2 ; hence ( ap is convergent & lim ap = (lim a) to_power p ) by A60, A58, SEQ_4:21, SEQ_4:22; ::_thesis: verum end; end; end; hence ( ap is convergent & lim ap = (lim a) to_power p ) ; ::_thesis: verum end; theorem :: HOLDER_1:11 for p being Real st 0 < p holds for a, ap being Real_Sequence st a is summable & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = ((Partial_Sums a) . n) to_power p ) holds ( ap is convergent & lim ap = (Sum a) to_power p & ap is V41() & ( for n being Element of NAT holds ap . n <= (Sum a) to_power p ) ) proof let p be Real; ::_thesis: ( 0 < p implies for a, ap being Real_Sequence st a is summable & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = ((Partial_Sums a) . n) to_power p ) holds ( ap is convergent & lim ap = (Sum a) to_power p & ap is V41() & ( for n being Element of NAT holds ap . n <= (Sum a) to_power p ) ) ) assume A1: 0 < p ; ::_thesis: for a, ap being Real_Sequence st a is summable & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = ((Partial_Sums a) . n) to_power p ) holds ( ap is convergent & lim ap = (Sum a) to_power p & ap is V41() & ( for n being Element of NAT holds ap . n <= (Sum a) to_power p ) ) let a, ap be Real_Sequence; ::_thesis: ( a is summable & ( for n being Element of NAT holds 0 <= a . n ) & ( for n being Element of NAT holds ap . n = ((Partial_Sums a) . n) to_power p ) implies ( ap is convergent & lim ap = (Sum a) to_power p & ap is V41() & ( for n being Element of NAT holds ap . n <= (Sum a) to_power p ) ) ) assume that A2: a is summable and A3: for n being Element of NAT holds 0 <= a . n and A4: for n being Element of NAT holds ap . n = ((Partial_Sums a) . n) to_power p ; ::_thesis: ( ap is convergent & lim ap = (Sum a) to_power p & ap is V41() & ( for n being Element of NAT holds ap . n <= (Sum a) to_power p ) ) A5: ( Partial_Sums a is convergent & ( for n being Element of NAT holds 0 <= (Partial_Sums a) . n ) ) by A2, A3, Lm2, SERIES_1:def_2; then lim ap = (lim (Partial_Sums a)) to_power p by A1, A4, Th10; hence A6: ( ap is convergent & lim ap = (Sum a) to_power p ) by A1, A4, A5, Th10, SERIES_1:def_3; ::_thesis: ( ap is V41() & ( for n being Element of NAT holds ap . n <= (Sum a) to_power p ) ) A7: Partial_Sums a is V41() by A3, SERIES_1:16; now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ ap_._n_<=_ap_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies ap . n <= ap . m ) assume n <= m ; ::_thesis: ap . n <= ap . m then A8: (Partial_Sums a) . n <= (Partial_Sums a) . m by A7, SEQM_3:6; A9: ( ap . n = ((Partial_Sums a) . n) to_power p & ap . m = ((Partial_Sums a) . m) to_power p ) by A4; 0 <= (Partial_Sums a) . n by A3, Lm2; hence ap . n <= ap . m by A1, A9, A8, Th3; ::_thesis: verum end; hence A10: ap is V41() by SEQM_3:6; ::_thesis: for n being Element of NAT holds ap . n <= (Sum a) to_power p thus for n being Element of NAT holds ap . n <= (Sum a) to_power p by A6, A10, SEQ_4:37; ::_thesis: verum end; theorem :: HOLDER_1:12 for p, q being Real st 1 < p & (1 / p) + (1 / q) = 1 holds for a, b, ap, bq, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) & ap is summable & bq is summable holds ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) proof let p, q be Real; ::_thesis: ( 1 < p & (1 / p) + (1 / q) = 1 implies for a, b, ap, bq, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) & ap is summable & bq is summable holds ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) ) assume that A1: 1 < p and A2: (1 / p) + (1 / q) = 1 ; ::_thesis: for a, b, ap, bq, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) & ap is summable & bq is summable holds ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) let a, b, ap, bq, ab be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) ) & ap is summable & bq is summable implies ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) ) assume that A3: for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bq . n = (abs (b . n)) to_power q & ab . n = abs ((a . n) * (b . n)) ) and A4: ap is summable and A5: bq is summable ; ::_thesis: ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) A6: Partial_Sums ap is convergent by A4, SERIES_1:def_2; reconsider pp = 1 / p as Real ; 1 / p < 1 by A1, XREAL_1:189; then A7: 1 - 1 < 1 - pp by XREAL_1:15; then A8: 0 < q by A2; for n being Element of NAT holds 0 <= bq . n proof let n be Element of NAT ; ::_thesis: 0 <= bq . n A9: bq . n = (abs (b . n)) to_power q by A3; now__::_thesis:_(_(_abs_(b_._n)_=_0_&_0_<=_bq_._n_)_or_(_abs_(b_._n)_>_0_&_0_<=_bq_._n_)_) percases ( abs (b . n) = 0 or abs (b . n) > 0 ) by COMPLEX1:46; case abs (b . n) = 0 ; ::_thesis: 0 <= bq . n hence 0 <= bq . n by A8, A9, POWER:def_2; ::_thesis: verum end; case abs (b . n) > 0 ; ::_thesis: 0 <= bq . n hence 0 <= bq . n by A9, POWER:34; ::_thesis: verum end; end; end; hence 0 <= bq . n ; ::_thesis: verum end; then A10: for n being Element of NAT holds 0 <= (Partial_Sums bq) . n by Lm2; for n being Element of NAT holds 0 <= ab . n proof let n be Element of NAT ; ::_thesis: 0 <= ab . n ab . n = abs ((a . n) * (b . n)) by A3; hence 0 <= ab . n by COMPLEX1:46; ::_thesis: verum end; then A11: Partial_Sums ab is V41() by SERIES_1:16; deffunc H1( Element of NAT ) -> Element of REAL = ((Partial_Sums bq) . $1) to_power (1 / q); consider y being Real_Sequence such that A12: for n being Element of NAT holds y . n = H1(n) from SEQ_1:sch_1(); for n being Element of NAT holds 0 <= ap . n proof let n be Element of NAT ; ::_thesis: 0 <= ap . n A13: ap . n = (abs (a . n)) to_power p by A3; now__::_thesis:_(_(_abs_(a_._n)_=_0_&_0_<=_ap_._n_)_or_(_abs_(a_._n)_>_0_&_0_<=_ap_._n_)_) percases ( abs (a . n) = 0 or abs (a . n) > 0 ) by COMPLEX1:46; case abs (a . n) = 0 ; ::_thesis: 0 <= ap . n hence 0 <= ap . n by A1, A13, POWER:def_2; ::_thesis: verum end; case abs (a . n) > 0 ; ::_thesis: 0 <= ap . n hence 0 <= ap . n by A13, POWER:34; ::_thesis: verum end; end; end; hence 0 <= ap . n ; ::_thesis: verum end; then A14: for n being Element of NAT holds 0 <= (Partial_Sums ap) . n by Lm2; deffunc H2( Element of NAT ) -> Element of REAL = ((Partial_Sums ap) . $1) to_power (1 / p); consider x being Real_Sequence such that A15: for n being Element of NAT holds x . n = H2(n) from SEQ_1:sch_1(); A16: for n being Element of NAT holds (Partial_Sums ab) . n <= (x (#) y) . n proof let n be Element of NAT ; ::_thesis: (Partial_Sums ab) . n <= (x (#) y) . n A17: y . n = ((Partial_Sums bq) . n) to_power (1 / q) by A12; ( (Partial_Sums ab) . n <= (((Partial_Sums ap) . n) to_power (1 / p)) * (((Partial_Sums bq) . n) to_power (1 / q)) & x . n = ((Partial_Sums ap) . n) to_power (1 / p) ) by A1, A2, A3, A15, Th6; hence (Partial_Sums ab) . n <= (x (#) y) . n by A17, SEQ_1:8; ::_thesis: verum end; A18: 1 / p > 0 by A1, XREAL_1:139; then A19: x is convergent by A15, A6, A14, Th10; A20: Partial_Sums bq is convergent by A5, SERIES_1:def_2; then A21: y is convergent by A2, A7, A12, A10, Th10; then x (#) y is convergent by A19; then A22: ( Partial_Sums ab is convergent & lim (Partial_Sums ab) <= lim (x (#) y) ) by A16, A11, Th8; Sum ap = lim (Partial_Sums ap) by SERIES_1:def_3; then A23: lim x = (Sum ap) to_power (1 / p) by A18, A15, A6, A14, Th10; Sum bq = lim (Partial_Sums bq) by SERIES_1:def_3; then lim y = (Sum bq) to_power (1 / q) by A2, A7, A12, A20, A10, Th10; then lim (x (#) y) = ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) by A19, A23, A21, SEQ_2:15; hence ( ab is summable & Sum ab <= ((Sum ap) to_power (1 / p)) * ((Sum bq) to_power (1 / q)) ) by A22, SERIES_1:def_2, SERIES_1:def_3; ::_thesis: verum end; theorem :: HOLDER_1:13 for p being Real st 1 < p holds for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) & ap is summable & bp is summable holds ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) proof let p be Real; ::_thesis: ( 1 < p implies for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) & ap is summable & bp is summable holds ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) ) assume A1: 1 < p ; ::_thesis: for a, b, ap, bp, ab being Real_Sequence st ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) & ap is summable & bp is summable holds ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) A2: 1 / p > 0 by A1, XREAL_1:139; let a, b, ap, bp, ab be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) ) & ap is summable & bp is summable implies ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) ) assume that A3: for n being Element of NAT holds ( ap . n = (abs (a . n)) to_power p & bp . n = (abs (b . n)) to_power p & ab . n = (abs ((a . n) + (b . n))) to_power p ) and A4: ap is summable and A5: bp is summable ; ::_thesis: ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) deffunc H1( Element of NAT ) -> Element of REAL = ((Partial_Sums ab) . $1) to_power (1 / p); consider z being Real_Sequence such that A6: for n being Element of NAT holds z . n = H1(n) from SEQ_1:sch_1(); A7: for n being Element of NAT holds 0 <= ab . n proof let n be Element of NAT ; ::_thesis: 0 <= ab . n A8: ab . n = (abs ((a . n) + (b . n))) to_power p by A3; percases ( abs ((a . n) + (b . n)) = 0 or abs ((a . n) + (b . n)) > 0 ) by COMPLEX1:46; suppose abs ((a . n) + (b . n)) = 0 ; ::_thesis: 0 <= ab . n hence 0 <= ab . n by A1, A8, POWER:def_2; ::_thesis: verum end; suppose abs ((a . n) + (b . n)) > 0 ; ::_thesis: 0 <= ab . n hence 0 <= ab . n by A8, POWER:34; ::_thesis: verum end; end; end; A9: for n being Element of NAT holds 0 <= z . n proof let n be Element of NAT ; ::_thesis: 0 <= z . n A10: z . n = ((Partial_Sums ab) . n) to_power (1 / p) by A6; percases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n > 0 ) by A7, Lm2; suppose (Partial_Sums ab) . n = 0 ; ::_thesis: 0 <= z . n hence 0 <= z . n by A2, A10, POWER:def_2; ::_thesis: verum end; suppose (Partial_Sums ab) . n > 0 ; ::_thesis: 0 <= z . n hence 0 <= z . n by A10, POWER:34; ::_thesis: verum end; end; end; A11: Partial_Sums ab is V41() by A7, SERIES_1:16; A12: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ ((Partial_Sums_ab)_._n)_to_power_(1_/_p)_<=_((Partial_Sums_ab)_._m)_to_power_(1_/_p) let n, m be Element of NAT ; ::_thesis: ( n <= m implies ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ) assume n <= m ; ::_thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) then A13: (Partial_Sums ab) . n <= (Partial_Sums ab) . m by A11, SEQM_3:6; A14: 0 <= ((Partial_Sums ab) . m) to_power (1 / p) proof percases ( (Partial_Sums ab) . m = 0 or (Partial_Sums ab) . m > 0 ) by A7, Lm2; suppose (Partial_Sums ab) . m = 0 ; ::_thesis: 0 <= ((Partial_Sums ab) . m) to_power (1 / p) hence 0 <= ((Partial_Sums ab) . m) to_power (1 / p) by A2, POWER:def_2; ::_thesis: verum end; suppose (Partial_Sums ab) . m > 0 ; ::_thesis: 0 <= ((Partial_Sums ab) . m) to_power (1 / p) hence 0 <= ((Partial_Sums ab) . m) to_power (1 / p) by POWER:34; ::_thesis: verum end; end; end; now__::_thesis:_(_(_(Partial_Sums_ab)_._n_=_(Partial_Sums_ab)_._m_&_((Partial_Sums_ab)_._n)_to_power_(1_/_p)_<=_((Partial_Sums_ab)_._m)_to_power_(1_/_p)_)_or_(_(Partial_Sums_ab)_._n_<>_(Partial_Sums_ab)_._m_&_((Partial_Sums_ab)_._n)_to_power_(1_/_p)_<=_((Partial_Sums_ab)_._m)_to_power_(1_/_p)_)_) percases ( (Partial_Sums ab) . n = (Partial_Sums ab) . m or (Partial_Sums ab) . n <> (Partial_Sums ab) . m ) ; case (Partial_Sums ab) . n = (Partial_Sums ab) . m ; ::_thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ; ::_thesis: verum end; case (Partial_Sums ab) . n <> (Partial_Sums ab) . m ; ::_thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) then A15: (Partial_Sums ab) . n < (Partial_Sums ab) . m by A13, XXREAL_0:1; now__::_thesis:_(_(_(Partial_Sums_ab)_._n_=_0_&_((Partial_Sums_ab)_._n)_to_power_(1_/_p)_<=_((Partial_Sums_ab)_._m)_to_power_(1_/_p)_)_or_(_(Partial_Sums_ab)_._n_<>_0_&_((Partial_Sums_ab)_._n)_to_power_(1_/_p)_<=_((Partial_Sums_ab)_._m)_to_power_(1_/_p)_)_) percases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n <> 0 ) ; case (Partial_Sums ab) . n = 0 ; ::_thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) by A2, A14, POWER:def_2; ::_thesis: verum end; caseA16: (Partial_Sums ab) . n <> 0 ; ::_thesis: ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) 0 <= (Partial_Sums ab) . n by A7, Lm2; hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) by A2, A15, A16, POWER:37; ::_thesis: verum end; end; end; hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ; ::_thesis: verum end; end; end; hence ((Partial_Sums ab) . n) to_power (1 / p) <= ((Partial_Sums ab) . m) to_power (1 / p) ; ::_thesis: verum end; now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ z_._n_<=_z_._m let n, m be Element of NAT ; ::_thesis: ( n <= m implies z . n <= z . m ) assume A17: n <= m ; ::_thesis: z . n <= z . m ( z . n = ((Partial_Sums ab) . n) to_power (1 / p) & z . m = ((Partial_Sums ab) . m) to_power (1 / p) ) by A6; hence z . n <= z . m by A12, A17; ::_thesis: verum end; then A18: z is V41() by SEQM_3:6; for n being Element of NAT holds 0 <= ap . n proof let n be Element of NAT ; ::_thesis: 0 <= ap . n A19: ap . n = (abs (a . n)) to_power p by A3; now__::_thesis:_(_(_abs_(a_._n)_=_0_&_0_<=_ap_._n_)_or_(_abs_(a_._n)_>_0_&_0_<=_ap_._n_)_) percases ( abs (a . n) = 0 or abs (a . n) > 0 ) by COMPLEX1:46; case abs (a . n) = 0 ; ::_thesis: 0 <= ap . n hence 0 <= ap . n by A1, A19, POWER:def_2; ::_thesis: verum end; case abs (a . n) > 0 ; ::_thesis: 0 <= ap . n hence 0 <= ap . n by A19, POWER:34; ::_thesis: verum end; end; end; hence 0 <= ap . n ; ::_thesis: verum end; then A20: for n being Element of NAT holds 0 <= (Partial_Sums ap) . n by Lm2; deffunc H2( Element of NAT ) -> Element of REAL = ((Partial_Sums ap) . $1) to_power (1 / p); consider x being Real_Sequence such that A21: for n being Element of NAT holds x . n = H2(n) from SEQ_1:sch_1(); for n being Element of NAT holds 0 <= bp . n proof let n be Element of NAT ; ::_thesis: 0 <= bp . n A22: bp . n = (abs (b . n)) to_power p by A3; now__::_thesis:_(_(_abs_(b_._n)_=_0_&_0_<=_bp_._n_)_or_(_abs_(b_._n)_>_0_&_0_<=_bp_._n_)_) percases ( abs (b . n) = 0 or abs (b . n) > 0 ) by COMPLEX1:46; case abs (b . n) = 0 ; ::_thesis: 0 <= bp . n hence 0 <= bp . n by A1, A22, POWER:def_2; ::_thesis: verum end; case abs (b . n) > 0 ; ::_thesis: 0 <= bp . n hence 0 <= bp . n by A22, POWER:34; ::_thesis: verum end; end; end; hence 0 <= bp . n ; ::_thesis: verum end; then A23: for n being Element of NAT holds 0 <= (Partial_Sums bp) . n by Lm2; deffunc H3( Element of NAT ) -> Element of REAL = ((Partial_Sums bp) . $1) to_power (1 / p); consider y being Real_Sequence such that A24: for n being Element of NAT holds y . n = H3(n) from SEQ_1:sch_1(); A25: Partial_Sums bp is convergent by A5, SERIES_1:def_2; then A26: y is convergent by A2, A24, A23, Th10; A27: Partial_Sums ap is convergent by A4, SERIES_1:def_2; then A28: x is convergent by A2, A21, A20, Th10; A29: for n being Element of NAT holds z . n <= (x . n) + (y . n) proof let n be Element of NAT ; ::_thesis: z . n <= (x . n) + (y . n) A30: y . n = ((Partial_Sums bp) . n) to_power (1 / p) by A24; ( ((Partial_Sums ab) . n) to_power (1 / p) <= (((Partial_Sums ap) . n) to_power (1 / p)) + (((Partial_Sums bp) . n) to_power (1 / p)) & x . n = ((Partial_Sums ap) . n) to_power (1 / p) ) by A1, A3, A21, Th7; hence z . n <= (x . n) + (y . n) by A6, A30; ::_thesis: verum end; then A31: z is convergent by A28, A26, A18, Th9; A32: for n being Element of NAT holds (z . n) to_power p = (Partial_Sums ab) . n proof let n be Element of NAT ; ::_thesis: (z . n) to_power p = (Partial_Sums ab) . n A33: z . n = ((Partial_Sums ab) . n) to_power (1 / p) by A6; now__::_thesis:_(_(_(Partial_Sums_ab)_._n_=_0_&_(z_._n)_to_power_p_=_(Partial_Sums_ab)_._n_)_or_(_(Partial_Sums_ab)_._n_<>_0_&_(z_._n)_to_power_p_=_(Partial_Sums_ab)_._n_)_) percases ( (Partial_Sums ab) . n = 0 or (Partial_Sums ab) . n <> 0 ) ; caseA34: (Partial_Sums ab) . n = 0 ; ::_thesis: (z . n) to_power p = (Partial_Sums ab) . n then z . n = 0 by A2, A33, POWER:def_2; hence (z . n) to_power p = (Partial_Sums ab) . n by A1, A34, POWER:def_2; ::_thesis: verum end; caseA35: (Partial_Sums ab) . n <> 0 ; ::_thesis: (z . n) to_power p = (Partial_Sums ab) . n 0 <= (Partial_Sums ab) . n by A7, Lm2; hence (z . n) to_power p = ((Partial_Sums ab) . n) to_power ((1 / p) * p) by A33, A35, POWER:33 .= ((Partial_Sums ab) . n) to_power 1 by A1, XCMPLX_1:106 .= (Partial_Sums ab) . n by POWER:25 ; ::_thesis: verum end; end; end; hence (z . n) to_power p = (Partial_Sums ab) . n ; ::_thesis: verum end; then lim (Partial_Sums ab) = (lim z) to_power p by A1, A9, A31, Th10; then A36: Sum ab = (lim z) to_power p by SERIES_1:def_3; A37: (Sum ab) to_power (1 / p) = lim z proof percases ( lim z = 0 or lim z <> 0 ) ; supposeA38: lim z = 0 ; ::_thesis: (Sum ab) to_power (1 / p) = lim z hence (Sum ab) to_power (1 / p) = 0 to_power (1 / p) by A1, A36, POWER:def_2 .= lim z by A2, A38, POWER:def_2 ; ::_thesis: verum end; suppose lim z <> 0 ; ::_thesis: (Sum ab) to_power (1 / p) = lim z then 0 < lim z by A9, A31, SEQ_2:17; hence (Sum ab) to_power (1 / p) = (lim z) to_power ((1 / p) * p) by A36, POWER:33 .= (lim z) to_power 1 by A1, XCMPLX_1:106 .= lim z by POWER:25 ; ::_thesis: verum end; end; end; Sum bp = lim (Partial_Sums bp) by SERIES_1:def_3; then A39: lim y = (Sum bp) to_power (1 / p) by A2, A24, A25, A23, Th10; Sum ap = lim (Partial_Sums ap) by SERIES_1:def_3; then A40: lim x = (Sum ap) to_power (1 / p) by A2, A21, A27, A20, Th10; Partial_Sums ab is convergent by A1, A9, A31, A32, Th10; hence ( ab is summable & (Sum ab) to_power (1 / p) <= ((Sum ap) to_power (1 / p)) + ((Sum bp) to_power (1 / p)) ) by A28, A40, A26, A39, A29, A18, A37, Th9, SERIES_1:def_2; ::_thesis: verum end;