let g be Real_Sequence; :: thesis: ( g . 0 = 0 & ( 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: ( g . 0 = 0 & ( 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 )
set f = seq_n! 1;
set h = (seq_n! 1) /" g;
g is eventually-positive
proof
take 1 ; :: according to ASYMPT_0:def 6 :: thesis: for b1 being Element of NAT holds
( not 1 <= b1 or not g . b1 <= 0 )
let n be Element of NAT ; :: thesis: ( not 1 <= n or not g . n <= 0 )
assume A2: n >= 1 ; :: thesis: not g . n <= 0
then g . n = n to_power n by A1;
hence not g . n <= 0 by A2, POWER:39; :: thesis: verum
end;
then reconsider g = g as eventually-positive Real_Sequence ;
take g ; :: thesis: ( g = g & Big_Oh (seq_n! 1) c= Big_Oh g & not Big_Oh (seq_n! 1) = Big_Oh g )
A3: 3 = 4 - 1 ;
A4: 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 )
assume A5: n >= 1 ; :: thesis: ((seq_n! 1) /" g) . n > 0
A6: ((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, A5 ;
n to_power n > 0 by A5, POWER:39;
then (n to_power n) " > 0 ;
then A7: 1 / (n to_power n) > 0 ;
(n + 1) ! > 0 by NEWTON:23;
then ((n + 1) ! ) * (1 / (n to_power n)) > ((n + 1) ! ) * 0 by A7, XREAL_1:70;
hence ((seq_n! 1) /" g) . n > 0 by A6; :: thesis: verum
end;
deffunc H1( Element of NAT ) -> Element of REAL = (((seq_n! 1) /" g) . $1) / (((seq_n! 1) /" g) . ($1 + 1));
consider p being Real_Sequence such that
A8: for n being Element of NAT holds p . n = H1(n) from SEQ_1:sch 1();
 A9: 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 A10: n > 0 ; :: thesis: p . n = ((n + 1) / (n + 2)) * (((n + 1) / n) to_power n)
A11: (n + 1) ! > 0 by NEWTON:23;
p . n = (((seq_n! 1) /" g) . n) / (((seq_n! 1) /" g) . (n + 1)) by A8
.= (((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, A10
.= (((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 Lm44
.= (((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 A11, 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 A10, 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;
defpred S1[ Nat] means p . $1 > 2;
A12: S1[4]
proof
p . 4 = ((4 + 1) / (4 + 2)) * (((4 + 1) / 4) to_power 4) by A9
.= (5 / 6) * ((5 to_power 4) / 256) by Lm43, 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 Lm42 ;
hence S1[4] ; :: thesis: verum
end;
A13: for k being Nat st k >= 4 & S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( k >= 4 & S1[k] implies S1[k + 1] )
assume that
A14: k >= 4 and
A15: p . k > 2 ; :: thesis: S1[k + 1]
A16: k in NAT by ORDINAL1:def 13;
A17: 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;
(k + 2) * ((k + 1) " ) > 0 * ((k + 1) " ) by XREAL_1:70;
then (k + 2) / (k + 1) > 0 ;
then A18: ((k + 2) / (k + 1)) to_power (k + 1) > 0 by POWER:39;
(k + 2) * ((k + 3) " ) > 0 * ((k + 3) " ) by XREAL_1:70;
then A19: (k + 2) / (k + 3) > 0 ;
A20: p . (k + 1) = (((k + 1) + 1) / ((k + 1) + 2)) * (((k + (1 + 1)) / (k + 1)) to_power (k + 1)) by A9
.= ((k + 2) / (k + 3)) * (((k + 2) / (k + 1)) to_power (k + 1)) ;
A21: ((k + 2) / (k + 3)) * (((k + 2) / (k + 1)) to_power (k + 1)) > ((k + 2) / (k + 3)) * 0 by A18, A19, XREAL_1:70;
A22: k >= 1 by A14, XXREAL_0:2;
k " > 0 by A14;
then (k + 1) * (k " ) > 0 * (k " ) by XREAL_1:70;
then (k + 1) / k > 0 ;
then A23: ((k + 1) / k) to_power k > 0 by POWER:39;
(((k + 2) / (k + 1)) to_power (k + 1)) " > 0 by A18;
then (((k + 1) / k) to_power k) * ((((k + 2) / (k + 1)) to_power (k + 1)) " ) > 0 * ((((k + 2) / (k + 1)) to_power (k + 1)) " ) by A23, XREAL_1:70;
then A24: (((k + 1) / k) to_power k) / (((k + 2) / (k + 1)) to_power (k + 1)) > 0 ;
A25: (k + 1) * (k + 3) > 0 * (k + 3) by XREAL_1:70;
((k + 2) * (k + 2)) " > 0 by A17;
then ((k + 1) * (k + 3)) * (((k + 2) * (k + 2)) " ) > 0 * (((k + 2) * (k + 2)) " ) by A25, XREAL_1:70;
then A26: ((k + 1) * (k + 3)) / ((k + 2) * (k + 2)) > 0 ;
A27: (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 A9, A14, A16, A20
.= (((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 ;
(k + 1) * (k + 3) < 1 * ((k + 2) * (k + 2)) by A17;
then A28: ((k + 1) * (k + 3)) / ((k + 2) * (k + 2)) < 1 by XREAL_1:85;
((k + 1) / k) to_power k <= 1 * (((k + 2) / (k + 1)) to_power (k + 1)) by A16, A22, Lm48;
then (((k + 1) / k) to_power k) / (((k + 2) / (k + 1)) to_power (k + 1)) <= 1 by A18, XREAL_1:81;
then (((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 A24, A26, A28, XREAL_1:100;
then ((p . k) / (p . (k + 1))) * (p . (k + 1)) < 1 * (p . (k + 1)) by A20, A21, A27, XREAL_1:70;
then p . (k + 1) > p . k by A20, A21, XCMPLX_1:88;
hence S1[k + 1] by A15, XXREAL_0:2; :: thesis: verum
end;
A29: for n being Nat st n >= 4 holds
S1[n] from NAT_1:sch 8(A12, A13);
 defpred S2[ Nat] means ((seq_n! 1) /" g) . $1 < 1 / ($1 - 2);
A30: S2[4]
proof
((seq_n! 1) /" g) . 4 = ((seq_n! 1) . 4) / (g . 4) by Lm4
.= ((4 + 1) ! ) / (g . 4) by Def5
.= 120 / 256 by A1, Lm39, Lm43 ;
hence S2[4] ; :: thesis: verum
end;
A31: for k being Nat st k >= 4 & S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( k >= 4 & S2[k] implies S2[k + 1] )
assume that
A32: k >= 4 and
A33: ((seq_n! 1) /" g) . k < 1 / (k - 2) ; :: thesis: S2[k + 1]
A34: k in NAT by ORDINAL1:def 13;
p . k > 2 by A29, A32;
then A35: (((seq_n! 1) /" g) . k) / (((seq_n! 1) /" g) . (k + 1)) > 2 by A8, A34;
A36: ((seq_n! 1) /" g) . (k + 1) > 0 by A4, NAT_1:11;
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 A35, XREAL_1:70;
then ((seq_n! 1) /" g) . k > 2 * (((seq_n! 1) /" g) . (k + 1)) by A36, XCMPLX_1:88;
then A37: (((seq_n! 1) /" g) . k) / 2 > ((seq_n! 1) /" g) . (k + 1) by XREAL_1:83;
(((seq_n! 1) /" g) . k) * (1 / 2) < (1 / (k - 2)) * (1 / 2) by A33, XREAL_1:70;
then A38: (((seq_n! 1) /" g) . k) / 2 < 1 / (2 * (k - 2)) by XCMPLX_1:103;
k >= 3 by A32, XXREAL_0:2;
then A39: 2 * (k - 2) >= k - 1 by A34, Lm41;
k - 1 >= 3 by A3, A32, XREAL_1:11;
then 1 / (2 * (k - 2)) <= 1 / (k - 1) by A39, XREAL_1:87;
then (((seq_n! 1) /" g) . k) / 2 < 1 / (k - 1) by A38, XXREAL_0:2;
hence S2[k + 1] by A37, XXREAL_0:2; :: thesis: verum
end;
A40: for n being Nat st n >= 4 holds
S2[n] from NAT_1:sch 8(A30, A31);
A41: 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 )
assume 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 p " > 0 ;
then A42: 1 / p > 0 ;
set N = [/((1 / p) + 4)\];
A43: [/((1 / p) + 4)\] >= (1 / p) + 4 by INT_1:def 5;
A44: 4 + (1 / p) > 4 by A42, XREAL_1:31;
then A45: [/((1 / p) + 4)\] >= 4 by A43, XXREAL_0:2;
reconsider N = [/((1 / p) + 4)\] as Element of NAT by A43, A44, 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 A46: n >= N ; :: thesis: abs ((((seq_n! 1) /" g) . n) - 0 ) < p
then A47: n >= 4 by A45, XXREAL_0:2;
then A48: ((seq_n! 1) /" g) . n < 1 / (n - 2) by A40;
n >= ((1 / p) + 2) + 2 by A43, A46, XXREAL_0:2;
then A49: n - 2 >= (1 / p) + 2 by XREAL_1:21;
(1 / p) + 2 > 1 / p by XREAL_1:31;
then n - 2 > 1 / p by A49, XXREAL_0:2;
then 1 / (n - 2) < 1 / (1 / p) by A42, XREAL_1:90;
then 1 / (n - 2) < 1 * p ;
then A50: ((seq_n! 1) /" g) . n < p by A48, XXREAL_0:2;
n >= 1 by A47, XXREAL_0:2;
then ((seq_n! 1) /" g) . n > 0 by A4;
hence abs ((((seq_n! 1) /" g) . n) - 0 ) < p by A50, ABSVALUE:def 1; :: thesis: verum
end;
then A51: (seq_n! 1) /" g is convergent by SEQ_2:def 6;
then lim ((seq_n! 1) /" g) = 0 by A41, SEQ_2:def 7;
then ( seq_n! 1 in Big_Oh g & not g in Big_Oh (seq_n! 1) ) by A51, ASYMPT_0:16;
then ( seq_n! 1 in Big_Oh g & not seq_n! 1 in Big_Omega g ) by ASYMPT_0:19;
hence ( g = g & Big_Oh (seq_n! 1) c= Big_Oh g & not Big_Oh (seq_n! 1) = Big_Oh g ) by Th4; :: thesis: verum