:: SERIES_1 semantic presentation begin theorem Th1: :: SERIES_1:1 for a being real number for s being Real_Sequence st 0 < a & a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds ( s is convergent & lim s = 0 ) proof let a be real number ; ::_thesis: for s being Real_Sequence st 0 < a & a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds ( s is convergent & lim s = 0 ) let s be Real_Sequence; ::_thesis: ( 0 < a & a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) ) assume that A1: 0 < a and A2: a < 1 and A3: for n being Element of NAT holds s . n = a to_power (n + 1) ; ::_thesis: ( s is convergent & lim s = 0 ) set r = (1 / a) - 1; 1 / a > 1 / 1 by A1, A2, XREAL_1:88; then A4: (1 / a) - 1 > 0 by XREAL_1:50; A5: for p being real number st 0 < p holds ex m being Element of NAT st for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p proof let p be real number ; ::_thesis: ( 0 < p implies ex m being Element of NAT st for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p ) A6: 1 / (p * ((1 / a) - 1)) <= [\(1 / (p * ((1 / a) - 1)))/] + 1 by INT_1:29; assume A7: 0 < p ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p then p * ((1 / a) - 1) > 0 by A4; then 1 / (p * ((1 / a) - 1)) > 0 ; then [\(1 / (p * ((1 / a) - 1)))/] is Element of NAT by A6, INT_1:3, INT_1:7; then consider m being Element of NAT such that A8: m = [\(1 / (p * ((1 / a) - 1)))/] ; take m ; ::_thesis: for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p A9: 1 / (p * ((1 / a) - 1)) = (1 / p) / ((1 / a) - 1) by XCMPLX_1:78; now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_ abs_((s_._n)_-_0)_<_p A10: [\(1 / (p * ((1 / a) - 1)))/] > (1 / (p * ((1 / a) - 1))) - 1 by INT_1:def_6; let n be Element of NAT ; ::_thesis: ( m <= n implies abs ((s . n) - 0) < p ) assume m <= n ; ::_thesis: abs ((s . n) - 0) < p then n > (1 / (p * ((1 / a) - 1))) - 1 by A8, A10, XXREAL_0:2; then n + 1 > (1 / p) / ((1 / a) - 1) by A9, XREAL_1:19; then A11: (n + 1) * ((1 / a) - 1) > 1 / p by A4, XREAL_1:77; 0 + ((n + 1) * ((1 / a) - 1)) < 1 + ((n + 1) * ((1 / a) - 1)) by XREAL_1:6; then A12: 1 / p < 1 + ((n + 1) * ((1 / a) - 1)) by A11, XXREAL_0:2; A13: (1 + ((1 / a) - 1)) to_power (n + 1) = (1 to_power (n + 1)) / (a to_power (n + 1)) by A1, POWER:31 .= 1 / (a to_power (n + 1)) by POWER:26 ; a to_power (n + 1) > 0 by A1, POWER:34; then A14: abs (a to_power (n + 1)) = a to_power (n + 1) by ABSVALUE:def_1; 1 + ((n + 1) * ((1 / a) - 1)) <= (1 + ((1 / a) - 1)) to_power (n + 1) by A4, POWER:49; then 1 / p < 1 / (a to_power (n + 1)) by A13, A12, XXREAL_0:2; then abs (a to_power (n + 1)) < p by A7, A14, XREAL_1:91; hence abs ((s . n) - 0) < p by A3; ::_thesis: verum end; hence for n being Element of NAT st m <= n holds abs ((s . n) - 0) < p ; ::_thesis: verum end; hence s is convergent by SEQ_2:def_6; ::_thesis: lim s = 0 hence lim s = 0 by A5, SEQ_2:def_7; ::_thesis: verum end; theorem Th2: :: SERIES_1:2 for a being real number for n being Nat holds (abs a) to_power n = abs (a to_power n) proof let a be real number ; ::_thesis: for n being Nat holds (abs a) to_power n = abs (a to_power n) let n be Nat; ::_thesis: (abs a) to_power n = abs (a to_power n) percases ( a <> 0 or a = 0 ) ; supposeA1: a <> 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n) then A2: abs a > 0 by COMPLEX1:47; now__::_thesis:_(abs_a)_to_power_n_=_abs_(a_to_power_n) percases ( a > 0 or a < 0 ) by A1; suppose a > 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n) then ( a to_power n = (abs a) to_power n & a to_power n > 0 ) by ABSVALUE:def_1, POWER:34; hence (abs a) to_power n = abs (a to_power n) by ABSVALUE:def_1; ::_thesis: verum end; supposeA3: a < 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n) reconsider m = n as Integer ; now__::_thesis:_(abs_a)_to_power_n_=_abs_(a_to_power_n) percases ( m is even or m is odd ) ; supposeA4: m is even ; ::_thesis: (abs a) to_power n = abs (a to_power n) A5: (abs a) to_power n > 0 by A2, POWER:34; (abs a) to_power n = (- a) to_power m by A3, ABSVALUE:def_1 .= a to_power m by A4, POWER:47 ; hence (abs a) to_power n = abs (a to_power n) by A5, ABSVALUE:def_1; ::_thesis: verum end; supposeA6: m is odd ; ::_thesis: (abs a) to_power n = abs (a to_power n) A7: (abs a) to_power n > 0 by A2, POWER:34; (abs a) to_power n = (- a) to_power m by A3, ABSVALUE:def_1 .= - (a to_power m) by A6, POWER:48 ; hence (abs a) to_power n = abs (- (a to_power n)) by A7, ABSVALUE:def_1 .= abs (a to_power n) by COMPLEX1:52 ; ::_thesis: verum end; end; end; hence (abs a) to_power n = abs (a to_power n) ; ::_thesis: verum end; end; end; hence (abs a) to_power n = abs (a to_power n) ; ::_thesis: verum end; supposeA8: a = 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n) percases ( n = 0 or n > 0 ) ; suppose n = 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n) then a to_power n = 1 by NEWTON:4; hence (abs a) to_power n = abs (a to_power n) by A8, COMPLEX1:44, COMPLEX1:48; ::_thesis: verum end; suppose n > 0 ; ::_thesis: (abs a) to_power n = abs (a to_power n) then (abs a) to_power n = 0 by A8, COMPLEX1:44, POWER:def_2; hence (abs a) to_power n = abs (a to_power n) by A8, COMPLEX1:44; ::_thesis: verum end; end; end; end; end; theorem Th3: :: SERIES_1:3 for a being real number for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds ( s is convergent & lim s = 0 ) proof let a be real number ; ::_thesis: for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) holds ( s is convergent & lim s = 0 ) let s be Real_Sequence; ::_thesis: ( abs a < 1 & ( for n being Element of NAT holds s . n = a to_power (n + 1) ) implies ( s is convergent & lim s = 0 ) ) assume that A1: abs a < 1 and A2: for n being Element of NAT holds s . n = a to_power (n + 1) ; ::_thesis: ( s is convergent & lim s = 0 ) now__::_thesis:_(_s_is_convergent_&_lim_s_=_0_) percases ( abs a = 0 or not abs a = 0 ) ; suppose abs a = 0 ; ::_thesis: ( s is convergent & lim s = 0 ) then A3: a = 0 by ABSVALUE:2; now__::_thesis:_for_n_being_Nat_holds_s_._n_=_0 let n be Nat; ::_thesis: s . n = 0 ( n in NAT & a to_power (n + 1) = 0 ) by A3, ORDINAL1:def_12, POWER:def_2; hence s . n = 0 by A2; ::_thesis: verum end; then ( s is constant & s . 0 = 0 ) by VALUED_0:def_18; hence ( s is convergent & lim s = 0 ) by SEQ_4:26; ::_thesis: verum end; supposeA4: not abs a = 0 ; ::_thesis: ( s is convergent & lim s = 0 ) deffunc H1( Element of NAT ) -> Element of REAL = (abs a) to_power ($1 + 1); consider s1 being Real_Sequence such that A5: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch_1(); A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_abs_(s_._n) let n be Element of NAT ; ::_thesis: s1 . n = abs (s . n) thus s1 . n = (abs a) to_power (n + 1) by A5 .= abs (a to_power (n + 1)) by Th2 .= abs (s . n) by A2 ; ::_thesis: verum end; A7: abs a > 0 by A4, COMPLEX1:46; then lim s1 = 0 by A1, A5, Th1; then A8: lim (abs s) = 0 by A6, SEQ_1:12; s1 is convergent by A1, A7, A5, Th1; then abs s is convergent by A6, SEQ_1:12; hence ( s is convergent & lim s = 0 ) by A8, SEQ_4:15; ::_thesis: verum end; end; end; hence ( s is convergent & lim s = 0 ) ; ::_thesis: verum end; definition let X be non empty complex-membered add-closed set ; let s1, s2 be sequence of X; :: original: + redefine funcs1 + s2 -> sequence of X; coherence s1 + s2 is sequence of X proof A1: dom (s1 + s2) = (dom s1) /\ (dom s2) by VALUED_1:def_1 .= NAT /\ (dom s2) by FUNCT_2:def_1 .= NAT /\ NAT by FUNCT_2:def_1 ; now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ (s1_+_s2)_._x_in_X let x be set ; ::_thesis: ( x in NAT implies (s1 + s2) . x in X ) assume A2: x in NAT ; ::_thesis: (s1 + s2) . x in X A3: ( s1 . x in X & s2 . x in X ) by A2, FUNCT_2:5; (s1 + s2) . x = (s1 . x) + (s2 . x) by A1, A2, VALUED_1:def_1; hence (s1 + s2) . x in X by A3, MEMBERED:def_25; ::_thesis: verum end; hence s1 + s2 is sequence of X by A1, FUNCT_2:3; ::_thesis: verum end; end; definition let s be complex-valued ManySortedSet of NAT ; func Partial_Sums s -> complex-valued ManySortedSet of NAT means :Def1: :: SERIES_1:def 1 ( it . 0 = s . 0 & ( for n being Element of NAT holds it . (n + 1) = (it . n) + (s . (n + 1)) ) ); existence ex b1 being complex-valued ManySortedSet of NAT st ( b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) ) proof set X = COMPLEX ; A1: dom s = NAT by PARTFUN1:def_2; rng s c= COMPLEX by VALUED_0:def_1; then reconsider ss = s as Function of NAT,COMPLEX by A1, RELSET_1:4; defpred S1[ Nat, Element of COMPLEX , set ] means $3 = $2 + (ss . ($1 + 1)); A2: for n being Element of NAT for x being Element of COMPLEX ex y being Element of COMPLEX st S1[n,x,y] ; ex f being Function of NAT,COMPLEX st ( f . 0 = ss . 0 & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A2); hence ex b1 being complex-valued ManySortedSet of NAT st ( b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being complex-valued ManySortedSet of NAT st b1 . 0 = s . 0 & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) + (s . (n + 1)) ) & b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) holds b1 = b2 proof let s1, s2 be complex-valued ManySortedSet of NAT ; ::_thesis: ( s1 . 0 = s . 0 & ( for n being Element of NAT holds s1 . (n + 1) = (s1 . n) + (s . (n + 1)) ) & s2 . 0 = s . 0 & ( for n being Element of NAT holds s2 . (n + 1) = (s2 . n) + (s . (n + 1)) ) implies s1 = s2 ) assume that A3: s1 . 0 = s . 0 and A4: for n being Element of NAT holds s1 . (n + 1) = (s1 . n) + (s . (n + 1)) and A5: s2 . 0 = s . 0 and A6: for n being Element of NAT holds s2 . (n + 1) = (s2 . n) + (s . (n + 1)) ; ::_thesis: s1 = s2 defpred S1[ Element of NAT ] means s1 . $1 = s2 . $1; A7: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume s1 . k = s2 . k ; ::_thesis: S1[k + 1] hence s1 . (k + 1) = (s2 . k) + (s . (k + 1)) by A4 .= s2 . (k + 1) by A6 ; ::_thesis: verum end; A8: S1[ 0 ] by A3, A5; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A8, A7); :: according to PBOOLE:def_21 ::_thesis: verum end; end; :: deftheorem Def1 defines Partial_Sums SERIES_1:def_1_:_ for s, b2 being complex-valued ManySortedSet of NAT holds ( b2 = Partial_Sums s iff ( b2 . 0 = s . 0 & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) + (s . (n + 1)) ) ) ); registration let s be real-valued ManySortedSet of NAT ; cluster Partial_Sums s -> complex-valued real-valued ; coherence Partial_Sums s is real-valued proof set f = Partial_Sums s; let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (Partial_Sums s) or (Partial_Sums s) . x is real ) assume x in dom (Partial_Sums s) ; ::_thesis: (Partial_Sums s) . x is real then reconsider n = x as Element of NAT ; defpred S1[ Nat] means (Partial_Sums s) . s is real ; (Partial_Sums s) . 0 = s . 0 by Def1; then A1: S1[ 0 ] ; A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] reconsider k = k as Element of NAT by ORDINAL1:def_12; (Partial_Sums s) . (k + 1) = ((Partial_Sums s) . k) + (s . (k + 1)) by Def1; hence S1[k + 1] by A3; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2); then (Partial_Sums s) . n is real ; hence (Partial_Sums s) . x is real ; ::_thesis: verum end; end; definition let s be Real_Sequence; :: original: Partial_Sums redefine func Partial_Sums s -> Real_Sequence; coherence Partial_Sums s is Real_Sequence proof A1: dom (Partial_Sums s) = NAT by PARTFUN1:def_2; rng (Partial_Sums s) c= REAL by VALUED_0:def_3; then Partial_Sums s is Relation of NAT,REAL by A1, RELSET_1:4; hence Partial_Sums s is Real_Sequence ; ::_thesis: verum end; end; definition let s be Real_Sequence; attrs is summable means :Def2: :: SERIES_1:def 2 Partial_Sums s is convergent ; func Sum s -> Real equals :: SERIES_1:def 3 lim (Partial_Sums s); correctness coherence lim (Partial_Sums s) is Real; ; end; :: deftheorem Def2 defines summable SERIES_1:def_2_:_ for s being Real_Sequence holds ( s is summable iff Partial_Sums s is convergent ); :: deftheorem defines Sum SERIES_1:def_3_:_ for s being Real_Sequence holds Sum s = lim (Partial_Sums s); theorem Th4: :: SERIES_1:4 for s being Real_Sequence st s is summable holds ( s is convergent & lim s = 0 ) proof let s be Real_Sequence; ::_thesis: ( s is summable implies ( s is convergent & lim s = 0 ) ) assume s is summable ; ::_thesis: ( s is convergent & lim s = 0 ) then A1: Partial_Sums s is convergent by Def2; now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s)_^\_1)_._n_=_((Partial_Sums_s)_._n)_+_((s_^\_1)_._n) let n be Element of NAT ; ::_thesis: ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n) (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by Def1; then (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def_3; hence ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def_3; ::_thesis: verum end; then A2: (Partial_Sums s) ^\ 1 = (Partial_Sums s) + (s ^\ 1) by SEQ_1:7; now__::_thesis:_for_n_being_Element_of_NAT_holds_((s_^\_1)_+_((Partial_Sums_s)_-_(Partial_Sums_s)))_._n_=_(s_^\_1)_._n let n be Element of NAT ; ::_thesis: ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = (s ^\ 1) . n thus ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = ((s ^\ 1) . n) + (((Partial_Sums s) + (- (Partial_Sums s))) . n) by SEQ_1:7 .= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + ((- (Partial_Sums s)) . n)) by SEQ_1:7 .= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + (- ((Partial_Sums s) . n))) by SEQ_1:10 .= (s ^\ 1) . n ; ::_thesis: verum end; then (s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s)) = s ^\ 1 by FUNCT_2:63; then A3: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by A2, SEQ_1:31; then A4: s ^\ 1 is convergent by A1; hence s is convergent by SEQ_4:21; ::_thesis: lim s = 0 lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) by A1, SEQ_4:20; then lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, SEQ_2:12 .= 0 ; hence lim s = 0 by A3, A4, SEQ_4:22; ::_thesis: verum end; Lm1: for seq, seq1, seq2 being complex-valued ManySortedSet of NAT holds ( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) proof let seq, seq1, seq2 be complex-valued ManySortedSet of NAT ; ::_thesis: ( seq = seq1 + seq2 iff for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) thus ( seq = seq1 + seq2 implies for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ) implies seq = seq1 + seq2 ) proof assume A1: seq = seq1 + seq2 ; ::_thesis: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) let n be Element of NAT ; ::_thesis: seq . n = (seq1 . n) + (seq2 . n) dom seq = NAT by PARTFUN1:def_2; hence seq . n = (seq1 . n) + (seq2 . n) by A1, VALUED_1:def_1; ::_thesis: verum end; assume for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ; ::_thesis: seq = seq1 + seq2 then A2: for n being set st n in dom seq holds seq . n = (seq1 . n) + (seq2 . n) ; dom seq = NAT /\ NAT by PARTFUN1:def_2 .= NAT /\ (dom seq2) by PARTFUN1:def_2 .= (dom seq1) /\ (dom seq2) by PARTFUN1:def_2 ; hence seq = seq1 + seq2 by A2, VALUED_1:def_1; ::_thesis: verum end; theorem Th5: :: SERIES_1:5 for X being non empty complex-membered add-closed set for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) proof let X be non empty complex-membered add-closed set ; ::_thesis: for s1, s2 being sequence of X holds (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) let s1, s2 be sequence of X; ::_thesis: (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s1)_+_(Partial_Sums_s2))_._(n_+_1)_=_(((Partial_Sums_s1)_+_(Partial_Sums_s2))_._n)_+_((s1_+_s2)_._(n_+_1)) let n be Element of NAT ; ::_thesis: ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1)) thus ((Partial_Sums s1) + (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) + ((Partial_Sums s2) . (n + 1)) by Lm1 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((Partial_Sums s2) . (n + 1)) by Def1 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) + ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by Def1 .= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) + (s2 . (n + 1)))) + ((Partial_Sums s2) . n) .= (((Partial_Sums s1) . n) + ((s1 + s2) . (n + 1))) + ((Partial_Sums s2) . n) by Lm1 .= (((Partial_Sums s1) . n) + ((Partial_Sums s2) . n)) + ((s1 + s2) . (n + 1)) .= (((Partial_Sums s1) + (Partial_Sums s2)) . n) + ((s1 + s2) . (n + 1)) by Lm1 ; ::_thesis: verum end; ((Partial_Sums s1) + (Partial_Sums s2)) . 0 = ((Partial_Sums s1) . 0) + ((Partial_Sums s2) . 0) by Lm1 .= (s1 . 0) + ((Partial_Sums s2) . 0) by Def1 .= (s1 . 0) + (s2 . 0) by Def1 .= (s1 + s2) . 0 by Lm1 ; hence (Partial_Sums s1) + (Partial_Sums s2) = Partial_Sums (s1 + s2) by A1, Def1; ::_thesis: verum end; theorem Th6: :: SERIES_1:6 for s1, s2 being Real_Sequence holds (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) proof let s1, s2 be Real_Sequence; ::_thesis: (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_((Partial_Sums_s1)_-_(Partial_Sums_s2))_._(n_+_1)_=_(((Partial_Sums_s1)_-_(Partial_Sums_s2))_._n)_+_((s1_-_s2)_._(n_+_1)) let n be Element of NAT ; ::_thesis: ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1)) thus ((Partial_Sums s1) - (Partial_Sums s2)) . (n + 1) = ((Partial_Sums s1) . (n + 1)) - ((Partial_Sums s2) . (n + 1)) by RFUNCT_2:1 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((Partial_Sums s2) . (n + 1)) by Def1 .= (((Partial_Sums s1) . n) + (s1 . (n + 1))) - ((s2 . (n + 1)) + ((Partial_Sums s2) . n)) by Def1 .= (((Partial_Sums s1) . n) + ((s1 . (n + 1)) - (s2 . (n + 1)))) - ((Partial_Sums s2) . n) .= (((s1 - s2) . (n + 1)) + ((Partial_Sums s1) . n)) - ((Partial_Sums s2) . n) by RFUNCT_2:1 .= ((s1 - s2) . (n + 1)) + (((Partial_Sums s1) . n) - ((Partial_Sums s2) . n)) .= (((Partial_Sums s1) - (Partial_Sums s2)) . n) + ((s1 - s2) . (n + 1)) by RFUNCT_2:1 ; ::_thesis: verum end; ((Partial_Sums s1) - (Partial_Sums s2)) . 0 = ((Partial_Sums s1) . 0) - ((Partial_Sums s2) . 0) by RFUNCT_2:1 .= (s1 . 0) - ((Partial_Sums s2) . 0) by Def1 .= (s1 . 0) - (s2 . 0) by Def1 .= (s1 - s2) . 0 by RFUNCT_2:1 ; hence (Partial_Sums s1) - (Partial_Sums s2) = Partial_Sums (s1 - s2) by A1, Def1; ::_thesis: verum end; theorem :: SERIES_1:7 for s1, s2 being Real_Sequence st s1 is summable & s2 is summable holds ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) ) proof let s1, s2 be Real_Sequence; ::_thesis: ( s1 is summable & s2 is summable implies ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) ) ) assume ( s1 is summable & s2 is summable ) ; ::_thesis: ( s1 + s2 is summable & Sum (s1 + s2) = (Sum s1) + (Sum s2) ) then A1: ( Partial_Sums s1 is convergent & Partial_Sums s2 is convergent ) by Def2; then (Partial_Sums s1) + (Partial_Sums s2) is convergent ; then Partial_Sums (s1 + s2) is convergent by Th5; hence s1 + s2 is summable by Def2; ::_thesis: Sum (s1 + s2) = (Sum s1) + (Sum s2) thus Sum (s1 + s2) = lim ((Partial_Sums s1) + (Partial_Sums s2)) by Th5 .= (Sum s1) + (Sum s2) by A1, SEQ_2:6 ; ::_thesis: verum end; theorem :: SERIES_1:8 for s1, s2 being Real_Sequence st s1 is summable & s2 is summable holds ( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) ) proof let s1, s2 be Real_Sequence; ::_thesis: ( s1 is summable & s2 is summable implies ( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) ) ) assume ( s1 is summable & s2 is summable ) ; ::_thesis: ( s1 - s2 is summable & Sum (s1 - s2) = (Sum s1) - (Sum s2) ) then A1: ( Partial_Sums s1 is convergent & Partial_Sums s2 is convergent ) by Def2; then (Partial_Sums s1) - (Partial_Sums s2) is convergent ; then Partial_Sums (s1 - s2) is convergent by Th6; hence s1 - s2 is summable by Def2; ::_thesis: Sum (s1 - s2) = (Sum s1) - (Sum s2) thus Sum (s1 - s2) = lim ((Partial_Sums s1) - (Partial_Sums s2)) by Th6 .= (Sum s1) - (Sum s2) by A1, SEQ_2:12 ; ::_thesis: verum end; theorem Th9: :: SERIES_1:9 for r being real number for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s) proof let r be real number ; ::_thesis: for s being Real_Sequence holds Partial_Sums (r (#) s) = r (#) (Partial_Sums s) let s be Real_Sequence; ::_thesis: Partial_Sums (r (#) s) = r (#) (Partial_Sums s) A1: now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(Partial_Sums_s))_._(n_+_1)_=_((r_(#)_(Partial_Sums_s))_._n)_+_((r_(#)_s)_._(n_+_1)) let n be Element of NAT ; ::_thesis: (r (#) (Partial_Sums s)) . (n + 1) = ((r (#) (Partial_Sums s)) . n) + ((r (#) s) . (n + 1)) thus (r (#) (Partial_Sums s)) . (n + 1) = r * ((Partial_Sums s) . (n + 1)) by SEQ_1:9 .= r * (((Partial_Sums s) . n) + (s . (n + 1))) by Def1 .= (r * ((Partial_Sums s) . n)) + (r * (s . (n + 1))) .= ((r (#) (Partial_Sums s)) . n) + (r * (s . (n + 1))) by SEQ_1:9 .= ((r (#) (Partial_Sums s)) . n) + ((r (#) s) . (n + 1)) by SEQ_1:9 ; ::_thesis: verum end; (r (#) (Partial_Sums s)) . 0 = r * ((Partial_Sums s) . 0) by SEQ_1:9 .= r * (s . 0) by Def1 .= (r (#) s) . 0 by SEQ_1:9 ; hence Partial_Sums (r (#) s) = r (#) (Partial_Sums s) by A1, Def1; ::_thesis: verum end; theorem Th10: :: SERIES_1:10 for r being real number for s being Real_Sequence st s is summable holds ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) ) proof let r be real number ; ::_thesis: for s being Real_Sequence st s is summable holds ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) ) let s be Real_Sequence; ::_thesis: ( s is summable implies ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) ) ) assume s is summable ; ::_thesis: ( r (#) s is summable & Sum (r (#) s) = r * (Sum s) ) then A1: Partial_Sums s is convergent by Def2; then r (#) (Partial_Sums s) is convergent ; then Partial_Sums (r (#) s) is convergent by Th9; hence r (#) s is summable by Def2; ::_thesis: Sum (r (#) s) = r * (Sum s) thus Sum (r (#) s) = lim (r (#) (Partial_Sums s)) by Th9 .= r * (Sum s) by A1, SEQ_2:8 ; ::_thesis: verum end; theorem Th11: :: SERIES_1:11 for s, s1 being Real_Sequence st ( for n being Element of NAT holds s1 . n = s . 0 ) holds Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 proof let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = s . 0 ) implies Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 ) assume A1: for n being Element of NAT holds s1 . n = s . 0 ; ::_thesis: Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 A2: now__::_thesis:_for_k_being_Element_of_NAT_holds_(((Partial_Sums_s)_^\_1)_-_s1)_._(k_+_1)_=_((((Partial_Sums_s)_^\_1)_-_s1)_._k)_+_((s_^\_1)_._(k_+_1)) let k be Element of NAT ; ::_thesis: (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1)) thus (((Partial_Sums s) ^\ 1) - s1) . (k + 1) = (((Partial_Sums s) ^\ 1) . (k + 1)) - (s1 . (k + 1)) by RFUNCT_2:1 .= (((Partial_Sums s) ^\ 1) . (k + 1)) - (s . 0) by A1 .= ((Partial_Sums s) . ((k + 1) + 1)) - (s . 0) by NAT_1:def_3 .= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s . 0) by Def1 .= ((s . ((k + 1) + 1)) + ((Partial_Sums s) . (k + 1))) - (s1 . k) by A1 .= (s . ((k + 1) + 1)) + (((Partial_Sums s) . (k + 1)) - (s1 . k)) .= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) . k) - (s1 . k)) by NAT_1:def_3 .= (s . ((k + 1) + 1)) + ((((Partial_Sums s) ^\ 1) - s1) . k) by RFUNCT_2:1 .= ((((Partial_Sums s) ^\ 1) - s1) . k) + ((s ^\ 1) . (k + 1)) by NAT_1:def_3 ; ::_thesis: verum end; (((Partial_Sums s) ^\ 1) - s1) . 0 = (((Partial_Sums s) ^\ 1) . 0) - (s1 . 0) by RFUNCT_2:1 .= (((Partial_Sums s) ^\ 1) . 0) - (s . 0) by A1 .= ((Partial_Sums s) . (0 + 1)) - (s . 0) by NAT_1:def_3 .= (((Partial_Sums s) . 0) + (s . (0 + 1))) - (s . 0) by Def1 .= ((s . (0 + 1)) + (s . 0)) - (s . 0) by Def1 .= (s ^\ 1) . 0 by NAT_1:def_3 ; hence Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 by A2, Def1; ::_thesis: verum end; theorem Th12: :: SERIES_1:12 for s being Real_Sequence st s is summable holds for n being Element of NAT holds s ^\ n is summable proof let s be Real_Sequence; ::_thesis: ( s is summable implies for n being Element of NAT holds s ^\ n is summable ) defpred S1[ Element of NAT ] means s ^\ $1 is summable ; 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] ) reconsider s1 = NAT --> ((s ^\ n) . 0) as Real_Sequence ; for k being Element of NAT holds s1 . k = (s ^\ n) . 0 by FUNCOP_1:7; then A2: Partial_Sums ((s ^\ n) ^\ 1) = ((Partial_Sums (s ^\ n)) ^\ 1) - s1 by Th11; assume s ^\ n is summable ; ::_thesis: S1[n + 1] then Partial_Sums (s ^\ n) is convergent by Def2; then ( s ^\ (n + 1) = (s ^\ n) ^\ 1 & Partial_Sums ((s ^\ n) ^\ 1) is convergent ) by A2, NAT_1:48; hence S1[n + 1] by Def2; ::_thesis: verum end; assume s is summable ; ::_thesis: for n being Element of NAT holds s ^\ n is summable then A3: S1[ 0 ] by NAT_1:47; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); ::_thesis: verum end; theorem Th13: :: SERIES_1:13 for s being Real_Sequence st ex n being Element of NAT st s ^\ n is summable holds s is summable proof let s be Real_Sequence; ::_thesis: ( ex n being Element of NAT st s ^\ n is summable implies s is summable ) given n being Element of NAT such that A1: s ^\ n is summable ; ::_thesis: s is summable reconsider s1 = NAT --> ((Partial_Sums s) . n) as Real_Sequence ; for k being Element of NAT holds ((Partial_Sums s) ^\ (n + 1)) . k = ((Partial_Sums (s ^\ (n + 1))) . k) + (s1 . k) proof defpred S1[ Element of NAT ] means ((Partial_Sums s) ^\ (n + 1)) . $1 = ((Partial_Sums (s ^\ (n + 1))) . $1) + (s1 . $1); A2: (Partial_Sums (s ^\ (n + 1))) . 0 = (s ^\ (n + 1)) . 0 by Def1 .= s . (0 + (n + 1)) by NAT_1:def_3 .= s . (n + 1) ; A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: ((Partial_Sums s) ^\ (n + 1)) . k = ((Partial_Sums (s ^\ (n + 1))) . k) + (s1 . k) ; ::_thesis: S1[k + 1] ((Partial_Sums (s ^\ (n + 1))) . (k + 1)) + (s1 . (k + 1)) = (s1 . (k + 1)) + (((Partial_Sums (s ^\ (n + 1))) . k) + ((s ^\ (n + 1)) . (k + 1))) by Def1 .= ((s1 . (k + 1)) + ((Partial_Sums (s ^\ (n + 1))) . k)) + ((s ^\ (n + 1)) . (k + 1)) .= (((Partial_Sums s) . n) + ((Partial_Sums (s ^\ (n + 1))) . k)) + ((s ^\ (n + 1)) . (k + 1)) by FUNCOP_1:7 .= (((Partial_Sums s) ^\ (n + 1)) . k) + ((s ^\ (n + 1)) . (k + 1)) by A4, FUNCOP_1:7 .= ((Partial_Sums s) . (k + (n + 1))) + ((s ^\ (n + 1)) . (k + 1)) by NAT_1:def_3 .= ((Partial_Sums s) . (k + (n + 1))) + (s . ((k + 1) + (n + 1))) by NAT_1:def_3 .= (Partial_Sums s) . ((k + (n + 1)) + 1) by Def1 .= (Partial_Sums s) . ((k + 1) + (n + 1)) .= ((Partial_Sums s) ^\ (n + 1)) . (k + 1) by NAT_1:def_3 ; hence S1[k + 1] ; ::_thesis: verum end; ((Partial_Sums s) ^\ (n + 1)) . 0 = (Partial_Sums s) . (0 + (n + 1)) by NAT_1:def_3 .= (s . (n + 1)) + ((Partial_Sums s) . n) by Def1 .= ((Partial_Sums (s ^\ (n + 1))) . 0) + (s1 . 0) by A2, FUNCOP_1:7 ; then A5: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A3); ::_thesis: verum end; then A6: (Partial_Sums s) ^\ (n + 1) = (Partial_Sums (s ^\ (n + 1))) + s1 by SEQ_1:7 .= (Partial_Sums ((s ^\ n) ^\ 1)) + s1 by NAT_1:48 ; (s ^\ n) ^\ 1 is summable by A1, Th12; then Partial_Sums ((s ^\ n) ^\ 1) is convergent by Def2; then (Partial_Sums s) ^\ (n + 1) is convergent by A6; then Partial_Sums s is convergent by SEQ_4:21; hence s is summable by Def2; ::_thesis: verum end; theorem Th14: :: SERIES_1:14 for s1, s2 being Real_Sequence st ( for n being Element of NAT holds s1 . n <= s2 . n ) holds for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n proof let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n <= s2 . n ) implies for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n ) defpred S1[ Element of NAT ] means (Partial_Sums s1) . $1 <= (Partial_Sums s2) . $1; assume A1: for n being Element of NAT holds s1 . n <= s2 . n ; ::_thesis: for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n 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 A3: (Partial_Sums s1) . n <= (Partial_Sums s2) . n ; ::_thesis: S1[n + 1] A4: s1 . (n + 1) <= s2 . (n + 1) by A1; ( (Partial_Sums s1) . (n + 1) = ((Partial_Sums s1) . n) + (s1 . (n + 1)) & (Partial_Sums s2) . (n + 1) = ((Partial_Sums s2) . n) + (s2 . (n + 1)) ) by Def1; hence S1[n + 1] by A3, A4, XREAL_1:7; ::_thesis: verum end; ( (Partial_Sums s2) . 0 = s2 . 0 & (Partial_Sums s1) . 0 = s1 . 0 ) by Def1; then A5: S1[ 0 ] by A1; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A2); ::_thesis: verum end; theorem :: SERIES_1:15 for s being Real_Sequence st s is summable holds for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) proof let s be Real_Sequence; ::_thesis: ( s is summable implies for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) ) defpred S1[ Element of NAT ] means Sum s = ((Partial_Sums s) . $1) + (Sum (s ^\ ($1 + 1))); assume A1: s is summable ; ::_thesis: for n being Element of NAT holds Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 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 A3: Sum s = ((Partial_Sums s) . n) + (Sum (s ^\ (n + 1))) ; ::_thesis: S1[n + 1] reconsider s1 = NAT --> ((s ^\ (n + 1)) . 0) as Real_Sequence ; for k being Element of NAT holds s1 . k = (s ^\ (n + 1)) . 0 by FUNCOP_1:7; then A4: Partial_Sums ((s ^\ (n + 1)) ^\ 1) = ((Partial_Sums (s ^\ (n + 1))) ^\ 1) - s1 by Th11; s ^\ (n + 1) is summable by A1, Th12; then A5: Partial_Sums (s ^\ (n + 1)) is convergent by Def2; lim (Partial_Sums (s ^\ ((n + 1) + 1))) = lim (Partial_Sums ((s ^\ (n + 1)) ^\ 1)) by NAT_1:48 .= (lim ((Partial_Sums (s ^\ (n + 1))) ^\ 1)) - (lim s1) by A5, A4, SEQ_2:12 .= (lim (Partial_Sums (s ^\ (n + 1)))) - (lim s1) by A5, SEQ_4:20 .= (Sum (s ^\ (n + 1))) - (s1 . 0) by SEQ_4:26 .= (Sum (s ^\ (n + 1))) - ((s ^\ (n + 1)) . 0) by FUNCOP_1:7 ; then Sum (s ^\ ((n + 1) + 1)) = (Sum s) - (((Partial_Sums s) . n) + ((s ^\ (n + 1)) . 0)) by A3 .= (Sum s) - (((Partial_Sums s) . n) + (s . (0 + (n + 1)))) by NAT_1:def_3 .= (Sum s) - ((Partial_Sums s) . (n + 1)) by Def1 ; hence S1[n + 1] ; ::_thesis: verum end; A6: S1[ 0 ] proof reconsider s1 = NAT --> (s . 0) as Real_Sequence ; A7: Partial_Sums s is convergent by A1, Def2; for k being Element of NAT holds s1 . k = s . 0 by FUNCOP_1:7; then Partial_Sums (s ^\ 1) = ((Partial_Sums s) ^\ 1) - s1 by Th11; then lim (Partial_Sums (s ^\ 1)) = (lim ((Partial_Sums s) ^\ 1)) - (lim s1) by A7, SEQ_2:12 .= (lim (Partial_Sums s)) - (lim s1) by A7, SEQ_4:20 .= (Sum s) - (s1 . 0) by SEQ_4:26 .= (Sum s) - (s . 0) by FUNCOP_1:7 ; then Sum s = (Sum (s ^\ 1)) + (- (- (s . 0))) ; hence S1[ 0 ] by Def1; ::_thesis: verum end; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A2); ::_thesis: verum end; theorem Th16: :: SERIES_1:16 for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) holds Partial_Sums s is V41() proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= s . n ) implies Partial_Sums s is V41() ) assume A1: for n being Element of NAT holds 0 <= s . n ; ::_thesis: Partial_Sums s is V41() now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_s)_._n_<=_(Partial_Sums_s)_._(n_+_1) let n be Element of NAT ; ::_thesis: (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1) 0 <= s . (n + 1) by A1; then 0 + ((Partial_Sums s) . n) <= (s . (n + 1)) + ((Partial_Sums s) . n) by XREAL_1:6; hence (Partial_Sums s) . n <= (Partial_Sums s) . (n + 1) by Def1; ::_thesis: verum end; hence Partial_Sums s is V41() by SEQM_3:def_8; ::_thesis: verum end; theorem Th17: :: SERIES_1:17 for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) holds ( Partial_Sums s is bounded_above iff s is summable ) proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= s . n ) implies ( Partial_Sums s is bounded_above iff s is summable ) ) assume for n being Element of NAT holds 0 <= s . n ; ::_thesis: ( Partial_Sums s is bounded_above iff s is summable ) then Partial_Sums s is V41() by Th16; hence ( Partial_Sums s is bounded_above implies s is summable ) by Def2; ::_thesis: ( s is summable implies Partial_Sums s is bounded_above ) assume s is summable ; ::_thesis: Partial_Sums s is bounded_above then Partial_Sums s is convergent by Def2; then Partial_Sums s is bounded ; hence Partial_Sums s is bounded_above ; ::_thesis: verum end; theorem :: SERIES_1:18 for s being Real_Sequence st s is summable & ( for n being Element of NAT holds 0 <= s . n ) holds 0 <= Sum s proof let s be Real_Sequence; ::_thesis: ( s is summable & ( for n being Element of NAT holds 0 <= s . n ) implies 0 <= Sum s ) assume that A1: s is summable and A2: for n being Element of NAT holds 0 <= s . n ; ::_thesis: 0 <= Sum s A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(Partial_Sums_s)_._n let n be Element of NAT ; ::_thesis: 0 <= (Partial_Sums s) . n ( (Partial_Sums s) . 0 <= (Partial_Sums s) . n & 0 <= s . 0 ) by A2, Th16, SEQM_3:11; hence 0 <= (Partial_Sums s) . n by Def1; ::_thesis: verum end; Partial_Sums s is convergent by A1, Def2; hence 0 <= Sum s by A3, SEQ_2:17; ::_thesis: verum end; theorem Th19: :: SERIES_1:19 for s2, s1 being Real_Sequence st ( for n being Element of NAT holds 0 <= s2 . n ) & s1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds s2 . n <= s1 . n holds s2 is summable proof let s2, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= s2 . n ) & s1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds s2 . n <= s1 . n implies s2 is summable ) assume that A1: for n being Element of NAT holds 0 <= s2 . n and A2: s1 is summable ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st ( m <= n & not s2 . n <= s1 . n ) or s2 is summable ) given m being Element of NAT such that A3: for n being Element of NAT st m <= n holds s2 . n <= s1 . n ; ::_thesis: s2 is summable A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(s1_^\_m)_._n let n be Element of NAT ; ::_thesis: 0 <= (s1 ^\ m) . n ( (s1 ^\ m) . n = s1 . (n + m) & 0 <= s2 . (n + m) ) by A1, NAT_1:def_3; hence 0 <= (s1 ^\ m) . n by A3, NAT_1:11; ::_thesis: verum end; s1 ^\ m is summable by A2, Th12; then Partial_Sums (s1 ^\ m) is bounded_above by A4, Th17; then consider r being real number such that A5: for n being Element of NAT holds (Partial_Sums (s1 ^\ m)) . n < r by SEQ_2:def_3; A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_(s2_^\_m)_._n_<=_(s1_^\_m)_._n let n be Element of NAT ; ::_thesis: (s2 ^\ m) . n <= (s1 ^\ m) . n s2 . (n + m) <= s1 . (n + m) by A3, NAT_1:12; then (s2 ^\ m) . n <= s1 . (n + m) by NAT_1:def_3; hence (s2 ^\ m) . n <= (s1 ^\ m) . n by NAT_1:def_3; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_(s2_^\_m))_._n_<_r let n be Element of NAT ; ::_thesis: (Partial_Sums (s2 ^\ m)) . n < r (Partial_Sums (s2 ^\ m)) . n <= (Partial_Sums (s1 ^\ m)) . n by A6, Th14; hence (Partial_Sums (s2 ^\ m)) . n < r by A5, XXREAL_0:2; ::_thesis: verum end; then A7: Partial_Sums (s2 ^\ m) is bounded_above by SEQ_2:def_3; now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_(s2_^\_m)_._n let n be Element of NAT ; ::_thesis: 0 <= (s2 ^\ m) . n (s2 ^\ m) . n = s2 . (n + m) by NAT_1:def_3; hence 0 <= (s2 ^\ m) . n by A1; ::_thesis: verum end; then s2 ^\ m is summable by A7, Th17; hence s2 is summable by Th13; ::_thesis: verum end; theorem :: SERIES_1:20 for s1, s2 being Real_Sequence st ( for n being Element of NAT holds ( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable holds ( s1 is summable & Sum s1 <= Sum s2 ) proof let s1, s2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( 0 <= s1 . n & s1 . n <= s2 . n ) ) & s2 is summable implies ( s1 is summable & Sum s1 <= Sum s2 ) ) assume that A1: for n being Element of NAT holds ( 0 <= s1 . n & s1 . n <= s2 . n ) and A2: s2 is summable ; ::_thesis: ( s1 is summable & Sum s1 <= Sum s2 ) for n being Element of NAT st 0 <= n holds s1 . n <= s2 . n by A1; hence s1 is summable by A1, A2, Th19; ::_thesis: Sum s1 <= Sum s2 then A3: Partial_Sums s1 is convergent by Def2; ( Partial_Sums s2 is convergent & ( for n being Element of NAT holds (Partial_Sums s1) . n <= (Partial_Sums s2) . n ) ) by A1, A2, Def2, Th14; hence Sum s1 <= Sum s2 by A3, SEQ_2:18; ::_thesis: verum end; theorem Th21: :: SERIES_1:21 for s being Real_Sequence holds ( s is summable iff for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) proof let s be Real_Sequence; ::_thesis: ( s is summable iff for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) thus ( s is summable implies for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) ::_thesis: ( ( for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) implies s is summable ) proof assume s is summable ; ::_thesis: for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r then Partial_Sums s is convergent by Def2; hence for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r by SEQ_4:41; ::_thesis: verum end; assume for r being real number st 0 < r holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ; ::_thesis: s is summable then Partial_Sums s is convergent by SEQ_4:41; hence s is summable by Def2; ::_thesis: verum end; theorem Th22: :: SERIES_1:22 for n being Element of NAT for a being real number st a <> 1 holds (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) proof let n be Element of NAT ; ::_thesis: for a being real number st a <> 1 holds (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) let a be real number ; ::_thesis: ( a <> 1 implies (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) ) defpred S1[ Element of NAT ] means (Partial_Sums (a GeoSeq)) . $1 = (1 - (a to_power ($1 + 1))) / (1 - a); assume a <> 1 ; ::_thesis: (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) then A1: 1 - a <> 0 ; 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 (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) ; ::_thesis: S1[n + 1] hence (Partial_Sums (a GeoSeq)) . (n + 1) = ((1 - (a to_power (n + 1))) / (1 - a)) + ((a GeoSeq) . (n + 1)) by Def1 .= ((1 - (a to_power (n + 1))) / (1 - a)) + ((a to_power (n + 1)) * 1) by PREPOWER:def_1 .= ((1 - (a to_power (n + 1))) / (1 - a)) + ((a to_power (n + 1)) * ((1 - a) / (1 - a))) by A1, XCMPLX_1:60 .= ((1 - (a to_power (n + 1))) / (1 - a)) + (((a to_power (n + 1)) * (1 - a)) / (1 - a)) .= ((1 - (a to_power (n + 1))) + ((a to_power (n + 1)) - ((a |^ (n + 1)) * a))) / (1 - a) .= ((1 - (a to_power (n + 1))) + ((a to_power (n + 1)) - (a |^ ((n + 1) + 1)))) / (1 - a) by NEWTON:6 .= (1 - (a to_power ((n + 1) + 1))) / (1 - a) ; ::_thesis: verum end; (Partial_Sums (a GeoSeq)) . 0 = (a GeoSeq) . 0 by Def1 .= 1 by PREPOWER:3 .= (1 - a) / (1 - a) by A1, XCMPLX_1:60 .= (1 - (a to_power (0 + 1))) / (1 - a) by POWER:25 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence (Partial_Sums (a GeoSeq)) . n = (1 - (a to_power (n + 1))) / (1 - a) ; ::_thesis: verum end; theorem :: SERIES_1:23 for a being real number for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) proof let a be real number ; ::_thesis: for s being Real_Sequence st a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) let s be Real_Sequence; ::_thesis: ( a <> 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) implies for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) ) assume that A1: a <> 1 and A2: for n being Element of NAT holds s . (n + 1) = a * (s . n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) defpred S1[ Element of NAT ] means s . $1 = (s . 0) * ((a GeoSeq) . $1); A3: 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 s . n = (s . 0) * ((a GeoSeq) . n) ; ::_thesis: S1[n + 1] then s . (n + 1) = a * ((s . 0) * ((a GeoSeq) . n)) by A2 .= (s . 0) * (((a GeoSeq) . n) * a) .= (s . 0) * ((a GeoSeq) . (n + 1)) by PREPOWER:3 ; hence S1[n + 1] ; ::_thesis: verum end; (a GeoSeq) . 0 = 1 by PREPOWER:3; then A4: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3); then s = (s . 0) (#) (a GeoSeq) by SEQ_1:9; then A5: Partial_Sums s = (s . 0) (#) (Partial_Sums (a GeoSeq)) by Th9; now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_s)_._n_=_((s_._0)_*_(1_-_(a_to_power_(n_+_1))))_/_(1_-_a) let n be Element of NAT ; ::_thesis: (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) thus (Partial_Sums s) . n = (s . 0) * ((Partial_Sums (a GeoSeq)) . n) by A5, SEQ_1:9 .= (s . 0) * ((1 - (a to_power (n + 1))) / (1 - a)) by A1, Th22 .= ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) ; ::_thesis: verum end; hence for n being Element of NAT holds (Partial_Sums s) . n = ((s . 0) * (1 - (a to_power (n + 1)))) / (1 - a) ; ::_thesis: verum end; theorem Th24: :: SERIES_1:24 for a being real number st abs a < 1 holds ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) ) proof let a be real number ; ::_thesis: ( abs a < 1 implies ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) ) ) deffunc H1( Element of NAT ) -> set = a to_power ($1 + 1); consider s being Real_Sequence such that A1: for n being Element of NAT holds s . n = H1(n) from SEQ_1:sch_1(); assume A2: abs a < 1 ; ::_thesis: ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) ) then A3: ( s is convergent & lim s = 0 ) by A1, Th3; A4: now__::_thesis:_for_r_being_real_number_st_r_>_0_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_m_holds_ abs_(((Partial_Sums_(a_GeoSeq))_._n)_-_(1_/_(1_-_a)))_<_r a < 1 by A2, SEQ_2:1; then A5: 1 - a > 0 by XREAL_1:50; let r be real number ; ::_thesis: ( r > 0 implies ex m being Element of NAT st for n being Element of NAT st n >= m holds abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r ) assume r > 0 ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st n >= m holds abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r then r * (1 - a) > 0 * r by A5; then consider m being Element of NAT such that A6: for n being Element of NAT st n >= m holds abs ((s . n) - 0) < r * (1 - a) by A3, SEQ_2:def_7; take m = m; ::_thesis: for n being Element of NAT st n >= m holds abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r let n be Element of NAT ; ::_thesis: ( n >= m implies abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r ) assume n >= m ; ::_thesis: abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r then abs ((s . n) - 0) < r * (1 - a) by A6; then abs ((a to_power (n + 1)) - 0) < r * (1 - a) by A1; then A7: (abs (a to_power (n + 1))) / (1 - a) < (r * (1 - a)) / (1 - a) by A5, XREAL_1:74; a <> 1 by A2, SEQ_2:1; then A8: abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) = abs (((1 - (a to_power (n + 1))) / (1 - a)) - (1 / (1 - a))) by Th22 .= abs (((1 + (- (a to_power (n + 1)))) - 1) / (1 - a)) .= abs (- ((a to_power (n + 1)) / (1 - a))) .= abs ((a to_power (n + 1)) / (1 - a)) by COMPLEX1:52 .= (abs (a to_power (n + 1))) / (abs (1 - a)) by COMPLEX1:67 .= (abs (a to_power (n + 1))) / (1 - a) by A5, ABSVALUE:def_1 ; 1 - a <> 0 by A2, SEQ_2:1; hence abs (((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))) < r by A8, A7, XCMPLX_1:89; ::_thesis: verum end; then A9: Partial_Sums (a GeoSeq) is convergent by SEQ_2:def_6; hence a GeoSeq is summable by Def2; ::_thesis: Sum (a GeoSeq) = 1 / (1 - a) thus Sum (a GeoSeq) = 1 / (1 - a) by A4, A9, SEQ_2:def_7; ::_thesis: verum end; theorem :: SERIES_1:25 for a being real number for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds ( s is summable & Sum s = (s . 0) / (1 - a) ) proof let a be real number ; ::_thesis: for s being Real_Sequence st abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) holds ( s is summable & Sum s = (s . 0) / (1 - a) ) let s be Real_Sequence; ::_thesis: ( abs a < 1 & ( for n being Element of NAT holds s . (n + 1) = a * (s . n) ) implies ( s is summable & Sum s = (s . 0) / (1 - a) ) ) assume that A1: abs a < 1 and A2: for n being Element of NAT holds s . (n + 1) = a * (s . n) ; ::_thesis: ( s is summable & Sum s = (s . 0) / (1 - a) ) defpred S1[ Element of NAT ] means s . $1 = (s . 0) * ((a GeoSeq) . $1); A3: 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 s . n = (s . 0) * ((a GeoSeq) . n) ; ::_thesis: S1[n + 1] then s . (n + 1) = a * ((s . 0) * ((a GeoSeq) . n)) by A2 .= (s . 0) * (((a GeoSeq) . n) * a) .= (s . 0) * ((a GeoSeq) . (n + 1)) by PREPOWER:3 ; hence S1[n + 1] ; ::_thesis: verum end; (a GeoSeq) . 0 = 1 by PREPOWER:3; then A4: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3); then s = (s . 0) (#) (a GeoSeq) by SEQ_1:9; then A5: Partial_Sums s = (s . 0) (#) (Partial_Sums (a GeoSeq)) by Th9; a GeoSeq is summable by A1, Th24; then A6: Partial_Sums (a GeoSeq) is convergent by Def2; then Partial_Sums s is convergent by A5; hence s is summable by Def2; ::_thesis: Sum s = (s . 0) / (1 - a) Sum (a GeoSeq) = 1 / (1 - a) by A1, Th24; then lim (Partial_Sums s) = (s . 0) * (1 / (1 - a)) by A5, A6, SEQ_2:8 .= ((s . 0) * 1) / (1 - a) .= (s . 0) / (1 - a) ; hence Sum s = (s . 0) / (1 - a) ; ::_thesis: verum end; theorem Th26: :: SERIES_1:26 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) ) & s1 is convergent & lim s1 < 1 holds s is summable proof let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) ) & s1 is convergent & lim s1 < 1 implies s is summable ) assume that A1: for n being Element of NAT holds ( s . n > 0 & s1 . n = (s . (n + 1)) / (s . n) ) and A2: s1 is convergent and A3: lim s1 < 1 ; ::_thesis: s is summable set r = (1 - (lim s1)) / 2; 0 + (lim s1) < 1 by A3; then 0 < 1 - (lim s1) by XREAL_1:20; then (1 - (lim s1)) / 2 > 0 ; then consider m being Element of NAT such that A4: for n being Element of NAT st m <= n holds abs ((s1 . n) - (lim s1)) < (1 - (lim s1)) / 2 by A2, SEQ_2:def_7; set s2 = ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq); defpred S1[ Element of NAT ] means s . (m + $1) <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + $1); A5: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_>=_0 let n be Element of NAT ; ::_thesis: s1 . n >= 0 ( s . n > 0 & s . (n + 1) > 0 ) by A1; then (s . (n + 1)) / (s . n) > 0 ; hence s1 . n >= 0 by A1; ::_thesis: verum end; then A6: lim s1 >= 0 by A2, PREPOWER:1; then 1 + (- (lim s1)) < 1 + 1 by XREAL_1:6; then A7: (1 - (lim s1)) / 2 < 2 / 2 by XREAL_1:74; A8: ((1 - (lim s1)) / 2) + (lim s1) = 1 - ((1 - (lim s1)) / 2) ; A9: for k being Element of NAT st S1[k] holds S1[k + 1] proof set X = (s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m)); let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A10: s . (m + k) <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k) ; ::_thesis: S1[k + 1] abs ((s1 . (m + k)) - (lim s1)) < (1 - (lim s1)) / 2 by A4, NAT_1:11; then (s1 . (m + k)) - (lim s1) < (1 - (lim s1)) / 2 by SEQ_2:1; then A11: s1 . (m + k) <= 1 - ((1 - (lim s1)) / 2) by A8, XREAL_1:19; (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k) >= 0 by A1, A10; then A12: (s1 . (m + k)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) <= (1 - ((1 - (lim s1)) / 2)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) by A11, XREAL_1:64; s . (m + k) <> 0 by A1; then A13: s . (m + (k + 1)) = ((s . ((m + k) + 1)) / (s . (m + k))) * (s . (m + k)) by XCMPLX_1:87 .= (s1 . (m + k)) * (s . (m + k)) by A1 ; s1 . (m + k) >= 0 by A5; then A14: s . (m + (k + 1)) <= (s1 . (m + k)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) by A10, A13, XREAL_1:64; (1 - ((1 - (lim s1)) / 2)) * ((((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + k)) = (1 - ((1 - (lim s1)) / 2)) * (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . (m + k))) by SEQ_1:9 .= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * ((((1 - ((1 - (lim s1)) / 2)) GeoSeq) . (m + k)) * (1 - ((1 - (lim s1)) / 2))) .= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . ((m + k) + 1)) by PREPOWER:3 .= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + (k + 1)) by SEQ_1:9 ; hence S1[k + 1] by A14, A12, XXREAL_0:2; ::_thesis: verum end; (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . (m + 0) = ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * (((1 - ((1 - (lim s1)) / 2)) GeoSeq) . m) by SEQ_1:9 .= ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) * ((1 - ((1 - (lim s1)) / 2)) |^ m) by PREPOWER:def_1 .= (s . m) * (((1 - ((1 - (lim s1)) / 2)) to_power (- m)) * ((1 - ((1 - (lim s1)) / 2)) to_power m)) .= (s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power ((- m) + m)) by A7, POWER:27, XREAL_1:50 .= (s . m) * 1 by POWER:24 .= s . (m + 0) ; then A15: S1[ 0 ] ; A16: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A9); A17: now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_ s_._n_<=_(((s_._m)_*_((1_-_((1_-_(lim_s1))_/_2))_to_power_(-_m)))_(#)_((1_-_((1_-_(lim_s1))_/_2))_GeoSeq))_._n let n be Element of NAT ; ::_thesis: ( m <= n implies s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n ) assume m <= n ; ::_thesis: s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n then consider k being Nat such that A18: n = m + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; n = m + k by A18; hence s . n <= (((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq)) . n by A16; ::_thesis: verum end; 1 - (lim s1) <= 1 - 0 by A6, XREAL_1:6; then 1 - (lim s1) < 2 * 2 by XXREAL_0:2; then (1 - (lim s1)) / 2 < (2 * 2) / 2 by XREAL_1:74; then (1 - (lim s1)) / 2 < 1 + 1 ; then ((1 - (lim s1)) / 2) - 1 < 1 by XREAL_1:19; then A19: - (((1 - (lim s1)) / 2) - 1) > - 1 by XREAL_1:24; 1 - (lim s1) > 0 by A3, XREAL_1:50; then (1 - (lim s1)) / 2 > 0 ; then 1 - ((1 - (lim s1)) / 2) < 1 - 0 by XREAL_1:10; then abs (1 - ((1 - (lim s1)) / 2)) < 1 by A19, SEQ_2:1; then (1 - ((1 - (lim s1)) / 2)) GeoSeq is summable by Th24; then A20: ((s . m) * ((1 - ((1 - (lim s1)) / 2)) to_power (- m))) (#) ((1 - ((1 - (lim s1)) / 2)) GeoSeq) is summable by Th10; for n being Element of NAT holds 0 <= s . n by A1; hence s is summable by A20, A17, Th19; ::_thesis: verum end; theorem :: SERIES_1:27 for s being Real_Sequence st ( for n being Element of NAT holds s . n > 0 ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds (s . (n + 1)) / (s . n) >= 1 holds not s is summable proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n > 0 ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds (s . (n + 1)) / (s . n) >= 1 implies not s is summable ) assume that A1: for n being Element of NAT holds s . n > 0 and A2: ex m being Element of NAT st for n being Element of NAT st n >= m holds (s . (n + 1)) / (s . n) >= 1 ; ::_thesis: not s is summable consider m being Element of NAT such that A3: for n being Element of NAT st n >= m holds (s . (n + 1)) / (s . n) >= 1 by A2; defpred S1[ Element of NAT ] means s . (m + $1) >= s . m; A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: s . (m + k) >= s . m ; ::_thesis: S1[k + 1] ( s . (m + k) > 0 & (s . ((m + k) + 1)) / (s . (m + k)) >= 1 ) by A1, A3, NAT_1:11; then s . ((m + k) + 1) >= s . (m + k) by XREAL_1:191; hence S1[k + 1] by A5, XXREAL_0:2; ::_thesis: verum end; A6: S1[ 0 ] ; A7: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A6, A4); A8: for k being Element of NAT ex n being Element of NAT st ( n >= k & not abs ((s . n) - 0) < s . m ) proof let k be Element of NAT ; ::_thesis: ex n being Element of NAT st ( n >= k & not abs ((s . n) - 0) < s . m ) take n = m + k; ::_thesis: ( n >= k & not abs ((s . n) - 0) < s . m ) s . n >= s . m by A7; hence ( n >= k & not abs ((s . n) - 0) < s . m ) by NAT_1:11, SEQ_2:1; ::_thesis: verum end; s . m > 0 by A1; then ( not lim s = 0 or not s is convergent ) by A8, SEQ_2:def_7; hence not s is summable by Th4; ::_thesis: verum end; theorem Th28: :: SERIES_1:28 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 holds s is summable proof let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 < 1 implies s is summable ) assume that A1: for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) and A2: s1 is convergent and A3: lim s1 < 1 ; ::_thesis: s is summable A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(s1_^\_1)_._n_>=_0 let n be Element of NAT ; ::_thesis: (s1 ^\ 1) . n >= 0 A5: (s1 ^\ 1) . n = s1 . (n + 1) by NAT_1:def_3 .= (n + 1) -root (s . (n + 1)) by A1 ; s . (n + 1) >= 0 by A1; hence (s1 ^\ 1) . n >= 0 by A5, NAT_1:11, POWER:7; ::_thesis: verum end; set r = (1 - (lim s1)) / 2; 0 + (lim s1) < 1 by A3; then 0 < 1 - (lim s1) by XREAL_1:20; then (1 - (lim s1)) / 2 > 0 ; then consider m being Element of NAT such that A6: for n being Element of NAT st m <= n holds abs ((s1 . n) - (lim s1)) < (1 - (lim s1)) / 2 by A2, SEQ_2:def_7; lim (s1 ^\ 1) = lim s1 by A2, SEQ_4:20; then A7: lim s1 >= 0 by A2, A4, PREPOWER:1; then 1 + (- (lim s1)) < 1 + 1 by XREAL_1:6; then (1 - (lim s1)) / 2 < 2 / 2 by XREAL_1:74; then A8: 1 - ((1 - (lim s1)) / 2) > 0 by XREAL_1:50; set s2 = (1 - ((1 - (lim s1)) / 2)) GeoSeq ; A9: ((1 - (lim s1)) / 2) + (lim s1) = 1 - ((1 - (lim s1)) / 2) ; A10: for n being Element of NAT st m + 1 <= n holds s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n proof let n be Element of NAT ; ::_thesis: ( m + 1 <= n implies s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n ) assume A11: m + 1 <= n ; ::_thesis: s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n 1 <= m + 1 by NAT_1:11; then A12: 1 <= n by A11, XXREAL_0:2; A13: s . n >= 0 by A1; m <= n by A11, NAT_1:13; then abs ((s1 . n) - (lim s1)) < (1 - (lim s1)) / 2 by A6; then (s1 . n) - (lim s1) < (1 - (lim s1)) / 2 by SEQ_2:1; then s1 . n < 1 - ((1 - (lim s1)) / 2) by A9, XREAL_1:19; then A14: n -root (s . n) < 1 - ((1 - (lim s1)) / 2) by A1; now__::_thesis:_s_._n_<_(1_-_((1_-_(lim_s1))_/_2))_to_power_n percases ( s . n = 0 or s . n <> 0 ) ; suppose s . n = 0 ; ::_thesis: s . n < (1 - ((1 - (lim s1)) / 2)) to_power n hence s . n < (1 - ((1 - (lim s1)) / 2)) to_power n by A8, POWER:34; ::_thesis: verum end; suppose s . n <> 0 ; ::_thesis: s . n < (1 - ((1 - (lim s1)) / 2)) to_power n then n -Root (s . n) > 0 by A12, A13, PREPOWER:def_2; then n -root (s . n) > 0 by A12, A13, POWER:def_1; then (n -root (s . n)) to_power n < (1 - ((1 - (lim s1)) / 2)) to_power n by A11, A14, POWER:37; hence s . n < (1 - ((1 - (lim s1)) / 2)) to_power n by A12, A13, POWER:4; ::_thesis: verum end; end; end; hence s . n <= (1 - ((1 - (lim s1)) / 2)) to_power n ; ::_thesis: verum end; A15: for n being Element of NAT st m + 1 <= n holds s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n proof let n be Element of NAT ; ::_thesis: ( m + 1 <= n implies s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n ) ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n = (1 - ((1 - (lim s1)) / 2)) to_power n by PREPOWER:def_1; hence ( m + 1 <= n implies s . n <= ((1 - ((1 - (lim s1)) / 2)) GeoSeq) . n ) by A10; ::_thesis: verum end; 1 - (lim s1) <= 1 - 0 by A7, XREAL_1:6; then 1 - (lim s1) < 2 * 2 by XXREAL_0:2; then (1 - (lim s1)) / 2 < (2 * 2) / 2 by XREAL_1:74; then (1 - (lim s1)) / 2 < 1 + 1 ; then ((1 - (lim s1)) / 2) - 1 < 1 by XREAL_1:19; then A16: - (((1 - (lim s1)) / 2) - 1) > - 1 by XREAL_1:24; 1 - (lim s1) > 0 by A3, XREAL_1:50; then (1 - (lim s1)) / 2 > 0 ; then 1 - ((1 - (lim s1)) / 2) < 1 - 0 by XREAL_1:10; then abs (1 - ((1 - (lim s1)) / 2)) < 1 by A16, SEQ_2:1; then (1 - ((1 - (lim s1)) / 2)) GeoSeq is summable by Th24; hence s is summable by A1, A15, Th19; ::_thesis: verum end; theorem Th29: :: SERIES_1:29 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds s1 . n >= 1 holds not s is summable proof let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds s1 . n >= 1 implies not s is summable ) assume that A1: for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) and A2: ex m being Element of NAT st for n being Element of NAT st m <= n holds s1 . n >= 1 ; ::_thesis: not s is summable consider m being Element of NAT such that A3: for n being Element of NAT st m <= n holds s1 . n >= 1 by A2; A4: for n being Element of NAT st m + 1 <= n holds s . n >= 1 proof let n be Element of NAT ; ::_thesis: ( m + 1 <= n implies s . n >= 1 ) assume A5: m + 1 <= n ; ::_thesis: s . n >= 1 1 <= 1 + m by NAT_1:11; then A6: 1 <= n by A5, XXREAL_0:2; A7: s . n >= 0 by A1; m <= m + 1 by NAT_1:11; then m <= n by A5, XXREAL_0:2; then s1 . n >= 1 by A3; then A8: n -root (s . n) >= 1 by A1; now__::_thesis:_s_._n_>=_1 percases ( n -root (s . n) = 1 or n -root (s . n) > 1 ) by A8, XXREAL_0:1; suppose n -root (s . n) = 1 ; ::_thesis: s . n >= 1 then s . n = 1 |^ n by A6, A7, POWER:4; hence s . n >= 1 by NEWTON:10; ::_thesis: verum end; suppose n -root (s . n) > 1 ; ::_thesis: s . n >= 1 then (n -root (s . n)) to_power n > 1 by A5, POWER:35; hence s . n >= 1 by A6, A7, POWER:4; ::_thesis: verum end; end; end; hence s . n >= 1 ; ::_thesis: verum end; for k being Element of NAT ex n being Element of NAT st ( k <= n & not abs ((s . n) - 0) < 1 ) proof let k be Element of NAT ; ::_thesis: ex n being Element of NAT st ( k <= n & not abs ((s . n) - 0) < 1 ) take n = (m + 1) + k; ::_thesis: ( k <= n & not abs ((s . n) - 0) < 1 ) not s . n < 1 by A4, NAT_1:11; hence ( k <= n & not abs ((s . n) - 0) < 1 ) by NAT_1:11, SEQ_2:1; ::_thesis: verum end; then ( not s is convergent or not lim s = 0 ) by SEQ_2:def_7; hence not s is summable by Th4; ::_thesis: verum end; theorem :: SERIES_1:30 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 holds not s is summable proof let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) ) & s1 is convergent & lim s1 > 1 implies not s is summable ) assume that A1: for n being Element of NAT holds ( s . n >= 0 & s1 . n = n -root (s . n) ) and A2: s1 is convergent and A3: lim s1 > 1 ; ::_thesis: not s is summable set r = (lim s1) - 1; (lim s1) - 1 > 0 by A3, XREAL_1:50; then consider m being Element of NAT such that A4: for n being Element of NAT st m <= n holds abs ((s1 . n) - (lim s1)) < (lim s1) - 1 by A2, SEQ_2:def_7; for n being Element of NAT st m <= n holds s1 . n >= 1 proof let n be Element of NAT ; ::_thesis: ( m <= n implies s1 . n >= 1 ) assume m <= n ; ::_thesis: s1 . n >= 1 then abs ((s1 . n) - (lim s1)) < (lim s1) - 1 by A4; then (s1 . n) - (lim s1) > - ((lim s1) - 1) by SEQ_2:1; then ((s1 . n) - (lim s1)) + (lim s1) > (- ((lim s1) - 1)) + (lim s1) by XREAL_1:6; hence s1 . n >= 1 ; ::_thesis: verum end; hence not s is summable by A1, Th29; ::_thesis: verum end; registration let k, n be Nat; clusterk to_power n -> natural ; coherence k to_power n is natural ; end; definition let k, n be Nat; :: original: to_power redefine funck to_power n -> Element of NAT ; coherence k to_power n is Element of NAT by ORDINAL1:def_12; end; theorem Th31: :: SERIES_1:31 for s, s1 being Real_Sequence st s is V42() & ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ) holds ( s is summable iff s1 is summable ) proof let s, s1 be Real_Sequence; ::_thesis: ( s is V42() & ( for n being Element of NAT holds ( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ) implies ( s is summable iff s1 is summable ) ) assume that A1: s is V42() and A2: for n being Element of NAT holds ( s . n >= 0 & s1 . n = (2 to_power n) * (s . (2 to_power n)) ) ; ::_thesis: ( s is summable iff s1 is summable ) A3: (Partial_Sums s) . (2 to_power (0 + 1)) = (Partial_Sums s) . (1 + 1) by POWER:25 .= ((Partial_Sums s) . (0 + 1)) + (s . 2) by Def1 .= (((Partial_Sums s) . 0) + (s . 1)) + (s . 2) by Def1 .= ((s . 0) + (s . 1)) + (s . 2) by Def1 ; A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_>=_0 let n be Element of NAT ; ::_thesis: s1 . n >= 0 s . (2 to_power n) >= 0 by A2; then (2 to_power n) * (s . (2 to_power n)) >= 0 ; hence s1 . n >= 0 by A2; ::_thesis: verum end; thus ( s is summable implies s1 is summable ) ::_thesis: ( s1 is summable implies s is summable ) proof defpred S1[ Element of NAT ] means (Partial_Sums s1) . $1 <= 2 * ((Partial_Sums s) . (2 to_power $1)); A5: s . 0 >= 0 by A2; A6: 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] ) deffunc H1( Element of NAT ) -> Element of REAL = ((Partial_Sums s) . ((2 to_power n) + $1)) - ((Partial_Sums s) . (2 to_power n)); consider a being Real_Sequence such that A7: for m being Element of NAT holds a . m = H1(m) from SEQ_1:sch_1(); defpred S2[ Element of NAT ] means ( $1 > 2 to_power n or $1 * (s . (2 to_power (n + 1))) <= a . $1 ); A8: for m being Element of NAT st S2[m] holds S2[m + 1] proof let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] ) assume A9: ( m > 2 to_power n or m * (s . (2 to_power (n + 1))) <= a . m ) ; ::_thesis: S2[m + 1] now__::_thesis:_S2[m_+_1] percases ( m > 2 to_power n or m * (s . (2 to_power (n + 1))) <= a . m ) by A9; suppose m > 2 to_power n ; ::_thesis: S2[m + 1] hence S2[m + 1] by NAT_1:13; ::_thesis: verum end; supposeA10: m * (s . (2 to_power (n + 1))) <= a . m ; ::_thesis: S2[m + 1] now__::_thesis:_S2[m_+_1] percases ( m < 2 to_power n or m >= 2 to_power n ) ; suppose m < 2 to_power n ; ::_thesis: S2[m + 1] then m + 1 <= 2 to_power n by NAT_1:13; then (2 to_power n) + (m + 1) <= (2 to_power n) + (2 to_power n) by XREAL_1:7; then ((2 to_power n) + m) + 1 <= 2 * (2 to_power n) ; then ((2 to_power n) + m) + 1 <= (2 to_power 1) * (2 to_power n) by POWER:25; then ((2 to_power n) + m) + 1 <= 2 to_power (n + 1) by POWER:27; then s . (((2 to_power n) + m) + 1) >= s . (2 to_power (n + 1)) by A1, SEQM_3:8; then (m * (s . (2 to_power (n + 1)))) + (1 * (s . (2 to_power (n + 1)))) <= (a . m) + (s . (((2 to_power n) + m) + 1)) by A10, XREAL_1:7; then (m + 1) * (s . (2 to_power (n + 1))) <= (((Partial_Sums s) . ((2 to_power n) + m)) - ((Partial_Sums s) . (2 to_power n))) + (s . (((2 to_power n) + m) + 1)) by A7; then (m + 1) * (s . (2 to_power (n + 1))) <= (((Partial_Sums s) . ((2 to_power n) + m)) + (s . (((2 to_power n) + m) + 1))) - ((Partial_Sums s) . (2 to_power n)) ; then (m + 1) * (s . (2 to_power (n + 1))) <= ((Partial_Sums s) . ((2 to_power n) + (m + 1))) - ((Partial_Sums s) . (2 to_power n)) by Def1; hence S2[m + 1] by A7; ::_thesis: verum end; suppose m >= 2 to_power n ; ::_thesis: S2[m + 1] hence S2[m + 1] by NAT_1:13; ::_thesis: verum end; end; end; hence S2[m + 1] ; ::_thesis: verum end; end; end; hence S2[m + 1] ; ::_thesis: verum end; a . 0 = ((Partial_Sums s) . ((2 to_power n) + 0)) - ((Partial_Sums s) . (2 to_power n)) by A7 .= 0 ; then A11: S2[ 0 ] ; for m being Element of NAT holds S2[m] from NAT_1:sch_1(A11, A8); then 2 * ((2 to_power n) * (s . (2 to_power (n + 1)))) <= 2 * (a . (2 to_power n)) by XREAL_1:64; then (2 * (2 to_power n)) * (s . (2 to_power (n + 1))) <= 2 * (a . (2 to_power n)) ; then ((2 to_power 1) * (2 to_power n)) * (s . (2 to_power (n + 1))) <= 2 * (a . (2 to_power n)) by POWER:25; then (2 to_power (n + 1)) * (s . (2 to_power (n + 1))) <= 2 * (a . (2 to_power n)) by POWER:27; then s1 . (n + 1) <= 2 * (a . (2 to_power n)) by A2; then s1 . (n + 1) <= 2 * (((Partial_Sums s) . ((2 to_power n) + (2 to_power n))) - ((Partial_Sums s) . (2 to_power n))) by A7; then A12: (2 * ((Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1)) <= (2 * ((Partial_Sums s) . (2 to_power n))) + (2 * (((Partial_Sums s) . ((2 to_power n) + (2 to_power n))) - ((Partial_Sums s) . (2 to_power n)))) by XREAL_1:7; assume (Partial_Sums s1) . n <= 2 * ((Partial_Sums s) . (2 to_power n)) ; ::_thesis: S1[n + 1] then ((Partial_Sums s1) . n) + (s1 . (n + 1)) <= (2 * ((Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1)) by XREAL_1:6; then A13: (Partial_Sums s1) . (n + 1) <= (2 * ((Partial_Sums s) . (2 to_power n))) + (s1 . (n + 1)) by Def1; (2 to_power n) + (2 to_power n) = 2 * (2 to_power n) .= (2 to_power 1) * (2 to_power n) by POWER:25 .= 2 to_power (n + 1) by POWER:27 ; hence S1[n + 1] by A13, A12, XXREAL_0:2; ::_thesis: verum end; A14: 2 to_power 0 = 0 + 1 by POWER:24; then A15: 2 * ((Partial_Sums s) . (2 to_power 0)) = 2 * (((Partial_Sums s) . 0) + (s . 1)) by Def1 .= 2 * ((s . 0) + (s . 1)) by Def1 .= (2 * (s . 0)) + (2 * (s . 1)) ; assume s is summable ; ::_thesis: s1 is summable then Partial_Sums s is bounded_above by A2, Th17; then consider r being real number such that A16: for n being Element of NAT holds (Partial_Sums s) . n < r by SEQ_2:def_3; s . 1 >= 0 by A2; then A17: (s . 1) + (s . 1) >= (s . 1) + 0 by XREAL_1:7; (Partial_Sums s1) . 0 = s1 . 0 by Def1 .= 1 * (s . 1) by A2, A14 .= s . 1 ; then A18: S1[ 0 ] by A15, A17, A5, XREAL_1:7; A19: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A18, A6); now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_s1)_._n_<_2_*_r let n be Element of NAT ; ::_thesis: (Partial_Sums s1) . n < 2 * r ( 2 * ((Partial_Sums s) . (2 to_power n)) < 2 * r & (Partial_Sums s1) . n <= 2 * ((Partial_Sums s) . (2 to_power n)) ) by A19, A16, XREAL_1:68; hence (Partial_Sums s1) . n < 2 * r by XXREAL_0:2; ::_thesis: verum end; then Partial_Sums s1 is bounded_above by SEQ_2:def_3; hence s1 is summable by A4, Th17; ::_thesis: verum end; assume s1 is summable ; ::_thesis: s is summable then Partial_Sums s1 is bounded_above by A4, Th17; then consider r being real number such that A20: for n being Element of NAT holds (Partial_Sums s1) . n < r by SEQ_2:def_3; A21: 2 to_power 0 = 1 by POWER:24; defpred S1[ Element of NAT ] means (Partial_Sums s) . (2 to_power ($1 + 1)) <= (((Partial_Sums s1) . $1) + (s . 0)) + (s . 2); A22: 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] ) defpred S2[ Element of NAT ] means ((Partial_Sums s) . ((2 to_power (n + 1)) + $1)) - ((Partial_Sums s) . (2 to_power (n + 1))) <= $1 * (s . (2 to_power (n + 1))); A23: for m being Element of NAT st S2[m] holds S2[m + 1] proof let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] ) (2 to_power (n + 1)) + (m + 1) >= 2 to_power (n + 1) by NAT_1:11; then A24: s . ((2 to_power (n + 1)) + (m + 1)) <= s . (2 to_power (n + 1)) by A1, SEQM_3:8; assume ((Partial_Sums s) . ((2 to_power (n + 1)) + m)) - ((Partial_Sums s) . (2 to_power (n + 1))) <= m * (s . (2 to_power (n + 1))) ; ::_thesis: S2[m + 1] then (((Partial_Sums s) . ((2 to_power (n + 1)) + m)) - ((Partial_Sums s) . (2 to_power (n + 1)))) + (s . (((2 to_power (n + 1)) + m) + 1)) <= (m * (s . (2 to_power (n + 1)))) + (s . (2 to_power (n + 1))) by A24, XREAL_1:7; then (((Partial_Sums s) . ((2 to_power (n + 1)) + m)) + (s . (((2 to_power (n + 1)) + m) + 1))) - ((Partial_Sums s) . (2 to_power (n + 1))) <= (m * (s . (2 to_power (n + 1)))) + (s . (2 to_power (n + 1))) ; hence S2[m + 1] by Def1; ::_thesis: verum end; A25: S2[ 0 ] ; for m being Element of NAT holds S2[m] from NAT_1:sch_1(A25, A23); then ((Partial_Sums s) . ((2 to_power (n + 1)) + (2 to_power (n + 1)))) - ((Partial_Sums s) . (2 to_power (n + 1))) <= (2 to_power (n + 1)) * (s . (2 to_power (n + 1))) ; then A26: ((Partial_Sums s) . ((2 to_power (n + 1)) + (2 to_power (n + 1)))) - ((Partial_Sums s) . (2 to_power (n + 1))) <= s1 . (n + 1) by A2; assume (Partial_Sums s) . (2 to_power (n + 1)) <= (((Partial_Sums s1) . n) + (s . 0)) + (s . 2) ; ::_thesis: S1[n + 1] then ((Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1)) <= (s1 . (n + 1)) + ((((Partial_Sums s1) . n) + (s . 0)) + (s . 2)) by XREAL_1:7; then ((Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1)) <= ((((Partial_Sums s1) . n) + (s1 . (n + 1))) + (s . 0)) + (s . 2) ; then A27: ((Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1)) <= (((Partial_Sums s1) . (n + 1)) + (s . 0)) + (s . 2) by Def1; (2 to_power (n + 1)) + (2 to_power (n + 1)) = 2 * (2 to_power (n + 1)) .= (2 to_power 1) * (2 to_power (n + 1)) by POWER:25 .= 2 to_power ((n + 1) + 1) by POWER:27 ; then (((Partial_Sums s) . (2 to_power ((n + 1) + 1))) - ((Partial_Sums s) . (2 to_power (n + 1)))) + ((Partial_Sums s) . (2 to_power (n + 1))) <= ((Partial_Sums s) . (2 to_power (n + 1))) + (s1 . (n + 1)) by A26, XREAL_1:7; hence S1[n + 1] by A27, XXREAL_0:2; ::_thesis: verum end; (((Partial_Sums s1) . 0) + (s . 0)) + (s . 2) = ((s1 . 0) + (s . 0)) + (s . 2) by Def1 .= (((2 to_power 0) * (s . (2 to_power 0))) + (s . 0)) + (s . 2) by A2 .= ((s . 0) + (s . 1)) + (s . 2) by A21 ; then A28: S1[ 0 ] by A3; A29: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A28, A22); A30: Partial_Sums s is V41() by A2, Th16; now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_s)_._n_<_r_+_((s_._0)_+_(s_._2)) let n be Element of NAT ; ::_thesis: (Partial_Sums s) . n < r + ((s . 0) + (s . 2)) (Partial_Sums s1) . n < r by A20; then A31: ((Partial_Sums s1) . n) + ((s . 0) + (s . 2)) < r + ((s . 0) + (s . 2)) by XREAL_1:6; ( (1 + 1) to_power n >= 1 + (n * 1) & 1 + n >= n ) by NAT_1:11, POWER:49; then 2 to_power n >= n by XXREAL_0:2; then (2 to_power n) + (2 to_power n) >= n + n by XREAL_1:7; then 2 * (2 to_power n) >= n + n ; then (2 to_power 1) * (2 to_power n) >= n + n by POWER:25; then A32: 2 to_power (n + 1) >= n + n by POWER:27; n + n >= n by NAT_1:11; then 2 to_power (n + 1) >= n by A32, XXREAL_0:2; then A33: (Partial_Sums s) . (2 to_power (n + 1)) >= (Partial_Sums s) . n by A30, SEQM_3:6; (Partial_Sums s) . (2 to_power (n + 1)) <= (((Partial_Sums s1) . n) + (s . 0)) + (s . 2) by A29; then (Partial_Sums s) . n <= (((Partial_Sums s1) . n) + (s . 0)) + (s . 2) by A33, XXREAL_0:2; hence (Partial_Sums s) . n < r + ((s . 0) + (s . 2)) by A31, XXREAL_0:2; ::_thesis: verum end; then Partial_Sums s is bounded_above by SEQ_2:def_3; hence s is summable by A2, Th17; ::_thesis: verum end; theorem :: SERIES_1:32 for p being real number for s being Real_Sequence st p > 1 & ( for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ) holds s is summable proof let p be real number ; ::_thesis: for s being Real_Sequence st p > 1 & ( for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ) holds s is summable let s be Real_Sequence; ::_thesis: ( p > 1 & ( for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ) implies s is summable ) assume that A1: p > 1 and A2: for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ; ::_thesis: s is summable defpred S1[ Element of NAT , real number ] means ( ( $1 = 0 & $2 = 1 ) or ( $1 >= 1 & $2 = 1 / ($1 to_power p) ) ); A3: for n being Element of NAT ex r being Real st S1[n,r] proof let n be Element of NAT ; ::_thesis: ex r being Real st S1[n,r] ( n = 0 or n >= 1 ) proof assume that A4: n <> 0 and A5: n < 1 ; ::_thesis: contradiction n >= 0 + 1 by A4, NAT_1:13; hence contradiction by A5; ::_thesis: verum end; hence ex r being Real st S1[n,r] ; ::_thesis: verum end; consider s1 being Real_Sequence such that A6: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A3); deffunc H1( Element of NAT ) -> Element of REAL = (2 to_power $1) * (s1 . (2 to_power $1)); consider s2 being Real_Sequence such that A7: for n being Element of NAT holds s2 . n = H1(n) from SEQ_1:sch_1(); A8: s1 . 0 = 1 by A6; now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._(n_+_1)_<=_s1_._n let n be Element of NAT ; ::_thesis: s1 . (n + 1) <= s1 . n now__::_thesis:_s1_._(n_+_1)_<=_s1_._n percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6; supposeA9: n = 0 ; ::_thesis: s1 . (n + 1) <= s1 . n then (n + 1) #R p >= 1 by A1, PREPOWER:85; then A10: (n + 1) to_power p >= 1 by POWER:def_2; s1 . (n + 1) = 1 / ((n + 1) to_power p) by A6; hence s1 . (n + 1) <= s1 . n by A8, A9, A10, XREAL_1:211; ::_thesis: verum end; supposeA11: ex m being Nat st n = m + 1 ; ::_thesis: s1 . (n + 1) <= s1 . n then n to_power p > 0 by POWER:34; then 1 / (n to_power p) > 0 ; then A12: s1 . n > 0 by A6; A13: n / (n + 1) <= 1 by NAT_1:11, XREAL_1:183; A14: n / (n + 1) > 0 by A11; (s1 . (n + 1)) / (s1 . n) = (1 / ((n + 1) to_power p)) / (s1 . n) by A6 .= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A6, A11 .= (1 / ((n + 1) to_power p)) * (n to_power p) .= (n to_power p) / ((n + 1) to_power p) .= (n / (n + 1)) to_power p by A11, POWER:31 .= (n / (n + 1)) #R p by A14, POWER:def_2 ; then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A1, A14, A13, PREPOWER:84; then (s1 . (n + 1)) / (s1 . n) <= 1 by A11, PREPOWER:71; hence s1 . (n + 1) <= s1 . n by A12, XREAL_1:187; ::_thesis: verum end; end; end; hence s1 . (n + 1) <= s1 . n ; ::_thesis: verum end; then A15: s1 is V42() by SEQM_3:def_9; A16: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_0_holds_ (s1_^\_1)_._n_>=_(s_^\_1)_._n let n be Element of NAT ; ::_thesis: ( n >= 0 implies (s1 ^\ 1) . n >= (s ^\ 1) . n ) assume n >= 0 ; ::_thesis: (s1 ^\ 1) . n >= (s ^\ 1) . n A17: n + 1 >= 0 + 1 by XREAL_1:6; (s ^\ 1) . n = s . (n + 1) by NAT_1:def_3 .= 1 / ((n + 1) to_power p) by A2, A17 .= s1 . (n + 1) by A6 .= (s1 ^\ 1) . n by NAT_1:def_3 ; hence (s1 ^\ 1) . n >= (s ^\ 1) . n ; ::_thesis: verum end; deffunc H2( Element of NAT ) -> Element of REAL = $1 -root (s2 . $1); consider s3 being Real_Sequence such that A18: for n being Element of NAT holds s3 . n = H2(n) from SEQ_1:sch_1(); A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_s2_._n_=_2_to_power_((1_-_p)_*_n)_&_s2_._n_>=_0_&_s3_._n_=_n_-root_((2_to_power_(1_-_p))_to_power_n)_) let n be Element of NAT ; ::_thesis: ( s2 . n = 2 to_power ((1 - p) * n) & s2 . n >= 0 & s3 . n = n -root ((2 to_power (1 - p)) to_power n) ) A20: 2 to_power n > 0 by POWER:34; thus A21: s2 . n = (2 to_power n) * (s1 . (2 to_power n)) by A7 .= (2 to_power n) * (1 / ((2 to_power n) to_power p)) by A6, A20 .= (2 to_power n) * (1 / (2 to_power (n * p))) by POWER:33 .= (2 to_power n) * (2 to_power (- (n * p))) by POWER:28 .= 2 to_power (n + (- (n * p))) by POWER:27 .= 2 to_power ((1 - p) * n) ; ::_thesis: ( s2 . n >= 0 & s3 . n = n -root ((2 to_power (1 - p)) to_power n) ) hence s2 . n >= 0 by POWER:34; ::_thesis: s3 . n = n -root ((2 to_power (1 - p)) to_power n) s2 . n = (2 to_power (1 - p)) to_power n by A21, POWER:33; hence s3 . n = n -root ((2 to_power (1 - p)) to_power n) by A18; ::_thesis: verum end; A22: now__::_thesis:_for_n_being_Nat_holds_(s3_^\_1)_._n_=_2_to_power_(1_-_p) let n be Nat; ::_thesis: (s3 ^\ 1) . n = 2 to_power (1 - p) A23: ( n + 1 >= 0 + 1 & 2 to_power (1 - p) >= 0 ) by POWER:34, XREAL_1:6; thus (s3 ^\ 1) . n = s3 . (n + 1) by NAT_1:def_3 .= (n + 1) -root ((2 to_power (1 - p)) to_power (n + 1)) by A19 .= 2 to_power (1 - p) by A23, POWER:4 ; ::_thesis: verum end; then A24: s3 ^\ 1 is constant by VALUED_0:def_18; then lim (s3 ^\ 1) = (s3 ^\ 1) . 0 by SEQ_4:26 .= 2 to_power (1 - p) by A22 ; then A25: lim s3 = 2 to_power (1 - p) by A24, SEQ_4:22; A26: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_s1_._n_>=_0_&_s2_._n_=_(2_to_power_n)_*_(s1_._(2_to_power_n))_) let n be Element of NAT ; ::_thesis: ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) ) now__::_thesis:_s1_._n_>=_0 percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6; suppose n = 0 ; ::_thesis: s1 . n >= 0 hence s1 . n >= 0 by A6; ::_thesis: verum end; suppose ex m being Nat st n = m + 1 ; ::_thesis: s1 . n >= 0 then n to_power p > 0 by POWER:34; then 1 / (n to_power p) >= 0 ; hence s1 . n >= 0 by A6; ::_thesis: verum end; end; end; hence ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) ) by A7; ::_thesis: verum end; A27: now__::_thesis:_for_n_being_Element_of_NAT_holds_(s_^\_1)_._n_>=_0 let n be Element of NAT ; ::_thesis: (s ^\ 1) . n >= 0 A28: n + 1 >= 0 + 1 by XREAL_1:6; A29: s1 . (n + 1) >= 0 by A26; (s ^\ 1) . n = s . (n + 1) by NAT_1:def_3 .= 1 / ((n + 1) to_power p) by A2, A28 .= s1 . (n + 1) by A6 .= (s1 ^\ 1) . n by NAT_1:def_3 ; hence (s ^\ 1) . n >= 0 by A29, NAT_1:def_3; ::_thesis: verum end; A30: s3 is convergent by A24, SEQ_4:21; 1 - p < 0 by A1, XREAL_1:49; then lim s3 < 1 by A25, POWER:36; then s2 is summable by A18, A19, A30, Th28; then s1 is summable by A15, A26, Th31; then s1 ^\ 1 is summable by Th12; then s ^\ 1 is summable by A27, A16, Th19; hence s is summable by Th13; ::_thesis: verum end; theorem :: SERIES_1:33 for p being real number for s being Real_Sequence st p <= 1 & ( for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ) holds not s is summable proof let p be real number ; ::_thesis: for s being Real_Sequence st p <= 1 & ( for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ) holds not s is summable let s be Real_Sequence; ::_thesis: ( p <= 1 & ( for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ) implies not s is summable ) assume that A1: p <= 1 and A2: for n being Element of NAT st n >= 1 holds s . n = 1 / (n to_power p) ; ::_thesis: not s is summable now__::_thesis:_not_s_is_summable percases ( p < 0 or p >= 0 ) ; supposeA3: p < 0 ; ::_thesis: not s is summable now__::_thesis:_(_s_is_convergent_implies_not_lim_s_=_0_) assume ( s is convergent & lim s = 0 ) ; ::_thesis: contradiction then consider m being Element of NAT such that A4: for n being Element of NAT st n >= m holds abs ((s . n) - 0) < 1 by SEQ_2:def_7; consider k being Element of NAT such that A5: k > m by SEQ_4:3; now__::_thesis:_for_n_being_Element_of_NAT_holds_not_n_>=_k let n be Element of NAT ; ::_thesis: not n >= k assume A6: n >= k ; ::_thesis: contradiction A7: n > 0 by A5, A6; then A8: n >= 0 + 1 by NAT_1:13; n >= m by A5, A6, XXREAL_0:2; then abs ((s . n) - 0) < 1 by A4; then abs (1 / (n to_power p)) < 1 by A2, A8; then abs (n to_power (- p)) < 1 by A7, POWER:28; then A9: n to_power (- p) < 1 by ABSVALUE:def_1; n #R (- p) >= 1 by A3, A8, PREPOWER:85; hence contradiction by A7, A9, POWER:def_2; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; hence not s is summable by Th4; ::_thesis: verum end; supposeA10: p >= 0 ; ::_thesis: not s is summable defpred S1[ Element of NAT , real number ] means ( ( $1 = 0 & $2 = 1 ) or ( $1 >= 1 & $2 = 1 / ($1 to_power p) ) ); A11: for n being Element of NAT ex r being Real st S1[n,r] proof let n be Element of NAT ; ::_thesis: ex r being Real st S1[n,r] ( n = 0 or n >= 1 ) proof assume that A12: n <> 0 and A13: n < 1 ; ::_thesis: contradiction n >= 0 + 1 by A12, NAT_1:13; hence contradiction by A13; ::_thesis: verum end; hence ex r being Real st S1[n,r] ; ::_thesis: verum end; consider s1 being Real_Sequence such that A14: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A11); A15: s1 . 0 = 1 by A14; now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._(n_+_1)_<=_s1_._n let n be Element of NAT ; ::_thesis: s1 . (n + 1) <= s1 . n now__::_thesis:_s1_._(n_+_1)_<=_s1_._n percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6; supposeA16: n = 0 ; ::_thesis: s1 . (n + 1) <= s1 . n then (n + 1) #R p >= 1 by A10, PREPOWER:85; then A17: (n + 1) to_power p >= 1 by POWER:def_2; s1 . (n + 1) = 1 / ((n + 1) to_power p) by A14; hence s1 . (n + 1) <= s1 . n by A15, A16, A17, XREAL_1:211; ::_thesis: verum end; supposeA18: ex m being Nat st n = m + 1 ; ::_thesis: s1 . (n + 1) <= s1 . n then n to_power p > 0 by POWER:34; then 1 / (n to_power p) > 0 ; then A19: s1 . n > 0 by A14; A20: n / (n + 1) <= 1 by NAT_1:11, XREAL_1:183; A21: n / (n + 1) > 0 by A18; (s1 . (n + 1)) / (s1 . n) = (1 / ((n + 1) to_power p)) / (s1 . n) by A14 .= (1 / ((n + 1) to_power p)) / (1 / (n to_power p)) by A14, A18 .= (1 / ((n + 1) to_power p)) * (n to_power p) .= (n to_power p) / ((n + 1) to_power p) .= (n / (n + 1)) to_power p by A18, POWER:31 .= (n / (n + 1)) #R p by A21, POWER:def_2 ; then (s1 . (n + 1)) / (s1 . n) <= (n / (n + 1)) #R 0 by A10, A21, A20, PREPOWER:84; then (s1 . (n + 1)) / (s1 . n) <= 1 by A18, PREPOWER:71; hence s1 . (n + 1) <= s1 . n by A19, XREAL_1:187; ::_thesis: verum end; end; end; hence s1 . (n + 1) <= s1 . n ; ::_thesis: verum end; then A22: s1 is V42() by SEQM_3:def_9; A23: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_1_holds_ s_._n_>=_s1_._n let n be Element of NAT ; ::_thesis: ( n >= 1 implies s . n >= s1 . n ) assume A24: n >= 1 ; ::_thesis: s . n >= s1 . n then s . n = 1 / (n to_power p) by A2 .= s1 . n by A14, A24 ; hence s . n >= s1 . n ; ::_thesis: verum end; deffunc H1( Element of NAT ) -> Element of REAL = (2 to_power $1) * (s1 . (2 to_power $1)); consider s2 being Real_Sequence such that A25: for n being Element of NAT holds s2 . n = H1(n) from SEQ_1:sch_1(); A26: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_s1_._n_>=_0_&_s2_._n_=_(2_to_power_n)_*_(s1_._(2_to_power_n))_) let n be Element of NAT ; ::_thesis: ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) ) now__::_thesis:_s1_._n_>=_0 percases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6; suppose n = 0 ; ::_thesis: s1 . n >= 0 hence s1 . n >= 0 by A14; ::_thesis: verum end; suppose ex m being Nat st n = m + 1 ; ::_thesis: s1 . n >= 0 then n to_power p > 0 by POWER:34; then 1 / (n to_power p) >= 0 ; hence s1 . n >= 0 by A14; ::_thesis: verum end; end; end; hence ( s1 . n >= 0 & s2 . n = (2 to_power n) * (s1 . (2 to_power n)) ) by A25; ::_thesis: verum end; now__::_thesis:_(_s2_is_convergent_implies_not_lim_s2_=_0_) assume ( s2 is convergent & lim s2 = 0 ) ; ::_thesis: contradiction then consider m being Element of NAT such that A27: for n being Element of NAT st n >= m holds abs ((s2 . n) - 0) < 1 / 2 by SEQ_2:def_7; now__::_thesis:_for_n_being_Element_of_NAT_holds_not_n_>=_m let n be Element of NAT ; ::_thesis: not n >= m assume n >= m ; ::_thesis: contradiction then abs ((s2 . n) - 0) < 1 / 2 by A27; then A28: abs ((2 to_power n) * (s1 . (2 to_power n))) < 1 / 2 by A25; 2 to_power n >= 1 by PREPOWER:11; then abs ((2 to_power n) * (1 / ((2 to_power n) to_power p))) < 1 / 2 by A14, A28; then abs ((2 to_power n) * (1 / (2 to_power (n * p)))) < 1 / 2 by POWER:33; then abs ((2 to_power n) * (2 to_power (- (n * p)))) < 1 / 2 by POWER:28; then abs (2 to_power (n + (- (n * p)))) < 1 / 2 by POWER:27; then 2 to_power (n - (n * p)) < 1 / 2 by ABSVALUE:def_1; then (2 to_power (n - (n * p))) * 2 < (1 / 2) * 2 by XREAL_1:68; then (2 to_power (n - (n * p))) * (2 to_power 1) < 1 by POWER:25; then A29: 2 to_power ((n - (n * p)) + 1) < 1 by POWER:27; 1 - p >= 0 by A1, XREAL_1:48; then n * (1 - p) >= 0 ; then 2 #R ((n - (n * p)) + 1) >= 1 by PREPOWER:85; hence contradiction by A29, POWER:def_2; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; then not s2 is summable by Th4; then not s1 is summable by A22, A26, Th31; hence not s is summable by A26, A23, Th19; ::_thesis: verum end; end; end; hence not s is summable ; ::_thesis: verum end; definition let s be Real_Sequence; attrs is absolutely_summable means :Def4: :: SERIES_1:def 4 abs s is summable ; end; :: deftheorem Def4 defines absolutely_summable SERIES_1:def_4_:_ for s being Real_Sequence holds ( s is absolutely_summable iff abs s is summable ); theorem Th34: :: SERIES_1:34 for s being Real_Sequence for n, m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) proof let s be Real_Sequence; ::_thesis: for n, m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) let n, m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) ) assume A1: n <= m ; ::_thesis: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) reconsider u = n, v = m as Integer ; set s2 = Partial_Sums (abs s); set s1 = Partial_Sums s; defpred S1[ Element of NAT ] means abs (((Partial_Sums s) . (n + $1)) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . (n + $1)) - ((Partial_Sums (abs s)) . n)); now__::_thesis:_for_k_being_Element_of_NAT_holds_(abs_s)_._k_>=_0 let k be Element of NAT ; ::_thesis: (abs s) . k >= 0 abs (s . k) >= 0 by COMPLEX1:46; hence (abs s) . k >= 0 by SEQ_1:12; ::_thesis: verum end; then A2: Partial_Sums (abs s) is V41() by Th16; A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A4: abs (s . ((n + k) + 1)) >= 0 by COMPLEX1:46; assume abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)) ; ::_thesis: S1[k + 1] then A5: (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))) by XREAL_1:7; A6: abs (((Partial_Sums (abs s)) . (n + (k + 1))) - ((Partial_Sums (abs s)) . n)) = abs ((((Partial_Sums (abs s)) . (n + k)) + ((abs s) . ((n + k) + 1))) - ((Partial_Sums (abs s)) . n)) by Def1 .= abs (((abs (s . ((n + k) + 1))) + ((Partial_Sums (abs s)) . (n + k))) - ((Partial_Sums (abs s)) . n)) by SEQ_1:12 .= abs ((abs (s . ((n + k) + 1))) + (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))) ; (Partial_Sums (abs s)) . (n + k) >= (Partial_Sums (abs s)) . n by A2, SEQM_3:5; then A7: ((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n) >= 0 by XREAL_1:48; abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) = abs (((s . ((n + k) + 1)) + ((Partial_Sums s) . (n + k))) - ((Partial_Sums s) . n)) by Def1 .= abs ((s . ((n + k) + 1)) + (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) ; then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums s) . (n + k)) - ((Partial_Sums s) . n))) by COMPLEX1:56; then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (s . ((n + k) + 1))) + (abs (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n))) by A5, XXREAL_0:2; then abs (((Partial_Sums s) . (n + (k + 1))) - ((Partial_Sums s) . n)) <= (abs (s . ((n + k) + 1))) + (((Partial_Sums (abs s)) . (n + k)) - ((Partial_Sums (abs s)) . n)) by A7, ABSVALUE:def_1; hence S1[k + 1] by A7, A4, A6, ABSVALUE:def_1; ::_thesis: verum end; reconsider k = v - u as Element of NAT by A1, INT_1:5; A8: n + k = m ; A9: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A3); hence abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) by A8; ::_thesis: verum end; registration cluster Function-like V18( NAT , REAL ) absolutely_summable -> summable for Element of K19(K20(NAT,REAL)); coherence for b1 being Real_Sequence st b1 is absolutely_summable holds b1 is summable proof let s be Real_Sequence; ::_thesis: ( s is absolutely_summable implies s is summable ) assume s is absolutely_summable ; ::_thesis: s is summable then A1: abs s is summable by Def4; now__::_thesis:_for_r_being_real_number_st_0_<_r_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_(((Partial_Sums_s)_._m)_-_((Partial_Sums_s)_._n))_<_r let r be real number ; ::_thesis: ( 0 < r implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) assume 0 < r ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r then consider n being Element of NAT such that A2: for m being Element of NAT st n <= m holds abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) < r by A1, Th21; take n = n; ::_thesis: for m being Element of NAT st n <= m holds abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r ) assume A3: n <= m ; ::_thesis: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r then A4: abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) <= abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) by Th34; abs (((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)) < r by A2, A3; hence abs (((Partial_Sums s) . m) - ((Partial_Sums s) . n)) < r by A4, XXREAL_0:2; ::_thesis: verum end; hence s is summable by Th21; ::_thesis: verum end; end; theorem :: SERIES_1:35 for s being Real_Sequence st s is absolutely_summable holds s is summable ; theorem :: SERIES_1:36 for s being Real_Sequence st ( for n being Element of NAT holds 0 <= s . n ) & s is summable holds s is absolutely_summable proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= s . n ) & s is summable implies s is absolutely_summable ) assume that A1: for n being Element of NAT holds 0 <= s . n and A2: s is summable ; ::_thesis: s is absolutely_summable A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_s_._n_=_abs_(s_._n) let n be Element of NAT ; ::_thesis: s . n = abs (s . n) 0 <= s . n by A1; hence s . n = abs (s . n) by ABSVALUE:def_1; ::_thesis: verum end; Partial_Sums s is convergent by A2, Def2; then Partial_Sums (abs s) is convergent by A3, SEQ_1:12; then abs s is summable by Def2; hence s is absolutely_summable by Def4; ::_thesis: verum end; theorem :: SERIES_1:37 for s, s1 being Real_Sequence st ( for n being Element of NAT holds ( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) ) & s1 is convergent & lim s1 < 1 holds s is absolutely_summable proof let s, s1 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) ) & s1 is convergent & lim s1 < 1 implies s is absolutely_summable ) assume that A1: for n being Element of NAT holds ( s . n <> 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) and A2: ( s1 is convergent & lim s1 < 1 ) ; ::_thesis: s is absolutely_summable now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(abs_s)_._n_>_0_&_s1_._n_=_((abs_s)_._(n_+_1))_/_((abs_s)_._n)_) let n be Element of NAT ; ::_thesis: ( (abs s) . n > 0 & s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) ) ( (abs s) . n = abs (s . n) & s . n <> 0 ) by A1, SEQ_1:12; hence (abs s) . n > 0 by COMPLEX1:47; ::_thesis: s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) thus s1 . n = ((abs s) . (n + 1)) / ((abs s) . n) by A1; ::_thesis: verum end; then abs s is summable by A2, Th26; hence s is absolutely_summable by Def4; ::_thesis: verum end; theorem Th38: :: SERIES_1:38 for r being real number for s being Real_Sequence st r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds abs (s . n) >= r & s is convergent holds lim s <> 0 proof let r be real number ; ::_thesis: for s being Real_Sequence st r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds abs (s . n) >= r & s is convergent holds lim s <> 0 let s be Real_Sequence; ::_thesis: ( r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds abs (s . n) >= r & s is convergent implies lim s <> 0 ) assume A1: r > 0 ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st ( n >= m & not abs (s . n) >= r ) or not s is convergent or lim s <> 0 ) given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds abs (s . n) >= r ; ::_thesis: ( not s is convergent or lim s <> 0 ) now__::_thesis:_(_not_s_is_convergent_or_lim_s_<>_0_) percases ( not s is convergent or s is convergent ) ; suppose not s is convergent ; ::_thesis: ( not s is convergent or lim s <> 0 ) hence ( not s is convergent or lim s <> 0 ) ; ::_thesis: verum end; supposeA3: s is convergent ; ::_thesis: ( not s is convergent or lim s <> 0 ) now__::_thesis:_not_lim_s_=_0 assume lim s = 0 ; ::_thesis: contradiction then consider k being Element of NAT such that A4: for n being Element of NAT st n >= k holds abs ((s . n) - 0) < r by A1, A3, SEQ_2:def_7; now__::_thesis:_for_n_being_Element_of_NAT_holds_not_n_>=_m_+_k let n be Element of NAT ; ::_thesis: not n >= m + k assume A5: n >= m + k ; ::_thesis: contradiction m + k >= k by NAT_1:11; then n >= k by A5, XXREAL_0:2; then A6: abs ((s . n) - 0) < r by A4; m + k >= m by NAT_1:11; then n >= m by A5, XXREAL_0:2; hence contradiction by A2, A6; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; hence ( not s is convergent or lim s <> 0 ) ; ::_thesis: verum end; end; end; hence ( not s is convergent or lim s <> 0 ) ; ::_thesis: verum end; theorem :: SERIES_1:39 for s being Real_Sequence st ( for n being Element of NAT holds s . n <> 0 ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds ((abs s) . (n + 1)) / ((abs s) . n) >= 1 holds not s is summable proof let s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s . n <> 0 ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds ((abs s) . (n + 1)) / ((abs s) . n) >= 1 implies not s is summable ) assume A1: for n being Element of NAT holds s . n <> 0 ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st ( n >= m & not ((abs s) . (n + 1)) / ((abs s) . n) >= 1 ) or not s is summable ) given m being Element of NAT such that A2: for n being Element of NAT st n >= m holds ((abs s) . (n + 1)) / ((abs s) . n) >= 1 ; ::_thesis: not s is summable A3: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_ abs_(s_._n)_>=_abs_(s_._m) defpred S1[ Element of NAT ] means abs (s . (m + $1)) >= abs (s . m); A4: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A5: abs (s . (m + k)) >= abs (s . m) ; ::_thesis: S1[k + 1] ((abs s) . ((m + k) + 1)) / ((abs s) . (m + k)) >= 1 by A2, NAT_1:11; then (abs (s . ((m + k) + 1))) / ((abs s) . (m + k)) >= 1 by SEQ_1:12; then A6: (abs (s . ((m + k) + 1))) / (abs (s . (m + k))) >= 1 by SEQ_1:12; s . (m + k) <> 0 by A1; then abs (s . (m + k)) > 0 by COMPLEX1:47; then abs (s . ((m + k) + 1)) >= abs (s . (m + k)) by A6, XREAL_1:191; hence S1[k + 1] by A5, XXREAL_0:2; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: ( n >= m implies abs (s . n) >= abs (s . m) ) assume n >= m ; ::_thesis: abs (s . n) >= abs (s . m) then consider k being Nat such that A7: n = m + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; A8: n = m + k by A7; A9: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A4); hence abs (s . n) >= abs (s . m) by A8; ::_thesis: verum end; s . m <> 0 by A1; then abs (s . m) > 0 by COMPLEX1:47; then ( not s is convergent or lim s <> 0 ) by A3, Th38; hence not s is summable by Th4; ::_thesis: verum end; theorem :: SERIES_1:40 for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 < 1 holds s is absolutely_summable proof let s1, s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 < 1 implies s is absolutely_summable ) assume that A1: for n being Element of NAT holds s1 . n = n -root ((abs s) . n) and A2: ( s1 is convergent & lim s1 < 1 ) ; ::_thesis: s is absolutely_summable now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(abs_s)_._n_>=_0_&_s1_._n_=_n_-root_((abs_s)_._n)_) let n be Element of NAT ; ::_thesis: ( (abs s) . n >= 0 & s1 . n = n -root ((abs s) . n) ) (abs s) . n = abs (s . n) by SEQ_1:12; hence (abs s) . n >= 0 by COMPLEX1:46; ::_thesis: s1 . n = n -root ((abs s) . n) thus s1 . n = n -root ((abs s) . n) by A1; ::_thesis: verum end; then abs s is summable by A2, Th28; hence s is absolutely_summable by Def4; ::_thesis: verum end; theorem :: SERIES_1:41 for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds s1 . n >= 1 holds not s is summable proof let s1, s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds s1 . n >= 1 implies not s is summable ) assume A1: for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ; ::_thesis: ( for m being Element of NAT ex n being Element of NAT st ( m <= n & not s1 . n >= 1 ) or not s is summable ) given m being Element of NAT such that A2: for n being Element of NAT st m <= n holds s1 . n >= 1 ; ::_thesis: not s is summable now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_ abs_(s_._n)_>=_1 let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies abs (s . n) >= 1 ) assume A3: n >= m + 1 ; ::_thesis: abs (s . n) >= 1 m + 1 >= 1 by NAT_1:11; then A4: n >= 1 by A3, XXREAL_0:2; m + 1 >= m by NAT_1:11; then A5: n >= m by A3, XXREAL_0:2; s1 . n = n -root ((abs s) . n) by A1 .= n -root (abs (s . n)) by SEQ_1:12 ; then ( abs (s . n) >= 0 & (n -root (abs (s . n))) |^ n >= 1 ) by A2, A5, COMPLEX1:46, PREPOWER:11; hence abs (s . n) >= 1 by A4, POWER:4; ::_thesis: verum end; then ( not s is convergent or lim s <> 0 ) by Th38; hence not s is summable by Th4; ::_thesis: verum end; theorem :: SERIES_1:42 for s1, s being Real_Sequence st ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 > 1 holds not s is summable proof let s1, s be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds s1 . n = n -root ((abs s) . n) ) & s1 is convergent & lim s1 > 1 implies not s is summable ) assume that A1: for n being Element of NAT holds s1 . n = n -root ((abs s) . n) and A2: s1 is convergent and A3: lim s1 > 1 ; ::_thesis: not s is summable (lim s1) - 1 > 0 by A3, XREAL_1:50; then consider m being Element of NAT such that A4: for n being Element of NAT st n >= m holds abs ((s1 . n) - (lim s1)) < (lim s1) - 1 by A2, SEQ_2:def_7; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_+_1_holds_ abs_(s_._n)_>=_1 let n be Element of NAT ; ::_thesis: ( n >= m + 1 implies abs (s . n) >= 1 ) assume A5: n >= m + 1 ; ::_thesis: abs (s . n) >= 1 A6: s1 . n = n -root ((abs s) . n) by A1 .= n -root (abs (s . n)) by SEQ_1:12 ; m + 1 >= m by NAT_1:11; then n >= m by A5, XXREAL_0:2; then abs ((n -root (abs (s . n))) - (lim s1)) < (lim s1) - 1 by A4, A6; then - ((lim s1) - 1) < (n -root (abs (s . n))) - (lim s1) by SEQ_2:1; then (1 - (lim s1)) + (lim s1) < ((n -root (abs (s . n))) - (lim s1)) + (lim s1) by XREAL_1:6; then A7: ( abs (s . n) >= 0 & (n -root (abs (s . n))) |^ n >= 1 ) by COMPLEX1:46, PREPOWER:11; m + 1 >= 1 by NAT_1:11; then n >= 1 by A5, XXREAL_0:2; hence abs (s . n) >= 1 by A7, POWER:4; ::_thesis: verum end; then ( not s is convergent or lim s <> 0 ) by Th38; hence not s is summable by Th4; ::_thesis: verum end; begin definition let s be Real_Sequence; let n be Nat; func Sum (s,n) -> Real equals :: SERIES_1:def 5 (Partial_Sums s) . n; coherence (Partial_Sums s) . n is Real ; end; :: deftheorem defines Sum SERIES_1:def_5_:_ for s being Real_Sequence for n being Nat holds Sum (s,n) = (Partial_Sums s) . n; definition let s be Real_Sequence; let n, m be Nat; func Sum (s,n,m) -> Real equals :: SERIES_1:def 6 (Sum (s,n)) - (Sum (s,m)); coherence (Sum (s,n)) - (Sum (s,m)) is Real ; end; :: deftheorem defines Sum SERIES_1:def_6_:_ for s being Real_Sequence for n, m being Nat holds Sum (s,n,m) = (Sum (s,n)) - (Sum (s,m));