let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL holds
( f is_divergent_to+infty_in x0 iff ( f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0 ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_divergent_to+infty_in x0 iff ( f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0 ) )
thus ( f is_divergent_to+infty_in x0 implies ( f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0 ) ) :: thesis: ( f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0 implies f is_divergent_to+infty_in x0 )
proof
assume A1: f is_divergent_to+infty_in x0 ; :: thesis: ( f is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0 )
A2: now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) /\ (left_open_halfline x0) holds
f /* s is divergent_to+infty
let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) /\ (left_open_halfline x0) implies f /* s is divergent_to+infty )
assume that
A3: s is convergent and
A4: lim s = x0 and
A5: rng s c= (dom f) /\ (left_open_halfline x0) ; :: thesis: f /* s is divergent_to+infty
rng s c= (dom f) \ {x0} by A5, Th1;
hence f /* s is divergent_to+infty by A1, A3, A4; :: thesis: verum
end;
A6: now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) /\ (right_open_halfline x0) holds
f /* s is divergent_to+infty
let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) /\ (right_open_halfline x0) implies f /* s is divergent_to+infty )
assume that
A7: s is convergent and
A8: lim s = x0 and
A9: rng s c= (dom f) /\ (right_open_halfline x0) ; :: thesis: f /* s is divergent_to+infty
rng s c= (dom f) \ {x0} by A9, Th1;
hence f /* s is divergent_to+infty by A1, A7, A8; :: thesis: verum
end;
A10: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A1;
then for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) by Th8;
hence f is_left_divergent_to+infty_in x0 by A2, LIMFUNC2:def 2; :: thesis: f is_right_divergent_to+infty_in x0
for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) by A10, Th8;
hence f is_right_divergent_to+infty_in x0 by A6, LIMFUNC2:def 5; :: thesis: verum
end;
assume that
A11: f is_left_divergent_to+infty_in x0 and
A12: f is_right_divergent_to+infty_in x0 ; :: thesis: f is_divergent_to+infty_in x0
A13: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) by A12, LIMFUNC2:def 5;
A14: now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} holds
f /* s is divergent_to+infty
let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies f /* s is divergent_to+infty )
assume that
A15: s is convergent and
A16: lim s = x0 and
A17: rng s c= (dom f) \ {x0} ; :: thesis: f /* s is divergent_to+infty
now :: thesis: f /* s is divergent_to+infty
per cases ( ex k being Element of NAT st
for n being Element of NAT st k <= n holds
s . n < x0 or for k being Element of NAT ex n being Element of NAT st
( k <= n & s . n >= x0 ) ) ;
suppose ex k being Element of NAT st
for n being Element of NAT st k <= n holds
s . n < x0 ; :: thesis: f /* s is divergent_to+infty
then consider k being Element of NAT such that
A18: for n being Element of NAT st k <= n holds
s . n < x0 ;
A19: rng s c= dom f by A17, XBOOLE_1:1;
A20: rng (s ^\ k) c= (dom f) /\ (left_open_halfline x0)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s ^\ k) or x in (dom f) /\ (left_open_halfline x0) )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f) /\ (left_open_halfline x0)
then consider n being Element of NAT such that
A21: (s ^\ k) . n = x by FUNCT_2:113;
s . (n + k) < x0 by A18, NAT_1:12;
then s . (n + k) in { g1 where g1 is Real : g1 < x0 } ;
then s . (n + k) in left_open_halfline x0 by XXREAL_1:229;
then A22: x in left_open_halfline x0 by A21, NAT_1:def 3;
s . (n + k) in rng s by VALUED_0:28;
then x in rng s by A21, NAT_1:def 3;
hence x in (dom f) /\ (left_open_halfline x0) by A19, A22, XBOOLE_0:def 4; :: thesis: verum
end;
A23: f /* (s ^\ k) = (f /* s) ^\ k by A17, VALUED_0:27, XBOOLE_1:1;
lim (s ^\ k) = x0 by A15, A16, SEQ_4:20;
then f /* (s ^\ k) is divergent_to+infty by A11, A15, A20, LIMFUNC2:def 2;
hence f /* s is divergent_to+infty by A23, LIMFUNC1:7; :: thesis: verum
end;
suppose A24: for k being Element of NAT ex n being Element of NAT st
( k <= n & s . n >= x0 ) ; :: thesis: f /* s is divergent_to+infty
now :: thesis: f /* s is divergent_to+infty
per cases ( ex k being Element of NAT st
for n being Element of NAT st k <= n holds
x0 < s . n or for k being Element of NAT ex n being Element of NAT st
( k <= n & x0 >= s . n ) ) ;
suppose ex k being Element of NAT st
for n being Element of NAT st k <= n holds
x0 < s . n ; :: thesis: f /* s is divergent_to+infty
then consider k being Element of NAT such that
A25: for n being Element of NAT st k <= n holds
s . n > x0 ;
A26: rng s c= dom f by A17, XBOOLE_1:1;
A27: rng (s ^\ k) c= (dom f) /\ (right_open_halfline x0)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s ^\ k) or x in (dom f) /\ (right_open_halfline x0) )
assume x in rng (s ^\ k) ; :: thesis: x in (dom f) /\ (right_open_halfline x0)
then consider n being Element of NAT such that
A28: (s ^\ k) . n = x by FUNCT_2:113;
x0 < s . (n + k) by A25, NAT_1:12;
then s . (n + k) in { g1 where g1 is Real : x0 < g1 } ;
then s . (n + k) in right_open_halfline x0 by XXREAL_1:230;
then A29: x in right_open_halfline x0 by A28, NAT_1:def 3;
s . (n + k) in rng s by VALUED_0:28;
then x in rng s by A28, NAT_1:def 3;
hence x in (dom f) /\ (right_open_halfline x0) by A26, A29, XBOOLE_0:def 4; :: thesis: verum
end;
A30: f /* (s ^\ k) = (f /* s) ^\ k by A17, VALUED_0:27, XBOOLE_1:1;
lim (s ^\ k) = x0 by A15, A16, SEQ_4:20;
then f /* (s ^\ k) is divergent_to+infty by A12, A15, A27, LIMFUNC2:def 5;
hence f /* s is divergent_to+infty by A30, LIMFUNC1:7; :: thesis: verum
end;
suppose A31: for k being Element of NAT ex n being Element of NAT st
( k <= n & x0 >= s . n ) ; :: thesis: f /* s is divergent_to+infty
defpred S1[ Nat] means s . $1 < x0;
A32: now :: thesis: for k being Element of NAT ex n being Element of NAT st
( k <= n & s . n < x0 )
let k be Element of NAT ; :: thesis: ex n being Element of NAT st
( k <= n & s . n < x0 )
consider n being Element of NAT such that
A33: k <= n and
A34: s . n <= x0 by A31;
take n = n; :: thesis: ( k <= n & s . n < x0 )
thus k <= n by A33; :: thesis: s . n < x0
s . n in rng s by VALUED_0:28;
then not s . n in {x0} by A17, XBOOLE_0:def 5;
then s . n <> x0 by TARSKI:def 1;
hence s . n < x0 by A34, XXREAL_0:1; :: thesis: verum
end;
then ex m1 being Element of NAT st
( 0 <= m1 & s . m1 < x0 ) ;
then A35: ex m being Nat st S1[m] ;
consider M being Nat such that
A36: ( S1[M] & ( for n being Nat st S1[n] holds
M <= n ) ) from NAT_1:sch 5(A35);
defpred S2[ Nat] means s . $1 > x0;
defpred S3[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds
( n < m & s . m < x0 & ( for k being Element of NAT st n < k & s . k < x0 holds
m <= k ) );
defpred S4[ Nat, set , set ] means S3[$2,$3];
reconsider M9 = M as Element of NAT by ORDINAL1:def 12;
A37: now :: thesis: for n being Element of NAT ex m being Element of NAT st
( n < m & s . m < x0 )
let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n < m & s . m < x0 )
consider m being Element of NAT such that
A38: n + 1 <= m and
A39: s . m < x0 by A32;
take m = m; :: thesis: ( n < m & s . m < x0 )
thus ( n < m & s . m < x0 ) by A38, A39, NAT_1:13; :: thesis: verum
end;
A40: for n being Nat
for x being Element of NAT ex y being Element of NAT st S4[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S4[n,x,y]
let x be Element of NAT ; :: thesis: ex y being Element of NAT st S4[n,x,y]
defpred S5[ Nat] means ( x < $1 & s . $1 < x0 );
ex m being Element of NAT st S5[m] by A37;
then A41: ex m being Nat st S5[m] ;
consider l being Nat such that
A42: ( S5[l] & ( for k being Nat st S5[k] holds
l <= k ) ) from NAT_1:sch 5(A41);
 take l ; :: thesis: ( l is Element of NAT & S4[n,x,l] )
l in NAT by ORDINAL1:def 12;
hence ( l is Element of NAT & S4[n,x,l] ) by A42; :: thesis: verum
end;
consider F being sequence of NAT such that
A43: ( F . 0 = M9 & ( for n being Nat holds S4[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A40);
A44: rng F c= NAT by RELAT_1:def 19;
then A45: rng F c= REAL by NUMBERS:19;
A46: dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Real_Sequence by A45, RELSET_1:4;
A47: now :: thesis: for n being Element of NAT holds F . n is Element of NAT
let n be Element of NAT ; :: thesis: F . n is Element of NAT
F . n in rng F by A46, FUNCT_1:def 3;
hence F . n is Element of NAT by A44; :: thesis: verum
end;
now :: thesis: for n being Nat holds F . n < F . (n + 1)
let n be Nat; :: thesis: F . n < F . (n + 1)
A48: F . (n + 1) is Element of NAT by A47;
A49: n in NAT by ORDINAL1:def 12;
F . n is Element of NAT by A47, A49;
hence F . n < F . (n + 1) by A43, A48; :: thesis: verum
end;
then reconsider F = F as increasing sequence of NAT by SEQM_3:def 6;
A50: s * F is subsequence of s by VALUED_0:def 17;
then rng (s * F) c= rng s by VALUED_0:21;
then A51: rng (s * F) c= (dom f) \ {x0} by A17;
A52: for n being Element of NAT st s . n < x0 holds
ex m being Element of NAT st F . m = n
proof
defpred S5[ Nat] means ( s . $1 < x0 & ( for m being Element of NAT holds F . m <> $1 ) );
assume ex n being Element of NAT st S5[n] ; :: thesis: contradiction
then A53: ex n being Nat st S5[n] ;
consider M1 being Nat such that
A54: ( S5[M1] & ( for n being Nat st S5[n] holds
M1 <= n ) ) from NAT_1:sch 5(A53);
 defpred S6[ Nat] means ( $1 < M1 & s . $1 < x0 & ex m being Element of NAT st F . m = $1 );
A55: ex n being Nat st S6[n]
proof
take M ; :: thesis: S6[M]
A56: M <> M1 by A43, A54;
M <= M1 by A36, A54;
hence M < M1 by A56, XXREAL_0:1; :: thesis: ( s . M < x0 & ex m being Element of NAT st F . m = M )
thus s . M < x0 by A36; :: thesis: ex m being Element of NAT st F . m = M
take 0 ; :: thesis: F . 0 = M
thus F . 0 = M by A43; :: thesis: verum
end;
A57: for n being Nat st S6[n] holds
n <= M1 ;
consider MX being Nat such that
A58: ( S6[MX] & ( for n being Nat st S6[n] holds
n <= MX ) ) from NAT_1:sch 6(A57, A55);
 A59: for k being Element of NAT st MX < k & k < M1 holds
s . k >= x0
proof
given k being Element of NAT such that A60: MX < k and
A61: k < M1 and
A62: s . k < x0 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( ex m being Element of NAT st F . m = k or for m being Element of NAT holds F . m <> k ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider m being Element of NAT such that
A63: F . m = MX by A58;
M1 in NAT by ORDINAL1:def 12;
then A64: F . (m + 1) <= M1 by A43, A54, A58, A63;
A65: s . (F . (m + 1)) < x0 by A43, A63;
A66: MX < F . (m + 1) by A43, A63;
now :: thesis: not F . (m + 1) <> M1
assume F . (m + 1) <> M1 ; :: thesis: contradiction
then F . (m + 1) < M1 by A64, XXREAL_0:1;
hence contradiction by A59, A66, A65; :: thesis: verum
end;
hence contradiction by A54; :: thesis: verum
end;
A67: now :: thesis: for k being Element of NAT ex n being Element of NAT st
( k <= n & s . n > x0 )
let k be Element of NAT ; :: thesis: ex n being Element of NAT st
( k <= n & s . n > x0 )
consider n being Element of NAT such that
A68: k <= n and
A69: s . n >= x0 by A24;
take n = n; :: thesis: ( k <= n & s . n > x0 )
thus k <= n by A68; :: thesis: s . n > x0
s . n in rng s by VALUED_0:28;
then not s . n in {x0} by A17, XBOOLE_0:def 5;
then s . n <> x0 by TARSKI:def 1;
hence s . n > x0 by A69, XXREAL_0:1; :: thesis: verum
end;
then ex mn being Element of NAT st
( 0 <= mn & s . mn > x0 ) ;
then A70: ex m being Nat st S2[m] ;
consider N being Nat such that
A71: ( S2[N] & ( for n being Nat st S2[n] holds
N <= n ) ) from NAT_1:sch 5(A70);
defpred S5[ Nat] means (s * F) . $1 < x0;
A72: for k being Nat st S5[k] holds
S5[k + 1]
proof
let k be Nat; :: thesis: ( S5[k] implies S5[k + 1] )
assume (s * F) . k < x0 ; :: thesis: S5[k + 1]
S3[F . k,F . (k + 1)] by A43;
then s . (F . (k + 1)) < x0 ;
hence S5[k + 1] by FUNCT_2:15; :: thesis: verum
end;
A73: S5[ 0 ] by A36, A43, FUNCT_2:15;
A74: for k being Nat holds S5[k] from NAT_1:sch 2(A73, A72);
A75: rng (s * F) c= (dom f) /\ (left_open_halfline x0)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s * F) or x in (dom f) /\ (left_open_halfline x0) )
assume A76: x in rng (s * F) ; :: thesis: x in (dom f) /\ (left_open_halfline x0)
then consider n being Element of NAT such that
A77: (s * F) . n = x by FUNCT_2:113;
(s * F) . n < x0 by A74;
then x in { g1 where g1 is Real : g1 < x0 } by A77;
then A78: x in left_open_halfline x0 by XXREAL_1:229;
x in dom f by A51, A76, XBOOLE_0:def 5;
hence x in (dom f) /\ (left_open_halfline x0) by A78, XBOOLE_0:def 4; :: thesis: verum
end;
defpred S6[ set , set ] means for n, m being Element of NAT st $1 = n & $2 = m holds
( n < m & s . m > x0 & ( for k being Element of NAT st n < k & s . k > x0 holds
m <= k ) );
defpred S7[ Nat, set , set ] means S6[$2,$3];
A79: s * F is convergent by A15, A50, SEQ_4:16;
reconsider N9 = N as Element of NAT by ORDINAL1:def 12;
A80: now :: thesis: for n being Element of NAT ex m being Element of NAT st
( n < m & s . m > x0 )
let n be Element of NAT ; :: thesis: ex m being Element of NAT st
( n < m & s . m > x0 )
consider m being Element of NAT such that
A81: n + 1 <= m and
A82: s . m > x0 by A67;
take m = m; :: thesis: ( n < m & s . m > x0 )
thus ( n < m & s . m > x0 ) by A81, A82, NAT_1:13; :: thesis: verum
end;
A83: for n being Nat
for x being Element of NAT ex y being Element of NAT st S7[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S7[n,x,y]
let x be Element of NAT ; :: thesis: ex y being Element of NAT st S7[n,x,y]
defpred S8[ Nat] means ( x < $1 & s . $1 > x0 );
ex m being Element of NAT st S8[m] by A80;
then A84: ex m being Nat st S8[m] ;
consider l being Nat such that
A85: ( S8[l] & ( for k being Nat st S8[k] holds
l <= k ) ) from NAT_1:sch 5(A84);
 reconsider l = l as Element of NAT by ORDINAL1:def 12;
take l ; :: thesis: S7[n,x,l]
thus S7[n,x,l] by A85; :: thesis: verum
end;
consider G being sequence of NAT such that
A86: ( G . 0 = N9 & ( for n being Nat holds S7[n,G . n,G . (n + 1)] ) ) from RECDEF_1:sch 2(A83);
A87: rng G c= NAT by RELAT_1:def 19;
then A88: rng G c= REAL by NUMBERS:19;
A89: dom G = NAT by FUNCT_2:def 1;
then reconsider G = G as Real_Sequence by A88, RELSET_1:4;
A90: now :: thesis: for n being Element of NAT holds G . n is Element of NAT
let n be Element of NAT ; :: thesis: G . n is Element of NAT
G . n in rng G by A89, FUNCT_1:def 3;
hence G . n is Element of NAT by A87; :: thesis: verum
end;
now :: thesis: for n being Nat holds G . n < G . (n + 1)
let n be Nat; :: thesis: G . n < G . (n + 1)
A91: n in NAT by ORDINAL1:def 12;
A92: G . (n + 1) is Element of NAT by A90;
G . n is Element of NAT by A90, A91;
hence G . n < G . (n + 1) by A86, A92; :: thesis: verum
end;
then reconsider G = G as increasing sequence of NAT by SEQM_3:def 6;
A93: s * G is subsequence of s by VALUED_0:def 17;
then rng (s * G) c= rng s by VALUED_0:21;
then A94: rng (s * G) c= (dom f) \ {x0} by A17;
defpred S8[ Nat] means ( s . $1 > x0 & ( for m being Element of NAT holds G . m <> $1 ) );
A95: for n being Element of NAT st s . n > x0 holds
ex m being Element of NAT st G . m = n
proof
assume ex n being Element of NAT st S8[n] ; :: thesis: contradiction
then A96: ex n being Nat st S8[n] ;
consider N1 being Nat such that
A97: ( S8[N1] & ( for n being Nat st S8[n] holds
N1 <= n ) ) from NAT_1:sch 5(A96);
 defpred S9[ Nat] means ( $1 < N1 & s . $1 > x0 & ex m being Element of NAT st G . m = $1 );
A98: ex n being Nat st S9[n]
proof
take N ; :: thesis: S9[N]
A99: N <> N1 by A86, A97;
N <= N1 by A71, A97;
hence N < N1 by A99, XXREAL_0:1; :: thesis: ( s . N > x0 & ex m being Element of NAT st G . m = N )
thus s . N > x0 by A71; :: thesis: ex m being Element of NAT st G . m = N
take 0 ; :: thesis: G . 0 = N
thus G . 0 = N by A86; :: thesis: verum
end;
A100: for n being Nat st S9[n] holds
n <= N1 ;
consider NX being Nat such that
A101: ( S9[NX] & ( for n being Nat st S9[n] holds
n <= NX ) ) from NAT_1:sch 6(A100, A98);
 A102: for k being Element of NAT st NX < k & k < N1 holds
s . k <= x0
proof
given k being Element of NAT such that A103: NX < k and
A104: k < N1 and
A105: s . k > x0 ; :: thesis: contradiction
now :: thesis: contradiction
per cases ( ex m being Element of NAT st G . m = k or for m being Element of NAT holds G . m <> k ) ;
end;
end;
hence contradiction ; :: thesis: verum
end;
consider m being Element of NAT such that
A106: G . m = NX by A101;
N1 in NAT by ORDINAL1:def 12;
then A107: G . (m + 1) <= N1 by A86, A97, A101, A106;
A108: s . (G . (m + 1)) > x0 by A86, A106;
A109: NX < G . (m + 1) by A86, A106;
now :: thesis: not G . (m + 1) <> N1
assume G . (m + 1) <> N1 ; :: thesis: contradiction
then G . (m + 1) < N1 by A107, XXREAL_0:1;
hence contradiction by A102, A109, A108; :: thesis: verum
end;
hence contradiction by A97; :: thesis: verum
end;
defpred S9[ Nat] means (s * G) . $1 > x0;
A110: for k being Nat st S9[k] holds
S9[k + 1]
proof
let k be Nat; :: thesis: ( S9[k] implies S9[k + 1] )
assume (s * G) . k > x0 ; :: thesis: S9[k + 1]
S6[G . k,G . (k + 1)] by A86;
then s . (G . (k + 1)) > x0 ;
hence S9[k + 1] by FUNCT_2:15; :: thesis: verum
end;
A111: S9[ 0 ] by A71, A86, FUNCT_2:15;
A112: for k being Nat holds S9[k] from NAT_1:sch 2(A111, A110);
A113: rng (s * G) c= (dom f) /\ (right_open_halfline x0)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (s * G) or x in (dom f) /\ (right_open_halfline x0) )
assume A114: x in rng (s * G) ; :: thesis: x in (dom f) /\ (right_open_halfline x0)
then consider n being Element of NAT such that
A115: (s * G) . n = x by FUNCT_2:113;
(s * G) . n > x0 by A112;
then x in { g1 where g1 is Real : x0 < g1 } by A115;
then A116: x in right_open_halfline x0 by XXREAL_1:230;
x in dom f by A94, A114, XBOOLE_0:def 5;
hence x in (dom f) /\ (right_open_halfline x0) by A116, XBOOLE_0:def 4; :: thesis: verum
end;
A117: s * G is convergent by A15, A93, SEQ_4:16;
lim (s * G) = x0 by A15, A16, A93, SEQ_4:17;
then A118: f /* (s * G) is divergent_to+infty by A12, A117, A113, LIMFUNC2:def 5;
lim (s * F) = x0 by A15, A16, A50, SEQ_4:17;
then A119: f /* (s * F) is divergent_to+infty by A11, A79, A75, LIMFUNC2:def 2;
now :: thesis: for r being Real ex n being Nat st
for k being Nat st n <= k holds
r < (f /* s) . k
let r be Real; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
r < (f /* s) . k
consider n1 being Nat such that
A120: for k being Nat st n1 <= k holds
r < (f /* (s * F)) . k by A119;
consider n2 being Nat such that
A121: for k being Nat st n2 <= k holds
r < (f /* (s * G)) . k by A118;
reconsider n = max ((F . n1),(G . n2)) as Nat ;
take n = n; :: thesis: for k being Nat st n <= k holds
r < (f /* s) . k
let k be Nat; :: thesis: ( n <= k implies r < (f /* s) . k )
A122: k in NAT by ORDINAL1:def 12;
assume A123: n <= k ; :: thesis: r < (f /* s) . k
s . k in rng s by VALUED_0:28;
then not s . k in {x0} by A17, XBOOLE_0:def 5;
then A124: s . k <> x0 by TARSKI:def 1;
now :: thesis: r < (f /* s) . k
per cases ( s . k < x0 or s . k > x0 ) by A124, XXREAL_0:1;
suppose s . k < x0 ; :: thesis: r < (f /* s) . k
then consider l being Element of NAT such that
A125: k = F . l by A52, A122;
F . n1 <= n by XXREAL_0:25;
then F . n1 <= k by A123, XXREAL_0:2;
then l >= n1 by A125, SEQM_3:1;
then r < (f /* (s * F)) . l by A120;
then r < f . ((s * F) . l) by A51, FUNCT_2:108, XBOOLE_1:1;
then r < f . (s . k) by A125, FUNCT_2:15;
hence r < (f /* s) . k by A17, FUNCT_2:108, XBOOLE_1:1, A122; :: thesis: verum
end;
suppose s . k > x0 ; :: thesis: r < (f /* s) . k
then consider l being Element of NAT such that
A126: k = G . l by A95, A122;
G . n2 <= n by XXREAL_0:25;
then G . n2 <= k by A123, XXREAL_0:2;
then l >= n2 by A126, SEQM_3:1;
then r < (f /* (s * G)) . l by A121;
then r < f . ((s * G) . l) by A94, FUNCT_2:108, XBOOLE_1:1;
then r < f . (s . k) by A126, FUNCT_2:15;
hence r < (f /* s) . k by A17, FUNCT_2:108, XBOOLE_1:1, A122; :: thesis: verum
end;
end;
end;
hence r < (f /* s) . k ; :: thesis: verum
end;
hence f /* s is divergent_to+infty ; :: thesis: verum
end;
end;
end;
hence f /* s is divergent_to+infty ; :: thesis: verum
end;
end;
end;
hence f /* s is divergent_to+infty ; :: thesis: verum
end;
for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) by A11, LIMFUNC2:def 2;
then for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) by A13, Th8;
hence f is_divergent_to+infty_in x0 by A14; :: thesis: verum