let a, b be positive Real; ( a < b implies not seq_a^ (b,1,0) in Big_Oh (seq_a^ (a,1,0)) )
assume A1:
a < b
; not seq_a^ (b,1,0) in Big_Oh (seq_a^ (a,1,0))
set g = seq_a^ (a,1,0);
set f = seq_a^ (b,1,0);
hereby verum
set d =
(log (2,b)) - (log (2,a));
assume
seq_a^ (
b,1,
0)
in Big_Oh (seq_a^ (a,1,0))
;
contradictionthen consider s being
Element of
Funcs (
NAT,
REAL)
such that A2:
s = seq_a^ (
b,1,
0)
and A3:
ex
c being
Real ex
N being
Element of
NAT st
(
c > 0 & ( for
n being
Element of
NAT st
n >= N holds
(
s . n <= c * ((seq_a^ (a,1,0)) . n) &
s . n >= 0 ) ) )
;
consider c being
Real,
N being
Element of
NAT such that A4:
c > 0
and A5:
for
n being
Element of
NAT st
n >= N holds
(
s . n <= c * ((seq_a^ (a,1,0)) . n) &
s . n >= 0 )
by A3;
set N0 =
[/((log (2,c)) / ((log (2,b)) - (log (2,a))))\];
set N1 =
max (
N,
[/((log (2,c)) / ((log (2,b)) - (log (2,a))))\]);
A6:
max (
N,
[/((log (2,c)) / ((log (2,b)) - (log (2,a))))\])
>= N
by XXREAL_0:25;
A7:
(
max (
N,
[/((log (2,c)) / ((log (2,b)) - (log (2,a))))\])
= N or
max (
N,
[/((log (2,c)) / ((log (2,b)) - (log (2,a))))\])
= [/((log (2,c)) / ((log (2,b)) - (log (2,a))))\] )
by XXREAL_0:16;
A8:
max (
N,
[/((log (2,c)) / ((log (2,b)) - (log (2,a))))\])
>= [/((log (2,c)) / ((log (2,b)) - (log (2,a))))\]
by XXREAL_0:25;
reconsider N1 =
max (
N,
[/((log (2,c)) / ((log (2,b)) - (log (2,a))))\]) as
Element of
NAT by A6, A7, INT_1:3;
set n =
N1 + 1;
set e = 2
to_power ((N1 + 1) * (log (2,a)));
A9:
2
to_power ((N1 + 1) * (log (2,a))) > 0
by POWER:34;
A10:
[/((log (2,c)) / ((log (2,b)) - (log (2,a))))\] >= (log (2,c)) / ((log (2,b)) - (log (2,a)))
by INT_1:def 7;
log (2,
b)
> (log (2,a)) + 0
by A1, POWER:57;
then A11:
(log (2,b)) - (log (2,a)) > 0
by XREAL_1:20;
A12:
N1 + 1
> N1 + 0
by XREAL_1:8;
then
N1 + 1
> [/((log (2,c)) / ((log (2,b)) - (log (2,a))))\]
by A8, XXREAL_0:2;
then
N1 + 1
> (log (2,c)) / ((log (2,b)) - (log (2,a)))
by A10, XXREAL_0:2;
then
(N1 + 1) * ((log (2,b)) - (log (2,a))) > ((log (2,c)) / ((log (2,b)) - (log (2,a)))) * ((log (2,b)) - (log (2,a)))
by A11, XREAL_1:68;
then
(N1 + 1) * ((log (2,b)) - (log (2,a))) > log (2,
c)
by A11, XCMPLX_1:87;
then
2
to_power ((N1 + 1) * ((log (2,b)) - (log (2,a)))) > 2
to_power (log (2,c))
by POWER:39;
then
2
to_power (((N1 + 1) * (log (2,b))) - ((N1 + 1) * (log (2,a)))) > c
by A4, POWER:def 3;
then
(2 to_power ((N1 + 1) * (log (2,b)))) / (2 to_power ((N1 + 1) * (log (2,a)))) > c
by POWER:29;
then
((2 to_power ((N1 + 1) * (log (2,b)))) / (2 to_power ((N1 + 1) * (log (2,a))))) * (2 to_power ((N1 + 1) * (log (2,a)))) > c * (2 to_power ((N1 + 1) * (log (2,a))))
by A9, XREAL_1:68;
then
2
to_power ((N1 + 1) * (log (2,b))) > c * (2 to_power ((N1 + 1) * (log (2,a))))
by A9, XCMPLX_1:87;
then
b to_power (N1 + 1) > c * (2 to_power ((N1 + 1) * (log (2,a))))
by Lm3;
then A13:
b to_power (N1 + 1) > c * (a to_power (N1 + 1))
by Lm3;
N1 + 1
> N
by A6, A12, XXREAL_0:2;
then
(seq_a^ (b,1,0)) . (N1 + 1) <= c * ((seq_a^ (a,1,0)) . (N1 + 1))
by A2, A5;
then
b to_power ((1 * (N1 + 1)) + 0) <= c * ((seq_a^ (a,1,0)) . (N1 + 1))
by Def1;
hence
contradiction
by A13, Def1;
verum
end;