:: COMSEQ_3 semantic presentation begin Lm1: 0c = 0 + (0 * ) ; theorem :: COMSEQ_3:1 for n being Element of NAT holds ( n + 1 <> 0c & (n + 1) * <> 0c ) ; theorem Th2: :: COMSEQ_3:2 for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds for m being Element of NAT holds (Partial_Sums (abs rseq)) . m = 0 proof let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq . n = 0 ) implies for m being Element of NAT holds (Partial_Sums (abs rseq)) . m = 0 ) defpred S1[ Element of NAT ] means (abs rseq) . \$1 = (Partial_Sums (abs rseq)) . \$1; assume A1: for n being Element of NAT holds rseq . n = 0 ; ::_thesis: for m being Element of NAT holds (Partial_Sums (abs rseq)) . m = 0 A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1] thus (abs rseq) . (k + 1) = 0 + ((abs rseq) . (k + 1)) .= (abs 0) + ((abs rseq) . (k + 1)) by ABSVALUE:def_1 .= (abs (rseq . k)) + ((abs rseq) . (k + 1)) by A1 .= ((Partial_Sums (abs rseq)) . k) + ((abs rseq) . (k + 1)) by A3, SEQ_1:12 .= (Partial_Sums (abs rseq)) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum end; let m be Element of NAT ; ::_thesis: (Partial_Sums (abs rseq)) . m = 0 A4: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (Partial_Sums (abs rseq)) . m = (abs rseq) . m .= abs (rseq . m) by SEQ_1:12 .= abs 0 by A1 .= 0 by ABSVALUE:def_1 ; ::_thesis: verum end; theorem Th3: :: COMSEQ_3:3 for rseq being Real_Sequence st ( for n being Element of NAT holds rseq . n = 0 ) holds rseq is absolutely_summable proof let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq . n = 0 ) implies rseq is absolutely_summable ) assume A1: for n being Element of NAT holds rseq . n = 0 ; ::_thesis: rseq is absolutely_summable take 0 ; :: according to SEQ_2:def_6,SERIES_1:def_2,SERIES_1:def_4 ::_thesis: for b1 being set holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= abs (((Partial_Sums (abs rseq)) . b3) - 0) ) ) let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs (((Partial_Sums (abs rseq)) . b2) - 0) ) ) assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs (((Partial_Sums (abs rseq)) . b2) - 0) ) take 0 ; ::_thesis: for b1 being Element of NAT holds ( not 0 <= b1 or not p <= abs (((Partial_Sums (abs rseq)) . b1) - 0) ) let m be Element of NAT ; ::_thesis: ( not 0 <= m or not p <= abs (((Partial_Sums (abs rseq)) . m) - 0) ) assume 0 <= m ; ::_thesis: not p <= abs (((Partial_Sums (abs rseq)) . m) - 0) abs (((Partial_Sums (abs rseq)) . m) - 0) = abs (0 - 0) by A1, Th2 .= 0 by ABSVALUE:def_1 ; hence abs (((Partial_Sums (abs rseq)) . m) - 0) < p by A2; ::_thesis: verum end; reconsider C = NAT --> 0 as Real_Sequence by FUNCOP_1:45; Lm2: for n being Element of NAT holds C . n = 0 by FUNCOP_1:7; registration cluster Function-like V18( NAT , REAL ) summable -> convergent for Element of K19(K20(NAT,REAL)); coherence for b1 being Real_Sequence st b1 is summable holds b1 is convergent by SERIES_1:4; 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 ; end; registration cluster Relation-like NAT -defined REAL -valued Function-like non zero total V18( NAT , REAL ) complex-valued ext-real-valued real-valued absolutely_summable for Element of K19(K20(NAT,REAL)); existence ex b1 being Real_Sequence st b1 is absolutely_summable by Lm2, Th3; end; theorem :: COMSEQ_3:4 for rseq being Real_Sequence st rseq is convergent holds for p being Real st 0 < p holds ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds abs ((rseq . m) - (rseq . l)) < p proof let rseq be Real_Sequence; ::_thesis: ( rseq is convergent implies for p being Real st 0 < p holds ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds abs ((rseq . m) - (rseq . l)) < p ) assume A1: rseq is convergent ; ::_thesis: for p being Real st 0 < p holds ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds abs ((rseq . m) - (rseq . l)) < p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds abs ((rseq . m) - (rseq . l)) < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds abs ((rseq . m) - (rseq . l)) < p then consider n being Element of NAT such that A2: for m being Element of NAT st n <= m holds abs ((rseq . m) - (rseq . n)) < p / 2 by A1, SEQ_4:41; take n ; ::_thesis: for m, l being Element of NAT st n <= m & n <= l holds abs ((rseq . m) - (rseq . l)) < p now__::_thesis:_for_m,_l_being_Element_of_NAT_st_n_<=_m_&_n_<=_l_holds_ abs_((rseq_._m)_-_(rseq_._l))_<_p let m, l be Element of NAT ; ::_thesis: ( n <= m & n <= l implies abs ((rseq . m) - (rseq . l)) < p ) assume ( n <= m & n <= l ) ; ::_thesis: abs ((rseq . m) - (rseq . l)) < p then ( abs ((rseq . m) - (rseq . n)) < p / 2 & abs ((rseq . l) - (rseq . n)) < p / 2 ) by A2; then A3: (abs ((rseq . m) - (rseq . n))) + (abs ((rseq . l) - (rseq . n))) < (p / 2) + (p / 2) by XREAL_1:8; abs ((rseq . m) - (rseq . l)) = abs (((rseq . m) - (rseq . n)) - ((rseq . l) - (rseq . n))) ; then abs ((rseq . m) - (rseq . l)) <= (abs ((rseq . m) - (rseq . n))) + (abs ((rseq . l) - (rseq . n))) by COMPLEX1:57; hence abs ((rseq . m) - (rseq . l)) < p by A3, XXREAL_0:2; ::_thesis: verum end; hence for m, l being Element of NAT st n <= m & n <= l holds abs ((rseq . m) - (rseq . l)) < p ; ::_thesis: verum end; theorem :: COMSEQ_3:5 for rseq being Real_Sequence for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l proof let rseq be Real_Sequence; ::_thesis: for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l let p be Real; ::_thesis: ( ( for n being Element of NAT holds rseq . n <= p ) implies for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l ) assume A1: for n being Element of NAT holds rseq . n <= p ; ::_thesis: for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l now__::_thesis:_for_n,_l_being_Element_of_NAT_holds_S1[l] let n be Element of NAT ; ::_thesis: for l being Element of NAT holds S1[l] defpred S1[ Element of NAT ] means ((Partial_Sums rseq) . (n + \$1)) - ((Partial_Sums rseq) . n) <= p * \$1; A2: now__::_thesis:_for_l_being_Element_of_NAT_st_S1[l]_holds_ S1[l_+_1] let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] ) assume A3: S1[l] ; ::_thesis: S1[l + 1] rseq . ((n + l) + 1) <= p by A1; then A4: (p * l) + (rseq . ((n + l) + 1)) <= (p * l) + p by XREAL_1:6; ((Partial_Sums rseq) . (n + (l + 1))) - ((Partial_Sums rseq) . n) = (((Partial_Sums rseq) . (n + l)) + (rseq . ((n + l) + 1))) - ((Partial_Sums rseq) . n) by SERIES_1:def_1 .= (((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n)) + (rseq . ((n + l) + 1)) ; then ((Partial_Sums rseq) . (n + (l + 1))) - ((Partial_Sums rseq) . n) <= (p * l) + (rseq . ((n + l) + 1)) by A3, XREAL_1:6; hence S1[l + 1] by A4, XXREAL_0:2; ::_thesis: verum end; A5: S1[ 0 ] ; thus for l being Element of NAT holds S1[l] from NAT_1:sch_1(A5, A2); ::_thesis: verum end; hence for n, l being Element of NAT holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l ; ::_thesis: verum end; theorem :: COMSEQ_3:6 for rseq being Real_Sequence for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1) proof let rseq be Real_Sequence; ::_thesis: for p being Real st ( for n being Element of NAT holds rseq . n <= p ) holds for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1) let p be Real; ::_thesis: ( ( for n being Element of NAT holds rseq . n <= p ) implies for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1) ) defpred S1[ Element of NAT ] means (Partial_Sums rseq) . \$1 <= p * (\$1 + 1); assume A1: for n being Element of NAT holds rseq . n <= p ; ::_thesis: for n being Element of NAT holds (Partial_Sums rseq) . n <= p * (n + 1) A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] rseq . (n + 1) <= p by A1; then A4: (p * (n + 1)) + (rseq . (n + 1)) <= (p * (n + 1)) + p by XREAL_1:6; (Partial_Sums rseq) . (n + 1) = ((Partial_Sums rseq) . n) + (rseq . (n + 1)) by SERIES_1:def_1; then (Partial_Sums rseq) . (n + 1) <= (p * (n + 1)) + (rseq . (n + 1)) by A3, XREAL_1:6; hence S1[n + 1] by A4, XXREAL_0:2; ::_thesis: verum end; (Partial_Sums rseq) . 0 = rseq . 0 by SERIES_1:def_1; 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 :: COMSEQ_3:7 for rseq1, rseq2 being Real_Sequence for m being Element of NAT for p being Real st ( for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ) holds (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) proof let rseq1, rseq2 be Real_Sequence; ::_thesis: for m being Element of NAT for p being Real st ( for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ) holds (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) let m be Element of NAT ; ::_thesis: for p being Real st ( for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ) holds (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) let p be Real; ::_thesis: ( ( for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ) implies (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) ) defpred S1[ Element of NAT ] means ( \$1 <= m implies (Partial_Sums rseq1) . \$1 <= p * ((Partial_Sums rseq2) . \$1) ); assume A1: for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ; ::_thesis: (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) A2: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A3: S1[n] ; ::_thesis: S1[n + 1] now__::_thesis:_(_n_+_1_<=_m_implies_(Partial_Sums_rseq1)_._(n_+_1)_<=_p_*_((Partial_Sums_rseq2)_._(n_+_1))_) assume A4: n + 1 <= m ; ::_thesis: (Partial_Sums rseq1) . (n + 1) <= p * ((Partial_Sums rseq2) . (n + 1)) then rseq1 . (n + 1) <= p * (rseq2 . (n + 1)) by A1; then A5: (p * ((Partial_Sums rseq2) . n)) + (rseq1 . (n + 1)) <= (p * ((Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1))) by XREAL_1:6; ( n < n + 1 & (Partial_Sums rseq1) . (n + 1) = ((Partial_Sums rseq1) . n) + (rseq1 . (n + 1)) ) by SERIES_1:def_1, XREAL_1:29; then A6: (Partial_Sums rseq1) . (n + 1) <= (p * ((Partial_Sums rseq2) . n)) + (rseq1 . (n + 1)) by A3, A4, XREAL_1:6, XXREAL_0:2; (p * ((Partial_Sums rseq2) . n)) + (p * (rseq2 . (n + 1))) = p * (((Partial_Sums rseq2) . n) + (rseq2 . (n + 1))) .= p * ((Partial_Sums rseq2) . (n + 1)) by SERIES_1:def_1 ; hence (Partial_Sums rseq1) . (n + 1) <= p * ((Partial_Sums rseq2) . (n + 1)) by A6, A5, XXREAL_0:2; ::_thesis: verum end; hence S1[n + 1] ; ::_thesis: verum end; A7: S1[ 0 ] proof assume 0 <= m ; ::_thesis: (Partial_Sums rseq1) . 0 <= p * ((Partial_Sums rseq2) . 0) ( (Partial_Sums rseq1) . 0 = rseq1 . 0 & p * ((Partial_Sums rseq2) . 0) = p * (rseq2 . 0) ) by SERIES_1:def_1; hence (Partial_Sums rseq1) . 0 <= p * ((Partial_Sums rseq2) . 0) by A1; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A2); hence (Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m) ; ::_thesis: verum end; theorem :: COMSEQ_3:8 for rseq1, rseq2 being Real_Sequence for m being Element of NAT for p being Real st ( for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ) holds for n, l being Element of NAT st n + l <= m holds ((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n)) proof let rseq1, rseq2 be Real_Sequence; ::_thesis: for m being Element of NAT for p being Real st ( for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ) holds for n, l being Element of NAT st n + l <= m holds ((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n)) let m be Element of NAT ; ::_thesis: for p being Real st ( for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ) holds for n, l being Element of NAT st n + l <= m holds ((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n)) let p be Real; ::_thesis: ( ( for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ) implies for n, l being Element of NAT st n + l <= m holds ((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n)) ) assume A1: for n being Element of NAT st n <= m holds rseq1 . n <= p * (rseq2 . n) ; ::_thesis: for n, l being Element of NAT st n + l <= m holds ((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n)) let n be Element of NAT ; ::_thesis: for l being Element of NAT st n + l <= m holds ((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n)) defpred S1[ Element of NAT ] means ( n + \$1 <= m implies ((Partial_Sums rseq1) . (n + \$1)) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + \$1)) - ((Partial_Sums rseq2) . n)) ); A2: for l being Element of NAT st S1[l] holds S1[l + 1] proof let l be Element of NAT ; ::_thesis: ( S1[l] implies S1[l + 1] ) assume A3: S1[l] ; ::_thesis: S1[l + 1] assume A4: n + (l + 1) <= m ; ::_thesis: ((Partial_Sums rseq1) . (n + (l + 1))) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + (l + 1))) - ((Partial_Sums rseq2) . n)) then ( (Partial_Sums rseq1) . (n + (l + 1)) = ((Partial_Sums rseq1) . (n + l)) + (rseq1 . ((n + l) + 1)) & rseq1 . ((n + l) + 1) <= p * (rseq2 . ((n + l) + 1)) ) by A1, SERIES_1:def_1; then (Partial_Sums rseq1) . (n + (l + 1)) <= ((Partial_Sums rseq1) . (n + l)) + (p * (rseq2 . ((n + l) + 1))) by XREAL_1:6; then A5: ((Partial_Sums rseq1) . (n + (l + 1))) - ((Partial_Sums rseq1) . n) <= (((Partial_Sums rseq1) . (n + l)) + (p * (rseq2 . ((n + l) + 1)))) - ((Partial_Sums rseq1) . n) by XREAL_1:9; n + l < (n + l) + 1 by XREAL_1:29; then A6: (((Partial_Sums rseq1) . (n + l)) - ((Partial_Sums rseq1) . n)) + (p * (rseq2 . ((n + l) + 1))) <= (p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))) + (p * (rseq2 . ((n + l) + 1))) by A3, A4, XREAL_1:6, XXREAL_0:2; (p * (((Partial_Sums rseq2) . (n + l)) - ((Partial_Sums rseq2) . n))) + (p * (rseq2 . ((n + l) + 1))) = p * ((((Partial_Sums rseq2) . (n + l)) + (rseq2 . ((n + l) + 1))) - ((Partial_Sums rseq2) . n)) .= p * (((Partial_Sums rseq2) . (n + (l + 1))) - ((Partial_Sums rseq2) . n)) by SERIES_1:def_1 ; hence ((Partial_Sums rseq1) . (n + (l + 1))) - ((Partial_Sums rseq1) . n) <= p * (((Partial_Sums rseq2) . (n + (l + 1))) - ((Partial_Sums rseq2) . n)) by A5, A6, XXREAL_0:2; ::_thesis: verum end; A7: S1[ 0 ] ; thus for l being Element of NAT holds S1[l] from NAT_1:sch_1(A7, A2); ::_thesis: verum end; theorem :: COMSEQ_3:9 for rseq being Real_Sequence st ( for n being Element of NAT holds 0 <= rseq . n ) holds ( ( for n, m being Element of NAT st n <= m holds abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) ) proof let rseq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds 0 <= rseq . n ) implies ( ( for n, m being Element of NAT st n <= m holds abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) ) ) assume A1: for n being Element of NAT holds 0 <= rseq . n ; ::_thesis: ( ( for n, m being Element of NAT st n <= m holds abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) ) then A2: Partial_Sums rseq is non-decreasing by SERIES_1:16; A3: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_(((Partial_Sums_rseq)_._m)_-_((Partial_Sums_rseq)_._n))_=_((Partial_Sums_rseq)_._m)_-_((Partial_Sums_rseq)_._n) let n, m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) assume n <= m ; ::_thesis: abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) then (Partial_Sums rseq) . n <= (Partial_Sums rseq) . m by A2, SEQM_3:6; then ((Partial_Sums rseq) . n) - ((Partial_Sums rseq) . n) <= ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) by XREAL_1:9; hence abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) by ABSVALUE:def_1; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_((Partial_Sums_rseq)_._n)_=_(Partial_Sums_rseq)_._n let n be Element of NAT ; ::_thesis: abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n A4: (Partial_Sums rseq) . 0 <= (Partial_Sums rseq) . n by A2, SEQM_3:6; ( (Partial_Sums rseq) . 0 = rseq . 0 & 0 <= rseq . 0 ) by A1, SERIES_1:def_1; hence abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n by A4, ABSVALUE:def_1; ::_thesis: verum end; hence ( ( for n, m being Element of NAT st n <= m holds abs (((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n)) = ((Partial_Sums rseq) . m) - ((Partial_Sums rseq) . n) ) & ( for n being Element of NAT holds abs ((Partial_Sums rseq) . n) = (Partial_Sums rseq) . n ) ) by A3; ::_thesis: verum end; theorem :: COMSEQ_3:10 for seq1, seq2 being Complex_Sequence st seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0c holds lim seq1 = lim seq2 proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 is convergent & seq2 is convergent & lim (seq1 - seq2) = 0c implies lim seq1 = lim seq2 ) assume that A1: ( seq1 is convergent & seq2 is convergent ) and A2: lim (seq1 - seq2) = 0c ; ::_thesis: lim seq1 = lim seq2 lim (seq1 - seq2) = (lim seq1) - (lim seq2) by A1, COMSEQ_2:26; hence lim seq1 = lim seq2 by A2; ::_thesis: verum end; begin Lm3: for seq being Complex_Sequence for n being Element of NAT holds ( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n ) proof let seq be Complex_Sequence; ::_thesis: for n being Element of NAT holds ( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n ) let n be Element of NAT ; ::_thesis: ( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n ) |.(seq . n).| = |.seq.| . n by VALUED_1:18; hence ( |.(seq . n).| = |.seq.| . n & 0 <= |.seq.| . n ) by COMPLEX1:46; ::_thesis: verum end; definition let z be complex number ; funcz GeoSeq -> Complex_Sequence means :Def1: :: COMSEQ_3:def 1 ( it . 0 = 1r & ( for n being Element of NAT holds it . (n + 1) = (it . n) * z ) ); existence ex b1 being Complex_Sequence st ( b1 . 0 = 1r & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) ) proof reconsider z9 = z as Element of COMPLEX by XCMPLX_0:def_2; deffunc H1( set , Element of COMPLEX ) -> Element of COMPLEX = \$2 * z9; consider f being Function of NAT,COMPLEX such that A1: ( f . 0 = 1r & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch_12(); take f ; ::_thesis: ( f . 0 = 1r & ( for n being Element of NAT holds f . (n + 1) = (f . n) * z ) ) thus ( f . 0 = 1r & ( for n being Element of NAT holds f . (n + 1) = (f . n) * z ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Complex_Sequence st b1 . 0 = 1r & ( for n being Element of NAT holds b1 . (n + 1) = (b1 . n) * z ) & b2 . 0 = 1r & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) holds b1 = b2 proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 . 0 = 1r & ( for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) * z ) & seq2 . 0 = 1r & ( for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) * z ) implies seq1 = seq2 ) assume that A2: seq1 . 0 = 1r and A3: for n being Element of NAT holds seq1 . (n + 1) = (seq1 . n) * z and A4: seq2 . 0 = 1r and A5: for n being Element of NAT holds seq2 . (n + 1) = (seq2 . n) * z ; ::_thesis: seq1 = seq2 defpred S1[ Element of NAT ] means seq1 . \$1 = seq2 . \$1; A6: 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] ; ::_thesis: S1[k + 1] hence seq1 . (k + 1) = (seq2 . k) * z by A3 .= seq2 . (k + 1) by A5 ; ::_thesis: verum end; A7: S1[ 0 ] by A2, A4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A6); hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines GeoSeq COMSEQ_3:def_1_:_ for z being complex number for b2 being Complex_Sequence holds ( b2 = z GeoSeq iff ( b2 . 0 = 1r & ( for n being Element of NAT holds b2 . (n + 1) = (b2 . n) * z ) ) ); notation let z be complex number ; let n be natural number ; synonym z #N n for z |^ n; end; definition let z be complex number ; let n be natural number ; :: original: #N redefine funcz #N n -> Element of COMPLEX equals :: COMSEQ_3:def 2 (z GeoSeq) . n; coherence z #N n is Element of COMPLEX by XCMPLX_0:def_2; compatibility for b1 being Element of COMPLEX holds ( b1 = z #N n iff b1 = (z GeoSeq) . n ) proof reconsider n = n as Element of NAT by ORDINAL1:def_12; defpred S1[ Element of NAT ] means z |^ \$1 = (z GeoSeq) . \$1; let w be Element of COMPLEX ; ::_thesis: ( w = z #N n iff w = (z GeoSeq) . n ) A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] hence z |^ (n + 1) = ((z GeoSeq) . n) * z by NEWTON:6 .= (z GeoSeq) . (n + 1) by Def1 ; ::_thesis: verum end; z |^ 0 = 1r by COMPLEX1:def_4, NEWTON:4 .= (z GeoSeq) . 0 by Def1 ; then A2: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); then z |^ n = (z GeoSeq) . n ; hence ( w = z #N n iff w = (z GeoSeq) . n ) ; ::_thesis: verum end; end; :: deftheorem defines #N COMSEQ_3:def_2_:_ for z being complex number for n being natural number holds z #N n = (z GeoSeq) . n; theorem :: COMSEQ_3:11 for z being Element of COMPLEX holds z #N 0 = 1r by COMPLEX1:def_4, NEWTON:4; definition let f be complex-valued Function; set A = dom f; deffunc H1( set ) -> Element of REAL = Re (f . \$1); func Re f -> Function means :Def3: :: COMSEQ_3:def 3 ( dom it = dom f & ( for x being set st x in dom it holds it . x = Re (f . x) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = Re (f . x) ) ) proof ex f being Function st ( dom f = dom f & ( for x being set st x in dom f holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = Re (f . x) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = Re (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = Re (f . x) ) holds b1 = b2 proof let g, h be Function; ::_thesis: ( dom g = dom f & ( for x being set st x in dom g holds g . x = Re (f . x) ) & dom h = dom f & ( for x being set st x in dom h holds h . x = Re (f . x) ) implies g = h ) assume that A1: dom g = dom f and A2: for x being set st x in dom g holds g . x = H1(x) and A3: dom h = dom f and A4: for x being set st x in dom h holds h . x = H1(x) ; ::_thesis: g = h now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_ g_._x_=_h_._x let x be set ; ::_thesis: ( x in dom g implies g . x = h . x ) assume A5: x in dom g ; ::_thesis: g . x = h . x hence g . x = H1(x) by A2 .= h . x by A1, A3, A4, A5 ; ::_thesis: verum end; hence g = h by A1, A3, FUNCT_1:2; ::_thesis: verum end; deffunc H2( set ) -> Element of REAL = Im (f . \$1); func Im f -> Function means :Def4: :: COMSEQ_3:def 4 ( dom it = dom f & ( for x being set st x in dom it holds it . x = Im (f . x) ) ); existence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = Im (f . x) ) ) proof ex f being Function st ( dom f = dom f & ( for x being set st x in dom f holds f . x = H2(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = Im (f . x) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom b1 holds b1 . x = Im (f . x) ) & dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = Im (f . x) ) holds b1 = b2 proof let g, h be Function; ::_thesis: ( dom g = dom f & ( for x being set st x in dom g holds g . x = Im (f . x) ) & dom h = dom f & ( for x being set st x in dom h holds h . x = Im (f . x) ) implies g = h ) assume that A6: dom g = dom f and A7: for x being set st x in dom g holds g . x = H2(x) and A8: dom h = dom f and A9: for x being set st x in dom h holds h . x = H2(x) ; ::_thesis: g = h now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_ g_._x_=_h_._x let x be set ; ::_thesis: ( x in dom g implies g . x = h . x ) assume A10: x in dom g ; ::_thesis: g . x = h . x hence g . x = H2(x) by A7 .= h . x by A6, A8, A9, A10 ; ::_thesis: verum end; hence g = h by A6, A8, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines Re COMSEQ_3:def_3_:_ for f being complex-valued Function for b2 being Function holds ( b2 = Re f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = Re (f . x) ) ) ); :: deftheorem Def4 defines Im COMSEQ_3:def_4_:_ for f being complex-valued Function for b2 being Function holds ( b2 = Im f iff ( dom b2 = dom f & ( for x being set st x in dom b2 holds b2 . x = Im (f . x) ) ) ); registration let f be complex-valued Function; cluster Re f -> real-valued ; coherence Re f is real-valued proof let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (Re f) or (Re f) . x is real ) assume x in dom (Re f) ; ::_thesis: (Re f) . x is real then (Re f) . x = Re (f . x) by Def3; hence (Re f) . x is real ; ::_thesis: verum end; cluster Im f -> real-valued ; coherence Im f is real-valued proof let x be set ; :: according to VALUED_0:def_9 ::_thesis: ( not x in dom (Im f) or (Im f) . x is real ) assume x in dom (Im f) ; ::_thesis: (Im f) . x is real then (Im f) . x = Im (f . x) by Def4; hence (Im f) . x is real ; ::_thesis: verum end; end; definition let X be set ; let f be PartFunc of X,COMPLEX; :: original: Re redefine func Re f -> PartFunc of X,REAL; coherence Re f is PartFunc of X,REAL proof A1: dom f c= X by RELAT_1:def_18; A2: rng (Re f) c= REAL by VALUED_0:def_3; dom (Re f) = dom f by Def3; hence Re f is PartFunc of X,REAL by A1, A2, RELSET_1:4; ::_thesis: verum end; :: original: Im redefine func Im f -> PartFunc of X,REAL; coherence Im f is PartFunc of X,REAL proof A3: dom f c= X by RELAT_1:def_18; A4: rng (Im f) c= REAL by VALUED_0:def_3; dom (Im f) = dom f by Def4; hence Im f is PartFunc of X,REAL by A3, A4, RELSET_1:4; ::_thesis: verum end; end; definition let c be Complex_Sequence; :: original: Re redefine func Re c -> Real_Sequence means :Def5: :: COMSEQ_3:def 5 for n being Element of NAT holds it . n = Re (c . n); coherence Re c is Real_Sequence proof dom (Re c) = dom c by Def3 .= NAT by FUNCT_2:def_1 ; then Re c is total by PARTFUN1:def_2; hence Re c is Real_Sequence ; ::_thesis: verum end; compatibility for b1 being Real_Sequence holds ( b1 = Re c iff for n being Element of NAT holds b1 . n = Re (c . n) ) proof let f be Real_Sequence; ::_thesis: ( f = Re c iff for n being Element of NAT holds f . n = Re (c . n) ) A1: dom (Re c) = dom c by Def3; A2: dom c = NAT by FUNCT_2:def_1; A3: dom f = NAT by FUNCT_2:def_1; hence ( f = Re c implies for n being Element of NAT holds f . n = Re (c . n) ) by Def3; ::_thesis: ( ( for n being Element of NAT holds f . n = Re (c . n) ) implies f = Re c ) assume A4: for n being Element of NAT holds f . n = Re (c . n) ; ::_thesis: f = Re c now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_(Re_c)_._x let x be set ; ::_thesis: ( x in dom f implies f . x = (Re c) . x ) assume A5: x in dom f ; ::_thesis: f . x = (Re c) . x hence f . x = Re (c . x) by A3, A4 .= (Re c) . x by A1, A2, A3, A5, Def3 ; ::_thesis: verum end; hence f = Re c by A1, A2, A3, FUNCT_1:2; ::_thesis: verum end; :: original: Im redefine func Im c -> Real_Sequence means :Def6: :: COMSEQ_3:def 6 for n being Element of NAT holds it . n = Im (c . n); coherence Im c is Real_Sequence proof dom (Im c) = dom c by Def4 .= NAT by FUNCT_2:def_1 ; then Im c is total by PARTFUN1:def_2; hence Im c is Real_Sequence ; ::_thesis: verum end; compatibility for b1 being Real_Sequence holds ( b1 = Im c iff for n being Element of NAT holds b1 . n = Im (c . n) ) proof let f be Real_Sequence; ::_thesis: ( f = Im c iff for n being Element of NAT holds f . n = Im (c . n) ) A6: dom (Im c) = dom c by Def4; A7: dom c = NAT by FUNCT_2:def_1; A8: dom f = NAT by FUNCT_2:def_1; hence ( f = Im c implies for n being Element of NAT holds f . n = Im (c . n) ) by Def4; ::_thesis: ( ( for n being Element of NAT holds f . n = Im (c . n) ) implies f = Im c ) assume A9: for n being Element of NAT holds f . n = Im (c . n) ; ::_thesis: f = Im c now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_(Im_c)_._x let x be set ; ::_thesis: ( x in dom f implies f . x = (Im c) . x ) assume A10: x in dom f ; ::_thesis: f . x = (Im c) . x hence f . x = Im (c . x) by A8, A9 .= (Im c) . x by A6, A7, A8, A10, Def4 ; ::_thesis: verum end; hence f = Im c by A6, A7, A8, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines Re COMSEQ_3:def_5_:_ for c being Complex_Sequence for b2 being Real_Sequence holds ( b2 = Re c iff for n being Element of NAT holds b2 . n = Re (c . n) ); :: deftheorem Def6 defines Im COMSEQ_3:def_6_:_ for c being Complex_Sequence for b2 being Real_Sequence holds ( b2 = Im c iff for n being Element of NAT holds b2 . n = Im (c . n) ); theorem Th12: :: COMSEQ_3:12 for z being Element of COMPLEX holds |.z.| <= (abs (Re z)) + (abs (Im z)) proof let z be Element of COMPLEX ; ::_thesis: |.z.| <= (abs (Re z)) + (abs (Im z)) z = (Re z) + ((Im z) * ) by COMPLEX1:13; then A1: |.z.| <= |.((Re z) + (0 * )).| + |.(0 + ((Im z) * )).| by COMPLEX1:56; ( Re (0 + ((Im z) * )) = 0 & Im (0 + ((Im z) * )) = Im z ) by COMPLEX1:12; hence |.z.| <= (abs (Re z)) + (abs (Im z)) by A1, COMPLEX1:51; ::_thesis: verum end; theorem Th13: :: COMSEQ_3:13 for z being Element of COMPLEX holds ( abs (Re z) <= |.z.| & abs (Im z) <= |.z.| ) proof let z be Element of COMPLEX ; ::_thesis: ( abs (Re z) <= |.z.| & abs (Im z) <= |.z.| ) 0 <= (Re z) ^2 by XREAL_1:63; then A1: 0 + ((Im z) ^2) <= ((Re z) ^2) + ((Im z) ^2) by XREAL_1:6; 0 <= (Im z) ^2 by XREAL_1:63; then A2: sqrt ((Im z) ^2) <= sqrt (((Re z) ^2) + ((Im z) ^2)) by A1, SQUARE_1:26; 0 <= (Im z) ^2 by XREAL_1:63; then A3: 0 + ((Re z) ^2) <= ((Im z) ^2) + ((Re z) ^2) by XREAL_1:6; 0 <= (Re z) ^2 by XREAL_1:63; then ( |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2)) & sqrt ((Re z) ^2) <= sqrt (((Re z) ^2) + ((Im z) ^2)) ) by A3, COMPLEX1:def_12, SQUARE_1:26; hence ( abs (Re z) <= |.z.| & abs (Im z) <= |.z.| ) by A2, COMPLEX1:72; ::_thesis: verum end; theorem Th14: :: COMSEQ_3:14 for seq1, seq2 being Complex_Sequence st Re seq1 = Re seq2 & Im seq1 = Im seq2 holds seq1 = seq2 proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( Re seq1 = Re seq2 & Im seq1 = Im seq2 implies seq1 = seq2 ) assume that A1: Re seq1 = Re seq2 and A2: Im seq1 = Im seq2 ; ::_thesis: seq1 = seq2 now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_seq2_._n let n be Element of NAT ; ::_thesis: seq1 . n = seq2 . n A3: Im (seq1 . n) = (Im seq2) . n by A2, Def6 .= Im (seq2 . n) by Def6 ; Re (seq1 . n) = (Re seq2) . n by A1, Def5 .= Re (seq2 . n) by Def5 ; hence seq1 . n = seq2 . n by A3, COMPLEX1:3; ::_thesis: verum end; hence seq1 = seq2 by FUNCT_2:63; ::_thesis: verum end; theorem Th15: :: COMSEQ_3:15 for seq1, seq2 being Complex_Sequence holds ( (Re seq1) + (Re seq2) = Re (seq1 + seq2) & (Im seq1) + (Im seq2) = Im (seq1 + seq2) ) proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( (Re seq1) + (Re seq2) = Re (seq1 + seq2) & (Im seq1) + (Im seq2) = Im (seq1 + seq2) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((Re_seq1)_+_(Re_seq2))_._n_=_(Re_(seq1_+_seq2))_._n let n be Element of NAT ; ::_thesis: ((Re seq1) + (Re seq2)) . n = (Re (seq1 + seq2)) . n thus ((Re seq1) + (Re seq2)) . n = ((Re seq1) . n) + ((Re seq2) . n) by SEQ_1:7 .= (Re (seq1 . n)) + ((Re seq2) . n) by Def5 .= (Re (seq1 . n)) + (Re (seq2 . n)) by Def5 .= Re ((seq1 . n) + (seq2 . n)) by COMPLEX1:8 .= Re ((seq1 + seq2) . n) by VALUED_1:1 .= (Re (seq1 + seq2)) . n by Def5 ; ::_thesis: verum end; hence (Re seq1) + (Re seq2) = Re (seq1 + seq2) by FUNCT_2:63; ::_thesis: (Im seq1) + (Im seq2) = Im (seq1 + seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_((Im_seq1)_+_(Im_seq2))_._n_=_(Im_(seq1_+_seq2))_._n let n be Element of NAT ; ::_thesis: ((Im seq1) + (Im seq2)) . n = (Im (seq1 + seq2)) . n thus ((Im seq1) + (Im seq2)) . n = ((Im seq1) . n) + ((Im seq2) . n) by SEQ_1:7 .= (Im (seq1 . n)) + ((Im seq2) . n) by Def6 .= (Im (seq1 . n)) + (Im (seq2 . n)) by Def6 .= Im ((seq1 . n) + (seq2 . n)) by COMPLEX1:8 .= Im ((seq1 + seq2) . n) by VALUED_1:1 .= (Im (seq1 + seq2)) . n by Def6 ; ::_thesis: verum end; hence (Im seq1) + (Im seq2) = Im (seq1 + seq2) by FUNCT_2:63; ::_thesis: verum end; theorem Th16: :: COMSEQ_3:16 for seq being Complex_Sequence holds ( - (Re seq) = Re (- seq) & - (Im seq) = Im (- seq) ) proof let seq be Complex_Sequence; ::_thesis: ( - (Re seq) = Re (- seq) & - (Im seq) = Im (- seq) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(-_(Re_seq))_._n_=_(Re_(-_seq))_._n let n be Element of NAT ; ::_thesis: (- (Re seq)) . n = (Re (- seq)) . n thus (- (Re seq)) . n = - ((Re seq) . n) by SEQ_1:10 .= - (Re (seq . n)) by Def5 .= Re (- (seq . n)) by COMPLEX1:17 .= Re ((- seq) . n) by VALUED_1:8 .= (Re (- seq)) . n by Def5 ; ::_thesis: verum end; hence - (Re seq) = Re (- seq) by FUNCT_2:63; ::_thesis: - (Im seq) = Im (- seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_(-_(Im_seq))_._n_=_(Im_(-_seq))_._n let n be Element of NAT ; ::_thesis: (- (Im seq)) . n = (Im (- seq)) . n thus (- (Im seq)) . n = - ((Im seq) . n) by SEQ_1:10 .= - (Im (seq . n)) by Def6 .= Im (- (seq . n)) by COMPLEX1:17 .= Im ((- seq) . n) by VALUED_1:8 .= (Im (- seq)) . n by Def6 ; ::_thesis: verum end; hence - (Im seq) = Im (- seq) by FUNCT_2:63; ::_thesis: verum end; theorem Th17: :: COMSEQ_3:17 for r being Real for z being Element of COMPLEX holds ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) ) proof let r be Real; ::_thesis: for z being Element of COMPLEX holds ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) ) let z be Element of COMPLEX ; ::_thesis: ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) ) reconsider r9 = r as Element of COMPLEX by XCMPLX_0:def_2; r = r + (0 * ) ; then A1: ( Re r = r & Im r = 0 ) by COMPLEX1:12; r * z = (((Re r9) * (Re z)) - ((Im r9) * (Im z))) + ((((Re r9) * (Im z)) + ((Re z) * (Im r9))) * ) by COMPLEX1:def_6 .= (r * (Re z)) + ((r * (Im z)) * ) by A1 ; hence ( r * (Re z) = Re (r * z) & r * (Im z) = Im (r * z) ) by COMPLEX1:12; ::_thesis: verum end; theorem Th18: :: COMSEQ_3:18 for seq1, seq2 being Complex_Sequence holds ( (Re seq1) - (Re seq2) = Re (seq1 - seq2) & (Im seq1) - (Im seq2) = Im (seq1 - seq2) ) proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( (Re seq1) - (Re seq2) = Re (seq1 - seq2) & (Im seq1) - (Im seq2) = Im (seq1 - seq2) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((Re_seq1)_-_(Re_seq2))_._n_=_(Re_(seq1_-_seq2))_._n let n be Element of NAT ; ::_thesis: ((Re seq1) - (Re seq2)) . n = (Re (seq1 - seq2)) . n thus ((Re seq1) - (Re seq2)) . n = ((Re seq1) . n) + ((- (Re seq2)) . n) by SEQ_1:7 .= ((Re seq1) . n) + ((Re (- seq2)) . n) by Th16 .= ((Re seq1) + (Re (- seq2))) . n by SEQ_1:7 .= (Re (seq1 - seq2)) . n by Th15 ; ::_thesis: verum end; hence (Re seq1) - (Re seq2) = Re (seq1 - seq2) by FUNCT_2:63; ::_thesis: (Im seq1) - (Im seq2) = Im (seq1 - seq2) now__::_thesis:_for_n_being_Element_of_NAT_holds_((Im_seq1)_-_(Im_seq2))_._n_=_(Im_(seq1_-_seq2))_._n let n be Element of NAT ; ::_thesis: ((Im seq1) - (Im seq2)) . n = (Im (seq1 - seq2)) . n thus ((Im seq1) - (Im seq2)) . n = ((Im seq1) . n) + ((- (Im seq2)) . n) by SEQ_1:7 .= ((Im seq1) . n) + ((Im (- seq2)) . n) by Th16 .= ((Im seq1) + (Im (- seq2))) . n by SEQ_1:7 .= (Im (seq1 - seq2)) . n by Th15 ; ::_thesis: verum end; hence (Im seq1) - (Im seq2) = Im (seq1 - seq2) by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_3:19 for seq being Complex_Sequence for r being Real holds ( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) ) proof let seq be Complex_Sequence; ::_thesis: for r being Real holds ( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) ) let r be Real; ::_thesis: ( r (#) (Re seq) = Re (r (#) seq) & r (#) (Im seq) = Im (r (#) seq) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(Re_seq))_._n_=_(Re_(r_(#)_seq))_._n let n be Element of NAT ; ::_thesis: (r (#) (Re seq)) . n = (Re (r (#) seq)) . n thus (r (#) (Re seq)) . n = r * ((Re seq) . n) by SEQ_1:9 .= r * (Re (seq . n)) by Def5 .= Re (r * (seq . n)) by Th17 .= Re ((r (#) seq) . n) by VALUED_1:6 .= (Re (r (#) seq)) . n by Def5 ; ::_thesis: verum end; hence r (#) (Re seq) = Re (r (#) seq) by FUNCT_2:63; ::_thesis: r (#) (Im seq) = Im (r (#) seq) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(Im_seq))_._n_=_(Im_(r_(#)_seq))_._n let n be Element of NAT ; ::_thesis: (r (#) (Im seq)) . n = (Im (r (#) seq)) . n thus (r (#) (Im seq)) . n = r * ((Im seq) . n) by SEQ_1:9 .= r * (Im (seq . n)) by Def6 .= Im (r * (seq . n)) by Th17 .= Im ((r (#) seq) . n) by VALUED_1:6 .= (Im (r (#) seq)) . n by Def6 ; ::_thesis: verum end; hence r (#) (Im seq) = Im (r (#) seq) by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_3:20 for seq being Complex_Sequence for z being Element of COMPLEX holds ( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) ) proof let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX holds ( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) ) let z be Element of COMPLEX ; ::_thesis: ( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Re_(z_(#)_seq))_._n_=_(((Re_z)_(#)_(Re_seq))_-_((Im_z)_(#)_(Im_seq)))_._n let n be Element of NAT ; ::_thesis: (Re (z (#) seq)) . n = (((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq))) . n thus (Re (z (#) seq)) . n = Re ((z (#) seq) . n) by Def5 .= Re (z * (seq . n)) by VALUED_1:6 .= Re ((((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n)))) + ((((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z))) * )) by COMPLEX1:def_6 .= ((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n))) by COMPLEX1:12 .= ((Re z) * ((Re seq) . n)) - ((Im z) * (Im (seq . n))) by Def5 .= ((Re z) * ((Re seq) . n)) - ((Im z) * ((Im seq) . n)) by Def6 .= (((Re z) (#) (Re seq)) . n) - ((Im z) * ((Im seq) . n)) by SEQ_1:9 .= (((Re z) (#) (Re seq)) . n) - (((Im z) (#) (Im seq)) . n) by SEQ_1:9 .= (((Re z) (#) (Re seq)) . n) + (- (((Im z) (#) (Im seq)) . n)) .= (((Re z) (#) (Re seq)) . n) + ((- ((Im z) (#) (Im seq))) . n) by SEQ_1:10 .= (((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq))) . n by SEQ_1:7 ; ::_thesis: verum end; hence Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) by FUNCT_2:63; ::_thesis: Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Im_(z_(#)_seq))_._n_=_(((Re_z)_(#)_(Im_seq))_+_((Im_z)_(#)_(Re_seq)))_._n let n be Element of NAT ; ::_thesis: (Im (z (#) seq)) . n = (((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))) . n thus (Im (z (#) seq)) . n = Im ((z (#) seq) . n) by Def6 .= Im (z * (seq . n)) by VALUED_1:6 .= Im ((((Re z) * (Re (seq . n))) - ((Im z) * (Im (seq . n)))) + ((((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z))) * )) by COMPLEX1:def_6 .= ((Re z) * (Im (seq . n))) + ((Re (seq . n)) * (Im z)) by COMPLEX1:12 .= ((Re z) * (Im (seq . n))) + ((Im z) * ((Re seq) . n)) by Def5 .= ((Re z) * ((Im seq) . n)) + ((Im z) * ((Re seq) . n)) by Def6 .= (((Re z) (#) (Im seq)) . n) + ((Im z) * ((Re seq) . n)) by SEQ_1:9 .= (((Re z) (#) (Im seq)) . n) + (((Im z) (#) (Re seq)) . n) by SEQ_1:9 .= (((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq))) . n by SEQ_1:7 ; ::_thesis: verum end; hence Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_3:21 for seq1, seq2 being Complex_Sequence holds ( Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) & Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) ) proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) & Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Re_(seq1_(#)_seq2))_._n_=_(((Re_seq1)_(#)_(Re_seq2))_-_((Im_seq1)_(#)_(Im_seq2)))_._n let n be Element of NAT ; ::_thesis: (Re (seq1 (#) seq2)) . n = (((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2))) . n thus (Re (seq1 (#) seq2)) . n = Re ((seq1 (#) seq2) . n) by Def5 .= Re ((seq1 . n) * (seq2 . n)) by VALUED_1:5 .= Re ((((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n)))) + ((((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n)))) * )) by COMPLEX1:def_6 .= ((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n))) by COMPLEX1:12 .= (((Re seq1) . n) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n))) by Def5 .= (((Re seq1) . n) * ((Re seq2) . n)) - ((Im (seq1 . n)) * (Im (seq2 . n))) by Def5 .= (((Re seq1) . n) * ((Re seq2) . n)) - ((Im (seq1 . n)) * ((Im seq2) . n)) by Def6 .= (((Re seq1) . n) * ((Re seq2) . n)) - (((Im seq1) . n) * ((Im seq2) . n)) by Def6 .= (((Re seq1) (#) (Re seq2)) . n) - (((Im seq1) . n) * ((Im seq2) . n)) by SEQ_1:8 .= (((Re seq1) (#) (Re seq2)) . n) - (((Im seq1) (#) (Im seq2)) . n) by SEQ_1:8 .= (((Re seq1) (#) (Re seq2)) . n) + (- (((Im seq1) (#) (Im seq2)) . n)) .= (((Re seq1) (#) (Re seq2)) . n) + ((- ((Im seq1) (#) (Im seq2))) . n) by SEQ_1:10 .= (((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2))) . n by SEQ_1:7 ; ::_thesis: verum end; hence Re (seq1 (#) seq2) = ((Re seq1) (#) (Re seq2)) - ((Im seq1) (#) (Im seq2)) by FUNCT_2:63; ::_thesis: Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Im_(seq1_(#)_seq2))_._n_=_(((Re_seq1)_(#)_(Im_seq2))_+_((Im_seq1)_(#)_(Re_seq2)))_._n let n be Element of NAT ; ::_thesis: (Im (seq1 (#) seq2)) . n = (((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2))) . n thus (Im (seq1 (#) seq2)) . n = Im ((seq1 (#) seq2) . n) by Def6 .= Im ((seq1 . n) * (seq2 . n)) by VALUED_1:5 .= Im ((((Re (seq1 . n)) * (Re (seq2 . n))) - ((Im (seq1 . n)) * (Im (seq2 . n)))) + ((((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n)))) * )) by COMPLEX1:def_6 .= ((Re (seq1 . n)) * (Im (seq2 . n))) + ((Re (seq2 . n)) * (Im (seq1 . n))) by COMPLEX1:12 .= ((Re (seq1 . n)) * (Im (seq2 . n))) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def5 .= (((Re seq1) . n) * (Im (seq2 . n))) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def5 .= (((Re seq1) . n) * ((Im seq2) . n)) + ((Im (seq1 . n)) * ((Re seq2) . n)) by Def6 .= (((Re seq1) . n) * ((Im seq2) . n)) + (((Im seq1) . n) * ((Re seq2) . n)) by Def6 .= (((Re seq1) (#) (Im seq2)) . n) + (((Im seq1) . n) * ((Re seq2) . n)) by SEQ_1:8 .= (((Re seq1) (#) (Im seq2)) . n) + (((Im seq1) (#) (Re seq2)) . n) by SEQ_1:8 .= (((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2))) . n by SEQ_1:7 ; ::_thesis: verum end; hence Im (seq1 (#) seq2) = ((Re seq1) (#) (Im seq2)) + ((Im seq1) (#) (Re seq2)) by FUNCT_2:63; ::_thesis: verum end; definition let Nseq be increasing sequence of NAT; let seq be Complex_Sequence; :: original: (#) redefine funcseq * Nseq -> Complex_Sequence; coherence Nseq (#) seq is Complex_Sequence proof dom (seq * Nseq) = NAT by FUNCT_2:def_1; hence Nseq (#) seq is Complex_Sequence ; ::_thesis: verum end; end; theorem Th22: :: COMSEQ_3:22 for seq being Complex_Sequence for Nseq being increasing sequence of NAT holds ( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq ) proof let seq be Complex_Sequence; ::_thesis: for Nseq being increasing sequence of NAT holds ( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq ) let Nseq be increasing sequence of NAT; ::_thesis: ( Re (seq * Nseq) = (Re seq) * Nseq & Im (seq * Nseq) = (Im seq) * Nseq ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Re_(seq_*_Nseq))_._n_=_((Re_seq)_*_Nseq)_._n let n be Element of NAT ; ::_thesis: (Re (seq * Nseq)) . n = ((Re seq) * Nseq) . n thus (Re (seq * Nseq)) . n = Re ((seq * Nseq) . n) by Def5 .= Re (seq . (Nseq . n)) by FUNCT_2:15 .= (Re seq) . (Nseq . n) by Def5 .= ((Re seq) * Nseq) . n by FUNCT_2:15 ; ::_thesis: verum end; hence Re (seq * Nseq) = (Re seq) * Nseq by FUNCT_2:63; ::_thesis: Im (seq * Nseq) = (Im seq) * Nseq now__::_thesis:_for_n_being_Element_of_NAT_holds_(Im_(seq_*_Nseq))_._n_=_((Im_seq)_*_Nseq)_._n let n be Element of NAT ; ::_thesis: (Im (seq * Nseq)) . n = ((Im seq) * Nseq) . n thus (Im (seq * Nseq)) . n = Im ((seq * Nseq) . n) by Def6 .= Im (seq . (Nseq . n)) by FUNCT_2:15 .= (Im seq) . (Nseq . n) by Def6 .= ((Im seq) * Nseq) . n by FUNCT_2:15 ; ::_thesis: verum end; hence Im (seq * Nseq) = (Im seq) * Nseq by FUNCT_2:63; ::_thesis: verum end; theorem Th23: :: COMSEQ_3:23 for seq being Complex_Sequence for k being Element of NAT holds ( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) ) proof let seq be Complex_Sequence; ::_thesis: for k being Element of NAT holds ( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) ) let k be Element of NAT ; ::_thesis: ( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_((Re_seq)_^\_k)_._n_=_(Re_(seq_^\_k))_._n_&_((Im_seq)_^\_k)_._n_=_(Im_(seq_^\_k))_._n_) let n be Element of NAT ; ::_thesis: ( ((Re seq) ^\ k) . n = (Re (seq ^\ k)) . n & ((Im seq) ^\ k) . n = (Im (seq ^\ k)) . n ) thus ((Re seq) ^\ k) . n = (Re seq) . (n + k) by NAT_1:def_3 .= Re (seq . (n + k)) by Def5 .= Re ((seq ^\ k) . n) by NAT_1:def_3 .= (Re (seq ^\ k)) . n by Def5 ; ::_thesis: ((Im seq) ^\ k) . n = (Im (seq ^\ k)) . n thus ((Im seq) ^\ k) . n = (Im seq) . (n + k) by NAT_1:def_3 .= Im (seq . (n + k)) by Def6 .= Im ((seq ^\ k) . n) by NAT_1:def_3 .= (Im (seq ^\ k)) . n by Def6 ; ::_thesis: verum end; hence ( (Re seq) ^\ k = Re (seq ^\ k) & (Im seq) ^\ k = Im (seq ^\ k) ) by FUNCT_2:63; ::_thesis: verum end; definition let s be Complex_Sequence; :: original: Partial_Sums redefine func Partial_Sums s -> Complex_Sequence; coherence Partial_Sums s is Complex_Sequence proof A1: dom (Partial_Sums s) = NAT by PARTFUN1:def_2; rng (Partial_Sums s) c= COMPLEX by VALUED_0:def_1; then Partial_Sums s is PartFunc of NAT,COMPLEX by A1, RELSET_1:4; hence Partial_Sums s is Complex_Sequence ; ::_thesis: verum end; end; definition let seq be Complex_Sequence; func Sum seq -> Element of COMPLEX equals :: COMSEQ_3:def 7 lim (Partial_Sums seq); coherence lim (Partial_Sums seq) is Element of COMPLEX ; end; :: deftheorem defines Sum COMSEQ_3:def_7_:_ for seq being Complex_Sequence holds Sum seq = lim (Partial_Sums seq); theorem Th24: :: COMSEQ_3:24 for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds for m being Element of NAT holds (Partial_Sums seq) . m = 0c proof let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies for m being Element of NAT holds (Partial_Sums seq) . m = 0c ) defpred S1[ Element of NAT ] means seq . \$1 = (Partial_Sums seq) . \$1; assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: for m being Element of NAT holds (Partial_Sums seq) . m = 0c A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1] thus seq . (k + 1) = 0c + (seq . (k + 1)) .= ((Partial_Sums seq) . k) + (seq . (k + 1)) by A1, A3 .= (Partial_Sums seq) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum end; let m be Element of NAT ; ::_thesis: (Partial_Sums seq) . m = 0c A4: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); then seq = Partial_Sums seq by FUNCT_2:63; hence (Partial_Sums seq) . m = 0c by A1; ::_thesis: verum end; theorem Th25: :: COMSEQ_3:25 for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds for m being Element of NAT holds (Partial_Sums |.seq.|) . m = 0 proof let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies for m being Element of NAT holds (Partial_Sums |.seq.|) . m = 0 ) defpred S1[ Element of NAT ] means |.seq.| . \$1 = (Partial_Sums |.seq.|) . \$1; assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: for m being Element of NAT holds (Partial_Sums |.seq.|) . m = 0 A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1] thus |.seq.| . (k + 1) = |.0c.| + (|.seq.| . (k + 1)) by COMPLEX1:44 .= |.(seq . k).| + (|.seq.| . (k + 1)) by A1 .= ((Partial_Sums |.seq.|) . k) + (|.seq.| . (k + 1)) by A3, VALUED_1:18 .= (Partial_Sums |.seq.|) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum end; let m be Element of NAT ; ::_thesis: (Partial_Sums |.seq.|) . m = 0 A4: S1[ 0 ] by SERIES_1:def_1; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (Partial_Sums |.seq.|) . m = |.seq.| . m .= |.(seq . m).| by VALUED_1:18 .= 0 by A1, COMPLEX1:44 ; ::_thesis: verum end; theorem Th26: :: COMSEQ_3:26 for seq being Complex_Sequence holds ( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) ) proof let seq be Complex_Sequence; ::_thesis: ( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) ) defpred S1[ Element of NAT ] means (Partial_Sums (Re seq)) . \$1 = (Re (Partial_Sums seq)) . \$1; defpred S2[ Element of NAT ] means (Partial_Sums (Im seq)) . \$1 = (Im (Partial_Sums seq)) . \$1; A1: 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] ; ::_thesis: S1[k + 1] then (Partial_Sums (Re seq)) . (k + 1) = ((Re (Partial_Sums seq)) . k) + ((Re seq) . (k + 1)) by SERIES_1:def_1 .= ((Re (Partial_Sums seq)) . k) + (Re (seq . (k + 1))) by Def5 .= (Re ((Partial_Sums seq) . k)) + (Re (seq . (k + 1))) by Def5 .= Re (((Partial_Sums seq) . k) + (seq . (k + 1))) by COMPLEX1:8 .= Re ((Partial_Sums seq) . (k + 1)) by SERIES_1:def_1 .= (Re (Partial_Sums seq)) . (k + 1) by Def5 ; hence S1[k + 1] ; ::_thesis: verum end; A2: for k being Element of NAT st S2[k] holds S2[k + 1] proof let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume S2[k] ; ::_thesis: S2[k + 1] then (Partial_Sums (Im seq)) . (k + 1) = ((Im (Partial_Sums seq)) . k) + ((Im seq) . (k + 1)) by SERIES_1:def_1 .= ((Im (Partial_Sums seq)) . k) + (Im (seq . (k + 1))) by Def6 .= (Im ((Partial_Sums seq) . k)) + (Im (seq . (k + 1))) by Def6 .= Im (((Partial_Sums seq) . k) + (seq . (k + 1))) by COMPLEX1:8 .= Im ((Partial_Sums seq) . (k + 1)) by SERIES_1:def_1 .= (Im (Partial_Sums seq)) . (k + 1) by Def6 ; hence S2[k + 1] ; ::_thesis: verum end; (Partial_Sums (Im seq)) . 0 = (Im seq) . 0 by SERIES_1:def_1 .= Im (seq . 0) by Def6 .= Im ((Partial_Sums seq) . 0) by SERIES_1:def_1 .= (Im (Partial_Sums seq)) . 0 by Def6 ; then A3: S2[ 0 ] ; A4: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A3, A2); (Partial_Sums (Re seq)) . 0 = (Re seq) . 0 by SERIES_1:def_1 .= Re (seq . 0) by Def5 .= Re ((Partial_Sums seq) . 0) by SERIES_1:def_1 .= (Re (Partial_Sums seq)) . 0 by Def5 ; then A5: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A5, A1); hence ( Partial_Sums (Re seq) = Re (Partial_Sums seq) & Partial_Sums (Im seq) = Im (Partial_Sums seq) ) by A4, FUNCT_2:63; ::_thesis: verum end; theorem Th27: :: COMSEQ_3:27 for seq1, seq2 being Complex_Sequence holds (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by SERIES_1:5; theorem Th28: :: COMSEQ_3:28 for seq1, seq2 being Complex_Sequence holds (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) proof let seq1, seq2 be Complex_Sequence; ::_thesis: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) A1: Im ((Partial_Sums seq1) - (Partial_Sums seq2)) = (Im (Partial_Sums seq1)) - (Im (Partial_Sums seq2)) by Th18 .= (Partial_Sums (Im seq1)) - (Im (Partial_Sums seq2)) by Th26 .= (Partial_Sums (Im seq1)) - (Partial_Sums (Im seq2)) by Th26 .= Partial_Sums ((Im seq1) - (Im seq2)) by SERIES_1:6 .= Partial_Sums (Im (seq1 - seq2)) by Th18 .= Im (Partial_Sums (seq1 - seq2)) by Th26 ; Re ((Partial_Sums seq1) - (Partial_Sums seq2)) = (Re (Partial_Sums seq1)) - (Re (Partial_Sums seq2)) by Th18 .= (Partial_Sums (Re seq1)) - (Re (Partial_Sums seq2)) by Th26 .= (Partial_Sums (Re seq1)) - (Partial_Sums (Re seq2)) by Th26 .= Partial_Sums ((Re seq1) - (Re seq2)) by SERIES_1:6 .= Partial_Sums (Re (seq1 - seq2)) by Th18 .= Re (Partial_Sums (seq1 - seq2)) by Th26 ; hence (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by A1, Th14; ::_thesis: verum end; theorem Th29: :: COMSEQ_3:29 for seq being Complex_Sequence for z being complex number holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) proof let seq be Complex_Sequence; ::_thesis: for z being complex number holds Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) let z be complex number ; ::_thesis: Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) defpred S1[ Element of NAT ] means (Partial_Sums (z (#) seq)) . \$1 = (z (#) (Partial_Sums seq)) . \$1; A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] (Partial_Sums (z (#) seq)) . (n + 1) = ((Partial_Sums (z (#) seq)) . n) + ((z (#) seq) . (n + 1)) by SERIES_1:def_1 .= (z * ((Partial_Sums seq) . n)) + ((z (#) seq) . (n + 1)) by A2, VALUED_1:6 .= (z * ((Partial_Sums seq) . n)) + (z * (seq . (n + 1))) by VALUED_1:6 .= z * (((Partial_Sums seq) . n) + (seq . (n + 1))) .= z * ((Partial_Sums seq) . (n + 1)) by SERIES_1:def_1 .= (z (#) (Partial_Sums seq)) . (n + 1) by VALUED_1:6 ; hence S1[n + 1] ; ::_thesis: verum end; (Partial_Sums (z (#) seq)) . 0 = (z (#) seq) . 0 by SERIES_1:def_1 .= z * (seq . 0) by VALUED_1:6 .= z * ((Partial_Sums seq) . 0) by SERIES_1:def_1 .= (z (#) (Partial_Sums seq)) . 0 by VALUED_1:6 ; then A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_3:30 for seq being Complex_Sequence for k being Element of NAT holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k proof let seq be Complex_Sequence; ::_thesis: for k being Element of NAT holds |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k let k be Element of NAT ; ::_thesis: |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k defpred S1[ Element of NAT ] means |.((Partial_Sums seq) . \$1).| <= (Partial_Sums |.seq.|) . \$1; A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then A2: |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).| by XREAL_1:6; ( |.((Partial_Sums seq) . (k + 1)).| = |.(((Partial_Sums seq) . k) + (seq . (k + 1))).| & |.(((Partial_Sums seq) . k) + (seq . (k + 1))).| <= |.((Partial_Sums seq) . k).| + |.(seq . (k + 1)).| ) by COMPLEX1:56, SERIES_1:def_1; then |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + |.(seq . (k + 1)).| by A2, XXREAL_0:2; then |.((Partial_Sums seq) . (k + 1)).| <= ((Partial_Sums |.seq.|) . k) + (|.seq.| . (k + 1)) by VALUED_1:18; hence S1[k + 1] by SERIES_1:def_1; ::_thesis: verum end; (Partial_Sums |.seq.|) . 0 = |.seq.| . 0 by SERIES_1:def_1 .= |.(seq . 0).| by VALUED_1:18 ; then A3: S1[ 0 ] by SERIES_1:def_1; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A1); hence |.((Partial_Sums seq) . k).| <= (Partial_Sums |.seq.|) . k ; ::_thesis: verum end; theorem Th31: :: COMSEQ_3:31 for seq being Complex_Sequence for m, n being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) proof let seq be Complex_Sequence; ::_thesis: for m, n being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) let m, n be Element of NAT ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) A1: for n, k being Element of NAT holds 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) proof let n be Element of NAT ; ::_thesis: for k being Element of NAT holds 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) defpred S1[ Element of NAT ] means 0 <= ((Partial_Sums |.seq.|) . (n + \$1)) - ((Partial_Sums |.seq.|) . n); A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A3: ((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n) = (((Partial_Sums |.seq.|) . (n + k)) + (|.seq.| . ((n + k) + 1))) - ((Partial_Sums |.seq.|) . n) by SERIES_1:def_1 .= (((Partial_Sums |.seq.|) . (n + k)) + |.(seq . ((n + k) + 1)).|) - ((Partial_Sums |.seq.|) . n) by VALUED_1:18 .= (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).| ; A4: 0 <= |.(seq . ((n + k) + 1)).| by COMPLEX1:46; assume S1[k] ; ::_thesis: S1[k + 1] hence S1[k + 1] by A3, A4; ::_thesis: verum end; A5: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2); ::_thesis: verum end; A6: for n, k being Element of NAT holds abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) proof let n, k be Element of NAT ; ::_thesis: abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) by A1; hence abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) by ABSVALUE:def_1; ::_thesis: verum end; A7: for n, m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) proof let n, m be Element of NAT ; ::_thesis: ( n <= m implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ) assume n <= m ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) then consider k being Nat such that A8: m = n + k by NAT_1:10; A9: for k being Element of NAT holds |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) proof defpred S1[ Element of NAT ] means |.(((Partial_Sums seq) . (n + \$1)) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . (n + \$1)) - ((Partial_Sums |.seq.|) . n)); A10: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] then A11: ( |.((((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).| <= |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).| & |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).| <= (abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n))) + |.(seq . ((n + k) + 1)).| ) by COMPLEX1:56, XREAL_1:6; A12: |.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).| = |.((((Partial_Sums seq) . (n + k)) + (seq . ((n + k) + 1))) - ((Partial_Sums seq) . n)).| by SERIES_1:def_1 .= |.((((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).| ; (abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n))) + |.(seq . ((n + k) + 1)).| = (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).| by A6 .= (((Partial_Sums |.seq.|) . (n + k)) + |.(seq . ((n + k) + 1)).|) - ((Partial_Sums |.seq.|) . n) .= (((Partial_Sums |.seq.|) . (n + k)) + (|.seq.| . ((n + k) + 1))) - ((Partial_Sums |.seq.|) . n) by VALUED_1:18 .= ((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n) by SERIES_1:def_1 .= abs (((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n)) by A6 ; hence S1[k + 1] by A12, A11, XXREAL_0:2; ::_thesis: verum end; A13: S1[ 0 ] ; thus for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A10); ::_thesis: verum end; k in NAT by ORDINAL1:def_12; hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A9, A8; ::_thesis: verum end; for n, m being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) proof let n, m be Element of NAT ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ( m <= n implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ) proof assume m <= n ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) then A14: |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= abs (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m)) by A7; abs (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m)) = abs (- (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m))) by COMPLEX1:52 .= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ; hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A14, COMPLEX1:60; ::_thesis: verum end; hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A7; ::_thesis: verum end; hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ; ::_thesis: verum end; theorem Th32: :: COMSEQ_3:32 for seq being Complex_Sequence for k being Element of NAT holds ( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) ) proof let seq be Complex_Sequence; ::_thesis: for k being Element of NAT holds ( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) ) let k be Element of NAT ; ::_thesis: ( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_((Partial_Sums_(Re_seq))_^\_k)_._n_=_(Re_((Partial_Sums_seq)_^\_k))_._n_&_((Partial_Sums_(Im_seq))_^\_k)_._n_=_(Im_((Partial_Sums_seq)_^\_k))_._n_) let n be Element of NAT ; ::_thesis: ( ((Partial_Sums (Re seq)) ^\ k) . n = (Re ((Partial_Sums seq) ^\ k)) . n & ((Partial_Sums (Im seq)) ^\ k) . n = (Im ((Partial_Sums seq) ^\ k)) . n ) thus ((Partial_Sums (Re seq)) ^\ k) . n = (Partial_Sums (Re seq)) . (n + k) by NAT_1:def_3 .= (Re (Partial_Sums seq)) . (n + k) by Th26 .= Re ((Partial_Sums seq) . (n + k)) by Def5 .= Re (((Partial_Sums seq) ^\ k) . n) by NAT_1:def_3 .= (Re ((Partial_Sums seq) ^\ k)) . n by Def5 ; ::_thesis: ((Partial_Sums (Im seq)) ^\ k) . n = (Im ((Partial_Sums seq) ^\ k)) . n thus ((Partial_Sums (Im seq)) ^\ k) . n = (Partial_Sums (Im seq)) . (n + k) by NAT_1:def_3 .= (Im (Partial_Sums seq)) . (n + k) by Th26 .= Im ((Partial_Sums seq) . (n + k)) by Def6 .= Im (((Partial_Sums seq) ^\ k) . n) by NAT_1:def_3 .= (Im ((Partial_Sums seq) ^\ k)) . n by Def6 ; ::_thesis: verum end; hence ( (Partial_Sums (Re seq)) ^\ k = Re ((Partial_Sums seq) ^\ k) & (Partial_Sums (Im seq)) ^\ k = Im ((Partial_Sums seq) ^\ k) ) by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_3:33 for seq1, seq being Complex_Sequence st ( for n being Element of NAT holds seq1 . n = seq . 0 ) holds Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 proof let seq1, seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq1 . n = seq . 0 ) implies Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 ) assume A1: for n being Element of NAT holds seq1 . n = seq . 0 ; ::_thesis: Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(Re_seq1)_._n_=_(Re_seq)_._0_&_(Im_seq1)_._n_=_(Im_seq)_._0_) let n be Element of NAT ; ::_thesis: ( (Re seq1) . n = (Re seq) . 0 & (Im seq1) . n = (Im seq) . 0 ) thus (Re seq1) . n = Re (seq1 . n) by Def5 .= Re (seq . 0) by A1 .= (Re seq) . 0 by Def5 ; ::_thesis: (Im seq1) . n = (Im seq) . 0 thus (Im seq1) . n = Im (seq1 . n) by Def6 .= Im (seq . 0) by A1 .= (Im seq) . 0 by Def6 ; ::_thesis: verum end; A3: Im (Partial_Sums (seq ^\ 1)) = Partial_Sums (Im (seq ^\ 1)) by Th26 .= Partial_Sums ((Im seq) ^\ 1) by Th23 .= ((Partial_Sums (Im seq)) ^\ 1) - (Im seq1) by A2, SERIES_1:11 .= (Im ((Partial_Sums seq) ^\ 1)) - (Im seq1) by Th32 .= Im (((Partial_Sums seq) ^\ 1) - seq1) by Th18 ; Re (Partial_Sums (seq ^\ 1)) = Partial_Sums (Re (seq ^\ 1)) by Th26 .= Partial_Sums ((Re seq) ^\ 1) by Th23 .= ((Partial_Sums (Re seq)) ^\ 1) - (Re seq1) by A2, SERIES_1:11 .= (Re ((Partial_Sums seq) ^\ 1)) - (Re seq1) by Th32 .= Re (((Partial_Sums seq) ^\ 1) - seq1) by Th18 ; hence Partial_Sums (seq ^\ 1) = ((Partial_Sums seq) ^\ 1) - seq1 by A3, Th14; ::_thesis: verum end; theorem Th34: :: COMSEQ_3:34 for seq being Complex_Sequence holds Partial_Sums |.seq.| is non-decreasing proof let seq be Complex_Sequence; ::_thesis: Partial_Sums |.seq.| is non-decreasing for n being Element of NAT holds 0 <= |.seq.| . n by Lm3; hence Partial_Sums |.seq.| is non-decreasing by SERIES_1:16; ::_thesis: verum end; registration let seq be Complex_Sequence; cluster Partial_Sums |.seq.| -> non-decreasing for Real_Sequence; coherence for b1 being Real_Sequence st b1 = Partial_Sums |.seq.| holds b1 is non-decreasing by Th34; end; theorem :: COMSEQ_3:35 for seq1, seq2 being Complex_Sequence for m being Element of NAT st ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) holds (Partial_Sums seq1) . m = (Partial_Sums seq2) . m proof let seq1, seq2 be Complex_Sequence; ::_thesis: for m being Element of NAT st ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) holds (Partial_Sums seq1) . m = (Partial_Sums seq2) . m let m be Element of NAT ; ::_thesis: ( ( for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ) implies (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ) defpred S1[ Element of NAT ] means ( \$1 <= m implies (Partial_Sums seq1) . \$1 = (Partial_Sums seq2) . \$1 ); assume A1: for n being Element of NAT st n <= m holds seq1 . n = seq2 . n ; ::_thesis: (Partial_Sums seq1) . m = (Partial_Sums seq2) . m A2: 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 A3: S1[k] ; ::_thesis: S1[k + 1] assume A4: k + 1 <= m ; ::_thesis: (Partial_Sums seq1) . (k + 1) = (Partial_Sums seq2) . (k + 1) k < k + 1 by XREAL_1:29; hence (Partial_Sums seq1) . (k + 1) = ((Partial_Sums seq2) . k) + (seq1 . (k + 1)) by A3, A4, SERIES_1:def_1, XXREAL_0:2 .= ((Partial_Sums seq2) . k) + (seq2 . (k + 1)) by A1, A4 .= (Partial_Sums seq2) . (k + 1) by SERIES_1:def_1 ; ::_thesis: verum end; A5: S1[ 0 ] proof assume 0 <= m ; ::_thesis: (Partial_Sums seq1) . 0 = (Partial_Sums seq2) . 0 thus (Partial_Sums seq1) . 0 = seq1 . 0 by SERIES_1:def_1 .= seq2 . 0 by A1 .= (Partial_Sums seq2) . 0 by SERIES_1:def_1 ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A2); hence (Partial_Sums seq1) . m = (Partial_Sums seq2) . m ; ::_thesis: verum end; theorem Th36: :: COMSEQ_3:36 for z being Element of COMPLEX st 1r <> z holds for n being Element of NAT holds (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z) proof let z be Element of COMPLEX ; ::_thesis: ( 1r <> z implies for n being Element of NAT holds (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z) ) now__::_thesis:_for_z_being_Element_of_COMPLEX_st_1r_<>_z_holds_ for_n_being_Element_of_NAT_holds_S1[n] let z be Element of COMPLEX ; ::_thesis: ( 1r <> z implies for n being Element of NAT holds S1[n] ) defpred S1[ Element of NAT ] means (Partial_Sums (z GeoSeq)) . \$1 = (1r - (z #N (\$1 + 1))) / (1r - z); assume 1r <> z ; ::_thesis: for n being Element of NAT holds S1[n] then A1: 1r - z <> 0c ; A2: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] hence (Partial_Sums (z GeoSeq)) . (n + 1) = ((1r - (z #N (n + 1))) / (1r - z)) + ((z #N (n + 1)) * 1r) by COMPLEX1:def_4, SERIES_1:def_1 .= ((1r - (z #N (n + 1))) / (1r - z)) + ((z #N (n + 1)) * ((1r - z) / (1r - z))) by A1, COMPLEX1:def_4, XCMPLX_1:60 .= ((1r - (z #N (n + 1))) / (1r - z)) + (((z #N (n + 1)) * (1r - z)) / (1r - z)) by XCMPLX_1:74 .= ((1r - (z #N (n + 1))) + ((z #N (n + 1)) - ((z #N (n + 1)) * z))) / (1r - z) by COMPLEX1:def_4, XCMPLX_1:62 .= (1r - ((z #N (n + 1)) * z)) / (1r - z) .= (1r - (z #N ((n + 1) + 1))) / (1r - z) by NEWTON:6 ; ::_thesis: verum end; (Partial_Sums (z GeoSeq)) . 0 = (z GeoSeq) . 0 by SERIES_1:def_1 .= 1r by Def1 .= (1r - (1 * z)) / (1r - z) by A1, COMPLEX1:def_4, XCMPLX_1:60 .= (1r - (z #N (0 + 1))) / (1r - z) by NEWTON:5 ; then A3: S1[ 0 ] ; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); ::_thesis: verum end; hence ( 1r <> z implies for n being Element of NAT holds (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z) ) ; ::_thesis: verum end; theorem Th37: :: COMSEQ_3:37 for seq being Complex_Sequence for z being Element of COMPLEX st z <> 1r & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) proof let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX st z <> 1r & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) let z be Element of COMPLEX ; ::_thesis: ( z <> 1r & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) implies for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) ) assume that A1: z <> 1r and A2: for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ; ::_thesis: for n being Element of NAT holds (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) defpred S1[ Element of NAT ] means seq . \$1 = (seq . 0) * ((z GeoSeq) . \$1); A3: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then seq . (n + 1) = z * ((seq . 0) * ((z GeoSeq) . n)) by A2 .= (seq . 0) * (z * ((z GeoSeq) . n)) .= (seq . 0) * ((z GeoSeq) . (n + 1)) by Def1 ; hence S1[n + 1] ; ::_thesis: verum end; let n be Element of NAT ; ::_thesis: (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) seq . 0 = (seq . 0) * 1r by COMPLEX1:def_4 .= (seq . 0) * ((z GeoSeq) . 0) by Def1 ; then A4: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A3); then Partial_Sums seq = Partial_Sums ((seq . 0) (#) (z GeoSeq)) by VALUED_1:7 .= (seq . 0) (#) (Partial_Sums (z GeoSeq)) by Th29 ; hence (Partial_Sums seq) . n = (seq . 0) * ((Partial_Sums (z GeoSeq)) . n) by VALUED_1:6 .= (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) by A1, Th36 ; ::_thesis: verum end; begin theorem Th38: :: COMSEQ_3:38 for a, b being Real_Sequence for c being Complex_Sequence st ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds ( ( a is convergent & b is convergent ) iff c is convergent ) proof let a, b be Real_Sequence; ::_thesis: for c being Complex_Sequence st ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds ( ( a is convergent & b is convergent ) iff c is convergent ) let c be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) implies ( ( a is convergent & b is convergent ) iff c is convergent ) ) assume A1: for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ; ::_thesis: ( ( a is convergent & b is convergent ) iff c is convergent ) thus ( a is convergent & b is convergent implies c is convergent ) ::_thesis: ( c is convergent implies ( a is convergent & b is convergent ) ) proof assume that A2: a is convergent and A3: b is convergent ; ::_thesis: c is convergent consider a1 being real number such that A4: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((a . m) - a1) < p by A2, SEQ_2:def_6; consider b1 being real number such that A5: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((b . m) - b1) < p by A3, SEQ_2:def_6; reconsider a1 = a1, b1 = b1 as Real by XREAL_0:def_1; reconsider g = a1 + (b1 * ) as Element of COMPLEX by XCMPLX_0:def_2; take g ; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= |.((c . b3) - g).| ) ) for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((c . m) - g).| < p proof let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((c . m) - g).| < p ) assume A6: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((c . m) - g).| < p then consider n1 being Element of NAT such that A7: for m being Element of NAT st n1 <= m holds abs ((a . m) - a1) < p / 2 by A4; consider n2 being Element of NAT such that A8: for m being Element of NAT st n2 <= m holds abs ((b . m) - b1) < p / 2 by A5, A6; ( n1 <= n1 + n2 & n2 <= n1 + n2 ) by NAT_1:11; then consider n being Element of NAT such that A9: n1 <= n and A10: n2 <= n ; take n ; ::_thesis: for m being Element of NAT st n <= m holds |.((c . m) - g).| < p for m being Element of NAT st n <= m holds |.((c . m) - g).| < p proof let m be Element of NAT ; ::_thesis: ( n <= m implies |.((c . m) - g).| < p ) ( Re (c . m) = a . m & Re g = a1 ) by A1, COMPLEX1:12; then A11: Re ((c . m) - g) = (a . m) - a1 by COMPLEX1:19; ( Im (c . m) = b . m & Im g = b1 ) by A1, COMPLEX1:12; then A12: Im ((c . m) - g) = (b . m) - b1 by COMPLEX1:19; assume A13: n <= m ; ::_thesis: |.((c . m) - g).| < p then n2 <= m by A10, XXREAL_0:2; then A14: abs ((b . m) - b1) < p / 2 by A8; n1 <= m by A9, A13, XXREAL_0:2; then abs ((a . m) - a1) < p / 2 by A7; then A15: (abs ((a . m) - a1)) + (abs ((b . m) - b1)) < (p / 2) + (p / 2) by A14, XREAL_1:8; |.((c . m) - g).| <= (abs (Re ((c . m) - g))) + (abs (Im ((c . m) - g))) by Th12; hence |.((c . m) - g).| < p by A15, A11, A12, XXREAL_0:2; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds |.((c . m) - g).| < p ; ::_thesis: verum end; hence for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= |.((c . b3) - g).| ) ) ; ::_thesis: verum end; assume c is convergent ; ::_thesis: ( a is convergent & b is convergent ) then consider z being Element of COMPLEX such that A16: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((c . m) - z).| < p by COMSEQ_2:def_5; thus a is convergent ::_thesis: b is convergent proof reconsider z = z as Element of COMPLEX ; take Re z ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= abs ((a . b3) - (Re z)) ) ) let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs ((a . b2) - (Re z)) ) ) assume A17: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs ((a . b2) - (Re z)) ) p is Real by XREAL_0:def_1; then consider n being Element of NAT such that A18: for m being Element of NAT st n <= m holds |.((c . m) - z).| < p by A16, A17; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= abs ((a . b1) - (Re z)) ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs ((a . m) - (Re z)) ) assume n <= m ; ::_thesis: not p <= abs ((a . m) - (Re z)) then A19: |.((c . m) - z).| < p by A18; ( Re (c . m) = a . m & Re ((c . m) - z) = (Re (c . m)) - (Re z) ) by A1, COMPLEX1:19; then abs ((a . m) - (Re z)) <= |.((c . m) - z).| by Th13; hence not p <= abs ((a . m) - (Re z)) by A19, XXREAL_0:2; ::_thesis: verum end; take Im z ; :: according to SEQ_2:def_6 ::_thesis: for b1 being set holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= abs ((b . b3) - (Im z)) ) ) let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs ((b . b2) - (Im z)) ) ) assume A20: p > 0 ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs ((b . b2) - (Im z)) ) p is Real by XREAL_0:def_1; then consider n being Element of NAT such that A21: for m being Element of NAT st n <= m holds |.((c . m) - z).| < p by A16, A20; take n ; ::_thesis: for b1 being Element of NAT holds ( not n <= b1 or not p <= abs ((b . b1) - (Im z)) ) let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= abs ((b . m) - (Im z)) ) assume n <= m ; ::_thesis: not p <= abs ((b . m) - (Im z)) then A22: |.((c . m) - z).| < p by A21; A23: Im ((c . m) - z) = (Im (c . m)) - (Im z) by COMPLEX1:19; Im (c . m) = b . m by A1; then abs ((b . m) - (Im z)) <= |.((c . m) - z).| by A23, Th13; hence not p <= abs ((b . m) - (Im z)) by A22, XXREAL_0:2; ::_thesis: verum end; theorem Th39: :: COMSEQ_3:39 for a, b being convergent Real_Sequence for c being Complex_Sequence st ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds ( c is convergent & lim c = (lim a) + ((lim b) * ) ) proof let a, b be convergent Real_Sequence; ::_thesis: for c being Complex_Sequence st ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds ( c is convergent & lim c = (lim a) + ((lim b) * ) ) let c be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) implies ( c is convergent & lim c = (lim a) + ((lim b) * ) ) ) reconsider g = (lim a) + ((lim b) * ) as Element of COMPLEX by XCMPLX_0:def_2; assume A1: for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ; ::_thesis: ( c is convergent & lim c = (lim a) + ((lim b) * ) ) hence A2: c is convergent by Th38; ::_thesis: lim c = (lim a) + ((lim b) * ) for p being Element of REAL st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((c . m) - g).| < p proof let p be Element of REAL ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((c . m) - g).| < p ) assume A3: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((c . m) - g).| < p then consider n1 being Element of NAT such that A4: for m being Element of NAT st n1 <= m holds abs ((a . m) - (lim a)) < p / 2 by SEQ_2:def_7; consider n2 being Element of NAT such that A5: for m being Element of NAT st n2 <= m holds abs ((b . m) - (lim b)) < p / 2 by A3, SEQ_2:def_7; ( n1 <= n1 + n2 & n2 <= n1 + n2 ) by NAT_1:11; then consider n being Element of NAT such that A6: n1 <= n and A7: n2 <= n ; take n ; ::_thesis: for m being Element of NAT st n <= m holds |.((c . m) - g).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((c . m) - g).| < p ) assume A8: n <= m ; ::_thesis: |.((c . m) - g).| < p then n2 <= m by A7, XXREAL_0:2; then A9: abs ((b . m) - (lim b)) < p / 2 by A5; n1 <= m by A6, A8, XXREAL_0:2; then abs ((a . m) - (lim a)) < p / 2 by A4; then A10: (abs ((a . m) - (lim a))) + (abs ((b . m) - (lim b))) < (p / 2) + (p / 2) by A9, XREAL_1:8; ( Re (c . m) = a . m & Re g = lim a ) by A1, COMPLEX1:12; then A11: Re ((c . m) - g) = (a . m) - (lim a) by COMPLEX1:19; ( Im (c . m) = b . m & Im g = lim b ) by A1, COMPLEX1:12; then A12: Im ((c . m) - g) = (b . m) - (lim b) by COMPLEX1:19; |.((c . m) - g).| <= (abs (Re ((c . m) - g))) + (abs (Im ((c . m) - g))) by Th12; hence |.((c . m) - g).| < p by A10, A11, A12, XXREAL_0:2; ::_thesis: verum end; hence lim c = (lim a) + ((lim b) * ) by A2, COMSEQ_2:def_6; ::_thesis: verum end; theorem Th40: :: COMSEQ_3:40 for a, b being Real_Sequence for c being convergent Complex_Sequence st ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) ) proof let a, b be Real_Sequence; ::_thesis: for c being convergent Complex_Sequence st ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) holds ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) ) let c be convergent Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ) implies ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) ) ) assume A1: for n being Element of NAT holds ( Re (c . n) = a . n & Im (c . n) = b . n ) ; ::_thesis: ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) ) A2: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((b . m) - (Im (lim c))) < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((b . m) - (Im (lim c))) < p ) assume A3: p > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((b . m) - (Im (lim c))) < p p is Real by XREAL_0:def_1; then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds |.((c . m) - (lim c)).| < p by A3, COMSEQ_2:def_6; take n ; ::_thesis: for m being Element of NAT st n <= m holds abs ((b . m) - (Im (lim c))) < p let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((b . m) - (Im (lim c))) < p ) assume n <= m ; ::_thesis: abs ((b . m) - (Im (lim c))) < p then A5: |.((c . m) - (lim c)).| < p by A4; ( Im (c . m) = b . m & Im ((c . m) - (lim c)) = (Im (c . m)) - (Im (lim c)) ) by A1, COMPLEX1:19; then abs ((b . m) - (Im (lim c))) <= |.((c . m) - (lim c)).| by Th13; hence abs ((b . m) - (Im (lim c))) < p by A5, XXREAL_0:2; ::_thesis: verum end; A6: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((a . m) - (Re (lim c))) < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((a . m) - (Re (lim c))) < p ) assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((a . m) - (Re (lim c))) < p p is Real by XREAL_0:def_1; then consider n being Element of NAT such that A8: for m being Element of NAT st n <= m holds |.((c . m) - (lim c)).| < p by A7, COMSEQ_2:def_6; take n ; ::_thesis: for m being Element of NAT st n <= m holds abs ((a . m) - (Re (lim c))) < p let m be Element of NAT ; ::_thesis: ( n <= m implies abs ((a . m) - (Re (lim c))) < p ) Re (c . m) = a . m by A1; then Re ((c . m) - (lim c)) = (a . m) - (Re (lim c)) by COMPLEX1:19; then A9: abs ((a . m) - (Re (lim c))) <= |.((c . m) - (lim c)).| by Th13; assume n <= m ; ::_thesis: abs ((a . m) - (Re (lim c))) < p then |.((c . m) - (lim c)).| < p by A8; hence abs ((a . m) - (Re (lim c))) < p by A9, XXREAL_0:2; ::_thesis: verum end; ( a is convergent & b is convergent ) by A1, Th38; hence ( a is convergent & b is convergent & lim a = Re (lim c) & lim b = Im (lim c) ) by A6, A2, SEQ_2:def_7; ::_thesis: verum end; theorem Th41: :: COMSEQ_3:41 for c being convergent Complex_Sequence holds ( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) ) proof let c be convergent Complex_Sequence; ::_thesis: ( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) ) ( ( for n being Element of NAT holds (Re c) . n = Re (c . n) ) & ( for n being Element of NAT holds (Im c) . n = Im (c . n) ) ) by Def5, Def6; hence ( Re c is convergent & Im c is convergent & lim (Re c) = Re (lim c) & lim (Im c) = Im (lim c) ) by Th40; ::_thesis: verum end; registration let c be convergent Complex_Sequence; cluster Re c -> convergent for Real_Sequence; coherence for b1 being Real_Sequence st b1 = Re c holds b1 is convergent by Th41; cluster Im c -> convergent for Real_Sequence; coherence for b1 being Real_Sequence st b1 = Im c holds b1 is convergent by Th41; end; theorem Th42: :: COMSEQ_3:42 for c being Complex_Sequence st Re c is convergent & Im c is convergent holds ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) ) proof let c be Complex_Sequence; ::_thesis: ( Re c is convergent & Im c is convergent implies ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) ) ) assume A1: ( Re c is convergent & Im c is convergent ) ; ::_thesis: ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) ) A2: ( ( for n being Element of NAT holds (Re c) . n = Re (c . n) ) & ( for n being Element of NAT holds (Im c) . n = Im (c . n) ) ) by Def5, Def6; then lim c = (lim (Re c)) + ((lim (Im c)) * ) by A1, Th39; hence ( c is convergent & Re (lim c) = lim (Re c) & Im (lim c) = lim (Im c) ) by A1, A2, Th39, COMPLEX1:12; ::_thesis: verum end; theorem Th43: :: COMSEQ_3:43 for seq being Complex_Sequence for z being Element of COMPLEX st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) holds ( seq is convergent & lim seq = 0c ) proof let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX st 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) holds ( seq is convergent & lim seq = 0c ) let z be Element of COMPLEX ; ::_thesis: ( 0 < |.z.| & |.z.| < 1 & seq . 0 = z & ( for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ) implies ( seq is convergent & lim seq = 0c ) ) assume that A1: 0 < |.z.| and A2: |.z.| < 1 ; ::_thesis: ( not seq . 0 = z or ex n being Element of NAT st not seq . (n + 1) = (seq . n) * z or ( seq is convergent & lim seq = 0c ) ) deffunc H1( Element of NAT ) -> Element of REAL = |.z.| to_power (\$1 + 1); consider rseq1 being Real_Sequence such that A3: for n being Element of NAT holds rseq1 . n = H1(n) from SEQ_1:sch_1(); assume that A4: seq . 0 = z and A5: for n being Element of NAT holds seq . (n + 1) = (seq . n) * z ; ::_thesis: ( seq is convergent & lim seq = 0c ) A6: for n being Element of NAT holds |.(seq . n).| = |.z.| to_power (n + 1) proof defpred S1[ Element of NAT ] means |.(seq . \$1).| = |.z.| to_power (\$1 + 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 A8: S1[k] ; ::_thesis: S1[k + 1] |.(seq . (k + 1)).| = |.((seq . k) * z).| by A5 .= (|.z.| to_power (k + 1)) * |.z.| by A8, COMPLEX1:65 .= (|.z.| to_power (k + 1)) * (|.z.| to_power 1) by POWER:25 .= |.z.| to_power ((k + 1) + 1) by A1, POWER:27 ; hence S1[k + 1] ; ::_thesis: verum end; A9: S1[ 0 ] by A4, POWER:25; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A7); hence for n being Element of NAT holds |.(seq . n).| = |.z.| to_power (n + 1) ; ::_thesis: verum end; A10: now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(Re_seq))_._n_<=_rseq1_._n let n be Element of NAT ; ::_thesis: (abs (Re seq)) . n <= rseq1 . n (abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:12; then A11: (abs (Re seq)) . n = abs (Re (seq . n)) by Def5; ( abs (Re (seq . n)) <= |.(seq . n).| & |.(seq . n).| = |.z.| to_power (n + 1) ) by A6, Th13; hence (abs (Re seq)) . n <= rseq1 . n by A3, A11; ::_thesis: verum end; A12: now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(Im_seq))_._n_<=_rseq1_._n let n be Element of NAT ; ::_thesis: (abs (Im seq)) . n <= rseq1 . n A13: |.(seq . n).| = |.z.| to_power (n + 1) by A6; ( (abs (Im seq)) . n = abs ((Im seq) . n) & abs (Im (seq . n)) <= |.(seq . n).| ) by Th13, SEQ_1:12; then (abs (Im seq)) . n <= |.z.| to_power (n + 1) by A13, Def6; hence (abs (Im seq)) . n <= rseq1 . n by A3; ::_thesis: verum end; C . 0 = 0 by FUNCOP_1:7; then A14: lim C = 0 by SEQ_4:25; A15: ( rseq1 is convergent & lim rseq1 = 0 ) by A1, A2, A3, SERIES_1:1; now__::_thesis:_for_n_being_Element_of_NAT_holds_C_._n_<=_(abs_(Re_seq))_._n let n be Element of NAT ; ::_thesis: C . n <= (abs (Re seq)) . n (abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:12; then 0 <= (abs (Re seq)) . n by COMPLEX1:46; hence C . n <= (abs (Re seq)) . n by FUNCOP_1:7; ::_thesis: verum end; then A16: ( abs (Re seq) is convergent & lim (abs (Re seq)) = 0 ) by A14, A15, A10, SEQ_2:19, SEQ_2:20; then A17: Re seq is convergent by SEQ_4:15; now__::_thesis:_for_n_being_Element_of_NAT_holds_C_._n_<=_(abs_(Im_seq))_._n let n be Element of NAT ; ::_thesis: C . n <= (abs (Im seq)) . n (abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:12; then 0 <= (abs (Im seq)) . n by COMPLEX1:46; hence C . n <= (abs (Im seq)) . n by FUNCOP_1:7; ::_thesis: verum end; then A18: ( abs (Im seq) is convergent & lim (abs (Im seq)) = 0 ) by A14, A15, A12, SEQ_2:19, SEQ_2:20; then A19: Im seq is convergent by SEQ_4:15; lim (Im seq) = 0 by A18, SEQ_4:15; then A20: Im (lim seq) = 0 by A17, A19, Th42; lim (Re seq) = 0 by A16, SEQ_4:15; then Re (lim seq) = 0 by A17, A19, Th42; hence ( seq is convergent & lim seq = 0c ) by A17, A19, A20, Lm1, Th42, COMPLEX1:13; ::_thesis: verum end; theorem Th44: :: COMSEQ_3:44 for seq being Complex_Sequence for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) holds ( seq is convergent & lim seq = 0c ) proof let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) holds ( seq is convergent & lim seq = 0c ) let z be Element of COMPLEX ; ::_thesis: ( |.z.| < 1 & ( for n being Element of NAT holds seq . n = z #N (n + 1) ) implies ( seq is convergent & lim seq = 0c ) ) assume that A1: |.z.| < 1 and A2: for n being Element of NAT holds seq . n = z #N (n + 1) ; ::_thesis: ( seq is convergent & lim seq = 0c ) A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._(n_+_1)_=_(seq_._n)_*_z let n be Element of NAT ; ::_thesis: seq . (n + 1) = (seq . n) * z thus seq . (n + 1) = z #N ((n + 1) + 1) by A2 .= (z #N (n + 1)) * z by NEWTON:6 .= (seq . n) * z by A2 ; ::_thesis: verum end; A4: now__::_thesis:_(_|.z.|_=_0_implies_(_seq_is_convergent_&_seq_is_convergent_&_lim_seq_=_0c_)_) assume |.z.| = 0 ; ::_thesis: ( seq is convergent & seq is convergent & lim seq = 0c ) then A5: z = 0c by COMPLEX1:45; A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_=_0c let n be Element of NAT ; ::_thesis: seq . n = 0c thus seq . n = 0c #N (n + 1) by A2, A5 .= ((0c GeoSeq) . n) * 0c by Def1 .= 0c ; ::_thesis: verum end; hence seq is convergent by COMSEQ_2:9; ::_thesis: ( seq is convergent & lim seq = 0c ) thus ( seq is convergent & lim seq = 0c ) by A6, COMSEQ_2:9, COMSEQ_2:10; ::_thesis: verum end; A7: seq . 0 = z #N (0 + 1) by A2 .= z by NEWTON:5 ; now__::_thesis:_(_|.z.|_<>_0_implies_(_seq_is_convergent_&_lim_seq_=_0c_)_) A8: 0 <= |.z.| by COMPLEX1:46; assume |.z.| <> 0 ; ::_thesis: ( seq is convergent & lim seq = 0c ) hence ( seq is convergent & lim seq = 0c ) by A1, A7, A3, A8, Th43; ::_thesis: verum end; hence ( seq is convergent & lim seq = 0c ) by A4; ::_thesis: verum end; theorem :: COMSEQ_3:45 for seq being Complex_Sequence for r being Real st r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds |.(seq . n).| >= r & |.seq.| is convergent holds lim |.seq.| <> 0 proof let seq be Complex_Sequence; ::_thesis: for r being Real st r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds |.(seq . n).| >= r & |.seq.| is convergent holds lim |.seq.| <> 0 let r be Real; ::_thesis: ( r > 0 & ex m being Element of NAT st for n being Element of NAT st n >= m holds |.(seq . n).| >= r & |.seq.| is convergent implies lim |.seq.| <> 0 ) assume that A1: r > 0 and A2: ex m being Element of NAT st for n being Element of NAT st n >= m holds |.(seq . n).| >= r ; ::_thesis: ( not |.seq.| is convergent or lim |.seq.| <> 0 ) consider m being Element of NAT such that A3: for n being Element of NAT st n >= m holds |.(seq . n).| >= r by A2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_m_holds_ abs_(|.seq.|_._n)_>=_r let n be Element of NAT ; ::_thesis: ( n >= m implies abs (|.seq.| . n) >= r ) assume A4: n >= m ; ::_thesis: abs (|.seq.| . n) >= r 0 <= |.seq.| . n by Lm3; then abs (|.seq.| . n) = |.seq.| . n by ABSVALUE:def_1 .= |.(seq . n).| by VALUED_1:18 ; hence abs (|.seq.| . n) >= r by A3, A4; ::_thesis: verum end; hence ( not |.seq.| is convergent or lim |.seq.| <> 0 ) by A1, SERIES_1:38; ::_thesis: verum end; theorem Th46: :: COMSEQ_3:46 for seq being Complex_Sequence holds ( seq is convergent iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p ) proof let seq be Complex_Sequence; ::_thesis: ( seq is convergent iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p ) A1: now__::_thesis:_(_(_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.((seq_._m)_-_(seq_._n)).|_<_p_)_implies_(_Re_seq_is_convergent_&_Im_seq_is_convergent_&_seq_is_convergent_)_) assume A2: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p ; ::_thesis: ( Re seq is convergent & Im seq is convergent & seq is convergent ) for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Re seq) . m) - ((Re seq) . n)) < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Re seq) . m) - ((Re seq) . n)) < p ) assume A3: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Re seq) . m) - ((Re seq) . n)) < p p is Real by XREAL_0:def_1; then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p by A2, A3; take n ; ::_thesis: for m being Element of NAT st n <= m holds abs (((Re seq) . m) - ((Re seq) . n)) < p let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Re seq) . m) - ((Re seq) . n)) < p ) assume n <= m ; ::_thesis: abs (((Re seq) . m) - ((Re seq) . n)) < p then A5: |.((seq . m) - (seq . n)).| < p by A4; Re ((seq . m) - (seq . n)) = (Re (seq . m)) - (Re (seq . n)) by COMPLEX1:19 .= ((Re seq) . m) - (Re (seq . n)) by Def5 .= ((Re seq) . m) - ((Re seq) . n) by Def5 ; then abs (((Re seq) . m) - ((Re seq) . n)) <= |.((seq . m) - (seq . n)).| by Th13; hence abs (((Re seq) . m) - ((Re seq) . n)) < p by A5, XXREAL_0:2; ::_thesis: verum end; hence A6: Re seq is convergent by SEQ_4:41; ::_thesis: ( Im seq is convergent & seq is convergent ) for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Im seq) . m) - ((Im seq) . n)) < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Im seq) . m) - ((Im seq) . n)) < p ) assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((Im seq) . m) - ((Im seq) . n)) < p p is Real by XREAL_0:def_1; then consider n being Element of NAT such that A8: for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p by A2, A7; take n ; ::_thesis: for m being Element of NAT st n <= m holds abs (((Im seq) . m) - ((Im seq) . n)) < p let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((Im seq) . m) - ((Im seq) . n)) < p ) assume n <= m ; ::_thesis: abs (((Im seq) . m) - ((Im seq) . n)) < p then A9: |.((seq . m) - (seq . n)).| < p by A8; Im ((seq . m) - (seq . n)) = (Im (seq . m)) - (Im (seq . n)) by COMPLEX1:19 .= ((Im seq) . m) - (Im (seq . n)) by Def6 .= ((Im seq) . m) - ((Im seq) . n) by Def6 ; then abs (((Im seq) . m) - ((Im seq) . n)) <= |.((seq . m) - (seq . n)).| by Th13; hence abs (((Im seq) . m) - ((Im seq) . n)) < p by A9, XXREAL_0:2; ::_thesis: verum end; hence Im seq is convergent by SEQ_4:41; ::_thesis: seq is convergent hence seq is convergent by A6, Th42; ::_thesis: verum end; now__::_thesis:_(_seq_is_convergent_implies_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.((seq_._m)_-_(seq_._n)).|_<_p_) assume seq is convergent ; ::_thesis: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p then consider z being Element of COMPLEX such that A10: for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - z).| < p by COMSEQ_2:def_5; let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p then consider n being Element of NAT such that A11: for m being Element of NAT st n <= m holds |.((seq . m) - z).| < p / 2 by A10; take n = n; ::_thesis: for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((seq . m) - (seq . n)).| < p ) assume n <= m ; ::_thesis: |.((seq . m) - (seq . n)).| < p then A12: |.((seq . m) - z).| < p / 2 by A11; |.((seq . n) - z).| < p / 2 by A11; then |.((seq . m) - z).| + |.((seq . n) - z).| < (p / 2) + (p / 2) by A12, XREAL_1:8; then A13: |.((seq . m) - z).| + |.(z - (seq . n)).| < p by COMPLEX1:60; |.((seq . m) - (seq . n)).| <= |.((seq . m) - z).| + |.(z - (seq . n)).| by COMPLEX1:63; hence |.((seq . m) - (seq . n)).| < p by A13, XXREAL_0:2; ::_thesis: verum end; hence ( seq is convergent iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p ) by A1; ::_thesis: verum end; theorem :: COMSEQ_3:47 for seq being Complex_Sequence st seq is convergent holds for p being Real st 0 < p holds ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds |.((seq . m) - (seq . l)).| < p proof let seq be Complex_Sequence; ::_thesis: ( seq is convergent implies for p being Real st 0 < p holds ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds |.((seq . m) - (seq . l)).| < p ) assume A1: seq is convergent ; ::_thesis: for p being Real st 0 < p holds ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds |.((seq . m) - (seq . l)).| < p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds |.((seq . m) - (seq . l)).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m, l being Element of NAT st n <= m & n <= l holds |.((seq . m) - (seq . l)).| < p then consider n being Element of NAT such that A2: for m being Element of NAT st n <= m holds |.((seq . m) - (seq . n)).| < p / 2 by A1, Th46; take n ; ::_thesis: for m, l being Element of NAT st n <= m & n <= l holds |.((seq . m) - (seq . l)).| < p now__::_thesis:_for_m,_l_being_Element_of_NAT_st_n_<=_m_&_n_<=_l_holds_ |.((seq_._m)_-_(seq_._l)).|_<_p let m, l be Element of NAT ; ::_thesis: ( n <= m & n <= l implies |.((seq . m) - (seq . l)).| < p ) assume ( n <= m & n <= l ) ; ::_thesis: |.((seq . m) - (seq . l)).| < p then ( |.((seq . m) - (seq . n)).| < p / 2 & |.((seq . l) - (seq . n)).| < p / 2 ) by A2; then A3: |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).| < (p / 2) + (p / 2) by XREAL_1:8; |.(((seq . m) - (seq . n)) - ((seq . l) - (seq . n))).| <= |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).| by COMPLEX1:57; hence |.((seq . m) - (seq . l)).| < p by A3, XXREAL_0:2; ::_thesis: verum end; hence for m, l being Element of NAT st n <= m & n <= l holds |.((seq . m) - (seq . l)).| < p ; ::_thesis: verum end; theorem :: COMSEQ_3:48 for rseq being Real_Sequence for seq being Complex_Sequence st ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds ( seq is convergent & lim seq = 0c ) proof let rseq be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 holds ( seq is convergent & lim seq = 0c ) let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds |.(seq . n).| <= rseq . n ) & rseq is convergent & lim rseq = 0 implies ( seq is convergent & lim seq = 0c ) ) assume that A1: for n being Element of NAT holds |.(seq . n).| <= rseq . n and A2: ( rseq is convergent & lim rseq = 0 ) ; ::_thesis: ( seq is convergent & lim seq = 0c ) A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_C_._n_<=_(abs_(Re_seq))_._n let n be Element of NAT ; ::_thesis: C . n <= (abs (Re seq)) . n (abs (Re seq)) . n = abs ((Re seq) . n) by SEQ_1:12; then 0 <= (abs (Re seq)) . n by COMPLEX1:46; hence C . n <= (abs (Re seq)) . n by FUNCOP_1:7; ::_thesis: verum end; C . 0 = 0 by FUNCOP_1:7; then A4: lim C = 0 by SEQ_4:25; now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(Re_seq))_._n_<=_rseq_._n let n be Element of NAT ; ::_thesis: (abs (Re seq)) . n <= rseq . n (Re seq) . n = Re (seq . n) by Def5; then A5: (abs (Re seq)) . n = abs (Re (seq . n)) by SEQ_1:12; ( abs (Re (seq . n)) <= |.(seq . n).| & |.(seq . n).| <= rseq . n ) by A1, Th13; hence (abs (Re seq)) . n <= rseq . n by A5, XXREAL_0:2; ::_thesis: verum end; then A6: ( abs (Re seq) is convergent & lim (abs (Re seq)) = 0 ) by A2, A4, A3, SEQ_2:19, SEQ_2:20; then A7: Re seq is convergent by SEQ_4:15; A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_C_._n_<=_(abs_(Im_seq))_._n let n be Element of NAT ; ::_thesis: C . n <= (abs (Im seq)) . n (abs (Im seq)) . n = abs ((Im seq) . n) by SEQ_1:12; then 0 <= (abs (Im seq)) . n by COMPLEX1:46; hence C . n <= (abs (Im seq)) . n by FUNCOP_1:7; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(Im_seq))_._n_<=_rseq_._n let n be Element of NAT ; ::_thesis: (abs (Im seq)) . n <= rseq . n A9: ( (Im seq) . n = Im (seq . n) & (abs (Im seq)) . n = abs ((Im seq) . n) ) by Def6, SEQ_1:12; ( abs (Im (seq . n)) <= |.(seq . n).| & |.(seq . n).| <= rseq . n ) by A1, Th13; hence (abs (Im seq)) . n <= rseq . n by A9, XXREAL_0:2; ::_thesis: verum end; then A10: ( abs (Im seq) is convergent & lim (abs (Im seq)) = 0 ) by A2, A4, A8, SEQ_2:19, SEQ_2:20; then A11: Im seq is convergent by SEQ_4:15; lim (Im seq) = 0 by A10, SEQ_4:15; then A12: Im (lim seq) = 0 by A7, A11, Th42; lim (Re seq) = 0 by A6, SEQ_4:15; then Re (lim seq) = 0 by A7, A11, Th42; hence ( seq is convergent & lim seq = 0c ) by A7, A11, A12, Lm1, Th42, COMPLEX1:13; ::_thesis: verum end; begin theorem :: COMSEQ_3:49 for seq, seq1 being Complex_Sequence st seq is subsequence of seq1 holds ( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 ) proof let seq, seq1 be Complex_Sequence; ::_thesis: ( seq is subsequence of seq1 implies ( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 ) ) assume seq is subsequence of seq1 ; ::_thesis: ( Re seq is subsequence of Re seq1 & Im seq is subsequence of Im seq1 ) then consider Nseq being increasing sequence of NAT such that A1: seq = seq1 * Nseq by VALUED_0:def_17; Re seq = (Re seq1) * Nseq by A1, Th22; hence Re seq is subsequence of Re seq1 ; ::_thesis: Im seq is subsequence of Im seq1 Im seq = (Im seq1) * Nseq by A1, Th22; hence Im seq is subsequence of Im seq1 ; ::_thesis: verum end; theorem :: COMSEQ_3:50 for seq being Complex_Sequence st seq is bounded holds ex seq1 being Complex_Sequence st ( seq1 is subsequence of seq & seq1 is convergent ) proof let seq be Complex_Sequence; ::_thesis: ( seq is bounded implies ex seq1 being Complex_Sequence st ( seq1 is subsequence of seq & seq1 is convergent ) ) assume seq is bounded ; ::_thesis: ex seq1 being Complex_Sequence st ( seq1 is subsequence of seq & seq1 is convergent ) then consider r being Real such that A1: 0 < r and A2: for n being Element of NAT holds |.(seq . n).| < r by COMSEQ_2:8; now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_((Re_seq)_._n)_<_r let n be Element of NAT ; ::_thesis: abs ((Re seq) . n) < r ( abs ((Re seq) . n) = abs (Re (seq . n)) & abs (Re (seq . n)) <= |.(seq . n).| ) by Def5, Th13; hence abs ((Re seq) . n) < r by A2, XXREAL_0:2; ::_thesis: verum end; then Re seq is bounded by A1, SEQ_2:3; then consider rseq1 being Real_Sequence such that A3: rseq1 is subsequence of Re seq and A4: rseq1 is convergent by SEQ_4:40; consider Nseq being increasing sequence of NAT such that A5: rseq1 = (Re seq) * Nseq by A3, VALUED_0:def_17; A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_|.((seq_*_Nseq)_._n).|_<_r let n be Element of NAT ; ::_thesis: |.((seq * Nseq) . n).| < r |.((seq * Nseq) . n).| = |.(seq . (Nseq . n)).| by FUNCT_2:15; hence |.((seq * Nseq) . n).| < r by A2; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_((Im_(seq_*_Nseq))_._n)_<_r let n be Element of NAT ; ::_thesis: abs ((Im (seq * Nseq)) . n) < r ( abs ((Im (seq * Nseq)) . n) = abs (Im ((seq * Nseq) . n)) & abs (Im ((seq * Nseq) . n)) <= |.((seq * Nseq) . n).| ) by Def6, Th13; hence abs ((Im (seq * Nseq)) . n) < r by A6, XXREAL_0:2; ::_thesis: verum end; then Im (seq * Nseq) is bounded by A1, SEQ_2:3; then consider rseq2 being Real_Sequence such that A7: rseq2 is subsequence of Im (seq * Nseq) and A8: rseq2 is convergent by SEQ_4:40; consider Nseq1 being increasing sequence of NAT such that A9: rseq2 = (Im (seq * Nseq)) * Nseq1 by A7, VALUED_0:def_17; Re ((seq * Nseq) * Nseq1) = (Re (seq * Nseq)) * Nseq1 by Th22 .= rseq1 * Nseq1 by A5, Th22 ; then A10: Re ((seq * Nseq) * Nseq1) is convergent by A4, SEQ_4:16; ( seq * Nseq is subsequence of seq & (seq * Nseq) * Nseq1 is subsequence of seq * Nseq ) by VALUED_0:def_17; then A11: (seq * Nseq) * Nseq1 is subsequence of seq by VALUED_0:20; Im ((seq * Nseq) * Nseq1) is convergent by A8, A9, Th22; hence ex seq1 being Complex_Sequence st ( seq1 is subsequence of seq & seq1 is convergent ) by A11, A10, Th42; ::_thesis: verum end; definition let seq be Complex_Sequence; attrseq is summable means :Def8: :: COMSEQ_3:def 8 Partial_Sums seq is convergent ; end; :: deftheorem Def8 defines summable COMSEQ_3:def_8_:_ for seq being Complex_Sequence holds ( seq is summable iff Partial_Sums seq is convergent ); set D = NAT --> 0c; registration cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued summable for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is summable proof take NAT --> 0c ; ::_thesis: NAT --> 0c is summable take 0c ; :: according to COMSEQ_2:def_5,COMSEQ_3:def_8 ::_thesis: for b1 being Element of REAL holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= |.(((Partial_Sums (NAT --> 0c)) . b3) - 0c).| ) ) let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= |.(((Partial_Sums (NAT --> 0c)) . b2) - 0c).| ) ) assume A1: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= |.(((Partial_Sums (NAT --> 0c)) . b2) - 0c).| ) take 0 ; ::_thesis: for b1 being Element of NAT holds ( not 0 <= b1 or not p <= |.(((Partial_Sums (NAT --> 0c)) . b1) - 0c).| ) for n being Element of NAT holds (NAT --> 0c) . n = 0c by FUNCOP_1:7; hence for b1 being Element of NAT holds ( not 0 <= b1 or not p <= |.(((Partial_Sums (NAT --> 0c)) . b1) - 0c).| ) by A1, Th24, COMPLEX1:44; ::_thesis: verum end; end; registration let seq be summable Complex_Sequence; cluster Partial_Sums seq -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = Partial_Sums seq holds b1 is convergent by Def8; end; definition let seq be Complex_Sequence; attrseq is absolutely_summable means :Def9: :: COMSEQ_3:def 9 |.seq.| is summable ; end; :: deftheorem Def9 defines absolutely_summable COMSEQ_3:def_9_:_ for seq being Complex_Sequence holds ( seq is absolutely_summable iff |.seq.| is summable ); theorem Th51: :: COMSEQ_3:51 for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n = 0c ) holds seq is absolutely_summable proof let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n = 0c ) implies seq is absolutely_summable ) assume A1: for n being Element of NAT holds seq . n = 0c ; ::_thesis: seq is absolutely_summable take 0 ; :: according to SEQ_2:def_6,SERIES_1:def_2,COMSEQ_3:def_9 ::_thesis: for b1 being set holds ( b1 <= 0 or ex b2 being Element of NAT st for b3 being Element of NAT holds ( not b2 <= b3 or not b1 <= abs (((Partial_Sums |.seq.|) . b3) - 0) ) ) let p be real number ; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs (((Partial_Sums |.seq.|) . b2) - 0) ) ) assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st for b2 being Element of NAT holds ( not b1 <= b2 or not p <= abs (((Partial_Sums |.seq.|) . b2) - 0) ) take 0 ; ::_thesis: for b1 being Element of NAT holds ( not 0 <= b1 or not p <= abs (((Partial_Sums |.seq.|) . b1) - 0) ) let m be Element of NAT ; ::_thesis: ( not 0 <= m or not p <= abs (((Partial_Sums |.seq.|) . m) - 0) ) abs (((Partial_Sums |.seq.|) . m) - 0) = abs (0 - 0) by A1, Th25 .= 0 by ABSVALUE:def_1 ; hence ( not 0 <= m or not p <= abs (((Partial_Sums |.seq.|) . m) - 0) ) by A2; ::_thesis: verum end; registration cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued absolutely_summable for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is absolutely_summable proof take NAT --> 0c ; ::_thesis: NAT --> 0c is absolutely_summable for n being Element of NAT holds (NAT --> 0c) . n = 0c by FUNCOP_1:7; hence NAT --> 0c is absolutely_summable by Th51; ::_thesis: verum end; end; registration let seq be absolutely_summable Complex_Sequence; cluster|.seq.| -> summable for Real_Sequence; coherence for b1 being Real_Sequence st b1 = |.seq.| holds b1 is summable by Def9; end; theorem Th52: :: COMSEQ_3:52 for seq being Complex_Sequence st seq is summable holds ( seq is convergent & lim seq = 0c ) proof let seq be Complex_Sequence; ::_thesis: ( seq is summable implies ( seq is convergent & lim seq = 0c ) ) assume A1: seq is summable ; ::_thesis: ( seq is convergent & lim seq = 0c ) then Re (Partial_Sums seq) is convergent ; then Partial_Sums (Re seq) is convergent by Th26; then A2: Re seq is summable by SERIES_1:def_2; Im (Partial_Sums seq) is convergent by A1; then Partial_Sums (Im seq) is convergent by Th26; then A3: Im seq is summable by SERIES_1:def_2; then lim (Im seq) = 0 by SERIES_1:4; then A4: Im (lim seq) = 0 by A2, A3, Th42; lim (Re seq) = 0 by A2, SERIES_1:4; then Re (lim seq) = 0 by A2, A3, Th42; hence ( seq is convergent & lim seq = 0c ) by A2, A3, A4, Lm1, Th42, COMPLEX1:13; ::_thesis: verum end; registration cluster Function-like V18( NAT , COMPLEX ) summable -> convergent for Element of K19(K20(NAT,COMPLEX)); coherence for b1 being Complex_Sequence st b1 is summable holds b1 is convergent by Th52; end; theorem Th53: :: COMSEQ_3:53 for seq being Complex_Sequence st seq is summable holds ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) ) proof let seq be Complex_Sequence; ::_thesis: ( seq is summable implies ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) ) ) A1: ( lim (Re (Partial_Sums seq)) = lim (Partial_Sums (Re seq)) & lim (Im (Partial_Sums seq)) = lim (Partial_Sums (Im seq)) ) by Th26; assume A2: seq is summable ; ::_thesis: ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) ) then Re (Partial_Sums seq) is convergent ; then A3: Partial_Sums (Re seq) is convergent by Th26; Im (Partial_Sums seq) is convergent by A2; then A4: Partial_Sums (Im seq) is convergent by Th26; ( lim (Re (Partial_Sums seq)) = Re (lim (Partial_Sums seq)) & lim (Im (Partial_Sums seq)) = Im (lim (Partial_Sums seq)) ) by A2, Th41; hence ( Re seq is summable & Im seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) ) by A3, A4, A1, COMPLEX1:13, SERIES_1:def_2; ::_thesis: verum end; registration let seq be summable Complex_Sequence; cluster Re seq -> summable for Real_Sequence; coherence for b1 being Real_Sequence st b1 = Re seq holds b1 is summable by Th53; cluster Im seq -> summable for Real_Sequence; coherence for b1 being Real_Sequence st b1 = Im seq holds b1 is summable by Th53; end; theorem Th54: :: COMSEQ_3:54 for seq1, seq2 being Complex_Sequence st seq1 is summable & seq2 is summable holds ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) ) assume A1: ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) then A2: (Partial_Sums seq1) + (Partial_Sums seq2) is convergent ; A3: (Partial_Sums seq1) + (Partial_Sums seq2) = Partial_Sums (seq1 + seq2) by Th27; Sum (seq1 + seq2) = lim ((Partial_Sums seq1) + (Partial_Sums seq2)) by Th27 .= (lim (Partial_Sums seq1)) + (lim (Partial_Sums seq2)) by A1, COMSEQ_2:14 ; hence ( seq1 + seq2 is summable & Sum (seq1 + seq2) = (Sum seq1) + (Sum seq2) ) by A2, A3, Def8; ::_thesis: verum end; theorem Th55: :: COMSEQ_3:55 for seq1, seq2 being Complex_Sequence st seq1 is summable & seq2 is summable holds ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( seq1 is summable & seq2 is summable implies ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) ) assume A1: ( seq1 is summable & seq2 is summable ) ; ::_thesis: ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) then A2: (Partial_Sums seq1) - (Partial_Sums seq2) is convergent ; A3: (Partial_Sums seq1) - (Partial_Sums seq2) = Partial_Sums (seq1 - seq2) by Th28; Sum (seq1 - seq2) = lim ((Partial_Sums seq1) - (Partial_Sums seq2)) by Th28 .= (lim (Partial_Sums seq1)) - (lim (Partial_Sums seq2)) by A1, COMSEQ_2:26 ; hence ( seq1 - seq2 is summable & Sum (seq1 - seq2) = (Sum seq1) - (Sum seq2) ) by A2, A3, Def8; ::_thesis: verum end; registration let seq1, seq2 be summable Complex_Sequence; clusterseq1 + seq2 -> summable for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = seq1 + seq2 holds b1 is summable by Th54; clusterseq1 - seq2 -> summable for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = seq1 - seq2 holds b1 is summable by Th55; end; theorem Th56: :: COMSEQ_3:56 for seq being Complex_Sequence st seq is summable holds for z being complex number holds ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) proof let seq be Complex_Sequence; ::_thesis: ( seq is summable implies for z being complex number holds ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) ) assume A1: seq is summable ; ::_thesis: for z being complex number holds ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) let z be complex number ; ::_thesis: ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) A2: Partial_Sums (z (#) seq) = z (#) (Partial_Sums seq) by Th29; Sum (z (#) seq) = lim (z (#) (Partial_Sums seq)) by Th29 .= z * (Sum seq) by A1, COMSEQ_2:18 ; hence ( z (#) seq is summable & Sum (z (#) seq) = z * (Sum seq) ) by A1, A2, Def8; ::_thesis: verum end; registration let z be Element of COMPLEX ; let seq be summable Complex_Sequence; clusterz (#) seq -> summable for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = z (#) seq holds b1 is summable by Th56; end; theorem Th57: :: COMSEQ_3:57 for seq being Complex_Sequence st Re seq is summable & Im seq is summable holds ( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) ) proof let seq be Complex_Sequence; ::_thesis: ( Re seq is summable & Im seq is summable implies ( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) ) ) assume that A1: Re seq is summable and A2: Im seq is summable ; ::_thesis: ( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) ) Partial_Sums (Im seq) is convergent by A2, SERIES_1:def_2; then A3: Im (Partial_Sums seq) is convergent by Th26; Partial_Sums (Re seq) is convergent by A1, SERIES_1:def_2; then A4: Re (Partial_Sums seq) is convergent by Th26; then A5: lim (Im (Partial_Sums seq)) = Im (lim (Partial_Sums seq)) by A3, Th42; A6: ( lim (Re (Partial_Sums seq)) = lim (Partial_Sums (Re seq)) & lim (Im (Partial_Sums seq)) = lim (Partial_Sums (Im seq)) ) by Th26; ( Partial_Sums seq is convergent & lim (Re (Partial_Sums seq)) = Re (lim (Partial_Sums seq)) ) by A4, A3, Th42; hence ( seq is summable & Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) ) by A6, A5, Def8, COMPLEX1:13; ::_thesis: verum end; theorem Th58: :: COMSEQ_3:58 for seq being Complex_Sequence st seq is summable holds for n being Element of NAT holds seq ^\ n is summable proof let seq be Complex_Sequence; ::_thesis: ( seq is summable implies for n being Element of NAT holds seq ^\ n is summable ) assume A1: seq is summable ; ::_thesis: for n being Element of NAT holds seq ^\ n is summable let n be Element of NAT ; ::_thesis: seq ^\ n is summable A2: ( Re (seq ^\ n) = (Re seq) ^\ n & Im (seq ^\ n) = (Im seq) ^\ n ) by Th23; ( (Re seq) ^\ n is summable & (Im seq) ^\ n is summable ) by A1, SERIES_1:12; hence seq ^\ n is summable by A2, Th57; ::_thesis: verum end; registration let seq be summable Complex_Sequence; let n be Element of NAT ; clusterseq ^\ n -> summable for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = seq ^\ n holds b1 is summable by Th58; end; theorem :: COMSEQ_3:59 for seq being Complex_Sequence st ex n being Element of NAT st seq ^\ n is summable holds seq is summable proof let seq be Complex_Sequence; ::_thesis: ( ex n being Element of NAT st seq ^\ n is summable implies seq is summable ) given n being Element of NAT such that A1: seq ^\ n is summable ; ::_thesis: seq is summable Im (seq ^\ n) = (Im seq) ^\ n by Th23; then A2: Im seq is summable by A1, SERIES_1:13; Re (seq ^\ n) = (Re seq) ^\ n by Th23; then Re seq is summable by A1, SERIES_1:13; hence seq is summable by A2, Th57; ::_thesis: verum end; theorem :: COMSEQ_3:60 for seq being Complex_Sequence st seq is summable holds for n being Element of NAT holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) proof let seq be Complex_Sequence; ::_thesis: ( seq is summable implies for n being Element of NAT holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) ) assume A1: seq is summable ; ::_thesis: for n being Element of NAT holds Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) then Sum seq = (Sum (Re seq)) + ((Sum (Im seq)) * ) by Th53; then A2: ( Re (Sum seq) = Sum (Re seq) & Im (Sum seq) = Sum (Im seq) ) by COMPLEX1:12; let n be Element of NAT ; ::_thesis: Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) A3: Sum (seq ^\ (n + 1)) = (Sum (Re (seq ^\ (n + 1)))) + ((Sum (Im (seq ^\ (n + 1)))) * ) by A1, Th53; A4: Sum (Im seq) = ((Partial_Sums (Im seq)) . n) + (Sum ((Im seq) ^\ (n + 1))) by A1, SERIES_1:15 .= ((Im (Partial_Sums seq)) . n) + (Sum ((Im seq) ^\ (n + 1))) by Th26 .= ((Im (Partial_Sums seq)) . n) + (Sum (Im (seq ^\ (n + 1)))) by Th23 .= ((Im (Partial_Sums seq)) . n) + (Im (Sum (seq ^\ (n + 1)))) by A3, COMPLEX1:12 .= (Im ((Partial_Sums seq) . n)) + (Im (Sum (seq ^\ (n + 1)))) by Def6 .= Im (((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))) by COMPLEX1:8 ; Sum (Re seq) = ((Partial_Sums (Re seq)) . n) + (Sum ((Re seq) ^\ (n + 1))) by A1, SERIES_1:15 .= ((Re (Partial_Sums seq)) . n) + (Sum ((Re seq) ^\ (n + 1))) by Th26 .= ((Re (Partial_Sums seq)) . n) + (Sum (Re (seq ^\ (n + 1)))) by Th23 .= ((Re (Partial_Sums seq)) . n) + (Re (Sum (seq ^\ (n + 1)))) by A3, COMPLEX1:12 .= (Re ((Partial_Sums seq) . n)) + (Re (Sum (seq ^\ (n + 1)))) by Def5 .= Re (((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1)))) by COMPLEX1:8 ; hence Sum seq = ((Partial_Sums seq) . n) + (Sum (seq ^\ (n + 1))) by A2, A4, COMPLEX1:def_3; ::_thesis: verum end; theorem Th61: :: COMSEQ_3:61 for seq being Complex_Sequence holds ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable ) proof let seq be Complex_Sequence; ::_thesis: ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable ) for n being Element of NAT holds 0 <= |.seq.| . n by Lm3; then ( Partial_Sums |.seq.| is bounded_above iff |.seq.| is summable ) by SERIES_1:17; hence ( Partial_Sums |.seq.| is bounded_above iff seq is absolutely_summable ) by Def9; ::_thesis: verum end; registration let seq be absolutely_summable Complex_Sequence; cluster Partial_Sums |.seq.| -> bounded_above for Real_Sequence; coherence for b1 being Real_Sequence st b1 = Partial_Sums |.seq.| holds b1 is bounded_above by Th61; end; theorem Th62: :: COMSEQ_3:62 for seq being Complex_Sequence holds ( seq is summable iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ) proof let seq be Complex_Sequence; ::_thesis: ( seq is summable iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ) now__::_thesis:_(_(_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).|_<_p_)_implies_seq_is_summable_) assume for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ; ::_thesis: seq is summable then Partial_Sums seq is convergent by Th46; hence seq is summable by Def8; ::_thesis: verum end; hence ( seq is summable iff for p being Real st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ) by Th46; ::_thesis: verum end; theorem Th63: :: COMSEQ_3:63 for seq being Complex_Sequence st seq is absolutely_summable holds seq is summable proof let seq be Complex_Sequence; ::_thesis: ( seq is absolutely_summable implies seq is summable ) assume A1: seq is absolutely_summable ; ::_thesis: seq is summable now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ |.(((Partial_Sums_seq)_._m)_-_((Partial_Sums_seq)_._n)).|_<_p let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p then consider n being Element of NAT such that A2: for m being Element of NAT st n <= m holds abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) < p by A1, SEQ_4:41; take n = n; ::_thesis: for m being Element of NAT st n <= m holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p ) assume n <= m ; ::_thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p then A3: abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) < p by A2; |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by Th31; hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| < p by A3, XXREAL_0:2; ::_thesis: verum end; hence seq is summable by Th62; ::_thesis: verum end; registration cluster Function-like V18( NAT , COMPLEX ) absolutely_summable -> summable for Element of K19(K20(NAT,COMPLEX)); coherence for b1 being Complex_Sequence st b1 is absolutely_summable holds b1 is summable by Th63; end; registration cluster Relation-like NAT -defined COMPLEX -valued Function-like non zero total V18( NAT , COMPLEX ) complex-valued absolutely_summable for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is absolutely_summable proof set C = the absolutely_summable Complex_Sequence; take the absolutely_summable Complex_Sequence ; ::_thesis: the absolutely_summable Complex_Sequence is absolutely_summable thus the absolutely_summable Complex_Sequence is absolutely_summable ; ::_thesis: verum end; end; theorem Th64: :: COMSEQ_3:64 for z being Element of COMPLEX st |.z.| < 1 holds ( z GeoSeq is summable & Sum (z GeoSeq) = 1r / (1r - z) ) proof let z be Element of COMPLEX ; ::_thesis: ( |.z.| < 1 implies ( z GeoSeq is summable & Sum (z GeoSeq) = 1r / (1r - z) ) ) set seq2 = NAT --> 1r; deffunc H1( Element of NAT ) -> Element of COMPLEX = z #N (\$1 + 1); consider seq1 being Complex_Sequence such that A1: for n being Element of NAT holds seq1 . n = H1(n) from COMSEQ_1:sch_1(); assume A2: |.z.| < 1 ; ::_thesis: ( z GeoSeq is summable & Sum (z GeoSeq) = 1r / (1r - z) ) then A3: lim seq1 = 0c by A1, Th44; A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_(z_GeoSeq))_._n_=_((1r_/_(1r_-_z))_(#)_((NAT_-->_1r)_-_seq1))_._n let n be Element of NAT ; ::_thesis: (Partial_Sums (z GeoSeq)) . n = ((1r / (1r - z)) (#) ((NAT --> 1r) - seq1)) . n thus (Partial_Sums (z GeoSeq)) . n = (1r - (z #N (n + 1))) / (1r - z) by A2, Th36, COMPLEX1:48 .= (1r - (seq1 . n)) / (1r - z) by A1 .= (1r * (((NAT --> 1r) . n) - (seq1 . n))) / (1r - z) by COMPLEX1:def_4, FUNCOP_1:7 .= (1r / (1r - z)) * (((NAT --> 1r) . n) + (- (seq1 . n))) by XCMPLX_1:74 .= (1r / (1r - z)) * (((NAT --> 1r) . n) + ((- seq1) . n)) by VALUED_1:8 .= (1r / (1r - z)) * (((NAT --> 1r) - seq1) . n) by VALUED_1:1 .= ((1r / (1r - z)) (#) ((NAT --> 1r) - seq1)) . n by VALUED_1:6 ; ::_thesis: verum end; A5: for n being Element of NAT holds (NAT --> 1r) . n = 1r by FUNCOP_1:7; then A6: NAT --> 1r is convergent by COMSEQ_2:9; A7: seq1 is convergent by A2, A1, Th44; then A8: (NAT --> 1r) - seq1 is convergent by A6; hence Partial_Sums (z GeoSeq) is convergent by A4, FUNCT_2:63; :: according to COMSEQ_3:def_8 ::_thesis: Sum (z GeoSeq) = 1r / (1r - z) lim ((NAT --> 1r) - seq1) = (lim (NAT --> 1r)) - (lim seq1) by A7, A6, COMSEQ_2:26 .= 1r by A3, A5, COMSEQ_2:10 ; then lim ((1r / (1r - z)) (#) ((NAT --> 1r) - seq1)) = (1r / (1r - z)) * 1r by A8, COMSEQ_2:18 .= 1r / (1r - z) by COMPLEX1:def_4 ; hence Sum (z GeoSeq) = 1r / (1r - z) by A4, FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_3:65 for seq being Complex_Sequence for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds ( seq is summable & Sum seq = (seq . 0) / (1r - z) ) proof let seq be Complex_Sequence; ::_thesis: for z being Element of COMPLEX st |.z.| < 1 & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) holds ( seq is summable & Sum seq = (seq . 0) / (1r - z) ) let z be Element of COMPLEX ; ::_thesis: ( |.z.| < 1 & ( for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ) implies ( seq is summable & Sum seq = (seq . 0) / (1r - z) ) ) assume that A1: |.z.| < 1 and A2: for n being Element of NAT holds seq . (n + 1) = z * (seq . n) ; ::_thesis: ( seq is summable & Sum seq = (seq . 0) / (1r - z) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(Partial_Sums_seq)_._n_=_((seq_._0)_(#)_(Partial_Sums_(z_GeoSeq)))_._n let n be Element of NAT ; ::_thesis: (Partial_Sums seq) . n = ((seq . 0) (#) (Partial_Sums (z GeoSeq))) . n thus (Partial_Sums seq) . n = (seq . 0) * ((1r - (z #N (n + 1))) / (1r - z)) by A1, A2, Th37, COMPLEX1:48 .= (seq . 0) * ((Partial_Sums (z GeoSeq)) . n) by A1, Th36, COMPLEX1:48 .= ((seq . 0) (#) (Partial_Sums (z GeoSeq))) . n by VALUED_1:6 ; ::_thesis: verum end; then A3: Partial_Sums seq = (seq . 0) (#) (Partial_Sums (z GeoSeq)) by FUNCT_2:63; A4: z GeoSeq is summable by A1, Th64; hence seq is summable by A3, Def8; ::_thesis: Sum seq = (seq . 0) / (1r - z) Sum seq = (seq . 0) * (Sum (z GeoSeq)) by A3, A4, COMSEQ_2:18 .= (seq . 0) * (1r / (1r - z)) by A1, Th64 .= ((seq . 0) * 1r) / (1r - z) by XCMPLX_1:74 .= (seq . 0) / (1r - z) by COMPLEX1:def_4 ; hence Sum seq = (seq . 0) / (1r - z) ; ::_thesis: verum end; theorem :: COMSEQ_3:66 for rseq1 being Real_Sequence for seq2 being Complex_Sequence st rseq1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds |.(seq2 . n).| <= rseq1 . n holds seq2 is absolutely_summable proof let rseq1 be Real_Sequence; ::_thesis: for seq2 being Complex_Sequence st rseq1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds |.(seq2 . n).| <= rseq1 . n holds seq2 is absolutely_summable let seq2 be Complex_Sequence; ::_thesis: ( rseq1 is summable & ex m being Element of NAT st for n being Element of NAT st m <= n holds |.(seq2 . n).| <= rseq1 . n implies seq2 is absolutely_summable ) assume that A1: rseq1 is summable and A2: ex m being Element of NAT st for n being Element of NAT st m <= n holds |.(seq2 . n).| <= rseq1 . n ; ::_thesis: seq2 is absolutely_summable consider m being Element of NAT such that A3: for n being Element of NAT st m <= n holds |.(seq2 . n).| <= rseq1 . n by A2; A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<=_|.seq2.|_._n let n be Element of NAT ; ::_thesis: 0 <= |.seq2.| . n |.(seq2 . n).| = |.seq2.| . n by VALUED_1:18; hence 0 <= |.seq2.| . n by COMPLEX1:46; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_ |.seq2.|_._n_<=_rseq1_._n let n be Element of NAT ; ::_thesis: ( m <= n implies |.seq2.| . n <= rseq1 . n ) assume m <= n ; ::_thesis: |.seq2.| . n <= rseq1 . n then |.(seq2 . n).| <= rseq1 . n by A3; hence |.seq2.| . n <= rseq1 . n by VALUED_1:18; ::_thesis: verum end; hence |.seq2.| is summable by A1, A4, SERIES_1:19; :: according to COMSEQ_3:def_9 ::_thesis: verum end; theorem :: COMSEQ_3:67 for seq1, seq2 being Complex_Sequence st ( for n being Element of NAT holds ( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable holds ( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| ) proof let seq1, seq2 be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable implies ( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| ) ) assume ( ( for n being Element of NAT holds ( 0 <= |.seq1.| . n & |.seq1.| . n <= |.seq2.| . n ) ) & seq2 is absolutely_summable ) ; ::_thesis: ( seq1 is absolutely_summable & Sum |.seq1.| <= Sum |.seq2.| ) hence ( |.seq1.| is summable & Sum |.seq1.| <= Sum |.seq2.| ) by SERIES_1:20; :: according to COMSEQ_3:def_9 ::_thesis: verum end; theorem :: COMSEQ_3:68 for seq being Complex_Sequence st ( for n being Element of NAT holds |.seq.| . n > 0 ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds (|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds not seq is absolutely_summable by SERIES_1:27; theorem :: COMSEQ_3:69 for rseq1 being Real_Sequence for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is absolutely_summable proof let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is absolutely_summable let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable ) assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 < 1 ) ; ::_thesis: seq is absolutely_summable for n being Element of NAT holds |.seq.| . n >= 0 by Lm3; hence |.seq.| is summable by A1, SERIES_1:28; :: according to COMSEQ_3:def_9 ::_thesis: verum end; theorem :: COMSEQ_3:70 for rseq1 being Real_Sequence for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 holds not |.seq.| is summable proof let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 holds not |.seq.| is summable let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 implies not |.seq.| is summable ) assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & ex m being Element of NAT st for n being Element of NAT st m <= n holds rseq1 . n >= 1 ) ; ::_thesis: not |.seq.| is summable for n being Element of NAT holds |.seq.| . n >= 0 by Lm3; hence not |.seq.| is summable by A1, SERIES_1:29; ::_thesis: verum end; theorem :: COMSEQ_3:71 for rseq1 being Real_Sequence for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds not seq is absolutely_summable proof let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 holds not seq is absolutely_summable let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 implies not seq is absolutely_summable ) assume A1: ( ( for n being Element of NAT holds rseq1 . n = n -root (|.seq.| . n) ) & rseq1 is convergent & lim rseq1 > 1 ) ; ::_thesis: not seq is absolutely_summable for n being Element of NAT holds |.seq.| . n >= 0 by Lm3; hence not |.seq.| is summable by A1, SERIES_1:30; :: according to COMSEQ_3:def_9 ::_thesis: verum end; theorem :: COMSEQ_3:72 for rseq1 being Real_Sequence for seq being Complex_Sequence st |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds ( seq is absolutely_summable iff rseq1 is summable ) proof let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) holds ( seq is absolutely_summable iff rseq1 is summable ) let seq be Complex_Sequence; ::_thesis: ( |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) implies ( seq is absolutely_summable iff rseq1 is summable ) ) assume ( |.seq.| is non-increasing & ( for n being Element of NAT holds rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) ) ; ::_thesis: ( seq is absolutely_summable iff rseq1 is summable ) then for n being Element of NAT holds ( |.seq.| is non-increasing & |.seq.| . n >= 0 & rseq1 . n = (2 to_power n) * (|.seq.| . (2 to_power n)) ) by Lm3; then ( |.seq.| is summable iff rseq1 is summable ) by SERIES_1:31; hence ( seq is absolutely_summable iff rseq1 is summable ) by Def9; ::_thesis: verum end; theorem :: COMSEQ_3:73 for seq being Complex_Sequence for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds |.seq.| . n = 1 / (n to_power p) ) holds seq is absolutely_summable proof let seq be Complex_Sequence; ::_thesis: for p being Real st p > 1 & ( for n being Element of NAT st n >= 1 holds |.seq.| . n = 1 / (n to_power p) ) holds seq is absolutely_summable let p be Real; ::_thesis: ( p > 1 & ( for n being Element of NAT st n >= 1 holds |.seq.| . n = 1 / (n to_power p) ) implies seq is absolutely_summable ) assume ( p > 1 & ( for n being Element of NAT st n >= 1 holds |.seq.| . n = 1 / (n to_power p) ) ) ; ::_thesis: seq is absolutely_summable then |.seq.| is summable by SERIES_1:32; hence seq is absolutely_summable by Def9; ::_thesis: verum end; theorem :: COMSEQ_3:74 for seq being Complex_Sequence for p being Real st p <= 1 & ( for n being Element of NAT st n >= 1 holds |.seq.| . n = 1 / (n to_power p) ) holds not seq is absolutely_summable by SERIES_1:33; theorem :: COMSEQ_3:75 for rseq1 being Real_Sequence for seq being Complex_Sequence st ( for n being Element of NAT holds ( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is absolutely_summable proof let rseq1 be Real_Sequence; ::_thesis: for seq being Complex_Sequence st ( for n being Element of NAT holds ( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds seq is absolutely_summable let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds ( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is absolutely_summable ) assume that A1: for n being Element of NAT holds ( seq . n <> 0c & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) and A2: ( rseq1 is convergent & lim rseq1 < 1 ) ; ::_thesis: seq is absolutely_summable now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_|.seq.|_._n_<>_0_&_rseq1_._n_=_(|.seq.|_._(n_+_1))_/_(|.seq.|_._n)_&_|.seq.|_._n_<>_0_&_rseq1_._n_=_((abs_|.seq.|)_._(n_+_1))_/_(|.seq.|_._n)_&_|.seq.|_._n_<>_0_&_rseq1_._n_=_((abs_|.seq.|)_._(n_+_1))_/_((abs_|.seq.|)_._n)_) let n be Element of NAT ; ::_thesis: ( |.seq.| . n <> 0 & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) ) A3: ( seq . n <> 0c & |.seq.| . n = |.(seq . n).| ) by A1, VALUED_1:18; hence ( |.seq.| . n <> 0 & rseq1 . n = (|.seq.| . (n + 1)) / (|.seq.| . n) ) by A1, COMPLEX1:47; ::_thesis: ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / (|.seq.| . n) & |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) ) thus ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / (|.seq.| . n) ) by A1, A3, COMPLEX1:47; ::_thesis: ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) ) thus ( |.seq.| . n <> 0 & rseq1 . n = ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) ) by A1, A3, COMPLEX1:47; ::_thesis: verum end; then |.seq.| is absolutely_summable by A2, SERIES_1:37; hence seq is absolutely_summable by Def9; ::_thesis: verum end; theorem :: COMSEQ_3:76 for seq being Complex_Sequence st ( for n being Element of NAT holds seq . n <> 0c ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds (|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 holds not seq is absolutely_summable proof let seq be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n <> 0c ) & ex m being Element of NAT st for n being Element of NAT st n >= m holds (|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 implies not seq is absolutely_summable ) assume that A1: for n being Element of NAT holds seq . n <> 0c and A2: ex m being Element of NAT st for n being Element of NAT st n >= m holds (|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 ; ::_thesis: not seq is absolutely_summable consider m being Element of NAT such that A3: for n being Element of NAT st n >= m holds (|.seq.| . (n + 1)) / (|.seq.| . n) >= 1 by A2; A4: now__::_thesis:_for_n_being_Element_of_NAT_holds_|.seq.|_._n_<>_0 let n be Element of NAT ; ::_thesis: |.seq.| . n <> 0 seq . n <> 0c by A1; then |.(seq . n).| <> 0 by COMPLEX1:47; hence |.seq.| . n <> 0 by VALUED_1:18; ::_thesis: verum end; for n being Element of NAT st n >= m holds ((abs |.seq.|) . (n + 1)) / ((abs |.seq.|) . n) >= 1 by A3; hence not |.seq.| is summable by A4, SERIES_1:39; :: according to COMSEQ_3:def_9 ::_thesis: verum end;