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 S₁[ 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 S₁[x,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[n,y]

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: ex y being Element of REAL st S₁[n,y]

hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: ex y being Element of REAL st S₁[n,y]

hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

end;

end;

consider h being Function of NAT ,REAL such that
A2: for x being Element of NAT holds S₁[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 A2; :: 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 A2; :: thesis: verum

end;

then consider p being Real_Sequence such that
A3: p . 0 = 0 and
A4: for n being Element of NAT st n > 0 holds
p . n = log 2,(n to_power e) ;
set q = p /" (seq_n^ e);
A5: p /" (seq_n^ e) is convergent by A4, Lm10;
A6: 1 = e / e by XCMPLX_1:60
.= e * (1 / e) ;
A7: for n being Element of NAT holds (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n)

proof

let n be Element of NAT ; :: thesis: (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n)
A8: (seq_logn /" (seq_n^ e)) . n = (seq_logn . n) / ((seq_n^ e) . n) by Lm4;
A9: (p /" (seq_n^ e)) . n = (p . n) / ((seq_n^ e) . n) by Lm4;

per cases ( n = 0 or n > 0 ) ;

suppose A10: 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 A8, Def2
.= 0 * (1 / e) ;
hence (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n) by A3, A9, A10; :: thesis: verum

end;

suppose A11: n > 0 ; :: thesis: (seq_logn /" (seq_n^ e)) . n = (1 / e) * ((p /" (seq_n^ e)) . n)

then A12: n to_power e > 0 by POWER:39;
(seq_logn /" (seq_n^ e)) . n = (log 2,n) / ((seq_n^ e) . n) by A8, A11, Def2
.= (log 2,(n to_power (e * (1 / e)))) / ((seq_n^ e) . n) by A6, POWER:30
.= (log 2,((n to_power e) to_power (1 / e))) / ((seq_n^ e) . n) by A11, POWER:38
.= ((1 / e) * (log 2,(n to_power e))) / ((seq_n^ e) . n) by A12, POWER:63
.= ((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 A4, A9, A11; :: thesis: verum

end;

end;

end;

then A13: seq_logn /" (seq_n^ e) = (1 / e) (#) (p /" (seq_n^ e)) by SEQ_1:13;
A14: lim (p /" (seq_n^ e)) = 0 by A4, Lm10;
lim (seq_logn /" (seq_n^ e)) = lim ((1 / e) (#) (p /" (seq_n^ e))) by A7, SEQ_1:13
.= (1 / e) * 0 by A5, A14, SEQ_2:22 ;
hence ( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 ) by A5, A13, SEQ_2:21; :: thesis: verum