:: Real Sequences and Basic Operations on Them :: by Jaros{\l}aw Kotowicz :: :: Received July 4, 1989 :: Copyright (c) 1990-2021 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, XREAL_0, NAT_1, RELAT_1, TARSKI, VALUED_0, REAL_1, PARTFUN1, FUNCOP_1, CARD_1, XBOOLE_0, ARYTM_3, VALUED_1, ARYTM_1, COMPLEX1, SEQ_1, ASYMPT_1, XCMPLX_0; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, VALUED_0, REAL_1, RELAT_1, FUNCT_1, FUNCOP_1, COMPLEX1, NAT_1, RELSET_1, PARTFUN1, FUNCT_2, VALUED_1; constructors PARTFUN1, FUNCT_2, XXREAL_0, REAL_1, COMPLEX1, VALUED_1, FUNCOP_1, RELSET_1, NUMBERS, TARSKI, XBOOLE_0; registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, FUNCOP_1, XXREAL_0; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve f for Function; reserve n,k,n1 for Nat; reserve r,p for Real; reserve x,y,z for object; definition mode Real_Sequence is :::real-valued ManySortedSet of NAT; sequence of REAL; end; reserve seq,seq1,seq2,seq3,seq9,seq19 for Real_Sequence; theorem :: SEQ_1:1 f is Real_Sequence iff (dom f=NAT & for x st x in NAT holds f.x is real); theorem :: SEQ_1:2 f is Real_Sequence iff (dom f=NAT & for n holds f.n is real); registration cluster non-zero for PartFunc of NAT,REAL; end; theorem :: SEQ_1:3 for f being non-zero PartFunc of NAT,REAL holds rng f c= REAL \ {0}; theorem :: SEQ_1:4 seq is non-zero iff for x st x in NAT holds seq.x<>0; theorem :: SEQ_1:5 seq is non-zero iff for n holds seq.n<>0; theorem :: SEQ_1:6 for r ex seq st rng seq={r}; scheme :: SEQ_1:sch 1 ExRealSeq{F(object)->Real}: ex seq st for n holds seq.n=F(n); :: :: Basic Operations on Sequences :: scheme :: SEQ_1:sch 2 PartFuncExD9{D,C()->non empty set, P[object,object]}: ex f being PartFunc of D(),C() st (for d be Element of D() holds d in dom f iff (ex c be Element of C() st P[d,c])) & for d be Element of D() st d in dom f holds P[d,f.d]; scheme :: SEQ_1:sch 3 LambdaPFD9{D,C()->non empty set, F(object)->Element of C(), P[object]}: ex f being PartFunc of D(),C() st (for d be Element of D() holds d in dom f iff P[d]) & for d be Element of D() st d in dom f holds f.d = F(d); scheme :: SEQ_1:sch 4 UnPartFuncD9{C,D,X() -> set, F(object)->object}: for f,g being PartFunc of C(),D() st (dom f=X() & for c be Element of C() st c in dom f holds f.c = F(c)) & (dom g=X() & for c be Element of C() st c in dom g holds g.c = F(c)) holds f = g; theorem :: SEQ_1:7 seq = seq1 + seq2 iff for n holds seq.n =seq1.n + seq2.n; theorem :: SEQ_1:8 seq = seq1 (#) seq2 iff for n holds seq.n =seq1.n * seq2.n; theorem :: SEQ_1:9 seq1 = r(#)seq2 iff for n holds seq1.n=r*seq2.n; theorem :: SEQ_1:10 seq1 = -seq2 iff for n holds seq1.n= -seq2.n; theorem :: SEQ_1:11 seq1 - seq2 = seq1 +- seq2; theorem :: SEQ_1:12 seq1 = abs seq iff for n holds seq1.n= |.seq.n.|; theorem :: SEQ_1:13 (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3); theorem :: SEQ_1:14 (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3); theorem :: SEQ_1:15 (seq1 + seq2) (#) seq3 = seq1 (#) seq3 + seq2 (#) seq3; theorem :: SEQ_1:16 seq3 (#) (seq1 + seq2) = seq3 (#) seq1 + seq3 (#) seq2; theorem :: SEQ_1:17 -seq = (-1) (#) seq; theorem :: SEQ_1:18 r(#)(seq1(#)seq2)=r(#)seq1(#)seq2; theorem :: SEQ_1:19 r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2); theorem :: SEQ_1:20 (seq1 - seq2) (#) seq3 = seq1 (#) seq3 - seq2 (#) seq3; theorem :: SEQ_1:21 seq3(#)seq1-seq3(#)seq2=seq3(#)(seq1-seq2); theorem :: SEQ_1:22 r(#)(seq1+seq2)=r(#)seq1+r(#)seq2; theorem :: SEQ_1:23 (r*p)(#)seq=r(#)(p(#)seq); theorem :: SEQ_1:24 r(#)(seq1-seq2)=r(#)seq1-r(#)seq2; theorem :: SEQ_1:25 r(#)(seq1/"seq)=(r(#)seq1)/"seq; theorem :: SEQ_1:26 seq1-(seq2+seq3)=seq1-seq2-seq3; theorem :: SEQ_1:27 1(#)seq=seq; ::$CT theorem :: SEQ_1:29 seq1 - (-seq2) = seq1 + seq2; theorem :: SEQ_1:30 seq1-(seq2-seq3)=seq1-seq2+seq3; theorem :: SEQ_1:31 seq1+(seq2-seq3)=seq1+seq2-seq3; theorem :: SEQ_1:32 (-seq1)(#)seq2=-(seq1(#)seq2) & seq1(#)(-seq2)=-(seq1(#)seq2); theorem :: SEQ_1:33 seq is non-zero implies seq" is non-zero; ::$CT theorem :: SEQ_1:35 seq is non-zero & seq1 is non-zero iff seq(#)seq1 is non-zero; theorem :: SEQ_1:36 seq"(#)seq1"=(seq(#)seq1)"; theorem :: SEQ_1:37 seq is non-zero implies (seq1/"seq)(#)seq=seq1; theorem :: SEQ_1:38 (seq9/"seq)(#)(seq19/"seq1)=(seq9(#)seq19)/"(seq(#)seq1); theorem :: SEQ_1:39 seq is non-zero & seq1 is non-zero implies seq/"seq1 is non-zero; theorem :: SEQ_1:40 (seq/"seq1)"=seq1/"seq; theorem :: SEQ_1:41 seq2(#)(seq1/"seq)=(seq2(#)seq1)/"seq; theorem :: SEQ_1:42 seq2/"(seq/"seq1)=(seq2(#)seq1)/"seq; theorem :: SEQ_1:43 seq1 is non-zero implies seq2/"seq=(seq2(#)seq1)/"(seq(#)seq1); theorem :: SEQ_1:44 r<>0 & seq is non-zero implies r(#)seq is non-zero; theorem :: SEQ_1:45 seq is non-zero implies -seq is non-zero; theorem :: SEQ_1:46 (r(#)seq)"=r"(#)seq"; theorem :: SEQ_1:47 (-seq)" = (-1)(#)seq"; theorem :: SEQ_1:48 -seq1/"seq=(-seq1)/"seq & seq1/"(-seq)=-seq1/"seq; theorem :: SEQ_1:49 seq1/"seq + seq19/"seq = (seq1 + seq19) /" seq & seq1/"seq - seq19/" seq = (seq1 - seq19) /" seq; theorem :: SEQ_1:50 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 :: SEQ_1:51 (seq19/"seq)/"(seq9/"seq1)=(seq19(#)seq1)/"(seq(#)seq9); theorem :: SEQ_1:52 abs(seq(#)seq9)=abs(seq)(#)abs(seq9); theorem :: SEQ_1:53 seq is non-zero implies abs(seq) is non-zero; theorem :: SEQ_1:54 abs(seq)"=abs(seq"); theorem :: SEQ_1:55 abs(seq9/"seq)=abs(seq9)/"abs(seq); theorem :: SEQ_1:56 abs(r(#)seq)=|.r.|(#)abs(seq); definition let b be Real; func seq_const b -> Real_Sequence equals :: SEQ_1:def 1 NAT --> b; end; registration let b be Real; cluster seq_const b -> constant; end; registration let b be non zero Real; cluster seq_const b -> non-zero; end; registration cluster constant for Real_Sequence; end; theorem :: SEQ_1:57 for a being Real, k being Nat holds (seq_const a).k = a; registration let k be object; reduce (NAT --> 0).k to 0; end; registration let k be object; reduce (seq_const 0).k to 0; end;