ex N being Element of NAT st
for n being Element of NAT st n >= N holds
n / 2 > (log (2,n)) * (log (2,n))
proof
reconsider N = 2
to_power 10 as
Element of
NAT ;
now ex N being Element of NAT st
for n being Element of NAT st n >= N holds
n / 2 > (log (2,n)) * (log (2,n))take N =
N;
for n being Element of NAT st n >= N holds
n / 2 > (log (2,n)) * (log (2,n))let n be
Element of
NAT ;
( n >= N implies n / 2 > (log (2,n)) * (log (2,n)) )set x =
log (2,
n);
A1:
2
to_power 9
> 0
by POWER:34;
assume A2:
n >= N
;
n / 2 > (log (2,n)) * (log (2,n))then A3:
n > 0
by POWER:34;
2
to_power 10
> 2
to_power 0
by POWER:39;
then
n > 2
to_power 0
by A2, XXREAL_0:2;
then
n > 1
by POWER:24;
then
log (2,
n)
> log (2,1)
by POWER:57;
then
log (2,
n)
> 0
by POWER:51;
then
(log (2,n)) * (log (2,n)) > 0 * (log (2,n))
by XREAL_1:68;
then A4:
4
* ((log (2,n)) * (log (2,n))) > 2
* ((log (2,n)) * (log (2,n)))
by XREAL_1:68;
2
to_power 10
> 2
to_power 1
by POWER:39;
then
n > 2
to_power 1
by A2, XXREAL_0:2;
then A5:
n > 2
by POWER:25;
then A6:
2
* n > 2
* 2
by XREAL_1:68;
n * n > 2
* n
by A5, XREAL_1:68;
then
n ^2 > 2
* 2
by A6, XXREAL_0:2;
then
log (2,
(n ^2))
> log (2,
(2 ^2))
by POWER:57;
then
log (2,
(n ^2))
> log (2,
(2 to_power 2))
by POWER:46;
then
log (2,
(n ^2))
> 2
* (log (2,2))
by POWER:55;
then A7:
log (2,
(n ^2))
> 2
* 1
by POWER:52;
then A8:
(log (2,(n ^2))) ^2 > 0
by SQUARE_1:12;
2
to_power 10
> 2
to_power 9
by POWER:39;
then
n > 2
to_power 9
by A2, XXREAL_0:2;
then
log (2,
n)
> log (2,
(2 to_power 9))
by A1, POWER:57;
then
log (2,
n)
> 9
* (log (2,2))
by POWER:55;
then A9:
log (2,
n)
> 9
* 1
by POWER:52;
then A10:
2
* (log (2,n)) > 0 * (log (2,n))
by XREAL_1:68;
then
(2 * (log (2,n))) * (2 * (log (2,n))) > 0 * (2 * (log (2,n)))
by XREAL_1:68;
then
log (2,
(2 to_power (log (2,n))))
> log (2,
((2 * (log (2,n))) ^2))
by A9, Lm31, POWER:57;
then
(log (2,n)) * (log (2,2)) > log (2,
((2 * (log (2,n))) ^2))
by POWER:55;
then
(log (2,n)) * 1
> log (2,
((2 * (log (2,n))) ^2))
by POWER:52;
then
log (2,
n)
> log (2,
((2 * (log (2,n))) to_power 2))
by POWER:46;
then
log (2,
n)
> 2
* (log (2,(2 * (log (2,n)))))
by A10, POWER:55;
then
log (2,
n)
> 2
* (log (2,(log (2,(n to_power 2)))))
by A3, POWER:55;
then
log (2,
n)
> 2
* (log (2,(log (2,(n ^2)))))
by POWER:46;
then
2
to_power (log (2,n)) > 2
to_power (2 * (log (2,(log (2,(n ^2))))))
by POWER:39;
then
n > 2
to_power (2 * (log (2,(log (2,(n ^2))))))
by A3, POWER:def 3;
then
n > 2
to_power (log (2,((log (2,(n ^2))) to_power 2)))
by A7, POWER:55;
then
n > 2
to_power (log (2,((log (2,(n ^2))) ^2)))
by POWER:46;
then
n > (log (2,(n ^2))) ^2
by A8, POWER:def 3;
then
n > (log (2,(n to_power 2))) ^2
by POWER:46;
then
n > (2 * (log (2,n))) ^2
by A3, POWER:55;
then
n > 2
* ((log (2,n)) * (log (2,n)))
by A4, XXREAL_0:2;
hence
n / 2
> (log (2,n)) * (log (2,n))
by XREAL_1:81;
verum end;
hence
ex
N being
Element of
NAT st
for
n being
Element of
NAT st
n >= N holds
n / 2
> (log (2,n)) * (log (2,n))
;
verum
end;
then consider N3 being Element of NAT such that
A11:
for n being Element of NAT st n >= N3 holds
n / 2 > (log (2,n)) * (log (2,n))
;
now ex N being Element of NAT st
for n being Element of NAT st n >= N holds
n / 3 > 2 * (log (2,n))take N = 30;
for n being Element of NAT st n >= N holds
n / 3 > 2 * (log (2,n))let n be
Element of
NAT ;
( n >= N implies n / 3 > 2 * (log (2,n)) )assume A12:
n >= N
;
n / 3 > 2 * (log (2,n))then A13:
n to_power 6
> 0
by POWER:34;
2
to_power n > n to_power 6
by A12, Lm30;
then
log (2,
(2 to_power n))
> log (2,
(n to_power 6))
by A13, POWER:57;
then
n * (log (2,2)) > log (2,
(n to_power 6))
by POWER:55;
then
n * 1
> log (2,
(n to_power 6))
by POWER:52;
then
n > (3 * 2) * (log (2,n))
by A12, POWER:55;
then
n > 3
* (2 * (log (2,n)))
;
hence
n / 3
> 2
* (log (2,n))
by XREAL_1:81;
verum end;
then consider N2 being Element of NAT such that
A14:
for n being Element of NAT st n >= N2 holds
n / 3 > 2 * (log (2,n))
;
then consider N1 being Element of NAT such that
A15:
for n being Element of NAT st n >= N1 holds
n / 6 > 1
;
set N = max ((max (N1,2)),(max (N2,N3)));
A16:
max ((max (N1,2)),(max (N2,N3))) >= max (N1,2)
by XXREAL_0:25;
max (N1,2) >= 2
by XXREAL_0:25;
then A17:
max ((max (N1,2)),(max (N2,N3))) >= 2
by A16, XXREAL_0:2;
A18:
max ((max (N1,2)),(max (N2,N3))) >= max (N2,N3)
by XXREAL_0:25;
max (N2,N3) >= N3
by XXREAL_0:25;
then A19:
max ((max (N1,2)),(max (N2,N3))) >= N3
by A18, XXREAL_0:2;
max (N2,N3) >= N2
by XXREAL_0:25;
then A20:
max ((max (N1,2)),(max (N2,N3))) >= N2
by A18, XXREAL_0:2;
max (N1,2) >= N1
by XXREAL_0:25;
then A21:
max ((max (N1,2)),(max (N2,N3))) >= N1
by A16, XXREAL_0:2;
now for n being Element of NAT st n >= max ((max (N1,2)),(max (N2,N3))) holds
(sqrt n) - (log (2,n)) > 1let n be
Element of
NAT ;
( n >= max ((max (N1,2)),(max (N2,N3))) implies (sqrt n) - (log (2,n)) > 1 )A22:
(1 + (2 * (log (2,n)))) + ((log (2,n)) * (log (2,n))) = (1 + (log (2,n))) ^2
;
assume A23:
n >= max (
(max (N1,2)),
(max (N2,N3)))
;
(sqrt n) - (log (2,n)) > 1then
n >= N2
by A20, XXREAL_0:2;
then A24:
n / 3
> 2
* (log (2,n))
by A14;
n >= 2
by A17, A23, XXREAL_0:2;
then
log (2,
n)
>= log (2,2)
by PRE_FF:10;
then A25:
log (2,
n)
>= 1
by POWER:52;
n >= N1
by A21, A23, XXREAL_0:2;
then
n / 6
> 1
by A15;
then A26:
(n / 6) + (n / 3) > 1
+ (2 * (log (2,n)))
by A24, XREAL_1:8;
n >= N3
by A19, A23, XXREAL_0:2;
then A27:
n / 2
> (log (2,n)) * (log (2,n))
by A11;
((n / 6) + (n / 3)) + (n / 2) = n
;
then
n > (1 + (log (2,n))) ^2
by A26, A27, A22, XREAL_1:8;
then
sqrt n > sqrt ((1 + (log (2,n))) ^2)
by SQUARE_1:27, XREAL_1:63;
then
sqrt n > 1
+ (log (2,n))
by A25, SQUARE_1:22;
hence
(sqrt n) - (log (2,n)) > 1
by XREAL_1:20;
verum end;
hence
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
(sqrt n) - (log (2,n)) > 1
; verum