:: Monotone Real Sequences. Subsequences
:: by Jaros{\l}aw Kotowicz
::
:: Received November 23, 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 NUMBERS, SUBSET_1, SEQ_1, ARYTM_3, NAT_1, CARD_1, FUNCT_1,
XXREAL_0, PARTFUN1, ORDINAL2, RELAT_1, TARSKI, VALUED_0, ARYTM_1,
VALUED_1, XXREAL_2, REAL_1, COMPLEX1, FINSEQ_1, SEQM_3, XBOOLE_0,
FINSEQ_3, FUNCT_7, NUMBER09;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_3, FINSEQ_1, FINSEQ_3,
VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, REAL_1, COMPLEX1, NAT_1, VALUED_0;
constructors PARTFUN1, FUNCT_3, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, COMPLEX1,
VALUED_1, SEQ_2, FINSEQ_1, RECDEF_1, RELSET_1, FINSEQ_3, COMSEQ_2;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0,
XREAL_0, MEMBERED, VALUED_0, FUNCT_2, VALUED_1, RFUNCT_1, RELAT_1, NAT_1,
FINSEQ_1, CARD_1, INT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, SEQ_2, FUNCT_1;
equalities VALUED_1;
expansions SEQ_2, FUNCT_1, VALUED_0, VALUED_1;
theorems FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, NAT_1, FUNCT_2, XREAL_1, XXREAL_0,
ORDINAL1, VALUED_0, VALUED_1, RELAT_1, COMPLEX1, INT_1, FINSEQ_1,
FINSEQ_3, XBOOLE_1, TARSKI, NUMBERS;
schemes NAT_1;
begin
reserve n,m,k for Nat;
reserve r,r1 for Real;
reserve f,seq,seq1 for Real_Sequence;
reserve x,y for set;
Lm1: n<m implies ex k st m=n+1+k
proof
assume
A1: n<m;
then consider k1 be Nat such that
A2: m=n+k1 by NAT_1:10;
k1 <> 0 by A1,A2;
then consider n1 be Nat such that
A3: k1=n1+1 by NAT_1:6;
reconsider n1 as Element of NAT by ORDINAL1:def 12;
take n1;
thus thesis by A2,A3;
end;
Lm2: ((for n holds seq.n<seq.(n+1)) implies for n,k holds seq.n<seq.(n+1+k)) &
((for n,k holds seq.n<seq.(n+1+k)) implies for n,m st n<m holds seq.n<seq.m) &
((for n,m st n<m holds seq.n<seq.m) implies for n holds seq.n<seq.(n+1))
proof
thus (for n holds seq.n<seq.(n+1)) implies for n,k holds seq.n<seq.(n+1+k)
proof
assume
A1: for n holds seq.n<seq.(n+1);
let n;
defpred X[Nat] means seq.n<seq.(n+1+$1);
A2: now
let k such that
A3: X[k];
seq.(n+1+k)<seq.(n+1+k+1) by A1;
hence X[k+1] by A3,XXREAL_0:2;
end;
A4: X[0] by A1;
thus for k holds X[k] from NAT_1:sch 2(A4,A2);
end;
thus (for n,k holds seq.n<seq.(n+1+k)) implies for n,m st n<m holds seq.n<
seq.m
proof
assume
A5: for n,k holds seq.n<seq.(n+1+k);
let n,m;
assume n<m;
then ex k st m=n+1+k by Lm1;
hence thesis by A5;
end;
assume
A6: for n,m st n<m holds seq.n<seq.m;
let n;
n<n+1 by NAT_1:13;
hence thesis by A6;
end;
Lm3: ((for n holds seq.(n+1)<seq.n) implies for n,k holds seq.(n+1+k)<seq.n) &
((for n,k holds seq.(n+1+k)<seq.n) implies for n,m st n<m holds seq.m<seq.n) &
((for n,m st n<m holds seq.m<seq.n) implies for n holds seq.(n+1)<seq.n)
proof
thus (for n holds seq.(n+1)<seq.n) implies for n,k holds seq.(n+1+k)<seq.n
proof
assume
A1: for n holds seq.(n+1)<seq.n;
let n;
defpred X[Nat] means seq.(n+1+$1)<seq.n;
A2: now
let k such that
A3: X[k];
seq.(n+1+k+1)<seq.(n+1+k) by A1;
hence X[k+1] by A3,XXREAL_0:2;
end;
A4: X[0] by A1;
thus for k holds X[k] from NAT_1:sch 2(A4,A2);
end;
thus (for n,k holds seq.(n+1+k)<seq.n) implies for n,m st n<m holds seq.m<
seq.n
proof
assume
A5: for n,k holds seq.(n+1+k)<seq.n;
let n,m;
assume n<m;
then ex k st m=n+1+k by Lm1;
hence thesis by A5;
end;
assume
A6: for n,m st n<m holds seq.m<seq.n;
let n;
n<n+1 by NAT_1:13;
hence thesis by A6;
end;
Lm4: ((for n holds seq.n<=seq.(n+1)) implies for n,k holds seq.n<=seq.(n+k)) &
((for n,k holds seq.n<=seq.(n+k)) implies for n,m st n<=m holds seq.n<=seq.m) &
((for n,m st n<=m holds seq.n<=seq.m) implies for n holds seq.n<=seq.(n+1))
proof
thus (for n holds seq.n<=seq.(n+1)) implies for n,k holds seq.n<=seq.(n+k)
proof
assume
A1: for n holds seq.n<=seq.(n+1);
let n;
defpred X[Nat] means seq.n<=seq.(n+$1);
A2: now
let k such that
A3: X[k];
seq.(n+k)<=seq.(n+k+1) by A1;
hence X[k+1] by A3,XXREAL_0:2;
end;
A4: X[0];
thus for k holds X[k] from NAT_1:sch 2(A4,A2);
end;
thus (for n,k holds seq.n<=seq.(n+k)) implies for n,m st n<=m holds seq.n<=
seq.m
proof
assume
A5: for n,k holds seq.n<=seq.(n+k);
let n,m;
assume n<=m;
then consider k1 be Nat such that
A6: m=n+k1 by NAT_1:10;
thus thesis by A5,A6;
end;
assume
A7: for n,m st n<=m holds seq.n<=seq.m;
let n;
n<=n+1 by NAT_1:13;
hence thesis by A7;
end;
Lm5: ((for n holds seq.(n+1)<=seq.n) implies for n,k holds seq.(n+k)<=seq.n) &
((for n,k holds seq.(n+k)<=seq.n) implies for n,m st n<=m holds seq.m<=seq.n) &
((for n,m st n<=m holds seq.m<=seq.n) implies for n holds seq.(n+1)<=seq.n)
proof
thus (for n holds seq.(n+1)<=seq.n) implies for n,k holds seq.(n+k)<=seq.n
proof
assume
A1: for n holds seq.(n+1)<=seq.n;
let n;
defpred X[Nat] means seq.(n+$1)<=seq.n;
A2: now
let k such that
A3: X[k];
seq.(n+k+1)<=seq.(n+k) by A1;
hence X[k+1] by A3,XXREAL_0:2;
end;
A4: X[0];
thus for k holds X[k] from NAT_1:sch 2(A4,A2);
end;
thus (for n,k holds seq.(n+k)<=seq.n) implies for n,m st n<=m holds seq.m<=
seq.n
proof
assume
A5: for n,k holds seq.(n+k)<=seq.n;
let n,m;
assume n<=m;
then consider k1 be Nat such that
A6: m=n+k1 by NAT_1:10;
thus thesis by A5,A6;
end;
assume
A7: for n,m st n<=m holds seq.m<=seq.n;
let n;
n<=n+1 by NAT_1:13;
hence thesis by A7;
end;
::
:: DEFINITIONS OF MONOTONE AND CONSTANT SEQUENCES
::
reserve e1,e2 for ExtReal;
definition
let f be NAT-defined real-valued Function;
redefine attr f is increasing means :: redefines increasing (VALUED_0, definition)
for m,n st m in dom f & n in dom f & m < n holds f.m < f.n;
compatibility;
redefine attr f is decreasing means :: redefines decreasing (VALUED_0, definition)
for m,n st m in dom f & n in dom f & m < n holds f.m > f.n;
compatibility;
redefine attr f is non-decreasing means :: redefines non-decreasing (VALUED_0, definition)
for m,n st m in dom f & n in dom f & m <= n holds f.m <= f.n;
compatibility;
redefine attr f is non-increasing means :: redefines non-increasing (VALUED_0, definition)
for m,n st m in dom f & n in dom f & m <= n holds f.m >= f.n;
compatibility;
end;
definition
let seq;
attr seq is monotone means
seq is non-decreasing or seq is non-increasing;
end;
theorem Th1:
seq is increasing iff for n,m st n<m holds seq.n<seq.m
proof
thus seq is increasing implies for n,m st n<m holds seq.n<seq.m
proof
assume seq is increasing;
then for n holds seq.n<seq.(n+1);
then for n,k holds seq.n<seq.(n+1+k) by Lm2;
hence thesis by Lm2;
end;
assume
A1: for n,m st n<m holds seq.n<seq.m;
let n,m;
assume that
n in dom seq and
m in dom seq and
A2: n < m;
thus thesis by A1,A2;
end;
theorem
seq is increasing iff for n,k holds seq.n<seq.(n+1+k)
by Lm2;
theorem Th3:
seq is decreasing iff for n,k holds seq.(n+1+k)<seq.n
by Lm3;
theorem Th4:
seq is decreasing iff for n,m st n<m holds seq.m<seq.n
proof
thus seq is decreasing implies for n,m st n<m holds seq.m<seq.n
proof
assume seq is decreasing;
then for n,k holds seq.(n+1+k)<seq.n by Th3;
hence thesis by Lm3;
end;
assume
A1: for n,m st n<m holds seq.m<seq.n;
let n,m;
assume that
n in dom seq and
m in dom seq and
A2: n < m;
thus thesis by A1,A2;
end;
theorem Th5:
seq is non-decreasing iff for n,k holds seq.n<=seq.(n+k)
by Lm4;
theorem Th6:
seq is non-decreasing iff for n,m st n<=m holds seq.n<=seq.m
proof
thus seq is non-decreasing implies for n,m st n<=m holds seq.n<=seq.m
proof
assume seq is non-decreasing;
then for n,k holds seq.n<=seq.(n+k) by Th5;
hence thesis by Lm4;
end;
assume
A1: for n,m st n<=m holds seq.n<=seq.m;
let n,m;
assume that
n in dom seq and
m in dom seq and
A2: n <= m;
thus thesis by A1,A2;
end;
theorem Th7:
seq is non-increasing iff for n,k holds seq.(n+k)<=seq.n
by Lm5;
theorem Th8:
seq is non-increasing iff for n,m st n<=m holds seq.m<=seq.n
proof
thus seq is non-increasing implies for n,m st n<=m holds seq.m<=seq.n
proof
assume seq is non-increasing;
then for n,k holds seq.(n+k)<=seq.n by Th7;
hence thesis by Lm5;
end;
assume
A1: for n,m st n<=m holds seq.m<=seq.n;
let n,m;
assume that
n in dom seq and
m in dom seq and
A2: n <= m;
thus thesis by A1,A2;
end;
::
:: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES
::
theorem
seq is increasing implies for n st 0<n holds seq.0<seq.n by Th1;
theorem
seq is decreasing implies for n st 0<n holds seq.n<seq.0 by Th4;
theorem Th11:
seq is non-decreasing implies for n holds seq.0<=seq.n by Th6;
theorem Th12:
seq is non-increasing implies for n holds seq.n<=seq.0 by Th8;
registration
cluster constant -> non-decreasing non-increasing for PartFunc of NAT, REAL;
coherence;
cluster non-decreasing non-increasing -> constant for PartFunc of NAT, REAL;
coherence
proof
let f be PartFunc of NAT, REAL such that
A1: f is non-decreasing non-increasing;
let x,y be object;
assume
A2: x in dom f & y in dom f;
dom f c= NAT by RELAT_1:def 18;
then reconsider m = x, n = y as Element of NAT by A2;
m <= n or n <= m;
then f.m <= f.n & f.n <= f.m by A1,A2;
hence thesis by XXREAL_0:1;
end;
end;
:: DEFINITIONS OF INCREASING SEQUENCE OF NATURAL NUMBERS,
:: RESTRICTION OF SEQUENCE.
Lm6: id NAT is increasing natural-valued;
registration
cluster increasing natural-valued for Real_Sequence;
existence
proof
reconsider i = id NAT as Real_Sequence by FUNCT_2:7, NUMBERS:19;
take i;
thus thesis;
end;
end;
registration
cluster increasing for sequence of NAT;
existence by Lm6;
end;
Lm7: for f being sequence of NAT holds f is increasing iff
for n being Nat holds f.n < f.(n+1);
reserve Nseq for increasing sequence of NAT;
theorem
seq is sequence of NAT iff for n holds seq.n is Element of NAT
proof
thus seq is sequence of NAT implies for n holds seq.n is Element of NAT
by ORDINAL1:def 12;
assume
A1: for n holds seq.n is Element of NAT;
rng seq c= NAT
proof
let x be object;
assume x in rng seq;
then consider y being object such that
A2: y in dom seq and
A3: x = seq.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A2,FUNCT_2:def 1;
x = seq.y by A3;
then x is Element of NAT by A1;
hence thesis;
end;
hence thesis by FUNCT_2:6;
end;
registration
let Nseq,k;
cluster Nseq ^\ k -> increasing natural-valued for ext-real-valued Function;
coherence
proof
now
let n;
Nseq.(n+k)<Nseq.(n+k+1) by Lm7;
then (Nseq ^\k).n<Nseq.(n+1+k) by NAT_1:def 3;
hence (Nseq ^\k).n<(Nseq ^\k).(n+1) by NAT_1:def 3;
end;
hence thesis by Lm7;
end;
end;
definition
let f be Real_Sequence;
redefine attr f is increasing means :: redefines increasing (SEQM_3, redefinition) → increasing (VALUED_0, definition)
for n being Nat holds f.n < f.(n+1);
compatibility;
redefine attr f is decreasing means :: redefines decreasing (SEQM_3, redefinition) → decreasing (VALUED_0, definition)
for n being Nat holds f.n > f.(n+1);
compatibility;
redefine attr f is non-decreasing means :: redefines non-decreasing (SEQM_3, redefinition) → non-decreasing (VALUED_0, definition)
for n being Nat holds f.n <= f.(n+1);
compatibility;
redefine attr f is non-increasing means :: redefines non-increasing (SEQM_3, redefinition) → non-increasing (VALUED_0, definition)
for n being Nat holds f.n >= f.(n+1);
compatibility;
end;
theorem
for n holds n<=Nseq.n
proof
defpred X[Nat] means $1<=Nseq.$1;
A1: now
let k such that
A2: X[k];
Nseq.k<Nseq.(k+1) by Lm7;
then k<Nseq.(k+1) by A2,XXREAL_0:2;
hence X[k+1] by NAT_1:13;
end;
A3: X[0];
thus for k holds X[k] from NAT_1:sch 2(A3,A1);
end;
registration
let s be Real_Sequence, k be Nat;
cluster s^\k ->real-valued;
coherence;
end;
theorem Th15:
(seq+seq1) ^\k=(seq ^\k) + (seq1 ^\k)
proof
now
let n be Element of NAT;
thus ((seq+seq1) ^\k).n=(seq+seq1).(n+k) by NAT_1:def 3
.=seq.(n+k) + seq1.(n+k) by SEQ_1:7
.=(seq ^\k).n +seq1.(n+k) by NAT_1:def 3
.=(seq ^\k).n +(seq1 ^\k).n by NAT_1:def 3
.=((seq ^\k) +(seq1 ^\k)).n by SEQ_1:7;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th16:
(-seq) ^\k=-(seq ^\k)
proof
now
let n be Element of NAT;
thus ((-seq) ^\k).n=(-seq).(n+k) by NAT_1:def 3
.=-(seq.(n+k)) by SEQ_1:10
.=-((seq ^\ k).n) by NAT_1:def 3
.=(-(seq ^\k)).n by SEQ_1:10;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq-seq1) ^\k=(seq ^\k)-(seq1 ^\k)
proof
thus (seq-seq1) ^\k=(seq ^\k)+((-seq1) ^\k) by Th15
.=(seq ^\k)-(seq1 ^\k) by Th16;
end;
theorem Th18:
(seq") ^\k=(seq ^\k)"
proof
now
let n be Element of NAT;
thus ((seq") ^\k).n=(seq").(n+k) by NAT_1:def 3
.=(seq.(n+k))" by VALUED_1:10
.=((seq ^\k).n)" by NAT_1:def 3
.=((seq ^\k)").n by VALUED_1:10;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th19:
(seq(#)seq1) ^\k=(seq ^\k)(#)(seq1 ^\k)
proof
now
let n be Element of NAT;
thus ((seq(#)seq1) ^\k).n=(seq(#)seq1).(n+k) by NAT_1:def 3
.=seq.(n+k)*seq1.(n+k) by SEQ_1:8
.=(seq ^\k).n*seq1.(n+k) by NAT_1:def 3
.=(seq ^\k).n*(seq1 ^\k).n by NAT_1:def 3
.=((seq ^\k)(#)(seq1 ^\k)).n by SEQ_1:8;
end;
hence thesis by FUNCT_2:63;
end;
theorem
(seq/"seq1) ^\k=(seq ^\k)/"(seq1 ^\k)
proof
thus (seq/"seq1) ^\k=(seq ^\k)(#)((seq1") ^\k) by Th19
.=(seq ^\k)/"(seq1 ^\k) by Th18;
end;
theorem
(r(#)seq) ^\k=r(#)(seq ^\k)
proof
now
let n be Element of NAT;
thus ((r(#)seq) ^\k).n=(r(#)seq).(n+k) by NAT_1:def 3
.=r*(seq.(n+k)) by SEQ_1:9
.=r*((seq ^\k).n) by NAT_1:def 3
.=(r(#)(seq ^\k)).n by SEQ_1:9;
end;
hence thesis by FUNCT_2:63;
end;
::
:: SUBSEQUENCES OF MONOTONE SEQUENCE
:: SUBSEQUENCE OF BOUNDED SEQUENCE
::
theorem
seq is increasing & seq1 is subsequence of seq implies seq1 is increasing
proof
assume that
A1: seq is increasing and
A2: seq1 is subsequence of seq;
let n;
consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
A4: n in NAT by ORDINAL1:def 12;
Nseq.n<Nseq.(n+1) by Lm7;
then (seq.(Nseq.n))<(seq.(Nseq.(n+1))) by A1,Th1;
then (seq*Nseq).n<(seq.(Nseq.(n+1))) by FUNCT_2:15,A4;
hence thesis by A3,FUNCT_2:15;
end;
theorem
seq is decreasing & seq1 is subsequence of seq implies seq1 is decreasing
proof
assume that
A1: seq is decreasing and
A2: seq1 is subsequence of seq;
let n;
consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
A4: n in NAT by ORDINAL1:def 12;
Nseq.n<Nseq.(n+1) by Lm7;
then seq.(Nseq.(n+1))<seq.(Nseq.n) by A1,Th4;
then (seq*Nseq).(n+1)<seq.(Nseq.n) by FUNCT_2:15;
hence thesis by A3,FUNCT_2:15,A4;
end;
theorem Th24:
seq is non-decreasing & seq1 is subsequence of seq implies seq1
is non-decreasing
proof
assume that
A1: seq is non-decreasing and
A2: seq1 is subsequence of seq;
let n;
consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
A4: n in NAT by ORDINAL1:def 12;
Nseq.n<=Nseq.(n+1) by Lm7;
then (seq.(Nseq.n))<=(seq.(Nseq.(n+1))) by A1,Th6;
then (seq*Nseq).n<=(seq.(Nseq.(n+1))) by FUNCT_2:15,A4;
hence thesis by A3,FUNCT_2:15;
end;
theorem Th25:
seq is non-increasing & seq1 is subsequence of seq implies seq1
is non-increasing
proof
assume that
A1: seq is non-increasing and
A2: seq1 is subsequence of seq;
let n;
consider Nseq such that
A3: seq1=seq*Nseq by A2,VALUED_0:def 17;
A4: n in NAT by ORDINAL1:def 12;
Nseq.n<=Nseq.(n+1) by Lm7;
then (seq.(Nseq.(n+1)))<=(seq.(Nseq.n)) by A1,Th8;
then (seq*Nseq).(n+1)<=(seq.(Nseq.n)) by FUNCT_2:15;
hence thesis by A3,FUNCT_2:15,A4;
end;
theorem
seq is monotone & seq1 is subsequence of seq implies seq1 is monotone
by Th25,Th24;
theorem Th27:
seq is bounded_above & seq1 is subsequence of seq implies seq1
is bounded_above
proof
assume that
A1: seq is bounded_above and
A2: seq1 is subsequence of seq;
consider r1 such that
A3: for n holds seq.n<r1 by A1;
consider Nseq such that
A4: seq1=seq*Nseq by A2,VALUED_0:def 17;
take r=r1;
let n be Nat;
n in NAT by ORDINAL1:def 12;
then seq1.n=seq.(Nseq.n) by A4,FUNCT_2:15;
hence seq1.n<r by A3;
end;
theorem Th28:
seq is bounded_below & seq1 is subsequence of seq implies seq1
is bounded_below
proof
assume that
A1: seq is bounded_below and
A2: seq1 is subsequence of seq;
consider r1 such that
A3: for n holds r1<seq.n by A1;
consider Nseq such that
A4: seq1=seq*Nseq by A2,VALUED_0:def 17;
take r=r1;
let n be Nat;
n in NAT by ORDINAL1:def 12;
then seq1.n=seq.(Nseq.n) by A4,FUNCT_2:15;
hence r<seq1.n by A3;
end;
theorem
seq is bounded & seq1 is subsequence of seq implies seq1 is bounded
by Th27,Th28;
::
:: OPERATIONS ON MONOTONE SEQUENCES
::
theorem
(seq is increasing & 0<r implies r(#)seq is increasing) & (0=r implies
r(#)seq is constant) & (seq is increasing & r<0 implies r(#)seq is decreasing)
proof
thus seq is increasing & 0<r implies r(#)seq is increasing
proof
assume that
A1: seq is increasing and
A2: 0<r;
let n;
seq.n<seq.(n+1) by A1;
then r*seq.n<r*seq.(n+1) by A2,XREAL_1:68;
then (r(#)seq).n<r*seq.(n+1) by SEQ_1:9;
hence thesis by SEQ_1:9;
end;
thus 0=r implies r(#)seq is constant
proof
assume
A3: 0=r;
now
let n be Nat;
n in NAT & r*seq.n=r*seq.(n+1) by A3,ORDINAL1:def 12;
then (r(#)seq).n=r*seq.(n+1) by SEQ_1:9;
hence (r(#)seq).n=(r(#)seq).(n+1) by SEQ_1:9;
end;
hence thesis by VALUED_0:25;
end;
assume that
A4: seq is increasing and
A5: r<0;
let n;
seq.n<seq.(n+1) by A4;
then r*seq.(n+1)<r*seq.n by A5,XREAL_1:69;
then (r(#)seq).(n+1)<r*seq.n by SEQ_1:9;
hence thesis by SEQ_1:9;
end;
theorem
(seq is decreasing & 0<r implies r(#)seq is decreasing) & (seq is
decreasing & r<0 implies r(#)seq is increasing)
proof
thus seq is decreasing & 0<r implies r(#)seq is decreasing
proof
assume that
A1: seq is decreasing and
A2: 0<r;
let n;
seq.(n+1)<seq.n by A1;
then r*seq.(n+1)<r*seq.n by A2,XREAL_1:68;
then (r(#)seq).(n+1)<r*seq.n by SEQ_1:9;
hence thesis by SEQ_1:9;
end;
assume that
A3: seq is decreasing and
A4: r<0;
let n;
seq.(n+1)<seq.n by A3;
then r*seq.n<r*seq.(n+1) by A4,XREAL_1:69;
then (r(#)seq).n<r*seq.(n+1) by SEQ_1:9;
hence thesis by SEQ_1:9;
end;
theorem
(seq is non-decreasing & 0<=r implies r(#)seq is non-decreasing) & (
seq is non-decreasing & r<=0 implies r(#)seq is non-increasing)
proof
thus seq is non-decreasing & 0<=r implies r(#)seq is non-decreasing
proof
assume that
A1: seq is non-decreasing and
A2: 0<=r;
let n;
seq.n<=seq.(n+1) by A1;
then r*seq.n<=r*seq.(n+1) by A2,XREAL_1:64;
then (r(#)seq).n<=r*seq.(n+1) by SEQ_1:9;
hence thesis by SEQ_1:9;
end;
assume that
A3: seq is non-decreasing and
A4: r<=0;
let n;
seq.n<=seq.(n+1) by A3;
then r*seq.(n+1)<=r*seq.n by A4,XREAL_1:65;
then (r(#)seq).(n+1)<=r*seq.n by SEQ_1:9;
hence thesis by SEQ_1:9;
end;
theorem
(seq is non-increasing & 0<=r implies r(#)seq is non-increasing) & (
seq is non-increasing & r<=0 implies r(#)seq is non-decreasing)
proof
thus seq is non-increasing & 0<=r implies r(#)seq is non-increasing
proof
assume that
A1: seq is non-increasing and
A2: 0<=r;
let n;
seq.(n+1)<=seq.n by A1;
then r*seq.(n+1)<=r*seq.n by A2,XREAL_1:64;
then (r(#)seq).(n+1)<=r*seq.n by SEQ_1:9;
hence thesis by SEQ_1:9;
end;
assume that
A3: seq is non-increasing and
A4: r<=0;
let n;
seq.(n+1)<=seq.n by A3;
then r*seq.n<=r*seq.(n+1) by A4,XREAL_1:65;
then (r(#)seq).n<=r*seq.(n+1) by SEQ_1:9;
hence thesis by SEQ_1:9;
end;
theorem Th34:
(seq is increasing & seq1 is increasing implies seq+seq1 is
increasing) & (seq is decreasing & seq1 is decreasing implies seq+seq1 is
decreasing) & (seq is non-decreasing & seq1 is non-decreasing implies seq+seq1
is non-decreasing) & (seq is non-increasing & seq1 is non-increasing implies
seq+seq1 is non-increasing)
proof
thus seq is increasing & seq1 is increasing implies seq+seq1 is increasing
proof
assume
A1: seq is increasing & seq1 is increasing;
let n;
seq.n<seq.(n+1) & seq1.n<seq1.(n+1) by A1;
then seq.n+seq1.n<seq.(n+1)+seq1.(n+1) by XREAL_1:8;
then (seq+seq1).n<seq.(n+1)+seq1.(n+1) by SEQ_1:7;
hence thesis by SEQ_1:7;
end;
thus seq is decreasing & seq1 is decreasing implies seq+seq1 is decreasing
proof
assume
A2: seq is decreasing & seq1 is decreasing;
let n;
seq.(n+1)<seq.n & seq1.(n+1)<seq1.n by A2;
then seq.(n+1)+seq1.(n+1)<seq.n+seq1.n by XREAL_1:8;
then (seq+seq1).(n+1)<seq.n+seq1.n by SEQ_1:7;
hence thesis by SEQ_1:7;
end;
thus seq is non-decreasing & seq1 is non-decreasing implies seq+seq1 is
non-decreasing
proof
assume
A3: seq is non-decreasing & seq1 is non-decreasing;
let n;
seq.n<=seq.(n+1) & seq1.n<=seq1.(n+1) by A3;
then seq.n+seq1.n<=seq.(n+1)+seq1.(n+1) by XREAL_1:7;
then (seq+seq1).n<=seq.(n+1)+seq1.(n+1) by SEQ_1:7;
hence thesis by SEQ_1:7;
end;
assume
A4: seq is non-increasing & seq1 is non-increasing;
let n;
seq.(n+1)<=seq.n & seq1.(n+1)<=seq1.n by A4;
then seq.(n+1)+seq1.(n+1)<=seq.n+seq1.n by XREAL_1:7;
then (seq+seq1).(n+1)<=seq.n+seq1.n by SEQ_1:7;
hence thesis by SEQ_1:7;
end;
theorem
(seq is increasing & seq1 is constant implies seq+seq1 is increasing)
& (seq is decreasing & seq1 is constant implies seq+seq1 is decreasing) & (seq
is non-decreasing & seq1 is constant implies seq+seq1 is non-decreasing) & (seq
is non-increasing & seq1 is constant implies seq+seq1 is non-increasing)
proof
thus seq is increasing & seq1 is constant implies seq+seq1 is increasing
proof
assume that
A1: seq is increasing and
A2: seq1 is constant;
let n;
consider r1 being Element of REAL such that
A3: for n being Nat holds seq1.n=r1 by A2;
seq.n<seq.(n+1) by A1;
then seq.n+r1<seq.(n+1)+r1 by XREAL_1:6;
then seq.n+seq1.n<seq.(n+1)+r1 by A3;
then seq.n+seq1.n<seq.(n+1)+seq1.(n+1) by A3;
then (seq+seq1).n<seq.(n+1)+seq1.(n+1) by SEQ_1:7;
hence thesis by SEQ_1:7;
end;
thus seq is decreasing & seq1 is constant implies seq+seq1 is decreasing
proof
assume that
A4: seq is decreasing and
A5: seq1 is constant;
let n;
consider r1 being Element of REAL such that
A6: for n being Nat holds seq1.n=r1 by A5;
seq.(n+1)<seq.n by A4;
then seq.(n+1)+r1<seq.n+r1 by XREAL_1:6;
then seq.(n+1)+seq1.(n+1)<seq.n+r1 by A6;
then seq.(n+1)+seq1.(n+1)<seq.n+seq1.n by A6;
then (seq+seq1).(n+1)<seq.n+seq1.n by SEQ_1:7;
hence thesis by SEQ_1:7;
end;
thus seq is non-decreasing & seq1 is constant implies seq+seq1 is
non-decreasing by Th34;
assume seq is non-increasing & seq1 is constant;
hence thesis by Th34;
end;
::
:: OPERATIONS ON BOUNDED SEQUENCES
::
theorem Th36:
(seq is bounded_above & 0<r implies r(#)seq is bounded_above) &
(0=r implies r(#)seq is bounded) & (seq is bounded_above & r<0 implies r(#)seq
is bounded_below)
proof
thus seq is bounded_above & 0<r implies r(#)seq is bounded_above;
thus 0=r implies r(#)seq is bounded
proof
assume
A1: 0=r;
now
let n;
(r(#)seq).n = 0*seq.n by A1,SEQ_1:9;
hence (r(#)seq).n < 1;
end;
hence r(#)seq is bounded_above;
take p=-1;
let n be Nat;
-1<0 & r*seq.n=0 by A1;
hence p<(r(#)seq).n by SEQ_1:9;
end;
assume that
A2: seq is bounded_above and
A3: r<0;
consider r1 such that
A4: for n holds seq.n<r1 by A2;
take p=r*|.r1.|;
let n be Nat;
r1<=|.r1.| by ABSVALUE:4;
then seq.n<|.r1.| by A4,XXREAL_0:2;
then r*|.r1.|<r*seq.n by A3,XREAL_1:69;
hence p<(r(#)seq).n by SEQ_1:9;
end;
theorem
(seq is bounded implies for r holds r(#)seq is bounded) & (seq is
bounded implies -seq is bounded) & (seq is bounded iff abs seq is bounded)
proof
thus seq is bounded implies for r holds r(#)seq is bounded
proof
assume
A1: seq is bounded;
let r;
per cases;
suppose
0<r;
hence thesis by A1;
end;
suppose
0=r;
hence thesis by Th36;
end;
suppose
r<0;
hence thesis by A1;
end;
end;
thus seq is bounded implies -seq is bounded;
thus seq is bounded implies abs seq is bounded;
assume abs seq is bounded;
then consider r be Real such that
A2: 0<r and
A3: for n be Nat holds |.abs seq.n.|<r by SEQ_2:3;
now
let n be Nat;
|.abs seq .n.|=|.|.seq.n.|.| by SEQ_1:12
.=|.seq.n.|;
hence |.seq.n.| < r by A3;
end;
hence thesis by A2,SEQ_2:3;
end;
::
:: OPERATIONS ON BOUNDED & MONOTONE SEQUENCES
::
theorem
seq is bounded_above & seq1 is non-increasing implies seq+seq1 is
bounded_above
proof
assume that
A1: seq is bounded_above and
A2: seq1 is non-increasing;
consider r1 such that
A3: for n holds seq.n<r1 by A1;
take r=r1+seq1.0;
let n be Nat;
seq1.n<=seq1.0 by A2,Th12;
then seq.n+seq1.n<r1+seq1.0 by A3,XREAL_1:8;
hence (seq+seq1).n<r by SEQ_1:7;
end;
theorem
seq is bounded_below & seq1 is non-decreasing implies seq+seq1 is
bounded_below
proof
assume that
A1: seq is bounded_below and
A2: seq1 is non-decreasing;
consider r1 such that
A3: for n holds r1<seq.n by A1;
take r=r1+seq1.0;
let n be Nat;
seq1.0<=seq1.n by A2,Th11;
then r1+seq1.0<seq.n+seq1.n by A3,XREAL_1:8;
hence r<(seq+seq1).n by SEQ_1:7;
end;
:::theorem
::: incl NAT is increasing natural-valued by Lm10;
registration
cluster -> natural-valued for FinSequence of NAT;
coherence;
end;
begin :: moved from GOBOARD1, 2010.03.01, A.T.
reserve v for FinSequence of REAL,
r,s for Real,
n,m,i,j,k for Nat;
::$CT
theorem Th40:
|.r-s.|=1 iff r>s & r=s+1 or r<s & s=r+1
proof
thus |.r-s.|=1 implies r>s & r=s+1 or r<s & s=r+1
proof
assume
A1: |.r-s.| = 1;
now
per cases by XXREAL_0:1;
case
A2: r>s;
then 0<r-s by XREAL_1:50;
then r-s=1 by A1,ABSVALUE:def 1;
hence thesis by A2;
end;
case
r=s;
hence contradiction by A1,ABSVALUE:2;
end;
case
A3: r<s;
then
A4: 0<s-r by XREAL_1:50;
1=|.-(r-s).| by A1,COMPLEX1:52
.=s-r by A4,ABSVALUE:def 1;
hence thesis by A3;
end;
end;
hence thesis;
end;
assume
A5: r>s & r=s+1 or r<s & s=r+1;
per cases by A5;
suppose
r>s & r=s+1;
hence thesis by ABSVALUE:def 1;
end;
suppose
A6: s>r & s=r+1;
thus |.r-s.|=|.-(r-s).| by COMPLEX1:52
.= 1 by A6,ABSVALUE:def 1;
end;
end;
theorem
|.i-j.|+|.n-m.|=1 iff |.i-j.|=1 & n=m or |.n-m.|=1 & i=j
proof
thus |.i-j.|+|.n-m.|=1 implies |.i-j.|=1 & n=m or |.n-m.|=1 & i=j
proof
assume
A1: |.i-j.|+|.n-m.|=1;
now
per cases;
suppose
A2: n=m;
then 1=|.i-j.|+|.0.| by A1
.=|.i-j.|+ (0 qua Real) by ABSVALUE:2
.= |.i-j.|;
hence thesis by A2;
end;
suppose
A3: n<>m;
now
per cases by A3,XXREAL_0:1;
suppose
A4: n<m;
reconsider l=m-n as Element of NAT by INT_1:5,A4;
0<l by A4,XREAL_1:50;
then
A5: 0+1<=l by NAT_1:13;
A6: |.-(m-n).|=|.l.| by COMPLEX1:52;
then
A7: |.n-m.|=|.l.|;
A8: |.l.|=l by ABSVALUE:def 1;
then
A9: l<=1 by A1,A6,COMPLEX1:46,XREAL_1:31;
then l=1 by A5,XXREAL_0:1;
then i-j=0 by A1,A8,A7,ABSVALUE:2;
hence thesis by A6,A5,A8,A9,XXREAL_0:1;
end;
suppose
A10: n>m;
then reconsider l=n-m as Element of NAT by INT_1:5;
0<l by A10,XREAL_1:50;
then
A11: 0+1<=l by NAT_1:13;
A12: |.n-m.|=l by ABSVALUE:def 1;
then
A13: l<=1 by A1,COMPLEX1:46,XREAL_1:31;
then l=1 by A11,XXREAL_0:1;
then i-j=0 by A1,A12,ABSVALUE:2;
hence thesis by A11,A12,A13,XXREAL_0:1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
assume
A14: |.i-j.|=1 & n=m or |.n-m.|=1 & i=j;
now
per cases by A14;
suppose
A15: |.i-j.|=1 & n=m;
then |.n-m.|=0 by ABSVALUE:2;
hence thesis by A15;
end;
suppose
A16: |.n-m.|=1 & i=j;
then |.i-j.|=0 by ABSVALUE:2;
hence thesis by A16;
end;
end;
hence thesis;
end;
theorem
n>1 iff ex m st n=m+1 & m>0
proof
thus n>1 implies ex m st n=m+1 & m>0
proof
assume
A1: 1<n;
then consider m being Nat such that
A2: n = m+1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
take m;
m <> 0 by A1,A2;
hence thesis by A2;
end;
given m such that
A3: n=m+1 & m>0;
0+1<n by A3,XREAL_1:6;
hence thesis;
end;
theorem
for f being FinSequence,n,m,k st len f = m+1 & n in dom f & k in Seg m
holds Del(f,n).k = f.k or Del(f,n).k = f.(k+1)
proof
let f be FinSequence,n,m,k such that
A1: len f = m+1 & n in dom f and
A2: k in Seg m;
set X = dom f \ {n};
A3: dom f=Seg len f by FINSEQ_1:def 3;
then
A4: n<=k & k<=m implies Sgm(X).k=k+1 by A1,A2,FINSEQ_3:108;
rng Sgm(X) = X by FINSEQ_1:def 14;
then
A5: dom (f*Sgm(X)) = dom Sgm(X) by RELAT_1:27,XBOOLE_1:36;
A6: dom Sgm(X)=Seg len Sgm(X) & Del(f,n) = f*Sgm(X) by FINSEQ_1:def 3
,FINSEQ_3:def 2;
A7: len Sgm(X) = m by A1,A3,FINSEQ_3:107;
1<=k & k<n implies Sgm(X).k=k by A1,A2,A3,FINSEQ_3:108;
hence thesis by A2,A6,A5,A7,A4,FINSEQ_3:25,FUNCT_1:12;
end;
definition
let f be FinSequence;
redefine attr f is constant means :: redefines constant (FUNCT_1, definition)
for n,m st n in dom f & m in dom f holds f.n=f.m;
compatibility;
end;
registration
cluster -> real-valued for FinSequence of REAL;
coherence;
end;
registration
cluster non empty increasing for FinSequence of REAL;
existence
proof
take v = <* In(0,REAL) *>;
thus v is non empty;
let n,m;
assume that
A1: n in dom v and
A2: m in dom v;
A3: dom<* 0 *> = { 1 } by FINSEQ_1:2,38;
then n = 1 by A1,TARSKI:def 1;
hence thesis by A3,A2,TARSKI:def 1;
end;
end;
registration
cluster constant for FinSequence of REAL;
existence
proof
take v = <*>REAL;
let n,m;
assume that
n in dom v and
m in dom v;
thus thesis;
end;
end;
theorem Th44:
v<>{} & rng v c= Seg n & v.(len v) = n & (for k st 1<=k & k<=len
v - 1 holds for r,s st r = v.k & s = v.(k+1) holds |.r-s.| = 1 or r=s) & i in
Seg n & i+1 in Seg n & m in dom v & v.m = i & (for k st k in dom v & v.k = i
holds k<=m) implies m+1 in dom v & v.(m+1)=i+1
proof
assume that
A1: v<>{} and
A2: rng v c= Seg n and
A3: v.(len v) = n and
A4: for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1)
holds |.r-s.| = 1 or r=s and
A5: i in Seg n and
A6: i+1 in Seg n and
A7: m in dom v and
A8: v.m = i and
A9: for k st k in dom v & v.k = i holds k<=m;
A10: m<=len v by A7,FINSEQ_3:25;
0+1<=len v by A1,NAT_1:13;
then
A11: len v in dom v by FINSEQ_3:25;
reconsider r=v.(m+1) as Real;
A12: i<=n by A5,FINSEQ_1:1;
A13: 1<=m by A7,FINSEQ_3:25;
A14: i+1<=n by A6,FINSEQ_1:1;
A15: now
assume not m+1 in dom v;
then 1>m+1 or m+1>len v by FINSEQ_3:25;
then
A16: len v <=m by NAT_1:11,13;
i<n by A14,NAT_1:13;
hence contradiction by A3,A8,A10,A16,XXREAL_0:1;
end;
then
A17: m+1<=len v by FINSEQ_3:25;
then
A18: m<len v by NAT_1:13;
A19: m<=len v - 1 by A17,XREAL_1:19;
now
per cases by A4,A8,A13,A19;
case
A20: |.i - r.| = 1;
now
per cases by A20,Th40;
case
A21: i>r & i=r+1;
defpred P[set] means for k,r st k=$1 & k>0 & m+k in dom v & r=v.(m+k
) holds r<i;
A22: for k st P[k] holds P[k+1]
proof
let k such that
A23: P[k];
let j,s such that
A24: j=k+1 and
A25: j>0 and
A26: m+j in dom v and
A27: s=v.(m+j);
now
per cases;
suppose
k=0;
hence thesis by A21,A24,A27;
end;
suppose
A28: k<>0;
A29: m+k<=m+k+1 by NAT_1:11;
m<=m+k by NAT_1:11;
then
A30: 1<=m+k by A13,XXREAL_0:2;
A31: m+(k+1)<=len v by A24,A26,FINSEQ_3:25;
then m+k<=len v by A29,XXREAL_0:2;
then
A32: m+k in dom v by A30,FINSEQ_3:25;
then v.(m+k) in rng v by FUNCT_1:def 3;
then v.(m+k) in Seg n by A2;
then reconsider r1=v.(m+k) as Element of NAT;
A33: r1<i by A23,A28,A32;
A34: m+k<=len v - 1 by A29,A31,XREAL_1:19;
now
per cases by A4,A24,A27,A29,A30,A34;
suppose
A35: |.r1-s.|=1;
now
per cases by A35,Th40;
suppose
r1>s & r1=s+1;
hence thesis by A33,XXREAL_0:2;
end;
suppose
r1<s & s=r1+1;
then
A36: s<=i by A33,NAT_1:13;
now
per cases by A36,XXREAL_0:1;
case
s<i;
hence thesis;
end;
case
s=i;
then m+j<=m by A9,A26,A27;
then j<=m-m by XREAL_1:19;
hence contradiction by A25;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
r1=s;
hence thesis by A23,A28,A32;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
reconsider l = len v - m as Element of NAT by A18,INT_1:5;
A37: 0< len v - m & m+l = len v by A17,XREAL_1:19;
A38: P[0];
for k holds P[k] from NAT_1:sch 2(A38,A22);
hence contradiction by A3,A11,A12,A37;
end;
case
i<r & r=i+1;
hence thesis by A15;
end;
end;
hence thesis;
end;
case
i=r;
then m+1<=m by A9,A15;
then 1<=m-m by XREAL_1:19;
then 1<=0;
hence contradiction;
end;
end;
hence thesis;
end;
theorem
v<>{} & rng v c= Seg n & v.1 = 1 & v.(len v) = n & (for k st 1<=k & k
<=len v - 1 holds for r,s st r = v.k & s = v.(k+1) holds |.r-s.| = 1 or r=s)
implies (for i st i in Seg n ex k st k in dom v & v.k = i) & for m,k,i,r st m
in dom v & v.m = i & (for j st j in dom v & v.j = i holds j<=m) & m<k & k in
dom v & r = v.k
holds i<r
proof
assume that
A1: v<>{} and
A2: rng v c= Seg n and
A3: v.1 = 1 and
A4: v.(len v) = n and
A5: for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1)
holds |.r-s.| = 1 or r=s;
defpred P[Nat] means
$1 in Seg n implies ex k st k in dom v & v.k = $1;
A6: 0+1<=len v by A1,NAT_1:13;
then
A7: len v in dom v by FINSEQ_3:25;
A8: for i st P[i] holds P[i+1]
proof
let i such that
A9: i in Seg n implies ex k st k in dom v & v.k = i;
assume
A10: i+1 in Seg n;
now
per cases;
suppose
A11: i = 0;
take k=1;
thus k in dom v & v.k = i+1 by A3,A6,A11,FINSEQ_3:25;
end;
suppose
A12: i<>0;
defpred R[set] means $1 in dom v & v.$1 = i;
A13: for k be Nat holds R[k] implies k<=len v by FINSEQ_3:25;
i+1<=n by A10,FINSEQ_1:1;
then
A14: i<=n by NAT_1:13;
A15: 0+1<=i by A12,NAT_1:13;
then
A16: ex k be Nat st R[k] by A9,A14,FINSEQ_1:1;
consider m be Nat such that
A17: R[m] & for k be Nat st R[k] holds k<=m from NAT_1:sch 6(A13,
A16);
reconsider m as Element of NAT by ORDINAL1:def 12;
take k = m+1;
i in Seg n by A15,A14,FINSEQ_1:1;
hence k in dom v & v.k = i+1 by A1,A2,A4,A5,A10,A17,Th44;
end;
end;
hence thesis;
end;
A18: P[0] by FINSEQ_1:1;
thus for i holds P[i] from NAT_1:sch 2(A18,A8);
let m,k,i,r;
assume that
A19: m in dom v and
A20: v.m = i and
A21: for j st j in dom v & v.j = i holds j<=m and
A22: m<k and
A23: k in dom v and
A24: r = v.k;
A25: m<=len v & k<=len v by A19,A23,FINSEQ_3:25;
A26: 1<=m by A19,FINSEQ_3:25;
A27: i in rng v by A19,A20,FUNCT_1:def 3;
then
A28: i<=n by A2,FINSEQ_1:1;
now
per cases;
suppose
i=n;
then len v<=m by A4,A7,A21;
hence thesis by A22,A25,XXREAL_0:1;
end;
suppose
A29: i<>n;
defpred P[set] means for j,s st j=$1 & j>0 & m+j in dom v & s=v.(m+j)
holds i<s;
i<n by A28,A29,XXREAL_0:1;
then 1<=i+1 & i+1<=n by NAT_1:11,13;
then i+1 in Seg n by FINSEQ_1:1;
then
A30: v.(m+1) = i+1 by A1,A2,A4,A5,A19,A20,A21,A27,Th44;
A31: for k st P[k] holds P[k+1]
proof
let k such that
A32: P[k];
let j,s such that
A33: j=k+1 and
A34: j>0 and
A35: m+j in dom v and
A36: s=v.(m+j);
per cases;
suppose
k=0;
hence thesis by A30,A33,A36,NAT_1:13;
end;
suppose
A37: k<>0;
m<=m+k by NAT_1:11;
then
A38: 1<=m+k by A26,XXREAL_0:2;
s in rng v by A35,A36,FUNCT_1:def 3;
then s in Seg n by A2;
then reconsider s1=s as Element of NAT;
A39: m+(k+1)<=len v by A33,A35,FINSEQ_3:25;
m+k<=m+k+1 by NAT_1:11;
then m+k<=len v by A39,XXREAL_0:2;
then
A40: m+k in dom v by A38,FINSEQ_3:25;
then v.(m+k) in rng v by FUNCT_1:def 3;
then v.(m+k) in Seg n by A2;
then reconsider r1=v.(m+k) as Element of NAT;
A41: i<r1 by A32,A37,A40;
A42: m+k+1 = m+(k+1);
then
A43: m+k<= len v - 1 by A39,XREAL_1:19;
now
per cases by A5,A33,A36,A42,A38,A43;
suppose
A44: |.r1-s.|=1;
now
per cases by A44,Th40;
suppose
r1>s & r1=s+1;
then
A45: i<=s1 by A41,NAT_1:13;
now
per cases by A45,XXREAL_0:1;
case
i<s;
hence thesis;
end;
case
s=i;
then m+j<=m by A21,A35,A36;
then j<=m-m by XREAL_1:19;
hence contradiction by A34;
end;
end;
hence thesis;
end;
suppose
r1<s & s=r1+1;
hence thesis by A41,XXREAL_0:2;
end;
end;
hence thesis;
end;
suppose
r1=s;
hence thesis by A32,A37,A40;
end;
end;
hence thesis;
end;
end;
reconsider l = k - m as Element of NAT by A22,INT_1:5;
A46: 0< k - m & m+l = k by A22,XREAL_1:50;
A47: P[0];
for k holds P[k] from NAT_1:sch 2(A47,A31);
hence thesis by A23,A24,A46;
end;
end;
hence thesis;
end;