let e be positive Real; :: thesis: for f being Real_Sequence st ( for n being Element of NAT st n > 0 holds
f . n = log (2,(n to_power e)) ) holds
( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 )
let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n > 0 holds
f . n = log (2,(n to_power e)) ) implies ( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 ) )
assume A1: for n being Element of NAT st n > 0 holds
f . n = log (2,(n to_power e)) ; :: thesis: ( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 )
set g = seq_n^ e;
set h = f /" (seq_n^ e);

A2: now :: thesis: for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ e)) . n) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ e)) . n) - 0).| < p )
reconsider p1 = p as Real ;
set i0 = [/((7 / p1) to_power (1 / e))\];
set i1 = [/((p1 to_power (- (2 / e))) + 1)\];
set N = max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2);
A3: max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) >= max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]) by XXREAL_0:25;
A4: max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) is Integer

proof

per cases ( max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) = max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]) or max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) = 2 ) by XXREAL_0:16;

suppose max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) = max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]) ; :: thesis: max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) is Integer

hence max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) is Integer by XXREAL_0:16; :: thesis: verum

end;

suppose max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) = 2 ; :: thesis: max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) is Integer

hence max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) is Integer ; :: thesis: verum

end;

end;

end;

A5: (p to_power (- (2 / e))) + 1 > (p to_power (- (2 / e))) + 0 by XREAL_1:8;
[/((p1 to_power (- (2 / e))) + 1)\] >= (p to_power (- (2 / e))) + 1 by INT_1:def 7;
then A6: [/((p1 to_power (- (2 / e))) + 1)\] > p to_power (- (2 / e)) by A5, XXREAL_0:2;
assume A7: p > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n^ e)) . n) - 0).| < p
then A8: p1 to_power 2 > 0 by POWER:34;
max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]) >= [/((p1 to_power (- (2 / e))) + 1)\] by XXREAL_0:25;
then A9: max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) >= [/((p1 to_power (- (2 / e))) + 1)\] by A3, XXREAL_0:2;
A10: [/((7 / p1) to_power (1 / e))\] >= (7 / p) to_power (1 / e) by INT_1:def 7;
max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]) >= [/((7 / p1) to_power (1 / e))\] by XXREAL_0:25;
then A11: max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) >= [/((7 / p1) to_power (1 / e))\] by A3, XXREAL_0:2;
A12: max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) >= 2 by XXREAL_0:25;
A13: p1 to_power (- (2 / e)) > 0 by A7, POWER:34;
A14: 7 * (p ") > 7 * 0 by A7, XREAL_1:68;
then A15: (7 / p1) to_power (1 / e) > 0 by POWER:34;
max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) in NAT by A12, A4, INT_1:3;
then reconsider N = max ((max ([/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\])),2) as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((f /" (seq_n^ e)) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N implies |.(((f /" (seq_n^ e)) . n) - 0).| < p )
set c = p1 * (n to_power e);
assume A16: n >= N ; :: thesis: |.(((f /" (seq_n^ e)) . n) - 0).| < p
then n >= [/((7 / p1) to_power (1 / e))\] by A11, XXREAL_0:2;
then n >= (7 / p) to_power (1 / e) by A10, XXREAL_0:2;
then n to_power e >= ((7 / p) to_power (1 / e)) to_power e by A15, Lm6;
then n to_power e >= (7 / p1) to_power (e * (1 / e)) by A14, POWER:33;
then n to_power e >= (7 / p) to_power 1 by XCMPLX_1:106;
then n to_power e >= 7 / p1 by POWER:25;
then p * (n to_power e) >= (7 / p) * p by A7, XREAL_1:64;
then p * (n to_power e) >= 7 by A7, XCMPLX_1:87;
then p * (n to_power e) > 6 by XXREAL_0:2;
then A17: (p1 * (n to_power e)) ^2 < 2 to_power (p1 * (n to_power e)) by Lm9;
n >= [/((p1 to_power (- (2 / e))) + 1)\] by A9, A16, XXREAL_0:2;
then n > p to_power (- (2 / e)) by A6, XXREAL_0:2;
then n to_power e > (p to_power (- (2 / e))) to_power e by A13, POWER:37;
then n to_power e > p1 to_power ((- (2 / e)) * e) by A7, POWER:33;
then n to_power e > p to_power (- ((2 / e) * e)) ;
then n to_power e > p to_power (- 2) by XCMPLX_1:87;
then (p to_power 2) * (n to_power e) > (p to_power 2) * (p to_power (- 2)) by A8, XREAL_1:68;
then (p1 to_power 2) * (n to_power e) > p1 to_power (2 + (- 2)) by A7, POWER:27;
then (p1 to_power 2) * (n to_power e) > 1 by POWER:24;
then (p1 ^2) * (n to_power e) > 1 by POWER:46;
then A18: 1 / (p * (p1 * (n to_power e))) < 1 / 1 by XREAL_1:88;
2 to_power (p1 * (n to_power e)) > 0 by POWER:34;
then A19: (2 to_power (p1 * (n to_power e))) / ((p1 * (n to_power e)) * p) < (2 to_power (p1 * (n to_power e))) * 1 by A18, XREAL_1:68;
A20: n to_power e > 0 by A12, A16, POWER:34;
then p * (n to_power e) > p * 0 by A7, XREAL_1:68;
then p1 * (n to_power e) < (2 to_power (p1 * (n to_power e))) / (p1 * (n to_power e)) by A17, XREAL_1:81;
then n to_power e < ((2 to_power (p1 * (n to_power e))) / (p1 * (n to_power e))) / p by A7, XREAL_1:81;
then n to_power e < (2 to_power (p1 * (n to_power e))) / ((p1 * (n to_power e)) * p) by XCMPLX_1:78;
then n to_power e < 2 to_power (p1 * (n to_power e)) by A19, XXREAL_0:2;
then log (2,(n to_power e)) < log (2,(2 to_power (p1 * (n to_power e)))) by A20, POWER:57;
then log (2,(n to_power e)) < (p1 * (n to_power e)) * (log (2,2)) by POWER:55;
then log (2,(n to_power e)) < (p1 * (n to_power e)) * 1 by POWER:52;
then A21: (log (2,(n to_power e))) / (n to_power e) < p by A12, A16, POWER:34, XREAL_1:83;
n >= 2 by A12, A16, XXREAL_0:2;
then n > 1 by XXREAL_0:2;
then n to_power e > n to_power 0 by POWER:39;
then n to_power e > 1 by POWER:24;
then log (2,(n to_power e)) > log (2,1) by POWER:57;
then A22: log (2,(n to_power e)) > 0 by POWER:51;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
(f /" (seq_n^ e)) . n = (f . n) / ((seq_n^ e) . nn) by Lm4
.= (log (2,(nn to_power e))) / ((seq_n^ e) . n) by A1, A12, A16
.= (log (2,(nn to_power e))) / (n to_power e) by A12, A16, Def3 ;
hence |.(((f /" (seq_n^ e)) . n) - 0).| < p by A20, A21, A22, ABSVALUE:def 1; :: thesis: verum

end;

hence f /" (seq_n^ e) is convergent by SEQ_2:def 6; :: thesis: lim (f /" (seq_n^ e)) = 0
hence lim (f /" (seq_n^ e)) = 0 by A2, SEQ_2:def 7; :: thesis: verum