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

let p be real number ; :: thesis: ( p > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ e)) . n) - 0 ) < p )
reconsider p1 = p as Real by XREAL_0:def 1;
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:10;
[/((p1 to_power (- (2 / e))) + 1)\] >= (p to_power (- (2 / e))) + 1 by INT_1:def 5;
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 Element of NAT st
for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ e)) . n) - 0 ) < p
then A8: p1 to_power 2 > 0 by POWER:39;
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 5;
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:39;
A14: 7 * (p " ) > 7 * 0 by A7, XREAL_1:70;
then A15: (7 / p1) to_power (1 / e) > 0 by POWER:39;
reconsider N = max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 as Element of NAT by A12, A4, INT_1:16;
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ e)) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N implies abs (((f /" (seq_n^ e)) . n) - 0 ) < p )
set c = p1 * (n to_power e);
assume A16: n >= N ; :: thesis: abs (((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:38;
then n to_power e >= (7 / p) to_power 1 by XCMPLX_1:107;
then n to_power e >= 7 / p1 by POWER:30;
then p * (n to_power e) >= (7 / p) * p by A7, XREAL_1:66;
then p * (n to_power e) >= 7 by A7, XCMPLX_1:88;
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:42;
then n to_power e > p1 to_power ((- (2 / e)) * e) by A7, POWER:38;
then n to_power e > p to_power (- ((2 / e) * e)) ;
then n to_power e > p to_power (- 2) by XCMPLX_1:88;
then (p to_power 2) * (n to_power e) > (p to_power 2) * (p to_power (- 2)) by A8, XREAL_1:70;
then (p1 to_power 2) * (n to_power e) > p1 to_power (2 + (- 2)) by A7, POWER:32;
then (p1 to_power 2) * (n to_power e) > 1 by POWER:29;
then (p1 ^2 ) * (n to_power e) > 1 by POWER:53;
then A18: 1 / (p * (p1 * (n to_power e))) < 1 / 1 by XREAL_1:90;
2 to_power (p1 * (n to_power e)) > 0 by POWER:39;
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:70;
A20: n to_power e > 0 by A12, A16, POWER:39;
then p * (n to_power e) > p * 0 by A7, XREAL_1:70;
then p1 * (n to_power e) < (2 to_power (p1 * (n to_power e))) / (p1 * (n to_power e)) by A17, XREAL_1:83;
then n to_power e < ((2 to_power (p1 * (n to_power e))) / (p1 * (n to_power e))) / p by A7, XREAL_1:83;
then n to_power e < (2 to_power (p1 * (n to_power e))) / ((p1 * (n to_power e)) * p) by XCMPLX_1:79;
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:65;
then log 2,(n to_power e) < (p1 * (n to_power e)) * (log 2,2) by POWER:63;
then log 2,(n to_power e) < (p1 * (n to_power e)) * 1 by POWER:60;
then A21: (log 2,(n to_power e)) / (n to_power e) < p by A12, A16, POWER:39, XREAL_1:85;
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:44;
then n to_power e > 1 by POWER:29;
then log 2,(n to_power e) > log 2,1 by POWER:65;
then A22: log 2,(n to_power e) > 0 by POWER:59;
(f /" (seq_n^ e)) . n = (f . n) / ((seq_n^ e) . n) by Lm4
.= (log 2,(n to_power e)) / ((seq_n^ e) . n) by A1, A12, A16
.= (log 2,(n to_power e)) / (n to_power e) by A12, A16, Def3 ;
hence abs (((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