:: Real Sequences and Basic Operations on Them :: by Jaros{\l}aw Kotowicz :: :: Received July 4, 1989 :: Copyright (c) 1990-2017 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; 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; definitions ORDINAL1; equalities VALUED_1; theorems FUNCT_1, TARSKI, ABSVALUE, FUNCT_2, PARTFUN1, RELSET_1, RELAT_1, XREAL_0, ZFMISC_1, XBOOLE_0, XCMPLX_0, XCMPLX_1, COMPLEX1, VALUED_1, FUNCOP_1, ORDINAL1, NUMBERS; schemes CLASSES1, FUNCT_2, XBOOLE_0; 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 Th1: f is Real_Sequence iff (dom f=NAT & for x st x in NAT holds f.x is real) proof thus f is Real_Sequence implies (dom f=NAT & for x st x in NAT holds f.x is real) by FUNCT_2:def 1; assume that A1: dom f= NAT and A2: for x st x in NAT holds f.x is real; now let y be object; assume y in rng f; then consider x being object such that A3: x in dom f and A4: y=f.x by FUNCT_1:def 3; f.x is real by A1,A2,A3; hence y in REAL by A4,XREAL_0:def 1; end; then rng f c=REAL by TARSKI:def 3; hence thesis by A1,FUNCT_2:def 1,RELSET_1:4; end; theorem Th2: f is Real_Sequence iff (dom f=NAT & for n holds f.n is real) proof thus f is Real_Sequence implies (dom f=NAT & for n holds f.n is real) by Th1; assume that A1: dom f=NAT and A2: for n holds f.n is real; for x holds x in NAT implies f.x is real by A2; hence thesis by A1,Th1; end; registration cluster non-zero for PartFunc of NAT,REAL; existence proof 1 in NAT; then 1 in REAL by NUMBERS:19; then reconsider p = NAT --> 1 as PartFunc of NAT,REAL by FUNCOP_1:46; take p; rng p = {1} by FUNCOP_1:8; hence not 0 in rng p by TARSKI:def 1; end; end; theorem for f being non-zero PartFunc of NAT,REAL holds rng f c= REAL \ {0} by ORDINAL1:def 15,ZFMISC_1:34; theorem Th4: seq is non-zero iff for x st x in NAT holds seq.x<>0 proof thus seq is non-zero implies for x st x in NAT holds seq.x<>0 proof assume A1: seq is non-zero; let x; assume x in NAT; then x in dom seq by Th2; then seq.x in rng seq by FUNCT_1:def 3; hence thesis by A1; end; assume A2: for x st x in NAT holds seq.x<>0; assume 0 in rng seq; then ex x being object st x in dom seq & seq.x=0 by FUNCT_1:def 3; hence contradiction by A2; end; theorem Th5: seq is non-zero iff for n holds seq.n<>0 proof thus seq is non-zero implies for n holds seq.n<>0 by ORDINAL1:def 12,Th4; assume for n holds seq.n<>0; then for x holds x in NAT implies seq.x<>0; hence thesis by Th4; end; theorem for r ex seq st rng seq={r} proof let r; consider f such that A1: dom f=NAT and A2: rng f={r} by FUNCT_1:5; for x being object st x in {r} holds x in REAL by XREAL_0:def 1; then rng f c= REAL by A2,TARSKI:def 3; then reconsider f as Real_Sequence by A1,FUNCT_2:def 1,RELSET_1:4; take f; thus thesis by A2; end; scheme ExRealSeq{F(object)->Real}: ex seq st for n holds seq.n=F(n) proof defpred P[object,object] means ex n st n=\$1 & \$2=F(n); A1: now let x be object; assume x in NAT; then consider n such that A2: n=x; reconsider r2=F(n) as object; take y=r2; thus P[x,y] by A2; end; consider f such that A3: dom f=NAT and A4: for x being object st x in NAT holds P[x,f.x] from CLASSES1:sch 1(A1); now let x; assume x in NAT; then ex n st n=x & f.x=F(n) by A4; hence f.x is real; end; then reconsider f as Real_Sequence by A3,Th1; take seq=f; let n; n in NAT by ORDINAL1:def 12; then ex k st k=n & seq.n=F(k) by A4; hence thesis; end; :: :: BASIC OPERATIONS ON SEQUENCES :: scheme 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] proof defpred X[object] means ex c be Element of C() st P[\$1,c]; set x = the Element of C(); defpred X[Element of D(),Element of C()] means ((ex c be Element of C() st P [\$1,c]) implies P[\$1,\$2]) & ((for c be Element of C() holds not P[\$1,c]) implies \$2=x); consider X be set such that A1: for x being object holds x in X iff x in D() & X[x] from XBOOLE_0:sch 1; for x being object holds x in X implies x in D() by A1; then reconsider X as Subset of D() by TARSKI:def 3; A2: for d be Element of D() ex z be Element of C() st X[d,z] proof let d be Element of D(); (for c be Element of C() holds not P[d,c]) implies ex z st ((ex c be Element of C() st P[d,c]) implies P[d,z]) & ((for c be Element of C() holds not P[d,c]) implies z=x); hence thesis; end; consider g being Function of D(),C() such that A3: for d be Element of D() holds X[d,g.d] from FUNCT_2:sch 3(A2); reconsider f=g|X as PartFunc of D(),C(); take f; A4: dom g = D() by FUNCT_2:def 1; thus for d be Element of D() holds d in dom f iff ex c be Element of C() st P[d,c] proof let d be Element of D(); dom f c= X by RELAT_1:58; hence d in dom f implies ex c be Element of C() st P[d,c] by A1; assume ex c be Element of C() st P[d,c]; then d in X by A1; then d in dom g /\ X by A4,XBOOLE_0:def 4; hence thesis by RELAT_1:61; end; let d be Element of D(); assume A5: d in dom f; dom f c= X by RELAT_1:58; then ex c be Element of C() st P[d,c] by A1,A5; then P[d,g.d] by A3; hence thesis by A5,FUNCT_1:47; end; scheme 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) proof defpred X[Element of D(),set] means P[\$1] & \$2 = F(\$1); consider f being PartFunc of D(),C() such that A1: for d be Element of D() holds d in dom f iff ex c be Element of C() st X[d,c] and A2: for d be Element of D() st d in dom f holds X[d,f.d] from PartFuncExD9; take f; thus for d be Element of D() holds d in dom f iff P[d] proof let d be Element of D(); thus d in dom f implies P[d] proof assume d in dom f; then ex c be Element of C() st P[d] & c = F(d) by A1; hence thesis; end; assume P[d]; then ex c be Element of C() st P[d] & c = F(d); hence thesis by A1; end; thus thesis by A2; end; scheme 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 proof let f,g be PartFunc of C(),D(); assume that A1: dom f=X() and A2: for c be Element of C() st c in dom f holds f.c = F(c) and A3: dom g=X() and A4: for c be Element of C() st c in dom g holds g.c = F(c); now let c be Element of C(); assume A5: c in dom f; hence f.c = F(c) by A2 .= g.c by A1,A3,A4,A5; end; hence thesis by A1,A3,PARTFUN1:5; end; theorem Th7: seq = seq1 + seq2 iff for n holds seq.n =seq1.n + seq2.n proof thus seq = seq1 + seq2 implies for n holds seq.n =seq1.n + seq2.n proof assume A1: seq = seq1 + seq2; let n; A2: n in NAT by ORDINAL1:def 12; dom seq = NAT by FUNCT_2:def 1; hence thesis by A1,VALUED_1:def 1,A2; end; assume for n holds seq.n =seq1.n + seq2.n; then A3: for n being object st n in dom seq holds seq.n = seq1.n + seq2.n; dom seq = NAT /\ NAT by FUNCT_2:def 1 .= NAT /\ dom seq2 by FUNCT_2:def 1 .= dom seq1 /\ dom seq2 by FUNCT_2:def 1; hence thesis by A3,VALUED_1:def 1; end; theorem Th8: seq = seq1 (#) seq2 iff for n holds seq.n =seq1.n * seq2.n proof thus seq = seq1 (#) seq2 implies for n holds seq.n =seq1.n * seq2.n proof assume A1: seq = seq1 (#) seq2; let n; A2: n in NAT by ORDINAL1:def 12; dom seq = NAT by FUNCT_2:def 1; hence thesis by A1,VALUED_1:def 4,A2; end; assume for n holds seq.n =seq1.n * seq2.n; then A3: for n being object st n in dom seq holds seq.n = seq1.n * seq2.n; dom seq = NAT /\ NAT by FUNCT_2:def 1 .= NAT /\ dom seq2 by FUNCT_2:def 1 .= dom seq1 /\ dom seq2 by FUNCT_2:def 1; hence thesis by A3,VALUED_1:def 4; end; theorem Th9: seq1 = r(#)seq2 iff for n holds seq1.n=r*seq2.n proof thus seq1 = r(#)seq2 implies for n holds seq1.n=r*seq2.n by VALUED_1:6; assume for n holds seq1.n=r*seq2.n; then A1: for n being object st n in dom seq1 holds seq1.n = r * seq2.n; dom seq1 = NAT by FUNCT_2:def 1 .= dom seq2 by FUNCT_2:def 1; hence thesis by A1,VALUED_1:def 5; end; theorem seq1 = -seq2 iff for n holds seq1.n= -seq2.n proof thus seq1 = -seq2 implies for n holds seq1.n=-seq2.n by VALUED_1:8; assume for n holds seq1.n= -seq2.n; then A1: for n being object st n in dom seq1 holds seq1.n = - seq2.n; dom seq1 = NAT by FUNCT_2:def 1 .= dom seq2 by FUNCT_2:def 1; hence thesis by A1,VALUED_1:9; end; theorem seq1 - seq2 = seq1 +- seq2; theorem Th12: seq1 = abs seq iff for n holds seq1.n= |.seq.n.| proof thus seq1 = abs seq implies for n holds seq1.n=|.seq.n.| by VALUED_1:18; assume for n holds seq1.n= |.seq.n.|; then A1: for n being object st n in dom seq1 holds seq1.n = |.seq.n.|; dom seq1 = NAT by FUNCT_2:def 1 .= dom seq by FUNCT_2:def 1; hence thesis by A1,VALUED_1:def 11; end; theorem Th13: (seq1 + seq2) + seq3 = seq1 + (seq2 + seq3) proof now let n be Element of NAT; thus ((seq1+seq2)+seq3).n=(seq1+seq2).n+ seq3.n by Th7 .=seq1.n+seq2.n+seq3.n by Th7 .=seq1.n+(seq2.n+seq3.n) .=seq1.n+(seq2+seq3).n by Th7 .=(seq1+(seq2+seq3)).n by Th7; end; hence thesis by FUNCT_2:63; end; theorem Th14: (seq1 (#) seq2) (#) seq3 = seq1 (#) (seq2 (#) seq3) proof now let n be Element of NAT; thus ((seq1(#)seq2)(#)seq3).n=(seq1(#)seq2).n*seq3.n by Th8 .=seq1.n*seq2.n*seq3.n by Th8 .=seq1.n*(seq2.n*seq3.n) .=seq1.n*(seq2(#)seq3).n by Th8 .=(seq1(#)(seq2(#)seq3)).n by Th8; end; hence thesis by FUNCT_2:63; end; theorem Th15: (seq1 + seq2) (#) seq3 = seq1 (#) seq3 + seq2 (#) seq3 proof now let n be Element of NAT; thus ((seq1+seq2)(#)seq3).n=(seq1+seq2).n*seq3.n by Th8 .=(seq1.n+seq2.n)*seq3.n by Th7 .=seq1.n*seq3.n+seq2.n*seq3.n .=(seq1(#)seq3).n+seq2.n*seq3.n by Th8 .=(seq1(#)seq3).n+(seq2(#)seq3).n by Th8 .=((seq1(#)seq3)+(seq2(#)seq3)).n by Th7; end; hence thesis by FUNCT_2:63; end; theorem seq3 (#) (seq1 + seq2) = seq3 (#) seq1 + seq3 (#) seq2 by Th15; theorem -seq = (-1) (#) seq; theorem Th18: r(#)(seq1(#)seq2)=r(#)seq1(#)seq2 proof now let n be Element of NAT; thus (r(#)(seq1(#)seq2)).n=r*(seq1(#)seq2).n by Th9 .=r*(seq1.n*seq2.n) by Th8 .=(r*seq1.n)*seq2.n .=(r(#)seq1).n*seq2.n by Th9 .=(r(#)seq1 (#) seq2).n by Th8; end; hence thesis by FUNCT_2:63; end; theorem Th19: r (#) (seq1 (#) seq2) = seq1 (#) (r (#) seq2) proof now let n be Element of NAT; thus (r(#)(seq1(#)seq2)).n=r*(seq1(#)seq2).n by Th9 .=r*(seq1.n*seq2.n) by Th8 .=seq1.n*(r*seq2.n) .=seq1.n*(r(#)seq2).n by Th9 .=(seq1(#)(r(#)seq2)).n by Th8; end; hence thesis by FUNCT_2:63; end; theorem Th20: (seq1 - seq2) (#) seq3 = seq1 (#) seq3 - seq2 (#) seq3 proof thus (seq1-seq2)(#)seq3=seq1(#)seq3+(-seq2)(#)seq3 by Th15 .=seq1(#)seq3-seq2(#)seq3 by Th18; end; theorem seq3(#)seq1-seq3(#)seq2=seq3(#)(seq1-seq2) by Th20; theorem Th22: r(#)(seq1+seq2)=r(#)seq1+r(#)seq2 proof now let n be Element of NAT; thus (r(#)(seq1 + seq2)).n=r*(seq1+seq2).n by Th9 .=r*(seq1.n+seq2.n) by Th7 .=r*seq1.n+r*seq2.n .=(r(#)seq1).n+r*seq2.n by Th9 .=(r(#)seq1).n+(r(#)seq2).n by Th9 .=((r(#)seq1)+(r(#)seq2)).n by Th7; end; hence thesis by FUNCT_2:63; end; theorem Th23: (r*p)(#)seq=r(#)(p(#)seq) proof now let n be Element of NAT; thus ((r*p)(#)seq).n=(r*p)*seq.n by Th9 .=r*(p*seq.n) .=r*(p(#)seq).n by Th9 .=(r(#)(p(#)seq)).n by Th9; end; hence thesis by FUNCT_2:63; end; theorem Th24: r(#)(seq1-seq2)=r(#)seq1-r(#)seq2 proof thus r(#)(seq1-seq2)=r(#)seq1+r(#)(-seq2) by Th22 .=r(#)seq1+((-1)*r)(#)seq2 by Th23 .=r(#)seq1-(r(#)seq2) by Th23; end; theorem r(#)(seq1/"seq)=(r(#)seq1)/"seq proof thus r(#)(seq1/"seq)= r(#)(seq1(#)(seq")) .= (r(#)seq1)/"seq by Th18; end; theorem seq1-(seq2+seq3)=seq1-seq2-seq3 proof thus seq1-(seq2+seq3)=seq1+(-seq2+(-1)(#)seq3) by Th22 .=seq1-seq2-seq3 by Th13; end; theorem 1(#)seq=seq proof now let n be Element of NAT; thus (1(#)seq).n=1*seq.n by Th9 .=seq.n; end; hence thesis by FUNCT_2:63; end; ::\$CT theorem seq1 - (-seq2) = seq1 + seq2; theorem seq1-(seq2-seq3)=seq1-seq2+seq3 proof thus seq1-(seq2-seq3)=seq1+(-seq2-(-seq3)) by Th24 .=seq1-seq2+seq3 by Th13; end; theorem seq1+(seq2-seq3)=seq1+seq2-seq3 proof thus seq1+(seq2-seq3)=seq1+seq2+-seq3 by Th13 .=seq1+seq2-seq3; end; theorem (-seq1)(#)seq2=-(seq1(#)seq2) & seq1(#)(-seq2)=-(seq1(#)seq2) by Th18; theorem Th32: seq is non-zero implies seq" is non-zero proof assume that A1: seq is non-zero and A2: not seq" is non-zero; consider n1 such that A3: (seq").n1=0 by A2,Th5; (seq.n1)"=(seq").n1 by VALUED_1:10; hence contradiction by A1,A3,Th5,XCMPLX_1:202; end; ::\$CT theorem Th33: seq is non-zero & seq1 is non-zero iff seq(#)seq1 is non-zero proof thus seq is non-zero & seq1 is non-zero implies seq(#)seq1 is non-zero proof assume A1: seq is non-zero & seq1 is non-zero; now let n; A2: (seq(#)seq1).n=(seq.n)*(seq1.n) by Th8; seq.n<>0 & seq1.n<>0 by A1,Th5; hence (seq(#)seq1).n<>0 by A2,XCMPLX_1:6; end; hence thesis by Th5; end; assume A3: seq(#)seq1 is non-zero; now let n; (seq(#)seq1).n=(seq.n)*(seq1.n) by Th8; hence seq.n<>0 by A3,Th5; end; hence seq is non-zero by Th5; now let n; (seq(#)seq1).n=(seq.n)*(seq1.n) by Th8; hence seq1.n<>0 by A3,Th5; end; hence thesis by Th5; end; theorem Th34: seq"(#)seq1"=(seq(#)seq1)" proof now let n be Element of NAT; thus ((seq")(#)(seq1")).n=((seq").n)*((seq1").n) by Th8 .=((seq").n)*(seq1.n)" by VALUED_1:10 .=(seq.n)"*(seq1.n)" by VALUED_1:10 .=((seq.n)*(seq1.n))" by XCMPLX_1:204 .=((seq(#)seq1).n)" by Th8 .=((seq(#)seq1)").n by VALUED_1:10; end; hence thesis by FUNCT_2:63; end; theorem seq is non-zero implies (seq1/"seq)(#)seq=seq1 proof assume A1: seq is non-zero; now let n be Element of NAT; A2: seq.n<>0 by A1,Th5; thus ((seq1/"seq)(#)seq).n=((seq1(#)seq").n)*seq.n by Th8 .=(seq1.n)*(seq".n)*seq.n by Th8 .=(seq1.n)*(seq.n)"*seq.n by VALUED_1:10 .=(seq1.n)*((seq.n)"*seq.n) .=(seq1.n)*1 by A2,XCMPLX_0:def 7 .=seq1.n; end; hence thesis by FUNCT_2:63; end; theorem (seq9/"seq)(#)(seq19/"seq1)=(seq9(#)seq19)/"(seq(#)seq1) proof now let n be Element of NAT; thus ((seq9/"seq)(#)(seq19/"seq1)).n=((seq9(#)seq").n)*(seq19/"seq1).n by Th8 .=(seq9.n)*(seq".n)*(seq19(#)seq1").n by Th8 .=(seq9.n)*(seq".n)*((seq19.n)*seq1".n) by Th8 .=(seq9.n)*((seq19.n)*((seq".n)*seq1".n)) .=(seq9.n)*((seq19.n)*((seq"(#)seq1").n)) by Th8 .=(seq9.n)*(seq19.n)*((seq"(#)seq1").n) .=(seq9.n)*(seq19.n)*((seq(#)seq1)".n) by Th34 .=((seq9(#)seq19).n)*(seq(#)seq1)".n by Th8 .=((seq9(#)seq19)/"(seq(#)seq1)).n by Th8; end; hence thesis by FUNCT_2:63; end; theorem seq is non-zero & seq1 is non-zero implies seq/"seq1 is non-zero proof assume that A1: seq is non-zero and A2: seq1 is non-zero; seq1" is non-zero by A2,Th32; hence thesis by A1,Th33; end; theorem Th38: (seq/"seq1)"=seq1/"seq proof now let n be Element of NAT; thus (seq/"seq1)".n=(seq"(#)seq1"").n by Th34 .=(seq1/"seq).n; end; hence thesis by FUNCT_2:63; end; theorem seq2(#)(seq1/"seq)=(seq2(#)seq1)/"seq proof thus seq2(#)(seq1/"seq) = seq2(#)(seq1(#)(seq")) .=(seq2(#)seq1)/"seq by Th14; end; theorem seq2/"(seq/"seq1)=(seq2(#)seq1)/"seq proof thus seq2/"(seq/"seq1) = seq2(#)(seq1/"seq) by Th38 .= seq2(#)(seq1(#)(seq")) .= (seq2(#)seq1)/"seq by Th14; end; theorem Th41: seq1 is non-zero implies seq2/"seq=(seq2(#)seq1)/"(seq(#)seq1) proof assume A1: seq1 is non-zero; now let n be Element of NAT; A2: seq1.n<>0 by A1,Th5; thus (seq2/"seq).n=(seq2.n)*1*seq".n by Th8 .=(seq2.n)*((seq1.n)*(seq1.n)")*seq".n by A2,XCMPLX_0:def 7 .=(seq2.n)*(seq1.n)*((seq1.n)"*seq".n) .=((seq2(#)seq1).n)*((seq1.n)"*seq".n) by Th8 .=((seq2(#)seq1).n)*((seq1".n)*seq".n) by VALUED_1:10 .=((seq2(#)seq1).n)*(seq"(#)seq1").n by Th8 .=((seq2(#)seq1).n)*(seq(#)seq1)".n by Th34 .=((seq2(#)seq1)/"(seq(#)seq1)).n by Th8; end; hence thesis by FUNCT_2:63; end; theorem Th42: r<>0 & seq is non-zero implies r(#)seq is non-zero proof assume that A1: r<>0 and A2: seq is non-zero and A3: not r(#)seq is non-zero; consider n1 such that A4: (r(#)seq).n1=0 by A3,Th5; A5: seq.n1 <> 0 by A2,Th5; r*seq.n1=0 by A4,Th9; hence contradiction by A1,A5,XCMPLX_1:6; end; theorem seq is non-zero implies -seq is non-zero by Th42; theorem Th44: (r(#)seq)"=r"(#)seq" proof now let n be Element of NAT; thus (r(#)seq)".n=((r(#)seq).n)" by VALUED_1:10 .=(r*(seq.n))" by Th9 .=r"*(seq.n)" by XCMPLX_1:204 .=r"*seq".n by VALUED_1:10 .=(r"(#)seq").n by Th9; end; hence thesis by FUNCT_2:63; end; Lm1: (-1)"=-1; theorem (-seq)" = (-1)(#)seq" by Lm1,Th44; theorem -seq1/"seq=(-seq1)/"seq & seq1/"(-seq)=-seq1/"seq proof thus -seq1/"seq=(-1)(#)(seq1(#)(seq")) .=(-seq1)/"seq by Th18; thus seq1/"(-seq)=seq1(#)((-1)(#)seq") by Lm1,Th44 .=-(seq1/"seq) by Th19; end; theorem seq1/"seq + seq19/"seq = (seq1 + seq19) /" seq & seq1/"seq - seq19/" seq = (seq1 - seq19) /" seq proof thus seq1/"seq + seq19/"seq = (seq1 + seq19) (#) (seq") by Th15 .= (seq1 + seq19) /" seq; thus seq1/"seq - seq19/"seq = (seq1 - seq19) (#) (seq") by Th20 .= (seq1 - seq19) /" seq; end; theorem 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) proof assume that A1: seq is non-zero and A2: seq9 is non-zero; thus seq1/"seq + seq19/"seq9=(seq1(#)seq9)/"(seq(#)seq9)+seq19/"seq9 by A2 ,Th41 .=(seq1(#)seq9)/"(seq(#)seq9)+(seq19(#)seq)/"(seq(#)seq9) by A1,Th41 .=(seq1(#)seq9+seq19(#)seq)(#)((seq(#)seq9)") by Th15 .=(seq1(#)seq9+seq19(#)seq)/"(seq(#)seq9); thus seq1/"seq - seq19/"seq9=(seq1(#)seq9)/"(seq(#)seq9)-seq19/"seq9 by A2 ,Th41 .=(seq1(#)seq9)/"(seq(#)seq9)-(seq19(#)seq)/"(seq(#)seq9) by A1,Th41 .=(seq1(#)seq9-seq19(#)seq)(#)((seq(#)seq9)") by Th20 .=(seq1(#)seq9-seq19(#)seq)/"(seq(#)seq9); end; theorem (seq19/"seq)/"(seq9/"seq1)=(seq19(#)seq1)/"(seq(#)seq9) proof thus (seq19/"seq)/"(seq9/"seq1)=(seq19/"seq)(#)(seq9"(#)seq1"") by Th34 .=seq19(#)seq"(#)seq1(#)seq9" by Th14 .=seq19(#)(seq1(#)seq")(#)seq9" by Th14 .=seq19(#)((seq1(#)seq")(#)seq9") by Th14 .=seq19(#)(seq1(#)(seq"(#)seq9")) by Th14 .=seq19(#)seq1(#)(seq"(#)seq9") by Th14 .=(seq19(#)seq1)/"(seq(#)seq9) by Th34; end; theorem Th50: abs(seq(#)seq9)=abs(seq)(#)abs(seq9) proof now let n be Element of NAT; thus (abs(seq(#)seq9)).n=|.(seq(#)seq9).n.| by Th12 .=|.(seq.n)*(seq9.n).| by Th8 .= |.seq.n.|*|.seq9.n.| by COMPLEX1:65 .= ((abs(seq)).n)*|.seq9.n.| by Th12 .=((abs(seq)).n)*(abs(seq9)).n by Th12 .=(abs(seq)(#)abs(seq9)).n by Th8; end; hence thesis by FUNCT_2:63; end; theorem seq is non-zero implies abs(seq) is non-zero proof assume A1: seq is non-zero; now let n; seq.n<>0 by A1,Th5; then |.seq.n.|<>0 by COMPLEX1:47; hence (abs(seq)).n<>0 by Th12; end; hence thesis by Th5; end; theorem Th52: abs(seq)"=abs(seq") proof now let n be Element of NAT; thus (abs(seq")).n=|.seq".n.| by Th12 .=|.(seq.n)".| by VALUED_1:10 .=|.1/(seq.n).| by XCMPLX_1:215 .=1/|.seq.n.| by ABSVALUE:7 .=(|.seq.n.|)" by XCMPLX_1:215 .=(abs(seq).n)" by Th12 .=(abs(seq))".n by VALUED_1:10; end; hence thesis by FUNCT_2:63; end; theorem abs(seq9/"seq)=abs(seq9)/"abs(seq) proof thus abs(seq9/"seq)=abs(seq9)(#)abs(seq") by Th50 .=abs(seq9)/"abs(seq) by Th52; end; theorem abs(r(#)seq)=|.r.|(#)abs(seq) proof now let n be Element of NAT; thus abs(r(#)seq).n=|.(r(#)seq).n.| by Th12 .=|.r*(seq.n).| by Th9 .=|.r.|*|.seq.n.| by COMPLEX1:65 .=|.r.|*(abs(seq)).n by Th12 .=(|.r.|(#)abs(seq)).n by Th9; end; hence thesis by FUNCT_2:63; end; definition let b be Real; func seq_const b -> Real_Sequence equals NAT --> b; coherence proof reconsider b as Element of REAL by XREAL_0:def 1; NAT --> b is Real_Sequence; hence thesis; end; end; registration let b be Real; cluster seq_const b -> constant; coherence; end; registration let b be non zero Real; cluster seq_const b -> non-zero; coherence proof rng seq_const b = {b} by FUNCOP_1:8; hence not 0 in rng seq_const b by TARSKI:def 1; end; end; registration cluster constant for Real_Sequence; existence proof take seq_const 0; thus thesis; end; end; theorem for a being Real, k being Nat holds (seq_const a).k = a by ORDINAL1:def 12,FUNCOP_1:7;