:: RINFSUP2 semantic presentation begin theorem Th1: :: RINFSUP2:1 for X being non empty Subset of ExtREAL for Y being non empty Subset of REAL st X = Y & Y is bounded_above holds ( X is bounded_above & sup X = upper_bound Y ) proof let X be non empty Subset of ExtREAL; ::_thesis: for Y being non empty Subset of REAL st X = Y & Y is bounded_above holds ( X is bounded_above & sup X = upper_bound Y ) let Y be non empty Subset of REAL; ::_thesis: ( X = Y & Y is bounded_above implies ( X is bounded_above & sup X = upper_bound Y ) ) assume that A1: X = Y and A2: Y is bounded_above ; ::_thesis: ( X is bounded_above & sup X = upper_bound Y ) A3: for s being real number st s in Y holds s <= sup X by A1, XXREAL_2:4; not -infty in X by A1; then A4: X <> {-infty} by TARSKI:def_1; for r being ext-real number st r in X holds r <= upper_bound Y by A1, A2, SEQ_4:def_1; then A5: upper_bound Y is UpperBound of X by XXREAL_2:def_1; hence X is bounded_above by XXREAL_2:def_10; ::_thesis: sup X = upper_bound Y then sup X in REAL by A4, XXREAL_2:57; then A6: upper_bound Y <= sup X by A3, SEQ_4:45; sup X <= upper_bound Y by A5, XXREAL_2:def_3; hence sup X = upper_bound Y by A6, XXREAL_0:1; ::_thesis: verum end; theorem :: RINFSUP2:2 for X being non empty Subset of ExtREAL for Y being non empty Subset of REAL st X = Y & X is bounded_above holds ( Y is bounded_above & sup X = upper_bound Y ) by Th1; theorem Th3: :: RINFSUP2:3 for X being non empty Subset of ExtREAL for Y being non empty Subset of REAL st X = Y & Y is bounded_below holds ( X is bounded_below & inf X = lower_bound Y ) proof let X be non empty Subset of ExtREAL; ::_thesis: for Y being non empty Subset of REAL st X = Y & Y is bounded_below holds ( X is bounded_below & inf X = lower_bound Y ) let Y be non empty Subset of REAL; ::_thesis: ( X = Y & Y is bounded_below implies ( X is bounded_below & inf X = lower_bound Y ) ) assume that A1: X = Y and A2: Y is bounded_below ; ::_thesis: ( X is bounded_below & inf X = lower_bound Y ) A3: for s being real number st s in Y holds inf X <= s by A1, XXREAL_2:3; not +infty in X by A1; then A4: X <> {+infty} by TARSKI:def_1; for r being ext-real number st r in X holds lower_bound Y <= r by A1, A2, SEQ_4:def_2; then A5: lower_bound Y is LowerBound of X by XXREAL_2:def_2; hence X is bounded_below by XXREAL_2:def_9; ::_thesis: inf X = lower_bound Y then inf X in REAL by A4, XXREAL_2:58; then A6: inf X <= lower_bound Y by A3, SEQ_4:43; lower_bound Y <= inf X by A5, XXREAL_2:def_4; hence inf X = lower_bound Y by A6, XXREAL_0:1; ::_thesis: verum end; theorem :: RINFSUP2:4 for X being non empty Subset of ExtREAL for Y being non empty Subset of REAL st X = Y & X is bounded_below holds ( Y is bounded_below & inf X = lower_bound Y ) by Th3; definition let seq be ExtREAL_sequence; func sup seq -> Element of ExtREAL equals :: RINFSUP2:def 1 sup (rng seq); coherence sup (rng seq) is Element of ExtREAL ; func inf seq -> Element of ExtREAL equals :: RINFSUP2:def 2 inf (rng seq); coherence inf (rng seq) is Element of ExtREAL ; end; :: deftheorem defines sup RINFSUP2:def_1_:_ for seq being ExtREAL_sequence holds sup seq = sup (rng seq); :: deftheorem defines inf RINFSUP2:def_2_:_ for seq being ExtREAL_sequence holds inf seq = inf (rng seq); definition let seq be ExtREAL_sequence; attrseq is bounded_below means :Def3: :: RINFSUP2:def 3 rng seq is bounded_below ; attrseq is bounded_above means :Def4: :: RINFSUP2:def 4 rng seq is bounded_above ; end; :: deftheorem Def3 defines bounded_below RINFSUP2:def_3_:_ for seq being ExtREAL_sequence holds ( seq is bounded_below iff rng seq is bounded_below ); :: deftheorem Def4 defines bounded_above RINFSUP2:def_4_:_ for seq being ExtREAL_sequence holds ( seq is bounded_above iff rng seq is bounded_above ); definition let seq be ExtREAL_sequence; attrseq is bounded means :Def5: :: RINFSUP2:def 5 ( seq is bounded_above & seq is bounded_below ); end; :: deftheorem Def5 defines bounded RINFSUP2:def_5_:_ for seq being ExtREAL_sequence holds ( seq is bounded iff ( seq is bounded_above & seq is bounded_below ) ); theorem Th5: :: RINFSUP2:5 for seq being ExtREAL_sequence for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL proof let seq be ExtREAL_sequence; ::_thesis: for n being Element of NAT holds { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL let n be Element of NAT ; ::_thesis: { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL deffunc H1( Element of NAT ) -> Element of ExtREAL = seq . $1; defpred S1[ Element of NAT ] means n <= $1; set Y = { H1(k) where k is Element of NAT : S1[k] } ; A1: seq . n in { H1(k) where k is Element of NAT : S1[k] } ; { H1(k) where k is Element of NAT : S1[k] } is Subset of ExtREAL from DOMAIN_1:sch_8(); hence { (seq . k) where k is Element of NAT : n <= k } is non empty Subset of ExtREAL by A1; ::_thesis: verum end; definition let seq be ExtREAL_sequence; func inferior_realsequence seq -> ExtREAL_sequence means :Def6: :: RINFSUP2:def 6 for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & it . n = inf Y ); existence ex b1 being ExtREAL_sequence st for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & b1 . n = inf Y ) proof defpred S1[ Element of NAT , Element of ExtREAL ] means ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : $1 <= k } & $2 = inf Y ); A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S1[n,y] reconsider Y = { (seq . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by Th5; reconsider y = inf Y as Element of ExtREAL ; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; thus ex f being Function of NAT,ExtREAL st for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being ExtREAL_sequence st ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & b1 . n = inf Y ) ) & ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & b2 . n = inf Y ) ) holds b1 = b2 proof let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = inf Y ) ) & ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = inf Y ) ) implies seq1 = seq2 ) assume that A2: for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = inf Y ) and A3: for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = inf 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 n = y as Element of NAT ; A5: ex Z being non empty Subset of ExtREAL st ( Z = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = inf Z ) by A3; ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = inf Y ) by A2; hence seq1 . y = seq2 . y by A5; ::_thesis: verum end; A6: NAT = dom seq2 by FUNCT_2:def_1; NAT = dom seq1 by FUNCT_2:def_1; hence seq1 = seq2 by A4, A6, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def6 defines inferior_realsequence RINFSUP2:def_6_:_ for seq, b2 being ExtREAL_sequence holds ( b2 = inferior_realsequence seq iff for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & b2 . n = inf Y ) ); definition let seq be ExtREAL_sequence; func superior_realsequence seq -> ExtREAL_sequence means :Def7: :: RINFSUP2:def 7 for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & it . n = sup Y ); existence ex b1 being ExtREAL_sequence st for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & b1 . n = sup Y ) proof defpred S1[ Element of NAT , Element of ExtREAL ] means ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : $1 <= k } & $2 = sup Y ); A1: for n being Element of NAT ex y being Element of ExtREAL st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of ExtREAL st S1[n,y] reconsider Y = { (seq . k) where k is Element of NAT : n <= k } as non empty Subset of ExtREAL by Th5; reconsider y = sup Y as Element of ExtREAL ; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; thus ex f being Function of NAT,ExtREAL st for n being Element of NAT holds S1[n,f . n] from FUNCT_2:sch_3(A1); ::_thesis: verum end; uniqueness for b1, b2 being ExtREAL_sequence st ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & b1 . n = sup Y ) ) & ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & b2 . n = sup Y ) ) holds b1 = b2 proof let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = sup Y ) ) & ( for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = sup Y ) ) implies seq1 = seq2 ) assume that A2: for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = sup Y ) and A3: for m being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : m <= k } & seq2 . m = sup 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 n = y as Element of NAT ; A5: ex Z being non empty Subset of ExtREAL st ( Z = { (seq . k) where k is Element of NAT : n <= k } & seq2 . n = sup Z ) by A3; ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & seq1 . n = sup Y ) by A2; hence seq1 . y = seq2 . y by A5; ::_thesis: verum end; A6: NAT = dom seq2 by FUNCT_2:def_1; NAT = dom seq1 by FUNCT_2:def_1; hence seq1 = seq2 by A4, A6, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def7 defines superior_realsequence RINFSUP2:def_7_:_ for seq, b2 being ExtREAL_sequence holds ( b2 = superior_realsequence seq iff for n being Element of NAT ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & b2 . n = sup Y ) ); theorem :: RINFSUP2:6 for seq being ExtREAL_sequence st seq is real-valued holds seq is Real_Sequence proof let seq be ExtREAL_sequence; ::_thesis: ( seq is real-valued implies seq is Real_Sequence ) assume seq is real-valued ; ::_thesis: seq is Real_Sequence then rng seq is Subset of REAL by MESFUNC2:32; hence seq is Real_Sequence by FUNCT_2:6; ::_thesis: verum end; theorem Th7: :: RINFSUP2:7 for seq being ExtREAL_sequence holds ( ( seq is increasing implies for n, m being Element of NAT st m < n holds seq . m < seq . n ) & ( ( for n, m being Element of NAT st m < n holds seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds seq . n <= seq . m ) implies seq is non-increasing ) ) proof let seq be ExtREAL_sequence; ::_thesis: ( ( seq is increasing implies for n, m being Element of NAT st m < n holds seq . m < seq . n ) & ( ( for n, m being Element of NAT st m < n holds seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds seq . n <= seq . m ) implies seq is non-increasing ) ) A1: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds seq . m < seq . n ) implies seq is increasing ) proof assume A2: for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds seq . m < seq . n ; ::_thesis: seq is increasing let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for b1 being set holds ( not e1 in K86(seq) or not b1 in K86(seq) or b1 <= e1 or not K68(seq,b1) <= K68(seq,e1) ) let e2 be ext-real number ; ::_thesis: ( not e1 in K86(seq) or not e2 in K86(seq) or e2 <= e1 or not K68(seq,e2) <= K68(seq,e1) ) thus ( not e1 in K86(seq) or not e2 in K86(seq) or e2 <= e1 or not K68(seq,e2) <= K68(seq,e1) ) by A2; ::_thesis: verum end; A3: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds seq . m > seq . n ) implies seq is decreasing ) proof assume A4: for m, n being Element of NAT st m in dom seq & n in dom seq & m < n holds seq . m > seq . n ; ::_thesis: seq is decreasing let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for b1 being set holds ( not e1 in K86(seq) or not b1 in K86(seq) or b1 <= e1 or not K68(seq,e1) <= K68(seq,b1) ) let e2 be ext-real number ; ::_thesis: ( not e1 in K86(seq) or not e2 in K86(seq) or e2 <= e1 or not K68(seq,e1) <= K68(seq,e2) ) thus ( not e1 in K86(seq) or not e2 in K86(seq) or e2 <= e1 or not K68(seq,e1) <= K68(seq,e2) ) by A4; ::_thesis: verum end; A5: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds seq . m <= seq . n ) implies seq is non-decreasing ) proof assume A6: for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds seq . m <= seq . n ; ::_thesis: seq is non-decreasing let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for b1 being set holds ( not e1 in K86(seq) or not b1 in K86(seq) or not e1 <= b1 or K68(seq,e1) <= K68(seq,b1) ) let e2 be ext-real number ; ::_thesis: ( not e1 in K86(seq) or not e2 in K86(seq) or not e1 <= e2 or K68(seq,e1) <= K68(seq,e2) ) thus ( not e1 in K86(seq) or not e2 in K86(seq) or not e1 <= e2 or K68(seq,e1) <= K68(seq,e2) ) by A6; ::_thesis: verum end; A7: ( ( for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds seq . m >= seq . n ) implies seq is non-increasing ) proof assume A8: for m, n being Element of NAT st m in dom seq & n in dom seq & m <= n holds seq . m >= seq . n ; ::_thesis: seq is non-increasing let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for b1 being set holds ( not e1 in K86(seq) or not b1 in K86(seq) or not e1 <= b1 or K68(seq,b1) <= K68(seq,e1) ) let e2 be ext-real number ; ::_thesis: ( not e1 in K86(seq) or not e2 in K86(seq) or not e1 <= e2 or K68(seq,e2) <= K68(seq,e1) ) thus ( not e1 in K86(seq) or not e2 in K86(seq) or not e1 <= e2 or K68(seq,e2) <= K68(seq,e1) ) by A8; ::_thesis: verum end; dom seq = NAT by FUNCT_2:def_1; hence ( ( seq is increasing implies for n, m being Element of NAT st m < n holds seq . m < seq . n ) & ( ( for n, m being Element of NAT st m < n holds seq . m < seq . n ) implies seq is increasing ) & ( seq is decreasing implies for n, m being Element of NAT st m < n holds seq . n < seq . m ) & ( ( for n, m being Element of NAT st m < n holds seq . n < seq . m ) implies seq is decreasing ) & ( seq is non-decreasing implies for n, m being Element of NAT st m <= n holds seq . m <= seq . n ) & ( ( for n, m being Element of NAT st m <= n holds seq . m <= seq . n ) implies seq is non-decreasing ) & ( seq is non-increasing implies for n, m being Element of NAT st m <= n holds seq . n <= seq . m ) & ( ( for n, m being Element of NAT st m <= n holds seq . n <= seq . m ) implies seq is non-increasing ) ) by A1, A3, A7, A5, VALUED_0:def_13, VALUED_0:def_14, VALUED_0:def_15, VALUED_0:def_16; ::_thesis: verum end; theorem Th8: :: RINFSUP2:8 for n being Element of NAT for seq being ExtREAL_sequence holds ( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n ) proof let n be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence holds ( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n ) let seq be ExtREAL_sequence; ::_thesis: ( (inferior_realsequence seq) . n <= seq . n & seq . n <= (superior_realsequence seq) . n ) consider Y being non empty Subset of ExtREAL such that A1: Y = { (seq . k) where k is Element of NAT : n <= k } and A2: (inferior_realsequence seq) . n = inf Y by Def6; A3: seq . n in Y by A1; hence (inferior_realsequence seq) . n <= seq . n by A2, XXREAL_2:3; ::_thesis: seq . n <= (superior_realsequence seq) . n ex Z being non empty Subset of ExtREAL st ( Z = { (seq . k) where k is Element of NAT : n <= k } & (superior_realsequence seq) . n = sup Z ) by Def7; hence seq . n <= (superior_realsequence seq) . n by A1, A3, XXREAL_2:4; ::_thesis: verum end; Lm1: for seq being ExtREAL_sequence holds superior_realsequence seq is non-increasing proof let seq be ExtREAL_sequence; ::_thesis: superior_realsequence seq is non-increasing now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_ (superior_realsequence_seq)_._n_<=_(superior_realsequence_seq)_._m let n, m be Element of NAT ; ::_thesis: ( m <= n implies (superior_realsequence seq) . n <= (superior_realsequence seq) . m ) consider Y being non empty Subset of ExtREAL such that A1: Y = { (seq . k) where k is Element of NAT : m <= k } and A2: (superior_realsequence seq) . m = sup Y by Def7; consider Z being non empty Subset of ExtREAL such that A3: Z = { (seq . k) where k is Element of NAT : n <= k } and A4: (superior_realsequence seq) . n = sup Z by Def7; assume A5: m <= n ; ::_thesis: (superior_realsequence seq) . n <= (superior_realsequence seq) . m Z c= Y proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in Y ) assume z in Z ; ::_thesis: z in Y then consider k being Element of NAT such that A6: z = seq . k and A7: n <= k by A3; m <= k by A5, A7, XXREAL_0:2; hence z in Y by A1, A6; ::_thesis: verum end; hence (superior_realsequence seq) . n <= (superior_realsequence seq) . m by A2, A4, XXREAL_2:59; ::_thesis: verum end; hence superior_realsequence seq is non-increasing by Th7; ::_thesis: verum end; Lm2: for seq being ExtREAL_sequence holds inferior_realsequence seq is non-decreasing proof let seq be ExtREAL_sequence; ::_thesis: inferior_realsequence seq is non-decreasing now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_ (inferior_realsequence_seq)_._m_<=_(inferior_realsequence_seq)_._n let n, m be Element of NAT ; ::_thesis: ( m <= n implies (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n ) consider Y being non empty Subset of ExtREAL such that A1: Y = { (seq . k) where k is Element of NAT : m <= k } and A2: (inferior_realsequence seq) . m = inf Y by Def6; consider Z being non empty Subset of ExtREAL such that A3: Z = { (seq . k) where k is Element of NAT : n <= k } and A4: (inferior_realsequence seq) . n = inf Z by Def6; assume A5: m <= n ; ::_thesis: (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n Z c= Y proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in Y ) assume z in Z ; ::_thesis: z in Y then consider k being Element of NAT such that A6: z = seq . k and A7: n <= k by A3; m <= k by A5, A7, XXREAL_0:2; hence z in Y by A1, A6; ::_thesis: verum end; hence (inferior_realsequence seq) . m <= (inferior_realsequence seq) . n by A2, A4, XXREAL_2:60; ::_thesis: verum end; hence inferior_realsequence seq is non-decreasing by Th7; ::_thesis: verum end; registration let seq be ExtREAL_sequence; cluster superior_realsequence seq -> non-increasing ; coherence superior_realsequence seq is non-increasing by Lm1; cluster inferior_realsequence seq -> non-decreasing ; coherence inferior_realsequence seq is non-decreasing by Lm2; end; definition let seq be ExtREAL_sequence; func lim_sup seq -> Element of ExtREAL equals :: RINFSUP2:def 8 inf (superior_realsequence seq); coherence inf (superior_realsequence seq) is Element of ExtREAL ; func lim_inf seq -> Element of ExtREAL equals :: RINFSUP2:def 9 sup (inferior_realsequence seq); coherence sup (inferior_realsequence seq) is Element of ExtREAL ; end; :: deftheorem defines lim_sup RINFSUP2:def_8_:_ for seq being ExtREAL_sequence holds lim_sup seq = inf (superior_realsequence seq); :: deftheorem defines lim_inf RINFSUP2:def_9_:_ for seq being ExtREAL_sequence holds lim_inf seq = sup (inferior_realsequence seq); theorem Th9: :: RINFSUP2:9 for seq being ExtREAL_sequence for rseq being Real_Sequence st seq = rseq & rseq is bounded holds ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) proof let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq & rseq is bounded holds ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) let rseq be Real_Sequence; ::_thesis: ( seq = rseq & rseq is bounded implies ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) ) assume that A1: seq = rseq and A2: rseq is bounded ; ::_thesis: ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) A3: NAT = dom (superior_realsequence rseq) by FUNCT_2:def_1; A4: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ (superior_realsequence_seq)_._x_=_(superior_realsequence_rseq)_._x let x be set ; ::_thesis: ( x in NAT implies (superior_realsequence seq) . x = (superior_realsequence rseq) . x ) assume x in NAT ; ::_thesis: (superior_realsequence seq) . x = (superior_realsequence rseq) . x then reconsider n = x as Element of NAT ; now__::_thesis:_for_x_being_set_st_x_in__{__(rseq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in_REAL let x be set ; ::_thesis: ( x in { (rseq . k) where k is Element of NAT : n <= k } implies x in REAL ) assume x in { (rseq . k) where k is Element of NAT : n <= k } ; ::_thesis: x in REAL then ex k being Element of NAT st ( x = rseq . k & n <= k ) ; hence x in REAL ; ::_thesis: verum end; then reconsider Y2 = { (rseq . k) where k is Element of NAT : n <= k } as Subset of REAL by TARSKI:def_3; A5: Y2 is bounded_above by A2, RINFSUP1:31; ex Y1 being non empty Subset of ExtREAL st ( Y1 = { (seq . k) where k is Element of NAT : n <= k } & (superior_realsequence seq) . n = sup Y1 ) by Def7; then (superior_realsequence seq) . x = upper_bound Y2 by A1, A5, Th1; hence (superior_realsequence seq) . x = (superior_realsequence rseq) . x by RINFSUP1:def_5; ::_thesis: verum end; superior_realsequence rseq is bounded by A2, RINFSUP1:56; then A6: rng (superior_realsequence rseq) is bounded_below by RINFSUP1:6; NAT = dom (superior_realsequence seq) by FUNCT_2:def_1; then superior_realsequence seq = superior_realsequence rseq by A4, A3, FUNCT_1:2; hence ( superior_realsequence seq = superior_realsequence rseq & lim_sup seq = lim_sup rseq ) by A6, Th3; ::_thesis: verum end; theorem Th10: :: RINFSUP2:10 for seq being ExtREAL_sequence for rseq being Real_Sequence st seq = rseq & rseq is bounded holds ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) proof let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq & rseq is bounded holds ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) let rseq be Real_Sequence; ::_thesis: ( seq = rseq & rseq is bounded implies ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) ) assume that A1: seq = rseq and A2: rseq is bounded ; ::_thesis: ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) A3: NAT = dom (inferior_realsequence rseq) by FUNCT_2:def_1; A4: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ (inferior_realsequence_seq)_._x_=_(inferior_realsequence_rseq)_._x let x be set ; ::_thesis: ( x in NAT implies (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x ) assume x in NAT ; ::_thesis: (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x then reconsider n = x as Element of NAT ; consider Y1 being non empty Subset of ExtREAL such that A5: Y1 = { (seq . k) where k is Element of NAT : n <= k } and A6: (inferior_realsequence seq) . n = inf Y1 by Def6; now__::_thesis:_for_x_being_set_st_x_in__{__(rseq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in_REAL let x be set ; ::_thesis: ( x in { (rseq . k) where k is Element of NAT : n <= k } implies x in REAL ) assume x in { (rseq . k) where k is Element of NAT : n <= k } ; ::_thesis: x in REAL then ex k being Element of NAT st ( x = rseq . k & n <= k ) ; hence x in REAL ; ::_thesis: verum end; then reconsider Y2 = { (rseq . k) where k is Element of NAT : n <= k } as Subset of REAL by TARSKI:def_3; Y2 is bounded_below by A2, RINFSUP1:32; then inf Y1 = lower_bound Y2 by A1, A5, Th3; hence (inferior_realsequence seq) . x = (inferior_realsequence rseq) . x by A6, RINFSUP1:def_4; ::_thesis: verum end; inferior_realsequence rseq is bounded by A2, RINFSUP1:56; then A7: rng (inferior_realsequence rseq) is bounded_above by RINFSUP1:5; NAT = dom (inferior_realsequence seq) by FUNCT_2:def_1; then inferior_realsequence seq = inferior_realsequence rseq by A4, A3, FUNCT_1:2; hence ( inferior_realsequence seq = inferior_realsequence rseq & lim_inf seq = lim_inf rseq ) by A7, Th1; ::_thesis: verum end; theorem Th11: :: RINFSUP2:11 for seq being ExtREAL_sequence st seq is bounded holds seq is Real_Sequence proof let seq be ExtREAL_sequence; ::_thesis: ( seq is bounded implies seq is Real_Sequence ) assume A1: seq is bounded ; ::_thesis: seq is Real_Sequence then seq is bounded_below by Def5; then rng seq is bounded_below by Def3; then consider UL being real number such that A2: UL is LowerBound of rng seq by XXREAL_2:def_9; A3: UL in REAL by XREAL_0:def_1; seq is bounded_above by A1, Def5; then rng seq is bounded_above by Def4; then consider UB being real number such that A4: UB is UpperBound of rng seq by XXREAL_2:def_10; A5: UB in REAL by XREAL_0:def_1; A6: now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ seq_._x_in_REAL let x be set ; ::_thesis: ( x in NAT implies seq . x in REAL ) assume x in NAT ; ::_thesis: seq . x in REAL then A7: seq . x in rng seq by FUNCT_2:4; then A8: seq . x <> -infty by A2, A3, XXREAL_0:12, XXREAL_2:def_2; seq . x <> +infty by A5, A4, A7, XXREAL_0:9, XXREAL_2:def_1; hence seq . x in REAL by A8, XXREAL_0:14; ::_thesis: verum end; dom seq = NAT by FUNCT_2:def_1; hence seq is Real_Sequence by A6, FUNCT_2:3; ::_thesis: verum end; theorem Th12: :: RINFSUP2:12 for seq being ExtREAL_sequence for rseq being Real_Sequence st seq = rseq holds ( seq is bounded_above iff rseq is V64() ) proof let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq holds ( seq is bounded_above iff rseq is V64() ) let rseq be Real_Sequence; ::_thesis: ( seq = rseq implies ( seq is bounded_above iff rseq is V64() ) ) assume A1: seq = rseq ; ::_thesis: ( seq is bounded_above iff rseq is V64() ) hereby ::_thesis: ( rseq is V64() implies seq is bounded_above ) assume seq is bounded_above ; ::_thesis: rseq is V64() then rng rseq is bounded_above by A1, Def4; then consider p being real number such that A2: p is UpperBound of rng rseq by XXREAL_2:def_10; A3: for y being real number st y in rng rseq holds y <= p by A2, XXREAL_2:def_1; now__::_thesis:_for_n_being_Element_of_NAT_holds_rseq_._n_<_p_+_1 let n be Element of NAT ; ::_thesis: rseq . n < p + 1 rseq . n in rng rseq by FUNCT_2:4; then 0 + (rseq . n) < 1 + p by A3, XREAL_1:8; hence rseq . n < p + 1 ; ::_thesis: verum end; hence rseq is V64() by SEQ_2:def_3; ::_thesis: verum end; assume rseq is V64() ; ::_thesis: seq is bounded_above then consider q being real number such that A4: for n being Element of NAT holds rseq . n < q by SEQ_2:def_3; now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_seq_holds_ r_<=_q let r be ext-real number ; ::_thesis: ( r in rng seq implies r <= q ) assume r in rng seq ; ::_thesis: r <= q then ex x being set st ( x in dom rseq & r = rseq . x ) by A1, FUNCT_1:def_3; hence r <= q by A4; ::_thesis: verum end; then q is UpperBound of rng seq by XXREAL_2:def_1; hence rng seq is bounded_above by XXREAL_2:def_10; :: according to RINFSUP2:def_4 ::_thesis: verum end; theorem Th13: :: RINFSUP2:13 for seq being ExtREAL_sequence for rseq being Real_Sequence st seq = rseq holds ( seq is bounded_below iff rseq is V65() ) proof let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq holds ( seq is bounded_below iff rseq is V65() ) let rseq be Real_Sequence; ::_thesis: ( seq = rseq implies ( seq is bounded_below iff rseq is V65() ) ) assume A1: seq = rseq ; ::_thesis: ( seq is bounded_below iff rseq is V65() ) hereby ::_thesis: ( rseq is V65() implies seq is bounded_below ) assume seq is bounded_below ; ::_thesis: rseq is V65() then rng rseq is bounded_below by A1, Def3; then consider p being real number such that A2: p is LowerBound of rng rseq by XXREAL_2:def_9; A3: for y being real number st y in rng rseq holds p <= y by A2, XXREAL_2:def_2; now__::_thesis:_for_n_being_Element_of_NAT_holds_p_-_1_<_rseq_._n let n be Element of NAT ; ::_thesis: p - 1 < rseq . n rseq . n in rng rseq by FUNCT_2:4; then p - 1 < (rseq . n) - 0 by A3, XREAL_1:15; hence p - 1 < rseq . n ; ::_thesis: verum end; hence rseq is V65() by SEQ_2:def_4; ::_thesis: verum end; assume rseq is V65() ; ::_thesis: seq is bounded_below then consider q being real number such that A4: for n being Element of NAT holds q < rseq . n by SEQ_2:def_4; now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_seq_holds_ q_<=_r let r be ext-real number ; ::_thesis: ( r in rng seq implies q <= r ) assume r in rng seq ; ::_thesis: q <= r then ex x being set st ( x in dom rseq & r = rseq . x ) by A1, FUNCT_1:def_3; hence q <= r by A4; ::_thesis: verum end; then q is LowerBound of rng seq by XXREAL_2:def_2; hence rng seq is bounded_below by XXREAL_2:def_9; :: according to RINFSUP2:def_3 ::_thesis: verum end; theorem Th14: :: RINFSUP2:14 for seq being ExtREAL_sequence for rseq being Real_Sequence st seq = rseq & rseq is convergent holds ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) proof let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq & rseq is convergent holds ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) let rseq be Real_Sequence; ::_thesis: ( seq = rseq & rseq is convergent implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) ) assume that A1: seq = rseq and A2: rseq is convergent ; ::_thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) A3: now__::_thesis:_for_e_being_real_number_st_0_<_e_holds_ ex_N_being_Nat_st_ for_m_being_Nat_st_N_<=_m_holds_ |.((seq_._m)_-_(R_EAL_(lim_rseq))).|_<_e let e be real number ; ::_thesis: ( 0 < e implies ex N being Nat st for m being Nat st N <= m holds |.((seq . m) - (R_EAL (lim rseq))).| < e ) assume 0 < e ; ::_thesis: ex N being Nat st for m being Nat st N <= m holds |.((seq . m) - (R_EAL (lim rseq))).| < e then consider n being Element of NAT such that A4: for m being Element of NAT st n <= m holds abs ((rseq . m) - (lim rseq)) < e by A2, SEQ_2:def_7; set N = n; now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_ |.((seq_._m)_-_(R_EAL_(lim_rseq))).|_<_e let m be Nat; ::_thesis: ( n <= m implies |.((seq . m) - (R_EAL (lim rseq))).| < e ) A5: m is Element of NAT by ORDINAL1:def_12; A6: (rseq . m) - (lim rseq) = (seq . m) - (R_EAL (lim rseq)) by A1, SUPINF_2:3; assume n <= m ; ::_thesis: |.((seq . m) - (R_EAL (lim rseq))).| < e then abs ((rseq . m) - (lim rseq)) < e by A4, A5; hence |.((seq . m) - (R_EAL (lim rseq))).| < e by A6, EXTREAL2:1; ::_thesis: verum end; hence ex N being Nat st for m being Nat st N <= m holds |.((seq . m) - (R_EAL (lim rseq))).| < e ; ::_thesis: verum end; then A7: seq is convergent_to_finite_number by MESFUNC5:def_8; then seq is convergent by MESFUNC5:def_11; hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim rseq ) by A3, A7, MESFUNC5:def_12; ::_thesis: verum end; theorem Th15: :: RINFSUP2:15 for seq being ExtREAL_sequence for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds ( rseq is convergent & lim seq = lim rseq ) proof let seq be ExtREAL_sequence; ::_thesis: for rseq being Real_Sequence st seq = rseq & seq is convergent_to_finite_number holds ( rseq is convergent & lim seq = lim rseq ) let rseq be Real_Sequence; ::_thesis: ( seq = rseq & seq is convergent_to_finite_number implies ( rseq is convergent & lim seq = lim rseq ) ) assume that A1: seq = rseq and A2: seq is convergent_to_finite_number ; ::_thesis: ( rseq is convergent & lim seq = lim rseq ) A3: ( not lim seq = +infty or not seq is convergent_to_+infty ) by A2, MESFUNC5:50; A4: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A2, MESFUNC5:51; seq is convergent by A2, MESFUNC5:def_11; then consider g being real number such that A5: lim seq = g and A6: for p being real number st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((seq . m) - (lim seq)).| < p and seq is convergent_to_finite_number by A3, A4, MESFUNC5:def_12; A7: 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 ((rseq . m) - g) < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((rseq . m) - g) < p ) assume 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs ((rseq . m) - g) < p then consider n being Nat such that A8: for m being Nat st n <= m holds |.((seq . m) - (lim seq)).| < p by A6; reconsider N = n as Element of NAT by ORDINAL1:def_12; take N ; ::_thesis: for m being Element of NAT st N <= m holds abs ((rseq . m) - g) < p hereby ::_thesis: verum let m be Element of NAT ; ::_thesis: ( N <= m implies abs ((rseq . m) - g) < p ) assume N <= m ; ::_thesis: abs ((rseq . m) - g) < p then A9: |.((seq . m) - (lim seq)).| < p by A8; g is Real by XREAL_0:def_1; then (rseq . m) - g = (seq . m) - (lim seq) by A1, A5, SUPINF_2:3; hence abs ((rseq . m) - g) < p by A9, EXTREAL2:1; ::_thesis: verum end; end; then rseq is convergent by SEQ_2:def_6; hence ( rseq is convergent & lim seq = lim rseq ) by A5, A7, SEQ_2:def_7; ::_thesis: verum end; theorem Th16: :: RINFSUP2:16 for k being Element of NAT for seq being ExtREAL_sequence st seq ^\ k is convergent_to_finite_number holds ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) ) proof let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq ^\ k is convergent_to_finite_number holds ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) ) let seq be ExtREAL_sequence; ::_thesis: ( seq ^\ k is convergent_to_finite_number implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) ) ) set seq0 = seq ^\ k; assume A1: seq ^\ k is convergent_to_finite_number ; ::_thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) ) then A2: ( not lim (seq ^\ k) = +infty or not seq ^\ k is convergent_to_+infty ) by MESFUNC5:50; A3: ( not lim (seq ^\ k) = -infty or not seq ^\ k is convergent_to_-infty ) by A1, MESFUNC5:51; seq ^\ k is convergent by A1, MESFUNC5:def_11; then A4: ex g being real number st ( lim (seq ^\ k) = g & ( for p being real number st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.(((seq ^\ k) . m) - (lim (seq ^\ k))).| < p ) & seq ^\ k is convergent_to_finite_number ) by A2, A3, MESFUNC5:def_12; then consider g being real number such that A5: lim (seq ^\ k) = g ; A6: for p being real number st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((seq . m) - (lim (seq ^\ k))).| < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Nat st for m being Nat st n <= m holds |.((seq . m) - (lim (seq ^\ k))).| < p ) assume 0 < p ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds |.((seq . m) - (lim (seq ^\ k))).| < p then consider n being Nat such that A7: for m being Nat st n <= m holds |.(((seq ^\ k) . m) - (lim (seq ^\ k))).| < p by A4; take n1 = n + k; ::_thesis: for m being Nat st n1 <= m holds |.((seq . m) - (lim (seq ^\ k))).| < p hereby ::_thesis: verum let m be Nat; ::_thesis: ( n1 <= m implies |.((seq . m) - (lim (seq ^\ k))).| < p ) assume A8: n1 <= m ; ::_thesis: |.((seq . m) - (lim (seq ^\ k))).| < p k <= n + k by NAT_1:11; then reconsider mk = m - k as Element of NAT by A8, INT_1:5, XXREAL_0:2; A9: (seq ^\ k) . (m - k) = seq . (mk + k) by NAT_1:def_3; (n + k) - k <= m - k by A8, XREAL_1:9; hence |.((seq . m) - (lim (seq ^\ k))).| < p by A7, A9; ::_thesis: verum end; end; lim (seq ^\ k) = R_EAL g by A5; hence A10: seq is convergent_to_finite_number by A6, MESFUNC5:def_8; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) ) hence seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k) hence lim seq = lim (seq ^\ k) by A5, A6, A10, MESFUNC5:def_12; ::_thesis: verum end; theorem Th17: :: RINFSUP2:17 for k being Element of NAT for seq being ExtREAL_sequence st seq ^\ k is convergent holds ( seq is convergent & lim seq = lim (seq ^\ k) ) proof let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq ^\ k is convergent holds ( seq is convergent & lim seq = lim (seq ^\ k) ) let seq be ExtREAL_sequence; ::_thesis: ( seq ^\ k is convergent implies ( seq is convergent & lim seq = lim (seq ^\ k) ) ) set seq0 = seq ^\ k; assume A1: seq ^\ k is convergent ; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) ) percases ( seq ^\ k is convergent_to_finite_number or seq ^\ k is convergent_to_+infty or seq ^\ k is convergent_to_-infty ) by A1, MESFUNC5:def_11; suppose seq ^\ k is convergent_to_finite_number ; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) ) hence ( seq is convergent & lim seq = lim (seq ^\ k) ) by Th16; ::_thesis: verum end; supposeA2: seq ^\ k is convergent_to_+infty ; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) ) for g being real number st 0 < g holds ex n being Nat st for m being Nat st n <= m holds g <= seq . m proof let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st for m being Nat st n <= m holds g <= seq . m ) assume 0 < g ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds g <= seq . m then consider n being Nat such that A3: for m being Nat st n <= m holds g <= (seq ^\ k) . m by A2, MESFUNC5:def_9; take n1 = n + k; ::_thesis: for m being Nat st n1 <= m holds g <= seq . m hereby ::_thesis: verum let m be Nat; ::_thesis: ( n1 <= m implies g <= seq . m ) assume A4: n1 <= m ; ::_thesis: g <= seq . m k <= n + k by NAT_1:11; then reconsider mk = m - k as Element of NAT by A4, INT_1:5, XXREAL_0:2; A5: (seq ^\ k) . (m - k) = seq . (mk + k) by NAT_1:def_3; (n + k) - k <= m - k by A4, XREAL_1:9; hence g <= seq . m by A3, A5; ::_thesis: verum end; end; then A6: seq is convergent_to_+infty by MESFUNC5:def_9; hence A7: seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k) lim (seq ^\ k) = +infty by A1, A2, MESFUNC5:def_12; hence lim seq = lim (seq ^\ k) by A6, A7, MESFUNC5:def_12; ::_thesis: verum end; supposeA8: seq ^\ k is convergent_to_-infty ; ::_thesis: ( seq is convergent & lim seq = lim (seq ^\ k) ) for g being real number st g < 0 holds ex n being Nat st for m being Nat st n <= m holds seq . m <= g proof let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st for m being Nat st n <= m holds seq . m <= g ) assume g < 0 ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds seq . m <= g then consider n being Nat such that A9: for m being Nat st n <= m holds (seq ^\ k) . m <= g by A8, MESFUNC5:def_10; take n1 = n + k; ::_thesis: for m being Nat st n1 <= m holds seq . m <= g hereby ::_thesis: verum let m be Nat; ::_thesis: ( n1 <= m implies seq . m <= g ) assume A10: n1 <= m ; ::_thesis: seq . m <= g k <= n + k by NAT_1:11; then reconsider mk = m - k as Element of NAT by A10, INT_1:5, XXREAL_0:2; A11: (seq ^\ k) . (m - k) = seq . (mk + k) by NAT_1:def_3; (n + k) - k <= m - k by A10, XREAL_1:9; hence seq . m <= g by A9, A11; ::_thesis: verum end; end; then A12: seq is convergent_to_-infty by MESFUNC5:def_10; hence A13: seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k) lim (seq ^\ k) = -infty by A1, A8, MESFUNC5:def_12; hence lim seq = lim (seq ^\ k) by A12, A13, MESFUNC5:def_12; ::_thesis: verum end; end; end; theorem Th18: :: RINFSUP2:18 for seq being ExtREAL_sequence st lim_sup seq = lim_inf seq & lim_inf seq in REAL holds ex k being Element of NAT st seq ^\ k is bounded proof let seq be ExtREAL_sequence; ::_thesis: ( lim_sup seq = lim_inf seq & lim_inf seq in REAL implies ex k being Element of NAT st seq ^\ k is bounded ) assume that A1: lim_sup seq = lim_inf seq and A2: lim_inf seq in REAL ; ::_thesis: ex k being Element of NAT st seq ^\ k is bounded reconsider a = lim_inf seq as Real by A2; set K1 = a + 1; ex k1 being Element of NAT st (superior_realsequence seq) . k1 <= a + 1 proof assume A3: for k1 being Element of NAT holds not (superior_realsequence seq) . k1 <= a + 1 ; ::_thesis: contradiction now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_(superior_realsequence_seq)_holds_ a_+_1_<=_x let x be ext-real number ; ::_thesis: ( x in rng (superior_realsequence seq) implies a + 1 <= x ) assume x in rng (superior_realsequence seq) ; ::_thesis: a + 1 <= x then ex n being set st ( n in dom (superior_realsequence seq) & x = (superior_realsequence seq) . n ) by FUNCT_1:def_3; hence a + 1 <= x by A3; ::_thesis: verum end; then a + 1 is LowerBound of rng (superior_realsequence seq) by XXREAL_2:def_2; then a + 1 <= a by A1, XXREAL_2:def_4; hence contradiction by XREAL_1:29; ::_thesis: verum end; then consider k1 being Element of NAT such that A4: (superior_realsequence seq) . k1 <= a + 1 ; set K2 = a - 1; ex k2 being Element of NAT st a - 1 <= (inferior_realsequence seq) . k2 proof assume A5: for k2 being Element of NAT holds not a - 1 <= (inferior_realsequence seq) . k2 ; ::_thesis: contradiction now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_(inferior_realsequence_seq)_holds_ x_<=_a_-_1 let x be ext-real number ; ::_thesis: ( x in rng (inferior_realsequence seq) implies x <= a - 1 ) assume x in rng (inferior_realsequence seq) ; ::_thesis: x <= a - 1 then ex n being set st ( n in dom (inferior_realsequence seq) & x = (inferior_realsequence seq) . n ) by FUNCT_1:def_3; hence x <= a - 1 by A5; ::_thesis: verum end; then a - 1 is UpperBound of rng (inferior_realsequence seq) by XXREAL_2:def_1; then a <= a - 1 by XXREAL_2:def_3; then a + 0 < (a - 1) + 1 by XREAL_1:8; hence contradiction ; ::_thesis: verum end; then consider k2 being Element of NAT such that A6: a - 1 <= (inferior_realsequence seq) . k2 ; take k = max (k1,k2); ::_thesis: seq ^\ k is bounded k2 <= k by XXREAL_0:25; then (inferior_realsequence seq) . k2 <= (inferior_realsequence seq) . k by Th7; then A7: a - 1 <= (inferior_realsequence seq) . k by A6, XXREAL_0:2; k1 <= k by XXREAL_0:25; then (superior_realsequence seq) . k <= (superior_realsequence seq) . k1 by Th7; then A8: (superior_realsequence seq) . k <= a + 1 by A4, XXREAL_0:2; A9: for n being Element of NAT st k <= n holds ( seq . n <= a + 1 & a - 1 <= seq . n ) proof let n be Element of NAT ; ::_thesis: ( k <= n implies ( seq . n <= a + 1 & a - 1 <= seq . n ) ) A10: (inferior_realsequence seq) . n <= seq . n by Th8; assume A11: k <= n ; ::_thesis: ( seq . n <= a + 1 & a - 1 <= seq . n ) then (superior_realsequence seq) . n <= (superior_realsequence seq) . k by Th7; then A12: (superior_realsequence seq) . n <= a + 1 by A8, XXREAL_0:2; (inferior_realsequence seq) . k <= (inferior_realsequence seq) . n by A11, Th7; then A13: a - 1 <= (inferior_realsequence seq) . n by A7, XXREAL_0:2; seq . n <= (superior_realsequence seq) . n by Th8; hence ( seq . n <= a + 1 & a - 1 <= seq . n ) by A12, A13, A10, XXREAL_0:2; ::_thesis: verum end; now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_(seq_^\_k)_holds_ x_<=_a_+_1 let x be ext-real number ; ::_thesis: ( x in rng (seq ^\ k) implies x <= a + 1 ) assume x in rng (seq ^\ k) ; ::_thesis: x <= a + 1 then consider n being set such that A14: n in dom (seq ^\ k) and A15: x = (seq ^\ k) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A14; A16: k <= n + k by NAT_1:11; x = seq . (n + k) by A15, NAT_1:def_3; hence x <= a + 1 by A9, A16; ::_thesis: verum end; then a + 1 is UpperBound of rng (seq ^\ k) by XXREAL_2:def_1; hence rng (seq ^\ k) is bounded_above by XXREAL_2:def_10; :: according to RINFSUP2:def_4,RINFSUP2:def_5 ::_thesis: seq ^\ k is bounded_below now__::_thesis:_for_x_being_ext-real_number_st_x_in_rng_(seq_^\_k)_holds_ a_-_1_<=_x let x be ext-real number ; ::_thesis: ( x in rng (seq ^\ k) implies a - 1 <= x ) assume x in rng (seq ^\ k) ; ::_thesis: a - 1 <= x then consider n being set such that A17: n in dom (seq ^\ k) and A18: x = (seq ^\ k) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A17; A19: k <= n + k by NAT_1:11; x = seq . (n + k) by A18, NAT_1:def_3; hence a - 1 <= x by A9, A19; ::_thesis: verum end; then a - 1 is LowerBound of rng (seq ^\ k) by XXREAL_2:def_2; hence rng (seq ^\ k) is bounded_below by XXREAL_2:def_9; :: according to RINFSUP2:def_3 ::_thesis: verum end; theorem Th19: :: RINFSUP2:19 for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds ex k being Element of NAT st seq ^\ k is bounded proof let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent_to_finite_number implies ex k being Element of NAT st seq ^\ k is bounded ) assume A1: seq is convergent_to_finite_number ; ::_thesis: ex k being Element of NAT st seq ^\ k is bounded then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:50; A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:51; seq is convergent by A1, MESFUNC5:def_11; then A4: ex g being real number st ( lim seq = g & ( for p being real number st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((seq . m) - (lim seq)).| < p ) & seq is convergent_to_finite_number ) by A2, A3, MESFUNC5:def_12; then consider g being real number such that A5: lim seq = g ; set UB = g + 1; consider k being Nat such that A6: for m being Nat st k <= m holds |.((seq . m) - (lim seq)).| < 1 by A4; reconsider K = k as Element of NAT by ORDINAL1:def_12; take K ; ::_thesis: seq ^\ K is bounded A7: g is Real by XREAL_0:def_1; now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_(seq_^\_K)_holds_ r_<=_g_+_1 let r be ext-real number ; ::_thesis: ( r in rng (seq ^\ K) implies r <= g + 1 ) assume r in rng (seq ^\ K) ; ::_thesis: r <= g + 1 then consider n being set such that A8: n in dom (seq ^\ K) and A9: r = (seq ^\ K) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A8; |.((seq . (n + k)) - (lim seq)).| <= 1. by A6, NAT_1:11; then (seq . (n + k)) - (lim seq) <= 1. by EXTREAL2:12; then ((seq . (n + k)) + (- (lim seq))) + (lim seq) <= 1. + (lim seq) by XXREAL_3:36; then (seq . (n + k)) + ((- (lim seq)) + (lim seq)) <= 1. + (lim seq) by A5, XXREAL_3:29; then (seq . (n + k)) + 0. <= 1. + (lim seq) by XXREAL_3:7; then seq . (n + k) <= 1. + (lim seq) by XXREAL_3:4; then seq . (n + k) <= g + 1 by A5, A7, SUPINF_2:1; hence r <= g + 1 by A9, NAT_1:def_3; ::_thesis: verum end; then g + 1 is UpperBound of rng (seq ^\ K) by XXREAL_2:def_1; hence rng (seq ^\ K) is bounded_above by XXREAL_2:def_10; :: according to RINFSUP2:def_4,RINFSUP2:def_5 ::_thesis: seq ^\ K is bounded_below set UL = g - 1; now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_(seq_^\_K)_holds_ g_-_1_<=_r let r be ext-real number ; ::_thesis: ( r in rng (seq ^\ K) implies g - 1 <= r ) assume r in rng (seq ^\ K) ; ::_thesis: g - 1 <= r then consider n being set such that A10: n in dom (seq ^\ K) and A11: r = (seq ^\ K) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A10; |.((seq . (n + k)) - (lim seq)).| < 1 by A6, NAT_1:11; then - 1. <= (seq . (n + k)) - (lim seq) by EXTREAL2:12; then (- 1.) + (lim seq) <= ((seq . (n + k)) + (- (lim seq))) + (lim seq) by XXREAL_3:36; then (- 1.) + (lim seq) <= (seq . (n + k)) + ((- (lim seq)) + (lim seq)) by A5, XXREAL_3:29; then A12: (- 1.) + (lim seq) <= (seq . (n + k)) + 0. by XXREAL_3:7; - 1. = - 1 by SUPINF_2:2; then (- 1) + g = (- 1.) + (lim seq) by A5, A7, SUPINF_2:1; then g - 1 <= seq . (n + k) by A12, XXREAL_3:4; hence g - 1 <= r by A11, NAT_1:def_3; ::_thesis: verum end; then g - 1 is LowerBound of rng (seq ^\ K) by XXREAL_2:def_2; hence rng (seq ^\ K) is bounded_below by XXREAL_2:def_9; :: according to RINFSUP2:def_3 ::_thesis: verum end; theorem Th20: :: RINFSUP2:20 for k being Element of NAT for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds ( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) proof let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds ( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent_to_finite_number implies ( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) ) set seq0 = seq ^\ k; assume A1: seq is convergent_to_finite_number ; ::_thesis: ( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:50; A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:51; seq is convergent by A1, MESFUNC5:def_11; then A4: ex g being real number st ( lim seq = g & ( for p being real number st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((seq . m) - (lim seq)).| < p ) & seq is convergent_to_finite_number ) by A2, A3, MESFUNC5:def_12; then consider g being real number such that A5: lim seq = g ; A6: for p being real number st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.(((seq ^\ k) . m) - (lim seq)).| < p proof let p be real number ; ::_thesis: ( 0 < p implies ex n being Nat st for m being Nat st n <= m holds |.(((seq ^\ k) . m) - (lim seq)).| < p ) assume 0 < p ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds |.(((seq ^\ k) . m) - (lim seq)).| < p then consider n being Nat such that A7: for m being Nat st n <= m holds |.((seq . m) - (lim seq)).| < p by A4; take n ; ::_thesis: for m being Nat st n <= m holds |.(((seq ^\ k) . m) - (lim seq)).| < p hereby ::_thesis: verum let m be Nat; ::_thesis: ( n <= m implies |.(((seq ^\ k) . m) - (lim seq)).| < p ) assume A8: n <= m ; ::_thesis: |.(((seq ^\ k) . m) - (lim seq)).| < p m <= m + k by NAT_1:11; then n <= m + k by A8, XXREAL_0:2; then |.((seq . (m + k)) - (lim seq)).| < p by A7; hence |.(((seq ^\ k) . m) - (lim seq)).| < p by NAT_1:def_3; ::_thesis: verum end; end; lim seq = R_EAL g by A5; hence A9: seq ^\ k is convergent_to_finite_number by A6, MESFUNC5:def_8; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) hence seq ^\ k is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k) hence lim seq = lim (seq ^\ k) by A5, A6, A9, MESFUNC5:def_12; ::_thesis: verum end; theorem :: RINFSUP2:21 for k being Element of NAT for seq being ExtREAL_sequence st seq is convergent holds ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) proof let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq is convergent holds ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent implies ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) ) set seq0 = seq ^\ k; assume A1: seq is convergent ; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) percases ( seq is convergent_to_finite_number or seq is convergent_to_+infty or seq is convergent_to_-infty ) by A1, MESFUNC5:def_11; suppose seq is convergent_to_finite_number ; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) hence ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) by Th20; ::_thesis: verum end; supposeA2: seq is convergent_to_+infty ; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) for g being real number st 0 < g holds ex n being Nat st for m being Nat st n <= m holds g <= (seq ^\ k) . m proof let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st for m being Nat st n <= m holds g <= (seq ^\ k) . m ) assume 0 < g ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds g <= (seq ^\ k) . m then consider n being Nat such that A3: for m being Nat st n <= m holds g <= seq . m by A2, MESFUNC5:def_9; take n ; ::_thesis: for m being Nat st n <= m holds g <= (seq ^\ k) . m hereby ::_thesis: verum let m be Nat; ::_thesis: ( n <= m implies g <= (seq ^\ k) . m ) assume A4: n <= m ; ::_thesis: g <= (seq ^\ k) . m m <= m + k by NAT_1:11; then n <= m + k by A4, XXREAL_0:2; then g <= seq . (m + k) by A3; hence g <= (seq ^\ k) . m by NAT_1:def_3; ::_thesis: verum end; end; then A5: seq ^\ k is convergent_to_+infty by MESFUNC5:def_9; hence A6: seq ^\ k is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k) lim seq = +infty by A1, A2, MESFUNC5:def_12; hence lim seq = lim (seq ^\ k) by A5, A6, MESFUNC5:def_12; ::_thesis: verum end; supposeA7: seq is convergent_to_-infty ; ::_thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) for g being real number st g < 0 holds ex n being Nat st for m being Nat st n <= m holds (seq ^\ k) . m <= g proof let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st for m being Nat st n <= m holds (seq ^\ k) . m <= g ) assume g < 0 ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds (seq ^\ k) . m <= g then consider n being Nat such that A8: for m being Nat st n <= m holds seq . m <= g by A7, MESFUNC5:def_10; take n ; ::_thesis: for m being Nat st n <= m holds (seq ^\ k) . m <= g hereby ::_thesis: verum let m be Nat; ::_thesis: ( n <= m implies (seq ^\ k) . m <= g ) assume A9: n <= m ; ::_thesis: (seq ^\ k) . m <= g m <= m + k by NAT_1:11; then n <= m + k by A9, XXREAL_0:2; then seq . (m + k) <= g by A8; hence (seq ^\ k) . m <= g by NAT_1:def_3; ::_thesis: verum end; end; then A10: seq ^\ k is convergent_to_-infty by MESFUNC5:def_10; hence A11: seq ^\ k is convergent by MESFUNC5:def_11; ::_thesis: lim seq = lim (seq ^\ k) lim seq = -infty by A1, A7, MESFUNC5:def_12; hence lim seq = lim (seq ^\ k) by A10, A11, MESFUNC5:def_12; ::_thesis: verum end; end; end; theorem :: RINFSUP2:22 for k being Element of NAT for seq being ExtREAL_sequence holds ( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) ) proof let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence holds ( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) ) let seq be ExtREAL_sequence; ::_thesis: ( ( seq is bounded_above implies seq ^\ k is bounded_above ) & ( seq is bounded_below implies seq ^\ k is bounded_below ) ) hereby ::_thesis: ( seq is bounded_below implies seq ^\ k is bounded_below ) assume seq is bounded_above ; ::_thesis: seq ^\ k is bounded_above then rng seq is bounded_above by Def4; then consider UB being real number such that A1: UB is UpperBound of rng seq by XXREAL_2:def_10; now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_(seq_^\_k)_holds_ r_<=_UB let r be ext-real number ; ::_thesis: ( r in rng (seq ^\ k) implies r <= UB ) assume r in rng (seq ^\ k) ; ::_thesis: r <= UB then consider n being set such that A2: n in dom (seq ^\ k) and A3: r = (seq ^\ k) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A2; seq . (n + k) <= UB by A1, FUNCT_2:4, XXREAL_2:def_1; hence r <= UB by A3, NAT_1:def_3; ::_thesis: verum end; then UB is UpperBound of rng (seq ^\ k) by XXREAL_2:def_1; then rng (seq ^\ k) is bounded_above by XXREAL_2:def_10; hence seq ^\ k is bounded_above by Def4; ::_thesis: verum end; hereby ::_thesis: verum assume seq is bounded_below ; ::_thesis: seq ^\ k is bounded_below then rng seq is bounded_below by Def3; then consider UB being real number such that A4: UB is LowerBound of rng seq by XXREAL_2:def_9; now__::_thesis:_for_r_being_ext-real_number_st_r_in_rng_(seq_^\_k)_holds_ UB_<=_r let r be ext-real number ; ::_thesis: ( r in rng (seq ^\ k) implies UB <= r ) assume r in rng (seq ^\ k) ; ::_thesis: UB <= r then consider n being set such that A5: n in dom (seq ^\ k) and A6: r = (seq ^\ k) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A5; seq . (n + k) in rng seq by FUNCT_2:4; then UB <= seq . (n + k) by A4, XXREAL_2:def_2; hence UB <= r by A6, NAT_1:def_3; ::_thesis: verum end; then UB is LowerBound of rng (seq ^\ k) by XXREAL_2:def_2; then rng (seq ^\ k) is bounded_below by XXREAL_2:def_9; hence seq ^\ k is bounded_below by Def3; ::_thesis: verum end; end; theorem Th23: :: RINFSUP2:23 for n being Element of NAT for seq being ExtREAL_sequence holds ( inf seq <= seq . n & seq . n <= sup seq ) proof let n be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence holds ( inf seq <= seq . n & seq . n <= sup seq ) let seq be ExtREAL_sequence; ::_thesis: ( inf seq <= seq . n & seq . n <= sup seq ) A1: inf (rng seq) is LowerBound of rng seq by XXREAL_2:def_4; A2: sup (rng seq) is UpperBound of rng seq by XXREAL_2:def_3; seq . n in rng seq by FUNCT_2:4; hence ( inf seq <= seq . n & seq . n <= sup seq ) by A1, A2, XXREAL_2:def_1, XXREAL_2:def_2; ::_thesis: verum end; theorem Th24: :: RINFSUP2:24 for seq being ExtREAL_sequence holds inf seq <= sup seq proof let seq be ExtREAL_sequence; ::_thesis: inf seq <= sup seq A1: seq . 0 <= sup seq by Th23; inf seq <= seq . 0 by Th23; hence inf seq <= sup seq by A1, XXREAL_0:2; ::_thesis: verum end; theorem Th25: :: RINFSUP2:25 for k being Element of NAT for seq being ExtREAL_sequence st seq is non-increasing holds ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) ) proof let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq is non-increasing holds ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) ) let seq be ExtREAL_sequence; ::_thesis: ( seq is non-increasing implies ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) ) ) set seq0 = seq ^\ k; assume A1: seq is non-increasing ; ::_thesis: ( seq ^\ k is non-increasing & inf seq = inf (seq ^\ k) ) now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_ (seq_^\_k)_._n_<=_(seq_^\_k)_._m let n, m be Element of NAT ; ::_thesis: ( m <= n implies (seq ^\ k) . n <= (seq ^\ k) . m ) assume m <= n ; ::_thesis: (seq ^\ k) . n <= (seq ^\ k) . m then k + m <= k + n by XREAL_1:6; then seq . (k + n) <= seq . (k + m) by A1, Th7; then (seq ^\ k) . n <= seq . (k + m) by NAT_1:def_3; hence (seq ^\ k) . n <= (seq ^\ k) . m by NAT_1:def_3; ::_thesis: verum end; hence seq ^\ k is non-increasing by Th7; ::_thesis: inf seq = inf (seq ^\ k) now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_seq_holds_ inf_(rng_(seq_^\_k))_<=_y let y be ext-real number ; ::_thesis: ( y in rng seq implies inf (rng (seq ^\ k)) <= y ) assume y in rng seq ; ::_thesis: inf (rng (seq ^\ k)) <= y then consider n being set such that A2: n in dom seq and A3: y = seq . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A2; (seq ^\ k) . n = seq . (n + k) by NAT_1:def_3; then A4: inf (seq ^\ k) <= seq . (n + k) by Th23; n <= n + k by NAT_1:11; then seq . (n + k) <= seq . n by A1, Th7; hence inf (rng (seq ^\ k)) <= y by A3, A4, XXREAL_0:2; ::_thesis: verum end; then inf (rng (seq ^\ k)) is LowerBound of rng seq by XXREAL_2:def_2; then A5: inf (rng (seq ^\ k)) <= inf (rng seq) by XXREAL_2:def_4; now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(seq_^\_k)_holds_ inf_(rng_seq)_<=_y let y be ext-real number ; ::_thesis: ( y in rng (seq ^\ k) implies inf (rng seq) <= y ) assume y in rng (seq ^\ k) ; ::_thesis: inf (rng seq) <= y then consider n being set such that A6: n in dom (seq ^\ k) and A7: y = (seq ^\ k) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; (seq ^\ k) . n = seq . (n + k) by NAT_1:def_3; then inf seq <= (seq ^\ k) . n by Th23; hence inf (rng seq) <= y by A7; ::_thesis: verum end; then inf (rng seq) is LowerBound of rng (seq ^\ k) by XXREAL_2:def_2; then inf (rng seq) <= inf (rng (seq ^\ k)) by XXREAL_2:def_4; hence inf seq = inf (seq ^\ k) by A5, XXREAL_0:1; ::_thesis: verum end; theorem Th26: :: RINFSUP2:26 for k being Element of NAT for seq being ExtREAL_sequence st seq is non-decreasing holds ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) ) proof let k be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence st seq is non-decreasing holds ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) ) let seq be ExtREAL_sequence; ::_thesis: ( seq is non-decreasing implies ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) ) ) set seq0 = seq ^\ k; assume A1: seq is non-decreasing ; ::_thesis: ( seq ^\ k is non-decreasing & sup seq = sup (seq ^\ k) ) now__::_thesis:_for_n,_m_being_Element_of_NAT_st_m_<=_n_holds_ (seq_^\_k)_._m_<=_(seq_^\_k)_._n let n, m be Element of NAT ; ::_thesis: ( m <= n implies (seq ^\ k) . m <= (seq ^\ k) . n ) assume m <= n ; ::_thesis: (seq ^\ k) . m <= (seq ^\ k) . n then k + m <= k + n by XREAL_1:6; then seq . (k + m) <= seq . (k + n) by A1, Th7; then (seq ^\ k) . m <= seq . (k + n) by NAT_1:def_3; hence (seq ^\ k) . m <= (seq ^\ k) . n by NAT_1:def_3; ::_thesis: verum end; hence seq ^\ k is non-decreasing by Th7; ::_thesis: sup seq = sup (seq ^\ k) now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_seq_holds_ y_<=_sup_(rng_(seq_^\_k)) let y be ext-real number ; ::_thesis: ( y in rng seq implies y <= sup (rng (seq ^\ k)) ) assume y in rng seq ; ::_thesis: y <= sup (rng (seq ^\ k)) then consider n being set such that A2: n in dom seq and A3: y = seq . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A2; (seq ^\ k) . n = seq . (n + k) by NAT_1:def_3; then A4: seq . (n + k) <= sup (seq ^\ k) by Th23; n <= n + k by NAT_1:11; then seq . n <= seq . (n + k) by A1, Th7; hence y <= sup (rng (seq ^\ k)) by A3, A4, XXREAL_0:2; ::_thesis: verum end; then sup (rng (seq ^\ k)) is UpperBound of rng seq by XXREAL_2:def_1; then A5: sup (rng seq) <= sup (rng (seq ^\ k)) by XXREAL_2:def_3; now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(seq_^\_k)_holds_ y_<=_sup_(rng_seq) let y be ext-real number ; ::_thesis: ( y in rng (seq ^\ k) implies y <= sup (rng seq) ) assume y in rng (seq ^\ k) ; ::_thesis: y <= sup (rng seq) then consider n being set such that A6: n in dom (seq ^\ k) and A7: y = (seq ^\ k) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; (seq ^\ k) . n = seq . (n + k) by NAT_1:def_3; then (seq ^\ k) . n <= sup seq by Th23; hence y <= sup (rng seq) by A7; ::_thesis: verum end; then sup (rng seq) is UpperBound of rng (seq ^\ k) by XXREAL_2:def_1; then sup (rng (seq ^\ k)) <= sup (rng seq) by XXREAL_2:def_3; hence sup seq = sup (seq ^\ k) by A5, XXREAL_0:1; ::_thesis: verum end; theorem :: RINFSUP2:27 for n being Element of NAT for seq being ExtREAL_sequence holds ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) ) proof let n be Element of NAT ; ::_thesis: for seq being ExtREAL_sequence holds ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) ) let seq be ExtREAL_sequence; ::_thesis: ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) ) set rseq = seq ^\ n; A1: ex Z being non empty Subset of ExtREAL st ( Z = { (seq . k) where k is Element of NAT : n <= k } & (inferior_realsequence seq) . n = inf Z ) by Def6; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in_rng_(seq_^\_n) let x be set ; ::_thesis: ( x in { (seq . k) where k is Element of NAT : n <= k } implies x in rng (seq ^\ n) ) assume x in { (seq . k) where k is Element of NAT : n <= k } ; ::_thesis: x in rng (seq ^\ n) then consider k being Element of NAT such that A2: x = seq . k and A3: n <= k ; reconsider k1 = k - n as Element of NAT by A3, INT_1:5; x = seq . (n + k1) by A2; then x = (seq ^\ n) . k1 by NAT_1:def_3; hence x in rng (seq ^\ n) by FUNCT_2:4; ::_thesis: verum end; then A4: { (seq . k) where k is Element of NAT : n <= k } c= rng (seq ^\ n) by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in_rng_(seq_^\_n)_holds_ x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}_ let x be set ; ::_thesis: ( x in rng (seq ^\ n) implies x in { (seq . k) where k is Element of NAT : n <= k } ) assume x in rng (seq ^\ n) ; ::_thesis: x in { (seq . k) where k is Element of NAT : n <= k } then consider z being set such that A5: z in dom (seq ^\ n) and A6: x = (seq ^\ n) . z by FUNCT_1:def_3; reconsider k0 = z as Element of NAT by A5; A7: n <= n + k0 by NAT_1:11; x = seq . (n + k0) by A6, NAT_1:def_3; hence x in { (seq . k) where k is Element of NAT : n <= k } by A7; ::_thesis: verum end; then A8: rng (seq ^\ n) c= { (seq . k) where k is Element of NAT : n <= k } by TARSKI:def_3; ex Y being non empty Subset of ExtREAL st ( Y = { (seq . k) where k is Element of NAT : n <= k } & (superior_realsequence seq) . n = sup Y ) by Def7; hence ( (superior_realsequence seq) . n = sup (seq ^\ n) & (inferior_realsequence seq) . n = inf (seq ^\ n) ) by A1, A4, A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th28: :: RINFSUP2:28 for seq being ExtREAL_sequence for j being Element of NAT holds ( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq ) proof let seq be ExtREAL_sequence; ::_thesis: for j being Element of NAT holds ( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq ) let j be Element of NAT ; ::_thesis: ( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq ) set rseq = seq ^\ j; now__::_thesis:_for_n_being_Element_of_NAT_holds_(superior_realsequence_(seq_^\_j))_._n_=_((superior_realsequence_seq)_^\_j)_._n let n be Element of NAT ; ::_thesis: (superior_realsequence (seq ^\ j)) . n = ((superior_realsequence seq) ^\ j) . n A1: ex Y2 being non empty Subset of ExtREAL st ( Y2 = { ((seq ^\ j) . k) where k is Element of NAT : n <= k } & (superior_realsequence (seq ^\ j)) . n = sup Y2 ) by Def7; A2: ex Y3 being non empty Subset of ExtREAL st ( Y3 = { (seq . k) where k is Element of NAT : j + n <= k } & (superior_realsequence seq) . (j + n) = sup Y3 ) by Def7; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_j_+_n_<=_k__}__holds_ x_in__{__(seq_._(j_+_k2))_where_k2_is_Element_of_NAT_:_n_<=_k2__}_ let x be set ; ::_thesis: ( x in { (seq . k) where k is Element of NAT : j + n <= k } implies x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } ) assume x in { (seq . k) where k is Element of NAT : j + n <= k } ; ::_thesis: x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } then consider k being Element of NAT such that A3: x = seq . k and A4: j + n <= k ; j <= j + n by NAT_1:11; then reconsider k1 = k - j as Element of NAT by A4, INT_1:5, XXREAL_0:2; A5: x = seq . (j + k1) by A3; (j + n) - j <= k - j by A4, XREAL_1:9; hence x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } by A5; ::_thesis: verum end; then A6: { (seq . k) where k is Element of NAT : j + n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._(j_+_k))_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in__{__(seq_._k1)_where_k1_is_Element_of_NAT_:_j_+_n_<=_k1__}_ let x be set ; ::_thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } ) assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; ::_thesis: x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } then consider k being Element of NAT such that A7: x = seq . (j + k) and A8: n <= k ; j + n <= j + k by A8, XREAL_1:6; hence x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } by A7; ::_thesis: verum end; then { (seq . (j + k)) where k is Element of NAT : n <= k } c= { (seq . k) where k is Element of NAT : j + n <= k } by TARSKI:def_3; then A9: { (seq . (j + k)) where k is Element of NAT : n <= k } = { (seq . k) where k is Element of NAT : j + n <= k } by A6, XBOOLE_0:def_10; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._(j_+_k))_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in__{__((seq_^\_j)_._k1)_where_k1_is_Element_of_NAT_:_n_<=_k1__}_ let x be set ; ::_thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } ) assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; ::_thesis: x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } then consider k being Element of NAT such that A10: x = seq . (j + k) and A11: n <= k ; x = (seq ^\ j) . k by A10, NAT_1:def_3; hence x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } by A11; ::_thesis: verum end; then A12: { (seq . (j + k)) where k is Element of NAT : n <= k } c= { ((seq ^\ j) . k) where k is Element of NAT : n <= k } by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in__{__((seq_^\_j)_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in__{__(seq_._(j_+_k1))_where_k1_is_Element_of_NAT_:_n_<=_k1__}_ let x be set ; ::_thesis: ( x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } implies x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } ) assume x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } ; ::_thesis: x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } then consider k being Element of NAT such that A13: x = (seq ^\ j) . k and A14: n <= k ; x = seq . (j + k) by A13, NAT_1:def_3; hence x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } by A14; ::_thesis: verum end; then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def_3; then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } = { (seq . (j + k)) where k is Element of NAT : n <= k } by A12, XBOOLE_0:def_10; hence (superior_realsequence (seq ^\ j)) . n = ((superior_realsequence seq) ^\ j) . n by A1, A2, A9, NAT_1:def_3; ::_thesis: verum end; then (superior_realsequence seq) ^\ j = superior_realsequence (seq ^\ j) by FUNCT_2:63; hence ( superior_realsequence (seq ^\ j) = (superior_realsequence seq) ^\ j & lim_sup (seq ^\ j) = lim_sup seq ) by Th25; ::_thesis: verum end; theorem Th29: :: RINFSUP2:29 for seq being ExtREAL_sequence for j being Element of NAT holds ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq ) proof let seq be ExtREAL_sequence; ::_thesis: for j being Element of NAT holds ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq ) let j be Element of NAT ; ::_thesis: ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq ) set rseq = seq ^\ j; now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_realsequence_(seq_^\_j))_._n_=_((inferior_realsequence_seq)_^\_j)_._n let n be Element of NAT ; ::_thesis: (inferior_realsequence (seq ^\ j)) . n = ((inferior_realsequence seq) ^\ j) . n A1: ex Y2 being non empty Subset of ExtREAL st ( Y2 = { ((seq ^\ j) . k) where k is Element of NAT : n <= k } & (inferior_realsequence (seq ^\ j)) . n = inf Y2 ) by Def6; A2: ex Y3 being non empty Subset of ExtREAL st ( Y3 = { (seq . k) where k is Element of NAT : j + n <= k } & (inferior_realsequence seq) . (j + n) = inf Y3 ) by Def6; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._k)_where_k_is_Element_of_NAT_:_j_+_n_<=_k__}__holds_ x_in__{__(seq_._(j_+_k2))_where_k2_is_Element_of_NAT_:_n_<=_k2__}_ let x be set ; ::_thesis: ( x in { (seq . k) where k is Element of NAT : j + n <= k } implies x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } ) assume x in { (seq . k) where k is Element of NAT : j + n <= k } ; ::_thesis: x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } then consider k being Element of NAT such that A3: x = seq . k and A4: j + n <= k ; j <= j + n by NAT_1:11; then reconsider k1 = k - j as Element of NAT by A4, INT_1:5, XXREAL_0:2; A5: x = seq . (j + k1) by A3; (j + n) - j <= k - j by A4, XREAL_1:9; hence x in { (seq . (j + k2)) where k2 is Element of NAT : n <= k2 } by A5; ::_thesis: verum end; then A6: { (seq . k) where k is Element of NAT : j + n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._(j_+_k))_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in__{__(seq_._k1)_where_k1_is_Element_of_NAT_:_j_+_n_<=_k1__}_ let x be set ; ::_thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } ) assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; ::_thesis: x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } then consider k being Element of NAT such that A7: x = seq . (j + k) and A8: n <= k ; j + n <= j + k by A8, XREAL_1:6; hence x in { (seq . k1) where k1 is Element of NAT : j + n <= k1 } by A7; ::_thesis: verum end; then { (seq . (j + k)) where k is Element of NAT : n <= k } c= { (seq . k) where k is Element of NAT : j + n <= k } by TARSKI:def_3; then A9: { (seq . (j + k)) where k is Element of NAT : n <= k } = { (seq . k) where k is Element of NAT : j + n <= k } by A6, XBOOLE_0:def_10; now__::_thesis:_for_x_being_set_st_x_in__{__(seq_._(j_+_k))_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in__{__((seq_^\_j)_._k1)_where_k1_is_Element_of_NAT_:_n_<=_k1__}_ let x be set ; ::_thesis: ( x in { (seq . (j + k)) where k is Element of NAT : n <= k } implies x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } ) assume x in { (seq . (j + k)) where k is Element of NAT : n <= k } ; ::_thesis: x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } then consider k being Element of NAT such that A10: x = seq . (j + k) and A11: n <= k ; x = (seq ^\ j) . k by A10, NAT_1:def_3; hence x in { ((seq ^\ j) . k1) where k1 is Element of NAT : n <= k1 } by A11; ::_thesis: verum end; then A12: { (seq . (j + k)) where k is Element of NAT : n <= k } c= { ((seq ^\ j) . k) where k is Element of NAT : n <= k } by TARSKI:def_3; now__::_thesis:_for_x_being_set_st_x_in__{__((seq_^\_j)_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in__{__(seq_._(j_+_k1))_where_k1_is_Element_of_NAT_:_n_<=_k1__}_ let x be set ; ::_thesis: ( x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } implies x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } ) assume x in { ((seq ^\ j) . k) where k is Element of NAT : n <= k } ; ::_thesis: x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } then consider k being Element of NAT such that A13: x = (seq ^\ j) . k and A14: n <= k ; x = seq . (j + k) by A13, NAT_1:def_3; hence x in { (seq . (j + k1)) where k1 is Element of NAT : n <= k1 } by A14; ::_thesis: verum end; then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } c= { (seq . (j + k)) where k is Element of NAT : n <= k } by TARSKI:def_3; then { ((seq ^\ j) . k) where k is Element of NAT : n <= k } = { (seq . (j + k)) where k is Element of NAT : n <= k } by A12, XBOOLE_0:def_10; hence (inferior_realsequence (seq ^\ j)) . n = ((inferior_realsequence seq) ^\ j) . n by A1, A2, A9, NAT_1:def_3; ::_thesis: verum end; then (inferior_realsequence seq) ^\ j = inferior_realsequence (seq ^\ j) by FUNCT_2:63; hence ( inferior_realsequence (seq ^\ j) = (inferior_realsequence seq) ^\ j & lim_inf (seq ^\ j) = lim_inf seq ) by Th26; ::_thesis: verum end; theorem Th30: :: RINFSUP2:30 for seq being ExtREAL_sequence for k being Element of NAT st seq is non-increasing & -infty < seq . k & seq . k < +infty holds ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) proof let seq be ExtREAL_sequence; ::_thesis: for k being Element of NAT st seq is non-increasing & -infty < seq . k & seq . k < +infty holds ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) let k be Element of NAT ; ::_thesis: ( seq is non-increasing & -infty < seq . k & seq . k < +infty implies ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) ) assume that A1: seq is non-increasing and A2: -infty < seq . k and A3: seq . k < +infty ; ::_thesis: ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) set seq0 = seq ^\ k; now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(seq_^\_k)_holds_ y_<=_seq_._k let y be ext-real number ; ::_thesis: ( y in rng (seq ^\ k) implies y <= seq . k ) assume y in rng (seq ^\ k) ; ::_thesis: y <= seq . k then consider n being set such that A4: n in dom (seq ^\ k) and A5: y = (seq ^\ k) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A4; k <= n + k by NAT_1:11; then seq . (n + k) <= seq . k by A1, Th7; hence y <= seq . k by A5, NAT_1:def_3; ::_thesis: verum end; then A6: seq . k is UpperBound of rng (seq ^\ k) by XXREAL_2:def_1; (seq ^\ k) . 0 = seq . (0 + k) by NAT_1:def_3; then A7: seq . k in rng (seq ^\ k) by FUNCT_2:4; seq . k in REAL by A2, A3, XXREAL_0:14; then rng (seq ^\ k) is bounded_above by A6, XXREAL_2:def_10; hence ( seq ^\ k is bounded_above & sup (seq ^\ k) = seq . k ) by A6, A7, Def4, XXREAL_2:55; ::_thesis: verum end; theorem Th31: :: RINFSUP2:31 for seq being ExtREAL_sequence for k being Element of NAT st seq is non-decreasing & -infty < seq . k & seq . k < +infty holds ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) proof let seq be ExtREAL_sequence; ::_thesis: for k being Element of NAT st seq is non-decreasing & -infty < seq . k & seq . k < +infty holds ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) let k be Element of NAT ; ::_thesis: ( seq is non-decreasing & -infty < seq . k & seq . k < +infty implies ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) ) assume that A1: seq is non-decreasing and A2: -infty < seq . k and A3: seq . k < +infty ; ::_thesis: ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) set seq0 = seq ^\ k; now__::_thesis:_for_y_being_ext-real_number_st_y_in_rng_(seq_^\_k)_holds_ seq_._k_<=_y let y be ext-real number ; ::_thesis: ( y in rng (seq ^\ k) implies seq . k <= y ) assume y in rng (seq ^\ k) ; ::_thesis: seq . k <= y then consider n being set such that A4: n in dom (seq ^\ k) and A5: y = (seq ^\ k) . n by FUNCT_1:def_3; reconsider n = n as Element of NAT by A4; k <= n + k by NAT_1:11; then seq . k <= seq . (n + k) by A1, Th7; hence seq . k <= y by A5, NAT_1:def_3; ::_thesis: verum end; then A6: seq . k is LowerBound of rng (seq ^\ k) by XXREAL_2:def_2; (seq ^\ k) . 0 = seq . (0 + k) by NAT_1:def_3; then A7: seq . k in rng (seq ^\ k) by FUNCT_2:4; seq . k in REAL by A2, A3, XXREAL_0:14; then rng (seq ^\ k) is bounded_below by A6, XXREAL_2:def_9; hence ( seq ^\ k is bounded_below & inf (seq ^\ k) = seq . k ) by A6, A7, Def3, XXREAL_2:56; ::_thesis: verum end; Lm3: for seq being ExtREAL_sequence st seq is bounded & seq is non-increasing holds ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is bounded & seq is non-increasing implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) ) assume that A1: seq is bounded and A2: seq is non-increasing ; ::_thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) reconsider rseq = seq as Real_Sequence by A1, Th11; A3: seq is bounded_below by A1, Def5; then A4: rseq is V65() by Th13; then lim rseq = lim_sup rseq by A2, RINFSUP1:89; then lim rseq = lower_bound rseq by A2, RINFSUP1:70; then A5: lim seq = lower_bound rseq by A2, A4, Th14; rng seq is bounded_below by A3, Def3; hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = inf seq ) by A2, A4, A5, Th3, Th14; ::_thesis: verum end; Lm4: for seq being ExtREAL_sequence st seq is bounded & seq is non-decreasing holds ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is bounded & seq is non-decreasing implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) ) assume that A1: seq is bounded and A2: seq is non-decreasing ; ::_thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) reconsider rseq = seq as Real_Sequence by A1, Th11; A3: seq is bounded_above by A1, Def5; then A4: rseq is V64() by Th12; then lim rseq = lim_inf rseq by A2, RINFSUP1:89; then lim rseq = upper_bound rseq by A2, RINFSUP1:64; then A5: lim seq = upper_bound rseq by A2, A4, Th14; rng seq is bounded_above by A3, Def4; hence ( seq is convergent_to_finite_number & seq is convergent & lim seq = sup seq ) by A2, A4, A5, Th1, Th14; ::_thesis: verum end; theorem Th32: :: RINFSUP2:32 for seq being ExtREAL_sequence st ( for n being Element of NAT holds +infty <= seq . n ) holds seq is convergent_to_+infty proof let seq be ExtREAL_sequence; ::_thesis: ( ( for n being Element of NAT holds +infty <= seq . n ) implies seq is convergent_to_+infty ) assume A1: for n being Element of NAT holds +infty <= seq . n ; ::_thesis: seq is convergent_to_+infty now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_ ex_n_being_Nat_st_ for_m_being_Nat_st_n_<=_m_holds_ g_<=_seq_._m let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st for m being Nat st n <= m holds g <= seq . m ) assume 0 < g ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds g <= seq . m now__::_thesis:_for_m_being_Nat_st_0_<=_m_holds_ g_<=_seq_._m let m be Nat; ::_thesis: ( 0 <= m implies g <= seq . m ) assume 0 <= m ; ::_thesis: g <= seq . m m is Element of NAT by ORDINAL1:def_12; then A2: +infty <= seq . m by A1; g <= +infty by XXREAL_0:3; hence g <= seq . m by A2, XXREAL_0:2; ::_thesis: verum end; hence ex n being Nat st for m being Nat st n <= m holds g <= seq . m ; ::_thesis: verum end; hence seq is convergent_to_+infty by MESFUNC5:def_9; ::_thesis: verum end; theorem Th33: :: RINFSUP2:33 for seq being ExtREAL_sequence st ( for n being Element of NAT holds seq . n <= -infty ) holds seq is convergent_to_-infty proof let seq be ExtREAL_sequence; ::_thesis: ( ( for n being Element of NAT holds seq . n <= -infty ) implies seq is convergent_to_-infty ) assume A1: for n being Element of NAT holds seq . n <= -infty ; ::_thesis: seq is convergent_to_-infty now__::_thesis:_for_g_being_real_number_st_g_<_0_holds_ ex_n_being_Nat_st_ for_m_being_Nat_st_n_<=_m_holds_ seq_._m_<=_g let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st for m being Nat st n <= m holds seq . m <= g ) assume g < 0 ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds seq . m <= g now__::_thesis:_for_m_being_Nat_st_0_<=_m_holds_ seq_._m_<=_g let m be Nat; ::_thesis: ( 0 <= m implies seq . m <= g ) assume 0 <= m ; ::_thesis: seq . m <= g m is Element of NAT by ORDINAL1:def_12; then A2: seq . m <= -infty by A1; -infty <= g by XXREAL_0:5; hence seq . m <= g by A2, XXREAL_0:2; ::_thesis: verum end; hence ex n being Nat st for m being Nat st n <= m holds seq . m <= g ; ::_thesis: verum end; hence seq is convergent_to_-infty by MESFUNC5:def_10; ::_thesis: verum end; theorem Th34: :: RINFSUP2:34 for seq being ExtREAL_sequence st seq is non-increasing & -infty = inf seq holds ( seq is convergent_to_-infty & lim seq = -infty ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is non-increasing & -infty = inf seq implies ( seq is convergent_to_-infty & lim seq = -infty ) ) assume that A1: seq is non-increasing and A2: -infty = inf seq ; ::_thesis: ( seq is convergent_to_-infty & lim seq = -infty ) A3: seq is convergent_to_-infty proof assume not seq is convergent_to_-infty ; ::_thesis: contradiction then consider g being real number such that g < 0 and A4: for n being Nat ex m being Nat st ( n <= m & g < seq . m ) by MESFUNC5:def_10; for y being ext-real number st y in rng seq holds g <= y proof let y be ext-real number ; ::_thesis: ( y in rng seq implies g <= y ) assume y in rng seq ; ::_thesis: g <= y then consider n being set such that A5: n in NAT and A6: y = seq . n by FUNCT_2:11; reconsider n = n as Element of NAT by A5; consider m being Nat such that A7: n <= m and A8: g < seq . m by A4; m is Element of NAT by ORDINAL1:def_12; then seq . m <= seq . n by A1, A7, Th7; hence g <= y by A6, A8, XXREAL_0:2; ::_thesis: verum end; then g is LowerBound of rng seq by XXREAL_2:def_2; then A9: g <= inf (rng seq) by XXREAL_2:def_4; g in REAL by XREAL_0:def_1; hence contradiction by A2, A9, XXREAL_0:12; ::_thesis: verum end; then seq is convergent by MESFUNC5:def_11; hence ( seq is convergent_to_-infty & lim seq = -infty ) by A3, MESFUNC5:def_12; ::_thesis: verum end; theorem Th35: :: RINFSUP2:35 for seq being ExtREAL_sequence st seq is non-decreasing & +infty = sup seq holds ( seq is convergent_to_+infty & lim seq = +infty ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is non-decreasing & +infty = sup seq implies ( seq is convergent_to_+infty & lim seq = +infty ) ) assume that A1: seq is non-decreasing and A2: +infty = sup seq ; ::_thesis: ( seq is convergent_to_+infty & lim seq = +infty ) A3: seq is convergent_to_+infty proof assume not seq is convergent_to_+infty ; ::_thesis: contradiction then consider g being real number such that 0 < g and A4: for n being Nat ex m being Nat st ( n <= m & seq . m < g ) by MESFUNC5:def_9; for y being ext-real number st y in rng seq holds y <= g proof let y be ext-real number ; ::_thesis: ( y in rng seq implies y <= g ) assume y in rng seq ; ::_thesis: y <= g then consider n being set such that A5: n in NAT and A6: y = seq . n by FUNCT_2:11; reconsider n = n as Element of NAT by A5; consider m being Nat such that A7: n <= m and A8: seq . m < g by A4; m is Element of NAT by ORDINAL1:def_12; then seq . n <= seq . m by A1, A7, Th7; hence y <= g by A6, A8, XXREAL_0:2; ::_thesis: verum end; then g is UpperBound of rng seq by XXREAL_2:def_1; then A9: sup (rng seq) <= g by XXREAL_2:def_3; g in REAL by XREAL_0:def_1; hence contradiction by A2, A9, XXREAL_0:9; ::_thesis: verum end; then seq is convergent by MESFUNC5:def_11; hence ( seq is convergent_to_+infty & lim seq = +infty ) by A3, MESFUNC5:def_12; ::_thesis: verum end; theorem Th36: :: RINFSUP2:36 for seq being ExtREAL_sequence st seq is non-increasing holds ( seq is convergent & lim seq = inf seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is non-increasing implies ( seq is convergent & lim seq = inf seq ) ) assume A1: seq is non-increasing ; ::_thesis: ( seq is convergent & lim seq = inf seq ) percases ( for n being Element of NAT holds +infty <= seq . n or ex n being Element of NAT st not +infty <= seq . n ) ; supposeA2: for n being Element of NAT holds +infty <= seq . n ; ::_thesis: ( seq is convergent & lim seq = inf seq ) now__::_thesis:_for_y_being_set_st_y_in_{+infty}_holds_ y_in_rng_seq let y be set ; ::_thesis: ( y in {+infty} implies y in rng seq ) assume y in {+infty} ; ::_thesis: y in rng seq then A3: y = +infty by TARSKI:def_1; now__::_thesis:_y_in_rng_seq assume A4: not y in rng seq ; ::_thesis: contradiction now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction let n be Element of NAT ; ::_thesis: contradiction n in NAT ; then n in dom seq by FUNCT_2:def_1; then seq . n <> +infty by A3, A4, FUNCT_1:def_3; hence contradiction by A2, XXREAL_0:4; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; hence y in rng seq ; ::_thesis: verum end; then A5: {+infty} c= rng seq by TARSKI:def_3; A6: seq is convergent_to_+infty by A2, Th32; hence A7: seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = inf seq now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_ y_in_{+infty} let y be set ; ::_thesis: ( y in rng seq implies y in {+infty} ) assume y in rng seq ; ::_thesis: y in {+infty} then ex x being set st ( x in dom seq & seq . x = y ) by FUNCT_1:def_3; then y = +infty by A2, XXREAL_0:4; hence y in {+infty} by TARSKI:def_1; ::_thesis: verum end; then rng seq c= {+infty} by TARSKI:def_3; then rng seq = {+infty} by A5, XBOOLE_0:def_10; then inf seq = +infty by XXREAL_2:13; hence lim seq = inf seq by A6, A7, MESFUNC5:def_12; ::_thesis: verum end; suppose not for n being Element of NAT holds +infty <= seq . n ; ::_thesis: ( seq is convergent & lim seq = inf seq ) then consider k being Element of NAT such that A8: seq . k < +infty ; percases ( -infty <> inf seq or -infty = inf seq ) ; supposeA9: -infty <> inf seq ; ::_thesis: ( seq is convergent & lim seq = inf seq ) set seq0 = seq ^\ k; A10: inf seq = inf (seq ^\ k) by A1, Th25; A11: now__::_thesis:_not_rng_(seq_^\_k)_=_{-infty} assume rng (seq ^\ k) = {-infty} ; ::_thesis: contradiction then A12: -infty in rng (seq ^\ k) by TARSKI:def_1; -infty is LowerBound of rng (seq ^\ k) by XXREAL_2:42; hence contradiction by A9, A10, A12, XXREAL_2:56; ::_thesis: verum end; A13: inf (seq ^\ k) <= sup (seq ^\ k) by Th24; A14: inf (rng (seq ^\ k)) is LowerBound of rng (seq ^\ k) by XXREAL_2:def_4; inf seq <= seq . k by Th23; then -infty < seq . k by A9, XXREAL_0:2, XXREAL_0:6; then A15: seq ^\ k is bounded_above by A1, A8, Th30; then rng (seq ^\ k) is bounded_above by Def4; then sup (rng (seq ^\ k)) < +infty by A11, XXREAL_0:9, XXREAL_2:57; then inf (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14; then rng (seq ^\ k) is bounded_below by A14, XXREAL_2:def_9; then seq ^\ k is bounded_below by Def3; then A16: seq ^\ k is bounded by A15, Def5; A17: seq ^\ k is non-increasing by A1, Th25; then A18: lim (seq ^\ k) = inf (seq ^\ k) by A16, Lm3; seq ^\ k is convergent by A17, A16, Lm3; hence ( seq is convergent & lim seq = inf seq ) by A10, A18, Th17; ::_thesis: verum end; supposeA19: -infty = inf seq ; ::_thesis: ( seq is convergent & lim seq = inf seq ) then seq is convergent_to_-infty by A1, Th34; hence seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = inf seq thus lim seq = inf seq by A1, A19, Th34; ::_thesis: verum end; end; end; end; end; theorem Th37: :: RINFSUP2:37 for seq being ExtREAL_sequence st seq is non-decreasing holds ( seq is convergent & lim seq = sup seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is non-decreasing implies ( seq is convergent & lim seq = sup seq ) ) assume A1: seq is non-decreasing ; ::_thesis: ( seq is convergent & lim seq = sup seq ) percases ( for n being Element of NAT holds seq . n <= -infty or ex n being Element of NAT st not seq . n <= -infty ) ; supposeA2: for n being Element of NAT holds seq . n <= -infty ; ::_thesis: ( seq is convergent & lim seq = sup seq ) now__::_thesis:_for_y_being_set_st_y_in_{-infty}_holds_ y_in_rng_seq let y be set ; ::_thesis: ( y in {-infty} implies y in rng seq ) assume y in {-infty} ; ::_thesis: y in rng seq then A3: y = -infty by TARSKI:def_1; now__::_thesis:_y_in_rng_seq assume A4: not y in rng seq ; ::_thesis: contradiction now__::_thesis:_for_n_being_Element_of_NAT_holds_contradiction let n be Element of NAT ; ::_thesis: contradiction n in NAT ; then n in dom seq by FUNCT_2:def_1; then seq . n <> -infty by A3, A4, FUNCT_1:def_3; hence contradiction by A2, XXREAL_0:6; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; hence y in rng seq ; ::_thesis: verum end; then A5: {-infty} c= rng seq by TARSKI:def_3; A6: seq is convergent_to_-infty by A2, Th33; hence A7: seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = sup seq now__::_thesis:_for_y_being_set_st_y_in_rng_seq_holds_ y_in_{-infty} let y be set ; ::_thesis: ( y in rng seq implies y in {-infty} ) assume y in rng seq ; ::_thesis: y in {-infty} then ex x being set st ( x in dom seq & seq . x = y ) by FUNCT_1:def_3; then y = -infty by A2, XXREAL_0:6; hence y in {-infty} by TARSKI:def_1; ::_thesis: verum end; then rng seq c= {-infty} by TARSKI:def_3; then rng seq = {-infty} by A5, XBOOLE_0:def_10; then sup seq = -infty by XXREAL_2:11; hence lim seq = sup seq by A6, A7, MESFUNC5:def_12; ::_thesis: verum end; suppose not for n being Element of NAT holds seq . n <= -infty ; ::_thesis: ( seq is convergent & lim seq = sup seq ) then consider k being Element of NAT such that A8: -infty < seq . k ; percases ( +infty <> sup seq or +infty = sup seq ) ; supposeA9: +infty <> sup seq ; ::_thesis: ( seq is convergent & lim seq = sup seq ) set seq0 = seq ^\ k; A10: sup seq = sup (seq ^\ k) by A1, Th26; A11: now__::_thesis:_not_rng_(seq_^\_k)_=_{+infty} assume rng (seq ^\ k) = {+infty} ; ::_thesis: contradiction then A12: +infty in rng (seq ^\ k) by TARSKI:def_1; +infty is UpperBound of rng (seq ^\ k) by XXREAL_2:41; hence contradiction by A9, A10, A12, XXREAL_2:55; ::_thesis: verum end; A13: inf (seq ^\ k) <= sup (seq ^\ k) by Th24; A14: sup (rng (seq ^\ k)) is UpperBound of rng (seq ^\ k) by XXREAL_2:def_3; seq . k <= sup seq by Th23; then seq . k < +infty by A9, XXREAL_0:2, XXREAL_0:4; then A15: seq ^\ k is bounded_below by A1, A8, Th31; then rng (seq ^\ k) is bounded_below by Def3; then -infty < inf (rng (seq ^\ k)) by A11, XXREAL_0:12, XXREAL_2:58; then sup (rng (seq ^\ k)) in REAL by A9, A10, A13, XXREAL_0:14; then rng (seq ^\ k) is bounded_above by A14, XXREAL_2:def_10; then seq ^\ k is bounded_above by Def4; then A16: seq ^\ k is bounded by A15, Def5; A17: seq ^\ k is non-decreasing by A1, Th26; then A18: lim (seq ^\ k) = sup (seq ^\ k) by A16, Lm4; seq ^\ k is convergent by A17, A16, Lm4; hence ( seq is convergent & lim seq = sup seq ) by A10, A18, Th17; ::_thesis: verum end; supposeA19: +infty = sup seq ; ::_thesis: ( seq is convergent & lim seq = sup seq ) then seq is convergent_to_+infty by A1, Th35; hence seq is convergent by MESFUNC5:def_11; ::_thesis: lim seq = sup seq thus lim seq = sup seq by A1, A19, Th35; ::_thesis: verum end; end; end; end; end; theorem Th38: :: RINFSUP2:38 for seq1, seq2 being ExtREAL_sequence st seq1 is convergent & seq2 is convergent & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) holds lim seq1 <= lim seq2 proof let seq1, seq2 be ExtREAL_sequence; ::_thesis: ( seq1 is convergent & seq2 is convergent & ( for n being Element of NAT holds seq1 . n <= seq2 . n ) implies lim seq1 <= lim seq2 ) assume that A1: seq1 is convergent and A2: seq2 is convergent and A3: for n being Element of NAT holds seq1 . n <= seq2 . n ; ::_thesis: lim seq1 <= lim seq2 percases ( seq1 is convergent_to_finite_number or seq1 is convergent_to_+infty or seq1 is convergent_to_-infty ) by A1, MESFUNC5:def_11; supposeA4: seq1 is convergent_to_finite_number ; ::_thesis: lim seq1 <= lim seq2 A5: not seq2 is convergent_to_-infty proof assume A6: seq2 is convergent_to_-infty ; ::_thesis: contradiction now__::_thesis:_for_g_being_real_number_st_g_<_0_holds_ ex_n_being_Nat_st_ for_m_being_Nat_st_n_<=_m_holds_ seq1_._m_<=_g let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st for m being Nat st n <= m holds seq1 . m <= g ) assume g < 0 ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds seq1 . m <= g then consider n being Nat such that A7: for m being Nat st n <= m holds seq2 . m <= g by A6, MESFUNC5:def_10; now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_ seq1_._m_<=_g let m be Nat; ::_thesis: ( n <= m implies seq1 . m <= g ) m is Element of NAT by ORDINAL1:def_12; then A8: seq1 . m <= seq2 . m by A3; assume n <= m ; ::_thesis: seq1 . m <= g then seq2 . m <= g by A7; hence seq1 . m <= g by A8, XXREAL_0:2; ::_thesis: verum end; hence ex n being Nat st for m being Nat st n <= m holds seq1 . m <= g ; ::_thesis: verum end; then seq1 is convergent_to_-infty by MESFUNC5:def_10; hence contradiction by A4, MESFUNC5:51; ::_thesis: verum end; percases ( seq2 is convergent_to_finite_number or seq2 is convergent_to_+infty ) by A2, A5, MESFUNC5:def_11; supposeA9: seq2 is convergent_to_finite_number ; ::_thesis: lim seq1 <= lim seq2 consider k1 being Element of NAT such that A10: seq1 ^\ k1 is bounded by A4, Th19; seq1 ^\ k1 is bounded_above by A10, Def5; then rng (seq1 ^\ k1) is bounded_above by Def4; then consider UB being real number such that A11: UB is UpperBound of rng (seq1 ^\ k1) by XXREAL_2:def_10; consider k2 being Element of NAT such that A12: seq2 ^\ k2 is bounded by A9, Th19; reconsider k = max (k1,k2) as Element of NAT ; A13: lim seq2 = lim (seq2 ^\ k) by A9, Th20; A14: dom (seq1 ^\ k1) = NAT by FUNCT_2:def_1; now__::_thesis:_for_y_being_set_st_y_in_rng_(seq1_^\_k)_holds_ y_in_rng_(seq1_^\_k1) reconsider k2 = k - k1 as Element of NAT by INT_1:5, XXREAL_0:25; let y be set ; ::_thesis: ( y in rng (seq1 ^\ k) implies y in rng (seq1 ^\ k1) ) assume y in rng (seq1 ^\ k) ; ::_thesis: y in rng (seq1 ^\ k1) then consider n being set such that A15: n in dom (seq1 ^\ k) and A16: (seq1 ^\ k) . n = y by FUNCT_1:def_3; reconsider n = n as Element of NAT by A15; y = seq1 . (k + n) by A16, NAT_1:def_3; then y = seq1 . (k1 + (k2 + n)) ; then y = (seq1 ^\ k1) . (k2 + n) by NAT_1:def_3; hence y in rng (seq1 ^\ k1) by A14, FUNCT_1:def_3; ::_thesis: verum end; then A17: rng (seq1 ^\ k) c= rng (seq1 ^\ k1) by TARSKI:def_3; then UB is UpperBound of rng (seq1 ^\ k) by A11, XXREAL_2:6; then rng (seq1 ^\ k) is bounded_above by XXREAL_2:def_10; then A18: seq1 ^\ k is bounded_above by Def4; seq1 ^\ k1 is bounded_below by A10, Def5; then rng (seq1 ^\ k1) is bounded_below by Def3; then consider LB being real number such that A19: LB is LowerBound of rng (seq1 ^\ k1) by XXREAL_2:def_9; LB is LowerBound of rng (seq1 ^\ k) by A17, A19, XXREAL_2:5; then rng (seq1 ^\ k) is bounded_below by XXREAL_2:def_9; then seq1 ^\ k is bounded_below by Def3; then seq1 ^\ k is bounded by A18, Def5; then reconsider rseq1 = seq1 ^\ k as Real_Sequence by Th11; seq2 ^\ k2 is bounded_below by A12, Def5; then rng (seq2 ^\ k2) is bounded_below by Def3; then consider LB being real number such that A20: LB is LowerBound of rng (seq2 ^\ k2) by XXREAL_2:def_9; A21: lim seq1 = lim (seq1 ^\ k) by A4, Th20; seq2 ^\ k2 is bounded_above by A12, Def5; then rng (seq2 ^\ k2) is bounded_above by Def4; then consider UB being real number such that A22: UB is UpperBound of rng (seq2 ^\ k2) by XXREAL_2:def_10; A23: dom (seq2 ^\ k2) = NAT by FUNCT_2:def_1; now__::_thesis:_for_y_being_set_st_y_in_rng_(seq2_^\_k)_holds_ y_in_rng_(seq2_^\_k2) reconsider k3 = k - k2 as Element of NAT by INT_1:5, XXREAL_0:25; let y be set ; ::_thesis: ( y in rng (seq2 ^\ k) implies y in rng (seq2 ^\ k2) ) assume y in rng (seq2 ^\ k) ; ::_thesis: y in rng (seq2 ^\ k2) then consider n being set such that A24: n in dom (seq2 ^\ k) and A25: (seq2 ^\ k) . n = y by FUNCT_1:def_3; reconsider n = n as Element of NAT by A24; y = seq2 . (k + n) by A25, NAT_1:def_3; then y = seq2 . (k2 + (k3 + n)) ; then y = (seq2 ^\ k2) . (k3 + n) by NAT_1:def_3; hence y in rng (seq2 ^\ k2) by A23, FUNCT_1:def_3; ::_thesis: verum end; then A26: rng (seq2 ^\ k) c= rng (seq2 ^\ k2) by TARSKI:def_3; then UB is UpperBound of rng (seq2 ^\ k) by A22, XXREAL_2:6; then rng (seq2 ^\ k) is bounded_above by XXREAL_2:def_10; then A27: seq2 ^\ k is bounded_above by Def4; LB is LowerBound of rng (seq2 ^\ k) by A20, A26, XXREAL_2:5; then rng (seq2 ^\ k) is bounded_below by XXREAL_2:def_9; then seq2 ^\ k is bounded_below by Def3; then seq2 ^\ k is bounded by A27, Def5; then reconsider rseq2 = seq2 ^\ k as Real_Sequence by Th11; A28: seq2 ^\ k is convergent_to_finite_number by A9, Th20; then A29: rseq2 is convergent by Th15; A30: for n being Element of NAT holds rseq1 . n <= rseq2 . n proof let n be Element of NAT ; ::_thesis: rseq1 . n <= rseq2 . n A31: (seq2 ^\ k) . n = seq2 . (k + n) by NAT_1:def_3; (seq1 ^\ k) . n = seq1 . (k + n) by NAT_1:def_3; hence rseq1 . n <= rseq2 . n by A3, A31; ::_thesis: verum end; A32: seq1 ^\ k is convergent_to_finite_number by A4, Th20; then A33: lim (seq1 ^\ k) = lim rseq1 by Th15; A34: lim (seq2 ^\ k) = lim rseq2 by A28, Th15; rseq1 is convergent by A32, Th15; hence lim seq1 <= lim seq2 by A29, A33, A34, A30, A21, A13, SEQ_2:18; ::_thesis: verum end; supposeA35: seq2 is convergent_to_+infty ; ::_thesis: lim seq1 <= lim seq2 then seq2 is convergent by MESFUNC5:def_11; then lim seq2 = +infty by A35, MESFUNC5:def_12; hence lim seq1 <= lim seq2 by XXREAL_0:3; ::_thesis: verum end; end; end; supposeA36: seq1 is convergent_to_+infty ; ::_thesis: lim seq1 <= lim seq2 now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_ ex_n_being_Nat_st_ for_m_being_Nat_st_n_<=_m_holds_ g_<=_seq2_._m let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st for m being Nat st n <= m holds g <= seq2 . m ) assume 0 < g ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds g <= seq2 . m then consider n being Nat such that A37: for m being Nat st n <= m holds g <= seq1 . m by A36, MESFUNC5:def_9; now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_ g_<=_seq2_._m let m be Nat; ::_thesis: ( n <= m implies g <= seq2 . m ) m is Element of NAT by ORDINAL1:def_12; then A38: seq1 . m <= seq2 . m by A3; assume n <= m ; ::_thesis: g <= seq2 . m then g <= seq1 . m by A37; hence g <= seq2 . m by A38, XXREAL_0:2; ::_thesis: verum end; hence ex n being Nat st for m being Nat st n <= m holds g <= seq2 . m ; ::_thesis: verum end; then A39: seq2 is convergent_to_+infty by MESFUNC5:def_9; then seq2 is convergent by MESFUNC5:def_11; then lim seq2 = +infty by A39, MESFUNC5:def_12; hence lim seq1 <= lim seq2 by XXREAL_0:3; ::_thesis: verum end; supposeA40: seq1 is convergent_to_-infty ; ::_thesis: lim seq1 <= lim seq2 then seq1 is convergent by MESFUNC5:def_11; then lim seq1 = -infty by A40, MESFUNC5:def_12; hence lim seq1 <= lim seq2 by XXREAL_0:5; ::_thesis: verum end; end; end; theorem :: RINFSUP2:39 for seq being ExtREAL_sequence holds lim_inf seq <= lim_sup seq proof let seq be ExtREAL_sequence; ::_thesis: lim_inf seq <= lim_sup seq A1: lim (superior_realsequence seq) = lim_sup seq by Th36; A2: inferior_realsequence seq is convergent by Th37; A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_realsequence_seq)_._n_<=_(superior_realsequence_seq)_._n let n be Element of NAT ; ::_thesis: (inferior_realsequence seq) . n <= (superior_realsequence seq) . n A4: seq . n <= (superior_realsequence seq) . n by Th8; (inferior_realsequence seq) . n <= seq . n by Th8; hence (inferior_realsequence seq) . n <= (superior_realsequence seq) . n by A4, XXREAL_0:2; ::_thesis: verum end; A5: lim (inferior_realsequence seq) = lim_inf seq by Th37; superior_realsequence seq is convergent by Th36; hence lim_inf seq <= lim_sup seq by A1, A2, A5, A3, Th38; ::_thesis: verum end; Lm5: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = +infty holds ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( lim_inf seq = lim_sup seq & lim_inf seq = +infty implies ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) ) assume that A1: lim_inf seq = lim_sup seq and A2: lim_inf seq = +infty ; ::_thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) A3: inferior_realsequence seq is convergent_to_+infty by A2, Th35; now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_ ex_n_being_Nat_st_ for_m_being_Nat_st_n_<=_m_holds_ g_<=_seq_._m let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st for m being Nat st n <= m holds g <= seq . m ) assume 0 < g ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds g <= seq . m then consider n being Nat such that A4: for m being Nat st n <= m holds g <= (inferior_realsequence seq) . m by A3, MESFUNC5:def_9; now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_ g_<=_seq_._m let m be Nat; ::_thesis: ( n <= m implies g <= seq . m ) m is Element of NAT by ORDINAL1:def_12; then A5: (inferior_realsequence seq) . m <= seq . m by Th8; assume n <= m ; ::_thesis: g <= seq . m then g <= (inferior_realsequence seq) . m by A4; hence g <= seq . m by A5, XXREAL_0:2; ::_thesis: verum end; hence ex n being Nat st for m being Nat st n <= m holds g <= seq . m ; ::_thesis: verum end; then A6: seq is convergent_to_+infty by MESFUNC5:def_9; then seq is convergent by MESFUNC5:def_11; hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, A2, A6, MESFUNC5:def_12; ::_thesis: verum end; Lm6: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq = -infty holds ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( lim_inf seq = lim_sup seq & lim_inf seq = -infty implies ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) ) assume that A1: lim_inf seq = lim_sup seq and A2: lim_inf seq = -infty ; ::_thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) A3: superior_realsequence seq is convergent_to_-infty by A1, A2, Th34; now__::_thesis:_for_g_being_real_number_st_g_<_0_holds_ ex_n_being_Nat_st_ for_m_being_Nat_st_n_<=_m_holds_ seq_._m_<=_g let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st for m being Nat st n <= m holds seq . m <= g ) assume g < 0 ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds seq . m <= g then consider n being Nat such that A4: for m being Nat st n <= m holds (superior_realsequence seq) . m <= g by A3, MESFUNC5:def_10; now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_ seq_._m_<=_g let m be Nat; ::_thesis: ( n <= m implies seq . m <= g ) m is Element of NAT by ORDINAL1:def_12; then A5: seq . m <= (superior_realsequence seq) . m by Th8; assume n <= m ; ::_thesis: seq . m <= g then (superior_realsequence seq) . m <= g by A4; hence seq . m <= g by A5, XXREAL_0:2; ::_thesis: verum end; hence ex n being Nat st for m being Nat st n <= m holds seq . m <= g ; ::_thesis: verum end; then A6: seq is convergent_to_-infty by MESFUNC5:def_10; then seq is convergent by MESFUNC5:def_11; hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, A2, A6, MESFUNC5:def_12; ::_thesis: verum end; Lm7: for seq being ExtREAL_sequence st lim_inf seq = lim_sup seq & lim_inf seq in REAL holds ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( lim_inf seq = lim_sup seq & lim_inf seq in REAL implies ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) ) assume that A1: lim_inf seq = lim_sup seq and A2: lim_inf seq in REAL ; ::_thesis: ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) consider k being Element of NAT such that A3: seq ^\ k is bounded by A1, A2, Th18; reconsider rseq0 = seq ^\ k as Real_Sequence by A3, Th11; seq ^\ k is bounded_below by A3, Def5; then A4: rseq0 is V65() by Th13; seq ^\ k is bounded_above by A3, Def5; then A5: rseq0 is V64() by Th12; then lim_sup rseq0 = lim_sup (seq ^\ k) by A4, Th9; then A6: lim_sup rseq0 = lim_sup seq by Th28; lim_inf rseq0 = lim_inf (seq ^\ k) by A5, A4, Th10; then A7: lim_inf rseq0 = lim_inf seq by Th29; then A8: rseq0 is convergent by A1, A5, A4, A6, RINFSUP1:88; then A9: lim rseq0 = lim_inf seq by A7, RINFSUP1:89; A10: seq ^\ k is convergent by A8, Th14; A11: lim rseq0 = lim (seq ^\ k) by A8, Th14; lim rseq0 = lim_sup seq by A6, A8, RINFSUP1:89; hence ( seq is convergent & lim seq = lim_inf seq & lim seq = lim_sup seq ) by A9, A11, A10, Th17; ::_thesis: verum end; theorem Th40: :: RINFSUP2:40 for seq being ExtREAL_sequence holds ( seq is convergent iff lim_inf seq = lim_sup seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent iff lim_inf seq = lim_sup seq ) set a = lim_inf seq; thus ( seq is convergent implies lim_inf seq = lim_sup seq ) ::_thesis: ( lim_inf seq = lim_sup seq implies seq is convergent ) proof assume A1: seq is convergent ; ::_thesis: lim_inf seq = lim_sup seq percases ( seq is convergent_to_finite_number or seq is convergent_to_-infty or seq is convergent_to_+infty ) by A1, MESFUNC5:def_11; supposeA2: seq is convergent_to_finite_number ; ::_thesis: lim_inf seq = lim_sup seq then consider k being Element of NAT such that A3: seq ^\ k is bounded by Th19; reconsider rseq0 = seq ^\ k as Real_Sequence by A3, Th11; seq ^\ k is convergent_to_finite_number by A2, Th20; then A4: rseq0 is convergent by Th15; then A5: rseq0 is bounded ; then lim_sup rseq0 = lim_sup (seq ^\ k) by Th9; then A6: lim_sup rseq0 = lim_sup seq by Th28; lim_inf rseq0 = lim_inf (seq ^\ k) by A5, Th10; then lim_inf rseq0 = lim_inf seq by Th29; hence lim_inf seq = lim_sup seq by A4, A6, RINFSUP1:88; ::_thesis: verum end; supposeA7: seq is convergent_to_-infty ; ::_thesis: lim_inf seq = lim_sup seq now__::_thesis:_for_g_being_real_number_st_g_<_0_holds_ ex_n_being_Nat_st_ for_m_being_Nat_st_n_<=_m_holds_ (inferior_realsequence_seq)_._m_<=_g let g be real number ; ::_thesis: ( g < 0 implies ex n being Nat st for m being Nat st n <= m holds (inferior_realsequence seq) . m <= g ) assume g < 0 ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds (inferior_realsequence seq) . m <= g then consider n being Nat such that A8: for m being Nat st n <= m holds seq . m <= g by A7, MESFUNC5:def_10; now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_ (inferior_realsequence_seq)_._m_<=_g let m be Nat; ::_thesis: ( n <= m implies (inferior_realsequence seq) . m <= g ) m is Element of NAT by ORDINAL1:def_12; then A9: (inferior_realsequence seq) . m <= seq . m by Th8; assume n <= m ; ::_thesis: (inferior_realsequence seq) . m <= g then seq . m <= g by A8; hence (inferior_realsequence seq) . m <= g by A9, XXREAL_0:2; ::_thesis: verum end; hence ex n being Nat st for m being Nat st n <= m holds (inferior_realsequence seq) . m <= g ; ::_thesis: verum end; then A10: inferior_realsequence seq is convergent_to_-infty by MESFUNC5:def_10; then inferior_realsequence seq is convergent by MESFUNC5:def_11; then lim (inferior_realsequence seq) = -infty by A10, MESFUNC5:def_12; then A11: lim_inf seq = -infty by Th37; A12: superior_realsequence seq is convergent_to_-infty proof set iseq = superior_realsequence seq; assume not superior_realsequence seq is convergent_to_-infty ; ::_thesis: contradiction then consider g being real number such that A13: g < 0 and A14: for n being Nat ex m being Nat st ( n <= m & g < (superior_realsequence seq) . m ) by MESFUNC5:def_10; consider N being Nat such that A15: for m being Nat st N <= m holds seq . m <= g by A7, A13, MESFUNC5:def_10; now__::_thesis:_for_m_being_Nat_st_N_<=_m_holds_ (superior_realsequence_seq)_._m_<=_g let m be Nat; ::_thesis: ( N <= m implies (superior_realsequence seq) . m <= g ) m is Element of NAT by ORDINAL1:def_12; then consider Y being non empty Subset of ExtREAL such that A16: Y = { (seq . k) where k is Element of NAT : m <= k } and A17: (superior_realsequence seq) . m = sup Y by Def7; assume A18: N <= m ; ::_thesis: (superior_realsequence seq) . m <= g now__::_thesis:_for_x_being_ext-real_number_st_x_in_Y_holds_ x_<=_g let x be ext-real number ; ::_thesis: ( x in Y implies x <= g ) assume x in Y ; ::_thesis: x <= g then consider k being Element of NAT such that A19: x = seq . k and A20: m <= k by A16; N <= k by A18, A20, XXREAL_0:2; hence x <= g by A15, A19; ::_thesis: verum end; then g is UpperBound of Y by XXREAL_2:def_1; hence (superior_realsequence seq) . m <= g by A17, XXREAL_2:def_3; ::_thesis: verum end; hence contradiction by A14; ::_thesis: verum end; then superior_realsequence seq is convergent by MESFUNC5:def_11; then lim (superior_realsequence seq) = -infty by A12, MESFUNC5:def_12; hence lim_inf seq = lim_sup seq by A11, Th36; ::_thesis: verum end; supposeA21: seq is convergent_to_+infty ; ::_thesis: lim_inf seq = lim_sup seq now__::_thesis:_for_g_being_real_number_st_0_<_g_holds_ ex_n_being_Nat_st_ for_m_being_Nat_st_n_<=_m_holds_ g_<=_(superior_realsequence_seq)_._m let g be real number ; ::_thesis: ( 0 < g implies ex n being Nat st for m being Nat st n <= m holds g <= (superior_realsequence seq) . m ) assume 0 < g ; ::_thesis: ex n being Nat st for m being Nat st n <= m holds g <= (superior_realsequence seq) . m then consider n being Nat such that A22: for m being Nat st n <= m holds g <= seq . m by A21, MESFUNC5:def_9; now__::_thesis:_for_m_being_Nat_st_n_<=_m_holds_ g_<=_(superior_realsequence_seq)_._m let m be Nat; ::_thesis: ( n <= m implies g <= (superior_realsequence seq) . m ) m is Element of NAT by ORDINAL1:def_12; then A23: seq . m <= (superior_realsequence seq) . m by Th8; assume n <= m ; ::_thesis: g <= (superior_realsequence seq) . m then g <= seq . m by A22; hence g <= (superior_realsequence seq) . m by A23, XXREAL_0:2; ::_thesis: verum end; hence ex n being Nat st for m being Nat st n <= m holds g <= (superior_realsequence seq) . m ; ::_thesis: verum end; then A24: superior_realsequence seq is convergent_to_+infty by MESFUNC5:def_9; then superior_realsequence seq is convergent by MESFUNC5:def_11; then lim (superior_realsequence seq) = +infty by A24, MESFUNC5:def_12; then A25: lim_sup seq = +infty by Th36; A26: inferior_realsequence seq is convergent_to_+infty proof set iseq = inferior_realsequence seq; assume not inferior_realsequence seq is convergent_to_+infty ; ::_thesis: contradiction then consider g being real number such that A27: 0 < g and A28: for n being Nat ex m being Nat st ( n <= m & (inferior_realsequence seq) . m < g ) by MESFUNC5:def_9; consider N being Nat such that A29: for m being Nat st N <= m holds g <= seq . m by A21, A27, MESFUNC5:def_9; now__::_thesis:_for_m_being_Nat_st_N_<=_m_holds_ g_<=_(inferior_realsequence_seq)_._m let m be Nat; ::_thesis: ( N <= m implies g <= (inferior_realsequence seq) . m ) m is Element of NAT by ORDINAL1:def_12; then consider Y being non empty Subset of ExtREAL such that A30: Y = { (seq . k) where k is Element of NAT : m <= k } and A31: (inferior_realsequence seq) . m = inf Y by Def6; assume A32: N <= m ; ::_thesis: g <= (inferior_realsequence seq) . m now__::_thesis:_for_x_being_ext-real_number_st_x_in_Y_holds_ g_<=_x let x be ext-real number ; ::_thesis: ( x in Y implies g <= x ) assume x in Y ; ::_thesis: g <= x then consider k being Element of NAT such that A33: x = seq . k and A34: m <= k by A30; N <= k by A32, A34, XXREAL_0:2; hence g <= x by A29, A33; ::_thesis: verum end; then g is LowerBound of Y by XXREAL_2:def_2; hence g <= (inferior_realsequence seq) . m by A31, XXREAL_2:def_4; ::_thesis: verum end; hence contradiction by A28; ::_thesis: verum end; then inferior_realsequence seq is convergent by MESFUNC5:def_11; then lim (inferior_realsequence seq) = +infty by A26, MESFUNC5:def_12; hence lim_inf seq = lim_sup seq by A25, Th37; ::_thesis: verum end; end; end; assume A35: lim_inf seq = lim_sup seq ; ::_thesis: seq is convergent percases ( lim_inf seq in REAL or lim_inf seq = +infty or lim_inf seq = -infty ) by XXREAL_0:14; suppose lim_inf seq in REAL ; ::_thesis: seq is convergent hence seq is convergent by A35, Lm7; ::_thesis: verum end; suppose lim_inf seq = +infty ; ::_thesis: seq is convergent hence seq is convergent by A35, Lm5; ::_thesis: verum end; suppose lim_inf seq = -infty ; ::_thesis: seq is convergent hence seq is convergent by A35, Lm6; ::_thesis: verum end; end; end; theorem :: RINFSUP2:41 for seq being ExtREAL_sequence st seq is convergent holds ( lim seq = lim_inf seq & lim seq = lim_sup seq ) proof let seq be ExtREAL_sequence; ::_thesis: ( seq is convergent implies ( lim seq = lim_inf seq & lim seq = lim_sup seq ) ) set a = lim_inf seq; assume seq is convergent ; ::_thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq ) then A1: lim_inf seq = lim_sup seq by Th40; percases ( lim_inf seq in REAL or lim_inf seq = +infty or lim_inf seq = -infty ) by XXREAL_0:14; suppose lim_inf seq in REAL ; ::_thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq ) hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm7; ::_thesis: verum end; suppose lim_inf seq = +infty ; ::_thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq ) hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm5; ::_thesis: verum end; suppose lim_inf seq = -infty ; ::_thesis: ( lim seq = lim_inf seq & lim seq = lim_sup seq ) hence ( lim seq = lim_inf seq & lim seq = lim_sup seq ) by A1, Lm6; ::_thesis: verum end; end; end;