let a, b be positive Real; :: thesis: ( a < b implies not seq_a^ (b,1,0) in Big_Oh (seq_a^ (a,1,0)) )
assume A1: a < b ; :: thesis: 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 :: thesis: verum

set d = (log (2,b)) - (log (2,a));
assume seq_a^ (b,1,0) in Big_Oh (seq_a^ (a,1,0)) ; :: thesis: contradiction
then 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; :: thesis: verum

end;