set g = seq_n! 1;
set f = seq_n! 0;
A1:
Big_Theta (seq_n! 1) = { s where s is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((seq_n! 1) . n) <= s . n & s . n <= c * ((seq_n! 1) . n) ) ) ) }
by ASYMPT_0:27;
now not seq_n! 0 in Big_Theta (seq_n! 1)assume
seq_n! 0 in Big_Theta (seq_n! 1)
;
contradictionthen consider s being
Element of
Funcs (
NAT,
REAL)
such that A2:
s = seq_n! 0
and A3:
ex
c,
d being
Real ex
N being
Element of
NAT st
(
c > 0 &
d > 0 & ( for
n being
Element of
NAT st
n >= N holds
(
d * ((seq_n! 1) . n) <= s . n &
s . n <= c * ((seq_n! 1) . n) ) ) )
by A1;
consider c,
d being
Real,
N being
Element of
NAT such that
c > 0
and A4:
d > 0
and A5:
for
n being
Element of
NAT st
n >= N holds
(
d * ((seq_n! 1) . n) <= s . n &
s . n <= c * ((seq_n! 1) . n) )
by A3;
ex
n being
Element of
NAT st
(
n >= N &
d * ((seq_n! 1) . n) > (seq_n! 0) . n )
proof
[/((N + 1) / d)\] >= (N + 1) / d
by INT_1:def 7;
then
[/((N + 1) / d)\] + 1
>= ((N + 1) / d) + 1
by XREAL_1:6;
then A6:
d * ([/((N + 1) / d)\] + 1) >= d * (((N + 1) / d) + 1)
by A4, XREAL_1:64;
A7:
N + 1
>= 1
+ 0
by XREAL_1:6;
d * (((N + 1) / d) + 1) =
(d * ((N + 1) / d)) + (d * 1)
.=
(N + 1) + d
by A4, XCMPLX_1:87
;
then A8:
d * (((N + 1) / d) + 1) > 1
by A4, A7, XREAL_1:8;
take n =
max (
N,
[/((N + 1) / d)\]);
( n is set & n is Element of NAT & n >= N & d * ((seq_n! 1) . n) > (seq_n! 0) . n )
A9:
n >= N
by XXREAL_0:25;
A10:
n >= [/((N + 1) / d)\]
by XXREAL_0:25;
n is
Integer
by XXREAL_0:16;
then reconsider n =
n as
Element of
NAT by A9, INT_1:3;
A11:
n ! <> 0
by NEWTON:17;
n + 1
>= [/((N + 1) / d)\] + 1
by A10, XREAL_1:6;
then
d * (n + 1) >= d * ([/((N + 1) / d)\] + 1)
by A4, XREAL_1:64;
then A12:
d * (n + 1) >= d * (((N + 1) / d) + 1)
by A6, XXREAL_0:2;
A13:
((seq_n! 0) . n) * ((n !) ") =
((n + 0) !) * ((n !) ")
by Def4
.=
1
by A11, XCMPLX_0:def 7
;
(d * ((seq_n! 1) . n)) * ((n !) ") =
(d * ((n + 1) !)) * ((n !) ")
by Def4
.=
(d * ((n + 1) * (n !))) * ((n !) ")
by NEWTON:15
.=
(d * (n + 1)) * ((n !) * ((n !) "))
.=
(d * (n + 1)) * 1
by A11, XCMPLX_0:def 7
.=
d * (n + 1)
;
then
(d * ((seq_n! 1) . n)) * ((n !) ") > 1
by A12, A8, XXREAL_0:2;
hence
(
n is
set &
n is
Element of
NAT &
n >= N &
d * ((seq_n! 1) . n) > (seq_n! 0) . n )
by A13, XREAL_1:64, XXREAL_0:25;
verum
end; hence
contradiction
by A2, A5;
verum end;
hence
not seq_n! 0 in Big_Theta (seq_n! 1)
; verum