environ vocabulary SEQ_1, PARTFUN1, BOOLE, ARYTM, ARYTM_1, RELAT_1, ARYTM_3, LIMFUNC1, FUNCT_1, ABSVALUE, SEQ_2, ORDINAL2, RCOMP_1, SQUARE_1, LIMFUNC2, SEQM_3, RFUNCT_1, RFUNCT_2, FINSEQ_1, LATTICES, LIMFUNC3; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_2, ABSVALUE, SEQ_1, PARTFUN1, SEQ_2, SEQM_3, RCOMP_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, LIMFUNC2; constructors REAL_1, NAT_1, ABSVALUE, SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, LIMFUNC2, PARTFUN1, MEMBERED, XBOOLE_0; clusters RELSET_1, XREAL_0, SEQ_1, SEQM_3, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve r,r1,r2,g,g1,g2,x0 for Real; reserve n,k,m for Nat; reserve seq for Real_Sequence; reserve f,f1,f2 for PartFunc of REAL,REAL; theorem :: LIMFUNC3:1 (rng seq c= dom f /\ left_open_halfline(x0) or rng seq c= dom f /\ right_open_halfline(x0)) implies rng seq c= dom f \ {x0}; theorem :: LIMFUNC3:2 (for n holds 0<abs(x0-seq.n) & abs(x0-seq.n)<1/(n+1) & seq.n in dom f) implies seq is convergent & lim seq=x0 & rng seq c=dom f & rng seq c= dom f \ {x0}; theorem :: LIMFUNC3:3 seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} implies for r st 0<r ex n st for k st n<=k holds 0<abs(x0-seq.k) & abs(x0-seq.k)<r & seq.k in dom f; theorem :: LIMFUNC3:4 0<r implies ].x0-r,x0+r.[ \ {x0} = ].x0-r,x0.[ \/ ].x0,x0+r.[; theorem :: LIMFUNC3:5 0<r2 & ].x0-r2,x0.[ \/ ].x0,x0+r2.[ c= dom f implies for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f; theorem :: LIMFUNC3:6 (for n holds x0-1/(n+1)<seq.n & seq.n<x0 & seq.n in dom f) implies seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0}; theorem :: LIMFUNC3:7 seq is convergent & lim seq=x0 & 0<g implies ex k st for n st k<=n holds x0-g<seq.n & seq.n<x0+g; theorem :: LIMFUNC3:8 (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) iff (for r st r<x0 ex g st r<g & g<x0 & g in dom f) & (for r st x0<r ex g st g<r & x0<g & g in dom f); definition let f,x0; pred f is_convergent_in x0 means :: LIMFUNC3:def 1 (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & ex g st for seq st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds f*seq is convergent & lim(f*seq)=g; pred f is_divergent_to+infty_in x0 means :: LIMFUNC3:def 2 (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for seq st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds f*seq is divergent_to+infty; pred f is_divergent_to-infty_in x0 means :: LIMFUNC3:def 3 (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for seq st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds f*seq is divergent_to-infty; end; canceled 3; theorem :: LIMFUNC3:12 f is_convergent_in x0 iff (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & ex g st for g1 st 0<g1 ex g2 st 0<g2 & for r1 st 0<abs(x0-r1) & abs(x0-r1)<g2 & r1 in dom f holds abs(f.r1-g)<g1; theorem :: LIMFUNC3:13 f is_divergent_to+infty_in x0 iff (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for g1 ex g2 st 0<g2 & for r1 st 0<abs(x0-r1) & abs(x0-r1)<g2 & r1 in dom f holds g1<f.r1; theorem :: LIMFUNC3:14 f is_divergent_to-infty_in x0 iff (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for g1 ex g2 st 0<g2 & for r1 st 0<abs(x0-r1) & abs(x0-r1)<g2 & r1 in dom f holds f.r1<g1; theorem :: LIMFUNC3:15 f is_divergent_to+infty_in x0 iff f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0; theorem :: LIMFUNC3:16 f is_divergent_to-infty_in x0 iff f is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0; theorem :: LIMFUNC3:17 f1 is_divergent_to+infty_in x0 & f2 is_divergent_to+infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f1 /\ dom f2 & g2<r2 & x0<g2 & g2 in dom f1 /\ dom f2) implies f1+f2 is_divergent_to+infty_in x0 & f1(#)f2 is_divergent_to+infty_in x0 ; theorem :: LIMFUNC3:18 f1 is_divergent_to-infty_in x0 & f2 is_divergent_to-infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f1 /\ dom f2 & g2<r2 & x0<g2 & g2 in dom f1 /\ dom f2) implies f1+f2 is_divergent_to-infty_in x0 & f1(#) f2 is_divergent_to+infty_in x0; theorem :: LIMFUNC3:19 f1 is_divergent_to+infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1+f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2)) & (ex r st 0<r & f2 is_bounded_below_on ].x0-r,x0.[ \/ ].x0,x0+r.[) implies f1+f2 is_divergent_to+infty_in x0; theorem :: LIMFUNC3:20 f1 is_divergent_to+infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2)) & (ex r,r1 st 0<r & 0<r1 & for g st g in dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds r1<=f2.g) implies f1(#)f2 is_divergent_to+infty_in x0; theorem :: LIMFUNC3:21 (f is_divergent_to+infty_in x0 & r>0 implies r(#) f is_divergent_to+infty_in x0)& (f is_divergent_to+infty_in x0 & r<0 implies r(#) f is_divergent_to-infty_in x0)& (f is_divergent_to-infty_in x0 & r>0 implies r(#) f is_divergent_to-infty_in x0)& (f is_divergent_to-infty_in x0 & r<0 implies r(#)f is_divergent_to+infty_in x0) ; theorem :: LIMFUNC3:22 (f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0) implies abs(f) is_divergent_to+infty_in x0; theorem :: LIMFUNC3:23 (ex r st 0<r & f is_non_decreasing_on ].x0-r,x0.[ & f is_non_increasing_on ].x0,x0+r.[ & not f is_bounded_above_on ].x0-r,x0.[ & not f is_bounded_above_on ].x0,x0+r.[) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_divergent_to+infty_in x0; theorem :: LIMFUNC3:24 (ex r st 0<r & f is_increasing_on ].x0-r,x0.[ & f is_decreasing_on ].x0,x0+r.[ & not f is_bounded_above_on ].x0-r,x0.[ & not f is_bounded_above_on ].x0,x0+r.[) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_divergent_to+infty_in x0; theorem :: LIMFUNC3:25 (ex r st 0<r & f is_non_increasing_on ].x0-r,x0.[ & f is_non_decreasing_on ].x0,x0+r.[ & not f is_bounded_below_on ].x0-r,x0.[ & not f is_bounded_below_on ].x0,x0+r.[) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_divergent_to-infty_in x0; theorem :: LIMFUNC3:26 (ex r st 0<r & f is_decreasing_on ].x0-r,x0.[ & f is_increasing_on ].x0,x0+r.[ & not f is_bounded_below_on ].x0-r,x0.[ & not f is_bounded_below_on ].x0,x0+r.[) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_divergent_to-infty_in x0; theorem :: LIMFUNC3:27 f1 is_divergent_to+infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & (ex r st 0<r & dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<=f.g) implies f is_divergent_to+infty_in x0; theorem :: LIMFUNC3:28 f1 is_divergent_to-infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & (ex r st 0<r & dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f.g<=f1.g) implies f is_divergent_to-infty_in x0; theorem :: LIMFUNC3:29 f1 is_divergent_to+infty_in x0 & (ex r st 0<r & ].x0-r,x0.[ \/ ].x0,x0+r.[ c= dom f /\ dom f1 & for g st g in ].x0-r,x0.[ \/ ].x0,x0+r.[ holds f1.g<=f.g) implies f is_divergent_to+infty_in x0; theorem :: LIMFUNC3:30 f1 is_divergent_to-infty_in x0 & (ex r st 0<r & ].x0-r,x0.[ \/ ].x0,x0+r.[ c= dom f /\ dom f1 & for g st g in ].x0-r,x0.[ \/ ].x0,x0+r.[ holds f.g<=f1.g) implies f is_divergent_to-infty_in x0; definition let f,x0; assume f is_convergent_in x0; func lim(f,x0)->Real means :: LIMFUNC3:def 4 for seq st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds f*seq is convergent & lim(f*seq)=it; end; canceled; theorem :: LIMFUNC3:32 f is_convergent_in x0 implies (lim(f,x0)=g iff for g1 st 0<g1 ex g2 st 0<g2 & for r1 st 0<abs(x0-r1) & abs(x0-r1)<g2 & r1 in dom f holds abs(f.r1-g)<g1); theorem :: LIMFUNC3:33 f is_convergent_in x0 implies f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left(f,x0)=lim_right(f,x0) & lim(f,x0)=lim_left(f,x0) & lim(f,x0)=lim_right(f,x0); theorem :: LIMFUNC3:34 f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left(f,x0)=lim_right(f,x0) implies f is_convergent_in x0 & lim(f,x0)=lim_left(f,x0) & lim(f,x0)=lim_right(f,x0); theorem :: LIMFUNC3:35 f is_convergent_in x0 implies r(#)f is_convergent_in x0 & lim(r(#)f,x0)=r*(lim(f,x0)); theorem :: LIMFUNC3:36 f is_convergent_in x0 implies -f is_convergent_in x0 & lim(-f,x0)=-(lim(f,x0)); theorem :: LIMFUNC3:37 f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1+f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2)) implies f1+f2 is_convergent_in x0 & lim(f1+f2,x0)=lim(f1,x0)+lim(f2,x0); theorem :: LIMFUNC3:38 f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1-f2) & g2<r2 & x0<g2 & g2 in dom(f1-f2)) implies f1-f2 is_convergent_in x0 & lim(f1-f2,x0)=(lim(f1,x0))-(lim(f2,x0)); theorem :: LIMFUNC3:39 f is_convergent_in x0 & f"{0}={} & lim(f,x0)<>0 implies f^ is_convergent_in x0 & lim(f^,x0)=(lim(f,x0))"; theorem :: LIMFUNC3:40 f is_convergent_in x0 implies abs(f) is_convergent_in x0 & lim(abs(f),x0)=abs(lim(f,x0)); theorem :: LIMFUNC3:41 f is_convergent_in x0 & lim(f,x0)<>0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0) implies f^ is_convergent_in x0 & lim(f^,x0)=(lim(f,x0))"; theorem :: LIMFUNC3:42 f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#) f2)) implies f1(#)f2 is_convergent_in x0 & lim(f1(#)f2,x0)=(lim(f1,x0))*(lim(f2,x0)); theorem :: LIMFUNC3:43 f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim(f2,x0)<>0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1/f2) & g2<r2 & x0<g2 & g2 in dom(f1/f2)) implies f1/f2 is_convergent_in x0 & lim(f1/f2,x0)=(lim(f1,x0))/(lim(f2,x0)); theorem :: LIMFUNC3:44 f1 is_convergent_in x0 & lim(f1,x0)=0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2)) & (ex r st 0<r & f2 is_bounded_on ].x0-r,x0.[ \/ ].x0,x0+r.[) implies f1(#)f2 is_convergent_in x0 & lim(f1(#)f2,x0)=0; theorem :: LIMFUNC3:45 f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim(f1,x0)=lim(f2,x0) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & (ex r st 0<r & (for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<=f.g & f.g<=f2.g) & ((dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) & dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)) or (dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) & dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)))) implies f is_convergent_in x0 & lim(f,x0)=lim(f1,x0); theorem :: LIMFUNC3:46 f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim(f1,x0)=lim(f2,x0) & (ex r st 0<r & ].x0-r,x0.[ \/ ].x0,x0+r.[ c= dom f1 /\ dom f2 /\ dom f & for g st g in ].x0-r,x0.[ \/ ].x0,x0+r.[ holds f1.g<=f.g & f.g<=f2.g) implies f is_convergent_in x0 & lim(f,x0)=lim(f1,x0); theorem :: LIMFUNC3:47 f1 is_convergent_in x0 & f2 is_convergent_in x0 & (ex r st 0<r & ((dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) & for g st g in dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<=f2.g) or (dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) & for g st g in dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<= f2.g))) implies lim(f1,x0)<=lim(f2,x0); theorem :: LIMFUNC3:48 (f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0) implies f^ is_convergent_in x0 & lim(f^,x0)=0; theorem :: LIMFUNC3:49 f is_convergent_in x0 & lim(f,x0)=0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0) & (ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds 0<=f.g) implies f^ is_divergent_to+infty_in x0; theorem :: LIMFUNC3:50 f is_convergent_in x0 & lim(f,x0)=0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0) & (ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f.g<=0) implies f^ is_divergent_to-infty_in x0; theorem :: LIMFUNC3:51 f is_convergent_in x0 & lim(f,x0)=0 & (ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds 0<f.g) implies f^ is_divergent_to+infty_in x0; theorem :: LIMFUNC3:52 f is_convergent_in x0 & lim(f,x0)=0 & (ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f.g<0) implies f^ is_divergent_to-infty_in x0;