ex s being Real_Sequence st
( s . 0 = 0 & ( for n being Element of NAT st n > 0 holds
s . n = ((log (2,n)) ^2) + 36 ) )

proof

defpred S₁[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = ((log (2,$1)) ^2) + 36 ) );
A1: for x being Element of NAT ex y being Element of REAL st S₁[x,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[n,y]
( n = 0 or n > 0 ) ;
hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

consider h being Function of NAT,REAL such that
A2: for x being Element of NAT holds S₁[x,h . x] from FUNCT_2:sch 3(A1);
take h ; :: thesis: ( h . 0 = 0 & ( for n being Element of NAT st n > 0 holds
h . n = ((log (2,n)) ^2) + 36 ) )
thus ( h . 0 = 0 & ( for n being Element of NAT st n > 0 holds
h . n = ((log (2,n)) ^2) + 36 ) ) by A2; :: thesis: verum

end;

then consider q being Real_Sequence such that
A3: q . 0 = 0 and
A4: for n being Element of NAT st n > 0 holds
q . n = ((log (2,n)) ^2) + 36 ;
q is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not q . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not q . n <= 0 )
A5: ((log (2,n)) ^2) + 36 > 0 + 0 by XREAL_1:8, XREAL_1:63;
assume n >= 1 ; :: thesis: not q . n <= 0
hence not q . n <= 0 by A4, A5; :: thesis: verum

end;

then reconsider q = q as eventually-positive Real_Sequence ;
let f, g be Real_Sequence; :: thesis: ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 ) & ( for n being Element of NAT st n > 0 holds
g . n = (n to_power 3) * (log (2,n)) ) implies ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = g & s in Big_Oh s1 ) )
assume that
A6: f . 0 = 0 and
A7: for n being Element of NAT st n > 0 holds
f . n = ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 and
A8: for n being Element of NAT st n > 0 holds
g . n = (n to_power 3) * (log (2,n)) ; :: thesis: ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = g & s in Big_Oh s1 )
A9: g is eventually-positive

proof

take 2 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being Element of NAT holds
( not 2 <= b₁ or not g . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 2 <= n or not g . n <= 0 )
assume A10: n >= 2 ; :: thesis: not g . n <= 0
then log (2,n) >= log (2,2) by PRE_FF:10;
then A11: log (2,n) >= 1 by POWER:52;
n to_power 3 > 0 by A10, POWER:34;
then (n to_power 3) * (log (2,n)) > (n to_power 3) * 0 by A11, XREAL_1:68;
hence not g . n <= 0 by A8, A10; :: thesis: verum

end;

4 = 2 ^2
.= 2 to_power 2 by POWER:46 ;
then A12: log (2,4) = 2 * (log (2,2)) by POWER:55
.= 2 * 1 by POWER:52
.= 2 ;
A13: for n being Element of NAT st n >= 4 holds
7 * (n ^2) > q . n

proof

defpred S₁[ Nat] means 7 * ($1 ^2) > q . $1;
A14: for k being Nat st k >= 4 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 4 & S₁[k] implies S₁[k + 1] )
assume that
A15: k >= 4 and
A16: 7 * (k ^2) > q . k ; :: thesis: S₁[k + 1]
A17: q . (k + 1) = ((log (2,(k + 1))) ^2) + 36 by A4;
k >= 2 by A15, XXREAL_0:2;
then A18: 2 to_power k > k + 1 by Lm1;
k + 1 > k + 0 by XREAL_1:8;
then 2 to_power k > k by A18, XXREAL_0:2;
then log (2,(2 to_power k)) > log (2,k) by A15, POWER:57;
then k * (log (2,2)) > log (2,k) by POWER:55;
then A19: k * 1 > log (2,k) by POWER:52;
log (2,k) >= 2 by A12, A15, PRE_FF:10;
then 14 * k > 2 * (log (2,k)) by A19, XREAL_1:98;
then ((7 * 2) * k) + 7 > (2 * (log (2,k))) + 1 by XREAL_1:8;
then A20: ((log (2,k)) ^2) + ((2 * (log (2,k))) + 1) < ((log (2,k)) ^2) + ((7 * (2 * k)) + 7) by XREAL_1:6;
log (2,(k + k)) = log (2,(2 * k)) ;
then log (2,(k + k)) = (log (2,k)) + (log (2,2)) by A15, POWER:53;
then (log (2,(k + k))) ^2 = ((log (2,k)) + 1) ^2 by POWER:52
.= (((log (2,k)) ^2) + (2 * (log (2,k)))) + 1 ;
then A21: ((log (2,(k + k))) ^2) + 36 < (((log (2,k)) ^2) + ((7 * (2 * k)) + 7)) + 36 by A20, XREAL_1:6;
k >= 1 by A15, XXREAL_0:2;
then k + k >= k + 1 by XREAL_1:6;
then A22: log (2,(k + k)) >= log (2,(k + 1)) by PRE_FF:10;
k + 1 >= 4 + 0 by A15, XREAL_1:8;
then log (2,(k + 1)) >= 2 by A12, PRE_FF:10;
then (log (2,(k + k))) ^2 >= (log (2,(k + 1))) ^2 by A22, SQUARE_1:15;
then A23: q . (k + 1) <= ((log (2,(k + k))) ^2) + 36 by A17, XREAL_1:6;
7 * ((k + 1) ^2) = (7 * (k ^2)) + ((7 * (2 * k)) + (7 * 1)) ;
then A24: 7 * ((k + 1) ^2) > (q . k) + ((7 * (2 * k)) + (7 * 1)) by A16, XREAL_1:6;
k in NAT by ORDINAL1:def 12;
then q . k = ((log (2,k)) ^2) + 36 by A4, A15;
then (q . k) + ((7 * (2 * k)) + (7 * 1)) > q . (k + 1) by A23, A21, XXREAL_0:2;
hence S₁[k + 1] by A24, XXREAL_0:2; :: thesis: verum

end;

q . 4 = (2 ^2) + 36 by A4, A12
.= 40 ;
then A25: S₁[4] ;
for n being Nat st n >= 4 holds
S₁[n] from NAT_1:sch 8(A25, A14);
hence for n being Element of NAT st n >= 4 holds
7 * (n ^2) > q . n ; :: thesis: verum

end;

reconsider g = g as eventually-positive Real_Sequence by A9;
f is eventually-positive

proof

log (2,3) > log (2,2) by POWER:57;
then A26: log (2,3) > 1 by POWER:52;
take 3 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being Element of NAT holds
( not 3 <= b₁ or not f . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 3 <= n or not f . n <= 0 )
assume A27: n >= 3 ; :: thesis: not f . n <= 0
then A28: n to_power 2 > 0 by POWER:34;
n > 1 by A27, XXREAL_0:2;
then A29: n to_power 3 > n to_power 2 by POWER:39;
log (2,n) >= log (2,3) by A27, PRE_FF:10;
then log (2,n) > 1 by A26, XXREAL_0:2;
then (n to_power 3) * (log (2,n)) > (n to_power 2) * 1 by A29, A28, XREAL_1:98;
then 12 * ((n to_power 3) * (log (2,n))) > 5 * (n to_power 2) by A28, XREAL_1:98;
then (12 * (n to_power 3)) * (log (2,n)) > (5 * (n ^2)) + 0 by POWER:46;
then ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) > 0 by XREAL_1:20;
then (((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2) > 0 + 0 by XREAL_1:8, XREAL_1:63;
then ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 > 0 + 0 ;
hence not f . n <= 0 by A7, A27; :: thesis: verum

end;

then reconsider f = f as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = f & s1 = g & f in Big_Oh s1 )
take g ; :: thesis: ( f = f & g = g & f in Big_Oh g )
ex s being Real_Sequence st
( s . 0 = 0 & ( for n being Element of NAT st n > 0 holds
s . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) ) )

proof

defpred S₁[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = ((12 * ($1 to_power 3)) * (log (2,$1))) - (5 * ($1 ^2)) ) );
A30: for x being Element of NAT ex y being Element of REAL st S₁[x,y]

proof

let n be Element of NAT ; :: thesis: ex y being Element of REAL st S₁[n,y]
( n = 0 or n > 0 ) ;
hence ex y being Element of REAL st S₁[n,y] ; :: thesis: verum

end;

consider h being Function of NAT,REAL such that
A31: for x being Element of NAT holds S₁[x,h . x] from FUNCT_2:sch 3(A30);
take h ; :: thesis: ( h . 0 = 0 & ( for n being Element of NAT st n > 0 holds
h . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) ) )
thus h . 0 = 0 by A31; :: thesis: for n being Element of NAT st n > 0 holds
h . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) )
thus ( n > 0 implies h . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) ) by A31; :: thesis: verum

end;

then consider p being Real_Sequence such that
A32: p . 0 = 0 and
A33: for n being Element of NAT st n > 0 holds
p . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) ;
p is eventually-positive

proof

log (2,3) > log (2,2) by POWER:57;
then A34: log (2,3) > 1 by POWER:52;
take 3 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being Element of NAT holds
( not 3 <= b₁ or not p . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 3 <= n or not p . n <= 0 )
assume A35: n >= 3 ; :: thesis: not p . n <= 0
then A36: n to_power 2 > 0 by POWER:34;
n > 1 by A35, XXREAL_0:2;
then A37: n to_power 3 > n to_power 2 by POWER:39;
log (2,n) >= log (2,3) by A35, PRE_FF:10;
then log (2,n) > 1 by A34, XXREAL_0:2;
then (n to_power 3) * (log (2,n)) > (n to_power 2) * 1 by A37, A36, XREAL_1:98;
then 12 * ((n to_power 3) * (log (2,n))) > 5 * (n to_power 2) by A36, XREAL_1:98;
then (12 * (n to_power 3)) * (log (2,n)) > (5 * (n ^2)) + 0 by POWER:46;
then ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) > 0 by XREAL_1:20;
hence not p . n <= 0 by A33, A35; :: thesis: verum

end;

then reconsider p = p as eventually-positive Real_Sequence ;
set t = max (p,q);
consider N being Element of NAT such that
A38: for n being Element of NAT st n >= N holds
(max (p,q)) . n > 0 by ASYMPT_0:def 4;
A39: for n being Element of NAT st n >= 4 holds
p . n > 7 * (n ^2)

proof

let n be Element of NAT ; :: thesis: ( n >= 4 implies p . n > 7 * (n ^2) )
assume A40: n >= 4 ; :: thesis: p . n > 7 * (n ^2)
then n > 1 by XXREAL_0:2;
then A41: n to_power 3 > n to_power 2 by POWER:39;
log (2,n) >= log (2,4) by A40, PRE_FF:10;
then A42: log (2,n) > 1 by A12, XXREAL_0:2;
n to_power 2 > 0 by A40, POWER:34;
then (n to_power 3) * (log (2,n)) > (n to_power 2) * 1 by A41, A42, XREAL_1:98;
then 12 * ((n to_power 3) * (log (2,n))) > 12 * (n to_power 2) by XREAL_1:68;
then A43: (12 * (n to_power 3)) * (log (2,n)) > 12 * (n ^2) by POWER:46;
p . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) by A33, A40;
then p . n > (12 * (n ^2)) - (5 * (n ^2)) by A43, XREAL_1:9;
hence p . n > 7 * (n ^2) ; :: thesis: verum

end;

A44: for n being Element of NAT st n >= 4 holds
p . n > q . n

proof

let n be Element of NAT ; :: thesis: ( n >= 4 implies p . n > q . n )
assume A45: n >= 4 ; :: thesis: p . n > q . n
then A46: 7 * (n ^2) > q . n by A13;
p . n > 7 * (n ^2) by A39, A45;
hence p . n > q . n by A46, XXREAL_0:2; :: thesis: verum

end;

A47: for n being Element of NAT st n >= 4 holds
(max (p,q)) . n = p . n

proof

let n be Element of NAT ; :: thesis: ( n >= 4 implies (max (p,q)) . n = p . n )
assume n >= 4 ; :: thesis: (max (p,q)) . n = p . n
then A48: p . n > q . n by A44;
thus (max (p,q)) . n = max ((p . n),(q . n)) by ASYMPT_0:def 7
.= p . n by A48, XXREAL_0:def 10 ; :: thesis: verum

end;

A49: now

let n be Element of NAT ; :: thesis: ( n >= max (4,N) implies ( (max (p,q)) . n <= 12 * (g . n) & (max (p,q)) . n >= 0 ) )
assume A50: n >= max (4,N) ; :: thesis: ( (max (p,q)) . n <= 12 * (g . n) & (max (p,q)) . n >= 0 )
A51: max (4,N) >= 4 by XXREAL_0:25;
then (max (p,q)) . n = p . n by A47, A50, XXREAL_0:2
.= ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) by A33, A50, A51 ;
then (max (p,q)) . n <= ((12 * (n to_power 3)) * (log (2,n))) - 0 by XREAL_1:13;
then (max (p,q)) . n <= 12 * ((n to_power 3) * (log (2,n))) ;
hence (max (p,q)) . n <= 12 * (g . n) by A8, A50, A51; :: thesis: (max (p,q)) . n >= 0
max (4,N) >= N by XXREAL_0:25;
then n >= N by A50, XXREAL_0:2;
hence (max (p,q)) . n >= 0 by A38; :: thesis: verum

end;

max (p,q) is Element of Funcs (NAT,REAL) by FUNCT_2:8;
then A52: max (p,q) in Big_Oh g by A49;
for n being Element of NAT holds f . n = (p . n) + (q . n)

proof

let n be Element of NAT ; :: thesis: f . n = (p . n) + (q . n)
thus f . n = (p . n) + (q . n) :: thesis: verum

proof

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: f . n = (p . n) + (q . n)

hence f . n = (p . n) + (q . n) by A6, A32, A3; :: thesis: verum

end;

suppose A53: n > 0 ; :: thesis: f . n = (p . n) + (q . n)

then p . n = ((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2)) by A33;
then (p . n) + (q . n) = (((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + (((log (2,n)) ^2) + 36) by A4, A53
.= ((((12 * (n to_power 3)) * (log (2,n))) - (5 * (n ^2))) + ((log (2,n)) ^2)) + 36 ;
hence f . n = (p . n) + (q . n) by A7, A53; :: thesis: verum

end;

end;

end;

end;

then A54: Big_Oh f = Big_Oh (p + q) by SEQ_1:7
.= Big_Oh (max (p,q)) by ASYMPT_0:9 ;
f in Big_Oh f by ASYMPT_0:10;
hence ( f = f & g = g & f in Big_Oh g ) by A54, A52, ASYMPT_0:12; :: thesis: verum