let seq, seq1, seq2 be ExtREAL_sequence; ( seq1 is convergent & seq2 is convergent & seq1 is V116() & seq2 is V116() & ( for k being Nat holds seq . k = (seq1 . k) + (seq2 . k) ) implies ( seq is V116() & seq is convergent & lim seq = (lim seq1) + (lim seq2) ) )
assume that
A1:
seq1 is convergent
and
A2:
seq2 is convergent
and
A3:
seq1 is V116()
and
A4:
seq2 is V116()
and
A5:
for k being Nat holds seq . k = (seq1 . k) + (seq2 . k)
; ( seq is V116() & seq is convergent & lim seq = (lim seq1) + (lim seq2) )
A6:
not seq2 is convergent_to_-infty
by A4, Th8;
for n being object st n in dom seq holds
0. <= seq . n
hence
seq is V116()
by SUPINF_2:52; ( seq is convergent & lim seq = (lim seq1) + (lim seq2) )
A9:
not seq1 is convergent_to_-infty
by A3, Th8;
for n being Nat holds 0 <= seq2 . n
by A4, SUPINF_2:51;
then A10:
lim seq2 <> -infty
by A2, Th10;
per cases
( seq1 is convergent_to_+infty or seq1 is convergent_to_finite_number )
by A1, A9;
suppose A16:
seq1 is
convergent_to_finite_number
;
( seq is convergent & lim seq = (lim seq1) + (lim seq2) )then A17:
not
seq1 is
convergent_to_-infty
by MESFUNC5:51;
not
seq1 is
convergent_to_+infty
by A16, MESFUNC5:50;
then consider g being
Real such that A18:
lim seq1 = g
and A19:
for
p being
Real st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((seq1 . m) - (lim seq1)).| < p
and
seq1 is
convergent_to_finite_number
by A1, A17, MESFUNC5:def 12;
per cases
( seq2 is convergent_to_+infty or seq2 is convergent_to_finite_number )
by A2, A6;
suppose A25:
seq2 is
convergent_to_finite_number
;
( seq is convergent & lim seq = (lim seq1) + (lim seq2) )then A26:
not
seq2 is
convergent_to_-infty
by MESFUNC5:51;
not
seq2 is
convergent_to_+infty
by A25, MESFUNC5:50;
then consider h being
Real such that A27:
lim seq2 = h
and A28:
for
p being
Real st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((seq2 . m) - (lim seq2)).| < p
and
seq2 is
convergent_to_finite_number
by A2, A26, MESFUNC5:def 12;
reconsider h9 =
h,
g9 =
g as
Real ;
reconsider gh =
g + h as
R_eal by XXREAL_0:def 1;
A29:
for
p being
Real st
0 < p holds
ex
n being
Nat st
for
m being
Nat st
n <= m holds
|.((seq . m) - (g + h)).| < p
proof
let p be
Real;
( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (g + h)).| < p )
reconsider pp =
p as
Element of
REAL by XREAL_0:def 1;
assume A30:
0 < p
;
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (g + h)).| < p
then consider n1 being
Nat such that A31:
for
m being
Nat st
n1 <= m holds
|.((seq1 . m) - (lim seq1)).| < p / 2
by A19;
consider n2 being
Nat such that A32:
for
m being
Nat st
n2 <= m holds
|.((seq2 . m) - (lim seq2)).| < p / 2
by A28, A30;
reconsider n19 =
n1,
n29 =
n2 as
Element of
NAT by ORDINAL1:def 12;
reconsider n =
max (
n19,
n29) as
Nat ;
take
n
;
for m being Nat st n <= m holds
|.((seq . m) - (g + h)).| < p
let m be
Nat;
( n <= m implies |.((seq . m) - (g + h)).| < p )
assume A33:
n <= m
;
|.((seq . m) - (g + h)).| < p
A34:
pp / 2
in REAL
by XREAL_0:def 1;
n2 <= n
by XXREAL_0:25;
then
n2 <= m
by A33, XXREAL_0:2;
then A35:
|.((seq2 . m) - (lim seq2)).| < pp / 2
by A32;
then
|.((seq2 . m) - (lim seq2)).| < +infty
by XXREAL_0:2, XXREAL_0:9, A34;
then A36:
(seq2 . m) - h in REAL
by A27, EXTREAL1:41;
n1 <= n
by XXREAL_0:25;
then
n1 <= m
by A33, XXREAL_0:2;
then A37:
|.((seq1 . m) - (lim seq1)).| < pp / 2
by A31;
then
|.((seq1 . m) - (lim seq1)).| < +infty
by XXREAL_0:2, XXREAL_0:9, A34;
then
(seq1 . m) - g in REAL
by A18, EXTREAL1:41;
then consider e1,
e2 being
Real such that A38:
e1 = (seq1 . m) - g
and A39:
e2 = (seq2 . m) - h
by A36;
A40:
|.((seq2 . m) - h).| = |.e2.|
by A39, EXTREAL1:12;
A41:
0 <= seq2 . m
by A4, SUPINF_2:51;
then A42:
(seq2 . m) - h <> -infty
by XXREAL_3:19;
A43:
0 <= seq1 . m
by A3, SUPINF_2:51;
A44:
|.((seq1 . m) - g).| = |.e1.|
by A38, EXTREAL1:12;
then A45:
|.((seq2 . m) - h).| + |.((seq1 . m) - g).| = |.e1.| + |.e2.|
by A40, SUPINF_2:1;
g + h = g + h
;
then (seq . m) - (g + h) =
((seq . m) - h) - g
by XXREAL_3:31
.=
(((seq1 . m) + (seq2 . m)) - h) - g
by A5
.=
((seq1 . m) + ((seq2 . m) - h)) - g
by A43, A41, XXREAL_3:30
.=
((seq2 . m) - h) + ((seq1 . m) - g)
by A43, A42, XXREAL_3:30
;
then A46:
|.((seq . m) - (g + h)).| <= |.((seq2 . m) - h).| + |.((seq1 . m) - g).|
by EXTREAL1:24;
|.e1.| + |.e2.| < (p / 2) + (p / 2)
by A18, A27, A37, A35, A44, A40, XREAL_1:8;
hence
|.((seq . m) - (g + h)).| < p
by A46, A45, XXREAL_0:2;
verum
end; then A47:
seq is
convergent_to_finite_number
;
hence
seq is
convergent
;
lim seq = (lim seq1) + (lim seq2)then
lim seq = gh
by A29, A47, MESFUNC5:def 12;
hence
lim seq = (lim seq1) + (lim seq2)
by A18, A27, SUPINF_2:1;
verum end; end; end; end;