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 Nat such that
A2:
for n being Nat st n >= N holds
|.(((seq_logn /" (seq_n^ (1 / 2))) . n) - 0).| < 1 / 2
by A1, SEQ_2:def 7;
reconsider N = N as Element of NAT by ORDINAL1:def 12;
set N1 = max (2,N);
A3:
max (2,N) >= 2
by XXREAL_0:25;
A4:
max (2,N) >= N
by XXREAL_0:25;
now for n being Element of NAT st n >= max (2,N) holds
n / 2 < n - ((sqrt n) * (log (2,n)))let n be
Element of
NAT ;
( n >= max (2,N) implies n / 2 < n - ((sqrt n) * (log (2,n))) )assume A5:
n >= max (2,
N)
;
n / 2 < n - ((sqrt n) * (log (2,n)))then A6:
sqrt n > 0
by A3, SQUARE_1:25;
n >= N
by A4, A5, XXREAL_0:2;
then
|.(((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:25;
(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:68;
then
log (2,
n)
< (sqrt n) * (1 / 2)
by A8, XCMPLX_1:87;
then
(sqrt n) * (log (2,n)) < (sqrt n) * ((sqrt n) * (1 / 2))
by A6, XREAL_1:68;
then
(sqrt n) * (log (2,n)) < ((sqrt n) ^2) * (1 / 2)
;
then
(sqrt n) * (log (2,n)) < n * (1 / 2)
by SQUARE_1:def 2;
then
(n / 2) + ((sqrt n) * (log (2,n))) < (n / 2) + (n / 2)
by XREAL_1:6;
hence
n / 2
< n - ((sqrt n) * (log (2,n)))
by XREAL_1:20;
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
; verum