The abstract of the Mizar article:

The Limit of a Real Function at Infinity

by

Jaroslaw Kotowicz

Received August 20, 1990

MML identifier: LIMFUNC1

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, SEQ_1, PARTFUN1, ARYTM_1, RELAT_1, BOOLE, SQUARE_1, ARYTM_3,
      PROB_1, RCOMP_1, SEQ_2, FUNCT_1, ORDINAL2, ABSVALUE, SEQM_3, LATTICES,
      RFUNCT_1, RFUNCT_2, FINSEQ_1, LIMFUNC1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, PROB_1, RELSET_1,
      SQUARE_1, PARTFUN1, RFUNCT_1, RCOMP_1, RFUNCT_2;
 constructors REAL_1, NAT_1, ABSVALUE, SEQ_2, SEQM_3, PROB_1, SQUARE_1,
      RFUNCT_1, RCOMP_1, RFUNCT_2, PARTFUN1, MEMBERED, XBOOLE_0;
 clusters RELSET_1, XREAL_0, SEQ_1, SEQM_3, ARYTM_3, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

reserve r,r1,r2,g,g1,g2 for real number;
reserve n,m,k for Nat;
reserve seq,seq1,seq2 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;

definition let n,m;
  redefine func max(n,m) ->Nat;
end;

theorem :: LIMFUNC1:1
0<=r1 & r1<r2 & 0<g1 & g1<=g2 implies r1*g1<r2*g2;

definition let r be real number;
  redefine func halfline(r);
  synonym left_open_halfline(r);
end;

reserve r,r1,r2,g,g1,g2 for Real;

definition let r be real number;
func left_closed_halfline(r) ->Subset of REAL equals
:: LIMFUNC1:def 1
{g: g<=r};
func right_closed_halfline(r) ->Subset of REAL equals
:: LIMFUNC1:def 2
{g: r<=g};
func right_open_halfline(r) ->Subset of REAL equals
:: LIMFUNC1:def 3
{g: r<g};
end;

canceled 6;

theorem :: LIMFUNC1:8
  r1<=r2 implies right_open_halfline(r2) c= right_open_halfline(r1);

theorem :: LIMFUNC1:9
  r1<=r2 implies right_closed_halfline(r2) c= right_closed_halfline(r1);

theorem :: LIMFUNC1:10
  right_open_halfline(r) c= right_closed_halfline(r);

theorem :: LIMFUNC1:11
  ].r,g.[ c= right_open_halfline(r);

theorem :: LIMFUNC1:12
  [.r,g.] c= right_closed_halfline(r);

theorem :: LIMFUNC1:13
  r1<=r2 implies left_open_halfline(r1) c= left_open_halfline(r2);

theorem :: LIMFUNC1:14
  r1<=r2 implies left_closed_halfline(r1) c= left_closed_halfline(r2);

theorem :: LIMFUNC1:15
  left_open_halfline(r) c= left_closed_halfline(r);

theorem :: LIMFUNC1:16
  ].g,r.[ c= left_open_halfline(r);

theorem :: LIMFUNC1:17
  [.g,r.] c= left_closed_halfline(r);

theorem :: LIMFUNC1:18
left_open_halfline(r) /\ right_open_halfline(g) = ].g,r.[;

theorem :: LIMFUNC1:19
left_closed_halfline(r) /\ right_closed_halfline(g) = [.g,r.];

theorem :: LIMFUNC1:20
  r<=r1 implies ].r1,r2.[ c= right_open_halfline(r) &
[.r1,r2.] c= right_closed_halfline(r);

theorem :: LIMFUNC1:21
  r<r1 implies [.r1,r2.] c= right_open_halfline(r);

theorem :: LIMFUNC1:22
  r2<=r implies ].r1,r2.[ c= left_open_halfline(r) &
[.r1,r2.] c= left_closed_halfline(r);

theorem :: LIMFUNC1:23
  r2<r implies [.r1,r2.] c= left_open_halfline(r);

theorem :: LIMFUNC1:24
REAL \ right_open_halfline(r) = left_closed_halfline(r) &
REAL \ right_closed_halfline(r) = left_open_halfline(r) &
REAL \ left_open_halfline(r) = right_closed_halfline(r) &
REAL \ left_closed_halfline(r) = right_open_halfline(r);

theorem :: LIMFUNC1:25
  REAL \ ].r1,r2.[ = left_closed_halfline(r1) \/ right_closed_halfline(r2) &
REAL \ [.r1,r2.] = left_open_halfline(r1) \/ right_open_halfline(r2);

theorem :: LIMFUNC1:26
(seq is non-decreasing implies seq is bounded_below) &
(seq is non-increasing implies seq is bounded_above);

theorem :: LIMFUNC1:27
seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing implies
for n holds seq.n<0;

theorem :: LIMFUNC1:28
seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing implies
for n holds 0<seq.n;

theorem :: LIMFUNC1:29
seq is convergent & 0<lim seq implies ex n st for m st n<=m holds 0<seq.m;

theorem :: LIMFUNC1:30
seq is convergent & 0<lim seq implies
ex n st for m st n<=m holds (lim seq)/2<seq.m;

definition let seq;
 attr seq is divergent_to+infty means
:: LIMFUNC1:def 4
  for r ex n st for m st n<=m holds r<seq.m;
 attr seq is divergent_to-infty means
:: LIMFUNC1:def 5
  for r ex n st for m st n<=m holds seq.m<r;
end;

canceled 2;

theorem :: LIMFUNC1:33
  seq is divergent_to+infty or seq is divergent_to-infty implies
ex n st for m st n<=m holds seq^\m is_not_0;

theorem :: LIMFUNC1:34
(seq^\k is divergent_to+infty implies seq is divergent_to+infty) &
(seq^\k is divergent_to-infty implies seq is divergent_to-infty);

theorem :: LIMFUNC1:35
seq1 is divergent_to+infty & seq2 is divergent_to+infty implies
seq1+seq2 is divergent_to+infty;

theorem :: LIMFUNC1:36
seq1 is divergent_to+infty & seq2 is bounded_below implies
seq1+seq2 is divergent_to+infty;

theorem :: LIMFUNC1:37
seq1 is divergent_to+infty & seq2 is divergent_to+infty implies
seq1(#)seq2 is divergent_to+infty;

theorem :: LIMFUNC1:38
seq1 is divergent_to-infty & seq2 is divergent_to-infty implies
seq1+seq2 is divergent_to-infty;

theorem :: LIMFUNC1:39
seq1 is divergent_to-infty & seq2 is bounded_above implies
seq1+seq2 is divergent_to-infty;

theorem :: LIMFUNC1:40
(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) &
(seq is divergent_to+infty & r=0 implies rng (r(#)seq)={0} & r(#)
seq is constant);

theorem :: LIMFUNC1:41
(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) &
(seq is divergent_to-infty & r=0 implies rng (r(#)seq)={0} & r(#)
seq is constant);

theorem :: LIMFUNC1:42
  (seq is divergent_to+infty implies -seq is divergent_to-infty) &
(seq is divergent_to-infty implies -seq is divergent_to+infty);

theorem :: LIMFUNC1:43
  seq is bounded_below & seq1 is divergent_to-infty implies
seq-seq1 is divergent_to+infty;

theorem :: LIMFUNC1:44
  seq is bounded_above & seq1 is divergent_to+infty implies
seq-seq1 is divergent_to-infty;

theorem :: LIMFUNC1:45
  seq is divergent_to+infty & seq1 is convergent implies
 seq+seq1 is divergent_to+infty;

theorem :: LIMFUNC1:46
  seq is divergent_to-infty & seq1 is convergent implies
 seq+seq1 is divergent_to-infty;

theorem :: LIMFUNC1:47
(for n holds seq.n=n) implies seq is divergent_to+infty;

theorem :: LIMFUNC1:48
(for n holds seq.n=-n) implies seq is divergent_to-infty;

theorem :: LIMFUNC1:49
seq1 is divergent_to+infty & (ex r st r>0 & for n holds seq2.n>=r) implies
seq1(#)seq2 is divergent_to+infty;

theorem :: LIMFUNC1:50
  seq1 is divergent_to-infty & (ex r st 0<r & for n holds seq2.n>=r) implies
seq1(#)seq2 is divergent_to-infty;

theorem :: LIMFUNC1:51
seq1 is divergent_to-infty & seq2 is divergent_to-infty implies
seq1(#)seq2 is divergent_to+infty;

theorem :: LIMFUNC1:52
(seq is divergent_to+infty or seq is divergent_to-infty) implies
abs(seq) is divergent_to+infty;

theorem :: LIMFUNC1:53
seq is divergent_to+infty & seq1 is_subsequence_of seq implies
seq1 is divergent_to+infty;

theorem :: LIMFUNC1:54
seq is divergent_to-infty & seq1 is_subsequence_of seq implies
seq1 is divergent_to-infty;

theorem :: LIMFUNC1:55
  seq1 is divergent_to+infty & seq2 is convergent & 0<lim seq2 implies
seq1(#)seq2 is divergent_to+infty;

theorem :: LIMFUNC1:56
seq is non-decreasing & not seq is bounded_above implies
 seq is divergent_to+infty;

theorem :: LIMFUNC1:57
seq is non-increasing & not seq is bounded_below implies
 seq is divergent_to-infty;

theorem :: LIMFUNC1:58
  seq is increasing & not seq is bounded_above implies seq is
divergent_to+infty;

theorem :: LIMFUNC1:59
  seq is decreasing & not seq is bounded_below implies seq is
divergent_to-infty;

theorem :: LIMFUNC1:60
  seq is monotone implies seq is convergent or seq is divergent_to+infty or
seq is divergent_to-infty;

theorem :: LIMFUNC1:61
(seq is divergent_to+infty or seq is divergent_to-infty) implies
seq" is convergent & lim(seq")=0;

theorem :: LIMFUNC1:62
seq is_not_0 & seq is convergent & lim seq=0 &
(ex k st for n st k<=n holds 0<seq.n) implies
seq" is divergent_to+infty;

theorem :: LIMFUNC1:63
seq is_not_0 & seq is convergent & lim seq=0 &
(ex k st for n st k<=n holds seq.n<0) implies
seq" is divergent_to-infty;

theorem :: LIMFUNC1:64
seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing implies
seq" is divergent_to-infty;

theorem :: LIMFUNC1:65
seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing implies
seq" is divergent_to+infty;

theorem :: LIMFUNC1:66
  seq is_not_0 & seq is convergent & lim seq=0 & seq is increasing implies
seq" is divergent_to-infty;

theorem :: LIMFUNC1:67
  seq is_not_0 & seq is convergent & lim seq=0 & seq is decreasing implies
seq" is divergent_to+infty;

theorem :: LIMFUNC1:68
  seq1 is bounded & (seq2 is divergent_to+infty or seq2 is divergent_to-infty)
&
seq2 is_not_0 implies seq1/"seq2 is convergent & lim(seq1/"seq2)=0;

theorem :: LIMFUNC1:69
seq is divergent_to+infty & (for n holds seq.n<=seq1.n) implies
seq1 is divergent_to+infty;

theorem :: LIMFUNC1:70
seq is divergent_to-infty & (for n holds seq1.n<=seq.n) implies
seq1 is divergent_to-infty;

definition let f;
attr f is convergent_in+infty means
:: LIMFUNC1:def 6
 (for r ex g st r<g & g in dom f) &
 ex g st for seq st seq is divergent_to+infty & rng seq c= dom f holds
  f*seq is convergent & lim(f*seq)=g;
attr f is divergent_in+infty_to+infty means
:: LIMFUNC1:def 7
 (for r ex g st r<g & g in dom f) &
 for seq st seq is divergent_to+infty & rng seq c= dom f holds
  f*seq is divergent_to+infty;
attr f is divergent_in+infty_to-infty means
:: LIMFUNC1:def 8
 (for r ex g st r<g & g in dom f) &
 for seq st seq is divergent_to+infty & rng seq c= dom f holds
  f*seq is divergent_to-infty;
attr f is convergent_in-infty means
:: LIMFUNC1:def 9
 (for r ex g st g<r & g in dom f) &
 ex g st for seq st seq is divergent_to-infty & rng seq c= dom f holds
  f*seq is convergent & lim(f*seq)=g;
attr f is divergent_in-infty_to+infty means
:: LIMFUNC1:def 10
 (for r ex g st g<r & g in dom f) &
 for seq st seq is divergent_to-infty & rng seq c= dom f holds
  f*seq is divergent_to+infty;
attr f is divergent_in-infty_to-infty means
:: LIMFUNC1:def 11
 (for r ex g st g<r & g in dom f) &
 for seq st seq is divergent_to-infty & rng seq c= dom f holds
  f*seq is divergent_to-infty;
end;

canceled 6;

theorem :: LIMFUNC1:77
  f is convergent_in+infty iff
(for r ex g st r<g & g in dom f) &
(ex g st for g1 st 0<g1 ex r st for r1 st r<r1 &
 r1 in dom f holds abs(f.r1-g)<g1);

theorem :: LIMFUNC1:78
  f is convergent_in-infty iff
(for r ex g st g<r & g in dom f) &
ex g st for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds
  abs(f.r1-g)<g1;

theorem :: LIMFUNC1:79
  f is divergent_in+infty_to+infty iff
 (for r ex g st r<g & g in dom f) &
 for g ex r st for r1 st r<r1 & r1 in dom f holds g<f.r1;

theorem :: LIMFUNC1:80
  f is divergent_in+infty_to-infty iff
 (for r ex g st r<g & g in dom f) &
 for g ex r st for r1 st r<r1 & r1 in dom f holds f.r1<g;

theorem :: LIMFUNC1:81
  f is divergent_in-infty_to+infty iff
 (for r ex g st g<r & g in dom f) &
 for g ex r st for r1 st r1<r & r1 in dom f holds g<f.r1;

theorem :: LIMFUNC1:82
  f is divergent_in-infty_to-infty iff
 (for r ex g st g<r & g in dom f) &
 for g ex r st for r1 st r1<r & r1 in dom f holds f.r1<g;

theorem :: LIMFUNC1:83
  f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty &
(for r ex g st r<g & g in dom f1 /\ dom f2) implies
f1+f2 is divergent_in+infty_to+infty & f1(#)f2 is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:84
  f1 is divergent_in+infty_to-infty & f2 is divergent_in+infty_to-infty &
(for r ex g st r<g & g in dom f1 /\ dom f2) implies
f1+f2 is divergent_in+infty_to-infty & f1(#)f2 is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:85
  f1 is divergent_in-infty_to+infty & f2 is divergent_in-infty_to+infty &
(for r ex g st g<r & g in dom f1 /\ dom f2) implies
f1+f2 is divergent_in-infty_to+infty & f1(#)f2 is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:86
  f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty &
(for r ex g st g<r & g in dom f1 /\ dom f2) implies
f1+f2 is divergent_in-infty_to-infty & f1(#)f2 is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:87
  f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom(f1+f2)) &
(ex r st f2 is_bounded_below_on right_open_halfline(r))
implies f1+f2 is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:88
  f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom(f1(#)f2)) &
(ex r,r1 st 0<r & for g st g in dom f2 /\
 right_open_halfline(r1) holds r<=f2.g)
implies f1(#)f2 is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:89
  f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom(f1+f2)) &
(ex r st f2 is_bounded_below_on left_open_halfline(r))
implies f1+f2 is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:90
  f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom(f1(#)f2)) &
(ex r,r1 st 0<r & for g st g in dom f2 /\ left_open_halfline(r1) holds r<=f2.g)
implies f1(#)f2 is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:91
  (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);

theorem :: LIMFUNC1:92
  (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);

theorem :: LIMFUNC1:93
  (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty)
implies
abs(f) is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:94
  (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty)
implies
abs(f) is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:95
(ex r st f is_non_decreasing_on right_open_halfline(r) &
not f is_bounded_above_on right_open_halfline(r)) &
(for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:96
  (ex r st f is_increasing_on right_open_halfline(r) &
not f is_bounded_above_on right_open_halfline(r)) &
(for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:97
(ex r st f is_non_increasing_on right_open_halfline(r) &
not f is_bounded_below_on right_open_halfline(r)) &
(for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to-infty;

theorem :: LIMFUNC1:98
  (ex r st f is_decreasing_on right_open_halfline(r) &
not f is_bounded_below_on right_open_halfline(r)) &
(for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to-infty;

theorem :: LIMFUNC1:99
(ex r st f is_non_increasing_on left_open_halfline(r) &
not f is_bounded_above_on left_open_halfline(r)) &
(for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:100
  (ex r st f is_decreasing_on left_open_halfline(r) &
not f is_bounded_above_on left_open_halfline(r)) &
(for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:101
(ex r st f is_non_decreasing_on left_open_halfline(r) &
not f is_bounded_below_on left_open_halfline(r)) &
(for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to-infty;

theorem :: LIMFUNC1:102
  (ex r st f is_increasing_on left_open_halfline(r) &
not f is_bounded_below_on left_open_halfline(r)) &
(for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to-infty;

theorem :: LIMFUNC1:103
f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom f) &
(ex r st dom f /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) &
 for g st g in dom f /\ right_open_halfline(r) holds f1.g<=f.g) implies
f is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:104
f1 is divergent_in+infty_to-infty & (for r ex g st r<g & g in dom f) &
(ex r st dom f/\right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) &
 for g st g in dom f /\ right_open_halfline(r) holds f.g<=f1.g) implies
f is divergent_in+infty_to-infty;

theorem :: LIMFUNC1:105
f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom f) &
(ex r st dom f/\left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) &
 for g st g in dom f /\ left_open_halfline(r) holds f1.g<=f.g) implies
f is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:106
f1 is divergent_in-infty_to-infty & (for r ex g st g<r & g in dom f) &
(ex r st dom f/\left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) &
 for g st g in dom f /\ left_open_halfline(r) holds f.g<=f1.g) implies
f is divergent_in-infty_to-infty;

theorem :: LIMFUNC1:107
  f1 is divergent_in+infty_to+infty &
(ex r st right_open_halfline(r) c= dom f /\ dom f1 &
 for g st g in right_open_halfline(r) holds f1.g<=f.g) implies
f is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:108
  f1 is divergent_in+infty_to-infty & (ex r st
 right_open_halfline(r) c= dom f /\ dom f1 &
 for g st g in right_open_halfline(r) holds f.g<=f1.g) implies
f is divergent_in+infty_to-infty;

theorem :: LIMFUNC1:109
  f1 is divergent_in-infty_to+infty & (ex r st
 left_open_halfline(r) c= dom f /\ dom f1 &
 for g st g in left_open_halfline(r) holds f1.g<=f.g) implies
f is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:110
  f1 is divergent_in-infty_to-infty & (ex r st
 left_open_halfline(r) c= dom f /\ dom f1 &
 for g st g in left_open_halfline(r) holds f.g<=f1.g) implies
f is divergent_in-infty_to-infty;

definition let f;
assume  f is convergent_in+infty;
func lim_in+infty f ->Real means
:: LIMFUNC1:def 12
for seq st seq is divergent_to+infty & rng seq c= dom f holds
f*seq is convergent & lim(f*seq)=it;
end;

definition let f;
assume  f is convergent_in-infty;
func lim_in-infty f ->Real means
:: LIMFUNC1:def 13
for seq st seq is divergent_to-infty & rng seq c= dom f holds
f*seq is convergent & lim(f*seq)=it;
end;

canceled 2;

theorem :: LIMFUNC1:113
  f is convergent_in-infty implies (lim_in-infty f=g iff
for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1);

theorem :: LIMFUNC1:114
  f is convergent_in+infty implies (lim_in+infty f=g iff
for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1);

theorem :: LIMFUNC1:115
f is convergent_in+infty implies r(#)f is convergent_in+infty &
lim_in+infty(r(#)f)=r*(lim_in+infty f);

theorem :: LIMFUNC1:116
f is convergent_in+infty implies -f is convergent_in+infty &
lim_in+infty(-f)=-(lim_in+infty f);

theorem :: LIMFUNC1:117
f1 is convergent_in+infty & f2 is convergent_in+infty &
(for r ex g st r<g & g in dom(f1+f2)) implies f1+f2 is convergent_in+infty &
lim_in+infty(f1+f2) = lim_in+infty f1 + lim_in+infty f2;

theorem :: LIMFUNC1:118
  f1 is convergent_in+infty & f2 is convergent_in+infty &
(for r ex g st r<g & g in dom(f1-f2)) implies f1-f2 is convergent_in+infty &
lim_in+infty(f1-f2)=(lim_in+infty f1)-(lim_in+infty f2);

theorem :: LIMFUNC1:119
  f is convergent_in+infty & f"{0}={} & (lim_in+infty f)<>0 implies
f^ is convergent_in+infty & lim_in+infty(f^)=(lim_in+infty f)";

theorem :: LIMFUNC1:120
  f is convergent_in+infty implies abs(f) is convergent_in+infty &
lim_in+infty abs(f)=abs(lim_in+infty f);

theorem :: LIMFUNC1:121
f is convergent_in+infty & lim_in+infty f<>0 &
(for r ex g st r<g & g in dom f & f.g<>0) implies
f^ is convergent_in+infty & lim_in+infty(f^)=(lim_in+infty f)";

theorem :: LIMFUNC1:122
f1 is convergent_in+infty & f2 is convergent_in+infty &
(for r ex g st r<g & g in dom(f1(#)f2)) implies f1(#)
f2 is convergent_in+infty &
lim_in+infty(f1(#)f2)=(lim_in+infty f1)*(lim_in+infty f2);

theorem :: LIMFUNC1:123
  f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2<>0 &
(for r ex g st r<g & g in dom(f1/f2)) implies f1/f2 is convergent_in+infty &
lim_in+infty(f1/f2)=(lim_in+infty f1)/(lim_in+infty f2);

theorem :: LIMFUNC1:124
f is convergent_in-infty implies r(#)f is convergent_in-infty &
lim_in-infty(r(#)f)=r*(lim_in-infty f);

theorem :: LIMFUNC1:125
f is convergent_in-infty implies -f is convergent_in-infty &
lim_in-infty(-f)=-(lim_in-infty f);

theorem :: LIMFUNC1:126
f1 is convergent_in-infty & f2 is convergent_in-infty &
(for r ex g st g<r & g in dom(f1+f2)) implies f1+f2 is convergent_in-infty &
lim_in-infty(f1+f2) = lim_in-infty f1 + lim_in-infty f2;

theorem :: LIMFUNC1:127
  f1 is convergent_in-infty & f2 is convergent_in-infty &
(for r ex g st g<r & g in dom(f1-f2)) implies f1-f2 is convergent_in-infty &
lim_in-infty(f1-f2)=(lim_in-infty f1)-(lim_in-infty f2);

theorem :: LIMFUNC1:128
  f is convergent_in-infty & f"{0}={} & (lim_in-infty f)<>0 implies
f^ is convergent_in-infty & lim_in-infty(f^)=(lim_in-infty f)";

theorem :: LIMFUNC1:129
  f is convergent_in-infty implies abs(f) is convergent_in-infty &
lim_in-infty abs(f)=abs(lim_in-infty f);

theorem :: LIMFUNC1:130
f is convergent_in-infty & lim_in-infty f<>0 &
(for r ex g st g<r & g in dom f & f.g<>0) implies
f^ is convergent_in-infty & lim_in-infty(f^)=(lim_in-infty f)";

theorem :: LIMFUNC1:131
f1 is convergent_in-infty & f2 is convergent_in-infty &
(for r ex g st g<r & g in dom(f1(#)f2)) implies f1(#)
f2 is convergent_in-infty &
lim_in-infty(f1(#)f2)=(lim_in-infty f1)*(lim_in-infty f2);

theorem :: LIMFUNC1:132
  f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f2<>0 &
(for r ex g st g<r & g in dom(f1/f2)) implies f1/f2 is convergent_in-infty &
lim_in-infty(f1/f2)=(lim_in-infty f1)/(lim_in-infty f2);

theorem :: LIMFUNC1:133
  f1 is convergent_in+infty & lim_in+infty f1=0 &
(for r ex g st r<g & g in dom(f1(#)f2)) &
(ex r st f2 is_bounded_on right_open_halfline(r)) implies
f1(#)f2 is convergent_in+infty & lim_in+infty(f1(#)f2)=0;

theorem :: LIMFUNC1:134
  f1 is convergent_in-infty & lim_in-infty f1=0 &
(for r ex g st g<r & g in dom(f1(#)f2)) &
(ex r st f2 is_bounded_on left_open_halfline(r)) implies
f1(#)f2 is convergent_in-infty & lim_in-infty(f1(#)f2)=0;

theorem :: LIMFUNC1:135
f1 is convergent_in+infty & f2 is convergent_in+infty &
lim_in+infty f1=lim_in+infty f2 & (for r ex g st r<g & g in dom f) & (ex r 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 st g in dom f /\ right_open_halfline(r) holds
  f1.g<=f.g & f.g<=f2.g) implies
f is convergent_in+infty & lim_in+infty f=lim_in+infty f1;

theorem :: LIMFUNC1:136
  f1 is convergent_in+infty & f2 is convergent_in+infty &
  lim_in+infty f1=lim_in+infty f2
& (ex r st right_open_halfline(r) c= dom f1 /\ dom f2 /\ dom f &
for g st g in right_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g) implies
f is convergent_in+infty & lim_in+infty f=lim_in+infty f1;

theorem :: LIMFUNC1:137
f1 is convergent_in-infty & f2 is convergent_in-infty &
lim_in-infty f1=lim_in-infty f2 & (for r ex g st g<r & g in dom f) & (ex r 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 st g in dom f /\ left_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g)
 implies
f is convergent_in-infty & lim_in-infty f=lim_in-infty f1;

theorem :: LIMFUNC1:138
  f1 is convergent_in-infty & f2 is convergent_in-infty &
 lim_in-infty f1=lim_in-infty f2
& (ex r st left_open_halfline(r) c= dom f1 /\ dom f2 /\ dom f &
for g st g in left_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g) implies
f is convergent_in-infty & lim_in-infty f=lim_in-infty f1;

theorem :: LIMFUNC1:139
  f1 is convergent_in+infty & f2 is convergent_in+infty &
(ex r st ((dom f1 /\ right_open_halfline(r) c= dom f2 /\
 right_open_halfline(r) &
 for g 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 st g in dom f2 /\ right_open_halfline(r) holds f1.g<=f2.g))) implies
lim_in+infty f1<=lim_in+infty f2;

theorem :: LIMFUNC1:140
  f1 is convergent_in-infty & f2 is convergent_in-infty &
(ex r st ((dom f1 /\ left_open_halfline(r) c= dom f2 /\ left_open_halfline(r) &
 for g 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 st g in dom f2 /\ left_open_halfline(r) holds f1.g<=f2.g))) implies
lim_in-infty f1<=lim_in-infty f2;

theorem :: LIMFUNC1:141
  (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty) &
(for r ex g st r<g & g in dom f & f.g<>0) implies f^ is convergent_in+infty &
lim_in+infty(f^)=0;

theorem :: LIMFUNC1:142
  (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty) &
(for r ex g st g<r & g in dom f & f.g<>0) implies f^ is convergent_in-infty &
lim_in-infty(f^)=0;

theorem :: LIMFUNC1:143
  f is convergent_in+infty & lim_in+infty f=0 &
(for r ex g st r<g & g in dom f & f.g<>0) &
(ex r st for g st g in dom f /\ right_open_halfline(r) holds 0<=f.g) implies
f^ is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:144
  f is convergent_in+infty & lim_in+infty f=0 &
(for r ex g st r<g & g in dom f & f.g<>0) &
(ex r st for g st g in dom f /\ right_open_halfline(r) holds f.g<=0) implies
f^ is divergent_in+infty_to-infty;

theorem :: LIMFUNC1:145
  f is convergent_in-infty & lim_in-infty f=0 &
(for r ex g st g<r & g in dom f & f.g<>0) &
(ex r st for g st g in dom f /\ left_open_halfline(r) holds 0<=f.g) implies
f^ is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:146
  f is convergent_in-infty & lim_in-infty f=0 &
(for r ex g st g<r & g in dom f & f.g<>0) &
(ex r st for g st g in dom f /\ left_open_halfline(r) holds f.g<=0) implies
f^ is divergent_in-infty_to-infty;

theorem :: LIMFUNC1:147
  f is convergent_in+infty & lim_in+infty f=0 &
(ex r st for g st g in dom f /\ right_open_halfline(r) holds 0<f.g) implies
f^ is divergent_in+infty_to+infty;

theorem :: LIMFUNC1:148
  f is convergent_in+infty & lim_in+infty f=0 &
(ex r st for g st g in dom f /\ right_open_halfline(r) holds f.g<0) implies
f^ is divergent_in+infty_to-infty;

theorem :: LIMFUNC1:149
  f is convergent_in-infty & lim_in-infty f=0 &
(ex r st for g st g in dom f /\ left_open_halfline(r) holds 0<f.g) implies
f^ is divergent_in-infty_to+infty;

theorem :: LIMFUNC1:150
  f is convergent_in-infty & lim_in-infty f=0 &
(ex r st for g st g in dom f /\ left_open_halfline(r) holds f.g<0) implies
f^ is divergent_in-infty_to-infty;