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