set q = seq_const 1;
set p = seq_n^ 1;
set f = (seq_n^ 1) - (seq_const 1);
set g = seq_n^ 1;
A1:
Big_Theta (seq_n^ 1) = { t where t 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) <= t . n & t . n <= c * ((seq_n^ 1) . n) ) ) ) }
by ASYMPT_0:27;
let F be eventually-nonnegative Real_Sequence; ( F = (seq_n^ 1) - (seq_const 1) implies (Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1) )
assume
F = (seq_n^ 1) - (seq_const 1)
; (Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1)
then A2:
Big_Theta F = { t where t 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) - (seq_const 1)) . n) <= t . n & t . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) ) ) ) }
by ASYMPT_0:27;
now for x being object holds
( ( x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) implies x in Big_Theta (seq_n^ 1) ) & ( x in Big_Theta (seq_n^ 1) implies x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) ) )let x be
object ;
( ( x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) implies x in Big_Theta (seq_n^ 1) ) & ( x in Big_Theta (seq_n^ 1) implies x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) ) )hereby ( x in Big_Theta (seq_n^ 1) implies x in (Big_Theta F) + (Big_Theta (seq_n^ 1)) )
assume
x in (Big_Theta F) + (Big_Theta (seq_n^ 1))
;
x in Big_Theta (seq_n^ 1)then consider t being
Element of
Funcs (
NAT,
REAL)
such that A3:
t = x
and A4:
ex
f9,
g9 being
Element of
Funcs (
NAT,
REAL) st
(
f9 in Big_Theta F &
g9 in Big_Theta (seq_n^ 1) & ( for
n being
Element of
NAT holds
t . n = (f9 . n) + (g9 . n) ) )
;
consider f9,
g9 being
Element of
Funcs (
NAT,
REAL)
such that A5:
f9 in Big_Theta F
and A6:
g9 in Big_Theta (seq_n^ 1)
and A7:
for
n being
Element of
NAT holds
t . n = (f9 . n) + (g9 . n)
by A4;
ex
r being
Element of
Funcs (
NAT,
REAL) st
(
r = f9 & 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) - (seq_const 1)) . n) <= r . n &
r . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) ) ) ) )
by A2, A5;
then consider c1,
d1 being
Real,
N1 being
Element of
NAT such that A8:
c1 > 0
and A9:
d1 > 0
and A10:
for
n being
Element of
NAT st
n >= N1 holds
(
d1 * (((seq_n^ 1) - (seq_const 1)) . n) <= f9 . n &
f9 . n <= c1 * (((seq_n^ 1) - (seq_const 1)) . n) )
;
ex
s being
Element of
Funcs (
NAT,
REAL) st
(
s = g9 & 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, A6;
then consider c2,
d2 being
Real,
N2 being
Element of
NAT such that A11:
c2 > 0
and A12:
d2 > 0
and A13:
for
n being
Element of
NAT st
n >= N2 holds
(
d2 * ((seq_n^ 1) . n) <= g9 . n &
g9 . n <= c2 * ((seq_n^ 1) . n) )
;
set d =
d2;
set c =
c1 + c2;
set N =
max (1,
(max (N1,N2)));
A14:
max (1,
(max (N1,N2)))
>= 1
by XXREAL_0:25;
A15:
max (1,
(max (N1,N2)))
>= max (
N1,
N2)
by XXREAL_0:25;
max (
N1,
N2)
>= N2
by XXREAL_0:25;
then A16:
max (1,
(max (N1,N2)))
>= N2
by A15, XXREAL_0:2;
max (
N1,
N2)
>= N1
by XXREAL_0:25;
then A17:
max (1,
(max (N1,N2)))
>= N1
by A15, XXREAL_0:2;
now for n being Element of NAT st n >= max (1,(max (N1,N2))) holds
( d2 * ((seq_n^ 1) . n) <= t . n & t . n <= (c1 + c2) * ((seq_n^ 1) . n) )let n be
Element of
NAT ;
( n >= max (1,(max (N1,N2))) implies ( d2 * ((seq_n^ 1) . n) <= t . n & t . n <= (c1 + c2) * ((seq_n^ 1) . n) ) )A18:
(seq_const 1) . n = 1
by FUNCOP_1:7;
assume A19:
n >= max (1,
(max (N1,N2)))
;
( d2 * ((seq_n^ 1) . n) <= t . n & t . n <= (c1 + c2) * ((seq_n^ 1) . n) )then A20:
(seq_n^ 1) . n =
n to_power 1
by A14, Def3
.=
n
by POWER:25
;
n >= 1
by A14, A19, XXREAL_0:2;
then
- n <= - 1
by XREAL_1:24;
then
(- n) * d1 <= (- 1) * d1
by A9, XREAL_1:64;
then A21:
(n * (- d1)) + ((d1 + d2) * n) <= (- d1) + ((d1 + d2) * n)
by XREAL_1:6;
A22:
((seq_n^ 1) - (seq_const 1)) . n =
((seq_n^ 1) . n) + ((- (seq_const 1)) . n)
by SEQ_1:7
.=
((seq_n^ 1) . n) + (- ((seq_const 1) . n))
by SEQ_1:10
.=
(n to_power 1) + (- ((seq_const 1) . n))
by A14, A19, Def3
.=
n + (- 1)
by A18, POWER:25
;
A23:
n >= N2
by A16, A19, XXREAL_0:2;
then
d2 * ((seq_n^ 1) . n) <= g9 . n
by A13;
then A24:
(d1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (d2 * ((seq_n^ 1) . n)) <= (d1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (g9 . n)
by XREAL_1:6;
g9 . n <= c2 * ((seq_n^ 1) . n)
by A13, A23;
then A25:
(c1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (g9 . n) <= (c1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (c2 * ((seq_n^ 1) . n))
by XREAL_1:6;
A26:
n >= N1
by A17, A19, XXREAL_0:2;
then
f9 . n <= c1 * (((seq_n^ 1) - (seq_const 1)) . n)
by A10;
then
(f9 . n) + (g9 . n) <= (c1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (g9 . n)
by XREAL_1:6;
then A27:
(f9 . n) + (g9 . n) <= (c1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (c2 * ((seq_n^ 1) . n))
by A25, XXREAL_0:2;
d1 * (((seq_n^ 1) - (seq_const 1)) . n) <= f9 . n
by A10, A26;
then
(d1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (g9 . n) <= (f9 . n) + (g9 . n)
by XREAL_1:6;
then
(d1 * (((seq_n^ 1) - (seq_const 1)) . n)) + (d2 * ((seq_n^ 1) . n)) <= (f9 . n) + (g9 . n)
by A24, XXREAL_0:2;
then
d2 * n <= (f9 . n) + (g9 . n)
by A20, A22, A21, XXREAL_0:2;
hence
d2 * ((seq_n^ 1) . n) <= t . n
by A7, A20;
t . n <= (c1 + c2) * ((seq_n^ 1) . n)
(- c1) + ((c1 + c2) * n) <= 0 + ((c1 + c2) * n)
by A8, XREAL_1:6;
then
(f9 . n) + (g9 . n) <= (c1 + c2) * n
by A20, A22, A27, XXREAL_0:2;
hence
t . n <= (c1 + c2) * ((seq_n^ 1) . n)
by A7, A20;
verum end; hence
x in Big_Theta (seq_n^ 1)
by A1, A3, A8, A11, A12;
verum
end; assume
x in Big_Theta (seq_n^ 1)
;
x in (Big_Theta F) + (Big_Theta (seq_n^ 1))then consider t being
Element of
Funcs (
NAT,
REAL)
such that A28:
t = x
and A29:
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) <= t . n &
t . n <= c * ((seq_n^ 1) . n) ) ) )
by A1;
consider c,
d being
Real,
N being
Element of
NAT such that A30:
c > 0
and A31:
d > 0
and A32:
for
n being
Element of
NAT st
n >= N holds
(
d * ((seq_n^ 1) . n) <= t . n &
t . n <= c * ((seq_n^ 1) . n) )
by A29;
set f9 =
(2 ") (#) t;
set g9 =
(2 ") (#) t;
A33:
(2 ") (#) t is
Element of
Funcs (
NAT,
REAL)
by FUNCT_2:8;
A34:
for
n being
Element of
NAT holds
t . n = (((2 ") (#) t) . n) + (((2 ") (#) t) . n)
A35:
(2 ") * d > (2 ") * 0
by A31, XREAL_1:68;
set N0 =
max (
N,2);
A36:
max (
N,2)
>= N
by XXREAL_0:25;
A37:
max (
N,2)
>= 2
by XXREAL_0:25;
reconsider N0 =
max (
N,2) as
Element of
NAT ;
(2 ") * c > (2 ") * 0
by A30, XREAL_1:68;
then A41:
(2 ") (#) t in Big_Theta (seq_n^ 1)
by A1, A35, A33, A38;
now for n being Element of NAT st n >= N0 holds
( ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) )let n be
Element of
NAT ;
( n >= N0 implies ( ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) ) )A42:
(seq_const 1) . n = 1
by FUNCOP_1:7;
assume A43:
n >= N0
;
( ((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") (#) t) . n & ((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n) )then A44:
(seq_n^ 1) . n =
(n to_power 1) - 0
by A37, Def3
.=
n - 0
by POWER:25
;
n >= 2
by A37, A43, XXREAL_0:2;
then
n + 2
<= n + n
by XREAL_1:6;
then
n <= (2 * n) - (2 * 1)
by XREAL_1:19;
then
(2 ") * n <= (2 ") * (2 * (n - 1))
by XREAL_1:64;
then A45:
c * ((2 ") * n) <= c * (n - 1)
by A30, XREAL_1:64;
A46:
n >= N
by A36, A43, XXREAL_0:2;
then A47:
(2 ") * (d * ((seq_n^ 1) . n)) <= (2 ") * (t . n)
by A32, XREAL_1:64;
A48:
((seq_n^ 1) - (seq_const 1)) . n =
((seq_n^ 1) . n) + ((- (seq_const 1)) . n)
by SEQ_1:7
.=
((seq_n^ 1) . n) + (- 1)
by A42, SEQ_1:10
.=
((seq_n^ 1) . n) - 1
.=
(n to_power 1) - 1
by A37, A43, Def3
.=
n - 1
by POWER:25
;
then
((seq_n^ 1) - (seq_const 1)) . n <= (seq_n^ 1) . n
by A44, XREAL_1:13;
then
((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") * d) * ((seq_n^ 1) . n)
by A31, XREAL_1:64;
then
((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= (2 ") * (t . n)
by A47, XXREAL_0:2;
hence
((2 ") * d) * (((seq_n^ 1) - (seq_const 1)) . n) <= ((2 ") (#) t) . n
by SEQ_1:9;
((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n)
(2 ") * (t . n) <= (2 ") * (c * ((seq_n^ 1) . n))
by A32, A46, XREAL_1:64;
then
(2 ") * (t . n) <= c * (((seq_n^ 1) - (seq_const 1)) . n)
by A48, A44, A45, XXREAL_0:2;
hence
((2 ") (#) t) . n <= c * (((seq_n^ 1) - (seq_const 1)) . n)
by SEQ_1:9;
verum end; then
(2 ") (#) t in Big_Theta F
by A2, A30, A35, A33;
hence
x in (Big_Theta F) + (Big_Theta (seq_n^ 1))
by A28, A33, A41, A34;
verum end;
hence
(Big_Theta F) + (Big_Theta (seq_n^ 1)) = Big_Theta (seq_n^ 1)
by TARSKI:2; verum