:: Conjugate Sequences, Bounded Complex Sequences and Convergent :: Complex Sequences :: by Adam Naumowicz :: :: Received December 20, 1996 :: Copyright (c) 1996-2016 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, REAL_1, COMSEQ_1, COMPLEX1, RELAT_1, ARYTM_1, ARYTM_3, CARD_1, XXREAL_0, FUNCT_1, XBOOLE_0, PARTFUN1, VALUED_0, VALUED_1, XXREAL_2, FUNCOP_1, SEQ_2, ORDINAL2, XCMPLX_0, PBOOLE, TARSKI, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, RELAT_1, REAL_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, NAT_1, COMSEQ_1, XXREAL_0; constructors PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, RELSET_1, PBOOLE, NUMBERS; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, VALUED_1, VALUED_0, XCMPLX_0, NAT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve n,n1,n2,m for Nat; reserve r,g1,g2,g,g9 for Complex; reserve R,R2 for Real; reserve s,s9,s1 for Complex_Sequence; theorem :: COMSEQ_2:1 g<>0c & r<>0c implies |.g"-r".|=|.g-r.|/(|.g.|*|.r.|); theorem :: COMSEQ_2:2 for n ex r being Real st 0 complex-valued Function means :: COMSEQ_2:def 1 dom it = dom f & for c being set st c in dom it holds it.c = (f.c)*'; involutiveness; end; definition let C be non empty set; let f be Function of C,COMPLEX; redefine func f*' -> Function of C,COMPLEX means :: COMSEQ_2:def 2 for n being Element of C holds it.n=(f.n)*'; end; registration let C be non empty set; let s be complex-valued ManySortedSet of C; cluster s*' -> C-defined; end; registration let C be non empty set; let seq be complex-valued ManySortedSet of C; cluster seq*' -> total for C-defined Function; end; theorem :: COMSEQ_2:3 s is non-zero implies s*' is non-zero; theorem :: COMSEQ_2:4 (r(#)s)*' = (r*')(#)(s*'); theorem :: COMSEQ_2:5 (s (#) s9)*' = (s*') (#) (s9*'); theorem :: COMSEQ_2:6 (s*')" = (s")*'; theorem :: COMSEQ_2:7 (s9/"s)*' = (s9*') /" (s*'); begin :: BOUNDED COMPLEX SEQUENCES definition let f be complex-valued Function; attr f is bounded means :: COMSEQ_2:def 3 :: SEQ_2:def 5 ex r being Real st for y being set st y in dom f holds |.f.y.| Complex means :: COMSEQ_2:def 6 for p be Real st 0

convergent for Complex_Sequence; end; ::\$CT theorem :: COMSEQ_2:12 s is convergent implies lim(s*') = (lim s)*'; begin :: Main Theorems registration let s1,s2 be convergent Complex_Sequence; cluster s1 + s2 -> convergent for Complex_Sequence; end; ::\$CT theorem :: COMSEQ_2:14 for s,s9 being convergent Complex_Sequence holds lim (s + s9)=(lim s)+ (lim s9); ::\$CT theorem :: COMSEQ_2:16 for s,s9 being convergent Complex_Sequence holds lim (s + s9)*' = (lim s)*' + (lim s9)*'; registration let s be convergent Complex_Sequence, c be Complex; cluster c(#)s -> convergent for Complex_Sequence; end; ::\$CT theorem :: COMSEQ_2:18 for s being convergent Complex_Sequence, r being Complex holds lim(r(#)s)=r*(lim s); ::\$CT theorem :: COMSEQ_2:20 for s being convergent Complex_Sequence holds lim (r(#)s)*' = (r*')*(lim s)*'; registration let s be convergent Complex_Sequence; cluster -s -> convergent for Complex_Sequence; end; ::\$CT theorem :: COMSEQ_2:22 for s being convergent Complex_Sequence holds lim(-s)=-(lim s); ::\$CT theorem :: COMSEQ_2:24 for s being convergent Complex_Sequence holds lim (-s)*' = -(lim s)*'; registration let s1,s2 be convergent Complex_Sequence; cluster s1 - s2 -> convergent for Complex_Sequence; end; ::\$CT theorem :: COMSEQ_2:26 for s,s9 being convergent Complex_Sequence holds lim(s - s9)=(lim s)-( lim s9); ::\$CT theorem :: COMSEQ_2:28 for s,s9 being convergent Complex_Sequence holds lim (s - s9)*' = (lim s)*' - (lim s9)*'; registration cluster convergent -> bounded for Complex_Sequence; end; registration cluster non bounded -> non convergent for Complex_Sequence; end; registration let s1,s2 be convergent Complex_Sequence; cluster s1 (#) s2 -> convergent for Complex_Sequence; end; ::\$CT theorem :: COMSEQ_2:30 for s,s9 being convergent Complex_Sequence holds lim(s(#)s9)=(lim s)*(lim s9); ::\$CT theorem :: COMSEQ_2:32 for s,s9 being convergent Complex_Sequence holds lim (s(#)s9)*' = (lim s)*' * (lim s9)*'; theorem :: COMSEQ_2:33 for s being convergent Complex_Sequence st lim s <> 0c ex n st for m st n <=m holds |.(lim s).|/2<|.s.m.|; theorem :: COMSEQ_2:34 for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds s" is convergent; theorem :: COMSEQ_2:35 s is convergent & (lim s)<>0c & s is non-zero implies lim s"=( lim s)"; ::\$CT theorem :: COMSEQ_2:37 s is convergent & (lim s)<>0c & s is non-zero implies lim (s")*' = (( lim s)*')"; theorem :: COMSEQ_2:38 s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies s9/"s is convergent; theorem :: COMSEQ_2:39 s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim(s9/"s)=(lim s9)/(lim s); ::\$CT theorem :: COMSEQ_2:41 s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim (s9/"s)*' = ((lim s9)*')/((lim s)*'); theorem :: COMSEQ_2:42 s is convergent & s1 is bounded & (lim s)=0c implies s(#)s1 is convergent; theorem :: COMSEQ_2:43 s is convergent & s1 is bounded & (lim s)=0c implies lim(s(#)s1) =0c; ::\$CT theorem :: COMSEQ_2:45 s is convergent & s1 is bounded & (lim s)=0c implies lim (s(#)s1)*' = 0c;