set f = seq_n! 1;
let g be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n > 0 holds
g . n = n to_power n ) implies ex s being eventually-positive Real_Sequence st
( s = g & Big_Oh (seq_n! 1) c= Big_Oh s & not Big_Oh (seq_n! 1) = Big_Oh s ) )
assume A1: for n being Element of NAT st n > 0 holds
g . n = n to_power n ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = g & Big_Oh (seq_n! 1) c= Big_Oh s & not Big_Oh (seq_n! 1) = Big_Oh s )
A2: g is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 6 :: thesis: for b₁ being Element of NAT holds
( not 1 <= b₁ or not g . b₁ <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not g . n <= 0 )
assume A3: n >= 1 ; :: thesis: not g . n <= 0
then g . n = n to_power n by A1;
hence not g . n <= 0 by A3, POWER:39; :: thesis: verum

end;

set h = (seq_n! 1) /" g;
reconsider g = g as eventually-positive Real_Sequence by A2;
deffunc H₁( Element of NAT ) -> Element of REAL = (((seq_n! 1) /" g) . $1) / (((seq_n! 1) /" g) . ($1 + 1));
consider p being Real_Sequence such that
A4: for n being Element of NAT holds p . n = H₁(n) from SEQ_1:sch 1();
defpred S₁[ Nat] means p . $1 > 2;
A5: for n being Element of NAT st n > 0 holds
p . n = ((n + 1) / (n + 2)) * (((n + 1) / n) to_power n)

proof

let n be Element of NAT ; :: thesis: ( n > 0 implies p . n = ((n + 1) / (n + 2)) * (((n + 1) / n) to_power n) )
assume A6: n > 0 ; :: thesis: p . n = ((n + 1) / (n + 2)) * (((n + 1) / n) to_power n)
A7: (n + 1) ! > 0 by NEWTON:23;
p . n = (((seq_n! 1) /" g) . n) / (((seq_n! 1) /" g) . (n + 1)) by A4
.= (((seq_n! 1) . n) / (g . n)) / (((seq_n! 1) /" g) . (n + 1)) by Lm4
.= (((n + 1) ! ) / (g . n)) / (((seq_n! 1) /" g) . (n + 1)) by Def5
.= (((n + 1) ! ) / (n to_power n)) / (((seq_n! 1) /" g) . (n + 1)) by A1, A6
.= (((n + 1) ! ) / (n to_power n)) / (((seq_n! 1) . (n + 1)) / (g . (n + 1))) by Lm4
.= (((n + 1) ! ) / (n to_power n)) / ((((n + 1) + 1) ! ) / (g . (n + 1))) by Def5
.= (((n + 1) ! ) / (n to_power n)) / ((((n + 1) + 1) ! ) / ((n + 1) to_power (n + 1))) by A1
.= (((n + 1) ! ) / (((n + 1) + 1) ! )) * (((n + 1) to_power (n + 1)) / (n to_power n)) by Lm38
.= (((n + 1) ! ) / (((n + 1) + 1) * ((n + 1) ! ))) * (((n + 1) to_power (n + 1)) / (n to_power n)) by NEWTON:21
.= ((1 / ((n + 1) + 1)) * (((n + 1) ! ) / ((n + 1) ! ))) * (((n + 1) to_power (n + 1)) / (n to_power n)) by XCMPLX_1:104
.= ((1 / ((n + 1) + 1)) * 1) * (((n + 1) to_power (n + 1)) / (n to_power n)) by A7, XCMPLX_1:60
.= (1 / (n + 2)) * ((((n + 1) to_power n) * ((n + 1) to_power 1)) / (n to_power n)) by POWER:32
.= (1 / (n + 2)) * ((((n + 1) to_power n) * (n + 1)) / (n to_power n)) by POWER:30
.= (1 / (n + 2)) * ((((n + 1) to_power n) * (n + 1)) * ((n to_power n) " ))
.= (1 / (n + 2)) * ((((n + 1) to_power n) * ((n to_power n) " )) * (n + 1))
.= (1 / (n + 2)) * ((((n + 1) to_power n) / (n to_power n)) * (n + 1))
.= (1 / (n + 2)) * ((((n + 1) / n) to_power n) * (n + 1)) by A6, POWER:36
.= ((n + 1) * (1 / (n + 2))) * (((n + 1) / n) to_power n)
.= ((n + 1) / (n + 2)) * (((n + 1) / n) to_power n) ;
hence p . n = ((n + 1) / (n + 2)) * (((n + 1) / n) to_power n) ; :: thesis: verum

end;

A8: 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
A9: k >= 4 and
A10: p . k > 2 ; :: thesis: S₁[k + 1]
(k + 2) * ((k + 1) " ) > 0 * ((k + 1) " ) by XREAL_1:70;
then A11: ((k + 2) / (k + 1)) to_power (k + 1) > 0 by POWER:39;
(k + 1) * (k " ) > 0 * (k " ) by A9, XREAL_1:70;
then ((k + 1) / k) to_power k > 0 by POWER:39;
then A12: (((k + 1) / k) to_power k) * ((((k + 2) / (k + 1)) to_power (k + 1)) " ) > 0 * ((((k + 2) / (k + 1)) to_power (k + 1)) " ) by A11, XREAL_1:70;
A13: k in NAT by ORDINAL1:def 13;

A14: now

assume (k + 1) * (k + 3) >= (k + 2) * (k + 2) ; :: thesis: contradiction
then ((k * k) + (4 * k)) + 3 >= ((k * k) + (2 * (2 * k))) + (2 ^2 ) ;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then (k + 1) * (k + 3) < 1 * ((k + 2) * (k + 2)) ;
then A15: ((k + 1) * (k + 3)) / ((k + 2) * (k + 2)) < 1 by XREAL_1:85;
(k + 1) * (k + 3) > 0 * (k + 3) by XREAL_1:70;
then A16: ((k + 1) * (k + 3)) * (((k + 2) * (k + 2)) " ) > 0 * (((k + 2) * (k + 2)) " ) by A14, XREAL_1:70;
k >= 1 by A9, XXREAL_0:2;
then ((k + 1) / k) to_power k <= 1 * (((k + 2) / (k + 1)) to_power (k + 1)) by A13, Lm42;
then (((k + 1) / k) to_power k) / (((k + 2) / (k + 1)) to_power (k + 1)) <= 1 by A11, XREAL_1:81;
then A17: (((k + 1) * (k + 3)) / ((k + 2) * (k + 2))) * ((((k + 1) / k) to_power k) / (((k + 2) / (k + 1)) to_power (k + 1))) < 1 * 1 by A12, A16, A15, XREAL_1:100;
(k + 2) * ((k + 3) " ) > 0 * ((k + 3) " ) by XREAL_1:70;
then A18: ((k + 2) / (k + 3)) * (((k + 2) / (k + 1)) to_power (k + 1)) > ((k + 2) / (k + 3)) * 0 by A11, XREAL_1:70;
A19: p . (k + 1) = (((k + 1) + 1) / ((k + 1) + 2)) * (((k + (1 + 1)) / (k + 1)) to_power (k + 1)) by A5
.= ((k + 2) / (k + 3)) * (((k + 2) / (k + 1)) to_power (k + 1)) ;
then (p . k) / (p . (k + 1)) = (((k + 1) / (k + 2)) * (((k + 1) / k) to_power k)) / (((k + 2) / (k + 3)) * (((k + 2) / (k + 1)) to_power (k + 1))) by A5, A9, A13
.= (((k + 1) / (k + 2)) / ((k + 2) / (k + 3))) * ((((k + 1) / k) to_power k) / (((k + 2) / (k + 1)) to_power (k + 1))) by XCMPLX_1:77
.= (((k + 1) * (k + 3)) / ((k + 2) * (k + 2))) * ((((k + 1) / k) to_power k) / (((k + 2) / (k + 1)) to_power (k + 1))) by XCMPLX_1:85 ;
then ((p . k) / (p . (k + 1))) * (p . (k + 1)) < 1 * (p . (k + 1)) by A19, A18, A17, XREAL_1:70;
then p . (k + 1) > p . k by A19, A18, XCMPLX_1:88;
hence S₁[k + 1] by A10, XXREAL_0:2; :: thesis: verum

end;

defpred S₂[ Nat] means ((seq_n! 1) /" g) . $1 < 1 / ($1 - 2);
take g ; :: thesis: ( g = g & Big_Oh (seq_n! 1) c= Big_Oh g & not Big_Oh (seq_n! 1) = Big_Oh g )
A20: for n being Element of NAT st n >= 1 holds
((seq_n! 1) /" g) . n > 0

proof

let n be Element of NAT ; :: thesis: ( n >= 1 implies ((seq_n! 1) /" g) . n > 0 )
A21: (n + 1) ! > 0 by NEWTON:23;
assume A22: n >= 1 ; :: thesis: ((seq_n! 1) /" g) . n > 0
then n to_power n > 0 by POWER:39;
then A23: ((n + 1) ! ) * (1 / (n to_power n)) > ((n + 1) ! ) * 0 by A21, XREAL_1:70;
((seq_n! 1) /" g) . n = ((seq_n! 1) . n) / (g . n) by Lm4
.= ((n + 1) ! ) / (g . n) by Def5
.= ((n + 1) ! ) / (n to_power n) by A1, A22 ;
hence ((seq_n! 1) /" g) . n > 0 by A23; :: thesis: verum

end;

p . 4 = ((4 + 1) / (4 + 2)) * (((4 + 1) / 4) to_power 4) by A5
.= (5 / 6) * ((5 to_power 4) / 256) by Lm37, POWER:36
.= (5 * (5 to_power 4)) / (6 * 256)
.= ((5 to_power 1) * (5 to_power 4)) / 1536 by POWER:30
.= (5 to_power (4 + 1)) / 1536 by POWER:32
.= 3125 / 1536 by Lm36 ;
then A24: S₁[4] ;
A25: for n being Nat st n >= 4 holds
S₁[n] from NAT_1:sch 8(A24, A8);
A26: 3 = 4 - 1 ;
A27: 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
A28: k >= 4 and
A29: ((seq_n! 1) /" g) . k < 1 / (k - 2) ; :: thesis: S₂[k + 1]
A30: k in NAT by ORDINAL1:def 13;
A31: ((seq_n! 1) /" g) . (k + 1) > 0 by A20, NAT_1:11;
p . k > 2 by A25, A28;
then (((seq_n! 1) /" g) . k) / (((seq_n! 1) /" g) . (k + 1)) > 2 by A4, A30;
then ((((seq_n! 1) /" g) . k) / (((seq_n! 1) /" g) . (k + 1))) * (((seq_n! 1) /" g) . (k + 1)) > 2 * (((seq_n! 1) /" g) . (k + 1)) by A31, XREAL_1:70;
then ((seq_n! 1) /" g) . k > 2 * (((seq_n! 1) /" g) . (k + 1)) by A31, XCMPLX_1:88;
then A32: (((seq_n! 1) /" g) . k) / 2 > ((seq_n! 1) /" g) . (k + 1) by XREAL_1:83;
A33: k - 1 >= 3 by A26, A28, XREAL_1:11;
k >= 3 by A28, XXREAL_0:2;
then 2 * (k - 2) >= k - 1 by A30, Lm35;
then A34: 1 / (2 * (k - 2)) <= 1 / (k - 1) by A33, XREAL_1:87;
(((seq_n! 1) /" g) . k) * (1 / 2) < (1 / (k - 2)) * (1 / 2) by A29, XREAL_1:70;
then (((seq_n! 1) /" g) . k) / 2 < 1 / (2 * (k - 2)) by XCMPLX_1:103;
then (((seq_n! 1) /" g) . k) / 2 < 1 / (k - 1) by A34, XXREAL_0:2;
hence S₂[k + 1] by A32, XXREAL_0:2; :: thesis: verum

end;

((seq_n! 1) /" g) . 4 = ((seq_n! 1) . 4) / (g . 4) by Lm4
.= ((4 + 1) ! ) / (g . 4) by Def5
.= 120 / 256 by A1, Lm33, Lm37 ;
then A35: S₂[4] ;
A36: for n being Nat st n >= 4 holds
S₂[n] from NAT_1:sch 8(A35, A27);

A37: now

let p be real number ; :: thesis: ( p > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((((seq_n! 1) /" g) . n) - 0 ) < p )
set N = [/((1 / p) + 4)\];
A38: [/((1 / p) + 4)\] >= (1 / p) + 4 by INT_1:def 5;
assume A39: p > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((((seq_n! 1) /" g) . n) - 0 ) < p
then A40: 4 + (1 / p) > 4 by XREAL_1:31;
then A41: [/((1 / p) + 4)\] >= 4 by A38, XXREAL_0:2;
reconsider N = [/((1 / p) + 4)\] as Element of NAT by A38, A40, INT_1:16;
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs ((((seq_n! 1) /" g) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N implies abs ((((seq_n! 1) /" g) . n) - 0 ) < p )
assume A42: n >= N ; :: thesis: abs ((((seq_n! 1) /" g) . n) - 0 ) < p
then A43: n >= 4 by A41, XXREAL_0:2;
then n >= 1 by XXREAL_0:2;
then A44: ((seq_n! 1) /" g) . n > 0 by A20;
A45: (1 / p) + 2 > 1 / p by XREAL_1:31;
n >= ((1 / p) + 2) + 2 by A38, A42, XXREAL_0:2;
then n - 2 >= (1 / p) + 2 by XREAL_1:21;
then n - 2 > 1 / p by A45, XXREAL_0:2;
then A46: 1 / (n - 2) < 1 / (1 / p) by A39, XREAL_1:90;
((seq_n! 1) /" g) . n < 1 / (n - 2) by A36, A43;
then ((seq_n! 1) /" g) . n < p by A46, XXREAL_0:2;
hence abs ((((seq_n! 1) /" g) . n) - 0 ) < p by A44, ABSVALUE:def 1; :: thesis: verum

end;

then A47: (seq_n! 1) /" g is convergent by SEQ_2:def 6;
then A48: lim ((seq_n! 1) /" g) = 0 by A37, SEQ_2:def 7;
then not g in Big_Oh (seq_n! 1) by A47, ASYMPT_0:16;
then A49: not seq_n! 1 in Big_Omega g by ASYMPT_0:19;
seq_n! 1 in Big_Oh g by A47, A48, ASYMPT_0:16;
hence ( g = g & Big_Oh (seq_n! 1) c= Big_Oh g & not Big_Oh (seq_n! 1) = Big_Oh g ) by A49, Th4; :: thesis: verum