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 4 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not g . b₁ <= 0 )
let n be Nat; :: thesis: ( not 1 <= n or not g . n <= 0 )
A3: n in NAT by ORDINAL1:def 12;
assume A4: n >= 1 ; :: thesis: not g . n <= 0
then g . n = n to_power n by A1, A3;
hence not g . n <= 0 by A4, POWER:34; :: thesis: verum

end;

set h = (seq_n! 1) /" g;
reconsider g = g as eventually-positive Real_Sequence by A2;
deffunc H₁( Nat) -> Element of REAL = (((seq_n! 1) /" g) . $1) / (((seq_n! 1) /" g) . ($1 + 1));
consider p being Real_Sequence such that
A5: for n being Nat holds p . n = H₁(n) from SEQ_1:sch 1();
defpred S₁[ Nat] means p . $1 > 2;
A6: 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 A7: n > 0 ; :: thesis: p . n = ((n + 1) / (n + 2)) * (((n + 1) / n) to_power n)
A8: (n + 1) ! > 0 by NEWTON:17;
p . n = (((seq_n! 1) /" g) . n) / (((seq_n! 1) /" g) . (n + 1)) by A5
.= (((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 Def4
.= (((n + 1) !) / (n to_power n)) / (((seq_n! 1) /" g) . (n + 1)) by A1, A7
.= (((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 Def4
.= (((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:15
.= ((1 / ((n + 1) + 1)) * (((n + 1) !) / ((n + 1) !))) * (((n + 1) to_power (n + 1)) / (n to_power n)) by XCMPLX_1:103
.= ((1 / ((n + 1) + 1)) * 1) * (((n + 1) to_power (n + 1)) / (n to_power n)) by A8, XCMPLX_1:60
.= (1 / (n + 2)) * ((((n + 1) to_power n) * ((n + 1) to_power 1)) / (n to_power n)) by POWER:27
.= (1 / (n + 2)) * ((((n + 1) to_power n) * (n + 1)) / (n to_power n)) by POWER:25
.= (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 A7, POWER:31
.= ((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;

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

A15: now :: thesis: not (k + 1) * (k + 3) >= (k + 2) * (k + 2)

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:6; :: thesis: verum

end;

then (k + 1) * (k + 3) < 1 * ((k + 2) * (k + 2)) ;
then A16: ((k + 1) * (k + 3)) / ((k + 2) * (k + 2)) < 1 by XREAL_1:83;
(k + 1) * (k + 3) > 0 * (k + 3) by XREAL_1:68;
then A17: ((k + 1) * (k + 3)) * (((k + 2) * (k + 2)) ") > 0 * (((k + 2) * (k + 2)) ") by A15, XREAL_1:68;
k >= 1 by A10, XXREAL_0:2;
then ((k + 1) / k) to_power k <= 1 * (((k + 2) / (k + 1)) to_power (k + 1)) by A14, Lm42;
then (((k + 1) / k) to_power k) / (((k + 2) / (k + 1)) to_power (k + 1)) <= 1 by A12, XREAL_1:79;
then A18: (((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 A13, A17, A16, XREAL_1:98;
(k + 2) * ((k + 3) ") > 0 * ((k + 3) ") by XREAL_1:68;
then A19: ((k + 2) / (k + 3)) * (((k + 2) / (k + 1)) to_power (k + 1)) > ((k + 2) / (k + 3)) * 0 by A12, XREAL_1:68;
A20: p . (k + 1) = (((k + 1) + 1) / ((k + 1) + 2)) * (((k + (1 + 1)) / (k + 1)) to_power (k + 1)) by A6
.= ((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 A6, A10, A14
.= (((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:76
.= (((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:84 ;
then ((p . k) / (p . (k + 1))) * (p . (k + 1)) < 1 * (p . (k + 1)) by A20, A19, A18, XREAL_1:68;
then p . (k + 1) > p . k by A20, A19, XCMPLX_1:87;
hence S₁[k + 1] by A11, 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 )
A21: 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 )
A22: (n + 1) ! > 0 by NEWTON:17;
assume A23: n >= 1 ; :: thesis: ((seq_n! 1) /" g) . n > 0
then n to_power n > 0 by POWER:34;
then A24: ((n + 1) !) * (1 / (n to_power n)) > ((n + 1) !) * 0 by A22, XREAL_1:68;
((seq_n! 1) /" g) . n = ((seq_n! 1) . n) / (g . n) by Lm4
.= ((n + 1) !) / (g . n) by Def4
.= ((n + 1) !) / (n to_power n) by A1, A23 ;
hence ((seq_n! 1) /" g) . n > 0 by A24; :: thesis: verum

end;

p . 4 = ((4 + 1) / (4 + 2)) * (((4 + 1) / 4) to_power 4) by A6
.= (5 / 6) * ((5 to_power 4) / 256) by Lm37, POWER:31
.= (5 * (5 to_power 4)) / (6 * 256)
.= ((5 to_power 1) * (5 to_power 4)) / 1536 by POWER:25
.= (5 to_power (4 + 1)) / 1536 by POWER:27
.= 3125 / 1536 by Lm36 ;
then A25: S₁[4] ;
A26: for n being Nat st n >= 4 holds
S₁[n] from NAT_1:sch 8(A25, A9);
A27: 3 = 4 - 1 ;
A28: 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
A29: k >= 4 and
A30: ((seq_n! 1) /" g) . k < 1 / (k - 2) ; :: thesis: S₂[k + 1]
A31: k in NAT by ORDINAL1:def 12;
A32: ((seq_n! 1) /" g) . (k + 1) > 0 by A21, NAT_1:11;
p . k > 2 by A26, A29;
then (((seq_n! 1) /" g) . k) / (((seq_n! 1) /" g) . (k + 1)) > 2 by A5;
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 A32, XREAL_1:68;
then ((seq_n! 1) /" g) . k > 2 * (((seq_n! 1) /" g) . (k + 1)) by A32, XCMPLX_1:87;
then A33: (((seq_n! 1) /" g) . k) / 2 > ((seq_n! 1) /" g) . (k + 1) by XREAL_1:81;
A34: k - 1 >= 3 by A27, A29, XREAL_1:9;
k >= 3 by A29, XXREAL_0:2;
then 2 * (k - 2) >= k - 1 by A31, Lm35;
then A35: 1 / (2 * (k - 2)) <= 1 / (k - 1) by A34, XREAL_1:85;
(((seq_n! 1) /" g) . k) * (1 / 2) < (1 / (k - 2)) * (1 / 2) by A30, XREAL_1:68;
then (((seq_n! 1) /" g) . k) / 2 < 1 / (2 * (k - 2)) by XCMPLX_1:102;
then (((seq_n! 1) /" g) . k) / 2 < 1 / (k - 1) by A35, XXREAL_0:2;
hence S₂[k + 1] by A33, XXREAL_0:2; :: thesis: verum

end;

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

A38: now :: thesis: for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_n! 1) /" g) . n) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_n! 1) /" g) . n) - 0).| < p )
set N = [/((1 / p) + 4)\];
A39: [/((1 / p) + 4)\] >= (1 / p) + 4 by INT_1:def 7;
assume A40: p > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_n! 1) /" g) . n) - 0).| < p
then A41: 4 + (1 / p) > 4 by XREAL_1:29;
then A42: [/((1 / p) + 4)\] >= 4 by A39, XXREAL_0:2;
[/((1 / p) + 4)\] in NAT by A39, A41, INT_1:3;
then reconsider N = [/((1 / p) + 4)\] as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
|.((((seq_n! 1) /" g) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N implies |.((((seq_n! 1) /" g) . n) - 0).| < p )
A43: n in NAT by ORDINAL1:def 12;
assume A44: n >= N ; :: thesis: |.((((seq_n! 1) /" g) . n) - 0).| < p
then A45: n >= 4 by A42, XXREAL_0:2;
then n >= 1 by XXREAL_0:2;
then A46: ((seq_n! 1) /" g) . n > 0 by A21, A43;
A47: (1 / p) + 2 > 1 / p by XREAL_1:29;
n >= ((1 / p) + 2) + 2 by A39, A44, XXREAL_0:2;
then n - 2 >= (1 / p) + 2 by XREAL_1:19;
then n - 2 > 1 / p by A47, XXREAL_0:2;
then A48: 1 / (n - 2) < 1 / (1 / p) by A40, XREAL_1:88;
((seq_n! 1) /" g) . n < 1 / (n - 2) by A37, A45;
then ((seq_n! 1) /" g) . n < p by A48, XXREAL_0:2;
hence |.((((seq_n! 1) /" g) . n) - 0).| < p by A46, ABSVALUE:def 1; :: thesis: verum

end;

then A49: (seq_n! 1) /" g is convergent by SEQ_2:def 6;
then A50: lim ((seq_n! 1) /" g) = 0 by A38, SEQ_2:def 7;
then not g in Big_Oh (seq_n! 1) by A49, ASYMPT_0:16;
then A51: not seq_n! 1 in Big_Omega g by ASYMPT_0:19;
seq_n! 1 in Big_Oh g by A49, A50, 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 A51, Th4; :: thesis: verum