set g = seq_n! 1;
set f = seq_n! 0;
set h = (seq_n! 0) /" (seq_n! 1);
A1:
for n being Element of NAT holds ((seq_n! 0) /" (seq_n! 1)) . n = 1 / (n + 1)
A3:
now for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < plet p be
Real;
( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < p )assume A4:
p > 0
;
ex N being Nat st
for n being Nat st n >= N holds
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < pset N =
max (1,
[/(1 / p)\]);
A5:
max (1,
[/(1 / p)\])
>= 1
by XXREAL_0:25;
A6:
max (1,
[/(1 / p)\])
>= [/(1 / p)\]
by XXREAL_0:25;
max (1,
[/(1 / p)\]) is
Integer
by XXREAL_0:16;
then reconsider N =
max (1,
[/(1 / p)\]) as
Element of
NAT by A5, INT_1:3;
[/(1 / p)\] >= 1
/ p
by INT_1:def 7;
then A7:
N >= 1
/ p
by A6, XXREAL_0:2;
reconsider N =
N as
Nat ;
take N =
N;
for n being Nat st n >= N holds
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < plet n be
Nat;
( n >= N implies |.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < p )A8:
n in NAT
by ORDINAL1:def 12;
assume
n >= N
;
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < pthen
n + 1
> N
by NAT_1:13;
then
n + 1
> 1
/ p
by A7, XXREAL_0:2;
then
1
/ (n + 1) < 1
/ (1 / p)
by A4, XREAL_1:88;
then A9:
((seq_n! 0) /" (seq_n! 1)) . n < p
by A1, A8;
A10:
0 < 1
/ (n + 1)
;
- p < - 0
by A4, XREAL_1:24;
then A11:
- p < ((seq_n! 0) /" (seq_n! 1)) . n
by A1, A10, A8;
|.(((seq_n! 0) /" (seq_n! 1)) . n).| < p
hence
|.((((seq_n! 0) /" (seq_n! 1)) . n) - 0).| < p
;
verum end;
then A14:
(seq_n! 0) /" (seq_n! 1) is convergent
by SEQ_2:def 6;
then A15:
lim ((seq_n! 0) /" (seq_n! 1)) = 0
by A3, SEQ_2:def 7;
then
not seq_n! 1 in Big_Oh (seq_n! 0)
by A14, ASYMPT_0:16;
then A16:
not seq_n! 0 in Big_Omega (seq_n! 1)
by ASYMPT_0:19;
seq_n! 0 in Big_Oh (seq_n! 1)
by A14, A15, ASYMPT_0:16;
hence
( Big_Oh (seq_n! 0) c= Big_Oh (seq_n! 1) & Big_Oh (seq_n! 0) <> Big_Oh (seq_n! 1) )
by A16, Th4; verum