rinfsup1.miz



    begin

    reserve n,m,k,k1,k2 for Nat;

    reserve r,r1,r2,s,t,p for Real;

    reserve seq,seq1,seq2 for Real_Sequence;

    reserve x,y for set;

    

     Lm1: for s st 0 < s & r1 <= r2 holds r1 < (r2 + s) & (r1 - s) < r2

    proof

      let s such that

       A1: 0 < s;

      assume r1 <= r2;

      then (r1 + 0 ) < (r2 + s) by A1, XREAL_1: 8;

      hence thesis by XREAL_1: 19;

    end;

    theorem :: RINFSUP1:1

    

     Th1: (s - r) < t & (s + r) > t iff |.(t - s).| < r

    proof

      thus (s - r) < t & (s + r) > t implies |.(t - s).| < r

      proof

        assume that

         A1: (s - r) < t and

         A2: (s + r) > t;

        (( - r) + s) < t by A1;

        then

         A3: ( - r) < (t - s) by XREAL_1: 20;

        (t - s) < r by A2, XREAL_1: 19;

        hence thesis by A3, SEQ_2: 1;

      end;

      assume

       A4: |.(t - s).| < r;

      then ( - r) < (t - s) by SEQ_2: 1;

      then

       A5: (s + ( - r)) < t by XREAL_1: 20;

      (t - s) < r by A4, SEQ_2: 1;

      hence thesis by A5, XREAL_1: 19;

    end;

    definition

      let seq be Real_Sequence;

      :: RINFSUP1:def1

      func upper_bound seq -> Real equals ( upper_bound ( rng seq));

      coherence ;

    end

    definition

      let seq be Real_Sequence;

      :: RINFSUP1:def2

      func lower_bound seq -> Real equals ( lower_bound ( rng seq));

      coherence ;

    end

    theorem :: RINFSUP1:2

    

     Th2: ((seq1 + seq2) - seq2) = seq1

    proof

      for n be Element of NAT holds (((seq1 + seq2) - seq2) . n) = (seq1 . n)

      proof

        let n be Element of NAT ;

        (((seq1 + seq2) - seq2) . n) = ((seq1 + (seq2 - seq2)) . n) by SEQ_1: 31

        .= ((seq1 . n) + ((seq2 + ( - seq2)) . n)) by SEQ_1: 7

        .= ((seq1 . n) + ((seq2 . n) + (( - seq2) . n))) by SEQ_1: 7

        .= ((seq1 . n) + ((seq2 . n) + ( - (seq2 . n)))) by SEQ_1: 10

        .= (seq1 . n);

        hence thesis;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RINFSUP1:3

    

     Th3: r in ( rng seq) iff ( - r) in ( rng ( - seq))

    proof

      thus r in ( rng seq) implies ( - r) in ( rng ( - seq))

      proof

        assume r in ( rng seq);

        then

        consider n be Element of NAT such that

         A1: r = (seq . n) by FUNCT_2: 113;

        ( - r) = (( - seq) . n) by A1, SEQ_1: 10;

        hence thesis by VALUED_0: 28;

      end;

      assume ( - r) in ( rng ( - seq));

      then

      consider n be Element of NAT such that

       A2: ( - r) = (( - seq) . n) by FUNCT_2: 113;

      r = ( - (( - seq) . n)) by A2;

      then r = ( - ( - (seq . n))) by SEQ_1: 10;

      hence thesis by VALUED_0: 28;

    end;

    theorem :: RINFSUP1:4

    

     Th4: ( rng ( - seq)) = ( -- ( rng seq))

    proof

      thus ( rng ( - seq)) c= ( -- ( rng seq))

      proof

        let x be object;

        assume

         A1: x in ( rng ( - seq));

        then

        reconsider r = x as Real;

        ( - r) in ( rng ( - ( - seq))) by A1, Th3;

        then ( - ( - r)) in ( -- ( rng seq)) by MEASURE6: 40;

        hence thesis;

      end;

      let x be object;

      assume

       A2: x in ( -- ( rng seq));

      then

      reconsider r = x as Real;

      ( - r) in ( -- ( -- ( rng seq))) by A2, MEMBER_1: 12;

      then ( - ( - r)) in ( rng ( - seq)) by Th3;

      hence thesis;

    end;

    theorem :: RINFSUP1:5

    

     Th5: seq is bounded_above iff ( rng seq) is bounded_above

    proof

      

       A1: seq is bounded_above implies ( rng seq) is bounded_above

      proof

        assume seq is bounded_above;

        then

        consider t such that

         A2: for n holds (seq . n) < t by SEQ_2:def 3;

        t is UpperBound of ( rng seq)

        proof

          let r be ExtReal;

          assume r in ( rng seq);

          then ex n be object st n in ( dom seq) & (seq . n) = r by FUNCT_1:def 3;

          hence r <= t by A2;

        end;

        hence thesis;

      end;

      ( rng seq) is bounded_above implies seq is bounded_above

      proof

        assume ( rng seq) is bounded_above;

        then

        consider t such that

         A3: t is UpperBound of ( rng seq);

        

         A4: for r st r in ( rng seq) holds r <= t by A3, XXREAL_2:def 1;

        now

          let n;

          

           A5: n in NAT by ORDINAL1:def 12;

          (seq . n) <= t by A4, FUNCT_2: 4, A5;

          hence (seq . n) < (t + 1) by Lm1;

        end;

        hence thesis by SEQ_2:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: RINFSUP1:6

    

     Th6: seq is bounded_below iff ( rng seq) is bounded_below

    proof

      

       A1: seq is bounded_below implies ( rng seq) is bounded_below

      proof

        assume seq is bounded_below;

        then

        consider t such that

         A2: for n holds t < (seq . n) by SEQ_2:def 4;

        t is LowerBound of ( rng seq)

        proof

          let r be ExtReal;

          assume r in ( rng seq);

          then ex n be object st n in ( dom seq) & (seq . n) = r by FUNCT_1:def 3;

          hence t <= r by A2;

        end;

        hence thesis;

      end;

      ( rng seq) is bounded_below implies seq is bounded_below

      proof

        assume ( rng seq) is bounded_below;

        then

        consider t such that

         A3: t is LowerBound of ( rng seq);

        

         A4: for r st r in ( rng seq) holds t <= r by A3, XXREAL_2:def 2;

        now

          let n;

          

           A5: n in NAT by ORDINAL1:def 12;

          t <= (seq . n) by A4, FUNCT_2: 4, A5;

          hence (t - 1) < (seq . n) by Lm1;

        end;

        hence thesis by SEQ_2:def 4;

      end;

      hence thesis by A1;

    end;

    theorem :: RINFSUP1:7

    

     Th7: seq is bounded_above implies (r = ( upper_bound seq) iff (for n holds (seq . n) <= r) & for s st 0 < s holds ex k st (r - s) < (seq . k))

    proof

      set R = ( rng seq);

      assume seq is bounded_above;

      then

       A1: ( rng seq) is bounded_above by Th5;

      

       A2: ( rng seq) <> {} by RELAT_1: 41;

      

       A3: (for n holds (seq . n) <= r) & (for s st 0 < s holds ex k st (r - s) < (seq . k)) implies r = ( upper_bound seq)

      proof

        assume that

         A4: for n holds (seq . n) <= r and

         A5: for s st 0 < s holds ex k st (r - s) < (seq . k);

         A6:

        now

          let s;

          assume 0 < s;

          then

          consider k such that

           A7: (r - s) < (seq . k) by A5;

          

           A8: k in NAT by ORDINAL1:def 12;

          consider r2 such that

           A9: r2 in R & r2 = (seq . k) by FUNCT_2: 4, A8;

          take r2;

          thus r2 in R & (r - s) < r2 by A7, A9;

        end;

        now

          let r1;

          assume r1 in R;

          then ex n be object st n in ( dom seq) & (seq . n) = r1 by FUNCT_1:def 3;

          hence r1 <= r by A4;

        end;

        hence thesis by A1, A2, A6, SEQ_4:def 1;

      end;

      r = ( upper_bound seq) implies (for n holds (seq . n) <= r) & for s st 0 < s holds ex k st (r - s) < (seq . k)

      proof

        assume

         A10: r = ( upper_bound seq);

         A11:

        now

          let s;

          assume 0 < s;

          then

          consider r2 such that

           A12: r2 in R and

           A13: (r - s) < r2 by A1, A2, A10, SEQ_4:def 1;

          consider k be Nat such that

           A14: r2 = (seq . k) by A12, SETLIM_1: 4;

          reconsider k as Nat;

          take k;

          thus (r - s) < (seq . k) by A13, A14;

        end;

        now

          let n;

          

           A15: n in NAT by ORDINAL1:def 12;

          (seq . n) in R by FUNCT_2: 4, A15;

          hence (seq . n) <= r by A1, A10, SEQ_4:def 1;

        end;

        hence thesis by A11;

      end;

      hence thesis by A3;

    end;

    theorem :: RINFSUP1:8

    

     Th8: seq is bounded_below implies (r = ( lower_bound seq) iff (for n holds r <= (seq . n)) & for s st 0 < s holds ex k st (seq . k) < (r + s))

    proof

      set R = ( rng seq);

      assume seq is bounded_below;

      then

       A1: ( rng seq) is bounded_below by Th6;

      

       A2: ( rng seq) <> {} by RELAT_1: 41;

      

       A3: (for n holds r <= (seq . n)) & (for s st 0 < s holds ex k st (seq . k) < (r + s)) implies r = ( lower_bound seq)

      proof

        assume that

         A4: for n holds r <= (seq . n) and

         A5: for s st 0 < s holds ex k st (seq . k) < (r + s);

         A6:

        now

          let s;

          assume 0 < s;

          then

          consider k such that

           A7: (seq . k) < (r + s) by A5;

          

           A8: k in NAT by ORDINAL1:def 12;

          consider r2 such that

           A9: r2 in R & r2 = (seq . k) by FUNCT_2: 4, A8;

          take r2;

          thus r2 in R & r2 < (r + s) by A7, A9;

        end;

        now

          let r1;

          assume r1 in R;

          then ex n be object st n in ( dom seq) & (seq . n) = r1 by FUNCT_1:def 3;

          hence r <= r1 by A4;

        end;

        hence thesis by A1, A2, A6, SEQ_4:def 2;

      end;

      r = ( lower_bound seq) implies (for n holds r <= (seq . n)) & for s st 0 < s holds ex k st (seq . k) < (r + s)

      proof

        assume

         A10: r = ( lower_bound seq);

         A11:

        now

          let s;

          assume 0 < s;

          then

          consider r2 such that

           A12: r2 in R and

           A13: r2 < (r + s) by A1, A2, A10, SEQ_4:def 2;

          consider k be Nat such that

           A14: r2 = (seq . k) by A12, SETLIM_1: 4;

          reconsider k as Nat;

          take k;

          thus (seq . k) < (r + s) by A13, A14;

        end;

        now

          let n;

          n in NAT by ORDINAL1:def 12;

          then (seq . n) in R by FUNCT_2: 4;

          hence r <= (seq . n) by A1, A10, SEQ_4:def 2;

        end;

        hence thesis by A11;

      end;

      hence thesis by A3;

    end;

    theorem :: RINFSUP1:9

    

     Th9: (for n holds (seq . n) <= r) iff seq is bounded_above & ( upper_bound seq) <= r

    proof

      thus (for n holds (seq . n) <= r) implies seq is bounded_above & ( upper_bound seq) <= r

      proof

        assume

         A1: for n holds (seq . n) <= r;

        now

          let m;

          (seq . m) <= r by A1;

          hence (seq . m) < (r + 1) by Lm1;

        end;

        hence

         A2: seq is bounded_above by SEQ_2:def 3;

        now

          set r1 = (( upper_bound seq) - r);

          assume r < ( upper_bound seq);

          then r1 > 0 by XREAL_1: 50;

          then ex k st (( upper_bound seq) - r1) < (seq . k) by A2, Th7;

          hence contradiction by A1;

        end;

        hence thesis;

      end;

      assume that

       A3: seq is bounded_above and

       A4: ( upper_bound seq) <= r;

      now

        let n;

        (seq . n) <= ( upper_bound seq) by A3, Th7;

        hence (seq . n) <= r by A4, XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: RINFSUP1:10

    

     Th10: (for n holds r <= (seq . n)) iff seq is bounded_below & r <= ( lower_bound seq)

    proof

      thus (for n holds r <= (seq . n)) implies seq is bounded_below & r <= ( lower_bound seq)

      proof

        assume

         A1: for n holds r <= (seq . n);

        now

          let m;

          r <= (seq . m) by A1;

          hence (r - 1) < (seq . m) by Lm1;

        end;

        hence

         A2: seq is bounded_below by SEQ_2:def 4;

        now

          set r1 = (r - ( lower_bound seq));

          assume r > ( lower_bound seq);

          then r1 > 0 by XREAL_1: 50;

          then ex k st (seq . k) < (( lower_bound seq) + r1) by A2, Th8;

          hence contradiction by A1;

        end;

        hence thesis;

      end;

      assume that

       A3: seq is bounded_below and

       A4: r <= ( lower_bound seq);

      now

        let n;

        ( lower_bound seq) <= (seq . n) by A3, Th8;

        hence r <= (seq . n) by A4, XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: RINFSUP1:11

    seq is bounded_above iff ( - seq) is bounded_below

    proof

      set seq1 = ( - seq);

      thus seq is bounded_above implies ( - seq) is bounded_below;

      assume seq1 is bounded_below;

      then

      consider t such that

       A1: for n holds (seq1 . n) > t by SEQ_2:def 4;

      for n holds (seq . n) < ( - t)

      proof

        let n;

        (seq1 . n) = ( - (seq . n)) by SEQ_1: 10;

        then

         A2: ( - (seq1 . n)) = (seq . n);

        (seq1 . n) > t by A1;

        hence thesis by A2, XREAL_1: 24;

      end;

      hence thesis by SEQ_2:def 3;

    end;

    theorem :: RINFSUP1:12

    seq is bounded_below iff ( - seq) is bounded_above

    proof

      ( - ( - seq)) = seq;

      hence thesis;

    end;

    theorem :: RINFSUP1:13

    

     Th13: seq is bounded_above implies ( upper_bound seq) = ( - ( lower_bound ( - seq)))

    proof

      assume seq is bounded_above;

      then ( rng seq) is non empty bounded_above by Th5, RELAT_1: 41;

      

      then ( upper_bound ( rng seq)) = ( - ( lower_bound ( -- ( rng seq)))) by MEASURE6: 44

      .= ( - ( lower_bound ( rng ( - seq)))) by Th4;

      hence thesis;

    end;

    theorem :: RINFSUP1:14

    

     Th14: seq is bounded_below implies ( lower_bound seq) = ( - ( upper_bound ( - seq)))

    proof

      assume seq is bounded_below;

      then ( rng seq) is non empty bounded_below by Th6, RELAT_1: 41;

      

      then ( lower_bound ( rng seq)) = ( - ( upper_bound ( -- ( rng seq)))) by MEASURE6: 43

      .= ( - ( upper_bound ( rng ( - seq)))) by Th4;

      hence thesis;

    end;

    theorem :: RINFSUP1:15

    

     Th15: seq1 is bounded_below & seq2 is bounded_below implies ( lower_bound (seq1 + seq2)) >= (( lower_bound seq1) + ( lower_bound seq2))

    proof

      assume that

       A1: seq1 is bounded_below and

       A2: seq2 is bounded_below;

      for n holds ((seq1 + seq2) . n) >= (( lower_bound seq1) + ( lower_bound seq2))

      proof

        let n;

        

         A3: (seq2 . n) >= ( lower_bound seq2) by A2, Th8;

        ((seq1 + seq2) . n) = ((seq1 . n) + (seq2 . n)) & (seq1 . n) >= ( lower_bound seq1) by A1, Th8, SEQ_1: 7;

        hence thesis by A3, XREAL_1: 7;

      end;

      hence thesis by Th10;

    end;

    theorem :: RINFSUP1:16

    

     Th16: seq1 is bounded_above & seq2 is bounded_above implies ( upper_bound (seq1 + seq2)) <= (( upper_bound seq1) + ( upper_bound seq2))

    proof

      assume that

       A1: seq1 is bounded_above and

       A2: seq2 is bounded_above;

      for n holds ((seq1 + seq2) . n) <= (( upper_bound seq1) + ( upper_bound seq2))

      proof

        let n;

        

         A3: (seq2 . n) <= ( upper_bound seq2) by A2, Th7;

        ((seq1 + seq2) . n) = ((seq1 . n) + (seq2 . n)) & (seq1 . n) <= ( upper_bound seq1) by A1, Th7, SEQ_1: 7;

        hence thesis by A3, XREAL_1: 7;

      end;

      hence thesis by Th9;

    end;

    notation

      let f be Real_Sequence;

      synonym f is nonnegative for f is nonnegative-yielding;

    end

    definition

      let f be Real_Sequence;

      :: original: nonnegative

      redefine

      :: RINFSUP1:def3

      attr f is nonnegative means for n holds (f . n) >= 0 ;

      compatibility

      proof

        thus f is nonnegative implies for n holds (f . n) >= 0 by VALUED_0: 28;

        assume

         A1: for n holds (f . n) >= 0 ;

        let r be Real;

        assume r in ( rng f);

        then ex x be Element of NAT st r = (f . x) by FUNCT_2: 113;

        hence thesis by A1;

      end;

    end

    theorem :: RINFSUP1:17

    

     Th17: seq is nonnegative implies (seq ^\ k) is nonnegative

    proof

      assume

       A1: seq is nonnegative;

      for n holds ((seq ^\ k) . n) >= 0

      proof

        let n;

        ((seq ^\ k) . n) = (seq . (n + k)) by NAT_1:def 3;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: RINFSUP1:18

    

     Th18: seq is bounded_below nonnegative implies ( lower_bound seq) >= 0 by Th10;

    theorem :: RINFSUP1:19

    seq is bounded_above nonnegative implies ( upper_bound seq) >= 0

    proof

      assume

       A1: seq is bounded_above nonnegative;

      then

       A2: (seq . 0 ) <= ( upper_bound seq) by Th7;

       0 <= (seq . 0 ) by A1;

      hence thesis by A2;

    end;

    theorem :: RINFSUP1:20

    

     Th20: seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative implies (seq1 (#) seq2) is bounded_below & ( lower_bound (seq1 (#) seq2)) >= (( lower_bound seq1) * ( lower_bound seq2))

    proof

      assume that

       A1: seq1 is bounded_below nonnegative and

       A2: seq2 is bounded_below nonnegative;

      for n holds ((seq1 (#) seq2) . n) >= (( lower_bound seq1) * ( lower_bound seq2))

      proof

        let n;

        

         A3: ((seq1 (#) seq2) . n) = ((seq1 . n) * (seq2 . n)) & (seq1 . n) >= ( lower_bound seq1) by A1, Th8, SEQ_1: 8;

        

         A4: ( lower_bound seq2) >= 0 by A2, Th18;

        (seq2 . n) >= ( lower_bound seq2) & ( lower_bound seq1) >= 0 by A1, A2, Th8, Th18;

        hence thesis by A3, A4, XREAL_1: 66;

      end;

      hence thesis by Th10;

    end;

    theorem :: RINFSUP1:21

    

     Th21: seq1 is bounded_above nonnegative & seq2 is bounded_above nonnegative implies (seq1 (#) seq2) is bounded_above & ( upper_bound (seq1 (#) seq2)) <= (( upper_bound seq1) * ( upper_bound seq2))

    proof

      assume that

       A1: seq1 is bounded_above nonnegative and

       A2: seq2 is bounded_above nonnegative;

      for n holds ((seq1 (#) seq2) . n) <= (( upper_bound seq1) * ( upper_bound seq2))

      proof

        let n;

        

         A3: ((seq1 (#) seq2) . n) = ((seq1 . n) * (seq2 . n)) & (seq1 . n) <= ( upper_bound seq1) by A1, Th7, SEQ_1: 8;

        

         A4: (seq2 . n) >= 0 by A2;

        (seq2 . n) <= ( upper_bound seq2) & (seq1 . n) >= 0 by A1, A2, Th7;

        hence thesis by A3, A4, XREAL_1: 66;

      end;

      hence thesis by Th9;

    end;

    theorem :: RINFSUP1:22

    seq is non-decreasing bounded_above implies seq is bounded;

    theorem :: RINFSUP1:23

    seq is non-increasing bounded_below implies seq is bounded;

    theorem :: RINFSUP1:24

    

     Th24: seq is non-decreasing bounded_above implies ( lim seq) = ( upper_bound seq)

    proof

      assume

       A1: seq is non-decreasing bounded_above;

      then for n holds (seq . n) <= ( lim seq) by SEQ_4: 37;

      then

       A2: ( upper_bound seq) <= ( lim seq) by Th9;

      for n holds (seq . n) <= ( upper_bound seq) by A1, Th7;

      then ( lim seq) <= ( upper_bound seq) by A1, PREPOWER: 2;

      hence thesis by A2, XXREAL_0: 1;

    end;

    theorem :: RINFSUP1:25

    

     Th25: seq is non-increasing bounded_below implies ( lim seq) = ( lower_bound seq)

    proof

      assume

       A1: seq is non-increasing bounded_below;

      then for n holds ( lim seq) <= (seq . n) by SEQ_4: 38;

      then

       A2: ( lim seq) <= ( lower_bound seq) by Th10;

      for n holds ( lower_bound seq) <= (seq . n) by A1, Th8;

      then ( lower_bound seq) <= ( lim seq) by A1, PREPOWER: 1;

      hence thesis by A2, XXREAL_0: 1;

    end;

    theorem :: RINFSUP1:26

    seq is bounded_above implies (seq ^\ k) is bounded_above by SEQM_3: 27;

    theorem :: RINFSUP1:27

    seq is bounded_below implies (seq ^\ k) is bounded_below by SEQM_3: 28;

    theorem :: RINFSUP1:28

    seq is bounded implies (seq ^\ k) is bounded by SEQM_3: 29;

    theorem :: RINFSUP1:29

    

     Th29: for seq, n holds { (seq . k) : n <= k } is Subset of REAL

    proof

      let seq, n;

      set Y = { (seq . k) : n <= k };

      now

        let x be object;

        assume x in Y;

        then

        consider z1 be set such that

         A1: z1 = x and

         A2: z1 in Y;

        consider k1 be Nat such that

         A3: z1 = (seq . k1) & n <= k1 by A2;

        reconsider k1 as Element of NAT by ORDINAL1:def 12;

        z1 = (seq . k1) by A3;

        hence x in REAL by A1;

      end;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: RINFSUP1:30

    

     Th30: ( rng (seq ^\ k)) = { (seq . n) where n : k <= n }

    proof

      set seq1 = (seq ^\ k);

      set Z = { (seq . m) where m : k <= m };

      now

        let x be object;

        assume x in Z;

        then

        consider k1 be Nat such that

         A1: x = (seq . k1) and

         A2: k <= k1;

        consider k2 be Nat such that

         A3: k1 = (k + k2) by A2, NAT_1: 10;

        reconsider k2 as Element of NAT by ORDINAL1:def 12;

        x = (seq1 . k2) by A1, A3, NAT_1:def 3;

        hence x in ( rng seq1) by FUNCT_2: 4;

      end;

      then

       A4: Z c= ( rng seq1);

      

       A5: ( dom seq1) = NAT by FUNCT_2:def 1;

      now

        let y be object;

        assume y in ( rng seq1);

        then

        consider m1 be object such that

         A6: m1 in NAT and

         A7: y = (seq1 . m1) by A5, FUNCT_1:def 3;

        reconsider m1 as Nat by A6;

        reconsider km1 = (k + m1) as Nat;

        y = (seq . km1) by A7, NAT_1:def 3;

        hence y in Z by SETLIM_1: 1;

      end;

      then ( rng seq1) c= Z;

      hence thesis by A4;

    end;

    theorem :: RINFSUP1:31

    

     Th31: seq is bounded_above implies for n holds for R be Subset of REAL st R = { (seq . k) : n <= k } holds R is bounded_above

    proof

      assume

       A1: seq is bounded_above;

      let n;

      set seq1 = (seq ^\ n);

      seq1 is bounded_above by A1, SEQM_3: 27;

      then

       A2: ( rng seq1) is bounded_above by Th5;

      let R be Subset of REAL ;

      assume R = { (seq . k) : n <= k };

      hence thesis by A2, Th30;

    end;

    theorem :: RINFSUP1:32

    

     Th32: seq is bounded_below implies for n holds for R be Subset of REAL st R = { (seq . k) : n <= k } holds R is bounded_below

    proof

      assume

       A1: seq is bounded_below;

      let n;

      set seq1 = (seq ^\ n);

      seq1 is bounded_below by A1, SEQM_3: 28;

      then

       A2: ( rng seq1) is bounded_below by Th6;

      let R be Subset of REAL ;

      assume R = { (seq . k) : n <= k };

      hence thesis by A2, Th30;

    end;

    theorem :: RINFSUP1:33

    

     Th33: seq is bounded implies for n holds for R be Subset of REAL st R = { (seq . k) : n <= k } holds R is real-bounded by Th31, Th32;

    theorem :: RINFSUP1:34

    

     Th34: seq is non-decreasing implies for n holds for R be Subset of REAL st R = { (seq . k) : n <= k } holds ( lower_bound R) = (seq . n)

    proof

      assume

       A1: seq is non-decreasing;

      let n;

       A2:

      now

        let r;

        assume r in { (seq . k) : n <= k };

        then

        consider r1 be Real such that

         A3: r = r1 & r1 in { (seq . k) : n <= k };

        consider k1 such that

         A4: r1 = (seq . k1) and

         A5: n <= k1 by A3;

        consider k be Nat such that

         A6: (n + k) = k1 by A5, NAT_1: 10;

        thus (seq . n) <= r by A1, A3, A4, A6, SEQM_3: 5;

      end;

      let R be Subset of REAL ;

       A7:

      now

        let s;

        

         A8: (seq . n) in { (seq . k) : n <= k };

        assume 0 < s;

        hence ex r st r in { (seq . k) : n <= k } & r < ((seq . n) + s) by A8, XREAL_1: 29;

      end;

      assume

       A9: R = { (seq . k) : n <= k };

      then

       A10: R <> {} by SETLIM_1: 1;

      R is bounded_below by A1, A9, Th32, LIMFUNC1: 1;

      hence thesis by A9, A10, A2, A7, SEQ_4:def 2;

    end;

    theorem :: RINFSUP1:35

    

     Th35: seq is non-increasing implies for n holds for R be Subset of REAL st R = { (seq . k) : n <= k } holds ( upper_bound R) = (seq . n)

    proof

      assume

       A1: seq is non-increasing;

      let n;

       A2:

      now

        let r;

        assume r in { (seq . k) : n <= k };

        then

        consider r1 be Real such that

         A3: r = r1 & r1 in { (seq . k) : n <= k };

        consider k1 such that

         A4: r1 = (seq . k1) and

         A5: n <= k1 by A3;

        consider k be Nat such that

         A6: (n + k) = k1 by A5, NAT_1: 10;

        thus r <= (seq . n) by A1, A3, A4, A6, SEQM_3: 7;

      end;

      let R be Subset of REAL ;

       A7:

      now

        let s;

        

         A8: (seq . n) in { (seq . k) : n <= k };

        assume 0 < s;

        hence ex r st r in { (seq . k) : n <= k } & ((seq . n) - s) < r by A8, XREAL_1: 44;

      end;

      assume

       A9: R = { (seq . k) : n <= k };

      then

       A10: R <> {} by SETLIM_1: 1;

      R is bounded_above by A1, A9, Th31, LIMFUNC1: 1;

      hence thesis by A9, A10, A2, A7, SEQ_4:def 1;

    end;

    definition

      let seq be Real_Sequence;

      :: RINFSUP1:def4

      func inferior_realsequence seq -> Real_Sequence means

      : Def4: for n holds for Y be Subset of REAL st Y = { (seq . k) : n <= k } holds (it . n) = ( lower_bound Y);

      existence

      proof

        defpred P[ Element of NAT , Element of REAL ] means for Y be Subset of REAL st Y = { (seq . k) : $1 <= k } holds $2 = ( lower_bound Y);

        

         A1: for n be Element of NAT holds ex y be Element of REAL st P[n, y]

        proof

          let n be Element of NAT ;

          reconsider Y = { (seq . k) : n <= k } as Subset of REAL by Th29;

          reconsider y = ( lower_bound Y) as Element of REAL by XREAL_0:def 1;

          for Y be Subset of REAL st Y = { (seq . k) : n <= k } holds y = ( lower_bound Y);

          hence thesis;

        end;

        consider f be sequence of REAL such that

         A2: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A1);

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let seq1,seq2 be Real_Sequence such that

         A3: for n holds for Y be Subset of REAL st Y = { (seq . k) : n <= k } holds (seq1 . n) = ( lower_bound Y) and

         A4: for m holds for Y be Subset of REAL st Y = { (seq . k) : m <= k } holds (seq2 . m) = ( lower_bound Y);

        

         A5: for y be object st y in NAT holds (seq1 . y) = (seq2 . y)

        proof

          let y be object;

          assume y in NAT ;

          then

          reconsider y as Element of NAT ;

          reconsider Y = { (seq . k) : y <= k } as Subset of REAL by Th29;

          (seq1 . y) = ( lower_bound Y) by A3;

          hence thesis by A4;

        end;

         NAT = ( dom seq1) & NAT = ( dom seq2) by FUNCT_2:def 1;

        hence thesis by A5, FUNCT_1: 2;

      end;

    end

    definition

      let seq be Real_Sequence;

      :: RINFSUP1:def5

      func superior_realsequence seq -> Real_Sequence means

      : Def5: for n holds for Y be Subset of REAL st Y = { (seq . k) : n <= k } holds (it . n) = ( upper_bound Y);

      existence

      proof

        defpred P[ Element of NAT , Element of REAL ] means for Y be Subset of REAL st Y = { (seq . k) : $1 <= k } holds $2 = ( upper_bound Y);

        

         A1: for n be Element of NAT holds ex y be Element of REAL st P[n, y]

        proof

          let n be Element of NAT ;

          reconsider Y = { (seq . k) : n <= k } as Subset of REAL by Th29;

          reconsider y = ( upper_bound Y) as Element of REAL by XREAL_0:def 1;

          for Y be Subset of REAL st Y = { (seq . k) : n <= k } holds y = ( upper_bound Y);

          hence thesis;

        end;

        consider f be sequence of REAL such that

         A2: for n be Element of NAT holds P[n, (f . n)] from FUNCT_2:sch 3( A1);

        take f;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let seq1,seq2 be Real_Sequence such that

         A3: for n holds for Y be Subset of REAL st Y = { (seq . k) : n <= k } holds (seq1 . n) = ( upper_bound Y) and

         A4: for m holds for Y be Subset of REAL st Y = { (seq . k) : m <= k } holds (seq2 . m) = ( upper_bound Y);

        

         A5: for y be object st y in NAT holds (seq1 . y) = (seq2 . y)

        proof

          let y be object;

          assume y in NAT ;

          then

          reconsider y as Element of NAT ;

          reconsider Y = { (seq . k) : y <= k } as Subset of REAL by Th29;

          (seq1 . y) = ( upper_bound Y) by A3;

          hence thesis by A4;

        end;

         NAT = ( dom seq1) & NAT = ( dom seq2) by FUNCT_2:def 1;

        hence thesis by A5, FUNCT_1: 2;

      end;

    end

    theorem :: RINFSUP1:36

    

     Th36: (( inferior_realsequence seq) . n) = ( lower_bound (seq ^\ n))

    proof

      reconsider Y = { (seq . k) : n <= k } as Subset of REAL by Th29;

      (( inferior_realsequence seq) . n) = ( lower_bound Y) by Def4

      .= ( lower_bound ( rng (seq ^\ n))) by Th30;

      hence thesis;

    end;

    theorem :: RINFSUP1:37

    

     Th37: (( superior_realsequence seq) . n) = ( upper_bound (seq ^\ n))

    proof

      reconsider Y = { (seq . k) : n <= k } as Subset of REAL by Th29;

      (( superior_realsequence seq) . n) = ( upper_bound Y) by Def5

      .= ( upper_bound ( rng (seq ^\ n))) by Th30;

      hence thesis;

    end;

    theorem :: RINFSUP1:38

    

     Th38: seq is bounded_below implies (( inferior_realsequence seq) . 0 ) = ( lower_bound seq)

    proof

      reconsider Y1 = { (seq . k) : 0 <= k } as Subset of REAL by Th29;

      (( inferior_realsequence seq) . 0 ) = ( lower_bound Y1) by Def4

      .= ( lower_bound seq) by SETLIM_1: 5;

      hence thesis;

    end;

    theorem :: RINFSUP1:39

    

     Th39: seq is bounded_above implies (( superior_realsequence seq) . 0 ) = ( upper_bound seq)

    proof

      reconsider Y1 = { (seq . k) : 0 <= k } as Subset of REAL by Th29;

      (( superior_realsequence seq) . 0 ) = ( upper_bound Y1) by Def5

      .= ( upper_bound seq) by SETLIM_1: 5;

      hence thesis;

    end;

    theorem :: RINFSUP1:40

    

     Th40: seq is bounded_below implies (r = (( inferior_realsequence seq) . n) iff (for k holds r <= (seq . (n + k))) & for s st 0 < s holds ex k st (seq . (n + k)) < (r + s))

    proof

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      assume seq is bounded_below;

      then

       A1: Y1 is non empty bounded_below by Th32, SETLIM_1: 1;

      thus r = (( inferior_realsequence seq) . n) implies (for k holds r <= (seq . (n + k))) & for s st 0 < s holds ex k st (seq . (n + k)) < (r + s)

      proof

        assume r = (( inferior_realsequence seq) . n);

        then

         A2: r = ( lower_bound Y1) by Def4;

        

         A3: for s st 0 < s holds ex k st (seq . (n + k)) < (r + s)

        proof

          let s;

          assume 0 < s;

          then

          consider r1 such that

           A4: r1 in Y1 and

           A5: r1 < (r + s) by A1, A2, SEQ_4:def 2;

          consider k1 such that

           A6: r1 = (seq . k1) and

           A7: n <= k1 by A4;

          consider k2 be Nat such that

           A8: k1 = (n + k2) by A7, NAT_1: 10;

          thus thesis by A5, A6, A8;

        end;

        for k holds r <= (seq . (n + k))

        proof

          let k;

          (seq . (n + k)) in Y1 by SETLIM_1: 1;

          hence thesis by A1, A2, SEQ_4:def 2;

        end;

        hence thesis by A3;

      end;

      assume that

       A9: for k holds r <= (seq . (n + k)) and

       A10: for s st 0 < s holds ex k st (seq . (n + k)) < (r + s);

      

       A11: for s st 0 < s holds ex r1 st r1 in Y1 & r1 < (r + s)

      proof

        let s;

        assume 0 < s;

        then

        consider k such that

         A12: (seq . (n + k)) < (r + s) by A10;

        (n + k) >= n by NAT_1: 11;

        then (seq . (n + k)) in Y1;

        hence thesis by A12;

      end;

      for r1 st r1 in Y1 holds r <= r1

      proof

        let r1;

        assume r1 in Y1;

        then

        consider k1 such that

         A13: r1 = (seq . k1) and

         A14: n <= k1;

        consider k2 be Nat such that

         A15: k1 = (n + k2) by A14, NAT_1: 10;

        thus thesis by A9, A13, A15;

      end;

      then r = ( lower_bound Y1) by A1, A11, SEQ_4:def 2;

      hence thesis by Def4;

    end;

    theorem :: RINFSUP1:41

    

     Th41: seq is bounded_above implies (r = (( superior_realsequence seq) . n) iff (for k holds (seq . (n + k)) <= r) & for s st 0 < s holds ex k st (r - s) < (seq . (n + k)))

    proof

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      assume seq is bounded_above;

      then

       A1: Y1 is non empty bounded_above by Th31, SETLIM_1: 1;

      thus r = (( superior_realsequence seq) . n) implies (for k holds (seq . (n + k)) <= r) & for s st 0 < s holds ex k st (r - s) < (seq . (n + k))

      proof

        assume r = (( superior_realsequence seq) . n);

        then

         A2: r = ( upper_bound Y1) by Def5;

        

         A3: for s st 0 < s holds ex k st (r - s) < (seq . (n + k))

        proof

          let s;

          assume 0 < s;

          then

          consider r1 such that

           A4: r1 in Y1 and

           A5: (r - s) < r1 by A1, A2, SEQ_4:def 1;

          consider k1 such that

           A6: r1 = (seq . k1) and

           A7: n <= k1 by A4;

          consider k2 be Nat such that

           A8: k1 = (n + k2) by A7, NAT_1: 10;

          thus thesis by A5, A6, A8;

        end;

        for k holds (seq . (n + k)) <= r

        proof

          let k;

          (seq . (n + k)) in Y1 by SETLIM_1: 1;

          hence thesis by A1, A2, SEQ_4:def 1;

        end;

        hence thesis by A3;

      end;

      assume that

       A9: for k holds (seq . (n + k)) <= r and

       A10: for s st 0 < s holds ex k st (r - s) < (seq . (n + k));

      

       A11: for s st 0 < s holds ex r1 st r1 in Y1 & (r - s) < r1

      proof

        let s;

        assume 0 < s;

        then

        consider k such that

         A12: (r - s) < (seq . (n + k)) by A10;

        (n + k) >= n by NAT_1: 11;

        then (seq . (n + k)) in Y1;

        hence thesis by A12;

      end;

      for r1 st r1 in Y1 holds r1 <= r

      proof

        let r1;

        assume r1 in Y1;

        then

        consider k1 such that

         A13: r1 = (seq . k1) and

         A14: n <= k1;

        consider k2 be Nat such that

         A15: k1 = (n + k2) by A14, NAT_1: 10;

        thus thesis by A9, A13, A15;

      end;

      then r = ( upper_bound Y1) by A1, A11, SEQ_4:def 1;

      hence thesis by Def5;

    end;

    theorem :: RINFSUP1:42

    

     Th42: seq is bounded_below implies ((for k holds r <= (seq . (n + k))) iff r <= (( inferior_realsequence seq) . n))

    proof

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      set seq1 = (seq ^\ n);

      assume seq is bounded_below;

      then

       A1: seq1 is bounded_below by SEQM_3: 28;

      

       A2: ( rng seq1) = Y1 by Th30;

      thus (for k holds r <= (seq . (n + k))) implies r <= (( inferior_realsequence seq) . n)

      proof

        assume

         A3: for k holds r <= (seq . (n + k));

        now

          let n1 be Nat;

          n1 in NAT by ORDINAL1:def 12;

          then (seq1 . n1) in ( rng seq1) by FUNCT_2: 4;

          then

          consider r1 such that

           A4: (seq1 . n1) = r1 and

           A5: r1 in Y1 by A2;

          consider k1 be Nat such that

           A6: r1 = (seq . k1) and

           A7: n <= k1 by A5;

          consider k2 be Nat such that

           A8: k1 = (n + k2) by A7, NAT_1: 10;

          thus r <= (seq1 . n1) by A3, A4, A6, A8;

        end;

        then r <= ( lower_bound seq1) by Th10;

        then r <= ( lower_bound Y1) by Th30;

        hence thesis by Def4;

      end;

      assume r <= (( inferior_realsequence seq) . n);

      then r <= ( lower_bound Y1) by Def4;

      then

       A9: r <= ( lower_bound seq1) by Th30;

      now

        let m1 be Nat;

        n <= (n + m1) by NAT_1: 11;

        then (seq . (n + m1)) in Y1;

        then (seq . (n + m1)) in ( rng seq1) by Th30;

        then ex k be object st k in ( dom seq1) & (seq1 . k) = (seq . (n + m1)) by FUNCT_1:def 3;

        hence r <= (seq . (n + m1)) by A1, A9, Th10;

      end;

      hence thesis;

    end;

    theorem :: RINFSUP1:43

    

     Th43: seq is bounded_below implies ((for m st n <= m holds r <= (seq . m)) iff r <= (( inferior_realsequence seq) . n))

    proof

      assume

       A1: seq is bounded_below;

      thus (for m st n <= m holds r <= (seq . m)) implies r <= (( inferior_realsequence seq) . n)

      proof

        assume for m st n <= m holds r <= (seq . m);

        then for k holds r <= (seq . (n + k)) by NAT_1: 11;

        hence thesis by A1, Th42;

      end;

      assume

       A2: r <= (( inferior_realsequence seq) . n);

      now

        let m;

        assume n <= m;

        then

        consider k be Nat such that

         A3: m = (n + k) by NAT_1: 10;

        thus r <= (seq . m) by A1, A2, A3, Th42;

      end;

      hence thesis;

    end;

    theorem :: RINFSUP1:44

    

     Th44: seq is bounded_above implies ((for k holds (seq . (n + k)) <= r) iff (( superior_realsequence seq) . n) <= r)

    proof

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      set seq1 = (seq ^\ n);

      assume seq is bounded_above;

      then

       A1: seq1 is bounded_above by SEQM_3: 27;

      

       A2: ( rng seq1) = Y1 by Th30;

      thus (for k holds (seq . (n + k)) <= r) implies (( superior_realsequence seq) . n) <= r

      proof

        assume

         A3: for k holds (seq . (n + k)) <= r;

        now

          let n1 be Nat;

          n1 in NAT by ORDINAL1:def 12;

          then (seq1 . n1) in ( rng seq1) by FUNCT_2: 4;

          then

          consider r1 such that

           A4: (seq1 . n1) = r1 and

           A5: r1 in Y1 by A2;

          consider k1 be Nat such that

           A6: r1 = (seq . k1) and

           A7: n <= k1 by A5;

          consider k2 be Nat such that

           A8: k1 = (n + k2) by A7, NAT_1: 10;

          thus (seq1 . n1) <= r by A3, A4, A6, A8;

        end;

        then ( upper_bound seq1) <= r by Th9;

        then ( upper_bound Y1) <= r by Th30;

        hence thesis by Def5;

      end;

      assume (( superior_realsequence seq) . n) <= r;

      then ( upper_bound Y1) <= r by Def5;

      then

       A9: ( upper_bound seq1) <= r by Th30;

      now

        let m1 be Nat;

        n <= (n + m1) by NAT_1: 11;

        then (seq . (n + m1)) in Y1;

        then (seq . (n + m1)) in ( rng seq1) by Th30;

        then ex k be object st k in ( dom seq1) & (seq1 . k) = (seq . (n + m1)) by FUNCT_1:def 3;

        hence (seq . (n + m1)) <= r by A1, A9, Th9;

      end;

      hence thesis;

    end;

    theorem :: RINFSUP1:45

    

     Th45: seq is bounded_above implies ((for m st n <= m holds (seq . m) <= r) iff (( superior_realsequence seq) . n) <= r)

    proof

      assume

       A1: seq is bounded_above;

      thus (for m st n <= m holds (seq . m) <= r) implies (( superior_realsequence seq) . n) <= r

      proof

        assume for m st n <= m holds (seq . m) <= r;

        then for k holds (seq . (n + k)) <= r by NAT_1: 11;

        hence thesis by A1, Th44;

      end;

      assume

       A2: (( superior_realsequence seq) . n) <= r;

      now

        let m;

        assume n <= m;

        then

        consider k be Nat such that

         A3: m = (n + k) by NAT_1: 10;

        thus (seq . m) <= r by A1, A2, A3, Th44;

      end;

      hence thesis;

    end;

    theorem :: RINFSUP1:46

    

     Th46: seq is bounded_below implies (( inferior_realsequence seq) . n) = ( min ((( inferior_realsequence seq) . (n + 1)),(seq . n)))

    proof

      reconsider Y2 = { (seq . k) : (n + 1) <= k } as Subset of REAL by Th29;

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      reconsider Y3 = {(seq . n)} as Subset of REAL ;

      

       A1: (( inferior_realsequence seq) . (n + 1)) = ( lower_bound Y2) by Def4;

      assume

       A2: seq is bounded_below;

      then

       A3: Y2 <> {} & Y2 is bounded_below by Th32, SETLIM_1: 1;

      

       A4: Y3 is bounded_below

      proof

        consider t such that

         A5: for m holds t < (seq . m) by A2, SEQ_2:def 4;

        t is LowerBound of Y3

        proof

          let r be ExtReal;

          assume r in Y3;

          then r = (seq . n) by TARSKI:def 1;

          hence t <= r by A5;

        end;

        hence thesis;

      end;

      (( inferior_realsequence seq) . n) = ( lower_bound Y1) by Def4;

      

      then (( inferior_realsequence seq) . n) = ( lower_bound (Y2 \/ Y3)) by SETLIM_1: 2

      .= ( min (( lower_bound Y2),( lower_bound Y3))) by A3, A4, SEQ_4: 142

      .= ( min ((( inferior_realsequence seq) . (n + 1)),(seq . n))) by A1, SEQ_4: 9;

      hence thesis;

    end;

    theorem :: RINFSUP1:47

    

     Th47: seq is bounded_above implies (( superior_realsequence seq) . n) = ( max ((( superior_realsequence seq) . (n + 1)),(seq . n)))

    proof

      reconsider Y2 = { (seq . k) : (n + 1) <= k } as Subset of REAL by Th29;

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      reconsider Y3 = {(seq . n)} as Subset of REAL ;

      

       A1: (( superior_realsequence seq) . (n + 1)) = ( upper_bound Y2) by Def5;

      assume

       A2: seq is bounded_above;

      then

       A3: Y2 <> {} & Y2 is bounded_above by Th31, SETLIM_1: 1;

      

       A4: Y3 is bounded_above

      proof

        consider t such that

         A5: for m holds (seq . m) < t by A2, SEQ_2:def 3;

        t is UpperBound of Y3

        proof

          let r be ExtReal;

          assume r in Y3;

          then r = (seq . n) by TARSKI:def 1;

          hence r <= t by A5;

        end;

        hence thesis;

      end;

      (( superior_realsequence seq) . n) = ( upper_bound Y1) by Def5;

      

      then (( superior_realsequence seq) . n) = ( upper_bound (Y2 \/ Y3)) by SETLIM_1: 2

      .= ( max (( upper_bound Y2),( upper_bound Y3))) by A3, A4, SEQ_4: 143

      .= ( max ((( superior_realsequence seq) . (n + 1)),(seq . n))) by A1, SEQ_4: 9;

      hence thesis;

    end;

    theorem :: RINFSUP1:48

    

     Th48: seq is bounded_below implies (( inferior_realsequence seq) . n) <= (( inferior_realsequence seq) . (n + 1))

    proof

      

       A1: ( min ((( inferior_realsequence seq) . (n + 1)),(seq . n))) <= (( inferior_realsequence seq) . (n + 1)) by XXREAL_0: 17;

      assume seq is bounded_below;

      hence thesis by A1, Th46;

    end;

    theorem :: RINFSUP1:49

    

     Th49: seq is bounded_above implies (( superior_realsequence seq) . (n + 1)) <= (( superior_realsequence seq) . n)

    proof

      

       A1: (( superior_realsequence seq) . (n + 1)) <= ( max ((( superior_realsequence seq) . (n + 1)),(seq . n))) by XXREAL_0: 25;

      assume seq is bounded_above;

      hence thesis by A1, Th47;

    end;

    theorem :: RINFSUP1:50

    

     Th50: seq is bounded_below implies ( inferior_realsequence seq) is non-decreasing by Th48;

    theorem :: RINFSUP1:51

    

     Th51: seq is bounded_above implies ( superior_realsequence seq) is non-increasing by Th49;

    theorem :: RINFSUP1:52

    seq is bounded implies (( inferior_realsequence seq) . n) <= (( superior_realsequence seq) . n)

    proof

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      assume

       A1: seq is bounded;

      

       A2: Y1 <> {} by SETLIM_1: 1;

      (( superior_realsequence seq) . n) = ( upper_bound Y1) & (( inferior_realsequence seq) . n) = ( lower_bound Y1) by Def4, Def5;

      hence thesis by A1, A2, Th33, SEQ_4: 11;

    end;

    theorem :: RINFSUP1:53

    

     Th53: seq is bounded implies (( inferior_realsequence seq) . n) <= ( lower_bound ( superior_realsequence seq))

    proof

      reconsider Y2 = { (seq . k2) : n <= k2 } as Subset of REAL by Th29;

      assume

       A1: seq is bounded;

       A2:

      now

        let m;

        reconsider Y1 = { (seq . k1) : m <= k1 } as Subset of REAL by Th29;

        n <= (n + m) by NAT_1: 11;

        then

         A3: (seq . (n + m)) in Y2;

        Y2 is real-bounded by A1, Th33;

        then Y2 is bounded_below;

        then

         A4: ( lower_bound Y2) <= (seq . (n + m)) by A3, SEQ_4:def 2;

        m <= (n + m) by NAT_1: 11;

        then

         A5: (seq . (n + m)) in Y1;

        Y1 is real-bounded by A1, Th33;

        then Y1 is bounded_above;

        then

         A6: (seq . (n + m)) <= ( upper_bound Y1) by A5, SEQ_4:def 1;

        (( superior_realsequence seq) . m) = ( upper_bound Y1) by Def5;

        hence ( lower_bound Y2) <= (( superior_realsequence seq) . m) by A6, A4, XXREAL_0: 2;

      end;

      (( inferior_realsequence seq) . n) = ( lower_bound Y2) by Def4;

      hence thesis by A2, Th10;

    end;

    theorem :: RINFSUP1:54

    

     Th54: seq is bounded implies ( upper_bound ( inferior_realsequence seq)) <= (( superior_realsequence seq) . n)

    proof

      reconsider Y2 = { (seq . k2) : n <= k2 } as Subset of REAL by Th29;

      assume

       A1: seq is bounded;

       A2:

      now

        let m;

        reconsider Y1 = { (seq . k1) : m <= k1 } as Subset of REAL by Th29;

        n <= (n + m) by NAT_1: 11;

        then

         A3: (seq . (n + m)) in Y2;

        Y2 is real-bounded by A1, Th33;

        then Y2 is bounded_above;

        then

         A4: ( upper_bound Y2) >= (seq . (n + m)) by A3, SEQ_4:def 1;

        m <= (n + m) by NAT_1: 11;

        then

         A5: (seq . (n + m)) in Y1;

        Y1 is real-bounded by A1, Th33;

        then Y1 is bounded_below;

        then

         A6: (seq . (n + m)) >= ( lower_bound Y1) by A5, SEQ_4:def 2;

        (( inferior_realsequence seq) . m) = ( lower_bound Y1) by Def4;

        hence ( upper_bound Y2) >= (( inferior_realsequence seq) . m) by A6, A4, XXREAL_0: 2;

      end;

      (( superior_realsequence seq) . n) = ( upper_bound Y2) by Def5;

      hence thesis by A2, Th9;

    end;

    theorem :: RINFSUP1:55

    

     Th55: seq is bounded implies ( upper_bound ( inferior_realsequence seq)) <= ( lower_bound ( superior_realsequence seq))

    proof

      set seq1 = ( inferior_realsequence seq);

      set r = ( lower_bound ( superior_realsequence seq));

      assume seq is bounded;

      then (seq1 . n) <= r by Th53;

      hence thesis by Th9;

    end;

    theorem :: RINFSUP1:56

    

     Th56: seq is bounded implies ( superior_realsequence seq) is bounded & ( inferior_realsequence seq) is bounded

    proof

      assume

       A1: seq is bounded;

      then ( inferior_realsequence seq) is non-decreasing by Th50;

      then

       A2: ( inferior_realsequence seq) is bounded_below by LIMFUNC1: 1;

      now

        let m;

        ( upper_bound ( inferior_realsequence seq)) <= (( superior_realsequence seq) . m) by A1, Th54;

        hence (( upper_bound ( inferior_realsequence seq)) - 1) < (( superior_realsequence seq) . m) by Lm1;

      end;

      then

       A3: ( superior_realsequence seq) is bounded_below by SEQ_2:def 4;

      now

        let m;

        (( inferior_realsequence seq) . m) <= ( lower_bound ( superior_realsequence seq)) by A1, Th53;

        hence (( inferior_realsequence seq) . m) < (( lower_bound ( superior_realsequence seq)) + 1) by Lm1;

      end;

      then

       A4: ( inferior_realsequence seq) is bounded_above by SEQ_2:def 3;

      ( superior_realsequence seq) is non-increasing by A1, Th51;

      then ( superior_realsequence seq) is bounded_above by LIMFUNC1: 1;

      hence thesis by A2, A4, A3;

    end;

    theorem :: RINFSUP1:57

    

     Th57: seq is bounded implies ( inferior_realsequence seq) is convergent & ( lim ( inferior_realsequence seq)) = ( upper_bound ( inferior_realsequence seq))

    proof

      assume seq is bounded;

      then ( inferior_realsequence seq) is non-decreasing & ( inferior_realsequence seq) is bounded by Th50, Th56;

      hence thesis by Th24;

    end;

    theorem :: RINFSUP1:58

    

     Th58: seq is bounded implies ( superior_realsequence seq) is convergent & ( lim ( superior_realsequence seq)) = ( lower_bound ( superior_realsequence seq))

    proof

      assume seq is bounded;

      then ( superior_realsequence seq) is non-increasing & ( superior_realsequence seq) is bounded by Th51, Th56;

      hence thesis by Th25;

    end;

    theorem :: RINFSUP1:59

    

     Th59: seq is bounded_below implies (( inferior_realsequence seq) . n) = ( - (( superior_realsequence ( - seq)) . n))

    proof

      assume

       A1: seq is bounded_below;

      (( inferior_realsequence seq) . n) = ( lower_bound (seq ^\ n)) by Th36

      .= ( - ( upper_bound ( - (seq ^\ n)))) by A1, Th14, SEQM_3: 28

      .= ( - ( upper_bound (( - seq) ^\ n))) by SEQM_3: 16;

      hence thesis by Th37;

    end;

    theorem :: RINFSUP1:60

    

     Th60: seq is bounded_above implies (( superior_realsequence seq) . n) = ( - (( inferior_realsequence ( - seq)) . n))

    proof

      assume

       A1: seq is bounded_above;

      (( superior_realsequence seq) . n) = ( upper_bound (seq ^\ n)) by Th37

      .= ( - ( lower_bound ( - (seq ^\ n)))) by A1, Th13, SEQM_3: 27

      .= ( - ( lower_bound (( - seq) ^\ n))) by SEQM_3: 16;

      hence thesis by Th36;

    end;

    theorem :: RINFSUP1:61

    

     Th61: seq is bounded_below implies ( inferior_realsequence seq) = ( - ( superior_realsequence ( - seq)))

    proof

      assume seq is bounded_below;

      then (( inferior_realsequence seq) . n) = ( - (( superior_realsequence ( - seq)) . n)) by Th59;

      hence thesis by SEQ_1: 10;

    end;

    theorem :: RINFSUP1:62

    

     Th62: seq is bounded_above implies ( superior_realsequence seq) = ( - ( inferior_realsequence ( - seq)))

    proof

      assume seq is bounded_above;

      then (( superior_realsequence seq) . n) = ( - (( inferior_realsequence ( - seq)) . n)) by Th60;

      hence thesis by SEQ_1: 10;

    end;

    theorem :: RINFSUP1:63

    seq is non-decreasing implies (seq . n) <= (( inferior_realsequence seq) . (n + 1))

    proof

      reconsider Y1 = { (seq . k) : (n + 1) <= k } as Subset of REAL by Th29;

      

       A1: (( inferior_realsequence seq) . (n + 1)) = ( lower_bound Y1) by Def4;

      assume

       A2: seq is non-decreasing;

      then ( lower_bound Y1) = (seq . (n + 1)) by Th34;

      hence thesis by A2, A1;

    end;

    

     Lm2: seq is non-decreasing implies (( inferior_realsequence seq) . n) = (seq . n)

    proof

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      assume

       A1: seq is non-decreasing;

      (( inferior_realsequence seq) . n) = ( lower_bound Y1) by Def4;

      hence thesis by A1, Th34;

    end;

    theorem :: RINFSUP1:64

    seq is non-decreasing implies ( inferior_realsequence seq) = seq

    proof

      assume seq is non-decreasing;

      then for n be Element of NAT holds (( inferior_realsequence seq) . n) = (seq . n) by Lm2;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RINFSUP1:65

    

     Th65: seq is non-decreasing bounded_above implies (seq . n) <= (( superior_realsequence seq) . (n + 1))

    proof

      reconsider Y1 = { (seq . k) : (n + 1) <= k } as Subset of REAL by Th29;

      

       A1: (seq . (n + 1)) in Y1;

      assume

       A2: seq is non-decreasing bounded_above;

      then Y1 is bounded_above by Th31;

      then

       A3: (seq . (n + 1)) <= ( upper_bound Y1) by A1, SEQ_4:def 1;

      

       A4: (( superior_realsequence seq) . (n + 1)) = ( upper_bound Y1) by Def5;

      (seq . n) <= (seq . (n + 1)) by A2;

      hence thesis by A4, A3, XXREAL_0: 2;

    end;

    theorem :: RINFSUP1:66

    

     Th66: seq is non-decreasing bounded_above implies (( superior_realsequence seq) . n) = (( superior_realsequence seq) . (n + 1))

    proof

      assume

       A1: seq is non-decreasing bounded_above;

      then (seq . n) <= (( superior_realsequence seq) . (n + 1)) by Th65;

      then ( max ((( superior_realsequence seq) . (n + 1)),(seq . n))) = (( superior_realsequence seq) . (n + 1)) by XXREAL_0:def 10;

      hence thesis by A1, Th47;

    end;

    theorem :: RINFSUP1:67

    

     Th67: seq is non-decreasing bounded_above implies (( superior_realsequence seq) . n) = ( upper_bound seq) & ( superior_realsequence seq) is constant

    proof

      reconsider ubs = ( upper_bound seq) as Element of REAL by XREAL_0:def 1;

      defpred P[ Nat] means (( superior_realsequence seq) . $1) = ubs;

      assume

       A1: seq is non-decreasing bounded_above;

      

       A2: for k be Nat st P[k] holds P[(k + 1)] by A1, Th66;

      

       A3: P[ 0 ] by A1, Th39;

      for k be Nat holds P[k] from NAT_1:sch 2( A3, A2);

      hence thesis by VALUED_0:def 18;

    end;

    theorem :: RINFSUP1:68

    seq is non-decreasing bounded_above implies ( lower_bound ( superior_realsequence seq)) = ( upper_bound seq)

    proof

      assume

       A1: seq is non-decreasing bounded_above;

      then ( superior_realsequence seq) is constant by Th67;

      then

      consider r1 be Element of REAL such that

       A2: ( rng ( superior_realsequence seq)) = {r1} by FUNCT_2: 111;

      r1 in ( rng ( superior_realsequence seq)) by A2, TARSKI:def 1;

      then ex n be Element of NAT st r1 = (( superior_realsequence seq) . n) by FUNCT_2: 113;

      then ( rng ( superior_realsequence seq)) = {( upper_bound seq)} by A1, A2, Th67;

      hence thesis by SEQ_4: 9;

    end;

    theorem :: RINFSUP1:69

    seq is non-increasing implies (( superior_realsequence seq) . (n + 1)) <= (seq . n)

    proof

      reconsider Y1 = { (seq . k) : (n + 1) <= k } as Subset of REAL by Th29;

      

       A1: (( superior_realsequence seq) . (n + 1)) = ( upper_bound Y1) by Def5;

      assume

       A2: seq is non-increasing;

      then ( upper_bound Y1) = (seq . (n + 1)) by Th35;

      hence thesis by A2, A1;

    end;

    

     Lm3: seq is non-increasing implies (( superior_realsequence seq) . n) = (seq . n)

    proof

      reconsider Y1 = { (seq . k) : n <= k } as Subset of REAL by Th29;

      assume

       A1: seq is non-increasing;

      (( superior_realsequence seq) . n) = ( upper_bound Y1) by Def5;

      hence thesis by A1, Th35;

    end;

    theorem :: RINFSUP1:70

    seq is non-increasing implies ( superior_realsequence seq) = seq

    proof

      assume seq is non-increasing;

      then for n be Element of NAT holds (( superior_realsequence seq) . n) = (seq . n) by Lm3;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RINFSUP1:71

    

     Th71: seq is non-increasing bounded_below implies (( inferior_realsequence seq) . (n + 1)) <= (seq . n)

    proof

      reconsider Y1 = { (seq . k) : (n + 1) <= k } as Subset of REAL by Th29;

      

       A1: (seq . (n + 1)) in Y1;

      assume

       A2: seq is non-increasing bounded_below;

      then Y1 is bounded_below by Th32;

      then

       A3: ( lower_bound Y1) <= (seq . (n + 1)) by A1, SEQ_4:def 2;

      

       A4: (( inferior_realsequence seq) . (n + 1)) = ( lower_bound Y1) by Def4;

      (seq . (n + 1)) <= (seq . n) by A2;

      hence thesis by A4, A3, XXREAL_0: 2;

    end;

    theorem :: RINFSUP1:72

    

     Th72: seq is non-increasing bounded_below implies (( inferior_realsequence seq) . n) = (( inferior_realsequence seq) . (n + 1))

    proof

      assume

       A1: seq is non-increasing bounded_below;

      then (( inferior_realsequence seq) . (n + 1)) <= (seq . n) by Th71;

      then ( min ((( inferior_realsequence seq) . (n + 1)),(seq . n))) = (( inferior_realsequence seq) . (n + 1)) by XXREAL_0:def 9;

      hence thesis by A1, Th46;

    end;

    theorem :: RINFSUP1:73

    

     Th73: seq is non-increasing & seq is bounded_below implies (( inferior_realsequence seq) . n) = ( lower_bound seq) & ( inferior_realsequence seq) is constant

    proof

      assume that

       A1: seq is non-increasing and

       A2: seq is bounded_below;

      reconsider lbs = ( lower_bound seq) as Element of REAL by XREAL_0:def 1;

      defpred P[ Nat] means (( inferior_realsequence seq) . $1) = lbs;

      

       A3: for k be Nat st P[k] holds P[(k + 1)] by A1, A2, Th72;

      

       A4: P[ 0 ] by A2, Th38;

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A3);

      hence thesis by VALUED_0:def 18;

    end;

    theorem :: RINFSUP1:74

    seq is non-increasing bounded_below implies ( upper_bound ( inferior_realsequence seq)) = ( lower_bound seq)

    proof

      assume

       A1: seq is non-increasing bounded_below;

      then ( inferior_realsequence seq) is constant by Th73;

      then

      consider r1 be Element of REAL such that

       A2: ( rng ( inferior_realsequence seq)) = {r1} by FUNCT_2: 111;

      r1 in ( rng ( inferior_realsequence seq)) by A2, TARSKI:def 1;

      then ex n be Element of NAT st r1 = (( inferior_realsequence seq) . n) by FUNCT_2: 113;

      

      then ( upper_bound ( inferior_realsequence seq)) = ( upper_bound {( lower_bound seq)}) by A1, A2, Th73

      .= ( lower_bound seq) by SEQ_4: 9;

      hence thesis;

    end;

    theorem :: RINFSUP1:75

    

     Th75: seq1 is bounded & seq2 is bounded & (for n holds (seq1 . n) <= (seq2 . n)) implies (for n holds (( superior_realsequence seq1) . n) <= (( superior_realsequence seq2) . n)) & for n holds (( inferior_realsequence seq1) . n) <= (( inferior_realsequence seq2) . n)

    proof

      assume that

       A1: seq1 is bounded and

       A2: seq2 is bounded and

       A3: for n holds (seq1 . n) <= (seq2 . n);

      now

        let n;

        reconsider Y2 = { (seq2 . k2) : n <= k2 } as Subset of REAL by Th29;

        reconsider Y1 = { (seq1 . k1) : n <= k1 } as Subset of REAL by Th29;

        

         A4: Y1 <> {} & Y2 <> {} by SETLIM_1: 1;

        

         A5: (( inferior_realsequence seq1) . n) = ( lower_bound Y1) & (( inferior_realsequence seq2) . n) = ( lower_bound Y2) by Def4;

        Y1 is real-bounded by A1, Th33;

        then

         A6: Y1 is bounded_below;

        now

          let r;

          assume r in Y2;

          then

          consider k such that

           A7: r = (seq2 . k) and

           A8: n <= k;

          (seq1 . k) in Y1 by A8;

          then

           A9: ( lower_bound Y1) <= (seq1 . k) by A6, SEQ_4:def 2;

          (seq1 . k) <= r by A3, A7;

          hence ( lower_bound Y1) <= r by A9, XXREAL_0: 2;

        end;

        then

         A10: for r be Real st r in Y2 holds ( lower_bound Y1) <= r;

        Y2 is real-bounded by A2, Th33;

        then

         A11: Y2 is bounded_above;

         A12:

        now

          let r be Real;

          assume r in Y1;

          then

          consider k such that

           A13: r = (seq1 . k) and

           A14: n <= k;

          (seq2 . k) in Y2 by A14;

          then

           A15: (seq2 . k) <= ( upper_bound Y2) by A11, SEQ_4:def 1;

          r <= (seq2 . k) by A3, A13;

          hence r <= ( upper_bound Y2) by A15, XXREAL_0: 2;

        end;

        (( superior_realsequence seq1) . n) = ( upper_bound Y1) & (( superior_realsequence seq2) . n) = ( upper_bound Y2) by Def5;

        hence (( superior_realsequence seq1) . n) <= (( superior_realsequence seq2) . n) & (( inferior_realsequence seq1) . n) <= (( inferior_realsequence seq2) . n) by A5, A4, A12, A10, SEQ_4: 113, SEQ_4: 144;

      end;

      hence thesis;

    end;

    theorem :: RINFSUP1:76

    seq1 is bounded_below & seq2 is bounded_below implies (( inferior_realsequence (seq1 + seq2)) . n) >= ((( inferior_realsequence seq1) . n) + (( inferior_realsequence seq2) . n))

    proof

      assume seq1 is bounded_below & seq2 is bounded_below;

      then (seq1 ^\ n) is bounded_below & (seq2 ^\ n) is bounded_below by SEQM_3: 28;

      then ( lower_bound ((seq1 ^\ n) + (seq2 ^\ n))) >= (( lower_bound (seq1 ^\ n)) + ( lower_bound (seq2 ^\ n))) by Th15;

      then

       A1: ( lower_bound ((seq1 + seq2) ^\ n)) >= (( lower_bound (seq1 ^\ n)) + ( lower_bound (seq2 ^\ n))) by SEQM_3: 15;

      (( inferior_realsequence seq1) . n) = ( lower_bound (seq1 ^\ n)) & (( inferior_realsequence seq2) . n) = ( lower_bound (seq2 ^\ n)) by Th36;

      hence thesis by A1, Th36;

    end;

    theorem :: RINFSUP1:77

    seq1 is bounded_above & seq2 is bounded_above implies (( superior_realsequence (seq1 + seq2)) . n) <= ((( superior_realsequence seq1) . n) + (( superior_realsequence seq2) . n))

    proof

      assume seq1 is bounded_above & seq2 is bounded_above;

      then (seq1 ^\ n) is bounded_above & (seq2 ^\ n) is bounded_above by SEQM_3: 27;

      then ( upper_bound ((seq1 ^\ n) + (seq2 ^\ n))) <= (( upper_bound (seq1 ^\ n)) + ( upper_bound (seq2 ^\ n))) by Th16;

      then

       A1: ( upper_bound ((seq1 + seq2) ^\ n)) <= (( upper_bound (seq1 ^\ n)) + ( upper_bound (seq2 ^\ n))) by SEQM_3: 15;

      (( superior_realsequence seq1) . n) = ( upper_bound (seq1 ^\ n)) & (( superior_realsequence seq2) . n) = ( upper_bound (seq2 ^\ n)) by Th37;

      hence thesis by A1, Th37;

    end;

    theorem :: RINFSUP1:78

    seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative implies (( inferior_realsequence (seq1 (#) seq2)) . n) >= ((( inferior_realsequence seq1) . n) * (( inferior_realsequence seq2) . n))

    proof

      assume seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative;

      then (seq1 ^\ n) is bounded_below nonnegative & (seq2 ^\ n) is bounded_below nonnegative by Th17, SEQM_3: 28;

      then ( lower_bound ((seq1 ^\ n) (#) (seq2 ^\ n))) >= (( lower_bound (seq1 ^\ n)) * ( lower_bound (seq2 ^\ n))) by Th20;

      then

       A1: ( lower_bound ((seq1 (#) seq2) ^\ n)) >= (( lower_bound (seq1 ^\ n)) * ( lower_bound (seq2 ^\ n))) by SEQM_3: 19;

      (( inferior_realsequence seq1) . n) = ( lower_bound (seq1 ^\ n)) & (( inferior_realsequence seq2) . n) = ( lower_bound (seq2 ^\ n)) by Th36;

      hence thesis by A1, Th36;

    end;

    theorem :: RINFSUP1:79

    

     Th79: seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative implies (( inferior_realsequence (seq1 (#) seq2)) . n) >= ((( inferior_realsequence seq1) . n) * (( inferior_realsequence seq2) . n))

    proof

      assume seq1 is bounded_below nonnegative & seq2 is bounded_below nonnegative;

      then (seq1 ^\ n) is bounded_below nonnegative & (seq2 ^\ n) is bounded_below nonnegative by Th17, SEQM_3: 28;

      then ( lower_bound ((seq1 ^\ n) (#) (seq2 ^\ n))) >= (( lower_bound (seq1 ^\ n)) * ( lower_bound (seq2 ^\ n))) by Th20;

      then

       A1: ( lower_bound ((seq1 (#) seq2) ^\ n)) >= (( lower_bound (seq1 ^\ n)) * ( lower_bound (seq2 ^\ n))) by SEQM_3: 19;

      (( inferior_realsequence seq1) . n) = ( lower_bound (seq1 ^\ n)) & (( inferior_realsequence seq2) . n) = ( lower_bound (seq2 ^\ n)) by Th36;

      hence thesis by A1, Th36;

    end;

    theorem :: RINFSUP1:80

    

     Th80: seq1 is bounded_above nonnegative & seq2 is bounded_above nonnegative implies (( superior_realsequence (seq1 (#) seq2)) . n) <= ((( superior_realsequence seq1) . n) * (( superior_realsequence seq2) . n))

    proof

      assume seq1 is bounded_above nonnegative & seq2 is bounded_above nonnegative;

      then (seq1 ^\ n) is bounded_above nonnegative & (seq2 ^\ n) is bounded_above nonnegative by Th17, SEQM_3: 27;

      then ( upper_bound ((seq1 ^\ n) (#) (seq2 ^\ n))) <= (( upper_bound (seq1 ^\ n)) * ( upper_bound (seq2 ^\ n))) by Th21;

      then

       A1: ( upper_bound ((seq1 (#) seq2) ^\ n)) <= (( upper_bound (seq1 ^\ n)) * ( upper_bound (seq2 ^\ n))) by SEQM_3: 19;

      (( superior_realsequence seq1) . n) = ( upper_bound (seq1 ^\ n)) & (( superior_realsequence seq2) . n) = ( upper_bound (seq2 ^\ n)) by Th37;

      hence thesis by A1, Th37;

    end;

    definition

      let seq be Real_Sequence;

      :: RINFSUP1:def6

      func lim_sup seq -> Real equals ( lower_bound ( superior_realsequence seq));

      coherence ;

    end

    definition

      let seq be Real_Sequence;

      :: RINFSUP1:def7

      func lim_inf seq -> Real equals ( upper_bound ( inferior_realsequence seq));

      coherence ;

    end

    theorem :: RINFSUP1:81

    

     Th81: seq is bounded implies (( lim_inf seq) <= r iff for s st 0 < s holds for n holds ex k st (seq . (n + k)) < (r + s))

    proof

      set seq1 = ( inferior_realsequence seq);

      assume

       A1: seq is bounded;

      then

       A2: seq1 is bounded by Th56;

      thus ( lim_inf seq) <= r implies for s st 0 < s holds for n holds ex k st (seq . (n + k)) < (r + s)

      proof

        assume

         A3: ( lim_inf seq) <= r;

        let s such that

         A4: 0 < s;

        for n holds ex k st (seq . (n + k)) < (r + s)

        proof

          let n;

          consider k such that

           A5: (seq . (n + k)) < ((seq1 . n) + s) by A1, A4, Th40;

          (seq1 . n) <= r by A2, A3, Th9;

          then ((seq . (n + k)) + (seq1 . n)) < (r + ((seq1 . n) + s)) by A5, XREAL_1: 8;

          then (seq . (n + k)) < ((r + ((seq1 . n) + s)) - (seq1 . n)) by XREAL_1: 20;

          hence thesis;

        end;

        hence thesis;

      end;

      assume

       A6: for s st 0 < s holds for n holds ex k st (seq . (n + k)) < (r + s);

      for s st 0 < s holds ( lim_inf seq) <= (r + s)

      proof

        let s such that

         A7: 0 < s;

        for n holds (seq1 . n) <= (r + s)

        proof

          let n;

          consider k such that

           A8: (seq . (n + k)) < (r + s) by A6, A7;

          (seq1 . n) <= (seq . (n + k)) by A1, Th40;

          hence thesis by A8, XXREAL_0: 2;

        end;

        hence thesis by Th9;

      end;

      hence thesis by XREAL_1: 41;

    end;

    theorem :: RINFSUP1:82

    

     Th82: seq is bounded implies (r <= ( lim_inf seq) iff for s st 0 < s holds ex n st for k holds (r - s) < (seq . (n + k)))

    proof

      set seq1 = ( inferior_realsequence seq);

      assume

       A1: seq is bounded;

      then

       A2: seq1 is bounded by Th56;

      thus r <= ( lim_inf seq) implies for s st 0 < s holds ex n st for k holds (r - s) < (seq . (n + k))

      proof

        assume

         A3: r <= ( lim_inf seq);

        let s such that

         A4: 0 < s;

        ex n st for k holds (r - s) < (seq . (n + k))

        proof

          consider n1 be Nat such that

           A5: (seq1 . n1) > (( upper_bound seq1) - s) by A2, A4, Th7;

          ((seq1 . n1) + ( upper_bound seq1)) > (r + (( upper_bound seq1) - s)) by A3, A5, XREAL_1: 8;

          then ((seq1 . n1) + ( upper_bound seq1)) > ((r - s) + ( upper_bound seq1));

          then

           A6: (((seq1 . n1) + ( upper_bound seq1)) - ( upper_bound seq1)) > (r - s) by XREAL_1: 20;

          now

            let k;

            (seq1 . n1) <= (seq . (n1 + k)) by A1, Th40;

            then ((r - s) + (seq1 . n1)) < ((seq . (n1 + k)) + (seq1 . n1)) by A6, XREAL_1: 8;

            then (((r - s) + (seq1 . n1)) - (seq1 . n1)) < (seq . (n1 + k)) by XREAL_1: 19;

            hence (r - s) < (seq . (n1 + k));

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      assume

       A7: for s st 0 < s holds ex n st for k holds (r - s) < (seq . (n + k));

      for s st 0 < s holds (r - s) <= ( lim_inf seq)

      proof

        let s;

        assume 0 < s;

        then

        consider n1 be Nat such that

         A8: for k holds (r - s) < (seq . (n1 + k)) by A7;

        for k holds (r - s) <= (seq . (n1 + k)) by A8;

        then

         A9: (r - s) <= (seq1 . n1) by A1, Th42;

        (seq1 . n1) <= ( upper_bound seq1) by A2, Th7;

        hence thesis by A9, XXREAL_0: 2;

      end;

      hence thesis by XREAL_1: 57;

    end;

    theorem :: RINFSUP1:83

    seq is bounded implies (r = ( lim_inf seq) iff for s st 0 < s holds (for n holds ex k st (seq . (n + k)) < (r + s)) & ex n st for k holds (r - s) < (seq . (n + k)))

    proof

      assume

       A1: seq is bounded;

      hence r = ( lim_inf seq) implies for s st 0 < s holds (for n holds ex k st (seq . (n + k)) < (r + s)) & ex n st for k holds (r - s) < (seq . (n + k)) by Th81, Th82;

      assume

       A2: for s st 0 < s holds (for n holds ex k st (seq . (n + k)) < (r + s)) & ex n st for k holds (r - s) < (seq . (n + k));

      then for s st 0 < s holds ex n st for k holds (r - s) < (seq . (n + k));

      then

       A3: r <= ( lim_inf seq) by A1, Th82;

      for s st 0 < s holds for n holds ex k st (seq . (n + k)) < (r + s) by A2;

      then ( lim_inf seq) <= r by A1, Th81;

      hence thesis by A3, XXREAL_0: 1;

    end;

    theorem :: RINFSUP1:84

    

     Th84: seq is bounded implies (r <= ( lim_sup seq) iff for s st 0 < s holds for n holds ex k st (seq . (n + k)) > (r - s))

    proof

      set seq1 = ( superior_realsequence seq);

      assume

       A1: seq is bounded;

      then

       A2: seq1 is bounded by Th56;

      thus r <= ( lim_sup seq) implies for s st 0 < s holds for n holds ex k st (seq . (n + k)) > (r - s)

      proof

        assume

         A3: r <= ( lim_sup seq);

        let s such that

         A4: 0 < s;

        for n holds ex k st (seq . (n + k)) > (r - s)

        proof

          let n;

          consider k such that

           A5: (seq . (n + k)) > ((seq1 . n) - s) by A1, A4, Th41;

          (seq1 . n) >= r by A2, A3, Th10;

          then ((seq1 . n) + (seq . (n + k))) > (r + ((seq1 . n) - s)) by A5, XREAL_1: 8;

          then (seq . (n + k)) > (((r + (seq1 . n)) - s) - (seq1 . n)) by XREAL_1: 19;

          hence thesis;

        end;

        hence thesis;

      end;

      assume

       A6: for s st 0 < s holds for n holds ex k st (seq . (n + k)) > (r - s);

      for s st 0 < s holds ( lim_sup seq) >= (r - s)

      proof

        let s such that

         A7: 0 < s;

        for n holds (r - s) <= (seq1 . n)

        proof

          let n;

          consider k such that

           A8: (r - s) < (seq . (n + k)) by A6, A7;

          (seq . (n + k)) <= (seq1 . n) by A1, Th41;

          hence thesis by A8, XXREAL_0: 2;

        end;

        hence thesis by Th10;

      end;

      hence thesis by XREAL_1: 57;

    end;

    theorem :: RINFSUP1:85

    

     Th85: seq is bounded implies (( lim_sup seq) <= r iff for s st 0 < s holds ex n st for k holds (seq . (n + k)) < (r + s))

    proof

      set seq1 = ( superior_realsequence seq);

      assume

       A1: seq is bounded;

      then

       A2: seq1 is bounded by Th56;

      thus ( lim_sup seq) <= r implies for s st 0 < s holds ex n st for k holds (seq . (n + k)) < (r + s)

      proof

        assume

         A3: ( lim_sup seq) <= r;

        for s st 0 < s holds ex n st for k holds (seq . (n + k)) < (r + s)

        proof

          let s such that

           A4: 0 < s;

          ex n st for k holds (seq . (n + k)) < (r + s)

          proof

            consider n1 be Nat such that

             A5: (seq1 . n1) < (( lower_bound seq1) + s) by A2, A4, Th8;

            ((seq1 . n1) + ( lower_bound seq1)) < (r + (( lower_bound seq1) + s)) by A3, A5, XREAL_1: 8;

            then ((seq1 . n1) + ( lower_bound seq1)) < ((r + s) + ( lower_bound seq1));

            then

             A6: (((seq1 . n1) + ( lower_bound seq1)) - ( lower_bound seq1)) < (r + s) by XREAL_1: 19;

            now

              let k;

              (seq . (n1 + k)) <= (seq1 . n1) by A1, Th41;

              then ((seq . (n1 + k)) + (seq1 . n1)) < ((r + s) + (seq1 . n1)) by A6, XREAL_1: 8;

              then (((seq . (n1 + k)) + (seq1 . n1)) - (seq1 . n1)) < (r + s) by XREAL_1: 19;

              hence (seq . (n1 + k)) < (r + s);

            end;

            hence thesis;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

      assume

       A7: for s st 0 < s holds ex n st for k holds (seq . (n + k)) < (r + s);

      for s st 0 < s holds ( lim_sup seq) <= (r + s)

      proof

        let s;

        assume 0 < s;

        then

        consider n1 be Nat such that

         A8: for k holds (seq . (n1 + k)) < (r + s) by A7;

        for k holds (seq . (n1 + k)) <= (r + s) by A8;

        then

         A9: (seq1 . n1) <= (r + s) by A1, Th44;

        ( lower_bound seq1) <= (seq1 . n1) by A2, Th8;

        hence thesis by A9, XXREAL_0: 2;

      end;

      hence thesis by XREAL_1: 41;

    end;

    theorem :: RINFSUP1:86

    seq is bounded implies (r = ( lim_sup seq) iff for s st 0 < s holds (for n holds ex k st (seq . (n + k)) > (r - s)) & ex n st for k holds (seq . (n + k)) < (r + s))

    proof

      assume

       A1: seq is bounded;

      hence r = ( lim_sup seq) implies for s st 0 < s holds (for n holds ex k st (seq . (n + k)) > (r - s)) & ex n st for k holds (seq . (n + k)) < (r + s) by Th84, Th85;

      assume

       A2: for s st 0 < s holds (for n holds ex k st (seq . (n + k)) > (r - s)) & ex n st for k holds (seq . (n + k)) < (r + s);

      then for s st 0 < s holds ex n st for k holds (seq . (n + k)) < (r + s);

      then

       A3: ( lim_sup seq) <= r by A1, Th85;

      for s st 0 < s holds for n holds ex k st (seq . (n + k)) > (r - s) by A2;

      then r <= ( lim_sup seq) by A1, Th84;

      hence thesis by A3, XXREAL_0: 1;

    end;

    theorem :: RINFSUP1:87

    seq is bounded implies ( lim_inf seq) <= ( lim_sup seq) by Th55;

    theorem :: RINFSUP1:88

    

     Th88: seq is bounded & ( lim_sup seq) = ( lim_inf seq) iff seq is convergent

    proof

      thus seq is bounded & ( lim_sup seq) = ( lim_inf seq) implies seq is convergent

      proof

        reconsider r = ( lower_bound ( superior_realsequence seq)) as Real;

        assume that

         A1: seq is bounded and

         A2: ( lim_sup seq) = ( lim_inf seq);

        

         A3: ( inferior_realsequence seq) is bounded by A1, Th56;

        

         A4: ( inferior_realsequence seq) is non-decreasing by A1, Th50;

        

         A5: ( superior_realsequence seq) is non-increasing by A1, Th51;

        

         A6: ( superior_realsequence seq) is bounded by A1, Th56;

        for s st 0 < s holds ex n st for m st n <= m holds |.((seq . m) - r).| < s

        proof

          let s such that

           A7: 0 < s;

          consider k2 be Nat such that

           A8: (( superior_realsequence seq) . k2) < (r + s) by A6, A7, Th8;

          consider k1 be Nat such that

           A9: (r - s) < (( inferior_realsequence seq) . k1) by A2, A3, A7, Th7;

          reconsider k = ( max (k1,k2)) as Nat by TARSKI: 1;

          k2 <= k by XXREAL_0: 25;

          then

           A10: (( superior_realsequence seq) . k) <= (( superior_realsequence seq) . k2) by A5, SEQM_3: 8;

          k1 <= k by XXREAL_0: 25;

          then

           A11: (( inferior_realsequence seq) . k1) <= (( inferior_realsequence seq) . k) by A4, SEQM_3: 6;

          ex n st for m st n <= m holds |.((seq . m) - r).| < s

          proof

            take k;

            let m;

            assume k <= m;

            then

            consider k3 be Nat such that

             A12: m = (k + k3) by NAT_1: 10;

            (seq . m) <= (( superior_realsequence seq) . k) by A1, A12, Th41;

            then (seq . m) <= (( superior_realsequence seq) . k2) by A10, XXREAL_0: 2;

            then

             A13: (seq . m) < (r + s) by A8, XXREAL_0: 2;

            (( inferior_realsequence seq) . k) <= (seq . m) by A1, A12, Th40;

            then (( inferior_realsequence seq) . k1) <= (seq . m) by A11, XXREAL_0: 2;

            then (r - s) < (seq . m) by A9, XXREAL_0: 2;

            hence thesis by A13, Th1;

          end;

          hence thesis;

        end;

        hence thesis by SEQ_2:def 6;

      end;

      assume

       A14: seq is convergent;

      then

      consider r such that

       A15: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - r).| < p by SEQ_2:def 6;

      

       A16: seq is bounded by A14;

      

       A17: for p st 0 < p holds ex n st (r - p) <= (( inferior_realsequence seq) . n) & (( superior_realsequence seq) . n) <= (r + p)

      proof

        let p;

        assume 0 < p;

        then

        consider n such that

         A18: for m st n <= m holds |.((seq . m) - r).| < p by A15;

        

         A19: for m st n <= m holds (r - p) <= (seq . m) & (seq . m) <= (r + p)

        proof

          let m;

          assume n <= m;

          then |.((seq . m) - r).| < p by A18;

          hence thesis by Th1;

        end;

        then for m st n <= m holds (seq . m) <= (r + p);

        then

         A20: (( superior_realsequence seq) . n) <= (r + p) by A16, Th45;

        for m st n <= m holds (r - p) <= (seq . m) by A19;

        then (r - p) <= (( inferior_realsequence seq) . n) by A16, Th43;

        hence thesis by A20;

      end;

      

       A21: ( superior_realsequence seq) is bounded & ( inferior_realsequence seq) is bounded by A16, Th56;

      

       A22: for p holds 0 < p implies (r - p) <= ( upper_bound ( inferior_realsequence seq)) & ( lower_bound ( superior_realsequence seq)) <= (r + p)

      proof

        let p;

        assume 0 < p;

        then

        consider n such that

         A23: (r - p) <= (( inferior_realsequence seq) . n) & (( superior_realsequence seq) . n) <= (r + p) by A17;

        (( inferior_realsequence seq) . n) <= ( upper_bound ( inferior_realsequence seq)) & ( lower_bound ( superior_realsequence seq)) <= (( superior_realsequence seq) . n) by A21, Th7, Th8;

        hence thesis by A23, XXREAL_0: 2;

      end;

      reconsider r as Real;

      

       A24: for p holds 0 < p implies ( lower_bound ( superior_realsequence seq)) <= (r + p) by A22;

      then

       A25: ( lower_bound ( superior_realsequence seq)) <= r by XREAL_1: 41;

      for p holds 0 < p implies r <= (( upper_bound ( inferior_realsequence seq)) + p)

      proof

        let p;

        assume 0 < p;

        then (r - p) <= ( upper_bound ( inferior_realsequence seq)) by A22;

        hence thesis by XREAL_1: 20;

      end;

      then

       A26: r <= ( upper_bound ( inferior_realsequence seq)) by XREAL_1: 41;

      

       A27: ( upper_bound ( inferior_realsequence seq)) <= ( lower_bound ( superior_realsequence seq)) by A14, Th55;

      ( lower_bound ( superior_realsequence seq)) <= r by A24, XREAL_1: 41;

      then ( upper_bound ( inferior_realsequence seq)) <= r by A27, XXREAL_0: 2;

      then r = ( upper_bound ( inferior_realsequence seq)) by A26, XXREAL_0: 1;

      hence thesis by A14, A27, A25, XXREAL_0: 1;

    end;

    theorem :: RINFSUP1:89

    seq is convergent implies ( lim seq) = ( lim_sup seq) & ( lim seq) = ( lim_inf seq)

    proof

      reconsider r = ( lim seq) as Real;

      assume

       A1: seq is convergent;

      then

       A2: ( upper_bound ( inferior_realsequence seq)) <= ( lower_bound ( superior_realsequence seq)) by Th55;

      

       A3: seq is bounded by A1;

      then

       A4: ( superior_realsequence seq) is bounded & ( inferior_realsequence seq) is bounded by Th56;

      

       A5: for p holds 0 < p implies (r - p) <= ( upper_bound ( inferior_realsequence seq)) & ( lower_bound ( superior_realsequence seq)) <= (r + p)

      proof

        let p;

        assume 0 < p;

        then

        consider k such that

         A6: for m st k <= m holds |.((seq . m) - r).| < p by A1, SEQ_2:def 7;

        

         A7: for m st k <= m holds (r - p) <= (seq . m) & (seq . m) <= (r + p)

        proof

          let m;

          assume k <= m;

          then |.((seq . m) - r).| < p by A6;

          hence thesis by Th1;

        end;

        then for m st k <= m holds (r - p) <= (seq . m);

        then

         A8: (r - p) <= (( inferior_realsequence seq) . k) by A3, Th43;

        for m st k <= m holds (seq . m) <= (r + p) by A7;

        then

         A9: (( superior_realsequence seq) . k) <= (r + p) by A3, Th45;

        (( inferior_realsequence seq) . k) <= ( upper_bound ( inferior_realsequence seq)) & ( lower_bound ( superior_realsequence seq)) <= (( superior_realsequence seq) . k) by A4, Th7, Th8;

        hence thesis by A8, A9, XXREAL_0: 2;

      end;

      

       A10: for p holds 0 < p implies r <= (( upper_bound ( inferior_realsequence seq)) + p)

      proof

        let p;

        assume 0 < p;

        then (r - p) <= ( upper_bound ( inferior_realsequence seq)) by A5;

        hence thesis by XREAL_1: 20;

      end;

      then

       A11: r <= ( upper_bound ( inferior_realsequence seq)) by XREAL_1: 41;

      r <= ( upper_bound ( inferior_realsequence seq)) by A10, XREAL_1: 41;

      then

       A12: r <= ( lower_bound ( superior_realsequence seq)) by A2, XXREAL_0: 2;

      for p holds 0 < p implies ( lower_bound ( superior_realsequence seq)) <= (r + p) by A5;

      then

       A13: ( lower_bound ( superior_realsequence seq)) <= r by XREAL_1: 41;

      then ( upper_bound ( inferior_realsequence seq)) <= r by A2, XXREAL_0: 2;

      hence thesis by A13, A11, A12, XXREAL_0: 1;

    end;

    theorem :: RINFSUP1:90

    

     Th90: seq is bounded implies ( lim_sup ( - seq)) = ( - ( lim_inf seq)) & ( lim_inf ( - seq)) = ( - ( lim_sup seq))

    proof

      assume

       A1: seq is bounded;

      then ( inferior_realsequence seq) is bounded by Th56;

      

      then

       A2: ( - ( lim_inf seq)) = ( - ( - ( lower_bound ( - ( inferior_realsequence seq))))) by Th13

      .= ( lower_bound ( - ( - ( superior_realsequence ( - seq))))) by A1, Th61

      .= ( lim_sup ( - seq));

      ( superior_realsequence seq) is bounded by A1, Th56;

      

      then ( - ( lim_sup seq)) = ( - ( - ( upper_bound ( - ( superior_realsequence seq))))) by Th14

      .= ( upper_bound ( - ( - ( inferior_realsequence ( - seq))))) by A1, Th62

      .= ( lim_inf ( - seq));

      hence thesis by A2;

    end;

    theorem :: RINFSUP1:91

    seq1 is bounded & seq2 is bounded & (for n holds (seq1 . n) <= (seq2 . n)) implies ( lim_sup seq1) <= ( lim_sup seq2) & ( lim_inf seq1) <= ( lim_inf seq2)

    proof

      assume that

       A1: seq1 is bounded and

       A2: seq2 is bounded and

       A3: for n holds (seq1 . n) <= (seq2 . n);

      

       A4: ( superior_realsequence seq1) is convergent & ( inferior_realsequence seq1) is convergent by A1, Th57, Th58;

      ( superior_realsequence seq2) is bounded by A2, Th56;

      then

       A5: ( lim ( superior_realsequence seq2)) = ( lower_bound ( superior_realsequence seq2)) by A2, Th25, Th51;

      ( inferior_realsequence seq1) is bounded by A1, Th56;

      then

       A6: ( lim ( inferior_realsequence seq1)) = ( upper_bound ( inferior_realsequence seq1)) by A1, Th24, Th50;

      ( superior_realsequence seq1) is bounded by A1, Th56;

      then

       A7: ( lim ( superior_realsequence seq1)) = ( lower_bound ( superior_realsequence seq1)) by A1, Th25, Th51;

      

       A8: ( superior_realsequence seq2) is convergent & ( inferior_realsequence seq2) is convergent by A2, Th57, Th58;

      ( inferior_realsequence seq2) is bounded by A2, Th56;

      then

       A9: ( lim ( inferior_realsequence seq2)) = ( upper_bound ( inferior_realsequence seq2)) by A2, Th24, Th50;

      (for n holds (( superior_realsequence seq1) . n) <= (( superior_realsequence seq2) . n)) & for n holds (( inferior_realsequence seq1) . n) <= (( inferior_realsequence seq2) . n) by A1, A2, A3, Th75;

      hence thesis by A4, A8, A7, A6, A5, A9, SEQ_2: 18;

    end;

    theorem :: RINFSUP1:92

    seq1 is bounded & seq2 is bounded implies (( lim_inf seq1) + ( lim_inf seq2)) <= ( lim_inf (seq1 + seq2)) & ( lim_inf (seq1 + seq2)) <= (( lim_inf seq1) + ( lim_sup seq2)) & ( lim_inf (seq1 + seq2)) <= (( lim_sup seq1) + ( lim_inf seq2)) & (( lim_inf seq1) + ( lim_sup seq2)) <= ( lim_sup (seq1 + seq2)) & (( lim_sup seq1) + ( lim_inf seq2)) <= ( lim_sup (seq1 + seq2)) & ( lim_sup (seq1 + seq2)) <= (( lim_sup seq1) + ( lim_sup seq2)) & (seq1 is convergent or seq2 is convergent implies ( lim_inf (seq1 + seq2)) = (( lim_inf seq1) + ( lim_inf seq2)) & ( lim_sup (seq1 + seq2)) = (( lim_sup seq1) + ( lim_sup seq2)))

    proof

      assume

       A1: seq1 is bounded & seq2 is bounded;

      

       A2: for seq1, seq2 st seq1 is bounded & seq2 is bounded holds ( lim_sup (seq1 + seq2)) <= (( lim_sup seq1) + ( lim_sup seq2))

      proof

        let seq1, seq2;

        set r1 = ( lim_sup seq1), r2 = ( lim_sup seq2);

        assume that

         A3: seq1 is bounded and

         A4: seq2 is bounded;

        for s st 0 < s holds ex n st for k holds ((seq1 + seq2) . (n + k)) < ((r1 + r2) + s)

        proof

          let s;

          assume 0 < s;

          then

           A5: 0 < (s / 2) by XREAL_1: 215;

          then

          consider n1 be Nat such that

           A6: for k holds (seq1 . (n1 + k)) < (r1 + (s / 2)) by A3, Th85;

          consider n2 be Nat such that

           A7: for k holds (seq2 . (n2 + k)) < (r2 + (s / 2)) by A4, A5, Th85;

          for k holds ((seq1 + seq2) . ((n1 + n2) + k)) < ((r1 + r2) + s)

          proof

            let k;

            (seq1 . (n1 + (n2 + k))) < (r1 + (s / 2)) & (seq2 . (n2 + (n1 + k))) < (r2 + (s / 2)) by A6, A7;

            then ((seq1 . ((n1 + n2) + k)) + (seq2 . ((n1 + n2) + k))) < ((r1 + (s / 2)) + (r2 + (s / 2))) by XREAL_1: 8;

            hence thesis by SEQ_1: 7;

          end;

          hence thesis;

        end;

        hence thesis by A3, A4, Th85;

      end;

      

       A8: for seq1, seq2 st seq1 is bounded & seq2 is bounded holds (( lim_inf seq1) + ( lim_sup seq2)) <= ( lim_sup (seq1 + seq2))

      proof

        let seq1, seq2;

        assume that

         A9: seq1 is bounded and

         A10: seq2 is bounded;

        ( lim_sup ((seq1 + seq2) + ( - seq1))) <= (( lim_sup ( - seq1)) + ( lim_sup (seq1 + seq2))) by A2, A9, A10;

        then ( lim_sup ((seq1 + seq2) + ( - seq1))) <= (( - ( lim_inf seq1)) + ( lim_sup (seq1 + seq2))) by A9, Th90;

        then ( lim_sup ((seq2 + seq1) - seq1)) <= (( lim_sup (seq1 + seq2)) - ( lim_inf seq1));

        then ( lim_sup seq2) <= (( lim_sup (seq1 + seq2)) - ( lim_inf seq1)) by Th2;

        hence thesis by XREAL_1: 19;

      end;

      then

       A11: (( lim_inf seq1) + ( lim_sup seq2)) <= ( lim_sup (seq1 + seq2)) by A1;

      

       A12: (( lim_sup seq1) + ( lim_inf seq2)) <= ( lim_sup (seq1 + seq2)) by A8, A1;

      

       A13: ( lim_sup (seq1 + seq2)) <= (( lim_sup seq1) + ( lim_sup seq2)) by A2, A1;

      

       A14: for seq1, seq2 st seq1 is bounded & seq2 is bounded holds (( lim_inf seq1) + ( lim_inf seq2)) <= ( lim_inf (seq1 + seq2))

      proof

        let seq1, seq2;

        set r1 = ( lim_inf seq1), r2 = ( lim_inf seq2);

        assume that

         A15: seq1 is bounded and

         A16: seq2 is bounded;

        for s st 0 < s holds ex n st for k holds ((r1 + r2) - s) < ((seq1 + seq2) . (n + k))

        proof

          let s;

          assume 0 < s;

          then

           A17: 0 < (s / 2) by XREAL_1: 215;

          then

          consider n1 be Nat such that

           A18: for k holds (r1 - (s / 2)) < (seq1 . (n1 + k)) by A15, Th82;

          consider n2 be Nat such that

           A19: for k holds (r2 - (s / 2)) < (seq2 . (n2 + k)) by A16, A17, Th82;

          for k holds ((r1 + r2) - s) < ((seq1 + seq2) . ((n1 + n2) + k))

          proof

            let k;

            (r1 - (s / 2)) < (seq1 . (n1 + (n2 + k))) & (r2 - (s / 2)) < (seq2 . (n2 + (n1 + k))) by A18, A19;

            then ((r1 - (s / 2)) + (r2 - (s / 2))) < ((seq1 . ((n1 + n2) + k)) + (seq2 . ((n1 + n2) + k))) by XREAL_1: 8;

            hence thesis by SEQ_1: 7;

          end;

          hence thesis;

        end;

        hence thesis by A15, A16, Th82;

      end;

      then

       A20: (( lim_inf seq1) + ( lim_inf seq2)) <= ( lim_inf (seq1 + seq2)) by A1;

      

       A21: for seq1, seq2 st seq1 is bounded & seq2 is bounded holds ( lim_inf (seq1 + seq2)) <= (( lim_inf seq1) + ( lim_sup seq2))

      proof

        let seq1, seq2;

        assume that

         A22: seq1 is bounded and

         A23: seq2 is bounded;

        ( lim_inf ((seq1 + seq2) + ( - seq2))) >= (( lim_inf (seq1 + seq2)) + ( lim_inf ( - seq2))) by A14, A22, A23;

        then ( lim_inf ((seq1 + seq2) + ( - seq2))) >= (( lim_inf (seq1 + seq2)) + ( - ( lim_sup seq2))) by A23, Th90;

        then ( lim_inf ((seq1 + seq2) - seq2)) >= (( lim_inf (seq1 + seq2)) - ( lim_sup seq2));

        then ( lim_inf seq1) >= (( lim_inf (seq1 + seq2)) - ( lim_sup seq2)) by Th2;

        hence thesis by XREAL_1: 20;

      end;

      then

       A24: ( lim_inf (seq1 + seq2)) <= (( lim_sup seq1) + ( lim_inf seq2)) by A1;

      

       A25: ( lim_inf (seq1 + seq2)) <= (( lim_inf seq1) + ( lim_sup seq2)) by A21, A1;

      seq1 is convergent or seq2 is convergent implies ( lim_inf (seq1 + seq2)) = (( lim_inf seq1) + ( lim_inf seq2)) & ( lim_sup (seq1 + seq2)) = (( lim_sup seq1) + ( lim_sup seq2))

      proof

        assume

         A26: seq1 is convergent or seq2 is convergent;

        per cases by A26;

          suppose seq1 is convergent;

          then ( lim_inf seq1) = ( lim_sup seq1) by Th88;

          hence thesis by A20, A24, A11, A13, XXREAL_0: 1;

        end;

          suppose seq2 is convergent;

          then ( lim_inf seq2) = ( lim_sup seq2) by Th88;

          hence thesis by A20, A25, A12, A13, XXREAL_0: 1;

        end;

      end;

      hence thesis by A14, A21, A2, A8, A1;

    end;

    theorem :: RINFSUP1:93

    seq1 is bounded nonnegative & seq2 is bounded nonnegative implies (( lim_inf seq1) * ( lim_inf seq2)) <= ( lim_inf (seq1 (#) seq2)) & ( lim_sup (seq1 (#) seq2)) <= (( lim_sup seq1) * ( lim_sup seq2))

    proof

      

       A1: for seq1, seq2 st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds ( lim_sup (seq1 (#) seq2)) <= (( lim_sup seq1) * ( lim_sup seq2))

      proof

        let seq1, seq2;

        assume that

         A2: seq1 is bounded nonnegative and

         A3: seq2 is bounded nonnegative;

        set seq3 = ( superior_realsequence seq1), seq4 = ( superior_realsequence seq2), seq5 = ( superior_realsequence (seq1 (#) seq2));

        

         A4: seq5 is convergent by A2, A3, Th58;

        

         A5: ( lower_bound seq5) = ( lim seq5) & ( lower_bound seq3) = ( lim seq3) by A2, A3, Th58;

        

         A6: ( lower_bound seq4) = ( lim seq4) by A3, Th58;

        

         A7: for n holds (seq5 . n) <= ((seq3 (#) seq4) . n)

        proof

          let n;

          (seq5 . n) <= ((seq3 . n) * (seq4 . n)) by A2, A3, Th80;

          hence thesis by SEQ_1: 8;

        end;

        

         A8: seq3 is convergent & seq4 is convergent by A2, A3, Th58;

        then (seq3 (#) seq4) is convergent;

        then ( lim seq5) <= ( lim (seq3 (#) seq4)) by A4, A7, SEQ_2: 18;

        hence thesis by A8, A5, A6, SEQ_2: 15;

      end;

      for seq1, seq2 st seq1 is bounded nonnegative & seq2 is bounded nonnegative holds (( lim_inf seq1) * ( lim_inf seq2)) <= ( lim_inf (seq1 (#) seq2))

      proof

        let seq1, seq2;

        assume that

         A9: seq1 is bounded nonnegative and

         A10: seq2 is bounded nonnegative;

        set seq3 = ( inferior_realsequence seq1), seq4 = ( inferior_realsequence seq2), seq5 = ( inferior_realsequence (seq1 (#) seq2));

        

         A11: seq5 is convergent by A9, A10, Th57;

        

         A12: ( upper_bound seq5) = ( lim seq5) & ( upper_bound seq3) = ( lim seq3) by A9, A10, Th57;

        

         A13: ( upper_bound seq4) = ( lim seq4) by A10, Th57;

        

         A14: for n holds (seq5 . n) >= ((seq3 (#) seq4) . n)

        proof

          let n;

          (seq5 . n) >= ((seq3 . n) * (seq4 . n)) by A9, A10, Th79;

          hence thesis by SEQ_1: 8;

        end;

        

         A15: seq3 is convergent & seq4 is convergent by A9, A10, Th57;

        then (seq3 (#) seq4) is convergent;

        then ( lim seq5) >= ( lim (seq3 (#) seq4)) by A11, A14, SEQ_2: 18;

        hence thesis by A15, A12, A13, SEQ_2: 15;

      end;

      hence thesis by A1;

    end;