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:16;
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:39;
A10: [/((log 2,c) / ((log 2,b) - (log 2,a)))\] >= (log 2,c) / ((log 2,b) - (log 2,a)) by INT_1:def 5;
log 2,b > (log 2,a) + 0 by A1, POWER:65;
then A11: (log 2,b) - (log 2,a) > 0 by XREAL_1:22;
A12: N1 + 1 > N1 + 0 by XREAL_1:10;
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:70;
then (N1 + 1) * ((log 2,b) - (log 2,a)) > log 2,c by A11, XCMPLX_1:88;
then 2 to_power ((N1 + 1) * ((log 2,b) - (log 2,a))) > 2 to_power (log 2,c) by POWER:44;
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:34;
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:70;
then 2 to_power ((N1 + 1) * (log 2,b)) > c * (2 to_power ((N1 + 1) * (log 2,a))) by A9, XCMPLX_1:88;
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;