:: Real Sequences and Basic Operations on Them
:: by Jaros{\l}aw Kotowicz
::
:: Received July 4, 1989
:: Copyright (c) 1990-2026 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;
definitions ORDINAL1;
equalities VALUED_1, ORDINAL1;
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 X2[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 X2[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 X2[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;
registration let k be object;
reduce (NAT --> 0).k to 0;
reducibility
proof
A1: dom (NAT --> 0) = NAT;
per cases;
suppose k in NAT;
hence thesis by FUNCOP_1:7;
end;
suppose not k in NAT;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
end;
registration
let k be object;
reduce (seq_const 0).k to 0;
reducibility;
end;