:: RINFSUP1 semantic presentation begin Lm1: for r1, r2, s being real number st 0 < s & r1 <= r2 holds ( r1 < r2 + s & r1 - s < r2 ) proof let r1, r2, s be real number ; ::_thesis: ( 0 < s & r1 <= r2 implies ( r1 < r2 + s & r1 - s < r2 ) ) assume A1: 0 < s ; ::_thesis: ( not r1 <= r2 or ( r1 < r2 + s & r1 - s < r2 ) ) assume r1 <= r2 ; ::_thesis: ( r1 < r2 + s & r1 - s < r2 ) then r1 + 0 < r2 + s by A1, XREAL_1:8; hence ( r1 < r2 + s & r1 - s < r2 ) by XREAL_1:19; ::_thesis: verum end; theorem Th1: :: RINFSUP1:1 for s, r, t being real number holds ( ( s - r < t & s + r > t ) iff abs (t - s) < r ) proof let s, r, t be real number ; ::_thesis: ( ( s - r < t & s + r > t ) iff abs (t - s) < r ) thus ( s - r < t & s + r > t implies abs (t - s) < r ) ::_thesis: ( abs (t - s) < r implies ( s - r < t & s + r > t ) ) proof assume that A1: s - r < t and A2: s + r > t ; ::_thesis: abs (t - s) < r (- r) + s < t by A1; then A3: - r < t - s by XREAL_1:20; t - s < r by A2, XREAL_1:19; hence abs (t - s) < r by A3, SEQ_2:1; ::_thesis: verum end; assume A4: abs (t - s) < r ; ::_thesis: ( s - r < t & s + r > t ) 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 ( s - r < t & s + r > t ) by A5, XREAL_1:19; ::_thesis: verum end; definition let seq be Real_Sequence; func upper_bound seq -> Real equals :: RINFSUP1:def 1 upper_bound (rng seq); coherence upper_bound (rng seq) is Real ; end; :: deftheorem defines upper_bound RINFSUP1:def_1_:_ for seq being Real_Sequence holds upper_bound seq = upper_bound (rng seq); definition let seq be Real_Sequence; func lower_bound seq -> Real equals :: RINFSUP1:def 2 lower_bound (rng seq); coherence lower_bound (rng seq) is Real ; end; :: deftheorem defines lower_bound RINFSUP1:def_2_:_ for seq being Real_Sequence holds lower_bound seq = lower_bound (rng seq); theorem Th2: :: RINFSUP1:2 for seq1, seq2 being Real_Sequence holds (seq1 + seq2) - seq2 = seq1 proof let seq1, seq2 be Real_Sequence; ::_thesis: (seq1 + seq2) - seq2 = seq1 for n being Element of NAT holds ((seq1 + seq2) - seq2) . n = seq1 . n proof let n be Element of NAT ; ::_thesis: ((seq1 + seq2) - seq2) . n = seq1 . n ((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 ((seq1 + seq2) - seq2) . n = seq1 . n ; ::_thesis: verum end; hence (seq1 + seq2) - seq2 = seq1 by FUNCT_2:63; ::_thesis: verum end; theorem Th3: :: RINFSUP1:3 for r being real number for seq being Real_Sequence holds ( r in rng seq iff - r in rng (- seq) ) proof let r be real number ; ::_thesis: for seq being Real_Sequence holds ( r in rng seq iff - r in rng (- seq) ) let seq be Real_Sequence; ::_thesis: ( r in rng seq iff - r in rng (- seq) ) thus ( r in rng seq implies - r in rng (- seq) ) ::_thesis: ( - r in rng (- seq) implies r in rng seq ) proof assume r in rng seq ; ::_thesis: - r in rng (- seq) then consider n being Element of NAT such that A1: r = seq . n by FUNCT_2:113; - r = (- seq) . n by A1, SEQ_1:10; hence - r in rng (- seq) by VALUED_0:28; ::_thesis: verum end; assume - r in rng (- seq) ; ::_thesis: r in rng seq then consider n being 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 r in rng seq by VALUED_0:28; ::_thesis: verum end; theorem Th4: :: RINFSUP1:4 for seq being Real_Sequence holds rng (- seq) = -- (rng seq) proof let seq be Real_Sequence; ::_thesis: rng (- seq) = -- (rng seq) thus rng (- seq) c= -- (rng seq) :: according to XBOOLE_0:def_10 ::_thesis: -- (rng seq) c= rng (- seq) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (- seq) or x in -- (rng seq) ) assume A1: x in rng (- seq) ; ::_thesis: 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 x in -- (rng seq) ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in -- (rng seq) or x in rng (- seq) ) A2: -- (rng seq) c= REAL by MEMBERED:3; assume A3: x in -- (rng seq) ; ::_thesis: x in rng (- seq) then reconsider r = x as Real by A2; - r in -- (-- (rng seq)) by A3, MEMBER_1:12; then - (- r) in rng (- seq) by Th3; hence x in rng (- seq) ; ::_thesis: verum end; theorem Th5: :: RINFSUP1:5 for seq being Real_Sequence holds ( seq is V88() iff rng seq is bounded_above ) proof let seq be Real_Sequence; ::_thesis: ( seq is V88() iff rng seq is bounded_above ) A1: ( seq is V88() implies rng seq is bounded_above ) proof assume seq is V88() ; ::_thesis: rng seq is bounded_above then consider t being real number such that A2: for n being Element of NAT holds seq . n < t by SEQ_2:def_3; t is UpperBound of rng seq proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in rng seq or r <= t ) assume r in rng seq ; ::_thesis: r <= t then ex n being set st ( n in dom seq & seq . n = r ) by FUNCT_1:def_3; hence r <= t by A2; ::_thesis: verum end; hence rng seq is bounded_above by XXREAL_2:def_10; ::_thesis: verum end; ( rng seq is bounded_above implies seq is V88() ) proof assume rng seq is bounded_above ; ::_thesis: seq is V88() then consider t being real number such that A3: t is UpperBound of rng seq by XXREAL_2:def_10; A4: for r being real number st r in rng seq holds r <= t by A3, XXREAL_2:def_1; now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<_t_+_1 let n be Element of NAT ; ::_thesis: seq . n < t + 1 seq . n <= t by A4, FUNCT_2:4; hence seq . n < t + 1 by Lm1; ::_thesis: verum end; hence seq is V88() by SEQ_2:def_3; ::_thesis: verum end; hence ( seq is V88() iff rng seq is bounded_above ) by A1; ::_thesis: verum end; theorem Th6: :: RINFSUP1:6 for seq being Real_Sequence holds ( seq is V89() iff rng seq is bounded_below ) proof let seq be Real_Sequence; ::_thesis: ( seq is V89() iff rng seq is bounded_below ) A1: ( seq is V89() implies rng seq is bounded_below ) proof assume seq is V89() ; ::_thesis: rng seq is bounded_below then consider t being real number such that A2: for n being Element of NAT holds t < seq . n by SEQ_2:def_4; t is LowerBound of rng seq proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in rng seq or t <= r ) assume r in rng seq ; ::_thesis: t <= r then ex n being set st ( n in dom seq & seq . n = r ) by FUNCT_1:def_3; hence t <= r by A2; ::_thesis: verum end; hence rng seq is bounded_below by XXREAL_2:def_9; ::_thesis: verum end; ( rng seq is bounded_below implies seq is V89() ) proof assume rng seq is bounded_below ; ::_thesis: seq is V89() then consider t being real number such that A3: t is LowerBound of rng seq by XXREAL_2:def_9; A4: for r being real number st r in rng seq holds t <= r by A3, XXREAL_2:def_2; now__::_thesis:_for_n_being_Element_of_NAT_holds_t_-_1_<_seq_._n let n be Element of NAT ; ::_thesis: t - 1 < seq . n t <= seq . n by A4, FUNCT_2:4; hence t - 1 < seq . n by Lm1; ::_thesis: verum end; hence seq is V89() by SEQ_2:def_4; ::_thesis: verum end; hence ( seq is V89() iff rng seq is bounded_below ) by A1; ::_thesis: verum end; theorem Th7: :: RINFSUP1:7 for r being real number for seq being Real_Sequence st seq is V88() holds ( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) ) ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V88() holds ( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) ) ) let seq be Real_Sequence; ::_thesis: ( seq is V88() implies ( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) ) ) ) set R = rng seq; assume seq is V88() ; ::_thesis: ( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) ) ) then A1: rng seq is bounded_above by Th5; A2: rng seq <> {} by RELAT_1:41; A3: ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) implies r = upper_bound seq ) proof assume that A4: for n being Element of NAT holds seq . n <= r and A5: for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ; ::_thesis: r = upper_bound seq A6: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_r2_being_real_number_st_ (_r2_in_rng_seq_&_r_-_s_<_r2_) let s be real number ; ::_thesis: ( 0 < s implies ex r2 being real number st ( r2 in rng seq & r - s < r2 ) ) assume 0 < s ; ::_thesis: ex r2 being real number st ( r2 in rng seq & r - s < r2 ) then consider k being Element of NAT such that A7: r - s < seq . k by A5; consider r2 being real number such that A8: ( r2 in rng seq & r2 = seq . k ) by FUNCT_2:4; take r2 = r2; ::_thesis: ( r2 in rng seq & r - s < r2 ) thus ( r2 in rng seq & r - s < r2 ) by A7, A8; ::_thesis: verum end; now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_seq_holds_ r1_<=_r let r1 be real number ; ::_thesis: ( r1 in rng seq implies r1 <= r ) assume r1 in rng seq ; ::_thesis: r1 <= r then ex n being set st ( n in dom seq & seq . n = r1 ) by FUNCT_1:def_3; hence r1 <= r by A4; ::_thesis: verum end; hence r = upper_bound seq by A1, A2, A6, SEQ_4:def_1; ::_thesis: verum end; ( r = upper_bound seq implies ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) ) ) proof assume A9: r = upper_bound seq ; ::_thesis: ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) ) A10: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_k_being_Element_of_NAT_st_r_-_s_<_seq_._k let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st r - s < seq . k ) assume 0 < s ; ::_thesis: ex k being Element of NAT st r - s < seq . k then consider r2 being real number such that A11: r2 in rng seq and A12: r - s < r2 by A1, A2, A9, SEQ_4:def_1; consider k being Element of NAT such that A13: r2 = seq . k by A11, SETLIM_1:4; take k = k; ::_thesis: r - s < seq . k thus r - s < seq . k by A12, A13; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<=_r let n be Element of NAT ; ::_thesis: seq . n <= r seq . n in rng seq by FUNCT_2:4; hence seq . n <= r by A1, A9, SEQ_4:def_1; ::_thesis: verum end; hence ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) ) by A10; ::_thesis: verum end; hence ( r = upper_bound seq iff ( ( for n being Element of NAT holds seq . n <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . k ) ) ) by A3; ::_thesis: verum end; theorem Th8: :: RINFSUP1:8 for r being real number for seq being Real_Sequence st seq is V89() holds ( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) ) ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V89() holds ( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) ) ) let seq be Real_Sequence; ::_thesis: ( seq is V89() implies ( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) ) ) ) set R = rng seq; assume seq is V89() ; ::_thesis: ( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) ) ) then A1: rng seq is bounded_below by Th6; A2: rng seq <> {} by RELAT_1:41; A3: ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) implies r = lower_bound seq ) proof assume that A4: for n being Element of NAT holds r <= seq . n and A5: for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ; ::_thesis: r = lower_bound seq A6: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_r2_being_real_number_st_ (_r2_in_rng_seq_&_r2_<_r_+_s_) let s be real number ; ::_thesis: ( 0 < s implies ex r2 being real number st ( r2 in rng seq & r2 < r + s ) ) assume 0 < s ; ::_thesis: ex r2 being real number st ( r2 in rng seq & r2 < r + s ) then consider k being Element of NAT such that A7: seq . k < r + s by A5; consider r2 being real number such that A8: ( r2 in rng seq & r2 = seq . k ) by FUNCT_2:4; take r2 = r2; ::_thesis: ( r2 in rng seq & r2 < r + s ) thus ( r2 in rng seq & r2 < r + s ) by A7, A8; ::_thesis: verum end; now__::_thesis:_for_r1_being_real_number_st_r1_in_rng_seq_holds_ r_<=_r1 let r1 be real number ; ::_thesis: ( r1 in rng seq implies r <= r1 ) assume r1 in rng seq ; ::_thesis: r <= r1 then ex n being set st ( n in dom seq & seq . n = r1 ) by FUNCT_1:def_3; hence r <= r1 by A4; ::_thesis: verum end; hence r = lower_bound seq by A1, A2, A6, SEQ_4:def_2; ::_thesis: verum end; ( r = lower_bound seq implies ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) ) ) proof assume A9: r = lower_bound seq ; ::_thesis: ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) ) A10: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_k_being_Element_of_NAT_st_seq_._k_<_r_+_s let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st seq . k < r + s ) assume 0 < s ; ::_thesis: ex k being Element of NAT st seq . k < r + s then consider r2 being real number such that A11: r2 in rng seq and A12: r2 < r + s by A1, A2, A9, SEQ_4:def_2; consider k being Element of NAT such that A13: r2 = seq . k by A11, SETLIM_1:4; take k = k; ::_thesis: seq . k < r + s thus seq . k < r + s by A12, A13; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_holds_r_<=_seq_._n let n be Element of NAT ; ::_thesis: r <= seq . n seq . n in rng seq by FUNCT_2:4; hence r <= seq . n by A1, A9, SEQ_4:def_2; ::_thesis: verum end; hence ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) ) by A10; ::_thesis: verum end; hence ( r = lower_bound seq iff ( ( for n being Element of NAT holds r <= seq . n ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . k < r + s ) ) ) by A3; ::_thesis: verum end; theorem Th9: :: RINFSUP1:9 for r being real number for seq being Real_Sequence holds ( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() & upper_bound seq <= r ) ) proof let r be real number ; ::_thesis: for seq being Real_Sequence holds ( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() & upper_bound seq <= r ) ) let seq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n <= r ) iff ( seq is V88() & upper_bound seq <= r ) ) thus ( ( for n being Element of NAT holds seq . n <= r ) implies ( seq is V88() & upper_bound seq <= r ) ) ::_thesis: ( seq is V88() & upper_bound seq <= r implies for n being Element of NAT holds seq . n <= r ) proof assume A1: for n being Element of NAT holds seq . n <= r ; ::_thesis: ( seq is V88() & upper_bound seq <= r ) now__::_thesis:_for_m_being_Element_of_NAT_holds_seq_._m_<_r_+_1 let m be Element of NAT ; ::_thesis: seq . m < r + 1 seq . m <= r by A1; hence seq . m < r + 1 by Lm1; ::_thesis: verum end; hence A2: seq is V88() by SEQ_2:def_3; ::_thesis: upper_bound seq <= r now__::_thesis:_not_r_<_upper_bound_seq set r1 = (upper_bound seq) - r; assume r < upper_bound seq ; ::_thesis: contradiction then (upper_bound seq) - r > 0 by XREAL_1:50; then ex k being Element of NAT st (upper_bound seq) - ((upper_bound seq) - r) < seq . k by A2, Th7; hence contradiction by A1; ::_thesis: verum end; hence upper_bound seq <= r ; ::_thesis: verum end; assume that A3: seq is V88() and A4: upper_bound seq <= r ; ::_thesis: for n being Element of NAT holds seq . n <= r now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<=_r let n be Element of NAT ; ::_thesis: seq . n <= r seq . n <= upper_bound seq by A3, Th7; hence seq . n <= r by A4, XXREAL_0:2; ::_thesis: verum end; hence for n being Element of NAT holds seq . n <= r ; ::_thesis: verum end; theorem Th10: :: RINFSUP1:10 for r being real number for seq being Real_Sequence holds ( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() & r <= lower_bound seq ) ) proof let r be real number ; ::_thesis: for seq being Real_Sequence holds ( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() & r <= lower_bound seq ) ) let seq be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds r <= seq . n ) iff ( seq is V89() & r <= lower_bound seq ) ) thus ( ( for n being Element of NAT holds r <= seq . n ) implies ( seq is V89() & r <= lower_bound seq ) ) ::_thesis: ( seq is V89() & r <= lower_bound seq implies for n being Element of NAT holds r <= seq . n ) proof assume A1: for n being Element of NAT holds r <= seq . n ; ::_thesis: ( seq is V89() & r <= lower_bound seq ) now__::_thesis:_for_m_being_Element_of_NAT_holds_r_-_1_<_seq_._m let m be Element of NAT ; ::_thesis: r - 1 < seq . m r <= seq . m by A1; hence r - 1 < seq . m by Lm1; ::_thesis: verum end; hence A2: seq is V89() by SEQ_2:def_4; ::_thesis: r <= lower_bound seq now__::_thesis:_not_r_>_lower_bound_seq set r1 = r - (lower_bound seq); assume r > lower_bound seq ; ::_thesis: contradiction then r - (lower_bound seq) > 0 by XREAL_1:50; then ex k being Element of NAT st seq . k < (lower_bound seq) + (r - (lower_bound seq)) by A2, Th8; hence contradiction by A1; ::_thesis: verum end; hence r <= lower_bound seq ; ::_thesis: verum end; assume that A3: seq is V89() and A4: r <= lower_bound seq ; ::_thesis: for n being Element of NAT holds r <= seq . n now__::_thesis:_for_n_being_Element_of_NAT_holds_r_<=_seq_._n let n be Element of NAT ; ::_thesis: r <= seq . n lower_bound seq <= seq . n by A3, Th8; hence r <= seq . n by A4, XXREAL_0:2; ::_thesis: verum end; hence for n being Element of NAT holds r <= seq . n ; ::_thesis: verum end; theorem :: RINFSUP1:11 for seq being Real_Sequence holds ( seq is V88() iff - seq is V89() ) proof let seq be Real_Sequence; ::_thesis: ( seq is V88() iff - seq is V89() ) set seq1 = - seq; thus ( seq is V88() implies - seq is V89() ) ; ::_thesis: ( - seq is V89() implies seq is V88() ) assume - seq is V89() ; ::_thesis: seq is V88() then consider t being real number such that A1: for n being Element of NAT holds (- seq) . n > t by SEQ_2:def_4; for n being Element of NAT holds seq . n < - t proof let n be Element of NAT ; ::_thesis: seq . n < - t (- seq) . n = - (seq . n) by SEQ_1:10; then A2: - ((- seq) . n) = seq . n ; (- seq) . n > t by A1; hence seq . n < - t by A2, XREAL_1:24; ::_thesis: verum end; hence seq is V88() by SEQ_2:def_3; ::_thesis: verum end; theorem :: RINFSUP1:12 for seq being Real_Sequence holds ( seq is V89() iff - seq is V88() ) proof let seq be Real_Sequence; ::_thesis: ( seq is V89() iff - seq is V88() ) - (- seq) = seq ; hence ( seq is V89() iff - seq is V88() ) ; ::_thesis: verum end; theorem Th13: :: RINFSUP1:13 for seq being Real_Sequence st seq is V88() holds upper_bound seq = - (lower_bound (- seq)) proof let seq be Real_Sequence; ::_thesis: ( seq is V88() implies upper_bound seq = - (lower_bound (- seq)) ) assume seq is V88() ; ::_thesis: upper_bound seq = - (lower_bound (- seq)) then ( not rng seq is empty & rng seq is 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 upper_bound seq = - (lower_bound (- seq)) ; ::_thesis: verum end; theorem Th14: :: RINFSUP1:14 for seq being Real_Sequence st seq is V89() holds lower_bound seq = - (upper_bound (- seq)) proof let seq be Real_Sequence; ::_thesis: ( seq is V89() implies lower_bound seq = - (upper_bound (- seq)) ) assume seq is V89() ; ::_thesis: lower_bound seq = - (upper_bound (- seq)) then ( not rng seq is empty & rng seq is 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 lower_bound seq = - (upper_bound (- seq)) ; ::_thesis: verum end; theorem Th15: :: RINFSUP1:15 for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq2 is V89() implies lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2) ) assume that A1: seq1 is V89() and A2: seq2 is V89() ; ::_thesis: lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2) for n being Element of NAT holds (seq1 + seq2) . n >= (lower_bound seq1) + (lower_bound seq2) proof let n be Element of NAT ; ::_thesis: (seq1 + seq2) . n >= (lower_bound seq1) + (lower_bound seq2) 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 (seq1 + seq2) . n >= (lower_bound seq1) + (lower_bound seq2) by A3, XREAL_1:7; ::_thesis: verum end; hence lower_bound (seq1 + seq2) >= (lower_bound seq1) + (lower_bound seq2) by Th10; ::_thesis: verum end; theorem Th16: :: RINFSUP1:16 for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V88() & seq2 is V88() implies upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2) ) assume that A1: seq1 is V88() and A2: seq2 is V88() ; ::_thesis: upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2) for n being Element of NAT holds (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2) proof let n be Element of NAT ; ::_thesis: (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2) 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 (seq1 + seq2) . n <= (upper_bound seq1) + (upper_bound seq2) by A3, XREAL_1:7; ::_thesis: verum end; hence upper_bound (seq1 + seq2) <= (upper_bound seq1) + (upper_bound seq2) by Th9; ::_thesis: verum end; notation let f be Real_Sequence; synonym nonnegative f for nonnegative-yielding ; end; definition let f be Real_Sequence; redefine attr f is nonnegative-yielding means :Def3: :: RINFSUP1:def 3 for n being Element of NAT holds f . n >= 0 ; compatibility ( f is nonnegative iff for n being Element of NAT holds f . n >= 0 ) proof hereby ::_thesis: ( ( for n being Element of NAT holds f . n >= 0 ) implies f is nonnegative ) assume A1: f is nonnegative ; ::_thesis: for n being Element of NAT holds f . n >= 0 let n be Element of NAT ; ::_thesis: f . n >= 0 f . n in rng f by VALUED_0:28; hence f . n >= 0 by A1, PARTFUN3:def_4; ::_thesis: verum end; assume A2: for n being Element of NAT holds f . n >= 0 ; ::_thesis: f is nonnegative let r be real number ; :: according to PARTFUN3:def_4 ::_thesis: ( not r in K87(f) or 0 <= r ) assume r in rng f ; ::_thesis: 0 <= r then ex x being Element of NAT st r = f . x by FUNCT_2:113; hence 0 <= r by A2; ::_thesis: verum end; end; :: deftheorem Def3 defines nonnegative RINFSUP1:def_3_:_ for f being Real_Sequence holds ( f is nonnegative iff for n being Element of NAT holds f . n >= 0 ); theorem Th17: :: RINFSUP1:17 for k being Element of NAT for seq being Real_Sequence st seq is nonnegative holds seq ^\ k is nonnegative proof let k be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is nonnegative holds seq ^\ k is nonnegative let seq be Real_Sequence; ::_thesis: ( seq is nonnegative implies seq ^\ k is nonnegative ) assume A1: seq is nonnegative ; ::_thesis: seq ^\ k is nonnegative for n being Element of NAT holds (seq ^\ k) . n >= 0 proof let n be Element of NAT ; ::_thesis: (seq ^\ k) . n >= 0 (seq ^\ k) . n = seq . (n + k) by NAT_1:def_3; hence (seq ^\ k) . n >= 0 by A1, Def3; ::_thesis: verum end; hence seq ^\ k is nonnegative by Def3; ::_thesis: verum end; theorem Th18: :: RINFSUP1:18 for seq being Real_Sequence st seq is V89() & seq is nonnegative holds lower_bound seq >= 0 proof let seq be Real_Sequence; ::_thesis: ( seq is V89() & seq is nonnegative implies lower_bound seq >= 0 ) assume ( seq is V89() & seq is nonnegative ) ; ::_thesis: lower_bound seq >= 0 then for n being Element of NAT holds seq . n >= 0 by Def3; hence lower_bound seq >= 0 by Th10; ::_thesis: verum end; theorem :: RINFSUP1:19 for seq being Real_Sequence st seq is V88() & seq is nonnegative holds upper_bound seq >= 0 proof let seq be Real_Sequence; ::_thesis: ( seq is V88() & seq is nonnegative implies upper_bound seq >= 0 ) assume A1: ( seq is V88() & seq is nonnegative ) ; ::_thesis: upper_bound seq >= 0 then seq . 0 <= upper_bound seq by Th7; hence upper_bound seq >= 0 by A1, Def3; ::_thesis: verum end; theorem Th20: :: RINFSUP1:20 for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds ( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) ) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative implies ( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) ) ) assume that A1: ( seq1 is V89() & seq1 is nonnegative ) and A2: ( seq2 is V89() & seq2 is nonnegative ) ; ::_thesis: ( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) ) for n being Element of NAT holds (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2) proof let n be Element of NAT ; ::_thesis: (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2) 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 (seq1 (#) seq2) . n >= (lower_bound seq1) * (lower_bound seq2) by A3, A4, XREAL_1:66; ::_thesis: verum end; hence ( seq1 (#) seq2 is V89() & lower_bound (seq1 (#) seq2) >= (lower_bound seq1) * (lower_bound seq2) ) by Th10; ::_thesis: verum end; theorem Th21: :: RINFSUP1:21 for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds ( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) ) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative implies ( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) ) ) assume that A1: ( seq1 is V88() & seq1 is nonnegative ) and A2: ( seq2 is V88() & seq2 is nonnegative ) ; ::_thesis: ( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) ) for n being Element of NAT holds (seq1 (#) seq2) . n <= (upper_bound seq1) * (upper_bound seq2) proof let n be Element of NAT ; ::_thesis: (seq1 (#) seq2) . n <= (upper_bound seq1) * (upper_bound seq2) 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, Def3; ( seq2 . n <= upper_bound seq2 & seq1 . n >= 0 ) by A1, A2, Def3, Th7; hence (seq1 (#) seq2) . n <= (upper_bound seq1) * (upper_bound seq2) by A3, A4, XREAL_1:66; ::_thesis: verum end; hence ( seq1 (#) seq2 is V88() & upper_bound (seq1 (#) seq2) <= (upper_bound seq1) * (upper_bound seq2) ) by Th9; ::_thesis: verum end; theorem :: RINFSUP1:22 for seq being Real_Sequence st seq is V48() & seq is V88() holds seq is bounded ; theorem :: RINFSUP1:23 for seq being Real_Sequence st seq is V49() & seq is V89() holds seq is bounded ; theorem Th24: :: RINFSUP1:24 for seq being Real_Sequence st seq is V48() & seq is V88() holds lim seq = upper_bound seq proof let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies lim seq = upper_bound seq ) assume A1: ( seq is V48() & seq is V88() ) ; ::_thesis: lim seq = upper_bound seq then for n being Element of NAT holds seq . n <= lim seq by SEQ_4:37; then A2: upper_bound seq <= lim seq by Th9; for n being Element of NAT holds seq . n <= upper_bound seq by A1, Th7; then lim seq <= upper_bound seq by A1, PREPOWER:2; hence lim seq = upper_bound seq by A2, XXREAL_0:1; ::_thesis: verum end; theorem Th25: :: RINFSUP1:25 for seq being Real_Sequence st seq is V49() & seq is V89() holds lim seq = lower_bound seq proof let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies lim seq = lower_bound seq ) assume A1: ( seq is V49() & seq is V89() ) ; ::_thesis: lim seq = lower_bound seq then for n being Element of NAT holds lim seq <= seq . n by SEQ_4:38; then A2: lim seq <= lower_bound seq by Th10; for n being Element of NAT holds lower_bound seq <= seq . n by A1, Th8; then lower_bound seq <= lim seq by A1, PREPOWER:1; hence lim seq = lower_bound seq by A2, XXREAL_0:1; ::_thesis: verum end; theorem :: RINFSUP1:26 for k being Element of NAT for seq being Real_Sequence st seq is V88() holds seq ^\ k is V88() by SEQM_3:27; theorem :: RINFSUP1:27 for k being Element of NAT for seq being Real_Sequence st seq is V89() holds seq ^\ k is V89() by SEQM_3:28; theorem :: RINFSUP1:28 for k being Element of NAT for seq being Real_Sequence st seq is bounded holds seq ^\ k is bounded by SEQM_3:29; theorem Th29: :: RINFSUP1:29 for seq being Real_Sequence for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL proof let seq be Real_Sequence; ::_thesis: for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL let n be Element of NAT ; ::_thesis: { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL set Y = { (seq . k) where k is Element of NAT : n <= k } ; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in_REAL let x be set ; ::_thesis: ( x in { (seq . k) where k is Element of NAT : n <= k } implies x in REAL ) assume x in { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: x in REAL then consider z1 being set such that A1: z1 = x and A2: z1 in { (seq . k) where k is Element of NAT : n <= k } ; ex k1 being Element of NAT st ( z1 = seq . k1 & n <= k1 ) by A2; hence x in REAL by A1; ::_thesis: verum end; hence { (seq . k) where k is Element of NAT : n <= k } is Subset of REAL by TARSKI:def_3; ::_thesis: verum end; theorem Th30: :: RINFSUP1:30 for k being Element of NAT for seq being Real_Sequence holds rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n } proof let k be Element of NAT ; ::_thesis: for seq being Real_Sequence holds rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n } let seq be Real_Sequence; ::_thesis: rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n } set seq1 = seq ^\ k; set Z = { (seq . m) where m is Element of NAT : k <= m } ; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._m)_where_m_is_Element_of_NAT_:_k_<=_m__}__holds_ x_in_rng_(seq_^\_k) let x be set ; ::_thesis: ( x in { (seq . m) where m is Element of NAT : k <= m } implies x in rng (seq ^\ k) ) assume x in { (seq . m) where m is Element of NAT : k <= m } ; ::_thesis: x in rng (seq ^\ k) then consider k1 being Element of NAT such that A1: x = seq . k1 and A2: k <= k1 ; consider k2 being Nat such that A3: k1 = k + k2 by A2, NAT_1:10; reconsider k2 = k2 as Element of NAT by ORDINAL1:def_12; x = (seq ^\ k) . k2 by A1, A3, NAT_1:def_3; hence x in rng (seq ^\ k) by FUNCT_2:4; ::_thesis: verum end; then A4: { (seq . m) where m is Element of NAT : k <= m } c= rng (seq ^\ k) by TARSKI:def_3; A5: dom (seq ^\ k) = NAT by FUNCT_2:def_1; now__::_thesis:_for_y_being_set_st_y_in_rng_(seq_^\_k)_holds_ y_in__{__(seq_._m)_where_m_is_Element_of_NAT_:_k_<=_m__}_ let y be set ; ::_thesis: ( y in rng (seq ^\ k) implies y in { (seq . m) where m is Element of NAT : k <= m } ) assume y in rng (seq ^\ k) ; ::_thesis: y in { (seq . m) where m is Element of NAT : k <= m } then consider m1 being set such that A6: m1 in NAT and A7: y = (seq ^\ k) . m1 by A5, FUNCT_1:def_3; reconsider m1 = m1 as Element of NAT by A6; y = seq . (k + m1) by A7, NAT_1:def_3; hence y in { (seq . m) where m is Element of NAT : k <= m } by SETLIM_1:1; ::_thesis: verum end; then rng (seq ^\ k) c= { (seq . m) where m is Element of NAT : k <= m } by TARSKI:def_3; hence rng (seq ^\ k) = { (seq . n) where n is Element of NAT : k <= n } by A4, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th31: :: RINFSUP1:31 for seq being Real_Sequence st seq is V88() holds for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is bounded_above proof let seq be Real_Sequence; ::_thesis: ( seq is V88() implies for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is bounded_above ) assume A1: seq is V88() ; ::_thesis: for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is bounded_above let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is bounded_above set seq1 = seq ^\ n; seq ^\ n is V88() by A1, SEQM_3:27; then A2: rng (seq ^\ n) is bounded_above by Th5; let R be Subset of REAL; ::_thesis: ( R = { (seq . k) where k is Element of NAT : n <= k } implies R is bounded_above ) assume R = { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: R is bounded_above hence R is bounded_above by A2, Th30; ::_thesis: verum end; theorem Th32: :: RINFSUP1:32 for seq being Real_Sequence st seq is V89() holds for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is bounded_below proof let seq be Real_Sequence; ::_thesis: ( seq is V89() implies for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is bounded_below ) assume A1: seq is V89() ; ::_thesis: for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is bounded_below let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is bounded_below set seq1 = seq ^\ n; seq ^\ n is V89() by A1, SEQM_3:28; then A2: rng (seq ^\ n) is bounded_below by Th6; let R be Subset of REAL; ::_thesis: ( R = { (seq . k) where k is Element of NAT : n <= k } implies R is bounded_below ) assume R = { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: R is bounded_below hence R is bounded_below by A2, Th30; ::_thesis: verum end; theorem Th33: :: RINFSUP1:33 for seq being Real_Sequence st seq is bounded holds for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is real-bounded proof let seq be Real_Sequence; ::_thesis: ( seq is bounded implies for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is real-bounded ) assume A1: seq is bounded ; ::_thesis: for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is real-bounded let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds R is real-bounded let R be Subset of REAL; ::_thesis: ( R = { (seq . k) where k is Element of NAT : n <= k } implies R is real-bounded ) assume R = { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: R is real-bounded then ( R is bounded_above & R is bounded_below ) by A1, Th31, Th32; hence R is real-bounded by XXREAL_2:def_11; ::_thesis: verum end; theorem Th34: :: RINFSUP1:34 for seq being Real_Sequence st seq is V48() holds for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds lower_bound R = seq . n proof let seq be Real_Sequence; ::_thesis: ( seq is V48() implies for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds lower_bound R = seq . n ) assume A1: seq is V48() ; ::_thesis: for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds lower_bound R = seq . n let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds lower_bound R = seq . n A2: now__::_thesis:_for_r_being_real_number_st_r_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ seq_._n_<=_r let r be real number ; ::_thesis: ( r in { (seq . k) where k is Element of NAT : n <= k } implies seq . n <= r ) assume r in { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: seq . n <= r then consider r1 being real number such that A3: ( r = r1 & r1 in { (seq . k) where k is Element of NAT : n <= k } ) ; consider k1 being Element of NAT such that A4: r1 = seq . k1 and A5: n <= k1 by A3; consider k being Nat such that A6: n + k = k1 by A5, NAT_1:10; k in NAT by ORDINAL1:def_12; hence seq . n <= r by A1, A3, A4, A6, SEQM_3:5; ::_thesis: verum end; let R be Subset of REAL; ::_thesis: ( R = { (seq . k) where k is Element of NAT : n <= k } implies lower_bound R = seq . n ) A7: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_r_being_real_number_st_ (_r_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__&_r_<_(seq_._n)_+_s_) let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in { (seq . k) where k is Element of NAT : n <= k } & r < (seq . n) + s ) ) A8: seq . n in { (seq . k) where k is Element of NAT : n <= k } ; assume 0 < s ; ::_thesis: ex r being real number st ( r in { (seq . k) where k is Element of NAT : n <= k } & r < (seq . n) + s ) hence ex r being real number st ( r in { (seq . k) where k is Element of NAT : n <= k } & r < (seq . n) + s ) by A8, XREAL_1:29; ::_thesis: verum end; assume A9: R = { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: lower_bound R = seq . n then A10: R <> {} by SETLIM_1:1; R is bounded_below by A1, A9, Th32, LIMFUNC1:1; hence lower_bound R = seq . n by A9, A10, A2, A7, SEQ_4:def_2; ::_thesis: verum end; theorem Th35: :: RINFSUP1:35 for seq being Real_Sequence st seq is V49() holds for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds upper_bound R = seq . n proof let seq be Real_Sequence; ::_thesis: ( seq is V49() implies for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds upper_bound R = seq . n ) assume A1: seq is V49() ; ::_thesis: for n being Element of NAT for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds upper_bound R = seq . n let n be Element of NAT ; ::_thesis: for R being Subset of REAL st R = { (seq . k) where k is Element of NAT : n <= k } holds upper_bound R = seq . n A2: now__::_thesis:_for_r_being_real_number_st_r_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ r_<=_seq_._n let r be real number ; ::_thesis: ( r in { (seq . k) where k is Element of NAT : n <= k } implies r <= seq . n ) assume r in { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: r <= seq . n then consider r1 being real number such that A3: ( r = r1 & r1 in { (seq . k) where k is Element of NAT : n <= k } ) ; consider k1 being Element of NAT such that A4: r1 = seq . k1 and A5: n <= k1 by A3; consider k being Nat such that A6: n + k = k1 by A5, NAT_1:10; k in NAT by ORDINAL1:def_12; hence r <= seq . n by A1, A3, A4, A6, SEQM_3:7; ::_thesis: verum end; let R be Subset of REAL; ::_thesis: ( R = { (seq . k) where k is Element of NAT : n <= k } implies upper_bound R = seq . n ) A7: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_ ex_r_being_real_number_st_ (_r_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__&_(seq_._n)_-_s_<_r_) let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st ( r in { (seq . k) where k is Element of NAT : n <= k } & (seq . n) - s < r ) ) A8: seq . n in { (seq . k) where k is Element of NAT : n <= k } ; assume 0 < s ; ::_thesis: ex r being real number st ( r in { (seq . k) where k is Element of NAT : n <= k } & (seq . n) - s < r ) hence ex r being real number st ( r in { (seq . k) where k is Element of NAT : n <= k } & (seq . n) - s < r ) by A8, XREAL_1:44; ::_thesis: verum end; assume A9: R = { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: upper_bound R = seq . n then A10: R <> {} by SETLIM_1:1; R is bounded_above by A1, A9, Th31, LIMFUNC1:1; hence upper_bound R = seq . n by A9, A10, A2, A7, SEQ_4:def_1; ::_thesis: verum end; definition let seq be Real_Sequence; func inferior_realsequence seq -> Real_Sequence means :Def4: :: RINFSUP1:def 4 for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds it . n = lower_bound Y; existence ex b1 being Real_Sequence st for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b1 . n = lower_bound Y proof defpred S1[ Element of NAT , Element of REAL ] means for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : \$1 <= k } holds \$2 = lower_bound Y; A1: for n being Element of NAT ex y being Element of REAL st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S1[n,y] reconsider Y = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; reconsider y = lower_bound Y as Element of REAL ; for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds y = lower_bound Y ; hence ex y being Element of REAL st S1[n,y] ; ::_thesis: verum end; ex f being Function of NAT,REAL st for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1); hence ex b1 being Real_Sequence st for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b1 . n = lower_bound Y ; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b1 . n = lower_bound Y ) & ( for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b2 . n = lower_bound Y ) holds b1 = b2 proof let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds seq1 . n = lower_bound Y ) & ( for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds seq2 . n = lower_bound Y ) implies seq1 = seq2 ) assume that A2: for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds seq1 . n = lower_bound Y and A3: for m being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : m <= k } holds seq2 . m = lower_bound Y ; ::_thesis: seq1 = seq2 A4: for y being set st y in NAT holds seq1 . y = seq2 . y proof let y be set ; ::_thesis: ( y in NAT implies seq1 . y = seq2 . y ) assume y in NAT ; ::_thesis: seq1 . y = seq2 . y then reconsider y = y as Element of NAT ; reconsider Y = { (seq . k) where k is Element of NAT : y <= k } as Subset of REAL by Th29; seq1 . y = lower_bound Y by A2; hence seq1 . y = seq2 . y by A3; ::_thesis: verum end; ( NAT = dom seq1 & NAT = dom seq2 ) by FUNCT_2:def_1; hence seq1 = seq2 by A4, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def4 defines inferior_realsequence RINFSUP1:def_4_:_ for seq, b2 being Real_Sequence holds ( b2 = inferior_realsequence seq iff for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b2 . n = lower_bound Y ); definition let seq be Real_Sequence; func superior_realsequence seq -> Real_Sequence means :Def5: :: RINFSUP1:def 5 for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds it . n = upper_bound Y; existence ex b1 being Real_Sequence st for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b1 . n = upper_bound Y proof defpred S1[ Element of NAT , Element of REAL ] means for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : \$1 <= k } holds \$2 = upper_bound Y; A1: for n being Element of NAT ex y being Element of REAL st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S1[n,y] reconsider Y = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; reconsider y = upper_bound Y as Element of REAL ; for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds y = upper_bound Y ; hence ex y being Element of REAL st S1[n,y] ; ::_thesis: verum end; ex f being Function of NAT,REAL st for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1); hence ex b1 being Real_Sequence st for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b1 . n = upper_bound Y ; ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b1 . n = upper_bound Y ) & ( for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b2 . n = upper_bound Y ) holds b1 = b2 proof let seq1, seq2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds seq1 . n = upper_bound Y ) & ( for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds seq2 . n = upper_bound Y ) implies seq1 = seq2 ) assume that A2: for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds seq1 . n = upper_bound Y and A3: for m being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : m <= k } holds seq2 . m = upper_bound Y ; ::_thesis: seq1 = seq2 A4: for y being set st y in NAT holds seq1 . y = seq2 . y proof let y be set ; ::_thesis: ( y in NAT implies seq1 . y = seq2 . y ) assume y in NAT ; ::_thesis: seq1 . y = seq2 . y then reconsider y = y as Element of NAT ; reconsider Y = { (seq . k) where k is Element of NAT : y <= k } as Subset of REAL by Th29; seq1 . y = upper_bound Y by A2; hence seq1 . y = seq2 . y by A3; ::_thesis: verum end; ( NAT = dom seq1 & NAT = dom seq2 ) by FUNCT_2:def_1; hence seq1 = seq2 by A4, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def5 defines superior_realsequence RINFSUP1:def_5_:_ for seq, b2 being Real_Sequence holds ( b2 = superior_realsequence seq iff for n being Element of NAT for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds b2 . n = upper_bound Y ); theorem Th36: :: RINFSUP1:36 for n being Element of NAT for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence holds (inferior_realsequence seq) . n = lower_bound (seq ^\ n) let seq be Real_Sequence; ::_thesis: (inferior_realsequence seq) . n = lower_bound (seq ^\ n) reconsider Y = { (seq . k) where k is Element of NAT : 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 (inferior_realsequence seq) . n = lower_bound (seq ^\ n) ; ::_thesis: verum end; theorem Th37: :: RINFSUP1:37 for n being Element of NAT for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence holds (superior_realsequence seq) . n = upper_bound (seq ^\ n) let seq be Real_Sequence; ::_thesis: (superior_realsequence seq) . n = upper_bound (seq ^\ n) reconsider Y = { (seq . k) where k is Element of NAT : 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 (superior_realsequence seq) . n = upper_bound (seq ^\ n) ; ::_thesis: verum end; theorem Th38: :: RINFSUP1:38 for seq being Real_Sequence st seq is V89() holds (inferior_realsequence seq) . 0 = lower_bound seq proof let seq be Real_Sequence; ::_thesis: ( seq is V89() implies (inferior_realsequence seq) . 0 = lower_bound seq ) reconsider Y1 = { (seq . k) where k is Element of NAT : 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 ( seq is V89() implies (inferior_realsequence seq) . 0 = lower_bound seq ) ; ::_thesis: verum end; theorem Th39: :: RINFSUP1:39 for seq being Real_Sequence st seq is V88() holds (superior_realsequence seq) . 0 = upper_bound seq proof let seq be Real_Sequence; ::_thesis: ( seq is V88() implies (superior_realsequence seq) . 0 = upper_bound seq ) reconsider Y1 = { (seq . k) where k is Element of NAT : 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 ( seq is V88() implies (superior_realsequence seq) . 0 = upper_bound seq ) ; ::_thesis: verum end; theorem Th40: :: RINFSUP1:40 for n being Element of NAT for r being real number for seq being Real_Sequence st seq is V89() holds ( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) ) ) proof let n be Element of NAT ; ::_thesis: for r being real number for seq being Real_Sequence st seq is V89() holds ( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) ) ) let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V89() holds ( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) ) ) let seq be Real_Sequence; ::_thesis: ( seq is V89() implies ( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) ) ) ) reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; assume seq is V89() ; ::_thesis: ( r = (inferior_realsequence seq) . n iff ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) ) ) then A1: ( not Y1 is empty & Y1 is bounded_below ) by Th32, SETLIM_1:1; thus ( r = (inferior_realsequence seq) . n implies ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) ) ) ::_thesis: ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) implies r = (inferior_realsequence seq) . n ) proof assume r = (inferior_realsequence seq) . n ; ::_thesis: ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) ) then A2: r = lower_bound Y1 by Def4; A3: for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s proof let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st seq . (n + k) < r + s ) assume 0 < s ; ::_thesis: ex k being Element of NAT st seq . (n + k) < r + s then consider r1 being real number such that A4: r1 in Y1 and A5: r1 < r + s by A1, A2, SEQ_4:def_2; consider k1 being Element of NAT such that A6: r1 = seq . k1 and A7: n <= k1 by A4; consider k2 being Nat such that A8: k1 = n + k2 by A7, NAT_1:10; k2 in NAT by ORDINAL1:def_12; hence ex k being Element of NAT st seq . (n + k) < r + s by A5, A6, A8; ::_thesis: verum end; for k being Element of NAT holds r <= seq . (n + k) proof let k be Element of NAT ; ::_thesis: r <= seq . (n + k) seq . (n + k) in Y1 by SETLIM_1:1; hence r <= seq . (n + k) by A1, A2, SEQ_4:def_2; ::_thesis: verum end; hence ( ( for k being Element of NAT holds r <= seq . (n + k) ) & ( for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ) ) by A3; ::_thesis: verum end; assume that A9: for k being Element of NAT holds r <= seq . (n + k) and A10: for s being real number st 0 < s holds ex k being Element of NAT st seq . (n + k) < r + s ; ::_thesis: r = (inferior_realsequence seq) . n A11: for s being real number st 0 < s holds ex r1 being real number st ( r1 in Y1 & r1 < r + s ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r1 being real number st ( r1 in Y1 & r1 < r + s ) ) assume 0 < s ; ::_thesis: ex r1 being real number st ( r1 in Y1 & r1 < r + s ) then consider k being Element of NAT such that A12: seq . (n + k) < r + s by A10; n + k >= n by NAT_1:11; then seq . (n + k) in Y1 ; hence ex r1 being real number st ( r1 in Y1 & r1 < r + s ) by A12; ::_thesis: verum end; for r1 being real number st r1 in Y1 holds r <= r1 proof let r1 be real number ; ::_thesis: ( r1 in Y1 implies r <= r1 ) assume r1 in Y1 ; ::_thesis: r <= r1 then consider k1 being Element of NAT such that A13: r1 = seq . k1 and A14: n <= k1 ; consider k2 being Nat such that A15: k1 = n + k2 by A14, NAT_1:10; k2 in NAT by ORDINAL1:def_12; hence r <= r1 by A9, A13, A15; ::_thesis: verum end; then r = lower_bound Y1 by A1, A11, SEQ_4:def_2; hence r = (inferior_realsequence seq) . n by Def4; ::_thesis: verum end; theorem Th41: :: RINFSUP1:41 for n being Element of NAT for r being real number for seq being Real_Sequence st seq is V88() holds ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) ) ) proof let n be Element of NAT ; ::_thesis: for r being real number for seq being Real_Sequence st seq is V88() holds ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) ) ) let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V88() holds ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) ) ) let seq be Real_Sequence; ::_thesis: ( seq is V88() implies ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) ) ) ) reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; assume seq is V88() ; ::_thesis: ( r = (superior_realsequence seq) . n iff ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) ) ) then A1: ( not Y1 is empty & Y1 is bounded_above ) by Th31, SETLIM_1:1; thus ( r = (superior_realsequence seq) . n implies ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) ) ) ::_thesis: ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) implies r = (superior_realsequence seq) . n ) proof assume r = (superior_realsequence seq) . n ; ::_thesis: ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) ) then A2: r = upper_bound Y1 by Def5; A3: for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) proof let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st r - s < seq . (n + k) ) assume 0 < s ; ::_thesis: ex k being Element of NAT st r - s < seq . (n + k) then consider r1 being real number such that A4: r1 in Y1 and A5: r - s < r1 by A1, A2, SEQ_4:def_1; consider k1 being Element of NAT such that A6: r1 = seq . k1 and A7: n <= k1 by A4; consider k2 being Nat such that A8: k1 = n + k2 by A7, NAT_1:10; k2 in NAT by ORDINAL1:def_12; hence ex k being Element of NAT st r - s < seq . (n + k) by A5, A6, A8; ::_thesis: verum end; for k being Element of NAT holds seq . (n + k) <= r proof let k be Element of NAT ; ::_thesis: seq . (n + k) <= r seq . (n + k) in Y1 by SETLIM_1:1; hence seq . (n + k) <= r by A1, A2, SEQ_4:def_1; ::_thesis: verum end; hence ( ( for k being Element of NAT holds seq . (n + k) <= r ) & ( for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ) ) by A3; ::_thesis: verum end; assume that A9: for k being Element of NAT holds seq . (n + k) <= r and A10: for s being real number st 0 < s holds ex k being Element of NAT st r - s < seq . (n + k) ; ::_thesis: r = (superior_realsequence seq) . n A11: for s being real number st 0 < s holds ex r1 being real number st ( r1 in Y1 & r - s < r1 ) proof let s be real number ; ::_thesis: ( 0 < s implies ex r1 being real number st ( r1 in Y1 & r - s < r1 ) ) assume 0 < s ; ::_thesis: ex r1 being real number st ( r1 in Y1 & r - s < r1 ) then consider k being Element of NAT such that A12: r - s < seq . (n + k) by A10; n + k >= n by NAT_1:11; then seq . (n + k) in Y1 ; hence ex r1 being real number st ( r1 in Y1 & r - s < r1 ) by A12; ::_thesis: verum end; for r1 being real number st r1 in Y1 holds r1 <= r proof let r1 be real number ; ::_thesis: ( r1 in Y1 implies r1 <= r ) assume r1 in Y1 ; ::_thesis: r1 <= r then consider k1 being Element of NAT such that A13: r1 = seq . k1 and A14: n <= k1 ; consider k2 being Nat such that A15: k1 = n + k2 by A14, NAT_1:10; k2 in NAT by ORDINAL1:def_12; hence r1 <= r by A9, A13, A15; ::_thesis: verum end; then r = upper_bound Y1 by A1, A11, SEQ_4:def_1; hence r = (superior_realsequence seq) . n by Def5; ::_thesis: verum end; theorem Th42: :: RINFSUP1:42 for n being Element of NAT for r being real number for seq being Real_Sequence st seq is V89() holds ( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n ) proof let n be Element of NAT ; ::_thesis: for r being real number for seq being Real_Sequence st seq is V89() holds ( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n ) let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V89() holds ( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n ) let seq be Real_Sequence; ::_thesis: ( seq is V89() implies ( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n ) ) reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; set seq1 = seq ^\ n; assume seq is V89() ; ::_thesis: ( ( for k being Element of NAT holds r <= seq . (n + k) ) iff r <= (inferior_realsequence seq) . n ) then A1: seq ^\ n is V89() by SEQM_3:28; A2: rng (seq ^\ n) = Y1 by Th30; thus ( ( for k being Element of NAT holds r <= seq . (n + k) ) implies r <= (inferior_realsequence seq) . n ) ::_thesis: ( r <= (inferior_realsequence seq) . n implies for k being Element of NAT holds r <= seq . (n + k) ) proof assume A3: for k being Element of NAT holds r <= seq . (n + k) ; ::_thesis: r <= (inferior_realsequence seq) . n now__::_thesis:_for_n1_being_Element_of_NAT_holds_r_<=_(seq_^\_n)_._n1 let n1 be Element of NAT ; ::_thesis: r <= (seq ^\ n) . n1 (seq ^\ n) . n1 in rng (seq ^\ n) by FUNCT_2:4; then consider r1 being real number such that A4: (seq ^\ n) . n1 = r1 and A5: r1 in Y1 by A2; consider k1 being Element of NAT such that A6: r1 = seq . k1 and A7: n <= k1 by A5; consider k2 being Nat such that A8: k1 = n + k2 by A7, NAT_1:10; k2 in NAT by ORDINAL1:def_12; hence r <= (seq ^\ n) . n1 by A3, A4, A6, A8; ::_thesis: verum end; then r <= lower_bound (seq ^\ n) by Th10; then r <= lower_bound Y1 by Th30; hence r <= (inferior_realsequence seq) . n by Def4; ::_thesis: verum end; assume r <= (inferior_realsequence seq) . n ; ::_thesis: for k being Element of NAT holds r <= seq . (n + k) then r <= lower_bound Y1 by Def4; then A9: r <= lower_bound (seq ^\ n) by Th30; now__::_thesis:_for_m1_being_Element_of_NAT_holds_r_<=_seq_._(n_+_m1) let m1 be Element of NAT ; ::_thesis: r <= seq . (n + m1) n <= n + m1 by NAT_1:11; then seq . (n + m1) in Y1 ; then seq . (n + m1) in rng (seq ^\ n) by Th30; then ex k being set st ( k in dom (seq ^\ n) & (seq ^\ n) . k = seq . (n + m1) ) by FUNCT_1:def_3; hence r <= seq . (n + m1) by A1, A9, Th10; ::_thesis: verum end; hence for k being Element of NAT holds r <= seq . (n + k) ; ::_thesis: verum end; theorem Th43: :: RINFSUP1:43 for n being Element of NAT for r being real number for seq being Real_Sequence st seq is V89() holds ( ( for m being Element of NAT st n <= m holds r <= seq . m ) iff r <= (inferior_realsequence seq) . n ) proof let n be Element of NAT ; ::_thesis: for r being real number for seq being Real_Sequence st seq is V89() holds ( ( for m being Element of NAT st n <= m holds r <= seq . m ) iff r <= (inferior_realsequence seq) . n ) let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V89() holds ( ( for m being Element of NAT st n <= m holds r <= seq . m ) iff r <= (inferior_realsequence seq) . n ) let seq be Real_Sequence; ::_thesis: ( seq is V89() implies ( ( for m being Element of NAT st n <= m holds r <= seq . m ) iff r <= (inferior_realsequence seq) . n ) ) assume A1: seq is V89() ; ::_thesis: ( ( for m being Element of NAT st n <= m holds r <= seq . m ) iff r <= (inferior_realsequence seq) . n ) thus ( ( for m being Element of NAT st n <= m holds r <= seq . m ) implies r <= (inferior_realsequence seq) . n ) ::_thesis: ( r <= (inferior_realsequence seq) . n implies for m being Element of NAT st n <= m holds r <= seq . m ) proof assume for m being Element of NAT st n <= m holds r <= seq . m ; ::_thesis: r <= (inferior_realsequence seq) . n then for k being Element of NAT holds r <= seq . (n + k) by NAT_1:11; hence r <= (inferior_realsequence seq) . n by A1, Th42; ::_thesis: verum end; assume A2: r <= (inferior_realsequence seq) . n ; ::_thesis: for m being Element of NAT st n <= m holds r <= seq . m now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ r_<=_seq_._m let m be Element of NAT ; ::_thesis: ( n <= m implies r <= seq . m ) assume n <= m ; ::_thesis: r <= seq . m then consider k being Nat such that A3: m = n + k by NAT_1:10; k in NAT by ORDINAL1:def_12; hence r <= seq . m by A1, A2, A3, Th42; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds r <= seq . m ; ::_thesis: verum end; theorem Th44: :: RINFSUP1:44 for n being Element of NAT for r being real number for seq being Real_Sequence st seq is V88() holds ( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r ) proof let n be Element of NAT ; ::_thesis: for r being real number for seq being Real_Sequence st seq is V88() holds ( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r ) let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V88() holds ( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r ) let seq be Real_Sequence; ::_thesis: ( seq is V88() implies ( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r ) ) reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; set seq1 = seq ^\ n; assume seq is V88() ; ::_thesis: ( ( for k being Element of NAT holds seq . (n + k) <= r ) iff (superior_realsequence seq) . n <= r ) then A1: seq ^\ n is V88() by SEQM_3:27; A2: rng (seq ^\ n) = Y1 by Th30; thus ( ( for k being Element of NAT holds seq . (n + k) <= r ) implies (superior_realsequence seq) . n <= r ) ::_thesis: ( (superior_realsequence seq) . n <= r implies for k being Element of NAT holds seq . (n + k) <= r ) proof assume A3: for k being Element of NAT holds seq . (n + k) <= r ; ::_thesis: (superior_realsequence seq) . n <= r now__::_thesis:_for_n1_being_Element_of_NAT_holds_(seq_^\_n)_._n1_<=_r let n1 be Element of NAT ; ::_thesis: (seq ^\ n) . n1 <= r (seq ^\ n) . n1 in rng (seq ^\ n) by FUNCT_2:4; then consider r1 being real number such that A4: (seq ^\ n) . n1 = r1 and A5: r1 in Y1 by A2; consider k1 being Element of NAT such that A6: r1 = seq . k1 and A7: n <= k1 by A5; consider k2 being Nat such that A8: k1 = n + k2 by A7, NAT_1:10; k2 in NAT by ORDINAL1:def_12; hence (seq ^\ n) . n1 <= r by A3, A4, A6, A8; ::_thesis: verum end; then upper_bound (seq ^\ n) <= r by Th9; then upper_bound Y1 <= r by Th30; hence (superior_realsequence seq) . n <= r by Def5; ::_thesis: verum end; assume (superior_realsequence seq) . n <= r ; ::_thesis: for k being Element of NAT holds seq . (n + k) <= r then upper_bound Y1 <= r by Def5; then A9: upper_bound (seq ^\ n) <= r by Th30; now__::_thesis:_for_m1_being_Element_of_NAT_holds_seq_._(n_+_m1)_<=_r let m1 be Element of NAT ; ::_thesis: seq . (n + m1) <= r n <= n + m1 by NAT_1:11; then seq . (n + m1) in Y1 ; then seq . (n + m1) in rng (seq ^\ n) by Th30; then ex k being set st ( k in dom (seq ^\ n) & (seq ^\ n) . k = seq . (n + m1) ) by FUNCT_1:def_3; hence seq . (n + m1) <= r by A1, A9, Th9; ::_thesis: verum end; hence for k being Element of NAT holds seq . (n + k) <= r ; ::_thesis: verum end; theorem Th45: :: RINFSUP1:45 for n being Element of NAT for r being real number for seq being Real_Sequence st seq is V88() holds ( ( for m being Element of NAT st n <= m holds seq . m <= r ) iff (superior_realsequence seq) . n <= r ) proof let n be Element of NAT ; ::_thesis: for r being real number for seq being Real_Sequence st seq is V88() holds ( ( for m being Element of NAT st n <= m holds seq . m <= r ) iff (superior_realsequence seq) . n <= r ) let r be real number ; ::_thesis: for seq being Real_Sequence st seq is V88() holds ( ( for m being Element of NAT st n <= m holds seq . m <= r ) iff (superior_realsequence seq) . n <= r ) let seq be Real_Sequence; ::_thesis: ( seq is V88() implies ( ( for m being Element of NAT st n <= m holds seq . m <= r ) iff (superior_realsequence seq) . n <= r ) ) assume A1: seq is V88() ; ::_thesis: ( ( for m being Element of NAT st n <= m holds seq . m <= r ) iff (superior_realsequence seq) . n <= r ) thus ( ( for m being Element of NAT st n <= m holds seq . m <= r ) implies (superior_realsequence seq) . n <= r ) ::_thesis: ( (superior_realsequence seq) . n <= r implies for m being Element of NAT st n <= m holds seq . m <= r ) proof assume for m being Element of NAT st n <= m holds seq . m <= r ; ::_thesis: (superior_realsequence seq) . n <= r then for k being Element of NAT holds seq . (n + k) <= r by NAT_1:11; hence (superior_realsequence seq) . n <= r by A1, Th44; ::_thesis: verum end; assume A2: (superior_realsequence seq) . n <= r ; ::_thesis: for m being Element of NAT st n <= m holds seq . m <= r now__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ seq_._m_<=_r let m be Element of NAT ; ::_thesis: ( n <= m implies seq . m <= r ) assume n <= m ; ::_thesis: seq . m <= r then consider k being Nat such that A3: m = n + k by NAT_1:10; k in NAT by ORDINAL1:def_12; hence seq . m <= r by A1, A2, A3, Th44; ::_thesis: verum end; hence for m being Element of NAT st n <= m holds seq . m <= r ; ::_thesis: verum end; theorem Th46: :: RINFSUP1:46 for n being Element of NAT for seq being Real_Sequence st seq is V89() holds (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V89() holds (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) let seq be Real_Sequence; ::_thesis: ( seq is V89() implies (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) ) reconsider Y2 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29; reconsider Y1 = { (seq . k) where k is Element of NAT : 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 V89() ; ::_thesis: (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) then A3: ( Y2 <> {} & Y2 is bounded_below ) by Th32, SETLIM_1:1; A4: Y3 is bounded_below proof consider t being real number such that A5: for m being Element of NAT holds t < seq . m by A2, SEQ_2:def_4; t is LowerBound of Y3 proof let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in Y3 or t <= r ) assume r in Y3 ; ::_thesis: t <= r then r = seq . n by TARSKI:def_1; hence t <= r by A5; ::_thesis: verum end; hence Y3 is bounded_below by XXREAL_2:def_9; ::_thesis: verum 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 (inferior_realsequence seq) . n = min (((inferior_realsequence seq) . (n + 1)),(seq . n)) ; ::_thesis: verum end; theorem Th47: :: RINFSUP1:47 for n being Element of NAT for seq being Real_Sequence st seq is V88() holds (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V88() holds (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) let seq be Real_Sequence; ::_thesis: ( seq is V88() implies (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) ) reconsider Y2 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29; reconsider Y1 = { (seq . k) where k is Element of NAT : 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 V88() ; ::_thesis: (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) then A3: ( Y2 <> {} & Y2 is bounded_above ) by Th31, SETLIM_1:1; A4: Y3 is bounded_above proof consider t being real number such that A5: for m being Element of NAT holds seq . m < t by A2, SEQ_2:def_3; t is UpperBound of Y3 proof let r be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not r in Y3 or r <= t ) assume r in Y3 ; ::_thesis: r <= t then r = seq . n by TARSKI:def_1; hence r <= t by A5; ::_thesis: verum end; hence Y3 is bounded_above by XXREAL_2:def_10; ::_thesis: verum 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 (superior_realsequence seq) . n = max (((superior_realsequence seq) . (n + 1)),(seq . n)) ; ::_thesis: verum end; theorem Th48: :: RINFSUP1:48 for n being Element of NAT for seq being Real_Sequence st seq is V89() holds (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V89() holds (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) let seq be Real_Sequence; ::_thesis: ( seq is V89() implies (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) ) A1: min (((inferior_realsequence seq) . (n + 1)),(seq . n)) <= (inferior_realsequence seq) . (n + 1) by XXREAL_0:17; assume seq is V89() ; ::_thesis: (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) hence (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) by A1, Th46; ::_thesis: verum end; theorem Th49: :: RINFSUP1:49 for n being Element of NAT for seq being Real_Sequence st seq is V88() holds (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V88() holds (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n let seq be Real_Sequence; ::_thesis: ( seq is V88() implies (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n ) A1: (superior_realsequence seq) . (n + 1) <= max (((superior_realsequence seq) . (n + 1)),(seq . n)) by XXREAL_0:25; assume seq is V88() ; ::_thesis: (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n hence (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n by A1, Th47; ::_thesis: verum end; theorem Th50: :: RINFSUP1:50 for seq being Real_Sequence st seq is V89() holds inferior_realsequence seq is V48() proof let seq be Real_Sequence; ::_thesis: ( seq is V89() implies inferior_realsequence seq is V48() ) assume seq is V89() ; ::_thesis: inferior_realsequence seq is V48() then for n being Element of NAT holds (inferior_realsequence seq) . n <= (inferior_realsequence seq) . (n + 1) by Th48; hence inferior_realsequence seq is V48() by SEQM_3:def_8; ::_thesis: verum end; theorem Th51: :: RINFSUP1:51 for seq being Real_Sequence st seq is V88() holds superior_realsequence seq is V49() proof let seq be Real_Sequence; ::_thesis: ( seq is V88() implies superior_realsequence seq is V49() ) assume seq is V88() ; ::_thesis: superior_realsequence seq is V49() then for n being Element of NAT holds (superior_realsequence seq) . (n + 1) <= (superior_realsequence seq) . n by Th49; hence superior_realsequence seq is V49() by SEQM_3:def_9; ::_thesis: verum end; theorem :: RINFSUP1:52 for n being Element of NAT for seq being Real_Sequence st seq is bounded holds (inferior_realsequence seq) . n <= (superior_realsequence seq) . n proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is bounded holds (inferior_realsequence seq) . n <= (superior_realsequence seq) . n let seq be Real_Sequence; ::_thesis: ( seq is bounded implies (inferior_realsequence seq) . n <= (superior_realsequence seq) . n ) reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; assume A1: seq is bounded ; ::_thesis: (inferior_realsequence seq) . n <= (superior_realsequence seq) . n A2: Y1 <> {} by SETLIM_1:1; ( (superior_realsequence seq) . n = upper_bound Y1 & (inferior_realsequence seq) . n = lower_bound Y1 ) by Def4, Def5; hence (inferior_realsequence seq) . n <= (superior_realsequence seq) . n by A1, A2, Th33, SEQ_4:11; ::_thesis: verum end; theorem Th53: :: RINFSUP1:53 for n being Element of NAT for seq being Real_Sequence st seq is bounded holds (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is bounded holds (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) let seq be Real_Sequence; ::_thesis: ( seq is bounded implies (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) ) reconsider Y2 = { (seq . k2) where k2 is Element of NAT : n <= k2 } as Subset of REAL by Th29; assume A1: seq is bounded ; ::_thesis: (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) A2: now__::_thesis:_for_m_being_Element_of_NAT_holds_lower_bound_Y2_<=_(superior_realsequence_seq)_._m let m be Element of NAT ; ::_thesis: lower_bound Y2 <= (superior_realsequence seq) . m reconsider Y1 = { (seq . k1) where k1 is Element of NAT : 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 by XXREAL_2:def_11; 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 by XXREAL_2:def_11; 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; ::_thesis: verum end; (inferior_realsequence seq) . n = lower_bound Y2 by Def4; hence (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) by A2, Th10; ::_thesis: verum end; theorem Th54: :: RINFSUP1:54 for n being Element of NAT for seq being Real_Sequence st seq is bounded holds upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is bounded holds upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n let seq be Real_Sequence; ::_thesis: ( seq is bounded implies upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n ) reconsider Y2 = { (seq . k2) where k2 is Element of NAT : n <= k2 } as Subset of REAL by Th29; assume A1: seq is bounded ; ::_thesis: upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n A2: now__::_thesis:_for_m_being_Element_of_NAT_holds_upper_bound_Y2_>=_(inferior_realsequence_seq)_._m let m be Element of NAT ; ::_thesis: upper_bound Y2 >= (inferior_realsequence seq) . m reconsider Y1 = { (seq . k1) where k1 is Element of NAT : 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 by XXREAL_2:def_11; 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 by XXREAL_2:def_11; 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; ::_thesis: verum end; (superior_realsequence seq) . n = upper_bound Y2 by Def5; hence upper_bound (inferior_realsequence seq) <= (superior_realsequence seq) . n by A2, Th9; ::_thesis: verum end; theorem Th55: :: RINFSUP1:55 for seq being Real_Sequence st seq is bounded holds upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) proof let seq be Real_Sequence; ::_thesis: ( seq is bounded implies upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) ) set seq1 = inferior_realsequence seq; set r = lower_bound (superior_realsequence seq); assume seq is bounded ; ::_thesis: upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) then for n being Element of NAT holds (inferior_realsequence seq) . n <= lower_bound (superior_realsequence seq) by Th53; hence upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) by Th9; ::_thesis: verum end; theorem Th56: :: RINFSUP1:56 for seq being Real_Sequence st seq is bounded holds ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) proof let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) ) assume A1: seq is bounded ; ::_thesis: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) then inferior_realsequence seq is V48() by Th50; then A2: inferior_realsequence seq is V89() by LIMFUNC1:1; now__::_thesis:_for_m_being_Element_of_NAT_holds_(upper_bound_(inferior_realsequence_seq))_-_1_<_(superior_realsequence_seq)_._m let m be Element of NAT ; ::_thesis: (upper_bound (inferior_realsequence seq)) - 1 < (superior_realsequence seq) . 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; ::_thesis: verum end; then A3: superior_realsequence seq is V89() by SEQ_2:def_4; now__::_thesis:_for_m_being_Element_of_NAT_holds_(inferior_realsequence_seq)_._m_<_(lower_bound_(superior_realsequence_seq))_+_1 let m be Element of NAT ; ::_thesis: (inferior_realsequence seq) . m < (lower_bound (superior_realsequence seq)) + 1 (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; ::_thesis: verum end; then A4: inferior_realsequence seq is V88() by SEQ_2:def_3; superior_realsequence seq is V49() by A1, Th51; then superior_realsequence seq is V88() by LIMFUNC1:1; hence ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A2, A4, A3; ::_thesis: verum end; theorem Th57: :: RINFSUP1:57 for seq being Real_Sequence st seq is bounded holds ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) ) proof let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) ) ) assume seq is bounded ; ::_thesis: ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) ) then ( inferior_realsequence seq is V48() & inferior_realsequence seq is bounded ) by Th50, Th56; hence ( inferior_realsequence seq is convergent & lim (inferior_realsequence seq) = upper_bound (inferior_realsequence seq) ) by Th24; ::_thesis: verum end; theorem Th58: :: RINFSUP1:58 for seq being Real_Sequence st seq is bounded holds ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) ) proof let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) ) ) assume seq is bounded ; ::_thesis: ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) ) then ( superior_realsequence seq is V49() & superior_realsequence seq is bounded ) by Th51, Th56; hence ( superior_realsequence seq is convergent & lim (superior_realsequence seq) = lower_bound (superior_realsequence seq) ) by Th25; ::_thesis: verum end; theorem Th59: :: RINFSUP1:59 for n being Element of NAT for seq being Real_Sequence st seq is V89() holds (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V89() holds (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) let seq be Real_Sequence; ::_thesis: ( seq is V89() implies (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) ) assume A1: seq is V89() ; ::_thesis: (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) (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 (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) by Th37; ::_thesis: verum end; theorem Th60: :: RINFSUP1:60 for n being Element of NAT for seq being Real_Sequence st seq is V88() holds (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V88() holds (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) let seq be Real_Sequence; ::_thesis: ( seq is V88() implies (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) ) assume A1: seq is V88() ; ::_thesis: (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) (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 (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) by Th36; ::_thesis: verum end; theorem Th61: :: RINFSUP1:61 for seq being Real_Sequence st seq is V89() holds inferior_realsequence seq = - (superior_realsequence (- seq)) proof let seq be Real_Sequence; ::_thesis: ( seq is V89() implies inferior_realsequence seq = - (superior_realsequence (- seq)) ) assume seq is V89() ; ::_thesis: inferior_realsequence seq = - (superior_realsequence (- seq)) then for n being Element of NAT holds (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) by Th59; hence inferior_realsequence seq = - (superior_realsequence (- seq)) by SEQ_1:10; ::_thesis: verum end; theorem Th62: :: RINFSUP1:62 for seq being Real_Sequence st seq is V88() holds superior_realsequence seq = - (inferior_realsequence (- seq)) proof let seq be Real_Sequence; ::_thesis: ( seq is V88() implies superior_realsequence seq = - (inferior_realsequence (- seq)) ) assume seq is V88() ; ::_thesis: superior_realsequence seq = - (inferior_realsequence (- seq)) then for n being Element of NAT holds (superior_realsequence seq) . n = - ((inferior_realsequence (- seq)) . n) by Th60; hence superior_realsequence seq = - (inferior_realsequence (- seq)) by SEQ_1:10; ::_thesis: verum end; theorem :: RINFSUP1:63 for n being Element of NAT for seq being Real_Sequence st seq is V48() holds seq . n <= (inferior_realsequence seq) . (n + 1) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() holds seq . n <= (inferior_realsequence seq) . (n + 1) let seq be Real_Sequence; ::_thesis: ( seq is V48() implies seq . n <= (inferior_realsequence seq) . (n + 1) ) reconsider Y1 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29; A1: (inferior_realsequence seq) . (n + 1) = lower_bound Y1 by Def4; assume A2: seq is V48() ; ::_thesis: seq . n <= (inferior_realsequence seq) . (n + 1) then lower_bound Y1 = seq . (n + 1) by Th34; hence seq . n <= (inferior_realsequence seq) . (n + 1) by A2, A1, SEQM_3:def_8; ::_thesis: verum end; Lm2: for n being Element of NAT for seq being Real_Sequence st seq is V48() holds (inferior_realsequence seq) . n = seq . n proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() holds (inferior_realsequence seq) . n = seq . n let seq be Real_Sequence; ::_thesis: ( seq is V48() implies (inferior_realsequence seq) . n = seq . n ) reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; assume A1: seq is V48() ; ::_thesis: (inferior_realsequence seq) . n = seq . n (inferior_realsequence seq) . n = lower_bound Y1 by Def4; hence (inferior_realsequence seq) . n = seq . n by A1, Th34; ::_thesis: verum end; theorem :: RINFSUP1:64 for seq being Real_Sequence st seq is V48() holds inferior_realsequence seq = seq proof let seq be Real_Sequence; ::_thesis: ( seq is V48() implies inferior_realsequence seq = seq ) assume seq is V48() ; ::_thesis: inferior_realsequence seq = seq then for n being Element of NAT holds (inferior_realsequence seq) . n = seq . n by Lm2; hence inferior_realsequence seq = seq by FUNCT_2:63; ::_thesis: verum end; theorem Th65: :: RINFSUP1:65 for n being Element of NAT for seq being Real_Sequence st seq is V48() & seq is V88() holds seq . n <= (superior_realsequence seq) . (n + 1) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() & seq is V88() holds seq . n <= (superior_realsequence seq) . (n + 1) let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies seq . n <= (superior_realsequence seq) . (n + 1) ) reconsider Y1 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29; A1: seq . (n + 1) in Y1 ; assume A2: ( seq is V48() & seq is V88() ) ; ::_thesis: seq . n <= (superior_realsequence seq) . (n + 1) 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, SEQM_3:def_8; hence seq . n <= (superior_realsequence seq) . (n + 1) by A4, A3, XXREAL_0:2; ::_thesis: verum end; theorem Th66: :: RINFSUP1:66 for n being Element of NAT for seq being Real_Sequence st seq is V48() & seq is V88() holds (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() & seq is V88() holds (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) ) assume A1: ( seq is V48() & seq is V88() ) ; ::_thesis: (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) 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 (superior_realsequence seq) . n = (superior_realsequence seq) . (n + 1) by A1, Th47; ::_thesis: verum end; theorem Th67: :: RINFSUP1:67 for n being Element of NAT for seq being Real_Sequence st seq is V48() & seq is V88() holds ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V48() & seq is V88() holds ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) ) defpred S1[ Nat] means (superior_realsequence seq) . \$1 = upper_bound seq; assume A1: ( seq is V48() & seq is V88() ) ; ::_thesis: ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) A2: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) k in NAT by ORDINAL1:def_12; hence ( S1[k] implies S1[k + 1] ) by A1, Th66; ::_thesis: verum end; A3: S1[ 0 ] by A1, Th39; for k being Nat holds S1[k] from NAT_1:sch_2(A3, A2); hence ( (superior_realsequence seq) . n = upper_bound seq & superior_realsequence seq is constant ) by VALUED_0:def_18; ::_thesis: verum end; theorem :: RINFSUP1:68 for seq being Real_Sequence st seq is V48() & seq is V88() holds lower_bound (superior_realsequence seq) = upper_bound seq proof let seq be Real_Sequence; ::_thesis: ( seq is V48() & seq is V88() implies lower_bound (superior_realsequence seq) = upper_bound seq ) assume A1: ( seq is V48() & seq is V88() ) ; ::_thesis: lower_bound (superior_realsequence seq) = upper_bound seq then superior_realsequence seq is constant by Th67; then consider r1 being 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 being 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 lower_bound (superior_realsequence seq) = upper_bound seq by SEQ_4:9; ::_thesis: verum end; theorem :: RINFSUP1:69 for n being Element of NAT for seq being Real_Sequence st seq is V49() holds (superior_realsequence seq) . (n + 1) <= seq . n proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() holds (superior_realsequence seq) . (n + 1) <= seq . n let seq be Real_Sequence; ::_thesis: ( seq is V49() implies (superior_realsequence seq) . (n + 1) <= seq . n ) reconsider Y1 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29; A1: (superior_realsequence seq) . (n + 1) = upper_bound Y1 by Def5; assume A2: seq is V49() ; ::_thesis: (superior_realsequence seq) . (n + 1) <= seq . n then upper_bound Y1 = seq . (n + 1) by Th35; hence (superior_realsequence seq) . (n + 1) <= seq . n by A2, A1, SEQM_3:def_9; ::_thesis: verum end; Lm3: for n being Element of NAT for seq being Real_Sequence st seq is V49() holds (superior_realsequence seq) . n = seq . n proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() holds (superior_realsequence seq) . n = seq . n let seq be Real_Sequence; ::_thesis: ( seq is V49() implies (superior_realsequence seq) . n = seq . n ) reconsider Y1 = { (seq . k) where k is Element of NAT : n <= k } as Subset of REAL by Th29; assume A1: seq is V49() ; ::_thesis: (superior_realsequence seq) . n = seq . n (superior_realsequence seq) . n = upper_bound Y1 by Def5; hence (superior_realsequence seq) . n = seq . n by A1, Th35; ::_thesis: verum end; theorem :: RINFSUP1:70 for seq being Real_Sequence st seq is V49() holds superior_realsequence seq = seq proof let seq be Real_Sequence; ::_thesis: ( seq is V49() implies superior_realsequence seq = seq ) assume seq is V49() ; ::_thesis: superior_realsequence seq = seq then for n being Element of NAT holds (superior_realsequence seq) . n = seq . n by Lm3; hence superior_realsequence seq = seq by FUNCT_2:63; ::_thesis: verum end; theorem Th71: :: RINFSUP1:71 for n being Element of NAT for seq being Real_Sequence st seq is V49() & seq is V89() holds (inferior_realsequence seq) . (n + 1) <= seq . n proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() & seq is V89() holds (inferior_realsequence seq) . (n + 1) <= seq . n let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies (inferior_realsequence seq) . (n + 1) <= seq . n ) reconsider Y1 = { (seq . k) where k is Element of NAT : n + 1 <= k } as Subset of REAL by Th29; A1: seq . (n + 1) in Y1 ; assume A2: ( seq is V49() & seq is V89() ) ; ::_thesis: (inferior_realsequence seq) . (n + 1) <= seq . n 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, SEQM_3:def_9; hence (inferior_realsequence seq) . (n + 1) <= seq . n by A4, A3, XXREAL_0:2; ::_thesis: verum end; theorem Th72: :: RINFSUP1:72 for n being Element of NAT for seq being Real_Sequence st seq is V49() & seq is V89() holds (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() & seq is V89() holds (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) ) assume A1: ( seq is V49() & seq is V89() ) ; ::_thesis: (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) 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 (inferior_realsequence seq) . n = (inferior_realsequence seq) . (n + 1) by A1, Th46; ::_thesis: verum end; theorem Th73: :: RINFSUP1:73 for n being Element of NAT for seq being Real_Sequence st seq is V49() & seq is V89() holds ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) proof let n be Element of NAT ; ::_thesis: for seq being Real_Sequence st seq is V49() & seq is V89() holds ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) ) assume that A1: seq is V49() and A2: seq is V89() ; ::_thesis: ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) defpred S1[ Nat] means (inferior_realsequence seq) . \$1 = lower_bound seq; A3: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) k in NAT by ORDINAL1:def_12; hence ( S1[k] implies S1[k + 1] ) by A1, A2, Th72; ::_thesis: verum end; A4: S1[ 0 ] by A2, Th38; for k being Nat holds S1[k] from NAT_1:sch_2(A4, A3); hence ( (inferior_realsequence seq) . n = lower_bound seq & inferior_realsequence seq is constant ) by VALUED_0:def_18; ::_thesis: verum end; theorem :: RINFSUP1:74 for seq being Real_Sequence st seq is V49() & seq is V89() holds upper_bound (inferior_realsequence seq) = lower_bound seq proof let seq be Real_Sequence; ::_thesis: ( seq is V49() & seq is V89() implies upper_bound (inferior_realsequence seq) = lower_bound seq ) assume A1: ( seq is V49() & seq is V89() ) ; ::_thesis: upper_bound (inferior_realsequence seq) = lower_bound seq then inferior_realsequence seq is constant by Th73; then consider r1 being 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 being 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 upper_bound (inferior_realsequence seq) = lower_bound seq ; ::_thesis: verum end; theorem Th75: :: RINFSUP1:75 for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) implies ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) ) assume that A1: seq1 is bounded and A2: seq2 is bounded and A3: for n being Element of NAT holds seq1 . n <= seq2 . n ; ::_thesis: ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_ (_(superior_realsequence_seq1)_._n_<=_(superior_realsequence_seq2)_._n_&_(inferior_realsequence_seq1)_._n_<=_(inferior_realsequence_seq2)_._n_) let n be Element of NAT ; ::_thesis: ( (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n & (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) reconsider Y2 = { (seq2 . k2) where k2 is Element of NAT : n <= k2 } as Subset of REAL by Th29; reconsider Y1 = { (seq1 . k1) where k1 is Element of NAT : 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 by XXREAL_2:def_11; now__::_thesis:_for_r_being_real_number_st_r_in_Y2_holds_ lower_bound_Y1_<=_r let r be real number ; ::_thesis: ( r in Y2 implies lower_bound Y1 <= r ) assume r in Y2 ; ::_thesis: lower_bound Y1 <= r then consider k being Element of NAT 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; ::_thesis: verum end; then A10: for r being Real st r in Y2 holds lower_bound Y1 <= r ; Y2 is real-bounded by A2, Th33; then A11: Y2 is bounded_above by XXREAL_2:def_11; A12: now__::_thesis:_for_r_being_real_number_st_r_in_Y1_holds_ r_<=_upper_bound_Y2 let r be real number ; ::_thesis: ( r in Y1 implies r <= upper_bound Y2 ) assume r in Y1 ; ::_thesis: r <= upper_bound Y2 then consider k being Element of NAT 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; ::_thesis: verum 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; ::_thesis: verum end; hence ( ( for n being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) ; ::_thesis: verum end; theorem :: RINFSUP1:76 for n being Element of NAT for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) proof let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V89() & seq2 is V89() holds (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq2 is V89() implies (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) ) assume ( seq1 is V89() & seq2 is V89() ) ; ::_thesis: (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) then ( seq1 ^\ n is V89() & seq2 ^\ n is V89() ) 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 (inferior_realsequence (seq1 + seq2)) . n >= ((inferior_realsequence seq1) . n) + ((inferior_realsequence seq2) . n) by A1, Th36; ::_thesis: verum end; theorem :: RINFSUP1:77 for n being Element of NAT for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) proof let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V88() & seq2 is V88() holds (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V88() & seq2 is V88() implies (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) ) assume ( seq1 is V88() & seq2 is V88() ) ; ::_thesis: (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) then ( seq1 ^\ n is V88() & seq2 ^\ n is V88() ) 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 (superior_realsequence (seq1 + seq2)) . n <= ((superior_realsequence seq1) . n) + ((superior_realsequence seq2) . n) by A1, Th37; ::_thesis: verum end; theorem :: RINFSUP1:78 for n being Element of NAT for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) proof let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative implies (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) ) assume ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative ) ; ::_thesis: (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) then ( seq1 ^\ n is V89() & seq1 ^\ n is nonnegative & seq2 ^\ n is V89() & seq2 ^\ n is 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 (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) by A1, Th36; ::_thesis: verum end; theorem Th79: :: RINFSUP1:79 for n being Element of NAT for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) proof let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative holds (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative implies (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) ) assume ( seq1 is V89() & seq1 is nonnegative & seq2 is V89() & seq2 is nonnegative ) ; ::_thesis: (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) then ( seq1 ^\ n is V89() & seq1 ^\ n is nonnegative & seq2 ^\ n is V89() & seq2 ^\ n is 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 (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) by A1, Th36; ::_thesis: verum end; theorem Th80: :: RINFSUP1:80 for n being Element of NAT for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) proof let n be Element of NAT ; ::_thesis: for seq1, seq2 being Real_Sequence st seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative holds (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative implies (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) ) assume ( seq1 is V88() & seq1 is nonnegative & seq2 is V88() & seq2 is nonnegative ) ; ::_thesis: (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) then ( seq1 ^\ n is V88() & seq1 ^\ n is nonnegative & seq2 ^\ n is V88() & seq2 ^\ n is 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 (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) by A1, Th37; ::_thesis: verum end; definition let seq be Real_Sequence; func lim_sup seq -> Element of REAL equals :: RINFSUP1:def 6 lower_bound (superior_realsequence seq); coherence lower_bound (superior_realsequence seq) is Element of REAL ; end; :: deftheorem defines lim_sup RINFSUP1:def_6_:_ for seq being Real_Sequence holds lim_sup seq = lower_bound (superior_realsequence seq); definition let seq be Real_Sequence; func lim_inf seq -> Element of REAL equals :: RINFSUP1:def 7 upper_bound (inferior_realsequence seq); coherence upper_bound (inferior_realsequence seq) is Element of REAL ; end; :: deftheorem defines lim_inf RINFSUP1:def_7_:_ for seq being Real_Sequence holds lim_inf seq = upper_bound (inferior_realsequence seq); theorem Th81: :: RINFSUP1:81 for r being real number for seq being Real_Sequence st seq is bounded holds ( lim_inf seq <= r iff for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds ( lim_inf seq <= r iff for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( lim_inf seq <= r iff for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) ) set seq1 = inferior_realsequence seq; assume A1: seq is bounded ; ::_thesis: ( lim_inf seq <= r iff for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) then A2: inferior_realsequence seq is bounded by Th56; thus ( lim_inf seq <= r implies for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) ::_thesis: ( ( for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) implies lim_inf seq <= r ) proof assume A3: lim_inf seq <= r ; ::_thesis: for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s let s be real number ; ::_thesis: ( 0 < s implies for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) assume A4: 0 < s ; ::_thesis: for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s proof let n be Element of NAT ; ::_thesis: ex k being Element of NAT st seq . (n + k) < r + s consider k being Element of NAT such that A5: seq . (n + k) < ((inferior_realsequence seq) . n) + s by A1, A4, Th40; (inferior_realsequence seq) . n <= r by A2, A3, Th9; then (seq . (n + k)) + ((inferior_realsequence seq) . n) < r + (((inferior_realsequence seq) . n) + s) by A5, XREAL_1:8; then seq . (n + k) < (r + (((inferior_realsequence seq) . n) + s)) - ((inferior_realsequence seq) . n) by XREAL_1:20; hence ex k being Element of NAT st seq . (n + k) < r + s ; ::_thesis: verum end; hence for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ; ::_thesis: verum end; assume A6: for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ; ::_thesis: lim_inf seq <= r for s being real number st 0 < s holds lim_inf seq <= r + s proof let s be real number ; ::_thesis: ( 0 < s implies lim_inf seq <= r + s ) assume A7: 0 < s ; ::_thesis: lim_inf seq <= r + s for n being Element of NAT holds (inferior_realsequence seq) . n <= r + s proof let n be Element of NAT ; ::_thesis: (inferior_realsequence seq) . n <= r + s consider k being Element of NAT such that A8: seq . (n + k) < r + s by A6, A7; (inferior_realsequence seq) . n <= seq . (n + k) by A1, Th40; hence (inferior_realsequence seq) . n <= r + s by A8, XXREAL_0:2; ::_thesis: verum end; hence lim_inf seq <= r + s by Th9; ::_thesis: verum end; hence lim_inf seq <= r by XREAL_1:41; ::_thesis: verum end; theorem Th82: :: RINFSUP1:82 for r being real number for seq being Real_Sequence st seq is bounded holds ( r <= lim_inf seq iff for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds ( r <= lim_inf seq iff for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( r <= lim_inf seq iff for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ) set seq1 = inferior_realsequence seq; assume A1: seq is bounded ; ::_thesis: ( r <= lim_inf seq iff for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) then A2: inferior_realsequence seq is bounded by Th56; thus ( r <= lim_inf seq implies for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ::_thesis: ( ( for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) implies r <= lim_inf seq ) proof assume A3: r <= lim_inf seq ; ::_thesis: for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) assume A4: 0 < s ; ::_thesis: ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) proof consider n1 being Element of NAT such that A5: (inferior_realsequence seq) . n1 > (upper_bound (inferior_realsequence seq)) - s by A2, A4, Th7; ((inferior_realsequence seq) . n1) + (upper_bound (inferior_realsequence seq)) > r + ((upper_bound (inferior_realsequence seq)) - s) by A3, A5, XREAL_1:8; then ((inferior_realsequence seq) . n1) + (upper_bound (inferior_realsequence seq)) > (r - s) + (upper_bound (inferior_realsequence seq)) ; then A6: (((inferior_realsequence seq) . n1) + (upper_bound (inferior_realsequence seq))) - (upper_bound (inferior_realsequence seq)) > r - s by XREAL_1:20; now__::_thesis:_for_k_being_Element_of_NAT_holds_r_-_s_<_seq_._(n1_+_k) let k be Element of NAT ; ::_thesis: r - s < seq . (n1 + k) (inferior_realsequence seq) . n1 <= seq . (n1 + k) by A1, Th40; then (r - s) + ((inferior_realsequence seq) . n1) < (seq . (n1 + k)) + ((inferior_realsequence seq) . n1) by A6, XREAL_1:8; then ((r - s) + ((inferior_realsequence seq) . n1)) - ((inferior_realsequence seq) . n1) < seq . (n1 + k) by XREAL_1:19; hence r - s < seq . (n1 + k) ; ::_thesis: verum end; hence ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ; ::_thesis: verum end; hence ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ; ::_thesis: verum end; assume A7: for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ; ::_thesis: r <= lim_inf seq for s being real number st 0 < s holds r - s <= lim_inf seq proof let s be real number ; ::_thesis: ( 0 < s implies r - s <= lim_inf seq ) assume 0 < s ; ::_thesis: r - s <= lim_inf seq then consider n1 being Element of NAT such that A8: for k being Element of NAT holds r - s < seq . (n1 + k) by A7; for k being Element of NAT holds r - s <= seq . (n1 + k) by A8; then A9: r - s <= (inferior_realsequence seq) . n1 by A1, Th42; (inferior_realsequence seq) . n1 <= upper_bound (inferior_realsequence seq) by A2, Th7; hence r - s <= lim_inf seq by A9, XXREAL_0:2; ::_thesis: verum end; hence r <= lim_inf seq by XREAL_1:57; ::_thesis: verum end; theorem :: RINFSUP1:83 for r being real number for seq being Real_Sequence st seq is bounded holds ( r = lim_inf seq iff for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds ( r = lim_inf seq iff for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ) let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( r = lim_inf seq iff for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ) ) assume A1: seq is bounded ; ::_thesis: ( r = lim_inf seq iff for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ) hence ( r = lim_inf seq implies for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ) by Th81, Th82; ::_thesis: ( ( for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ) implies r = lim_inf seq ) assume A2: for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s ) & ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ) ; ::_thesis: r = lim_inf seq then for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds r - s < seq . (n + k) ; then A3: r <= lim_inf seq by A1, Th82; for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) < r + s by A2; then lim_inf seq <= r by A1, Th81; hence r = lim_inf seq by A3, XXREAL_0:1; ::_thesis: verum end; theorem Th84: :: RINFSUP1:84 for r being real number for seq being Real_Sequence st seq is bounded holds ( r <= lim_sup seq iff for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds ( r <= lim_sup seq iff for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( r <= lim_sup seq iff for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) ) set seq1 = superior_realsequence seq; assume A1: seq is bounded ; ::_thesis: ( r <= lim_sup seq iff for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) then A2: superior_realsequence seq is bounded by Th56; thus ( r <= lim_sup seq implies for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) ::_thesis: ( ( for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) implies r <= lim_sup seq ) proof assume A3: r <= lim_sup seq ; ::_thesis: for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s let s be real number ; ::_thesis: ( 0 < s implies for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) assume A4: 0 < s ; ::_thesis: for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s proof let n be Element of NAT ; ::_thesis: ex k being Element of NAT st seq . (n + k) > r - s consider k being Element of NAT such that A5: seq . (n + k) > ((superior_realsequence seq) . n) - s by A1, A4, Th41; (superior_realsequence seq) . n >= r by A2, A3, Th10; then ((superior_realsequence seq) . n) + (seq . (n + k)) > r + (((superior_realsequence seq) . n) - s) by A5, XREAL_1:8; then seq . (n + k) > ((r + ((superior_realsequence seq) . n)) - s) - ((superior_realsequence seq) . n) by XREAL_1:19; hence ex k being Element of NAT st seq . (n + k) > r - s ; ::_thesis: verum end; hence for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ; ::_thesis: verum end; assume A6: for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ; ::_thesis: r <= lim_sup seq for s being real number st 0 < s holds lim_sup seq >= r - s proof let s be real number ; ::_thesis: ( 0 < s implies lim_sup seq >= r - s ) assume A7: 0 < s ; ::_thesis: lim_sup seq >= r - s for n being Element of NAT holds r - s <= (superior_realsequence seq) . n proof let n be Element of NAT ; ::_thesis: r - s <= (superior_realsequence seq) . n consider k being Element of NAT such that A8: r - s < seq . (n + k) by A6, A7; seq . (n + k) <= (superior_realsequence seq) . n by A1, Th41; hence r - s <= (superior_realsequence seq) . n by A8, XXREAL_0:2; ::_thesis: verum end; hence lim_sup seq >= r - s by Th10; ::_thesis: verum end; hence r <= lim_sup seq by XREAL_1:57; ::_thesis: verum end; theorem Th85: :: RINFSUP1:85 for r being real number for seq being Real_Sequence st seq is bounded holds ( lim_sup seq <= r iff for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds ( lim_sup seq <= r iff for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( lim_sup seq <= r iff for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ) set seq1 = superior_realsequence seq; assume A1: seq is bounded ; ::_thesis: ( lim_sup seq <= r iff for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) then A2: superior_realsequence seq is bounded by Th56; thus ( lim_sup seq <= r implies for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ::_thesis: ( ( for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) implies lim_sup seq <= r ) proof assume A3: lim_sup seq <= r ; ::_thesis: for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s proof let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) assume A4: 0 < s ; ::_thesis: ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s proof consider n1 being Element of NAT such that A5: (superior_realsequence seq) . n1 < (lower_bound (superior_realsequence seq)) + s by A2, A4, Th8; ((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq)) < r + ((lower_bound (superior_realsequence seq)) + s) by A3, A5, XREAL_1:8; then ((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq)) < (r + s) + (lower_bound (superior_realsequence seq)) ; then A6: (((superior_realsequence seq) . n1) + (lower_bound (superior_realsequence seq))) - (lower_bound (superior_realsequence seq)) < r + s by XREAL_1:19; now__::_thesis:_for_k_being_Element_of_NAT_holds_seq_._(n1_+_k)_<_r_+_s let k be Element of NAT ; ::_thesis: seq . (n1 + k) < r + s seq . (n1 + k) <= (superior_realsequence seq) . n1 by A1, Th41; then (seq . (n1 + k)) + ((superior_realsequence seq) . n1) < (r + s) + ((superior_realsequence seq) . n1) by A6, XREAL_1:8; then ((seq . (n1 + k)) + ((superior_realsequence seq) . n1)) - ((superior_realsequence seq) . n1) < r + s by XREAL_1:19; hence seq . (n1 + k) < r + s ; ::_thesis: verum end; hence ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ; ::_thesis: verum end; hence ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ; ::_thesis: verum end; hence for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ; ::_thesis: verum end; assume A7: for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ; ::_thesis: lim_sup seq <= r for s being real number st 0 < s holds lim_sup seq <= r + s proof let s be real number ; ::_thesis: ( 0 < s implies lim_sup seq <= r + s ) assume 0 < s ; ::_thesis: lim_sup seq <= r + s then consider n1 being Element of NAT such that A8: for k being Element of NAT holds seq . (n1 + k) < r + s by A7; for k being Element of NAT holds seq . (n1 + k) <= r + s by A8; then A9: (superior_realsequence seq) . n1 <= r + s by A1, Th44; lower_bound (superior_realsequence seq) <= (superior_realsequence seq) . n1 by A2, Th8; hence lim_sup seq <= r + s by A9, XXREAL_0:2; ::_thesis: verum end; hence lim_sup seq <= r by XREAL_1:41; ::_thesis: verum end; theorem :: RINFSUP1:86 for r being real number for seq being Real_Sequence st seq is bounded holds ( r = lim_sup seq iff for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ) proof let r be real number ; ::_thesis: for seq being Real_Sequence st seq is bounded holds ( r = lim_sup seq iff for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ) let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( r = lim_sup seq iff for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ) ) assume A1: seq is bounded ; ::_thesis: ( r = lim_sup seq iff for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ) hence ( r = lim_sup seq implies for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ) by Th84, Th85; ::_thesis: ( ( for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ) implies r = lim_sup seq ) assume A2: for s being real number st 0 < s holds ( ( for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s ) & ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ) ; ::_thesis: r = lim_sup seq then for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds seq . (n + k) < r + s ; then A3: lim_sup seq <= r by A1, Th85; for s being real number st 0 < s holds for n being Element of NAT ex k being Element of NAT st seq . (n + k) > r - s by A2; then r <= lim_sup seq by A1, Th84; hence r = lim_sup seq by A3, XXREAL_0:1; ::_thesis: verum end; theorem :: RINFSUP1:87 for seq being Real_Sequence st seq is bounded holds lim_inf seq <= lim_sup seq by Th55; theorem Th88: :: RINFSUP1:88 for seq being Real_Sequence holds ( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent ) proof let seq be Real_Sequence; ::_thesis: ( ( seq is bounded & lim_sup seq = lim_inf seq ) iff seq is convergent ) thus ( seq is bounded & lim_sup seq = lim_inf seq implies seq is convergent ) ::_thesis: ( seq is convergent implies ( seq is bounded & lim_sup seq = lim_inf seq ) ) proof reconsider r = lower_bound (superior_realsequence seq) as real number ; assume that A1: seq is bounded and A2: lim_sup seq = lim_inf seq ; ::_thesis: seq is convergent A3: inferior_realsequence seq is bounded by A1, Th56; A4: inferior_realsequence seq is V48() by A1, Th50; A5: superior_realsequence seq is V49() by A1, Th51; A6: superior_realsequence seq is bounded by A1, Th56; for s being real number st 0 < s holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < s proof let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < s ) assume A7: 0 < s ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < s consider k2 being Element of NAT such that A8: (superior_realsequence seq) . k2 < r + s by A6, A7, Th8; consider k1 being Element of NAT such that A9: r - s < (inferior_realsequence seq) . k1 by A2, A3, A7, Th7; reconsider k = max (k1,k2) as Element of NAT ; 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 being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < s proof take k ; ::_thesis: for m being Element of NAT st k <= m holds abs ((seq . m) - r) < s let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((seq . m) - r) < s ) assume k <= m ; ::_thesis: abs ((seq . m) - r) < s then consider k3 being Nat such that A12: m = k + k3 by NAT_1:10; A13: k3 in NAT by ORDINAL1:def_12; then seq . m <= (superior_realsequence seq) . k by A1, A12, Th41; then seq . m <= (superior_realsequence seq) . k2 by A10, XXREAL_0:2; then A14: seq . m < r + s by A8, XXREAL_0:2; (inferior_realsequence seq) . k <= seq . m by A1, A12, A13, Th40; then (inferior_realsequence seq) . k1 <= seq . m by A11, XXREAL_0:2; then r - s < seq . m by A9, XXREAL_0:2; hence abs ((seq . m) - r) < s by A14, Th1; ::_thesis: verum end; hence ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < s ; ::_thesis: verum end; hence seq is convergent by SEQ_2:def_6; ::_thesis: verum end; assume A15: seq is convergent ; ::_thesis: ( seq is bounded & lim_sup seq = lim_inf seq ) then consider r being real number such that A16: for p being real number st 0 < p holds ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - r) < p by SEQ_2:def_6; A17: seq is bounded by A15; A18: for p being real number st 0 < p holds ex n being Element of NAT st ( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st ( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) ) assume 0 < p ; ::_thesis: ex n being Element of NAT st ( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) then consider n being Element of NAT such that A19: for m being Element of NAT st n <= m holds abs ((seq . m) - r) < p by A16; A20: for m being Element of NAT st n <= m holds ( r - p <= seq . m & seq . m <= r + p ) proof let m be Element of NAT ; ::_thesis: ( n <= m implies ( r - p <= seq . m & seq . m <= r + p ) ) assume n <= m ; ::_thesis: ( r - p <= seq . m & seq . m <= r + p ) then abs ((seq . m) - r) < p by A19; hence ( r - p <= seq . m & seq . m <= r + p ) by Th1; ::_thesis: verum end; then for m being Element of NAT st n <= m holds seq . m <= r + p ; then A21: (superior_realsequence seq) . n <= r + p by A17, Th45; for m being Element of NAT st n <= m holds r - p <= seq . m by A20; then r - p <= (inferior_realsequence seq) . n by A17, Th43; hence ex n being Element of NAT st ( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) by A21; ::_thesis: verum end; A22: ( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A17, Th56; A23: for p being real number st 0 < p holds ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) proof let p be real number ; ::_thesis: ( 0 < p implies ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) ) assume 0 < p ; ::_thesis: ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) then consider n being Element of NAT such that A24: ( r - p <= (inferior_realsequence seq) . n & (superior_realsequence seq) . n <= r + p ) by A18; ( (inferior_realsequence seq) . n <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= (superior_realsequence seq) . n ) by A22, Th7, Th8; hence ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) by A24, XXREAL_0:2; ::_thesis: verum end; reconsider r = r as Real by XREAL_0:def_1; A25: for p being real number st 0 < p holds lower_bound (superior_realsequence seq) <= r + p by A23; then A26: lower_bound (superior_realsequence seq) <= r by XREAL_1:41; for p being real number st 0 < p holds r <= (upper_bound (inferior_realsequence seq)) + p proof let p be real number ; ::_thesis: ( 0 < p implies r <= (upper_bound (inferior_realsequence seq)) + p ) assume 0 < p ; ::_thesis: r <= (upper_bound (inferior_realsequence seq)) + p then r - p <= upper_bound (inferior_realsequence seq) by A23; hence r <= (upper_bound (inferior_realsequence seq)) + p by XREAL_1:20; ::_thesis: verum end; then A27: r <= upper_bound (inferior_realsequence seq) by XREAL_1:41; A28: upper_bound (inferior_realsequence seq) <= lower_bound (superior_realsequence seq) by A15, Th55; lower_bound (superior_realsequence seq) <= r by A25, XREAL_1:41; then upper_bound (inferior_realsequence seq) <= r by A28, XXREAL_0:2; then r = upper_bound (inferior_realsequence seq) by A27, XXREAL_0:1; hence ( seq is bounded & lim_sup seq = lim_inf seq ) by A15, A28, A26, XXREAL_0:1; ::_thesis: verum end; theorem :: RINFSUP1:89 for seq being Real_Sequence st seq is convergent holds ( lim seq = lim_sup seq & lim seq = lim_inf seq ) proof let seq be Real_Sequence; ::_thesis: ( seq is convergent implies ( lim seq = lim_sup seq & lim seq = lim_inf seq ) ) reconsider r = lim seq as real number ; assume A1: seq is convergent ; ::_thesis: ( lim seq = lim_sup seq & lim seq = lim_inf seq ) 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 being real number st 0 < p holds ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) proof let p be real number ; ::_thesis: ( 0 < p implies ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) ) assume 0 < p ; ::_thesis: ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) then consider k being Element of NAT such that A6: for m being Element of NAT st k <= m holds abs ((seq . m) - r) < p by A1, SEQ_2:def_7; A7: for m being Element of NAT st k <= m holds ( r - p <= seq . m & seq . m <= r + p ) proof let m be Element of NAT ; ::_thesis: ( k <= m implies ( r - p <= seq . m & seq . m <= r + p ) ) assume k <= m ; ::_thesis: ( r - p <= seq . m & seq . m <= r + p ) then abs ((seq . m) - r) < p by A6; hence ( r - p <= seq . m & seq . m <= r + p ) by Th1; ::_thesis: verum end; then for m being Element of NAT st k <= m holds r - p <= seq . m ; then A8: r - p <= (inferior_realsequence seq) . k by A3, Th43; for m being Element of NAT 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 ( r - p <= upper_bound (inferior_realsequence seq) & lower_bound (superior_realsequence seq) <= r + p ) by A8, A9, XXREAL_0:2; ::_thesis: verum end; A10: for p being real number st 0 < p holds r <= (upper_bound (inferior_realsequence seq)) + p proof let p be real number ; ::_thesis: ( 0 < p implies r <= (upper_bound (inferior_realsequence seq)) + p ) assume 0 < p ; ::_thesis: r <= (upper_bound (inferior_realsequence seq)) + p then r - p <= upper_bound (inferior_realsequence seq) by A5; hence r <= (upper_bound (inferior_realsequence seq)) + p by XREAL_1:20; ::_thesis: verum 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 being real number st 0 < p holds 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 ( lim seq = lim_sup seq & lim seq = lim_inf seq ) by A13, A11, A12, XXREAL_0:1; ::_thesis: verum end; theorem Th90: :: RINFSUP1:90 for seq being Real_Sequence st seq is bounded holds ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) proof let seq be Real_Sequence; ::_thesis: ( seq is bounded implies ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) ) assume A1: seq is bounded ; ::_thesis: ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) 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 ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) by A2; ::_thesis: verum end; theorem :: RINFSUP1:91 for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) implies ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) ) assume that A1: seq1 is bounded and A2: seq2 is bounded and A3: for n being Element of NAT holds seq1 . n <= seq2 . n ; ::_thesis: ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) 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 being Element of NAT holds (superior_realsequence seq1) . n <= (superior_realsequence seq2) . n ) & ( for n being Element of NAT holds (inferior_realsequence seq1) . n <= (inferior_realsequence seq2) . n ) ) by A1, A2, A3, Th75; hence ( lim_sup seq1 <= lim_sup seq2 & lim_inf seq1 <= lim_inf seq2 ) by A4, A8, A7, A6, A5, A9, SEQ_2:18; ::_thesis: verum end; theorem :: RINFSUP1:92 for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds ( (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 let seq1, seq2 be Real_Sequence; ::_thesis: ( 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) ) ) ) ) assume A1: ( seq1 is bounded & seq2 is bounded ) ; ::_thesis: ( (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) ) ) ) A2: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) ) set r1 = lim_sup seq1; set r2 = lim_sup seq2; assume that A3: seq1 is bounded and A4: seq2 is bounded ; ::_thesis: lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s proof let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st for k being Element of NAT holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s ) assume 0 < s ; ::_thesis: ex n being Element of NAT st for k being Element of NAT holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s then A5: 0 < s / 2 by XREAL_1:215; then consider n1 being Element of NAT such that A6: for k being Element of NAT holds seq1 . (n1 + k) < (lim_sup seq1) + (s / 2) by A3, Th85; consider n2 being Element of NAT such that A7: for k being Element of NAT holds seq2 . (n2 + k) < (lim_sup seq2) + (s / 2) by A4, A5, Th85; for k being Element of NAT holds (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s proof let k be Element of NAT ; ::_thesis: (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s ( seq1 . (n1 + (n2 + k)) < (lim_sup seq1) + (s / 2) & seq2 . (n2 + (n1 + k)) < (lim_sup seq2) + (s / 2) ) by A6, A7; then (seq1 . ((n1 + n2) + k)) + (seq2 . ((n1 + n2) + k)) < ((lim_sup seq1) + (s / 2)) + ((lim_sup seq2) + (s / 2)) by XREAL_1:8; hence (seq1 + seq2) . ((n1 + n2) + k) < ((lim_sup seq1) + (lim_sup seq2)) + s by SEQ_1:7; ::_thesis: verum end; hence ex n being Element of NAT st for k being Element of NAT holds (seq1 + seq2) . (n + k) < ((lim_sup seq1) + (lim_sup seq2)) + s ; ::_thesis: verum end; hence lim_sup (seq1 + seq2) <= (lim_sup seq1) + (lim_sup seq2) by A3, A4, Th85; ::_thesis: verum end; A8: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) ) assume that A9: seq1 is bounded and A10: seq2 is bounded ; ::_thesis: (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) 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 (lim_inf seq1) + (lim_sup seq2) <= lim_sup (seq1 + seq2) by XREAL_1:19; ::_thesis: verum 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 being Real_Sequence st seq1 is bounded & seq2 is bounded holds (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) ) set r1 = lim_inf seq1; set r2 = lim_inf seq2; assume that A15: seq1 is bounded and A16: seq2 is bounded ; ::_thesis: (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) for s being real number st 0 < s holds ex n being Element of NAT st for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k) proof let s be real number ; ::_thesis: ( 0 < s implies ex n being Element of NAT st for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k) ) assume 0 < s ; ::_thesis: ex n being Element of NAT st for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k) then A17: 0 < s / 2 by XREAL_1:215; then consider n1 being Element of NAT such that A18: for k being Element of NAT holds (lim_inf seq1) - (s / 2) < seq1 . (n1 + k) by A15, Th82; consider n2 being Element of NAT such that A19: for k being Element of NAT holds (lim_inf seq2) - (s / 2) < seq2 . (n2 + k) by A16, A17, Th82; for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k) proof let k be Element of NAT ; ::_thesis: ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k) ( (lim_inf seq1) - (s / 2) < seq1 . (n1 + (n2 + k)) & (lim_inf seq2) - (s / 2) < seq2 . (n2 + (n1 + k)) ) by A18, A19; then ((lim_inf seq1) - (s / 2)) + ((lim_inf seq2) - (s / 2)) < (seq1 . ((n1 + n2) + k)) + (seq2 . ((n1 + n2) + k)) by XREAL_1:8; hence ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . ((n1 + n2) + k) by SEQ_1:7; ::_thesis: verum end; hence ex n being Element of NAT st for k being Element of NAT holds ((lim_inf seq1) + (lim_inf seq2)) - s < (seq1 + seq2) . (n + k) ; ::_thesis: verum end; hence (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) by A15, A16, Th82; ::_thesis: verum end; then A20: (lim_inf seq1) + (lim_inf seq2) <= lim_inf (seq1 + seq2) by A1; A21: for seq1, seq2 being Real_Sequence st seq1 is bounded & seq2 is bounded holds lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq2 is bounded implies lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) ) assume that A22: seq1 is bounded and A23: seq2 is bounded ; ::_thesis: lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) 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 lim_inf (seq1 + seq2) <= (lim_inf seq1) + (lim_sup seq2) by XREAL_1:20; ::_thesis: verum 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 ) ; ::_thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) percases ( seq1 is convergent or seq2 is convergent ) by A26; suppose seq1 is convergent ; ::_thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) then lim_inf seq1 = lim_sup seq1 by Th88; hence ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) by A20, A24, A11, A13, XXREAL_0:1; ::_thesis: verum end; suppose seq2 is convergent ; ::_thesis: ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) then lim_inf seq2 = lim_sup seq2 by Th88; hence ( lim_inf (seq1 + seq2) = (lim_inf seq1) + (lim_inf seq2) & lim_sup (seq1 + seq2) = (lim_sup seq1) + (lim_sup seq2) ) by A20, A25, A12, A13, XXREAL_0:1; ::_thesis: verum end; end; end; hence ( (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) ) ) ) by A14, A21, A2, A8, A1; ::_thesis: verum end; theorem :: RINFSUP1:93 for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) ) A1: for seq1, seq2 being Real_Sequence 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 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) assume that A2: ( seq1 is bounded & seq1 is nonnegative ) and A3: ( seq2 is bounded & seq2 is nonnegative ) ; ::_thesis: lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) set seq3 = superior_realsequence seq1; set seq4 = superior_realsequence seq2; set seq5 = superior_realsequence (seq1 (#) seq2); A4: superior_realsequence (seq1 (#) seq2) is convergent by A2, A3, Th58; A5: ( lower_bound (superior_realsequence (seq1 (#) seq2)) = lim (superior_realsequence (seq1 (#) seq2)) & lower_bound (superior_realsequence seq1) = lim (superior_realsequence seq1) ) by A2, A3, Th58; A6: lower_bound (superior_realsequence seq2) = lim (superior_realsequence seq2) by A3, Th58; A7: for n being Element of NAT holds (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n proof let n be Element of NAT ; ::_thesis: (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) . n) * ((superior_realsequence seq2) . n) by A2, A3, Th80; hence (superior_realsequence (seq1 (#) seq2)) . n <= ((superior_realsequence seq1) (#) (superior_realsequence seq2)) . n by SEQ_1:8; ::_thesis: verum end; A8: ( superior_realsequence seq1 is convergent & superior_realsequence seq2 is convergent ) by A2, A3, Th58; then (superior_realsequence seq1) (#) (superior_realsequence seq2) is convergent ; then lim (superior_realsequence (seq1 (#) seq2)) <= lim ((superior_realsequence seq1) (#) (superior_realsequence seq2)) by A4, A7, SEQ_2:18; hence lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) by A8, A5, A6, SEQ_2:15; ::_thesis: verum end; for seq1, seq2 being Real_Sequence st seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative holds (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) proof let seq1, seq2 be Real_Sequence; ::_thesis: ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) ) assume that A9: ( seq1 is bounded & seq1 is nonnegative ) and A10: ( seq2 is bounded & seq2 is nonnegative ) ; ::_thesis: (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) set seq3 = inferior_realsequence seq1; set seq4 = inferior_realsequence seq2; set seq5 = inferior_realsequence (seq1 (#) seq2); A11: inferior_realsequence (seq1 (#) seq2) is convergent by A9, A10, Th57; A12: ( upper_bound (inferior_realsequence (seq1 (#) seq2)) = lim (inferior_realsequence (seq1 (#) seq2)) & upper_bound (inferior_realsequence seq1) = lim (inferior_realsequence seq1) ) by A9, A10, Th57; A13: upper_bound (inferior_realsequence seq2) = lim (inferior_realsequence seq2) by A10, Th57; A14: for n being Element of NAT holds (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n proof let n be Element of NAT ; ::_thesis: (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) . n) * ((inferior_realsequence seq2) . n) by A9, A10, Th79; hence (inferior_realsequence (seq1 (#) seq2)) . n >= ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) . n by SEQ_1:8; ::_thesis: verum end; A15: ( inferior_realsequence seq1 is convergent & inferior_realsequence seq2 is convergent ) by A9, A10, Th57; then (inferior_realsequence seq1) (#) (inferior_realsequence seq2) is convergent ; then lim (inferior_realsequence (seq1 (#) seq2)) >= lim ((inferior_realsequence seq1) (#) (inferior_realsequence seq2)) by A11, A14, SEQ_2:18; hence (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) by A15, A12, A13, SEQ_2:15; ::_thesis: verum end; hence ( seq1 is bounded & seq1 is nonnegative & seq2 is bounded & seq2 is nonnegative implies ( (lim_inf seq1) * (lim_inf seq2) <= lim_inf (seq1 (#) seq2) & lim_sup (seq1 (#) seq2) <= (lim_sup seq1) * (lim_sup seq2) ) ) by A1; ::_thesis: verum end;