let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds f . n = ((3 * (10 to_power 6)) - ((18 * (10 to_power 3)) * n)) + (27 * (n ^2 )) ) implies f in Big_Oh (seq_n^ 2) )
assume A1: for n being Element of NAT holds f . n = ((3 * (10 to_power 6)) - ((18 * (10 to_power 3)) * n)) + (27 * (n ^2 )) ; :: thesis: f in Big_Oh (seq_n^ 2)
set g = seq_n^ 2;
A2: f is Element of Funcs NAT ,REAL by FUNCT_2:11;
consider t1 being Element of NAT such that
A3: t1 = (10 * 10) * 10 ;
consider t2 being Element of NAT such that
A4: t2 = t1 * t1 ;
t1 = 10 * (10 ^2 ) by A3;
then t1 = 10 * (10 to_power 2) by POWER:53;
then t1 = (10 to_power 1) * (10 to_power 2) by POWER:30;
then A5: t1 = 10 to_power (1 + 2) by POWER:32;
then A6: t2 = 10 to_power (3 + 3) by A4, POWER:32
.= 10 to_power 6 ;
A7: 10 to_power 3 = 10 to_power (2 + 1)
.= (10 to_power 2) * (10 to_power 1) by POWER:32
.= (10 to_power 2) * 10 by POWER:30
.= (10 ^2 ) * 10 by POWER:53
.= 1000 ;
A8: for n being Element of NAT st n >= 400 holds
f . n <= 27 * (n ^2 )

proof

let n be Element of NAT ; :: thesis: ( n >= 400 implies f . n <= 27 * (n ^2 ) )
assume A9: n >= 400 ; :: thesis: f . n <= 27 * (n ^2 )

now

assume f . n > 27 * (n ^2 ) ; :: thesis: contradiction
then ((3 * t2) - ((18 * (10 to_power 3)) * n)) + (27 * (n ^2 )) > 27 * (n ^2 ) by A1, A6;
then (3 * t2) + (- ((18 * t1) * n)) > (27 * (n ^2 )) - (27 * (n ^2 )) by A5, XREAL_1:21;
then (3 * t2) - ((18 * t1) * n) > 0 ;
then A10: 3 * t2 > 0 + ((18 * t1) * n) by XREAL_1:22;
(18 * t1) * n >= (18 * t1) * 400 by A9, XREAL_1:66;
then 3 * (10 to_power (3 + 3)) > t1 * 7200 by A6, A10, XXREAL_0:2;
then 3 * ((10 to_power 3) * (10 to_power 3)) > t1 * 7200 by POWER:32;
hence contradiction by A5, A7; :: thesis: verum

end;

hence f . n <= 27 * (n ^2 ) ; :: thesis: verum

end;

A11: for n being Element of NAT st n >= 400 holds
((18 * t1) * n) - (3 * t2) < 27 * (n ^2 )

proof

defpred S₁[ Nat] means ((18 * t1) * $1) - (3 * t2) < 27 * ($1 ^2 );
A12: S₁[400] by A4, A5, A7;
A13: for k being Nat st k >= 400 & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( k >= 400 & S₁[k] implies S₁[k + 1] )
assume that
A14: k >= 400 and
A15: ((18 * t1) * k) - (3 * t2) < 27 * (k ^2 ) ; :: thesis: S₁[k + 1]
((18 * t1) * (k + 1)) - (3 * t2) = (((18 * t1) * k) - (3 * t2)) + (18 * t1) ;
then A16: ((18 * t1) * (k + 1)) - (3 * t2) < (27 * (k ^2 )) + (18 * t1) by A15, XREAL_1:8;
54 * 400 <= 54 * k by A14, XREAL_1:66;
then A17: 18 * t1 < 54 * k by A5, A7, XXREAL_0:2;
(54 * k) + 0 <= (54 * k) + 27 by XREAL_1:9;
then 18 * t1 < (54 * k) + 27 by A17, XXREAL_0:2;
then (27 * (k ^2 )) + (18 * t1) < (27 * (k ^2 )) + ((54 * k) + 27) by XREAL_1:8;
hence S₁[k + 1] by A16, XXREAL_0:2; :: thesis: verum

end;

for n being Nat st n >= 400 holds
S₁[n] from NAT_1:sch 8(A12, A13);
hence for n being Element of NAT st n >= 400 holds
((18 * t1) * n) - (3 * t2) < 27 * (n ^2 ) ; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: ( n >= 400 implies ( f . n <= 27 * ((seq_n^ 2) . n) & f . n >= 0 ) )
assume A18: n >= 400 ; :: thesis: ( f . n <= 27 * ((seq_n^ 2) . n) & f . n >= 0 )
then f . n <= 27 * (n ^2 ) by A8;
then f . n <= 27 * (n to_power 2) by POWER:53;
hence f . n <= 27 * ((seq_n^ 2) . n) by A18, Def3; :: thesis: f . n >= 0
0 + (((18 * t1) * n) - (3 * t2)) < 27 * (n ^2 ) by A11, A18;
then 0 < (27 * (n ^2 )) - (((18 * t1) * n) - (3 * t2)) by XREAL_1:22;
then 0 < ((3 * (10 to_power 6)) - ((18 * t1) * n)) + (27 * (n ^2 )) by A6;
hence f . n >= 0 by A1, A5; :: thesis: verum

end;

hence f in Big_Oh (seq_n^ 2) by A2; :: thesis: verum