:: Complex Sequences :: by Agnieszka Banachowicz and Anna Winnicka :: :: Received November 5, 1993 :: Copyright (c) 1993-2018 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 FUNCT_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1, TARSKI, XCMPLX_0, VALUED_0, FUNCOP_1, COMPLEX1, CARD_1, XBOOLE_0, ARYTM_3, VALUED_1, ARYTM_1, COMSEQ_1, ZFMISC_1; notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, COMPLEX1, RELAT_1, ZFMISC_1, FUNCT_1, NAT_1, RELSET_1, FUNCOP_1, VALUED_1; constructors PARTFUN1, FUNCOP_1, REAL_1, COMPLEX1, VALUED_1, RELSET_1, VALUED_0; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, MEMBERED, VALUED_0, VALUED_1, XCMPLX_0, XREAL_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve f for Function; reserve n,k,n1 for Element of NAT; reserve r,p for Complex; reserve x,y for set; definition mode Complex_Sequence is sequence of COMPLEX; end; reserve seq,seq1,seq2,seq3,seq9,seq19 for Complex_Sequence; theorem :: COMSEQ_1:1 f is Complex_Sequence iff (dom f=NAT & for x st x in NAT holds f. x is Element of COMPLEX); theorem :: COMSEQ_1:2 f is Complex_Sequence iff (dom f=NAT & for n holds f.n is Element of COMPLEX) ; scheme :: COMSEQ_1:sch 1 ExComplexSeq{F(set) -> Complex}: ex seq st for n being Nat holds seq.n=F(n); registration cluster non-zero for Complex_Sequence; end; theorem :: COMSEQ_1:3 seq is non-zero iff for x st x in NAT holds seq.x<>0c; theorem :: COMSEQ_1:4 seq is non-zero iff for n holds seq.n<>0c; theorem :: COMSEQ_1:5 for IT being non-zero Complex_Sequence holds rng IT c= COMPLEX \ {0c}; theorem :: COMSEQ_1:6 for r ex seq st rng seq={r}; theorem :: COMSEQ_1:7 (seq1+seq2)+seq3=seq1+(seq2+seq3); theorem :: COMSEQ_1:8 (seq1(#)seq2)(#)seq3=seq1(#)(seq2(#)seq3); theorem :: COMSEQ_1:9 (seq1+seq2)(#)seq3=seq1(#)seq3+seq2(#)seq3; theorem :: COMSEQ_1:10 seq3(#)(seq1+seq2)=seq3(#)seq1+seq3(#)seq2; theorem :: COMSEQ_1:11 -seq=(-1r)(#)seq; theorem :: COMSEQ_1:12 r(#)(seq1(#)seq2)=r(#)seq1(#)seq2; theorem :: COMSEQ_1:13 r(#)(seq1(#)seq2)=seq1(#)(r(#)seq2); theorem :: COMSEQ_1:14 (seq1-seq2)(#)seq3=seq1(#)seq3-seq2(#)seq3; theorem :: COMSEQ_1:15 seq3(#)seq1-seq3(#)seq2=seq3(#)(seq1-seq2); theorem :: COMSEQ_1:16 r(#)(seq1+seq2)=r(#)seq1+r(#)seq2; theorem :: COMSEQ_1:17 (r*p)(#)seq=r(#)(p(#)seq); theorem :: COMSEQ_1:18 r(#)(seq1-seq2)=r(#)seq1-r(#)seq2; theorem :: COMSEQ_1:19 r(#)(seq1/"seq)=(r(#)seq1)/"seq; theorem :: COMSEQ_1:20 seq1-(seq2+seq3)=seq1-seq2-seq3; theorem :: COMSEQ_1:21 1r(#)seq=seq; theorem :: COMSEQ_1:22 --seq = seq; theorem :: COMSEQ_1:23 seq1 - (-seq2) = seq1 + seq2; theorem :: COMSEQ_1:24 seq1 - (seq2 - seq3) = seq1 - seq2 + seq3; theorem :: COMSEQ_1:25 seq1 + (seq2 - seq3) = seq1 + seq2 - seq3; theorem :: COMSEQ_1:26 (-seq1)(#)seq2=-(seq1(#)seq2) & seq1(#)(-seq2)=-(seq1(#)seq2); theorem :: COMSEQ_1:27 seq is non-zero implies seq" is non-zero; ::\$CT theorem :: COMSEQ_1:29 seq is non-zero & seq1 is non-zero iff seq(#)seq1 is non-zero; theorem :: COMSEQ_1:30 seq"(#)seq1"=(seq(#)seq1)"; theorem :: COMSEQ_1:31 seq is non-zero implies (seq1/"seq)(#)seq=seq1; theorem :: COMSEQ_1:32 (seq9/"seq)(#)(seq19/"seq1)=(seq9(#)seq19)/"(seq(#)seq1); theorem :: COMSEQ_1:33 seq is non-zero & seq1 is non-zero implies seq/"seq1 is non-zero; theorem :: COMSEQ_1:34 (seq/"seq1)"=seq1/"seq; theorem :: COMSEQ_1:35 seq2 (#) (seq1 /" seq) = (seq2 (#) seq1) /" seq; theorem :: COMSEQ_1:36 seq2/"(seq/"seq1)=(seq2(#)seq1)/"seq; theorem :: COMSEQ_1:37 seq1 is non-zero implies seq2/"seq=(seq2(#)seq1)/"(seq(#)seq1); theorem :: COMSEQ_1:38 r<>0c & seq is non-zero implies r(#)seq is non-zero; theorem :: COMSEQ_1:39 seq is non-zero implies -seq is non-zero; theorem :: COMSEQ_1:40 (r(#)seq)"=r"(#)seq"; theorem :: COMSEQ_1:41 seq is non-zero implies (-seq)"=(-1r)(#)seq"; theorem :: COMSEQ_1:42 seq is non-zero implies -seq1/"seq=(-seq1)/"seq & seq1/"(-seq)=-seq1/" seq; theorem :: COMSEQ_1:43 seq1/"seq + seq19/"seq = (seq1+seq19) /" seq & seq1/"seq - seq19/"seq = (seq1-seq19) /" seq; theorem :: COMSEQ_1:44 seq is non-zero & seq9 is non-zero implies seq1/"seq + seq19/"seq9=( seq1(#)seq9+seq19(#)seq)/"(seq(#)seq9) & seq1/"seq - seq19/"seq9=(seq1(#)seq9- seq19(#)seq)/"(seq(#)seq9); theorem :: COMSEQ_1:45 (seq19/"seq)/"(seq9/"seq1)=(seq19(#)seq1)/"(seq(#)seq9); theorem :: COMSEQ_1:46 |.seq(#)seq9.|=|.seq.|(#)|.seq9.|; ::\$CT theorem :: COMSEQ_1:48 |. seq .| " = |. seq" .|; theorem :: COMSEQ_1:49 |.seq9/"seq.|=|.seq9.|/"|.seq.|; theorem :: COMSEQ_1:50 |.r(#)seq.|=|.r.|(#)|.seq.|;