:: COMSEQ_2 semantic presentation begin theorem Th1: :: COMSEQ_2:1 for g, r being Element of COMPLEX st g <> 0c & r <> 0c holds |.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|) proof let g, r be Element of COMPLEX ; ::_thesis: ( g <> 0c & r <> 0c implies |.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|) ) assume A1: ( g <> 0c & r <> 0c ) ; ::_thesis: |.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|) thus |.((g ") - (r ")).| = |.((1r / g) - (r ")).| by COMPLEX1:def_4, XCMPLX_1:215 .= |.((1r / g) - (1r / r)).| by COMPLEX1:def_4, XCMPLX_1:215 .= |.((1r / g) + (- (1r / r))).| .= |.((1r / g) + (- (1r * (r ")))).| by XCMPLX_0:def_9 .= |.((1r / g) + ((- 1r) * (r "))).| .= |.((1r / g) + ((- 1r) / r)).| by XCMPLX_0:def_9 .= |.(((1r * r) + ((- 1r) * g)) / (r * g)).| by A1, XCMPLX_1:116 .= |.(r - g).| / |.(g * r).| by COMPLEX1:67, COMPLEX1:def_4 .= |.(- (g - r)).| / (|.g.| * |.r.|) by COMPLEX1:65 .= |.(g - r).| / (|.g.| * |.r.|) by COMPLEX1:52 ; ::_thesis: verum end; theorem Th2: :: COMSEQ_2:2 for s being Complex_Sequence for n being Element of NAT ex r being Real st ( 0 < r & ( for m being Element of NAT st m <= n holds |.(s . m).| < r ) ) proof let s be Complex_Sequence; ::_thesis: for n being Element of NAT ex r being Real st ( 0 < r & ( for m being Element of NAT st m <= n holds |.(s . m).| < r ) ) let n be Element of NAT ; ::_thesis: ex r being Real st ( 0 < r & ( for m being Element of NAT st m <= n holds |.(s . m).| < r ) ) defpred S1[ Element of NAT ] means ex r being real number st ( 0 < r & ( for m being Element of NAT st m <= \$1 holds |.(s . m).| < r ) ); 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] ) given R1 being real number such that A2: 0 < R1 and A3: for m being Element of NAT st m <= n holds |.(s . m).| < R1 ; ::_thesis: S1[n + 1] A4: now__::_thesis:_(_R1_<=_|.(s_._(n_+_1)).|_implies_ex_R_being_Element_of_REAL_st_ (_0_<_R_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_ |.(s_._m).|_<_R_)_)_) assume A5: R1 <= |.(s . (n + 1)).| ; ::_thesis: ex R being Element of REAL st ( 0 < R & ( for m being Element of NAT st m <= n + 1 holds |.(s . m).| < R ) ) take R = |.(s . (n + 1)).| + 1; ::_thesis: ( 0 < R & ( for m being Element of NAT st m <= n + 1 holds |.(s . m).| < R ) ) 0 + 0 < R by COMPLEX1:46, XREAL_1:8; hence 0 < R ; ::_thesis: for m being Element of NAT st m <= n + 1 holds |.(s . m).| < R let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies |.(s . m).| < R ) assume A6: m <= n + 1 ; ::_thesis: |.(s . m).| < R A7: now__::_thesis:_(_m_<=_n_implies_|.(s_._m).|_<_R_) assume m <= n ; ::_thesis: |.(s . m).| < R then |.(s . m).| < R1 by A3; then |.(s . m).| < |.(s . (n + 1)).| by A5, XXREAL_0:2; then |.(s . m).| + 0 < R by XREAL_1:8; hence |.(s . m).| < R ; ::_thesis: verum end; now__::_thesis:_(_m_=_n_+_1_implies_|.(s_._m).|_<_R_) assume m = n + 1 ; ::_thesis: |.(s . m).| < R then |.(s . m).| + 0 < R by XREAL_1:8; hence |.(s . m).| < R ; ::_thesis: verum end; hence |.(s . m).| < R by A6, A7, NAT_1:8; ::_thesis: verum end; now__::_thesis:_(_|.(s_._(n_+_1)).|_<=_R1_implies_ex_R_being_Element_of_REAL_st_ (_R_>_0_&_(_for_m_being_Element_of_NAT_st_m_<=_n_+_1_holds_ |.(s_._m).|_<_R_)_)_) assume A8: |.(s . (n + 1)).| <= R1 ; ::_thesis: ex R being Element of REAL st ( R > 0 & ( for m being Element of NAT st m <= n + 1 holds |.(s . m).| < R ) ) take R = R1 + 1; ::_thesis: ( R > 0 & ( for m being Element of NAT st m <= n + 1 holds |.(s . m).| < R ) ) thus R > 0 by A2; ::_thesis: for m being Element of NAT st m <= n + 1 holds |.(s . m).| < R let m be Element of NAT ; ::_thesis: ( m <= n + 1 implies |.(s . m).| < R ) assume A9: m <= n + 1 ; ::_thesis: |.(s . m).| < R A10: now__::_thesis:_(_m_<=_n_implies_|.(s_._m).|_<_R_) assume m <= n ; ::_thesis: |.(s . m).| < R then A11: |.(s . m).| < R1 by A3; R1 + 0 < R by XREAL_1:8; hence |.(s . m).| < R by A11, XXREAL_0:2; ::_thesis: verum end; now__::_thesis:_(_m_=_n_+_1_implies_|.(s_._m).|_<_R_) A12: R1 + 0 < R by XREAL_1:8; assume m = n + 1 ; ::_thesis: |.(s . m).| < R hence |.(s . m).| < R by A8, A12, XXREAL_0:2; ::_thesis: verum end; hence |.(s . m).| < R by A9, A10, NAT_1:8; ::_thesis: verum end; hence S1[n + 1] by A4; ::_thesis: verum end; A13: S1[ 0 ] proof take R = |.(s . 0).| + 1; ::_thesis: ( 0 < R & ( for m being Element of NAT st m <= 0 holds |.(s . m).| < R ) ) 0 + 0 < |.(s . 0).| + 1 by COMPLEX1:46, XREAL_1:8; hence 0 < R ; ::_thesis: for m being Element of NAT st m <= 0 holds |.(s . m).| < R let m be Element of NAT ; ::_thesis: ( m <= 0 implies |.(s . m).| < R ) assume m <= 0 ; ::_thesis: |.(s . m).| < R then m = 0 by NAT_1:2; then |.(s . m).| + 0 < R by XREAL_1:8; hence |.(s . m).| < R ; ::_thesis: verum end; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A1); then consider R being real number such that A14: ( R > 0 & ( for m being Element of NAT st m <= n holds |.(s . m).| < R ) ) ; R is Real by XREAL_0:def_1; hence ex r being Real st ( 0 < r & ( for m being Element of NAT st m <= n holds |.(s . m).| < r ) ) by A14; ::_thesis: verum end; begin definition let f be complex-valued Function; deffunc H1( set ) -> Element of COMPLEX = (f . \$1) *' ; funcf *' -> complex-valued Function means :Def1: :: COMSEQ_2:def 1 ( dom it = dom f & ( for c being set st c in dom it holds it . c = (f . c) *' ) ); existence ex b1 being complex-valued Function st ( dom b1 = dom f & ( for c being set st c in dom b1 holds b1 . c = (f . c) *' ) ) proof consider F being Function such that A1: dom F = dom f and A2: for x being set st x in dom f holds F . x = H1(x) from FUNCT_1:sch_3(); for x being set st x in dom F holds F . x is complex proof let x be set ; ::_thesis: ( x in dom F implies F . x is complex ) assume x in dom F ; ::_thesis: F . x is complex then F . x = H1(x) by A1, A2; hence F . x is complex ; ::_thesis: verum end; then reconsider F = F as complex-valued Function by VALUED_0:def_7; take F ; ::_thesis: ( dom F = dom f & ( for c being set st c in dom F holds F . c = (f . c) *' ) ) thus dom f = dom F by A1; ::_thesis: for c being set st c in dom F holds F . c = (f . c) *' thus for c being set st c in dom F holds F . c = (f . c) *' by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being complex-valued Function st dom b1 = dom f & ( for c being set st c in dom b1 holds b1 . c = (f . c) *' ) & dom b2 = dom f & ( for c being set st c in dom b2 holds b2 . c = (f . c) *' ) holds b1 = b2 proof let h, g be complex-valued Function; ::_thesis: ( dom h = dom f & ( for c being set st c in dom h holds h . c = (f . c) *' ) & dom g = dom f & ( for c being set st c in dom g holds g . c = (f . c) *' ) implies h = g ) assume that A3: dom h = dom f and A4: for c being set st c in dom h holds h . c = H1(c) and A5: dom g = dom f and A6: for c being set st c in dom g holds g . c = H1(c) ; ::_thesis: h = g thus dom h = dom g by A3, A5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in dom h or h . b1 = g . b1 ) let x be set ; ::_thesis: ( not x in dom h or h . x = g . x ) assume A7: x in dom h ; ::_thesis: h . x = g . x hence h . x = H1(x) by A4 .= g . x by A3, A5, A6, A7 ; ::_thesis: verum end; involutiveness for b1, b2 being complex-valued Function st dom b1 = dom b2 & ( for c being set st c in dom b1 holds b1 . c = (b2 . c) *' ) holds ( dom b2 = dom b1 & ( for c being set st c in dom b2 holds b2 . c = (b1 . c) *' ) ) proof let g, f be complex-valued Function; ::_thesis: ( dom g = dom f & ( for c being set st c in dom g holds g . c = (f . c) *' ) implies ( dom f = dom g & ( for c being set st c in dom f holds f . c = (g . c) *' ) ) ) assume that A8: dom g = dom f and A9: for c being set st c in dom g holds g . c = (f . c) *' ; ::_thesis: ( dom f = dom g & ( for c being set st c in dom f holds f . c = (g . c) *' ) ) thus dom f = dom g by A8; ::_thesis: for c being set st c in dom f holds f . c = (g . c) *' let c be set ; ::_thesis: ( c in dom f implies f . c = (g . c) *' ) assume A10: c in dom f ; ::_thesis: f . c = (g . c) *' thus f . c = ((f . c) *') *' .= (g . c) *' by A8, A10, A9 ; ::_thesis: verum end; end; :: deftheorem Def1 defines *' COMSEQ_2:def_1_:_ for f, b2 being complex-valued Function holds ( b2 = f *' iff ( dom b2 = dom f & ( for c being set st c in dom b2 holds b2 . c = (f . c) *' ) ) ); definition let C be non empty set ; let f be Function of C,COMPLEX; :: original: *' redefine funcf *' -> Function of C,COMPLEX means :Def2: :: COMSEQ_2:def 2 ( dom it = C & ( for n being Element of C holds it . n = (f . n) *' ) ); coherence f *' is Function of C,COMPLEX proof A1: dom (f *') = dom f by Def1 .= C by PARTFUN1:def_2 ; for x being set st x in C holds (f *') . x in COMPLEX by XCMPLX_0:def_2; hence f *' is Function of C,COMPLEX by A1, FUNCT_2:3; ::_thesis: verum end; compatibility for b1 being Function of C,COMPLEX holds ( b1 = f *' iff ( dom b1 = C & ( for n being Element of C holds b1 . n = (f . n) *' ) ) ) proof let IT be Function of C,COMPLEX; ::_thesis: ( IT = f *' iff ( dom IT = C & ( for n being Element of C holds IT . n = (f . n) *' ) ) ) thus ( IT = f *' implies ( dom IT = C & ( for c being Element of C holds IT . c = (f . c) *' ) ) ) ::_thesis: ( dom IT = C & ( for n being Element of C holds IT . n = (f . n) *' ) implies IT = f *' ) proof assume A2: IT = f *' ; ::_thesis: ( dom IT = C & ( for c being Element of C holds IT . c = (f . c) *' ) ) thus A3: dom IT = C by FUNCT_2:def_1; ::_thesis: for c being Element of C holds IT . c = (f . c) *' let c be Element of C; ::_thesis: IT . c = (f . c) *' thus IT . c = (f . c) *' by A2, A3, Def1; ::_thesis: verum end; assume that A4: dom IT = C and A5: for c being Element of C holds IT . c = (f . c) *' ; ::_thesis: IT = f *' A6: dom IT = dom f by A4, FUNCT_2:def_1; for c being set st c in dom IT holds IT . c = (f . c) *' by A5; hence IT = f *' by A6, Def1; ::_thesis: verum end; end; :: deftheorem Def2 defines *' COMSEQ_2:def_2_:_ for C being non empty set for f, b3 being Function of C,COMPLEX holds ( b3 = f *' iff ( dom b3 = C & ( for n being Element of C holds b3 . n = (f . n) *' ) ) ); registration let C be non empty set ; let s be complex-valued ManySortedSet of C; clusters *' -> C -defined complex-valued ; coherence s *' is C -defined proof dom s c= C ; hence dom (s *') c= C by Def1; :: according to RELAT_1:def_18 ::_thesis: verum end; end; registration let C be non empty set ; let seq be complex-valued ManySortedSet of C; clusterseq *' -> C -defined total for C -defined Function; coherence for b1 being C -defined Function st b1 = seq *' holds b1 is total proof let f be C -defined Function; ::_thesis: ( f = seq *' implies f is total ) assume A1: f = seq *' ; ::_thesis: f is total thus dom f = dom seq by Def1, A1 .= C by PARTFUN1:def_2 ; :: according to PARTFUN1:def_2 ::_thesis: verum end; end; theorem :: COMSEQ_2:3 for s being Complex_Sequence st s is non-zero holds s *' is non-zero proof let s be Complex_Sequence; ::_thesis: ( s is non-zero implies s *' is non-zero ) assume A1: s is non-zero ; ::_thesis: s *' is non-zero now__::_thesis:_for_n_being_Element_of_NAT_holds_(s_*')_._n_<>_0c let n be Element of NAT ; ::_thesis: (s *') . n <> 0c (s . n) *' <> 0c by A1, COMPLEX1:29; hence (s *') . n <> 0c by Def2; ::_thesis: verum end; hence s *' is non-zero by COMSEQ_1:4; ::_thesis: verum end; theorem :: COMSEQ_2:4 for r being Element of COMPLEX for s being Complex_Sequence holds (r (#) s) *' = (r *') (#) (s *') proof let r be Element of COMPLEX ; ::_thesis: for s being Complex_Sequence holds (r (#) s) *' = (r *') (#) (s *') let s be Complex_Sequence; ::_thesis: (r (#) s) *' = (r *') (#) (s *') now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_s)_*')_._n_=_((r_*')_(#)_(s_*'))_._n let n be Element of NAT ; ::_thesis: ((r (#) s) *') . n = ((r *') (#) (s *')) . n thus ((r (#) s) *') . n = ((r (#) s) . n) *' by Def2 .= (r * (s . n)) *' by VALUED_1:6 .= (r *') * ((s . n) *') by COMPLEX1:35 .= (r *') * ((s *') . n) by Def2 .= ((r *') (#) (s *')) . n by VALUED_1:6 ; ::_thesis: verum end; hence (r (#) s) *' = (r *') (#) (s *') by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_2:5 for s, s9 being Complex_Sequence holds (s (#) s9) *' = (s *') (#) (s9 *') proof let s, s9 be Complex_Sequence; ::_thesis: (s (#) s9) *' = (s *') (#) (s9 *') now__::_thesis:_for_n_being_Element_of_NAT_holds_((s_(#)_s9)_*')_._n_=_((s_*')_(#)_(s9_*'))_._n let n be Element of NAT ; ::_thesis: ((s (#) s9) *') . n = ((s *') (#) (s9 *')) . n thus ((s (#) s9) *') . n = ((s (#) s9) . n) *' by Def2 .= ((s . n) * (s9 . n)) *' by VALUED_1:5 .= ((s . n) *') * ((s9 . n) *') by COMPLEX1:35 .= ((s *') . n) * ((s9 . n) *') by Def2 .= ((s *') . n) * ((s9 *') . n) by Def2 .= ((s *') (#) (s9 *')) . n by VALUED_1:5 ; ::_thesis: verum end; hence (s (#) s9) *' = (s *') (#) (s9 *') by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_2:6 for s being Complex_Sequence holds (s *') " = (s ") *' proof let s be Complex_Sequence; ::_thesis: (s *') " = (s ") *' now__::_thesis:_for_n_being_Element_of_NAT_holds_((s_*')_")_._n_=_((s_")_*')_._n let n be Element of NAT ; ::_thesis: ((s *') ") . n = ((s ") *') . n thus ((s *') ") . n = ((s *') . n) " by VALUED_1:10 .= ((s . n) *') " by Def2 .= ((s . n) ") *' by COMPLEX1:36 .= ((s ") . n) *' by VALUED_1:10 .= ((s ") *') . n by Def2 ; ::_thesis: verum end; hence (s *') " = (s ") *' by FUNCT_2:63; ::_thesis: verum end; theorem :: COMSEQ_2:7 for s9, s being Complex_Sequence holds (s9 /" s) *' = (s9 *') /" (s *') proof let s9, s be Complex_Sequence; ::_thesis: (s9 /" s) *' = (s9 *') /" (s *') now__::_thesis:_for_n_being_Element_of_NAT_holds_((s9_/"_s)_*')_._n_=_((s9_*')_/"_(s_*'))_._n let n be Element of NAT ; ::_thesis: ((s9 /" s) *') . n = ((s9 *') /" (s *')) . n thus ((s9 /" s) *') . n = ((s9 (#) (s ")) . n) *' by Def2 .= ((s9 . n) * ((s ") . n)) *' by VALUED_1:5 .= ((s9 . n) * ((s . n) ")) *' by VALUED_1:10 .= ((s9 . n) *') * (((s . n) ") *') by COMPLEX1:35 .= ((s9 . n) *') * (((s . n) *') ") by COMPLEX1:36 .= ((s9 *') . n) * (((s . n) *') ") by Def2 .= ((s9 *') . n) * (((s *') . n) ") by Def2 .= ((s9 *') . n) * (((s *') ") . n) by VALUED_1:10 .= ((s9 *') /" (s *')) . n by VALUED_1:5 ; ::_thesis: verum end; hence (s9 /" s) *' = (s9 *') /" (s *') by FUNCT_2:63; ::_thesis: verum end; begin definition let f be complex-valued Function; attrf is bounded means :: COMSEQ_2:def 3 ex r being real number st for y being set st y in dom f holds abs (f . y) < r; end; :: deftheorem defines bounded COMSEQ_2:def_3_:_ for f being complex-valued Function holds ( f is bounded iff ex r being real number st for y being set st y in dom f holds abs (f . y) < r ); definition let s be Complex_Sequence; redefine attr s is bounded means :Def4: :: COMSEQ_2:def 4 ex r being Real st for n being Element of NAT holds |.(s . n).| < r; compatibility ( s is bounded iff ex r being Real st for n being Element of NAT holds |.(s . n).| < r ) proof thus ( s is bounded implies ex r being Real st for n being Element of NAT holds |.(s . n).| < r ) ::_thesis: ( ex r being Real st for n being Element of NAT holds |.(s . n).| < r implies s is bounded ) proof given r being real number such that A1: for y being set st y in dom s holds abs (s . y) < r ; :: according to COMSEQ_2:def_3 ::_thesis: ex r being Real st for n being Element of NAT holds |.(s . n).| < r reconsider r = r as Element of REAL by XREAL_0:def_1; take r ; ::_thesis: for n being Element of NAT holds |.(s . n).| < r let n be Element of NAT ; ::_thesis: |.(s . n).| < r n in NAT ; then n in dom s by FUNCT_2:def_1; hence |.(s . n).| < r by A1; ::_thesis: verum end; given r being Real such that A2: for n being Element of NAT holds |.(s . n).| < r ; ::_thesis: s is bounded take r ; :: according to COMSEQ_2:def_3 ::_thesis: for y being set st y in dom s holds abs (s . y) < r let y be set ; ::_thesis: ( y in dom s implies abs (s . y) < r ) assume y in dom s ; ::_thesis: abs (s . y) < r hence abs (s . y) < r by A2; ::_thesis: verum end; end; :: deftheorem Def4 defines bounded COMSEQ_2:def_4_:_ for s being Complex_Sequence holds ( s is bounded iff ex r being Real st for n being Element of NAT holds |.(s . n).| < r ); reconsider sc = NAT --> 0c as Complex_Sequence ; registration cluster Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued bounded for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is bounded proof take sc ; ::_thesis: sc is bounded take 1 ; :: according to COMSEQ_2:def_4 ::_thesis: for n being Element of NAT holds |.(sc . n).| < 1 let n be Element of NAT ; ::_thesis: |.(sc . n).| < 1 thus |.(sc . n).| < 1 by COMPLEX1:44, FUNCOP_1:7; ::_thesis: verum end; end; theorem Th8: :: COMSEQ_2:8 for s being Complex_Sequence holds ( s is bounded iff ex r being Real st ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) ) proof let s be Complex_Sequence; ::_thesis: ( s is bounded iff ex r being Real st ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) ) thus ( s is bounded implies ex r being Real st ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) ) ::_thesis: ( ex r being Real st ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) implies s is bounded ) proof assume s is bounded ; ::_thesis: ex r being Real st ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) then consider r being Real such that A1: for n being Element of NAT holds |.(s . n).| < r by Def4; take r ; ::_thesis: ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_r let n be Element of NAT ; ::_thesis: 0 < r 0 <= |.(s . n).| by COMPLEX1:46; hence 0 < r by A1; ::_thesis: verum end; hence ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) by A1; ::_thesis: verum end; thus ( ex r being Real st ( 0 < r & ( for n being Element of NAT holds |.(s . n).| < r ) ) implies s is bounded ) by Def4; ::_thesis: verum end; begin definition let s be complex-valued ManySortedSet of NAT ; attrs is convergent means :Def5: :: COMSEQ_2:def 5 ex g being Element of COMPLEX st 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 |.((s . m) - g).| < p; end; :: deftheorem Def5 defines convergent COMSEQ_2:def_5_:_ for s being complex-valued ManySortedSet of NAT holds ( s is convergent iff ex g being Element of COMPLEX st 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 |.((s . m) - g).| < p ); definition let s be Complex_Sequence; assume A1: s is convergent ; func lim s -> Element of COMPLEX means :Def6: :: COMSEQ_2:def 6 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 |.((s . m) - it).| < p; existence ex b1 being Element of COMPLEX st 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 |.((s . m) - b1).| < p by A1, Def5; uniqueness for b1, b2 being Element of COMPLEX st ( 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 |.((s . m) - b1).| < p ) & ( 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 |.((s . m) - b2).| < p ) holds b1 = b2 proof let g1, g2 be Element of COMPLEX ; ::_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 |.((s . m) - g1).| < p ) & ( 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 |.((s . m) - g2).| < p ) implies g1 = g2 ) assume that A2: for p being Real st 0 < p holds ex n1 being Element of NAT st for m being Element of NAT st n1 <= m holds |.((s . m) - g1).| < p and A3: for p being Real st 0 < p holds ex n2 being Element of NAT st for m being Element of NAT st n2 <= m holds |.((s . m) - g2).| < p and A4: g1 <> g2 ; ::_thesis: contradiction reconsider p = |.(g1 - g2).| / 2 as Real ; A5: |.(g1 - g2).| > 0 by A4, COMPLEX1:62; then consider n1 being Element of NAT such that A6: for m being Element of NAT st n1 <= m holds |.((s . m) - g1).| < p by A2; consider n2 being Element of NAT such that A7: for m being Element of NAT st n2 <= m holds |.((s . m) - g2).| < p by A3, A5; reconsider n = max (n1,n2) as Element of NAT by FINSEQ_2:1; for m being Element of NAT st n <= m holds 2 * p < 2 * p proof let m be Element of NAT ; ::_thesis: ( n <= m implies 2 * p < 2 * p ) assume A8: n <= m ; ::_thesis: 2 * p < 2 * p n2 <= n by XXREAL_0:25; then n + n2 <= n + m by A8, XREAL_1:7; then n2 <= m by XREAL_1:6; then A9: |.((s . m) - g2).| < p by A7; |.(g1 - g2).| = |.((g1 - (s . m)) - (g2 - (s . m))).| ; then |.(g1 - g2).| <= |.(g1 - (s . m)).| + |.(g2 - (s . m)).| by COMPLEX1:57; then A10: |.(g1 - g2).| <= |.((s . m) - g1).| + |.(g2 - (s . m)).| by COMPLEX1:60; n1 <= n by XXREAL_0:25; then n + n1 <= n + m by A8, XREAL_1:7; then n1 <= m by XREAL_1:6; then |.((s . m) - g1).| < p by A6; then |.((s . m) - g1).| + |.((s . m) - g2).| < p + p by A9, XREAL_1:8; hence 2 * p < 2 * p by A10, COMPLEX1:60; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; end; :: deftheorem Def6 defines lim COMSEQ_2:def_6_:_ for s being Complex_Sequence st s is convergent holds for b2 being Element of COMPLEX holds ( b2 = lim s 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 |.((s . m) - b2).| < p ); theorem Th9: :: COMSEQ_2:9 for s being Complex_Sequence st ex g being Element of COMPLEX st for n being Element of NAT holds s . n = g holds s is convergent proof let s be Complex_Sequence; ::_thesis: ( ex g being Element of COMPLEX st for n being Element of NAT holds s . n = g implies s is convergent ) given g being Element of COMPLEX such that A1: for n being Element of NAT holds s . n = g ; ::_thesis: s is convergent take g ; :: according to COMSEQ_2:def_5 ::_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 |.((s . m) - g).| < p now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_k_<=_n_holds_ |.((s_._n)_-_g).|_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for n being Element of NAT st k <= n holds |.((s . n) - g).| < p ) assume A2: 0 < p ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st k <= n holds |.((s . n) - g).| < p take k = 0 ; ::_thesis: for n being Element of NAT st k <= n holds |.((s . n) - g).| < p let n be Element of NAT ; ::_thesis: ( k <= n implies |.((s . n) - g).| < p ) assume k <= n ; ::_thesis: |.((s . n) - g).| < p s . n = g by A1; hence |.((s . n) - g).| < p by A2, COMPLEX1:44; ::_thesis: verum end; hence 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 |.((s . m) - g).| < p ; ::_thesis: verum end; theorem Th10: :: COMSEQ_2:10 for s being Complex_Sequence for g being Element of COMPLEX st ( for n being Element of NAT holds s . n = g ) holds lim s = g proof let s be Complex_Sequence; ::_thesis: for g being Element of COMPLEX st ( for n being Element of NAT holds s . n = g ) holds lim s = g let g be Element of COMPLEX ; ::_thesis: ( ( for n being Element of NAT holds s . n = g ) implies lim s = g ) assume A1: for n being Element of NAT holds s . n = g ; ::_thesis: lim s = g A2: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_k_<=_n_holds_ |.((s_._n)_-_g).|_<_p let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st for n being Element of NAT st k <= n holds |.((s . n) - g).| < p ) assume A3: 0 < p ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st k <= n holds |.((s . n) - g).| < p take k = 0 ; ::_thesis: for n being Element of NAT st k <= n holds |.((s . n) - g).| < p let n be Element of NAT ; ::_thesis: ( k <= n implies |.((s . n) - g).| < p ) assume k <= n ; ::_thesis: |.((s . n) - g).| < p s . n = g by A1; hence |.((s . n) - g).| < p by A3, COMPLEX1:44; ::_thesis: verum end; s is convergent by A1, Th9; hence lim s = g by A2, Def6; ::_thesis: verum end; Lm1: for n being Element of NAT holds sc . n = 0c by FUNCOP_1:7; registration cluster Relation-like NAT -defined COMPLEX -valued Function-like non empty total V18( NAT , COMPLEX ) complex-valued convergent for Element of K19(K20(NAT,COMPLEX)); existence ex b1 being Complex_Sequence st b1 is convergent by Lm1, Th9; end; registration let s be convergent Complex_Sequence; clusters *' -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s *' holds b1 is convergent proof let t be Complex_Sequence; ::_thesis: ( t = s *' implies t is convergent ) assume A1: t = s *' ; ::_thesis: t is convergent consider g being Element of COMPLEX such that 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 |.((s . m) - g).| < p by Def5; reconsider z = g *' as Element of COMPLEX ; take r = g *' ; :: according to COMSEQ_2:def_5 ::_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 |.((t . m) - r).| < 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 |.((t . m) - r).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((t . m) - r).| < p then consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds |.((s . m) - g).| < p by A2; take n ; ::_thesis: for m being Element of NAT st n <= m holds |.((t . m) - r).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((t . m) - r).| < p ) assume A4: n <= m ; ::_thesis: |.((t . m) - r).| < p |.(((s *') . m) - r).| = |.(((s . m) *') - (g *')).| by Def2 .= |.(((s . m) - g) *').| by COMPLEX1:34 .= |.((s . m) - g).| by COMPLEX1:53 ; hence |.((t . m) - r).| < p by A3, A4, A1; ::_thesis: verum end; end; theorem :: COMSEQ_2:11 canceled; theorem Th12: :: COMSEQ_2:12 for s being Complex_Sequence st s is convergent holds lim (s *') = (lim s) *' proof let s be Complex_Sequence; ::_thesis: ( s is convergent implies lim (s *') = (lim s) *' ) set g = lim s; assume A1: s is convergent ; ::_thesis: lim (s *') = (lim s) *' then reconsider s1 = s as convergent Complex_Sequence ; A2: 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_ |.(((s_*')_._m)_-_((lim_s)_*')).|_<_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 |.(((s *') . m) - ((lim s) *')).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((s *') . m) - ((lim s) *')).| < p then consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds |.((s . m) - (lim s)).| < p by A1, Def6; take n = n; ::_thesis: for m being Element of NAT st n <= m holds |.(((s *') . m) - ((lim s) *')).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s *') . m) - ((lim s) *')).| < p ) assume A4: n <= m ; ::_thesis: |.(((s *') . m) - ((lim s) *')).| < p |.(((s *') . m) - ((lim s) *')).| = |.(((s . m) *') - ((lim s) *')).| by Def2 .= |.(((s . m) - (lim s)) *').| by COMPLEX1:34 .= |.((s . m) - (lim s)).| by COMPLEX1:53 ; hence |.(((s *') . m) - ((lim s) *')).| < p by A3, A4; ::_thesis: verum end; s1 *' is convergent ; hence lim (s *') = (lim s) *' by A2, Def6; ::_thesis: verum end; begin registration let s1, s2 be convergent Complex_Sequence; clusters1 + s2 -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s1 + s2 holds b1 is convergent proof let s be Complex_Sequence; ::_thesis: ( s = s1 + s2 implies s is convergent ) assume A1: s = s1 + s2 ; ::_thesis: s is convergent consider g being Element of COMPLEX such that 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 |.((s1 . m) - g).| < p by Def5; consider g9 being Element of COMPLEX such that A3: 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 |.((s2 . m) - g9).| < p by Def5; take g1 = g + g9; :: according to COMSEQ_2:def_5 ::_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 |.((s . m) - g1).| < 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 |.((s . m) - g1).| < p ) assume A4: p > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - g1).| < p then consider n1 being Element of NAT such that A5: for m being Element of NAT st n1 <= m holds |.((s1 . m) - g).| < p / 2 by A2; consider n2 being Element of NAT such that A6: for m being Element of NAT st n2 <= m holds |.((s2 . m) - g9).| < p / 2 by A3, A4; reconsider n = max (n1,n2) as Element of NAT by FINSEQ_2:1; take n ; ::_thesis: for m being Element of NAT st n <= m holds |.((s . m) - g1).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((s . m) - g1).| < p ) assume A7: n <= m ; ::_thesis: |.((s . m) - g1).| < p n2 <= n by XXREAL_0:25; then n + n2 <= n + m by A7, XREAL_1:7; then n2 <= m by XREAL_1:6; then A8: |.((s2 . m) - g9).| < p / 2 by A6; A9: |.(((s1 + s2) . m) - g1).| = |.(((s1 . m) + (s2 . m)) - (g + g9)).| by VALUED_1:1 .= |.(((s1 . m) - g) + ((s2 . m) - g9)).| ; n1 <= n by XXREAL_0:25; then n + n1 <= n + m by A7, XREAL_1:7; then n1 <= m by XREAL_1:6; then |.((s1 . m) - g).| < p / 2 by A5; then |.((s1 . m) - g).| + |.((s2 . m) - g9).| < (p / 2) + (p / 2) by A8, XREAL_1:8; then (|.((s1 . m) - g).| + |.((s2 . m) - g9).|) + |.(((s1 + s2) . m) - g1).| < p + (|.((s1 . m) - g).| + |.((s2 . m) - g9).|) by A9, COMPLEX1:56, XREAL_1:8; hence |.((s . m) - g1).| < p by A1, XREAL_1:6; ::_thesis: verum end; end; theorem :: COMSEQ_2:13 canceled; theorem Th14: :: COMSEQ_2:14 for s, s9 being convergent Complex_Sequence holds lim (s + s9) = (lim s) + (lim s9) proof let s, s9 be convergent Complex_Sequence; ::_thesis: lim (s + s9) = (lim s) + (lim s9) 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 |.(((s + s9) . m) - ((lim s) + (lim s9))).| < 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 |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p then A1: 0 < p / 2 ; then consider n1 being Element of NAT such that A2: for m being Element of NAT st n1 <= m holds |.((s . m) - (lim s)).| < p / 2 by Def6; consider n2 being Element of NAT such that A3: for m being Element of NAT st n2 <= m holds |.((s9 . m) - (lim s9)).| < p / 2 by A1, Def6; reconsider n = max (n1,n2) as Element of NAT by FINSEQ_2:1; take n ; ::_thesis: for m being Element of NAT st n <= m holds |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p ) assume A4: n <= m ; ::_thesis: |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p n2 <= n by XXREAL_0:25; then n + n2 <= n + m by A4, XREAL_1:7; then n2 <= m by XREAL_1:6; then A5: |.((s9 . m) - (lim s9)).| < p / 2 by A3; A6: |.(((s + s9) . m) - ((lim s) + (lim s9))).| = |.(((s . m) + (s9 . m)) - ((lim s) + (lim s9))).| by VALUED_1:1 .= |.(((s . m) - (lim s)) + ((s9 . m) - (lim s9))).| ; n1 <= n by XXREAL_0:25; then n + n1 <= n + m by A4, XREAL_1:7; then n1 <= m by XREAL_1:6; then |.((s . m) - (lim s)).| < p / 2 by A2; then |.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).| < (p / 2) + (p / 2) by A5, XREAL_1:8; then (|.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).|) + |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p + (|.((s . m) - (lim s)).| + |.((s9 . m) - (lim s9)).|) by A6, COMPLEX1:56, XREAL_1:8; hence |.(((s + s9) . m) - ((lim s) + (lim s9))).| < p by XREAL_1:6; ::_thesis: verum end; hence lim (s + s9) = (lim s) + (lim s9) by Def6; ::_thesis: verum end; theorem :: COMSEQ_2:15 canceled; theorem :: COMSEQ_2:16 for s, s9 being convergent Complex_Sequence holds lim ((s + s9) *') = ((lim s) *') + ((lim s9) *') proof let s, s9 be convergent Complex_Sequence; ::_thesis: lim ((s + s9) *') = ((lim s) *') + ((lim s9) *') thus lim ((s + s9) *') = (lim (s + s9)) *' by Th12 .= ((lim s) + (lim s9)) *' by Th14 .= ((lim s) *') + ((lim s9) *') by COMPLEX1:32 ; ::_thesis: verum end; registration let s be convergent Complex_Sequence; let c be complex number ; clusterc (#) s -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = c (#) s holds b1 is convergent proof A1: now__::_thesis:_for_c_being_Element_of_COMPLEX_holds_c_(#)_s_is_convergent let c be Element of COMPLEX ; ::_thesis: b1 (#) s is convergent percases ( c = 0c or c <> 0c ) ; supposeA2: c = 0c ; ::_thesis: b1 (#) s is convergent now__::_thesis:_for_n_being_Element_of_NAT_holds_(c_(#)_s)_._n_=_0c let n be Element of NAT ; ::_thesis: (c (#) s) . n = 0c thus (c (#) s) . n = 0c * (s . n) by A2, VALUED_1:6 .= 0c ; ::_thesis: verum end; hence c (#) s is convergent by Th9; ::_thesis: verum end; supposeA3: c <> 0c ; ::_thesis: b1 (#) s is convergent thus c (#) s is convergent ::_thesis: verum proof consider g being Element of COMPLEX such that A4: 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 |.((s . m) - g).| < p by Def5; take g9 = c * g; :: according to COMSEQ_2:def_5 ::_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 |.(((c (#) s) . m) - g9).| < 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 |.(((c (#) s) . m) - g9).| < p ) assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((c (#) s) . m) - g9).| < p A6: |.c.| > 0 by A3, COMPLEX1:47; consider n being Element of NAT such that A7: for m being Element of NAT st n <= m holds |.((s . m) - g).| < p / |.c.| by A6, A4, A5; take n ; ::_thesis: for m being Element of NAT st n <= m holds |.(((c (#) s) . m) - g9).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((c (#) s) . m) - g9).| < p ) assume n <= m ; ::_thesis: |.(((c (#) s) . m) - g9).| < p then |.((s . m) - g).| < p / |.c.| by A7; then |.((s . m) - g).| * |.c.| < (p / |.c.|) * |.c.| by A6, XREAL_1:68; then |.((s . m) - g).| * |.c.| < (p * (|.c.| ")) * |.c.| by XCMPLX_0:def_9; then |.((s . m) - g).| * |.c.| < p * ((|.c.| ") * |.c.|) ; then A8: |.((s . m) - g).| * |.c.| < p * 1 by A6, XCMPLX_0:def_7; |.(((c (#) s) . m) - g9).| = |.((c * (s . m)) - (c * g)).| by VALUED_1:6 .= |.(c * ((s . m) - g)).| .= |.((s . m) - g).| * |.c.| by COMPLEX1:65 ; hence |.(((c (#) s) . m) - g9).| < p by A8; ::_thesis: verum end; end; end; end; c in COMPLEX by XCMPLX_0:def_2; hence for b1 being Complex_Sequence st b1 = c (#) s holds b1 is convergent by A1; ::_thesis: verum end; end; theorem :: COMSEQ_2:17 canceled; theorem Th18: :: COMSEQ_2:18 for s being convergent Complex_Sequence for r being complex number holds lim (r (#) s) = r * (lim s) proof let s be convergent Complex_Sequence; ::_thesis: for r being complex number holds lim (r (#) s) = r * (lim s) let r be complex number ; ::_thesis: lim (r (#) s) = r * (lim s) reconsider r = r as Element of COMPLEX by XCMPLX_0:def_2; percases ( r <> 0c or r = 0c ) ; supposeA1: r <> 0c ; ::_thesis: lim (r (#) s) = r * (lim s) for p being Real st p > 0 holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((r (#) s) . m) - (r * (lim s))).| < p proof let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((r (#) s) . m) - (r * (lim s))).| < p ) assume A2: p > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((r (#) s) . m) - (r * (lim s))).| < p A3: |.r.| > 0 by A1, COMPLEX1:47; p / |.r.| > 0 by A3, A2; then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds |.((s . m) - (lim s)).| < p / |.r.| by Def6; take n ; ::_thesis: for m being Element of NAT st n <= m holds |.(((r (#) s) . m) - (r * (lim s))).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((r (#) s) . m) - (r * (lim s))).| < p ) assume n <= m ; ::_thesis: |.(((r (#) s) . m) - (r * (lim s))).| < p then |.((s . m) - (lim s)).| < p / |.r.| by A4; then |.((s . m) - (lim s)).| * |.r.| < (p / |.r.|) * |.r.| by A3, XREAL_1:68; then |.((s . m) - (lim s)).| * |.r.| < (p * (|.r.| ")) * |.r.| by XCMPLX_0:def_9; then |.((s . m) - (lim s)).| * |.r.| < p * ((|.r.| ") * |.r.|) ; then A5: |.((s . m) - (lim s)).| * |.r.| < p * 1 by A3, XCMPLX_0:def_7; |.(((r (#) s) . m) - (r * (lim s))).| = |.((r * (s . m)) - (r * (lim s))).| by VALUED_1:6 .= |.(r * ((s . m) - (lim s))).| .= |.((s . m) - (lim s)).| * |.r.| by COMPLEX1:65 ; hence |.(((r (#) s) . m) - (r * (lim s))).| < p by A5; ::_thesis: verum end; hence lim (r (#) s) = r * (lim s) by Def6; ::_thesis: verum end; supposeA6: r = 0c ; ::_thesis: lim (r (#) s) = r * (lim s) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_s)_._n_=_0c let n be Element of NAT ; ::_thesis: (r (#) s) . n = 0c thus (r (#) s) . n = 0c * (s . n) by A6, VALUED_1:6 .= 0c ; ::_thesis: verum end; hence lim (r (#) s) = r * (lim s) by A6, Th10; ::_thesis: verum end; end; end; theorem :: COMSEQ_2:19 canceled; theorem :: COMSEQ_2:20 for r being Element of COMPLEX for s being convergent Complex_Sequence holds lim ((r (#) s) *') = (r *') * ((lim s) *') proof let r be Element of COMPLEX ; ::_thesis: for s being convergent Complex_Sequence holds lim ((r (#) s) *') = (r *') * ((lim s) *') let s be convergent Complex_Sequence; ::_thesis: lim ((r (#) s) *') = (r *') * ((lim s) *') thus lim ((r (#) s) *') = (lim (r (#) s)) *' by Th12 .= (r * (lim s)) *' by Th18 .= (r *') * ((lim s) *') by COMPLEX1:35 ; ::_thesis: verum end; registration let s be convergent Complex_Sequence; cluster - s -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = - s holds b1 is convergent ; end; theorem :: COMSEQ_2:21 canceled; theorem Th22: :: COMSEQ_2:22 for s being convergent Complex_Sequence holds lim (- s) = - (lim s) proof let s be convergent Complex_Sequence; ::_thesis: lim (- s) = - (lim s) lim (- s) = (- 1) * (lim s) by Th18 .= - (1r * (lim s)) by COMPLEX1:def_4 ; hence lim (- s) = - (lim s) by COMPLEX1:def_4; ::_thesis: verum end; theorem :: COMSEQ_2:23 canceled; theorem :: COMSEQ_2:24 for s being convergent Complex_Sequence holds lim ((- s) *') = - ((lim s) *') proof let s be convergent Complex_Sequence; ::_thesis: lim ((- s) *') = - ((lim s) *') thus lim ((- s) *') = (lim (- s)) *' by Th12 .= (- (lim s)) *' by Th22 .= - ((lim s) *') by COMPLEX1:33 ; ::_thesis: verum end; registration let s1, s2 be convergent Complex_Sequence; clusters1 - s2 -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s1 - s2 holds b1 is convergent proof - s2 is convergent ; hence for b1 being Complex_Sequence st b1 = s1 - s2 holds b1 is convergent ; ::_thesis: verum end; end; theorem :: COMSEQ_2:25 canceled; theorem Th26: :: COMSEQ_2:26 for s, s9 being convergent Complex_Sequence holds lim (s - s9) = (lim s) - (lim s9) proof let s, s9 be convergent Complex_Sequence; ::_thesis: lim (s - s9) = (lim s) - (lim s9) lim (s - s9) = (lim s) + (lim (- s9)) by Th14 .= (lim s) + (- (lim s9)) by Th22 ; hence lim (s - s9) = (lim s) - (lim s9) ; ::_thesis: verum end; theorem :: COMSEQ_2:27 canceled; theorem :: COMSEQ_2:28 for s, s9 being convergent Complex_Sequence holds lim ((s - s9) *') = ((lim s) *') - ((lim s9) *') proof let s, s9 be convergent Complex_Sequence; ::_thesis: lim ((s - s9) *') = ((lim s) *') - ((lim s9) *') thus lim ((s - s9) *') = (lim (s - s9)) *' by Th12 .= ((lim s) - (lim s9)) *' by Th26 .= ((lim s) *') - ((lim s9) *') by COMPLEX1:34 ; ::_thesis: verum end; registration cluster Function-like V18( NAT , COMPLEX ) convergent -> bounded for Element of K19(K20(NAT,COMPLEX)); coherence for b1 being Complex_Sequence st b1 is convergent holds b1 is bounded proof let s be Complex_Sequence; ::_thesis: ( s is convergent implies s is bounded ) assume s is convergent ; ::_thesis: s is bounded then consider g being Element of COMPLEX such that A1: 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 |.((s . m) - g).| < p by Def5; consider n1 being Element of NAT such that A2: for m being Element of NAT st n1 <= m holds |.((s . m) - g).| < 1 by A1; now__::_thesis:_ex_R_being_Element_of_REAL_st_ (_0_<_R_&_(_for_m_being_Element_of_NAT_st_n1_<=_m_holds_ |.(s_._m).|_<_R_)_) take R = |.g.| + 1; ::_thesis: ( 0 < R & ( for m being Element of NAT st n1 <= m holds |.(s . m).| < R ) ) 0 + 0 < R by COMPLEX1:46, XREAL_1:8; hence 0 < R ; ::_thesis: for m being Element of NAT st n1 <= m holds |.(s . m).| < R let m be Element of NAT ; ::_thesis: ( n1 <= m implies |.(s . m).| < R ) A3: (|.(s . m).| - |.g.|) + |.g.| = |.(s . m).| ; assume n1 <= m ; ::_thesis: |.(s . m).| < R then A4: |.((s . m) - g).| < 1 by A2; |.(s . m).| - |.g.| <= |.((s . m) - g).| by COMPLEX1:59; then |.(s . m).| - |.g.| < 1 by A4, XXREAL_0:2; hence |.(s . m).| < R by A3, XREAL_1:6; ::_thesis: verum end; then consider R1 being real number such that A5: 0 < R1 and A6: for m being Element of NAT st n1 <= m holds |.(s . m).| < R1 ; consider R2 being Real such that A7: 0 < R2 and A8: for m being Element of NAT st m <= n1 holds |.(s . m).| < R2 by Th2; take R = R1 + R2; :: according to COMSEQ_2:def_4 ::_thesis: for n being Element of NAT holds |.(s . n).| < R let m be Element of NAT ; ::_thesis: |.(s . m).| < R A9: R2 + 0 < R by A5, XREAL_1:8; A10: now__::_thesis:_(_m_<=_n1_implies_|.(s_._m).|_<_R_) assume m <= n1 ; ::_thesis: |.(s . m).| < R then |.(s . m).| < R2 by A8; hence |.(s . m).| < R by A9, XXREAL_0:2; ::_thesis: verum end; A11: R1 + 0 < R by A7, XREAL_1:8; now__::_thesis:_(_n1_<=_m_implies_|.(s_._m).|_<_R_) assume n1 <= m ; ::_thesis: |.(s . m).| < R then |.(s . m).| < R1 by A6; hence |.(s . m).| < R by A11, XXREAL_0:2; ::_thesis: verum end; hence |.(s . m).| < R by A10; ::_thesis: verum end; end; registration cluster Function-like V18( NAT , COMPLEX ) non bounded -> non convergent for Element of K19(K20(NAT,COMPLEX)); coherence for b1 being Complex_Sequence st not b1 is bounded holds not b1 is convergent ; end; registration let s1, s2 be convergent Complex_Sequence; clusters1 (#) s2 -> convergent for Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s1 (#) s2 holds b1 is convergent proof let s be Complex_Sequence; ::_thesis: ( s = s1 (#) s2 implies s is convergent ) assume A1: s = s1 (#) s2 ; ::_thesis: s is convergent consider g1 being Element of COMPLEX such that 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 |.((s1 . m) - g1).| < p by Def5; consider g2 being Element of COMPLEX such that A3: 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 |.((s2 . m) - g2).| < p by Def5; take g = g1 * g2; :: according to COMSEQ_2:def_5 ::_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 |.((s . m) - g).| < 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 |.((s . m) - g).| < p ) consider R being Real such that A4: 0 < R and A5: for n being Element of NAT holds |.(s1 . n).| < R by Th8; A6: 0 + 0 < |.g2.| + R by A4, COMPLEX1:46, XREAL_1:8; assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.((s . m) - g).| < p then consider n1 being Element of NAT such that A8: for m being Element of NAT st n1 <= m holds |.((s1 . m) - g1).| < p / (|.g2.| + R) by A2, A6; consider n2 being Element of NAT such that A9: for m being Element of NAT st n2 <= m holds |.((s2 . m) - g2).| < p / (|.g2.| + R) by A3, A6, A7; take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds |.((s . m) - g).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.((s . m) - g).| < p ) assume A10: n <= m ; ::_thesis: |.((s . m) - g).| < p n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A10, XXREAL_0:2; then A11: |.((s1 . m) - g1).| <= p / (|.g2.| + R) by A8; ( 0 <= |.g2.| & |.(((s1 . m) - g1) * g2).| = |.g2.| * |.((s1 . m) - g1).| ) by COMPLEX1:46, COMPLEX1:65; then A12: |.(((s1 . m) - g1) * g2).| <= |.g2.| * (p / (|.g2.| + R)) by A11, XREAL_1:64; |.(((s1 (#) s2) . m) - g).| = |.(((((s1 . m) * (s2 . m)) - ((s1 . m) * g2)) + ((s1 . m) * g2)) - (g1 * g2)).| by VALUED_1:5 .= |.(((s1 . m) * ((s2 . m) - g2)) + (((s1 . m) - g1) * g2)).| ; then A13: |.(((s1 (#) s2) . m) - g).| <= |.((s1 . m) * ((s2 . m) - g2)).| + |.(((s1 . m) - g1) * g2).| by COMPLEX1:56; n2 <= n by NAT_1:12; then n2 <= m by A10, XXREAL_0:2; then A14: |.((s2 . m) - g2).| < p / (|.g2.| + R) by A9; A15: ( 0 <= |.(s1 . m).| & 0 <= |.((s2 . m) - g2).| ) by COMPLEX1:46; |.(s1 . m).| < R by A5; then |.(s1 . m).| * |.((s2 . m) - g2).| < R * (p / (|.g2.| + R)) by A15, A14, XREAL_1:96; then A16: |.((s1 . m) * ((s2 . m) - g2)).| < R * (p / (|.g2.| + R)) by COMPLEX1:65; (R * (p / (|.g2.| + R))) + (|.g2.| * (p / (|.g2.| + R))) = (p / (|.g2.| + R)) * (|.g2.| + R) .= p by A6, XCMPLX_1:87 ; then |.((s1 . m) * ((s2 . m) - g2)).| + |.(((s1 . m) - g1) * g2).| < p by A16, A12, XREAL_1:8; hence |.((s . m) - g).| < p by A1, A13, XXREAL_0:2; ::_thesis: verum end; end; theorem :: COMSEQ_2:29 canceled; theorem Th30: :: COMSEQ_2:30 for s, s9 being convergent Complex_Sequence holds lim (s (#) s9) = (lim s) * (lim s9) proof let s, s9 be convergent Complex_Sequence; ::_thesis: lim (s (#) s9) = (lim s) * (lim s9) consider R being Real such that A1: 0 < R and A2: for n being Element of NAT holds |.(s . n).| < R by Th8; A3: 0 + 0 < |.(lim s9).| + R by A1, COMPLEX1:46, XREAL_1:8; A4: 0 <= |.(lim s9).| by COMPLEX1:46; 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_ |.(((s_(#)_s9)_._m)_-_((lim_s)_*_(lim_s9))).|_<_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 |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p then A5: 0 < p / (|.(lim s9).| + R) by A3; then consider n1 being Element of NAT such that A6: for m being Element of NAT st n1 <= m holds |.((s . m) - (lim s)).| < p / (|.(lim s9).| + R) by Def6; consider n2 being Element of NAT such that A7: for m being Element of NAT st n2 <= m holds |.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A5, Def6; take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p ) assume A8: n <= m ; ::_thesis: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A8, XXREAL_0:2; then A9: |.((s . m) - (lim s)).| <= p / (|.(lim s9).| + R) by A6; |.(((s . m) - (lim s)) * (lim s9)).| = |.(lim s9).| * |.((s . m) - (lim s)).| by COMPLEX1:65; then A10: |.(((s . m) - (lim s)) * (lim s9)).| <= |.(lim s9).| * (p / (|.(lim s9).| + R)) by A4, A9, XREAL_1:64; A11: ( 0 <= |.(s . m).| & 0 <= |.((s9 . m) - (lim s9)).| ) by COMPLEX1:46; n2 <= n by NAT_1:12; then n2 <= m by A8, XXREAL_0:2; then A12: |.((s9 . m) - (lim s9)).| < p / (|.(lim s9).| + R) by A7; |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| = |.(((((s . m) * (s9 . m)) - ((s . m) * (lim s9))) + ((s . m) * (lim s9))) - ((lim s) * (lim s9))).| by VALUED_1:5 .= |.(((s . m) * ((s9 . m) - (lim s9))) + (((s . m) - (lim s)) * (lim s9))).| ; then A13: |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| <= |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| by COMPLEX1:56; |.(s . m).| < R by A2; then |.(s . m).| * |.((s9 . m) - (lim s9)).| < R * (p / (|.(lim s9).| + R)) by A11, A12, XREAL_1:96; then A14: |.((s . m) * ((s9 . m) - (lim s9))).| < R * (p / (|.(lim s9).| + R)) by COMPLEX1:65; (R * (p / (|.(lim s9).| + R))) + (|.(lim s9).| * (p / (|.(lim s9).| + R))) = (p / (|.(lim s9).| + R)) * (|.(lim s9).| + R) .= p by A3, XCMPLX_1:87 ; then |.((s . m) * ((s9 . m) - (lim s9))).| + |.(((s . m) - (lim s)) * (lim s9)).| < p by A14, A10, XREAL_1:8; hence |.(((s (#) s9) . m) - ((lim s) * (lim s9))).| < p by A13, XXREAL_0:2; ::_thesis: verum end; hence lim (s (#) s9) = (lim s) * (lim s9) by Def6; ::_thesis: verum end; theorem :: COMSEQ_2:31 canceled; theorem :: COMSEQ_2:32 for s, s9 being convergent Complex_Sequence holds lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *') proof let s, s9 be convergent Complex_Sequence; ::_thesis: lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *') thus lim ((s (#) s9) *') = (lim (s (#) s9)) *' by Th12 .= ((lim s) * (lim s9)) *' by Th30 .= ((lim s) *') * ((lim s9) *') by COMPLEX1:35 ; ::_thesis: verum end; theorem Th33: :: COMSEQ_2:33 for s being convergent Complex_Sequence st lim s <> 0c holds ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(lim s).| / 2 < |.(s . m).| proof let s be convergent Complex_Sequence; ::_thesis: ( lim s <> 0c implies ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(lim s).| / 2 < |.(s . m).| ) assume A1: lim s <> 0c ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(lim s).| / 2 < |.(s . m).| 0 < |.(lim s).| by A1, COMPLEX1:47; then 0 < |.(lim s).| / 2 ; then consider n1 being Element of NAT such that A2: for m being Element of NAT st n1 <= m holds |.((s . m) - (lim s)).| < |.(lim s).| / 2 by Def6; take n = n1; ::_thesis: for m being Element of NAT st n <= m holds |.(lim s).| / 2 < |.(s . m).| let m be Element of NAT ; ::_thesis: ( n <= m implies |.(lim s).| / 2 < |.(s . m).| ) assume n <= m ; ::_thesis: |.(lim s).| / 2 < |.(s . m).| then A3: |.((s . m) - (lim s)).| < |.(lim s).| / 2 by A2; A4: |.((lim s) - (s . m)).| = |.(- ((s . m) - (lim s))).| .= |.((s . m) - (lim s)).| by COMPLEX1:52 ; A5: ( (|.(lim s).| / 2) + (|.(s . m).| - (|.(lim s).| / 2)) = |.(s . m).| & (|.(lim s).| - |.(s . m).|) + (|.(s . m).| - (|.(lim s).| / 2)) = |.(lim s).| / 2 ) ; |.(lim s).| - |.(s . m).| <= |.((lim s) - (s . m)).| by COMPLEX1:59; then |.(lim s).| - |.(s . m).| < |.(lim s).| / 2 by A3, A4, XXREAL_0:2; hence |.(lim s).| / 2 < |.(s . m).| by A5, XREAL_1:6; ::_thesis: verum end; theorem Th34: :: COMSEQ_2:34 for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds s " is convergent proof let s be convergent Complex_Sequence; ::_thesis: ( lim s <> 0c & s is non-zero implies s " is convergent ) assume that A1: lim s <> 0c and A2: s is non-zero ; ::_thesis: s " is convergent consider n1 being Element of NAT such that A3: for m being Element of NAT st n1 <= m holds |.(lim s).| / 2 < |.(s . m).| by A1, Th33; take (lim s) " ; :: according to COMSEQ_2:def_5 ::_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 |.(((s ") . m) - ((lim s) ")).| < 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 |.(((s ") . m) - ((lim s) ")).| < p ) assume A4: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((s ") . m) - ((lim s) ")).| < p A5: 0 < |.(lim s).| by A1, COMPLEX1:47; then 0 * 0 < |.(lim s).| * |.(lim s).| ; then 0 < (|.(lim s).| * |.(lim s).|) / 2 ; then 0 * 0 < p * ((|.(lim s).| * |.(lim s).|) / 2) by A4; then consider n2 being Element of NAT such that A6: for m being Element of NAT st n2 <= m holds |.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by Def6; take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds |.(((s ") . m) - ((lim s) ")).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s ") . m) - ((lim s) ")).| < p ) assume A7: n <= m ; ::_thesis: |.(((s ") . m) - ((lim s) ")).| < p n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A7, XXREAL_0:2; then A8: |.(lim s).| / 2 < |.(s . m).| by A3; A9: 0 < |.(lim s).| / 2 by A5; then 0 * 0 < p * (|.(lim s).| / 2) by A4; then A10: (p * (|.(lim s).| / 2)) / |.(s . m).| < (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) by A8, A9, XREAL_1:76; A11: 0 <> |.(lim s).| / 2 by A1, COMPLEX1:47; A12: (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) = (p * (|.(lim s).| / 2)) * ((|.(lim s).| / 2) ") by XCMPLX_0:def_9 .= p * ((|.(lim s).| / 2) * ((|.(lim s).| / 2) ")) .= p * 1 by A11, XCMPLX_0:def_7 .= p ; A13: 0 <> |.(lim s).| by A1, COMPLEX1:47; A14: (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) = (p * ((2 ") * (|.(lim s).| * |.(lim s).|))) * ((|.(s . m).| * |.(lim s).|) ") by XCMPLX_0:def_9 .= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| * |.(s . m).|) ")) .= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| ") * (|.(s . m).| "))) by XCMPLX_1:204 .= (p * (2 ")) * ((|.(lim s).| * (|.(lim s).| * (|.(lim s).| "))) * (|.(s . m).| ")) .= (p * (2 ")) * ((|.(lim s).| * 1) * (|.(s . m).| ")) by A13, XCMPLX_0:def_7 .= (p * (|.(lim s).| / 2)) * (|.(s . m).| ") .= (p * (|.(lim s).| / 2)) / |.(s . m).| by XCMPLX_0:def_9 ; (s . m) * (lim s) <> 0c by A1, A2; then 0 < |.((s . m) * (lim s)).| by COMPLEX1:47; then A15: 0 < |.(s . m).| * |.(lim s).| by COMPLEX1:65; n2 <= n by NAT_1:12; then n2 <= m by A7, XXREAL_0:2; then |.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A6; then A16: |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) < (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) by A15, XREAL_1:74; |.(((s ") . m) - ((lim s) ")).| = |.(((s . m) ") - ((lim s) ")).| by VALUED_1:10 .= |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) by A1, A2, Th1 ; hence |.(((s ") . m) - ((lim s) ")).| < p by A16, A14, A10, A12, XXREAL_0:2; ::_thesis: verum end; theorem Th35: :: COMSEQ_2:35 for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds lim (s ") = (lim s) " proof let s be Complex_Sequence; ::_thesis: ( s is convergent & lim s <> 0c & s is non-zero implies lim (s ") = (lim s) " ) assume that A1: s is convergent and A2: lim s <> 0c and A3: s is non-zero ; ::_thesis: lim (s ") = (lim s) " consider n1 being Element of NAT such that A4: for m being Element of NAT st n1 <= m holds |.(lim s).| / 2 < |.(s . m).| by A1, A2, Th33; A5: 0 < |.(lim s).| by A2, COMPLEX1:47; then 0 * 0 < |.(lim s).| * |.(lim s).| ; then A6: 0 < (|.(lim s).| * |.(lim s).|) / 2 ; A7: 0 <> |.(lim s).| by A2, COMPLEX1:47; A8: 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_ |.(((s_")_._m)_-_((lim_s)_")).|_<_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 |.(((s ") . m) - ((lim s) ")).| < p ) A9: 0 <> |.(lim s).| / 2 by A2, COMPLEX1:47; A10: (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) = (p * (|.(lim s).| / 2)) * ((|.(lim s).| / 2) ") by XCMPLX_0:def_9 .= p * ((|.(lim s).| / 2) * ((|.(lim s).| / 2) ")) .= p * 1 by A9, XCMPLX_0:def_7 .= p ; assume A11: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((s ") . m) - ((lim s) ")).| < p then 0 * 0 < p * ((|.(lim s).| * |.(lim s).|) / 2) by A6; then consider n2 being Element of NAT such that A12: for m being Element of NAT st n2 <= m holds |.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A1, Def6; take n = n1 + n2; ::_thesis: for m being Element of NAT st n <= m holds |.(((s ") . m) - ((lim s) ")).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s ") . m) - ((lim s) ")).| < p ) assume A13: n <= m ; ::_thesis: |.(((s ") . m) - ((lim s) ")).| < p n1 <= n1 + n2 by NAT_1:12; then n1 <= m by A13, XXREAL_0:2; then A14: |.(lim s).| / 2 < |.(s . m).| by A4; A15: 0 < |.(lim s).| / 2 by A5; then 0 * 0 < p * (|.(lim s).| / 2) by A11; then A16: (p * (|.(lim s).| / 2)) / |.(s . m).| < (p * (|.(lim s).| / 2)) / (|.(lim s).| / 2) by A14, A15, XREAL_1:76; A17: (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) = (p * ((2 ") * (|.(lim s).| * |.(lim s).|))) * ((|.(s . m).| * |.(lim s).|) ") by XCMPLX_0:def_9 .= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| * |.(s . m).|) ")) .= (p * (2 ")) * ((|.(lim s).| * |.(lim s).|) * ((|.(lim s).| ") * (|.(s . m).| "))) by XCMPLX_1:204 .= (p * (2 ")) * ((|.(lim s).| * (|.(lim s).| * (|.(lim s).| "))) * (|.(s . m).| ")) .= (p * (2 ")) * ((|.(lim s).| * 1) * (|.(s . m).| ")) by A7, XCMPLX_0:def_7 .= (p * (|.(lim s).| / 2)) * (|.(s . m).| ") .= (p * (|.(lim s).| / 2)) / |.(s . m).| by XCMPLX_0:def_9 ; (s . m) * (lim s) <> 0c by A2, A3; then 0 < |.((s . m) * (lim s)).| by COMPLEX1:47; then A18: 0 < |.(s . m).| * |.(lim s).| by COMPLEX1:65; n2 <= n by NAT_1:12; then n2 <= m by A13, XXREAL_0:2; then |.((s . m) - (lim s)).| < p * ((|.(lim s).| * |.(lim s).|) / 2) by A12; then A19: |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) < (p * ((|.(lim s).| * |.(lim s).|) / 2)) / (|.(s . m).| * |.(lim s).|) by A18, XREAL_1:74; |.(((s ") . m) - ((lim s) ")).| = |.(((s . m) ") - ((lim s) ")).| by VALUED_1:10 .= |.((s . m) - (lim s)).| / (|.(s . m).| * |.(lim s).|) by A2, A3, Th1 ; hence |.(((s ") . m) - ((lim s) ")).| < p by A19, A17, A16, A10, XXREAL_0:2; ::_thesis: verum end; s " is convergent by A1, A2, A3, Th34; hence lim (s ") = (lim s) " by A8, Def6; ::_thesis: verum end; theorem :: COMSEQ_2:36 canceled; theorem :: COMSEQ_2:37 for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds lim ((s ") *') = ((lim s) *') " proof let s be Complex_Sequence; ::_thesis: ( s is convergent & lim s <> 0c & s is non-zero implies lim ((s ") *') = ((lim s) *') " ) assume A1: ( s is convergent & lim s <> 0c & s is non-zero ) ; ::_thesis: lim ((s ") *') = ((lim s) *') " then s " is convergent by Th34; hence lim ((s ") *') = (lim (s ")) *' by Th12 .= ((lim s) ") *' by A1, Th35 .= ((lim s) *') " by COMPLEX1:36 ; ::_thesis: verum end; theorem Th38: :: COMSEQ_2:38 for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds s9 /" s is convergent proof let s9, s be Complex_Sequence; ::_thesis: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero implies s9 /" s is convergent ) assume that A1: s9 is convergent and A2: ( s is convergent & lim s <> 0c & s is non-zero ) ; ::_thesis: s9 /" s is convergent s " is convergent by A2, Th34; hence s9 /" s is convergent by A1; ::_thesis: verum end; theorem Th39: :: COMSEQ_2:39 for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds lim (s9 /" s) = (lim s9) / (lim s) proof let s9, s be Complex_Sequence; ::_thesis: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero implies lim (s9 /" s) = (lim s9) / (lim s) ) assume that A1: s9 is convergent and A2: ( s is convergent & lim s <> 0c & s is non-zero ) ; ::_thesis: lim (s9 /" s) = (lim s9) / (lim s) s " is convergent by A2, Th34; then lim (s9 (#) (s ")) = (lim s9) * (lim (s ")) by A1, Th30 .= (lim s9) * ((lim s) ") by A2, Th35 .= (lim s9) / (lim s) by XCMPLX_0:def_9 ; hence lim (s9 /" s) = (lim s9) / (lim s) ; ::_thesis: verum end; theorem :: COMSEQ_2:40 canceled; theorem :: COMSEQ_2:41 for s9, s being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *') proof let s9, s be Complex_Sequence; ::_thesis: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero implies lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *') ) assume A1: ( s9 is convergent & s is convergent & lim s <> 0c & s is non-zero ) ; ::_thesis: lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *') then s9 /" s is convergent by Th38; hence lim ((s9 /" s) *') = (lim (s9 /" s)) *' by Th12 .= ((lim s9) / (lim s)) *' by A1, Th39 .= ((lim s9) *') / ((lim s) *') by COMPLEX1:37 ; ::_thesis: verum end; theorem Th42: :: COMSEQ_2:42 for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds s (#) s1 is convergent proof let s, s1 be Complex_Sequence; ::_thesis: ( s is convergent & s1 is bounded & lim s = 0c implies s (#) s1 is convergent ) assume that A1: s is convergent and A2: s1 is bounded and A3: lim s = 0c ; ::_thesis: s (#) s1 is convergent take g = 0c ; :: according to COMSEQ_2:def_5 ::_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 |.(((s (#) s1) . m) - g).| < p consider R being Real such that A4: 0 < R and A5: for m being Element of NAT holds |.(s1 . m).| < R by A2, Th8; 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 |.(((s (#) s1) . 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 |.(((s (#) s1) . m) - g).| < p A7: 0 < p / R by A6, A4; then consider n1 being Element of NAT such that A8: for m being Element of NAT st n1 <= m holds |.((s . m) - 0c).| < p / R by A1, A3, Def6; take n = n1; ::_thesis: for m being Element of NAT st n <= m holds |.(((s (#) s1) . m) - g).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s (#) s1) . m) - g).| < p ) assume A9: n <= m ; ::_thesis: |.(((s (#) s1) . m) - g).| < p A10: |.(((s (#) s1) . m) - g).| = |.((s . m) * (s1 . m)).| by VALUED_1:5 .= |.(s . m).| * |.(s1 . m).| by COMPLEX1:65 ; |.(s . m).| = |.((s . m) - 0c).| ; then A11: |.(s . m).| < p / R by A8, A9; now__::_thesis:_(_|.(s1_._m).|_<>_0_implies_|.(((s_(#)_s1)_._m)_-_g).|_<_p_) (p / R) * R = (p * (R ")) * R by XCMPLX_0:def_9 .= p * ((R ") * R) .= p * 1 by A4, XCMPLX_0:def_7 .= p ; then A12: (p / R) * |.(s1 . m).| < p by A5, A7, XREAL_1:68; A13: 0 <= |.(s1 . m).| by COMPLEX1:46; assume |.(s1 . m).| <> 0 ; ::_thesis: |.(((s (#) s1) . m) - g).| < p then |.(((s (#) s1) . m) - g).| < (p / R) * |.(s1 . m).| by A11, A10, A13, XREAL_1:68; hence |.(((s (#) s1) . m) - g).| < p by A12, XXREAL_0:2; ::_thesis: verum end; hence |.(((s (#) s1) . m) - g).| < p by A6, A10; ::_thesis: verum end; theorem Th43: :: COMSEQ_2:43 for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds lim (s (#) s1) = 0c proof let s, s1 be Complex_Sequence; ::_thesis: ( s is convergent & s1 is bounded & lim s = 0c implies lim (s (#) s1) = 0c ) assume that A1: s is convergent and A2: s1 is bounded and A3: lim s = 0c ; ::_thesis: lim (s (#) s1) = 0c A4: 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_ |.(((s_(#)_s1)_._m)_-_0c).|_<_p consider R being Real such that A5: 0 < R and A6: for m being Element of NAT holds |.(s1 . m).| < R by A2, Th8; 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 |.(((s (#) s1) . m) - 0c).| < p ) assume A7: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds |.(((s (#) s1) . m) - 0c).| < p A8: 0 < p / R by A7, A5; then consider n1 being Element of NAT such that A9: for m being Element of NAT st n1 <= m holds |.((s . m) - 0c).| < p / R by A1, A3, Def6; take n = n1; ::_thesis: for m being Element of NAT st n <= m holds |.(((s (#) s1) . m) - 0c).| < p let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((s (#) s1) . m) - 0c).| < p ) (p / R) * R = (p * (R ")) * R by XCMPLX_0:def_9 .= p * ((R ") * R) .= p * 1 by A5, XCMPLX_0:def_7 ; then A10: (p / R) * |.(s1 . m).| < p by A6, A8, XREAL_1:68; assume n <= m ; ::_thesis: |.(((s (#) s1) . m) - 0c).| < p then A11: |.((s . m) - 0c).| < p / R by A9; A12: |.(((s (#) s1) . m) - 0c).| = |.((s . m) * (s1 . m)).| by VALUED_1:5 .= |.(s . m).| * |.(s1 . m).| by COMPLEX1:65 ; A13: 0 <= |.(s1 . m).| by COMPLEX1:46; now__::_thesis:_(_|.(s1_._m).|_<>_0_implies_|.(((s_(#)_s1)_._m)_-_0c).|_<_p_) assume |.(s1 . m).| <> 0 ; ::_thesis: |.(((s (#) s1) . m) - 0c).| < p then |.(((s (#) s1) . m) - 0c).| < (p / R) * |.(s1 . m).| by A11, A12, A13, XREAL_1:68; hence |.(((s (#) s1) . m) - 0c).| < p by A10, XXREAL_0:2; ::_thesis: verum end; hence |.(((s (#) s1) . m) - 0c).| < p by A7, A12; ::_thesis: verum end; s (#) s1 is convergent by A1, A2, A3, Th42; hence lim (s (#) s1) = 0c by A4, Def6; ::_thesis: verum end; theorem :: COMSEQ_2:44 canceled; theorem :: COMSEQ_2:45 for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds lim ((s (#) s1) *') = 0c proof let s, s1 be Complex_Sequence; ::_thesis: ( s is convergent & s1 is bounded & lim s = 0c implies lim ((s (#) s1) *') = 0c ) assume A1: ( s is convergent & s1 is bounded & lim s = 0c ) ; ::_thesis: lim ((s (#) s1) *') = 0c then s (#) s1 is convergent by Th42; hence lim ((s (#) s1) *') = (lim (s (#) s1)) *' by Th12 .= 0c by A1, Th43, COMPLEX1:28 ; ::_thesis: verum end;