set f = seq_logn ;
let e be Real; :: thesis: ( e > 0 implies ( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 ) )
assume e > 0 ; :: thesis: ( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 )
then reconsider e = e as positive Real ;
set g = seq_n^ e;
set h = seq_logn /" (seq_n^ e);
ex s being Real_Sequence st
( s . 0 = 0 & ( for n being Element of NAT st n > 0 holds
s . n = log (2,(n to_power e)) ) )
proof
defpred S1[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = log (2,($1 to_power e)) ) );
A1: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of REAL st S1[n,y]
per cases ( n = zz or n > 0 ) ;
suppose n = zz ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
suppose A2: n > 0 ; :: thesis: ex y being Element of REAL st S1[n,y]
log (2,(n to_power e)) in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S1[n,y] by A2; :: thesis: verum
end;
end;
end;
consider h being sequence of REAL such that
A3: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A1);
 take h ; :: thesis: ( h . 0 = 0 & ( for n being Element of NAT st n > 0 holds
h . n = log (2,(n to_power e)) ) )
thus h . 0 = 0 by A3; :: thesis: for n being Element of NAT st n > 0 holds
h . n = log (2,(n to_power e))
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = log (2,(n to_power e)) )
thus ( n > 0 implies h . n = log (2,(n to_power e)) ) by A3; :: thesis: verum
end;
then consider p being Real_Sequence such that
A4: p . 0 = 0 and
A5: for n being Element of NAT st n > 0 holds
p . n = log (2,(n to_power e)) ;
set q = p /" (seq_n^ e);
A6: p /" (seq_n^ e) is convergent by A5, Lm10;
A7: 1 = e / e by XCMPLX_1:60
.= e * (1 / e) ;
A8: for n being Nat holds (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n)
proof
let n be Nat; :: thesis: (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n)
A9: n in NAT by ORDINAL1:def 12;
A10: (seq_logn /" (seq_n^ e)) . n = (seq_logn . n) / ((seq_n^ e) . n) by Lm4;
A11: (p /" (seq_n^ e)) . n = (p . n) / ((seq_n^ e) . n) by Lm4;
per cases ( n = 0 or n > 0 ) ;
suppose A12: n = 0 ; :: thesis: (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n)
then (seq_logn /" (seq_n^ e)) . n = 0 / ((seq_n^ e) . n) by A10, Def2
.= 0 * (1 / e) ;
hence (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n) by A4, A11, A12; :: thesis: verum
end;
suppose A13: n > 0 ; :: thesis: (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n)
then A14: n to_power e > 0 by POWER:34;
(seq_logn /" (seq_n^ e)) . n = (log (2,n)) / ((seq_n^ e) . n) by A10, A13, Def2, A9
.= (log (2,(n to_power (e * (1 / e))))) / ((seq_n^ e) . n) by A7, POWER:25
.= (log (2,((n to_power e) to_power (1 / e)))) / ((seq_n^ e) . n) by A13, POWER:33
.= ((1 / e) * (log (2,(n to_power e)))) / ((seq_n^ e) . n) by A14, POWER:55
.= ((1 / e) * (log (2,(n to_power e)))) * (((seq_n^ e) . n) ")
.= (1 / e) * ((log (2,(n to_power e))) * (((seq_n^ e) . n) "))
.= (1 / e) * ((log (2,(n to_power e))) / ((seq_n^ e) . n)) ;
hence (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n) by A5, A11, A13, A9; :: thesis: verum
end;
end;
end;
then A15: seq_logn /" (seq_n^ e) = (1 / e) (#) (p /" (seq_n^ e)) by SEQ_1:9;
A16: lim (p /" (seq_n^ e)) = 0 by A5, Lm10;
lim (seq_logn /" (seq_n^ e)) = lim ((1 / e) (#) (p /" (seq_n^ e))) by A8, SEQ_1:9
.= (1 / e) * 0 by A6, A16, SEQ_2:8 ;
hence ( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 ) by A6, A15, SEQ_2:7; :: thesis: verum