:: The Limit of a Real Function at Infinity. Halflines. Real Sequence Divergent to Infinity :: by Jaros{\l}aw Kotowicz :: :: Received August 20, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for g, r, r1 being real number st 0 < g & r <= r1 holds ( r - g < r1 & r < r1 + g ) proofend; Lm2: for seq being Real_Sequence for f1, f2 being PartFunc of REAL,REAL st rng seq c= dom (f1 + f2) holds ( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 ) proofend; Lm3: for seq being Real_Sequence for f1, f2 being PartFunc of REAL,REAL st rng seq c= dom (f1 (#) f2) holds ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 ) proofend; notation let r be real number ; synonym left_open_halfline r for halfline r; end; definition let r be real number ; func left_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 1 ].-infty,r.]; coherence ].-infty,r.] is Subset of REAL proofend; func right_closed_halfline r -> Subset of REAL equals :: LIMFUNC1:def 2 [.r,+infty.[; coherence [.r,+infty.[ is Subset of REAL proofend; func right_open_halfline r -> Subset of REAL equals :: LIMFUNC1:def 3 ].r,+infty.[; coherence ].r,+infty.[ is Subset of REAL proofend; end; :: deftheorem defines left_closed_halfline LIMFUNC1:def_1_:_ for r being real number holds left_closed_halfline r = ].-infty,r.]; :: deftheorem defines right_closed_halfline LIMFUNC1:def_2_:_ for r being real number holds right_closed_halfline r = [.r,+infty.[; :: deftheorem defines right_open_halfline LIMFUNC1:def_3_:_ for r being real number holds right_open_halfline r = ].r,+infty.[; theorem :: LIMFUNC1:1 for seq being Real_Sequence holds ( ( seq is non-decreasing implies seq is bounded_below ) & ( seq is non-increasing implies seq is bounded_above ) ) proofend; theorem Th2: :: LIMFUNC1:2 for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing holds for n being Element of NAT holds seq . n < 0 proofend; theorem Th3: :: LIMFUNC1:3 for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing holds for n being Element of NAT holds 0 < seq . n proofend; theorem Th4: :: LIMFUNC1:4 for seq being Real_Sequence st seq is convergent & 0 < lim seq holds ex n being Element of NAT st for m being Element of NAT st n <= m holds 0 < seq . m proofend; theorem Th5: :: LIMFUNC1:5 for seq being Real_Sequence st seq is convergent & 0 < lim seq holds ex n being Element of NAT st for m being Element of NAT st n <= m holds (lim seq) / 2 < seq . m proofend; definition let seq be Real_Sequence; attrseq is divergent_to+infty means :Def4: :: LIMFUNC1:def 4 for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds r < seq . m; attrseq is divergent_to-infty means :Def5: :: LIMFUNC1:def 5 for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds seq . m < r; end; :: deftheorem Def4 defines divergent_to+infty LIMFUNC1:def_4_:_ for seq being Real_Sequence holds ( seq is divergent_to+infty iff for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds r < seq . m ); :: deftheorem Def5 defines divergent_to-infty LIMFUNC1:def_5_:_ for seq being Real_Sequence holds ( seq is divergent_to-infty iff for r being Real ex n being Element of NAT st for m being Element of NAT st n <= m holds seq . m < r ); theorem :: LIMFUNC1:6 for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds ex n being Element of NAT st for m being Element of NAT st n <= m holds seq ^\ m is non-zero proofend; theorem Th7: :: LIMFUNC1:7 for k being Element of NAT for seq being Real_Sequence holds ( ( seq ^\ k is divergent_to+infty implies seq is divergent_to+infty ) & ( seq ^\ k is divergent_to-infty implies seq is divergent_to-infty ) ) proofend; theorem Th8: :: LIMFUNC1:8 for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds seq1 + seq2 is divergent_to+infty proofend; theorem Th9: :: LIMFUNC1:9 for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is bounded_below holds seq1 + seq2 is divergent_to+infty proofend; theorem Th10: :: LIMFUNC1:10 for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is divergent_to+infty holds seq1 (#) seq2 is divergent_to+infty proofend; theorem Th11: :: LIMFUNC1:11 for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds seq1 + seq2 is divergent_to-infty proofend; theorem Th12: :: LIMFUNC1:12 for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is bounded_above holds seq1 + seq2 is divergent_to-infty proofend; theorem Th13: :: LIMFUNC1:13 for seq being Real_Sequence for r being Real holds ( ( seq is divergent_to+infty & r > 0 implies r (#) seq is divergent_to+infty ) & ( seq is divergent_to+infty & r < 0 implies r (#) seq is divergent_to-infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) ) proofend; theorem Th14: :: LIMFUNC1:14 for seq being Real_Sequence for r being Real holds ( ( seq is divergent_to-infty & r > 0 implies r (#) seq is divergent_to-infty ) & ( seq is divergent_to-infty & r < 0 implies r (#) seq is divergent_to+infty ) & ( r = 0 implies ( rng (r (#) seq) = {0} & r (#) seq is constant ) ) ) proofend; theorem :: LIMFUNC1:15 for seq being Real_Sequence holds ( ( seq is divergent_to+infty implies - seq is divergent_to-infty ) & ( seq is divergent_to-infty implies - seq is divergent_to+infty ) ) proofend; theorem :: LIMFUNC1:16 for seq, seq1 being Real_Sequence st seq is bounded_below & seq1 is divergent_to-infty holds seq - seq1 is divergent_to+infty proofend; theorem :: LIMFUNC1:17 for seq, seq1 being Real_Sequence st seq is bounded_above & seq1 is divergent_to+infty holds seq - seq1 is divergent_to-infty proofend; theorem :: LIMFUNC1:18 for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is convergent holds seq + seq1 is divergent_to+infty by Th9; theorem :: LIMFUNC1:19 for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is convergent holds seq + seq1 is divergent_to-infty by Th12; theorem Th20: :: LIMFUNC1:20 for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = n ) holds seq is divergent_to+infty proofend; set s1 = incl NAT; Lm4: for n being Element of NAT holds (incl NAT) . n = n by FUNCT_1:18; theorem Th21: :: LIMFUNC1:21 for seq being Real_Sequence st ( for n being Element of NAT holds seq . n = - n ) holds seq is divergent_to-infty proofend; theorem Th22: :: LIMFUNC1:22 for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & ex r being Real st ( r > 0 & ( for n being Element of NAT holds seq2 . n >= r ) ) holds seq1 (#) seq2 is divergent_to+infty proofend; theorem :: LIMFUNC1:23 for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & ex r being Real st ( 0 < r & ( for n being Element of NAT holds seq2 . n >= r ) ) holds seq1 (#) seq2 is divergent_to-infty proofend; theorem Th24: :: LIMFUNC1:24 for seq1, seq2 being Real_Sequence st seq1 is divergent_to-infty & seq2 is divergent_to-infty holds seq1 (#) seq2 is divergent_to+infty proofend; theorem Th25: :: LIMFUNC1:25 for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds abs seq is divergent_to+infty proofend; theorem Th26: :: LIMFUNC1:26 for seq, seq1 being Real_Sequence st seq is divergent_to+infty & seq1 is subsequence of seq holds seq1 is divergent_to+infty proofend; theorem Th27: :: LIMFUNC1:27 for seq, seq1 being Real_Sequence st seq is divergent_to-infty & seq1 is subsequence of seq holds seq1 is divergent_to-infty proofend; theorem :: LIMFUNC1:28 for seq1, seq2 being Real_Sequence st seq1 is divergent_to+infty & seq2 is convergent & 0 < lim seq2 holds seq1 (#) seq2 is divergent_to+infty proofend; theorem Th29: :: LIMFUNC1:29 for seq being Real_Sequence st seq is non-decreasing & not seq is bounded_above holds seq is divergent_to+infty proofend; theorem Th30: :: LIMFUNC1:30 for seq being Real_Sequence st seq is non-increasing & not seq is bounded_below holds seq is divergent_to-infty proofend; theorem :: LIMFUNC1:31 for seq being Real_Sequence st seq is increasing & not seq is bounded_above holds seq is divergent_to+infty by Th29; theorem :: LIMFUNC1:32 for seq being Real_Sequence st seq is decreasing & not seq is bounded_below holds seq is divergent_to-infty by Th30; theorem :: LIMFUNC1:33 for seq being Real_Sequence holds ( not seq is monotone or seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty ) proofend; theorem Th34: :: LIMFUNC1:34 for seq being Real_Sequence st ( seq is divergent_to+infty or seq is divergent_to-infty ) holds ( seq " is convergent & lim (seq ") = 0 ) proofend; theorem Th35: :: LIMFUNC1:35 for seq being Real_Sequence st seq is convergent & lim seq = 0 & ex k being Element of NAT st for n being Element of NAT st k <= n holds 0 < seq . n holds seq " is divergent_to+infty proofend; theorem Th36: :: LIMFUNC1:36 for seq being Real_Sequence st seq is convergent & lim seq = 0 & ex k being Element of NAT st for n being Element of NAT st k <= n holds seq . n < 0 holds seq " is divergent_to-infty proofend; theorem Th37: :: LIMFUNC1:37 for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-decreasing holds seq " is divergent_to-infty proofend; theorem Th38: :: LIMFUNC1:38 for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is non-increasing holds seq " is divergent_to+infty proofend; theorem :: LIMFUNC1:39 for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is increasing holds seq " is divergent_to-infty by Th37; theorem :: LIMFUNC1:40 for seq being Real_Sequence st seq is non-zero & seq is convergent & lim seq = 0 & seq is decreasing holds seq " is divergent_to+infty by Th38; theorem :: LIMFUNC1:41 for seq1, seq2 being Real_Sequence st seq1 is bounded & ( seq2 is divergent_to+infty or seq2 is divergent_to-infty ) holds ( seq1 /" seq2 is convergent & lim (seq1 /" seq2) = 0 ) proofend; theorem Th42: :: LIMFUNC1:42 for seq, seq1 being Real_Sequence st seq is divergent_to+infty & ( for n being Element of NAT holds seq . n <= seq1 . n ) holds seq1 is divergent_to+infty proofend; theorem Th43: :: LIMFUNC1:43 for seq, seq1 being Real_Sequence st seq is divergent_to-infty & ( for n being Element of NAT holds seq1 . n <= seq . n ) holds seq1 is divergent_to-infty proofend; definition let f be PartFunc of REAL,REAL; attrf is convergent_in+infty means :Def6: :: LIMFUNC1:def 6 ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ex g being Real st for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = g ) ); attrf is divergent_in+infty_to+infty means :Def7: :: LIMFUNC1:def 7 ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds f /* seq is divergent_to+infty ) ); attrf is divergent_in+infty_to-infty means :Def8: :: LIMFUNC1:def 8 ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds f /* seq is divergent_to-infty ) ); attrf is convergent_in-infty means :Def9: :: LIMFUNC1:def 9 ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ex g being Real st for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = g ) ); attrf is divergent_in-infty_to+infty means :Def10: :: LIMFUNC1:def 10 ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds f /* seq is divergent_to+infty ) ); attrf is divergent_in-infty_to-infty means :Def11: :: LIMFUNC1:def 11 ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds f /* seq is divergent_to-infty ) ); end; :: deftheorem Def6 defines convergent_in+infty LIMFUNC1:def_6_:_ for f being PartFunc of REAL,REAL holds ( f is convergent_in+infty iff ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ex g being Real st for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = g ) ) ); :: deftheorem Def7 defines divergent_in+infty_to+infty LIMFUNC1:def_7_:_ for f being PartFunc of REAL,REAL holds ( f is divergent_in+infty_to+infty iff ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds f /* seq is divergent_to+infty ) ) ); :: deftheorem Def8 defines divergent_in+infty_to-infty LIMFUNC1:def_8_:_ for f being PartFunc of REAL,REAL holds ( f is divergent_in+infty_to-infty iff ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds f /* seq is divergent_to-infty ) ) ); :: deftheorem Def9 defines convergent_in-infty LIMFUNC1:def_9_:_ for f being PartFunc of REAL,REAL holds ( f is convergent_in-infty iff ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ex g being Real st for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = g ) ) ); :: deftheorem Def10 defines divergent_in-infty_to+infty LIMFUNC1:def_10_:_ for f being PartFunc of REAL,REAL holds ( f is divergent_in-infty_to+infty iff ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds f /* seq is divergent_to+infty ) ) ); :: deftheorem Def11 defines divergent_in-infty_to-infty LIMFUNC1:def_11_:_ for f being PartFunc of REAL,REAL holds ( f is divergent_in-infty_to-infty iff ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds f /* seq is divergent_to-infty ) ) ); theorem :: LIMFUNC1:44 for f being PartFunc of REAL,REAL holds ( f is convergent_in+infty iff ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ex g being Real st for g1 being Real st 0 < g1 holds ex r being Real st for r1 being Real st r < r1 & r1 in dom f holds abs ((f . r1) - g) < g1 ) ) proofend; theorem :: LIMFUNC1:45 for f being PartFunc of REAL,REAL holds ( f is convergent_in-infty iff ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ex g being Real st for g1 being Real st 0 < g1 holds ex r being Real st for r1 being Real st r1 < r & r1 in dom f holds abs ((f . r1) - g) < g1 ) ) proofend; theorem :: LIMFUNC1:46 for f being PartFunc of REAL,REAL holds ( f is divergent_in+infty_to+infty iff ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ( for g being Real ex r being Real st for r1 being Real st r < r1 & r1 in dom f holds g < f . r1 ) ) ) proofend; theorem :: LIMFUNC1:47 for f being PartFunc of REAL,REAL holds ( f is divergent_in+infty_to-infty iff ( ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ( for g being Real ex r being Real st for r1 being Real st r < r1 & r1 in dom f holds f . r1 < g ) ) ) proofend; theorem :: LIMFUNC1:48 for f being PartFunc of REAL,REAL holds ( f is divergent_in-infty_to+infty iff ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ( for g being Real ex r being Real st for r1 being Real st r1 < r & r1 in dom f holds g < f . r1 ) ) ) proofend; theorem :: LIMFUNC1:49 for f being PartFunc of REAL,REAL holds ( f is divergent_in-infty_to-infty iff ( ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ( for g being Real ex r being Real st for r1 being Real st r1 < r & r1 in dom f holds f . r1 < g ) ) ) proofend; theorem :: LIMFUNC1:50 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st ( r < g & g in (dom f1) /\ (dom f2) ) ) holds ( f1 + f2 is divergent_in+infty_to+infty & f1 (#) f2 is divergent_in+infty_to+infty ) proofend; theorem :: LIMFUNC1:51 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & f2 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st ( r < g & g in (dom f1) /\ (dom f2) ) ) holds ( f1 + f2 is divergent_in+infty_to-infty & f1 (#) f2 is divergent_in+infty_to+infty ) proofend; theorem :: LIMFUNC1:52 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & f2 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st ( g < r & g in (dom f1) /\ (dom f2) ) ) holds ( f1 + f2 is divergent_in-infty_to+infty & f1 (#) f2 is divergent_in-infty_to+infty ) proofend; theorem :: LIMFUNC1:53 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st ( g < r & g in (dom f1) /\ (dom f2) ) ) holds ( f1 + f2 is divergent_in-infty_to-infty & f1 (#) f2 is divergent_in-infty_to+infty ) proofend; theorem :: LIMFUNC1:54 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st ( r < g & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (right_open_halfline r) is bounded_below holds f1 + f2 is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC1:55 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st ( r < g & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st ( 0 < r & ( for g being Real st g in (dom f2) /\ (right_open_halfline r1) holds r <= f2 . g ) ) holds f1 (#) f2 is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC1:56 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st ( g < r & g in dom (f1 + f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded_below holds f1 + f2 is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC1:57 for f1, f2 being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st ( g < r & g in dom (f1 (#) f2) ) ) & ex r, r1 being Real st ( 0 < r & ( for g being Real st g in (dom f2) /\ (left_open_halfline r1) holds r <= f2 . g ) ) holds f1 (#) f2 is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC1:58 for f being PartFunc of REAL,REAL for r being Real holds ( ( f is divergent_in+infty_to+infty & r > 0 implies r (#) f is divergent_in+infty_to+infty ) & ( f is divergent_in+infty_to+infty & r < 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r > 0 implies r (#) f is divergent_in+infty_to-infty ) & ( f is divergent_in+infty_to-infty & r < 0 implies r (#) f is divergent_in+infty_to+infty ) ) proofend; theorem :: LIMFUNC1:59 for f being PartFunc of REAL,REAL for r being Real holds ( ( f is divergent_in-infty_to+infty & r > 0 implies r (#) f is divergent_in-infty_to+infty ) & ( f is divergent_in-infty_to+infty & r < 0 implies r (#) f is divergent_in-infty_to-infty ) & ( f is divergent_in-infty_to-infty & r > 0 implies r (#) f is divergent_in-infty_to-infty ) & ( f is divergent_in-infty_to-infty & r < 0 implies r (#) f is divergent_in-infty_to+infty ) ) proofend; theorem :: LIMFUNC1:60 for f being PartFunc of REAL,REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) holds abs f is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC1:61 for f being PartFunc of REAL,REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) holds abs f is divergent_in-infty_to+infty proofend; theorem Th62: :: LIMFUNC1:62 for f being PartFunc of REAL,REAL st ex r being Real st ( f | (right_open_halfline r) is non-decreasing & not f | (right_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st ( r < g & g in dom f ) ) holds f is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC1:63 for f being PartFunc of REAL,REAL st ex r being Real st ( f | (right_open_halfline r) is increasing & not f | (right_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st ( r < g & g in dom f ) ) holds f is divergent_in+infty_to+infty by Th62; theorem Th64: :: LIMFUNC1:64 for f being PartFunc of REAL,REAL st ex r being Real st ( f | (right_open_halfline r) is non-increasing & not f | (right_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st ( r < g & g in dom f ) ) holds f is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC1:65 for f being PartFunc of REAL,REAL st ex r being Real st ( f | (right_open_halfline r) is decreasing & not f | (right_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st ( r < g & g in dom f ) ) holds f is divergent_in+infty_to-infty by Th64; theorem Th66: :: LIMFUNC1:66 for f being PartFunc of REAL,REAL st ex r being Real st ( f | (left_open_halfline r) is non-increasing & not f | (left_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st ( g < r & g in dom f ) ) holds f is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC1:67 for f being PartFunc of REAL,REAL st ex r being Real st ( f | (left_open_halfline r) is decreasing & not f | (left_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st ( g < r & g in dom f ) ) holds f is divergent_in-infty_to+infty by Th66; theorem Th68: :: LIMFUNC1:68 for f being PartFunc of REAL,REAL st ex r being Real st ( f | (left_open_halfline r) is non-decreasing & not f | (left_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st ( g < r & g in dom f ) ) holds f is divergent_in-infty_to-infty proofend; theorem :: LIMFUNC1:69 for f being PartFunc of REAL,REAL st ex r being Real st ( f | (left_open_halfline r) is increasing & not f | (left_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st ( g < r & g in dom f ) ) holds f is divergent_in-infty_to-infty by Th68; theorem Th70: :: LIMFUNC1:70 for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ex r being Real st ( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds f1 . g <= f . g ) ) holds f is divergent_in+infty_to+infty proofend; theorem Th71: :: LIMFUNC1:71 for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ex r being Real st ( (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds f . g <= f1 . g ) ) holds f is divergent_in+infty_to-infty proofend; theorem Th72: :: LIMFUNC1:72 for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ex r being Real st ( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds f1 . g <= f . g ) ) holds f is divergent_in-infty_to+infty proofend; theorem Th73: :: LIMFUNC1:73 for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ex r being Real st ( (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds f . g <= f1 . g ) ) holds f is divergent_in-infty_to-infty proofend; theorem :: LIMFUNC1:74 for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to+infty & ex r being Real st ( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds f1 . g <= f . g ) ) holds f is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC1:75 for f1, f being PartFunc of REAL,REAL st f1 is divergent_in+infty_to-infty & ex r being Real st ( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds f . g <= f1 . g ) ) holds f is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC1:76 for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to+infty & ex r being Real st ( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds f1 . g <= f . g ) ) holds f is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC1:77 for f1, f being PartFunc of REAL,REAL st f1 is divergent_in-infty_to-infty & ex r being Real st ( left_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in left_open_halfline r holds f . g <= f1 . g ) ) holds f is divergent_in-infty_to-infty proofend; definition let f be PartFunc of REAL,REAL; assume A1: f is convergent_in+infty ; func lim_in+infty f -> Real means :Def12: :: LIMFUNC1:def 12 for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = it ); existence ex b1 being Real st for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = b1 ) by A1, Def6; uniqueness for b1, b2 being Real st ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = b1 ) ) & ( for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = b2 ) ) holds b1 = b2 proofend; end; :: deftheorem Def12 defines lim_in+infty LIMFUNC1:def_12_:_ for f being PartFunc of REAL,REAL st f is convergent_in+infty holds for b2 being Real holds ( b2 = lim_in+infty f iff for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = b2 ) ); definition let f be PartFunc of REAL,REAL; assume A1: f is convergent_in-infty ; func lim_in-infty f -> Real means :Def13: :: LIMFUNC1:def 13 for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = it ); existence ex b1 being Real st for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = b1 ) by A1, Def9; uniqueness for b1, b2 being Real st ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = b1 ) ) & ( for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = b2 ) ) holds b1 = b2 proofend; end; :: deftheorem Def13 defines lim_in-infty LIMFUNC1:def_13_:_ for f being PartFunc of REAL,REAL st f is convergent_in-infty holds for b2 being Real holds ( b2 = lim_in-infty f iff for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds ( f /* seq is convergent & lim (f /* seq) = b2 ) ); theorem :: LIMFUNC1:78 for f being PartFunc of REAL,REAL for g being Real st f is convergent_in-infty holds ( lim_in-infty f = g iff for g1 being Real st 0 < g1 holds ex r being Real st for r1 being Real st r1 < r & r1 in dom f holds abs ((f . r1) - g) < g1 ) proofend; theorem :: LIMFUNC1:79 for f being PartFunc of REAL,REAL for g being Real st f is convergent_in+infty holds ( lim_in+infty f = g iff for g1 being Real st 0 < g1 holds ex r being Real st for r1 being Real st r < r1 & r1 in dom f holds abs ((f . r1) - g) < g1 ) proofend; theorem Th80: :: LIMFUNC1:80 for f being PartFunc of REAL,REAL for r being Real st f is convergent_in+infty holds ( r (#) f is convergent_in+infty & lim_in+infty (r (#) f) = r * (lim_in+infty f) ) proofend; theorem Th81: :: LIMFUNC1:81 for f being PartFunc of REAL,REAL st f is convergent_in+infty holds ( - f is convergent_in+infty & lim_in+infty (- f) = - (lim_in+infty f) ) proofend; theorem Th82: :: LIMFUNC1:82 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st ( r < g & g in dom (f1 + f2) ) ) holds ( f1 + f2 is convergent_in+infty & lim_in+infty (f1 + f2) = (lim_in+infty f1) + (lim_in+infty f2) ) proofend; theorem :: LIMFUNC1:83 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st ( r < g & g in dom (f1 - f2) ) ) holds ( f1 - f2 is convergent_in+infty & lim_in+infty (f1 - f2) = (lim_in+infty f1) - (lim_in+infty f2) ) proofend; theorem :: LIMFUNC1:84 for f being PartFunc of REAL,REAL st f is convergent_in+infty & f " {0} = {} & lim_in+infty f <> 0 holds ( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " ) proofend; theorem :: LIMFUNC1:85 for f being PartFunc of REAL,REAL st f is convergent_in+infty holds ( abs f is convergent_in+infty & lim_in+infty (abs f) = abs (lim_in+infty f) ) proofend; theorem Th86: :: LIMFUNC1:86 for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f <> 0 & ( for r being Real ex g being Real st ( r < g & g in dom f & f . g <> 0 ) ) holds ( f ^ is convergent_in+infty & lim_in+infty (f ^) = (lim_in+infty f) " ) proofend; theorem Th87: :: LIMFUNC1:87 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st ( r < g & g in dom (f1 (#) f2) ) ) holds ( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = (lim_in+infty f1) * (lim_in+infty f2) ) proofend; theorem :: LIMFUNC1:88 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2 <> 0 & ( for r being Real ex g being Real st ( r < g & g in dom (f1 / f2) ) ) holds ( f1 / f2 is convergent_in+infty & lim_in+infty (f1 / f2) = (lim_in+infty f1) / (lim_in+infty f2) ) proofend; theorem Th89: :: LIMFUNC1:89 for f being PartFunc of REAL,REAL for r being Real st f is convergent_in-infty holds ( r (#) f is convergent_in-infty & lim_in-infty (r (#) f) = r * (lim_in-infty f) ) proofend; theorem Th90: :: LIMFUNC1:90 for f being PartFunc of REAL,REAL st f is convergent_in-infty holds ( - f is convergent_in-infty & lim_in-infty (- f) = - (lim_in-infty f) ) proofend; theorem Th91: :: LIMFUNC1:91 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st ( g < r & g in dom (f1 + f2) ) ) holds ( f1 + f2 is convergent_in-infty & lim_in-infty (f1 + f2) = (lim_in-infty f1) + (lim_in-infty f2) ) proofend; theorem :: LIMFUNC1:92 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st ( g < r & g in dom (f1 - f2) ) ) holds ( f1 - f2 is convergent_in-infty & lim_in-infty (f1 - f2) = (lim_in-infty f1) - (lim_in-infty f2) ) proofend; theorem :: LIMFUNC1:93 for f being PartFunc of REAL,REAL st f is convergent_in-infty & f " {0} = {} & lim_in-infty f <> 0 holds ( f ^ is convergent_in-infty & lim_in-infty (f ^) = (lim_in-infty f) " ) proofend; theorem :: LIMFUNC1:94 for f being PartFunc of REAL,REAL st f is convergent_in-infty holds ( abs f is convergent_in-infty & lim_in-infty (abs f) = abs (lim_in-infty f) ) proofend; theorem Th95: :: LIMFUNC1:95 for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f <> 0 & ( for r being Real ex g being Real st ( g < r & g in dom f & f . g <> 0 ) ) holds ( f ^ is convergent_in-infty & lim_in-infty (f ^) = (lim_in-infty f) " ) proofend; theorem Th96: :: LIMFUNC1:96 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ( for r being Real ex g being Real st ( g < r & g in dom (f1 (#) f2) ) ) holds ( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = (lim_in-infty f1) * (lim_in-infty f2) ) proofend; theorem :: LIMFUNC1:97 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f2 <> 0 & ( for r being Real ex g being Real st ( g < r & g in dom (f1 / f2) ) ) holds ( f1 / f2 is convergent_in-infty & lim_in-infty (f1 / f2) = (lim_in-infty f1) / (lim_in-infty f2) ) proofend; theorem :: LIMFUNC1:98 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & lim_in+infty f1 = 0 & ( for r being Real ex g being Real st ( r < g & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 | (right_open_halfline r) is bounded holds ( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = 0 ) proofend; theorem :: LIMFUNC1:99 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & lim_in-infty f1 = 0 & ( for r being Real ex g being Real st ( g < r & g in dom (f1 (#) f2) ) ) & ex r being Real st f2 | (left_open_halfline r) is bounded holds ( f1 (#) f2 is convergent_in-infty & lim_in-infty (f1 (#) f2) = 0 ) proofend; theorem Th100: :: LIMFUNC1:100 for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ( for r being Real ex g being Real st ( r < g & g in dom f ) ) & ex r being Real st ( ( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds ( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds ( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 ) proofend; theorem :: LIMFUNC1:101 for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ex r being Real st ( right_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in right_open_halfline r holds ( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds ( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 ) proofend; theorem Th102: :: LIMFUNC1:102 for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 & ( for r being Real ex g being Real st ( g < r & g in dom f ) ) & ex r being Real st ( ( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (left_open_halfline r) holds ( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) proofend; theorem :: LIMFUNC1:103 for f1, f2, f being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1 = lim_in-infty f2 & ex r being Real st ( left_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in left_open_halfline r holds ( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) proofend; theorem :: LIMFUNC1:104 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & ex r being Real st ( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & ( for g being Real st g in (dom f1) /\ (right_open_halfline r) holds f1 . g <= f2 . g ) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f2) /\ (right_open_halfline r) holds f1 . g <= f2 . g ) ) ) holds lim_in+infty f1 <= lim_in+infty f2 proofend; theorem :: LIMFUNC1:105 for f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in-infty & f2 is convergent_in-infty & ex r being Real st ( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds f1 . g <= f2 . g ) ) ) holds lim_in-infty f1 <= lim_in-infty f2 proofend; theorem :: LIMFUNC1:106 for f being PartFunc of REAL,REAL st ( f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty ) & ( for r being Real ex g being Real st ( r < g & g in dom f & f . g <> 0 ) ) holds ( f ^ is convergent_in+infty & lim_in+infty (f ^) = 0 ) proofend; theorem :: LIMFUNC1:107 for f being PartFunc of REAL,REAL st ( f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty ) & ( for r being Real ex g being Real st ( g < r & g in dom f & f . g <> 0 ) ) holds ( f ^ is convergent_in-infty & lim_in-infty (f ^) = 0 ) proofend; theorem :: LIMFUNC1:108 for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st ( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st for g being Real st g in (dom f) /\ (right_open_halfline r) holds 0 <= f . g holds f ^ is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC1:109 for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ( for r being Real ex g being Real st ( r < g & g in dom f & f . g <> 0 ) ) & ex r being Real st for g being Real st g in (dom f) /\ (right_open_halfline r) holds f . g <= 0 holds f ^ is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC1:110 for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st ( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st for g being Real st g in (dom f) /\ (left_open_halfline r) holds 0 <= f . g holds f ^ is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC1:111 for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ( for r being Real ex g being Real st ( g < r & g in dom f & f . g <> 0 ) ) & ex r being Real st for g being Real st g in (dom f) /\ (left_open_halfline r) holds f . g <= 0 holds f ^ is divergent_in-infty_to-infty proofend; theorem :: LIMFUNC1:112 for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ex r being Real st for g being Real st g in (dom f) /\ (right_open_halfline r) holds 0 < f . g holds f ^ is divergent_in+infty_to+infty proofend; theorem :: LIMFUNC1:113 for f being PartFunc of REAL,REAL st f is convergent_in+infty & lim_in+infty f = 0 & ex r being Real st for g being Real st g in (dom f) /\ (right_open_halfline r) holds f . g < 0 holds f ^ is divergent_in+infty_to-infty proofend; theorem :: LIMFUNC1:114 for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st for g being Real st g in (dom f) /\ (left_open_halfline r) holds 0 < f . g holds f ^ is divergent_in-infty_to+infty proofend; theorem :: LIMFUNC1:115 for f being PartFunc of REAL,REAL st f is convergent_in-infty & lim_in-infty f = 0 & ex r being Real st for g being Real st g in (dom f) /\ (left_open_halfline r) holds f . g < 0 holds f ^ is divergent_in-infty_to-infty proofend;