The Mizar article:

Monotone Real Sequences. Subsequences

by
Jaroslaw Kotowicz

Received November 23, 1989

Copyright (c) 1989 Association of Mizar Users

MML identifier: SEQM_3
[ MML identifier index ]


environ

 vocabulary ARYTM, SEQ_1, PARTFUN1, ORDINAL2, FUNCT_1, PROB_1, RELAT_1,
      ARYTM_1, SEQ_2, LATTICES, ABSVALUE, SEQM_3, FUNCOP_1;
 notation TARSKI, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, RELAT_1, PARTFUN1,
      FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, NAT_1, FUNCOP_1;
 constructors REAL_1, SEQ_2, ABSVALUE, NAT_1, PARTFUN1, MEMBERED, FUNCOP_1,
      XBOOLE_0;
 clusters FUNCT_1, XREAL_0, RELSET_1, SEQ_1, ARYTM_3, MEMBERED, FUNCOP_1,
      ZFMISC_1, XBOOLE_0, ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions SEQ_2;
 theorems REAL_1, FUNCT_1, SEQ_1, SEQ_2, ABSVALUE, NAT_1, TARSKI, AXIOMS,
      FUNCT_2, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, FUNCOP_1;
 schemes NAT_1, SEQ_1;

begin

  reserve n,n1,m,k,k1 for Nat;
  reserve r,r1,r2 for real number;
  reserve f,seq,seq1,seq2 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 such that A2:m=n+k1 by NAT_1:28;
      k1 <> 0 by A1,A2;
  then consider n1 such that A3:k1=n1+1 by NAT_1:22;
  take k=n1;
  thus m=n+1+k by A2,A3,XCMPLX_1:1;
 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: X[0] by A1;
     A3:now let k such that A4: X[k];
        seq.(n+1+k)<seq.(n+1+k+1) by A1;
      then seq.n<seq.(n+1+k+1) by A4,AXIOMS:22;
      hence X[k+1] by XCMPLX_1:1;
     end;
    thus for k holds X[k] from Ind(A2,A3);
   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 seq.n<seq.m by A5;
   end;
  assume A6:for n,m st n<m holds seq.n<seq.m;
  let n;
    n<n+1 by NAT_1:38;
  hence seq.n<seq.(n+1) 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: X[0] by A1;
       A3:now let k such that A4: X[k];
          seq.(n+1+k+1)<seq.(n+1+k) by A1;
        then seq.(n+1+k+1)<seq.n by A4,AXIOMS:22;
        hence X[k+1] by XCMPLX_1:1;
       end;
      thus for k holds X[k] from Ind(A2,A3);
     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 seq.m<seq.n by A5;
     end;
    assume A6:for n,m st n<m holds seq.m<seq.n;
    let n;
      n<n+1 by NAT_1:38;
    hence seq.(n+1)<seq.n 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: X[0];
       A3:now let k such that A4: X[k];
          seq.(n+k)<=seq.(n+k+1) by A1;
        then seq.n<=seq.(n+k+1) by A4,AXIOMS:22;
        hence X[k+1] by XCMPLX_1:1;
       end;
      thus for k holds X[k] from Ind(A2,A3);
     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 ex k1 st m=n+k1 by NAT_1:28;
      hence seq.n<=seq.m by A5;
     end;
    assume A6:for n,m st n<=m holds seq.n<=seq.m;
    let n;
      n<=n+1 by NAT_1:38;
    hence seq.n<=seq.(n+1) by A6;
   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: X[0];
       A3:now let k such that A4: X[k];
          seq.(n+k+1)<=seq.(n+k) by A1;
        then seq.(n+k+1)<=seq.n by A4,AXIOMS:22;
        hence X[k+1] by XCMPLX_1:1;
       end;
      thus for k holds X[k] from Ind(A2,A3);
     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 ex k1 st m=n+k1 by NAT_1:28;
      hence seq.m<=seq.n by A5;
     end;
    assume A6:for n,m st n<=m holds seq.m<=seq.n;
    let n;
      n<=n+1 by NAT_1:38;
    hence seq.(n+1)<=seq.n by A6;
   end;

::
:: DEFINITIONS OF MONOTONE AND CONSTANT SEQUENCES
::

definition let f be PartFunc of NAT, REAL;
  attr f is increasing means :Def1:
   for m,n st m in dom f & n in dom f & m < n holds f.m < f.n;
  attr f is decreasing means :Def2:
   for m,n st m in dom f & n in dom f & m < n holds f.m > f.n;
  attr f is non-decreasing means :Def3:
   for m,n st m in dom f & n in dom f & m < n holds f.m <= f.n;
  attr f is non-increasing means :Def4:
   for m,n st m in dom f & n in dom f & m < n holds f.m >= f.n;
end;

Lm6: f is increasing iff for n being Nat holds f.n < f.(n+1)
  proof
    thus f is increasing implies for n being Nat holds f.n < f.(n+1)
    proof
      assume A1: f is increasing;
      let n be Nat;
A2:   dom f = NAT by FUNCT_2:def 1;
        n < n+1 by NAT_1:38;
      hence thesis by A1,A2,Def1;
    end;
    assume A3:for n being Nat holds f.n < f.(n+1);
    let m,n; assume m in dom f & n in dom f & m < n;
    then consider k such that
A4: n = m+1+k by Lm1;
    thus thesis by A3,A4,Lm2;
  end;

Lm7: f is decreasing iff for n being Nat holds f.n > f.(n+1)
  proof
    thus f is decreasing implies for n being Nat holds f.n > f.(n+1)
    proof
      assume A1: f is decreasing;
      let n be Nat;
A2:   dom f = NAT by FUNCT_2:def 1;
        n < n+1 by NAT_1:38;
      hence thesis by A1,A2,Def2;
    end;
    assume A3:for n being Nat holds f.n > f.(n+1);
    let m,n; assume m in dom f & n in dom f & m < n;
    then consider k such that
A4: n = m+1+k by Lm1;
    thus thesis by A3,A4,Lm3;
  end;

Lm8: f is non-decreasing iff for n being Nat holds f.n <= f.(n+1)
  proof
    thus f is non-decreasing implies for n being Nat holds f.n <= f.(n+1)
    proof
      assume A1: f is non-decreasing;
      let n be Nat;
A2:   dom f = NAT by FUNCT_2:def 1;
        n < n+1 by NAT_1:38;
      hence thesis by A1,A2,Def3;
    end;
    assume A3:for n being Nat holds f.n <= f.(n+1);
    let m,n; assume m in dom f & n in dom f & m < n;
    then consider k such that
A4: n = m+k by NAT_1:28;
    thus thesis by A3,A4,Lm4;
  end;

Lm9: f is non-increasing iff for n being Nat holds f.n >= f.(n+1)
  proof
    thus f is non-increasing implies for n being Nat holds f.n >= f.(n+1)
    proof
      assume A1: f is non-increasing;
      let n be Nat;
A2:   dom f = NAT by FUNCT_2:def 1;
        n < n+1 by NAT_1:38;
      hence thesis by A1,A2,Def4;
    end;
    assume A3:for n being Nat holds f.n >= f.(n+1);
    let m,n; assume m in dom f & n in dom f & m < n;
    then consider k such that
A4: n = m+k by NAT_1:28;
    thus thesis by A3,A4,Lm5;
  end;

definition let f be Function;
  attr f is constant means
:Def5: for n1,n2 being set st n1 in dom f & n2 in dom f holds f.n1=f.n2;
end;

definition let seq;
  redefine attr seq is constant means :Def6: ex r st for n holds seq.n=r;
 compatibility
  proof
A1:dom seq = NAT by FUNCT_2:def 1;
   hereby assume
A2:   seq is constant;
    consider n0 being Nat;
    reconsider r = seq.n0 as real number;
    take r;
    let n be Nat;
    thus seq.n = r by A1,A2,Def5;
   end;
   given r such that
A3:  for n holds seq.n=r;
   let n1,n2 be set;
   assume
A4:  n1 in dom seq & n2 in dom seq;
   hence seq.n1 = r by A1,A3 .= seq.n2 by A1,A3,A4;
  end;
end;

definition let seq;
  attr seq is monotone means :Def7:
   seq is non-decreasing or seq is non-increasing;
end;

canceled 6;

theorem
 Th7: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) by Lm6;
     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 n in dom seq & m in dom seq & n < m;
   hence thesis by A1;
  end;

theorem
   seq is increasing iff for n,k holds seq.n<seq.(n+1+k)
  proof
   thus seq is increasing implies for n,k holds seq.n<seq.(n+1+k)
    proof
     assume seq is increasing;
     then for n holds seq.n<seq.(n+1) by Lm6;
     hence thesis by Lm2;
    end;
   assume for n,k holds seq.n<seq.(n+1+k);
   then for n,m st n<m holds seq.n<seq.m by Lm2;
   hence thesis by Th7;
  end;

theorem
 Th9:seq is decreasing iff for n,k holds seq.(n+1+k)<seq.n
  proof
   thus seq is decreasing implies for n,k holds seq.(n+1+k)<seq.n
    proof
     assume seq is decreasing;
     then for n holds seq.(n+1)<seq.n by Lm7;
     hence thesis by Lm3;
    end;
   assume A1: for n,k holds seq.(n+1+k)<seq.n;
   let n,m; assume n in dom seq & m in dom seq & n < m;
   hence thesis by A1,Lm3;
  end;

theorem
 Th10: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 Th9;
     hence thesis by Lm3;
    end;
   assume A1:for n,m st n<m holds seq.m<seq.n;
   let n,m; assume n in dom seq & m in dom seq & n < m;
   hence thesis by A1;
  end;

theorem
 Th11:seq is non-decreasing iff for n,k holds seq.n<=seq.(n+k)
  proof
   thus seq is non-decreasing implies for n,k holds seq.n<=seq.(n+k)
    proof
     assume seq is non-decreasing;
     then for n holds seq.n<=seq.(n+1) by Lm8;
     hence thesis by Lm4;
    end;
   assume for n,k holds seq.n<=seq.(n+k);
   then for n holds seq.n<=seq.(n+1);
   hence thesis by Lm8;
  end;

theorem
 Th12: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 Th11;
     hence thesis by Lm4;
    end;
   assume A1:for n,m st n<=m holds seq.n<=seq.m;
   let n,m; assume n in dom seq & m in dom seq & n < m;
   hence thesis by A1;
  end;

theorem
 Th13:seq is non-increasing iff for n,k holds seq.(n+k)<=seq.n
  proof
   thus seq is non-increasing implies for n,k holds seq.(n+k)<=seq.n
    proof
     assume seq is non-increasing;
     then for n holds seq.(n+1)<=seq.n by Lm9;
     hence thesis by Lm5;
    end;
   assume for n,k holds seq.(n+k)<=seq.n;
   then for n holds seq.(n+1)<=seq.n;
   hence thesis by Lm9;
  end;

theorem
 Th14: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 Th13;
     hence thesis by Lm5;
    end;
   assume A1:for n,m st n<=m holds seq.m<=seq.n;
   let n,m; assume n in dom seq & m in dom seq & n < m;
   hence thesis by A1;
  end;

 Lm10:((ex r st for n holds seq.n=r) implies ex r st rng seq={r}) &
      ((ex r st rng seq={r}) implies for n holds seq.n=seq.(n+1)) &
      ((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 holds seq.n=seq.m) &
      ((for n,m holds seq.n=seq.m) implies ex r st for n holds seq.n=r)
  proof
   thus (ex r st for n holds seq.n=r) implies ex r st rng seq={r}
    proof
     given r1 such that A1:for n holds seq.n=r1;
     take r=r1;
        now let y; assume y in rng seq;
       then consider x such that A2:x in dom seq and
                            A3:seq.x=y by FUNCT_1:def 5;
         x in NAT by A2,FUNCT_2:def 1;
       then y=r1 by A1,A3;
       hence y in {r} by TARSKI:def 1;
      end;
     then A4:rng seq c={r} by TARSKI:def 3;
        now let y; assume y in {r};
       then A5:y=r by TARSKI:def 1;
          now assume A6:not y in rng seq;
            now let n;
             n in NAT;
           then n in dom seq by FUNCT_2:def 1;
           then seq.n<>r by A5,A6,FUNCT_1:def 5;
           hence contradiction by A1;
          end;
         hence contradiction;
        end;
       hence y in rng seq;
      end;
     then {r} c= rng seq by TARSKI:def 3;
     hence thesis by A4,XBOOLE_0:def 10;
    end;
   thus (ex r st rng seq={r}) implies for n holds seq.n=seq.(n+1)
    proof
     given r1 such that A7:rng seq={r1};
     let n;
       n in NAT & n+1 in NAT;
     then n in dom seq & n+1 in dom seq by FUNCT_2:def 1;
     then seq.n in{r1} & seq.(n+1) in{r1} by A7,FUNCT_1:def 5;
     then seq.n=r1 & seq.(n+1)=r1 by TARSKI:def 1;
     hence seq.n=seq.(n+1);
    end;
   thus (for n holds seq.n=seq.(n+1)) implies
                for n,k holds seq.n=seq.(n+k)
    proof
     assume A8:for n holds seq.n=seq.(n+1);
     let n;
      defpred X[Nat] means seq.n=seq.(n+$1);
     A9: X[0];
      A10:now let k such that A11: X[k];
         seq.(n+k)=seq.(n+k+1) by A8;
       hence X[k+1] by A11,XCMPLX_1:1;
      end;
     thus for k holds X[k] from Ind(A9,A10);
    end;
   thus (for n,k holds seq.n=seq.(n+k)) implies
               for n,m holds seq.n=seq.m
    proof
     assume A12:for n,k holds seq.n=seq.(n+k);
     let n,m;
      A13:now assume n<=m;
        then ex k st m=n+k by NAT_1:28;
       hence seq.n=seq.m by A12;
      end;
        now assume m<=n;
        then ex k st n=m+k by NAT_1:28;
       hence seq.n=seq.m by A12;
      end;
     hence seq.n=seq.m by A13;
    end;
   assume that A14:for n,m holds seq.n=seq.m and
               A15:for r ex n st seq.n<>r;
      now let n;
        ex n1 st seq.n1<>seq.n by A15;
     hence contradiction by A14;
    end;
   hence thesis;
  end;

theorem
 Th15:seq is constant iff ex r st rng seq={r}
  proof
   thus seq is constant implies ex r st rng seq={r}
    proof
     assume seq is constant;
     then ex r st for n holds seq.n=r by Def6;
     hence thesis by Lm10;
    end;
   assume ex r st rng seq={r};
   then for n holds seq.n=seq.(n+1) by Lm10;
   then for n,k holds seq.n=seq.(n+k) by Lm10;
   then for n,m holds seq.n=seq.m by Lm10;
   hence ex r st for n holds seq.n=r by Lm10;
  end;

theorem
 Th16:seq is constant iff for n holds seq.n=seq.(n+1)
  proof
   thus seq is constant implies for n holds seq.n=seq.(n+1)
    proof
     assume seq is constant;
     then ex r st rng seq={r} by Th15;
     hence thesis by Lm10;
    end;
   assume for n holds seq.n=seq.(n+1);
   then for n,k holds seq.n=seq.(n+k) by Lm10;
   then for n,m holds seq.n=seq.m by Lm10;
   hence ex r st for n holds seq.n=r by Lm10;
  end;

theorem
 Th17:seq is constant iff for n,k holds seq.n=seq.(n+k)
  proof
   thus seq is constant implies for n,k holds seq.n=seq.(n+k)
    proof
     assume seq is constant;
     then for n holds seq.n=seq.(n+1) by Th16;
     hence thesis by Lm10;
    end;
   assume for n,k holds seq.n=seq.(n+k);
   then for n,m holds seq.n=seq.m by Lm10;
   hence ex r st for n holds seq.n=r by Lm10;
  end;

theorem
 Th18:seq is constant iff for n,m holds seq.n=seq.m
  proof
   thus seq is constant implies for n,m holds seq.n=seq.m
    proof
     assume seq is constant;
     then for n,k holds seq.n=seq.(n+k) by Th17;
     hence thesis by Lm10;
    end;
   assume for n,m holds seq.n=seq.m;
   hence ex r st for n holds seq.n=r by Lm10;
  end;

::
:: PROPORTIES OF MONOTONE AND CONSTANT SEQUENCES
::
theorem
   seq is increasing implies for n st 0<n holds seq.0<seq.n by Th7;

theorem
   seq is decreasing implies for n st 0<n holds seq.n<seq.0 by Th10;

theorem
 Th21:seq is non-decreasing implies for n holds seq.0<=seq.n
  proof
   assume A1:seq is non-decreasing;
   let n;
     0<=n by NAT_1:18;
   hence seq.0<=seq.n by A1,Th12;
  end;

theorem
 Th22:seq is non-increasing implies for n holds seq.n<=seq.0
  proof
   assume A1:seq is non-increasing;
   let n;
     0<=n by NAT_1:18;
   hence seq.n<=seq.0 by A1,Th14;
  end;

theorem
   seq is increasing implies seq is non-decreasing
  proof
   assume seq is increasing;
   then for n holds seq.n <= seq.(n+1) by Lm6;
   hence thesis by Lm8;
  end;

theorem
   seq is decreasing implies seq is non-increasing
  proof
   assume seq is decreasing;
   then for n holds seq.n >= seq.(n+1) by Lm7;
   hence thesis by Lm9;
  end;

theorem
 Th25:seq is constant implies seq is non-decreasing
  proof
   assume seq is constant;
   then for n holds seq.n <= seq.(n+1) by Th16;
   hence thesis by Lm8;
  end;

theorem
 Th26:seq is constant implies seq is non-increasing
  proof
   assume seq is constant;
   then for n holds seq.n >= seq.(n+1) by Th16;
   hence thesis by Lm9;
  end;

theorem
   seq is non-decreasing & seq is non-increasing implies
        seq is constant
  proof
   assume that A1:seq is non-decreasing and
               A2:seq is non-increasing;
      now let n;
     A3:seq.n<=seq.(n+1) by A1,Lm8;
       seq.(n+1)<=seq.n by A2,Lm9;
     hence seq.n=seq.(n+1) by A3,AXIOMS:21;
    end;
   hence thesis by Th16;
  end;

::  DEFINITIONS OF INCREASING SEQUENCE OF NATURAL NUMBERS,
::  RESTRICTION OF SEQUENCE.

definition let IT be Relation;
 attr IT is natural-yielding means :Def8:
  rng IT c= NAT;
end;

definition
  cluster increasing natural-yielding Real_Sequence;
existence
 proof deffunc U(Nat) = $1;
  consider seq such that A1:for n holds seq.n=U(n) from ExRealSeq;
  take seq;
     now let y; assume y in rng seq;
    then consider x such that A2:x in dom seq and
                         A3:seq.x=y by FUNCT_1:def 5;
      x in NAT by A2,FUNCT_2:def 1;
    hence y in NAT by A1,A3;
   end;
  then A4: rng seq c=NAT by TARSKI:def 3;
    now let n;
     seq.n=n & seq.(n+1)=n+1 by A1;
   hence seq.n<seq.(n+1) by NAT_1:38;
  end;
  hence thesis by A4,Def8,Lm6;
 end;
end;

definition
  mode Seq_of_Nat is natural-yielding Real_Sequence;
end;

definition
 let seq,k;
func seq ^\k ->Real_Sequence means :Def9:
  for n holds it.n=seq.(n+k);
existence
 proof deffunc U(Nat) = seq.($1+k);
  thus ex f being Real_Sequence st
   for n holds f.n=U(n) from ExRealSeq;
 end;
uniqueness
 proof
  let seq1,seq2;
  assume that A1:for n holds seq1.n=seq.(n+k) and
              A2:for n holds seq2.n=seq.(n+k);
     now let n;
      seq1.n=seq.(n+k) & seq2.n=seq.(n+k) by A1,A2;
    hence seq1.n=seq2.n;
   end;
  hence seq1=seq2 by FUNCT_2:113;
 end;
end;

reserve Nseq,Nseq1,Nseq2 for increasing Seq_of_Nat;

canceled;

theorem
 Th29:seq is increasing Seq_of_Nat iff seq is increasing &
        for n holds seq.n is Nat
  proof
   thus seq is increasing Seq_of_Nat implies seq is increasing &
         for n holds seq.n is Nat
    proof
     assume A1:seq is increasing Seq_of_Nat;
     hence seq is increasing;
     let n;
     A2:rng seq c= NAT by A1,Def8;
       n in NAT;
     then n in dom seq by FUNCT_2:def 1;
     then seq.n in rng seq by FUNCT_1:def 5;
     hence seq.n is Nat by A2;
    end;
   assume that A3:seq is increasing and
               A4:for n holds seq.n is Nat;
     seq is natural-yielding
     proof
         now let y; assume y in rng seq;
        then consider x such that A5:x in dom seq and
                             A6:seq.x=y by FUNCT_1:def 5;
          x in NAT by A5,FUNCT_2:def 1;
        then seq.x is Nat by A4;
        hence y in NAT by A6;
       end;
      hence rng seq c= NAT by TARSKI:def 3;
     end;
    hence thesis by A3;
   end;

canceled;

theorem
 Th31:for n holds (seq*Nseq).n=seq.(Nseq.n)
  proof
   let n;
    A1:dom Nseq=NAT by FUNCT_2:def 1;
      rng Nseq c= NAT by Def8;
    then rng Nseq c= dom seq by FUNCT_2:def 1;
    then dom (seq*Nseq)=NAT by A1,RELAT_1:46;
    hence (seq*Nseq).n=seq.(Nseq.n) by FUNCT_1:22;
  end;

definition let Nseq,n;
  redefine func Nseq.n ->Nat;
coherence by Th29;
end;

definition let Nseq,seq;
  redefine func seq*Nseq ->Real_Sequence;
 coherence
  proof
     A1:dom Nseq=NAT by FUNCT_2:def 1;
     A2:rng seq c= REAL by RELSET_1:12;
       rng Nseq c= NAT by Def8;
     then rng Nseq c= dom seq by FUNCT_2:def 1;
     then A3:   dom (seq*Nseq)=NAT by A1,RELAT_1:46;
       rng (seq*Nseq) c= rng seq by RELAT_1:45;
     then rng (seq*Nseq) c= REAL by A2,XBOOLE_1:1;
   hence thesis by A3,FUNCT_2:def 1,RELSET_1:11;
  end;
end;

definition let Nseq,Nseq1;
  redefine func Nseq1*Nseq -> increasing Seq_of_Nat;
 coherence
  proof
   A1:rng Nseq1 c= NAT by Def8;
     rng (Nseq1*Nseq) c= rng Nseq1 by RELAT_1:45;
   then A2:rng (Nseq1*Nseq) c= NAT by A1,XBOOLE_1:1;
      now let n;
       Nseq.n<Nseq.(n+1) by Lm6;
     then Nseq1.(Nseq.n)<Nseq1.(Nseq.(n+1)) by Th7;
     then (Nseq1*Nseq).n<Nseq1.(Nseq.(n+1)) by Th31;
     hence (Nseq1*Nseq).n<(Nseq1*Nseq).(n+1) by Th31;
    end;
   hence thesis by A2,Def8,Lm6;
  end;
end;

definition let Nseq,k;
  cluster Nseq ^\k -> increasing natural-yielding;
 coherence
  proof
   A1:now let n;
      (Nseq ^\k).n=Nseq.(n+k) by Def9;
    hence (Nseq ^\k).n is Nat;
   end;
     now let n;
      Nseq.(n+k)<Nseq.(n+k+1) by Lm6;
    then (Nseq ^\k).n<Nseq.(n+k+1) by Def9;
    then (Nseq ^\k).n<Nseq.(n+1+k) by XCMPLX_1:1;
    hence (Nseq ^\k).n<(Nseq ^\k).(n+1) by Def9;
   end;
  then Nseq ^\k is increasing by Lm6;
  hence thesis by A1,Th29;
 end;
end;

::
:: DEFINITION OF SUBSEQUENCE
::

definition let seq,seq1;
  pred seq is_subsequence_of seq1 means :Def10:
   ex Nseq st seq=seq1*Nseq;
end;

definition let f be Real_Sequence;
  redefine attr f is increasing means
     for n being Nat holds f.n < f.(n+1);
  compatibility by Lm6;
  redefine attr f is decreasing means
     for n being Nat holds f.n > f.(n+1);
  compatibility by Lm7;
  redefine attr f is non-decreasing means
     for n being Nat holds f.n <= f.(n+1);
  compatibility by Lm8;
  redefine attr f is non-increasing means
     for n being Nat holds f.n >= f.(n+1);
  compatibility by Lm9;
end;

canceled;

theorem
   for n holds n<=Nseq.n
  proof
      defpred X[Nat] means $1<=Nseq.$1;
   A1: X[0] by NAT_1:18;
    A2:now let k such that A3: X[k];
       Nseq.k<Nseq.(k+1) by Lm6;
     then k<Nseq.(k+1) by A3,AXIOMS:22;
     hence X[k+1] by NAT_1:38;
    end;
   thus for k holds X[k] from Ind(A1,A2);
  end;

theorem
   seq ^\0 =seq
  proof
     now let n;
    thus (seq ^\0).n=seq.(n+0) by Def9
                  .=seq.n;
   end;
  hence thesis by FUNCT_2:113;
 end;

theorem
   (seq ^\k)^\m=(seq ^\m)^\k
  proof
      now let n;
     thus ((seq ^\k)^\m).n=(seq ^\k).(n+m) by Def9
      .=seq.(n+m+k) by Def9
      .=seq.(n+k+m) by XCMPLX_1:1
      .=(seq ^\m).(n+k) by Def9
      .=((seq ^\m)^\k).n by Def9;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   (seq ^\k)^\m=seq ^\(k+m)
  proof
      now let n;
     thus ((seq ^\k)^\m).n=(seq ^\k).(n+m) by Def9
      .=seq.(n+m+k) by Def9
      .=seq.(n+(k+m)) by XCMPLX_1:1
      .=(seq ^\(k+m)).n by Def9;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
 Th37:(seq+seq1) ^\k=(seq ^\k) +(seq1 ^\k)
  proof
      now let n;
     thus ((seq+seq1) ^\k).n=(seq+seq1).(n+k) by Def9
      .=seq.(n+k) + seq1.(n+k) by SEQ_1:11
      .=(seq ^\k).n +seq1.(n+k) by Def9
      .=(seq ^\k).n +(seq1 ^\k).n by Def9
      .=((seq ^\k) +(seq1 ^\k)).n by SEQ_1:11;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
 Th38:(-seq) ^\k=-(seq ^\k)
  proof
      now let n;
     thus ((-seq) ^\k).n=(-seq).(n+k) by Def9
      .=-(seq.(n+k)) by SEQ_1:14
      .=-((seq ^\ k).n) by Def9
      .=(-(seq ^\k)).n by SEQ_1:14;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   (seq-seq1) ^\k=(seq ^\k)-(seq1 ^\k)
  proof
   thus (seq-seq1) ^\k=(seq+(-seq1)) ^\k by SEQ_1:15
    .=(seq ^\k)+((-seq1) ^\k) by Th37
    .=(seq ^\k)+-(seq1 ^\k) by Th38
    .=(seq ^\k)-(seq1 ^\k) by SEQ_1:15;
  end;

theorem
   seq is_not_0 implies seq ^\k is_not_0
  proof
   assume A1:seq is_not_0;
      now let n;
       (seq ^\k).n=seq.(n+k) by Def9;
     hence (seq ^\k).n<>0 by A1,SEQ_1:7;
    end;
   hence thesis by SEQ_1:7;
  end;

theorem
 Th41:(seq") ^\k=(seq ^\k)"
  proof
      now let n;
     thus ((seq") ^\k).n=(seq").(n+k) by Def9
      .=(seq.(n+k))" by SEQ_1:def 8
      .=((seq ^\k).n)" by Def9
      .=((seq ^\k)").n by SEQ_1:def 8;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
 Th42:(seq(#)seq1) ^\k=(seq ^\k)(#)(seq1 ^\k)
  proof
      now let n;
     thus ((seq(#)seq1) ^\k).n=(seq(#)seq1).(n+k) by Def9
      .=seq.(n+k)*seq1.(n+k) by SEQ_1:12
      .=(seq ^\k).n*seq1.(n+k) by Def9
      .=(seq ^\k).n*(seq1 ^\k).n by Def9
      .=((seq ^\k)(#)(seq1 ^\k)).n by SEQ_1:12;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   (seq/"seq1) ^\k=(seq ^\k)/"(seq1 ^\k)
  proof
   thus (seq/"seq1) ^\k=(seq(#)seq1") ^\k by SEQ_1:def 9
    .=(seq ^\k)(#)((seq1") ^\k) by Th42
    .=(seq ^\k)(#)(seq1 ^\k)" by Th41
    .=(seq ^\k)/"(seq1 ^\k) by SEQ_1:def 9;
  end;

theorem
   (r(#)seq) ^\k=r(#)(seq ^\k)
  proof
      now let n;
     thus ((r(#)seq) ^\k).n=(r(#)seq).(n+k) by Def9
      .=r*(seq.(n+k)) by SEQ_1:13
      .=r*((seq ^\k).n) by Def9
      .=(r(#)(seq ^\k)).n by SEQ_1:13;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   (seq*Nseq) ^\k=seq*(Nseq ^\k)
  proof
     now let n;
    thus ((seq*Nseq) ^\k).n=(seq*Nseq).(n+k) by Def9
     .=seq.(Nseq.(n+k)) by Th31
     .=seq.((Nseq ^\k).n) by Def9
     .=(seq*(Nseq ^\k)).n by Th31;
   end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   seq is_subsequence_of seq
  proof deffunc U(Nat) = $1;
   consider seq1 such that A1:for n holds seq1.n=U(n) from ExRealSeq;
      now let n;
       seq1.n=n & seq1.(n+1)=n+1 by A1;
     hence seq1.n<seq1.(n+1) by NAT_1:38;
    end;
   then A2:seq1 is increasing by Lm6;
      for n holds seq1.n is Nat by A1;
   then reconsider seq1 as increasing Seq_of_Nat by A2,Th29;
   take Nseq=seq1;
      now let n;
     thus (seq*Nseq).n=seq.(Nseq.n) by Th31
       .=seq.n by A1;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   seq ^\k is_subsequence_of seq
  proof deffunc U(Nat) = $1+k;
   consider seq1 such that A1:for n holds seq1.n=U(n) from ExRealSeq;
      now let n;
     A2:seq1.n=n+k & seq1.(n+1)=n+1+k by A1;
       n+k<n+k+1 by NAT_1:38;
     hence seq1.n<seq1.(n+1) by A2,XCMPLX_1:1;
    end;
   then A3:seq1 is increasing by Lm6;
      now let n;
       n+k is Nat;
     hence seq1.n is Nat by A1;
    end;
   then reconsider seq1 as increasing Seq_of_Nat by A3,Th29;
   take Nseq=seq1;
      now let n;
     thus (seq*Nseq).n=seq.(Nseq.n) by Th31
       .=seq.(n+k) by A1
       .=(seq ^\k).n by Def9;
    end;
   hence thesis by FUNCT_2:113;
  end;

theorem
   seq is_subsequence_of seq1 & seq1 is_subsequence_of seq2
       implies seq is_subsequence_of seq2
  proof
   assume that A1:seq is_subsequence_of seq1 and
               A2:seq1 is_subsequence_of seq2;
   consider Nseq1 such that A3:seq=seq1*Nseq1 by A1,Def10;
   consider Nseq2 such that A4:seq1=seq2*Nseq2 by A2,Def10;
   take Nseq=Nseq2*Nseq1;
   thus seq=seq2*Nseq by A3,A4,RELAT_1:55;
  end;

::
::  SUBSEQUENCES OF MONOTONE SEQUENCE
::    SUBSEQUENCE  OF BOUND 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;
  consider Nseq such that A3:seq1=seq*Nseq by A2,Def10;
  let n;
    Nseq.n<Nseq.(n+1) by Lm6;
  then (seq.(Nseq.n))<(seq.(Nseq.(n+1))) by A1,Th7;
  then (seq*Nseq).n<(seq.(Nseq.(n+1))) by Th31;
  hence seq1.n<seq1.(n+1) by A3,Th31;
 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;
  consider Nseq such that A3:seq1=seq*Nseq by A2,Def10;
  let n;
    Nseq.n<Nseq.(n+1) by Lm6;
  then seq.(Nseq.(n+1))<seq.(Nseq.n) by A1,Th10;
  then (seq*Nseq).(n+1)<seq.(Nseq.n) by Th31;
  hence seq1.(n+1)<seq1.n by A3,Th31;
 end;

theorem
 Th51: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;
  consider Nseq such that A3:seq1=seq*Nseq by A2,Def10;
  let n;
    Nseq.n<=Nseq.(n+1) by Lm6;
  then (seq.(Nseq.n))<=(seq.(Nseq.(n+1))) by A1,Th12;
  then (seq*Nseq).n<=(seq.(Nseq.(n+1))) by Th31;
  hence seq1.n<=seq1.(n+1) by A3,Th31;
 end;

theorem
 Th52: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;
  consider Nseq such that A3:seq1=seq*Nseq by A2,Def10;
  let n;
    Nseq.n<=Nseq.(n+1) by Lm6;
  then (seq.(Nseq.(n+1)))<=(seq.(Nseq.n)) by A1,Th14;
  then (seq*Nseq).(n+1)<=(seq.(Nseq.n)) by Th31;
  hence seq1.(n+1)<=seq1.n by A3,Th31;
 end;

theorem
   seq is monotone & seq1 is_subsequence_of seq implies
        seq1 is monotone
  proof
   assume that A1:seq is monotone and
               A2:seq1 is_subsequence_of seq;
    A3:now assume seq is non-decreasing;
     then seq1 is non-decreasing by A2,Th51;
     hence seq1 is monotone by Def7;
    end;
      now assume seq is non-increasing;
     then seq1 is non-increasing by A2,Th52;
     hence seq1 is monotone by Def7;
    end;
   hence thesis by A1,A3,Def7;
  end;

theorem
   seq is constant & seq1 is_subsequence_of seq implies
       seq1 is constant
 proof
  assume that A1:seq is constant and
              A2:seq1 is_subsequence_of seq;
  consider Nseq such that A3:seq1=seq*Nseq by A2,Def10;
     now let n;
      seq.(Nseq.(n+1))=seq.(Nseq.n) by A1,Th18;
    then (seq*Nseq).(n+1)=seq.(Nseq.n) by Th31;
    hence seq1.n=seq1.(n+1) by A3,Th31;
   end;
  hence thesis by Th16;
 end;

theorem
   seq is constant & seq1 is_subsequence_of seq implies seq=seq1
  proof
    assume that
A1: seq is constant and
A2: seq1 is_subsequence_of seq;
    consider Nseq such that
A3: seq1=seq*Nseq by A2,Def10;
       now let n;
      thus seq1.n=seq.(Nseq.n) by A3,Th31
                .=seq.n by A1,Th18;
     end;
    hence thesis by FUNCT_2:113;
  end;

theorem
 Th56: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,SEQ_2:def 3;
  consider Nseq such that A4:seq1=seq*Nseq by A2,Def10;
  take r=r1;
  let n;
    seq1.n=seq.(Nseq.n) by A4,Th31;
  hence seq1.n<r by A3;
 end;

theorem
 Th57: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,SEQ_2:def 4;
  consider Nseq such that A4:seq1=seq*Nseq by A2,Def10;
  take r=r1;
  let n;
    seq1.n=seq.(Nseq.n) by A4,Th31;
  hence r<seq1.n by A3;
 end;

theorem
   seq is bounded & seq1 is_subsequence_of seq implies
       seq1 is bounded
 proof
  assume that A1:seq is bounded and
              A2:seq1 is_subsequence_of seq;
    seq is bounded_above by A1,SEQ_2:def 5;
  hence seq1 is bounded_above by A2,Th56;
    seq is bounded_below by A1,SEQ_2:def 5;
  hence seq1 is bounded_below by A2,Th57;
 end;

::
:: 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,Lm6;
    then r*seq.n<r*seq.(n+1) by A2,REAL_1:70;
    then (r(#)seq).n<r*seq.(n+1) by SEQ_1:13;
    hence (r(#)seq).n<(r(#)seq).(n+1) by SEQ_1:13;
   end;
  thus 0=r implies r(#)seq is constant
   proof
    assume A3:0=r;
       now let n;
        r*seq.n=r*seq.(n+1) by A3;
      then (r(#)seq).n=r*seq.(n+1) by SEQ_1:13;
      hence (r(#)seq).n=(r(#)seq).(n+1) by SEQ_1:13;
     end;
    hence thesis by Th16;
   end;
  assume that A4:seq is increasing and
              A5:r<0;
  let n;
    seq.n<seq.(n+1) by A4,Lm6;
  then r*seq.(n+1)<r*seq.n by A5,REAL_1:71;
  then (r(#)seq).(n+1)<r*seq.n by SEQ_1:13;
  hence (r(#)seq).(n+1)<(r(#)seq).n by SEQ_1:13;
 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,Lm7;
    then r*seq.(n+1)<r*seq.n by A2,REAL_1:70;
    then (r(#)seq).(n+1)<r*seq.n by SEQ_1:13;
    hence (r(#)seq).(n+1)<(r(#)seq).n by SEQ_1:13;
   end;
  assume that A3:seq is decreasing and
              A4:r<0;
  let n;
    seq.(n+1)<seq.n by A3,Lm7;
  then r*seq.n<r*seq.(n+1) by A4,REAL_1:71;
  then (r(#)seq).n<r*seq.(n+1) by SEQ_1:13;
  hence (r(#)seq).n<(r(#)seq).(n+1) by SEQ_1:13;
 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,Lm8;
    then r*seq.n<=r*seq.(n+1) by A2,AXIOMS:25;
    then (r(#)seq).n<=r*seq.(n+1) by SEQ_1:13;
    hence (r(#)seq).n<=(r(#)seq).(n+1) by SEQ_1:13;
   end;
  assume that A3:seq is non-decreasing and
              A4:r<=0;
  let n;
    seq.n<=seq.(n+1) by A3,Lm8;
  then r*seq.(n+1)<=r*seq.n by A4,REAL_1:52;
  then (r(#)seq).(n+1)<=r*seq.n by SEQ_1:13;
  hence (r(#)seq).(n+1)<=(r(#)seq).n by SEQ_1:13;
 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,Lm9;
    then r*seq.(n+1)<=r*seq.n by A2,AXIOMS:25;
    then (r(#)seq).(n+1)<=r*seq.n by SEQ_1:13;
    hence (r(#)seq).(n+1)<=(r(#)seq).n by SEQ_1:13;
   end;
  assume that A3:seq is non-increasing and
              A4:r<=0;
  let n;
    seq.(n+1)<=seq.n by A3,Lm9;
  then r*seq.n<=r*seq.(n+1) by A4,REAL_1:52;
  then (r(#)seq).n<=r*seq.(n+1) by SEQ_1:13;
  hence (r(#)seq).n<=(r(#)seq).(n+1) by SEQ_1:13;
 end;

theorem
 Th63:(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 that A1:seq is increasing and
                A2:seq1 is increasing;
    let n;
    A3:seq.n<seq.(n+1) by A1,Lm6;
      seq1.n<seq1.(n+1) by A2,Lm6;
    then seq.n+seq1.n<seq.(n+1)+seq1.(n+1) by A3,REAL_1:67;
    then (seq+seq1).n<seq.(n+1)+seq1.(n+1) by SEQ_1:11;
    hence (seq+seq1).n<(seq+seq1).(n+1) by SEQ_1:11;
   end;
  thus seq is decreasing & seq1 is decreasing implies
         seq+seq1 is decreasing
   proof
    assume that A4:seq is decreasing and
                A5:seq1 is decreasing;
    let n;
    A6:seq.(n+1)<seq.n by A4,Lm7;
      seq1.(n+1)<seq1.n by A5,Lm7;
    then seq.(n+1)+seq1.(n+1)<seq.n+seq1.n by A6,REAL_1:67;
    then (seq+seq1).(n+1)<seq.n+seq1.n by SEQ_1:11;
    hence (seq+seq1).(n+1)<(seq+seq1).n by SEQ_1:11;
   end;
  thus seq is non-decreasing & seq1 is non-decreasing implies
         seq+seq1 is non-decreasing
   proof
    assume that A7:seq is non-decreasing and
                A8:seq1 is non-decreasing;
    let n;
    A9:seq.n<=seq.(n+1) by A7,Lm8;
      seq1.n<=seq1.(n+1) by A8,Lm8;
    then seq.n+seq1.n<=seq.(n+1)+seq1.(n+1) by A9,REAL_1:55;
    then (seq+seq1).n<=seq.(n+1)+seq1.(n+1) by SEQ_1:11;
    hence (seq+seq1).n<=(seq+seq1).(n+1) by SEQ_1:11;
   end;
  assume that A10:seq is non-increasing and
              A11:seq1 is non-increasing;
  let n;
  A12:seq.(n+1)<=seq.n by A10,Lm9;
    seq1.(n+1)<=seq1.n by A11,Lm9;
  then seq.(n+1)+seq1.(n+1)<=seq.n+seq1.n by A12,REAL_1:55;
  then (seq+seq1).(n+1)<=seq.n+seq1.n by SEQ_1:11;
  hence (seq+seq1).(n+1)<=(seq+seq1).n by SEQ_1:11;
 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;
    consider r1 such that A3:for n holds seq1.n=r1 by A2,Def6;
    let n;
      seq.n<seq.(n+1) by A1,Lm6;
    then seq.n+r1<seq.(n+1)+r1 by REAL_1:53;
    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:11;
    hence (seq+seq1).n<(seq+seq1).(n+1) by SEQ_1:11;
   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;
    consider r1 such that A6:for n holds seq1.n=r1 by A5,Def6;
    let n;
      seq.(n+1)<seq.n by A4,Lm7;
    then seq.(n+1)+r1<seq.n+r1 by REAL_1:53;
    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:11;
    hence (seq+seq1).(n+1)<(seq+seq1).n by SEQ_1:11;
   end;
thus seq is non-decreasing & seq1 is constant implies
                                seq+seq1 is non-decreasing
   proof
    assume that A7:seq is non-decreasing and
                A8:seq1 is constant;
      seq1 is non-decreasing by A8,Th25;
    hence thesis by A7,Th63;
   end;
  assume that A9:seq is non-increasing and
              A10:seq1 is constant;
    seq1 is non-increasing by A10,Th26;
  hence thesis by A9,Th63;
 end;

theorem
 Th65:seq is constant implies (for r holds r(#)seq is constant) &
                              -seq is constant &
                              abs seq is constant
  proof
   assume seq is constant;
   then consider r1 such that A1:for n holds seq.n=r1 by Def6;
    A2:now let r;
        now take p=r*r1;
       let n;
         r*seq.n=p by A1;
       hence (r(#)seq).n=p by SEQ_1:13;
      end;
     hence r(#)seq is constant by Def6;
    end;
   hence for r holds r(#)seq is constant;
     (-1)(#)seq is constant by A2;
   hence -seq is constant by SEQ_1:25;
   take p=abs r1;
   let n;
     abs (seq.n)=abs r1 by A1;
   hence (abs seq).n=p by SEQ_1:16;
  end;

theorem
 Th66:seq is constant & seq1 is constant implies
        seq(#)seq1 is constant & seq+seq1 is constant
  proof
   assume that A1:seq is constant and
               A2:seq1 is constant;
   consider r1 such that A3:for n holds seq.n=r1 by A1,Def6;
   consider r2 such that A4:for n holds seq1.n=r2 by A2,Def6;
      now take p=r1*r2;
     let n;
       (seq.n)*r2=r1*r2 by A3;
     then seq.n*(seq1.n)=r1*r2 by A4;
     hence (seq(#)seq1).n=p by SEQ_1:12;
    end;
   hence seq(#)seq1 is constant by Def6;
   take p=r1+r2;
   let n;
     seq.n+r2=r1+r2 by A3;
   then seq.n+seq1.n=r1+r2 by A4;
   hence (seq+seq1).n=p by SEQ_1:11;
  end;

theorem
    seq is constant & seq1 is constant implies seq-seq1 is constant
  proof
   assume that A1:seq is constant and
               A2:seq1 is constant;
     -seq1 is constant by A2,Th65;
   then seq+-seq1 is constant by A1,Th66;
   hence thesis by SEQ_1:15;
  end;

::
:: OPERATIONS ON BOUND SEQUENCES
::
theorem
 Th68:(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
   proof
    assume that A1:seq is bounded_above and
                A2:0<r;
    consider r1 such that
    A3:for n holds seq.n<r1 by A1,SEQ_2:def 3;
    take p=r*abs r1;
    let n;
    A4:r1<=abs r1 by ABSVALUE:11;
      seq.n<r1 by A3;
    then seq.n<abs r1 by A4,AXIOMS:22;
    then r*seq.n<r*abs r1 by A2,REAL_1:70;
    hence (r(#)seq).n<p by SEQ_1:13;
   end;
  thus 0=r implies r(#)seq is bounded
   proof
    assume A5:0=r;
       now
      let n;
         (r(#)seq).n = 0*seq.n by A5,SEQ_1:13;
      hence (r(#)seq).n < 1;
     end;
    hence r(#)seq is bounded_above by SEQ_2:def 3;
    take p=-1;
    let n;
    A6:-1<0;
      r*seq.n=0 by A5;
    hence p<(r(#)seq).n by A6,SEQ_1:13;
   end;
  assume that A7:seq is bounded_above and
              A8:r<0;
  consider r1 such that
  A9:for n holds seq.n<r1 by A7,SEQ_2:def 3;
  take p=r*abs r1;
  let n;
  A10:r1<=abs r1 by ABSVALUE:11;
    seq.n<r1 by A9;
  then seq.n<abs r1 by A10,AXIOMS:22;
  then r*abs r1<r*seq.n by A8,REAL_1:71;
  hence p<(r(#)seq).n by SEQ_1:13;
 end;

theorem
 Th69:(seq is bounded_below & 0<r implies r(#)seq is bounded_below) &
       (seq is bounded_below & r<0 implies r(#)seq is bounded_above)
  proof
  thus seq is bounded_below & 0<r implies r(#)seq is bounded_below
   proof
    assume that A1:seq is bounded_below and
                A2:0<r;
    consider r1 such that
    A3:for n holds r1<seq.n by A1,SEQ_2:def 4;
    take p=r*r1;
    let n;
      r1<seq.n by A3;
    then r*r1<r*seq.n by A2,REAL_1:70;
    hence p<(r(#)seq).n by SEQ_1:13;
   end;
  assume that A4:seq is bounded_below and
              A5:r<0;
  consider r1 such that
  A6:for n holds r1<seq.n by A4,SEQ_2:def 4;
  take p=r*(-abs r1);
  let n;
  A7:-abs r1<=r1 by ABSVALUE:11;
    r1<seq.n by A6;
  then -abs r1<seq.n by A7,AXIOMS:22;
  then r*seq.n<r*(-abs r1) by A5,REAL_1:71;
  hence (r(#)seq).n<p by SEQ_1:13;
 end;

theorem
 Th70:seq is bounded implies (for r holds r(#)seq is bounded) &
                              -seq is bounded &
                              abs seq is bounded
  proof
   assume A1:seq is bounded;
   then A2:seq is bounded_above & seq is bounded_below by SEQ_2:def 5;
   hereby let r;
        per cases;
      suppose A3:0<r;
       then A4:r(#)seq is bounded_above by A2,Th68;
         r(#)seq is bounded_below by A2,A3,Th69;
       hence r(#)seq is bounded by A4,SEQ_2:def 5;
      suppose 0=r;
       hence r(#)seq is bounded by Th68;
      suppose A5:r<0;
       then A6:r(#)seq is bounded_above by A2,Th69;
         r(#)seq is bounded_below by A2,A5,Th68;
       hence r(#)seq is bounded by A6,SEQ_2:def 5;
    end;
   then (-1)(#)seq is bounded;
   hence -seq is bounded by SEQ_1:25;
   consider r such that A7:0<r and
                        A8:for n holds abs (seq.n) <r by A1,SEQ_2:15;
      now
     thus 0<r by A7;
     let n;
       abs (abs (seq.n))<r by A8;
     hence abs ((abs seq).n)<r by SEQ_1:16;
    end;
   hence thesis by SEQ_2:15;
  end;

theorem
 Th71:(seq is bounded_above & seq1 is bounded_above implies
                                 seq+seq1 is bounded_above) &
      (seq is bounded_below & seq1 is bounded_below implies
                                 seq+seq1 is bounded_below) &
      (seq is bounded & seq1 is bounded implies seq+seq1 is bounded)
  proof
   thus A1:seq is bounded_above & seq1 is bounded_above implies
             seq+seq1 is bounded_above
    proof
     assume that A2:seq is bounded_above and
                 A3:seq1 is bounded_above;
     consider r1 such that
     A4:for n holds seq.n<r1 by A2,SEQ_2:def 3;
     consider r2 such that
     A5:for n holds seq1.n<r2 by A3,SEQ_2:def 3;
     take r=r1+r2;
     let n;
     A6:seq.n<r1 by A4;
       seq1.n<r2 by A5;
     then seq.n+seq1.n<r1+r2 by A6,REAL_1:67;
     hence (seq+seq1).n<r by SEQ_1:11;
    end;
   thus A7:seq is bounded_below & seq1 is bounded_below implies
             seq+seq1 is bounded_below
    proof
     assume that A8:seq is bounded_below and
                 A9:seq1 is bounded_below;
     consider r1 such that
     A10:for n holds r1<seq.n by A8,SEQ_2:def 4;
     consider r2 such that
     A11:for n holds r2<seq1.n by A9,SEQ_2:def 4;
     take r=r1+r2;
     let n;
     A12:r1<seq.n by A10;
       r2<seq1.n by A11;
     then r1+r2<seq.n+seq1.n by A12,REAL_1:67;
     hence r<(seq+seq1).n by SEQ_1:11;
    end;
  assume that A13:seq is bounded and
              A14:seq1 is bounded;
  thus seq+seq1 is bounded_above by A1,A13,A14,SEQ_2:def 5;
  thus seq+seq1 is bounded_below by A7,A13,A14,SEQ_2:def 5;
 end;

theorem
 Th72:seq is bounded & seq1 is bounded implies seq(#)seq1 is bounded &
        seq-seq1 is bounded
  proof
   assume that A1:seq is bounded and
               A2:seq1 is bounded;
   consider r1 such that
   A3:0<r1 and A4:for n holds abs (seq.n)<r1 by A1,SEQ_2:15;
   consider r2 such that A5:0<r2 and
                         A6:for n holds abs (seq1.n)<r2 by A2,SEQ_2:15;
      now take r=r1*r2;
       0*0<r1*r2 by A3,A5,SEQ_2:7;
     hence 0<r;
     let n;
     A7:abs (seq.n)<r1 by A4;
     A8:abs (seq1.n)<r2 by A6;
     A9:0<=abs (seq.n) by ABSVALUE:5;
       0<=abs (seq1.n) by ABSVALUE:5;
     then abs (seq.n)*abs (seq1.n)<r by A7,A8,A9,SEQ_2:7;
     then abs ((seq.n)*seq1.n)<r by ABSVALUE:10;
     hence abs ((seq(#)seq1).n)<r by SEQ_1:12;
    end;
   hence seq (#)seq1 is bounded by SEQ_2:15;
     -seq1 is bounded by A2,Th70;
   then seq+-seq1 is bounded by A1,Th71;
   hence thesis by SEQ_1:15;
  end;

::
:: OPERATIONS ON BOUND & CONSTANT SEQUENCES
::
theorem
 Th73:seq is constant implies seq is bounded
  proof
   assume seq is constant;
   then consider r1 such that A1:for n holds seq.n=r1 by Def6;
      now take p=abs r1+1;
       0<=abs r1 by ABSVALUE:5;
     then 0+0<abs r1+1 by REAL_1:67;
     hence 0<p;
     let n;
       abs r1=abs (seq.n) by A1;
     then abs (seq.n)+0<abs r1+1 by REAL_1:53;
     hence abs (seq.n)<p;
    end;
   hence thesis by SEQ_2:15;
  end;

theorem
   seq is constant implies (for r holds r(#)seq is bounded) &
                               (-seq is bounded) &
                               abs seq is bounded
  proof
   assume A1:seq is constant;
      now let r;
       r(#)seq is constant by A1,Th65;
     hence r(#)seq is bounded by Th73;
    end;
   hence for r holds r(#)seq is bounded;
     -seq is constant by A1,Th65;
   hence -seq is bounded by Th73;
     abs seq is constant by A1,Th65;
   hence abs seq is bounded by Th73;
  end;

theorem
 Th75:(seq is bounded_above & seq1 is constant implies
         seq+seq1 is bounded_above) &
      (seq is bounded_below & seq1 is constant implies
         seq+seq1 is bounded_below) &
      (seq is bounded & seq1 is constant implies seq+seq1 is bounded)
  proof
   thus seq is bounded_above & seq1 is constant implies
          seq+seq1 is bounded_above
    proof
     assume that A1:seq is bounded_above and
                 A2:seq1 is constant;
       seq1 is bounded by A2,Th73;
     then seq1 is bounded_above by SEQ_2:def 5;
     hence thesis by A1,Th71;
    end;
   thus seq is bounded_below & seq1 is constant implies
          seq+seq1 is bounded_below
    proof
     assume that A3:seq is bounded_below and
                 A4:seq1 is constant;
       seq1 is bounded by A4,Th73;
     then seq1 is bounded_below by SEQ_2:def 5;
     hence thesis by A3,Th71;
    end;
   assume that A5:seq is bounded and
               A6:seq1 is constant;
     seq1 is bounded by A6,Th73;
   hence thesis by A5,Th71;
  end;

theorem
   (seq is bounded_above & seq1 is constant implies
          seq-seq1 is bounded_above) &
      (seq is bounded_below & seq1 is constant implies
          seq-seq1 is bounded_below) &
      (seq is bounded & seq1 is constant implies seq-seq1 is bounded &
          seq1-seq is bounded & seq(#)seq1 is bounded)
  proof
   thus seq is bounded_above & seq1 is constant implies
          seq-seq1 is bounded_above
    proof
     assume that A1:seq is bounded_above and
                 A2:seq1 is constant;
       -seq1 is constant by A2,Th65;
     then seq+-seq1 is bounded_above by A1,Th75;
     hence thesis by SEQ_1:15;
    end;
   thus seq is bounded_below & seq1 is constant implies
          seq-seq1 is bounded_below
    proof
     assume that A3:seq is bounded_below and
                 A4:seq1 is constant;
       -seq1 is constant by A4,Th65;
     then seq+-seq1 is bounded_below by A3,Th75;
     hence thesis by SEQ_1:15;
    end;
   assume that A5:seq is bounded and
               A6:seq1 is constant;
       -seq1 is constant by A6,Th65;
     then seq+-seq1 is bounded by A5,Th75;
     hence seq-seq1 is bounded by SEQ_1:15;
 A7: seq1 is bounded by A6,Th73;
     hence seq1-seq is bounded by A5,Th72;
     thus thesis by A5,A7,Th72;
  end;

::
:: OPERATIONS ON BOUND & 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,SEQ_2:def 3;
   take r=r1+seq1.0;
   let n;
   A4:seq1.n<=seq1.0 by A2,Th22;
     seq.n<r1 by A3;
   then seq.n+seq1.n<r1+seq1.0 by A4,REAL_1:67;
   hence (seq+seq1).n<r by SEQ_1:11;
  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,SEQ_2:def 4;
   take r=r1+seq1.0;
   let n;
   A4:seq1.0<=seq1.n by A2,Th21;
     r1<seq.n by A3;
   then r1+seq1.0<seq.n+seq1.n by A4,REAL_1:67;
   hence r<(seq+seq1).n by SEQ_1:11;
  end;

theorem Th79: :: YELLOW_6:1
 for X,x being set holds X --> x is constant
 proof let X,a be set;
  let x,y be set;
A1: dom(X --> a) = X by FUNCOP_1:19;
  assume
A2:  x in dom(X --> a) & y in dom(X --> a);
  hence (X --> a).x = a by A1,FUNCOP_1:13 .= (X --> a).y by A1,A2,FUNCOP_1:13;
 end;

definition let X,x be set;
 cluster X --> x -> constant;
 coherence by Th79;
end;


Back to top