set seq1 = seq_n^ (1 / 2);
set seq = seq_logn ;
set p = seq_logn /" (seq_n^ (1 / 2));
A1: lim (seq_logn /" (seq_n^ (1 / 2))) = 0 by Lm11;
seq_logn /" (seq_n^ (1 / 2)) is convergent by Lm11;
then consider N being Element of NAT such that
A2: for n being Element of NAT st n >= N holds
abs (((seq_logn /" (seq_n^ (1 / 2))) . n) - 0 ) < 1 / 2 by A1, SEQ_2:def 7;
set N1 = max 2,N;
A3: max 2,N >= 2 by XXREAL_0:25;
A4: max 2,N >= N by XXREAL_0:25;

now

let n be Element of NAT ; :: thesis: ( n >= max 2,N implies n / 2 < n - ((sqrt n) * (log 2,n)) )
assume A5: n >= max 2,N ; :: thesis: n / 2 < n - ((sqrt n) * (log 2,n))
then A6: sqrt n > 0 by A3, SQUARE_1:93;
n >= N by A4, A5, XXREAL_0:2;
then abs (((seq_logn /" (seq_n^ (1 / 2))) . n) - 0 ) < 1 / 2 by A2;
then A7: (seq_logn /" (seq_n^ (1 / 2))) . n < 1 / 2 by ABSVALUE:def 1;
A8: sqrt n <> 0 by A3, A5, SQUARE_1:93;
(seq_logn /" (seq_n^ (1 / 2))) . n = (seq_logn . n) / ((seq_n^ (1 / 2)) . n) by Lm4
.= (log 2,n) / ((seq_n^ (1 / 2)) . n) by A3, A5, Def2
.= (log 2,n) / (n to_power (1 / 2)) by A3, A5, Def3
.= (log 2,n) / (sqrt n) by Lm39 ;
then ((log 2,n) / (sqrt n)) * (sqrt n) < (sqrt n) * (1 / 2) by A6, A7, XREAL_1:70;
then log 2,n < (sqrt n) * (1 / 2) by A8, XCMPLX_1:88;
then (sqrt n) * (log 2,n) < (sqrt n) * ((sqrt n) * (1 / 2)) by A6, XREAL_1:70;
then (sqrt n) * (log 2,n) < ((sqrt n) ^2 ) * (1 / 2) ;
then (sqrt n) * (log 2,n) < n * (1 / 2) by SQUARE_1:def 4;
then (n / 2) + ((sqrt n) * (log 2,n)) < (n / 2) + (n / 2) by XREAL_1:8;
hence n / 2 < n - ((sqrt n) * (log 2,n)) by XREAL_1:22; :: thesis: verum

end;

hence ex N being Element of NAT st
for n being Element of NAT st n >= N holds
n - ((sqrt n) * (log 2,n)) > n / 2 ; :: thesis: verum