let J, K, L be ExtREAL_sequence; :: thesis: ( ( for n, m being Nat st n <= m holds
J . n <= J . m ) & ( for n, m being Nat st n <= m holds
K . n <= K . m ) & J is without-infty & K is without-infty & ( for n being Nat holds (J . n) + (K . n) = L . n ) implies ( L is convergent & lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) ) )
assume that
A1: for n, m being Nat st n <= m holds
J . n <= J . m and
A2: for n, m being Nat st n <= m holds
K . n <= K . m and
A3: ( J is without-infty & K is without-infty ) and
A4: for n being Nat holds (J . n) + (K . n) = L . n ; :: thesis: ( L is convergent & lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )
A5: ( dom J = NAT & dom K = NAT & dom L = NAT ) by FUNCT_2:def 1;
A6: now
per cases ( sup (rng J) in REAL or sup (rng J) = +infty ) by A3, Lm9;
suppose A7: sup (rng J) in REAL ; :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )
then reconsider SJ = sup (rng J) as real number ;
per cases ( sup (rng K) in REAL or sup (rng K) = +infty ) by A3, Lm9;
suppose A8: sup (rng K) in REAL ; :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )
then reconsider SK = sup (rng K) as real number ;
A10: now
let p be real number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (R_EAL (SJ + SK))).| < p )
assume Z: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((L . m) - (R_EAL (SJ + SK))).| < p
consider SJ' being ext-real number such that
A12: ( SJ' in rng J & (sup (rng J)) - (R_EAL (p / 2)) < SJ' ) by A7, Z, MEASURE6:33;
consider nj being set such that
A13: ( nj in dom J & SJ' = J . nj ) by A12, FUNCT_1:def 5;
reconsider nj = nj as Element of NAT by A13;
consider SK' being ext-real number such that
A14: ( SK' in rng K & (sup (rng K)) - (R_EAL (p / 2)) < SK' ) by A8, Z, MEASURE6:33;
consider nk being set such that
A15: ( nk in dom K & SK' = K . nk ) by A14, FUNCT_1:def 5;
reconsider nk = nk as Element of NAT by A15;
(p / 2) + (p / 2) = p ;
then A16: R_EAL p = (R_EAL (p / 2)) + (R_EAL (p / 2)) by SUPINF_2:1;
reconsider n = max nj,nk as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((L . m) - (R_EAL (SJ + SK))).| < p
hereby :: thesis: verum
let m be Nat; :: thesis: ( n <= m implies |.((L . m) - (R_EAL (SJ + SK))).| < p )
assume A17: n <= m ; :: thesis: |.((L . m) - (R_EAL (SJ + SK))).| < p
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
( R_EAL SJ in REAL & R_EAL SK in REAL & R_EAL (SJ + SK) in REAL ) by XREAL_0:def 1;
then A18: ( R_EAL SJ < +infty & -infty < R_EAL SJ & R_EAL SK < +infty & -infty < R_EAL SK & R_EAL (SJ + SK) < +infty & -infty < R_EAL (SJ + SK) ) by XXREAL_0:9, XXREAL_0:12;
( J . m1 in rng J & K . m1 in rng K ) by A5, FUNCT_1:12;
then A19: ( J . m <= R_EAL SJ & K . m <= R_EAL SK ) by XXREAL_2:4;
then A20: ( -infty < J . m & J . m < +infty & -infty < K . m & K . m < +infty ) by A3, A18, Def5, XXREAL_0:2;
B22: L . m = (J . m) + (K . m) by A4;
A23: - ((L . m) - (R_EAL (SJ + SK))) = (R_EAL (SJ + SK)) - (L . m) by XXREAL_3:27;
(J . m) + (K . m) <= (R_EAL SJ) + (R_EAL SK) by A19, XXREAL_3:38;
then (L . m) - (R_EAL (SJ + SK)) <= 0 by B22, A23, XXREAL_3:43;
then A24: |.((L . m) - (R_EAL (SJ + SK))).| = (R_EAL (SJ + SK)) - (L . m) by A23, EXTREAL2:55;
A25: ((R_EAL SJ) - (J . m)) + ((R_EAL SK) - (K . m)) = (((R_EAL SJ) - (J . m)) + (R_EAL SK)) - (K . m) by A20, XXREAL_3:31
.= (((R_EAL SK) + (R_EAL SJ)) - (J . m)) - (K . m) by XXREAL_3:31
.= (R_EAL (SK + SJ)) - ((J . m) + (K . m)) by A18, A19, XXREAL_3:32
.= (R_EAL (SK + SJ)) - (L . m) by A4 ;
reconsider SJ' = SJ', SK' = SK' as R_eal by XXREAL_0:def 1;
( R_EAL SJ < (R_EAL (p / 2)) + SJ' & R_EAL (p / 2) <> -infty & R_EAL SK < (R_EAL (p / 2)) + SK' & R_EAL (p / 2) <> -infty ) by A12, A14, XXREAL_3:65;
then A26: ( (R_EAL SJ) - SJ' < R_EAL (p / 2) & (R_EAL SK) - SK' < R_EAL (p / 2) ) by XXREAL_3:66;
nk <= n by XXREAL_0:25;
then nk <= m by A17, XXREAL_0:2;
then K . nk <= K . m by A2;
then ( -infty < SK' & SK' < +infty ) by A3, A15, A20, Def5, XXREAL_0:2;
then reconsider s0 = SK' as Real by XXREAL_0:14;
reconsider s1 = R_EAL SK as Real by XREAL_0:def 1;
(R_EAL SK) - SK' = s1 - s0 by SUPINF_2:5;
then A27: ((R_EAL SJ) - SJ') + ((R_EAL SK) - SK') < (R_EAL (p / 2)) + ((R_EAL SK) - SK') by A26, XXREAL_3:47;
(R_EAL (p / 2)) + ((R_EAL SK) - SK') < (R_EAL (p / 2)) + (R_EAL (p / 2)) by A26, XXREAL_3:47;
then A28: ((R_EAL SJ) - SJ') + ((R_EAL SK) - SK') < (R_EAL (p / 2)) + (R_EAL (p / 2)) by A27, XXREAL_0:2;
( nj <= n & nk <= n ) by XXREAL_0:25;
then ( nj <= m & nk <= m ) by A17, XXREAL_0:2;
then ( SJ' <= J . m & SK' <= K . m ) by A1, A2, A13, A15;
then ( (R_EAL SJ) - (J . m) <= (R_EAL SJ) - SJ' & (R_EAL SK) - (K . m) <= (R_EAL SK) - SK' ) by XXREAL_3:39;
then ((R_EAL SJ) - (J . m)) + ((R_EAL SK) - (K . m)) <= ((R_EAL SJ) - SJ') + ((R_EAL SK) - SK') by XXREAL_3:38;
hence |.((L . m) - (R_EAL (SJ + SK))).| < p by A16, A24, A25, A28, XXREAL_0:2; :: thesis: verum
end;
end;
then A30: L is convergent_to_finite_number by Def8;
hence L is convergent by Def11; :: thesis: lim L = (sup (rng J)) + (sup (rng K))
hence lim L = (sup (rng J)) + (sup (rng K)) by A10, A30, Def12; :: thesis: verum
end;
suppose A31: sup (rng K) = +infty ; :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )
for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
p <= L . m
proof
let p be real number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
p <= L . m )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
p <= L . m
then consider j being ext-real number such that
A32: ( j in rng J & (sup (rng J)) - (R_EAL (p / 2)) < j ) by A7, MEASURE6:33;
consider n1 being set such that
A33: ( n1 in dom J & j = J . n1 ) by A32, FUNCT_1:def 5;
reconsider n1 = n1 as Element of NAT by A33;
reconsider supj = sup (rng J) as Real by A7;
reconsider p'2 = p / 2, p' = p as Real by XREAL_0:def 1;
A34: supj - p'2 = (sup (rng J)) - (R_EAL (p / 2)) by SUPINF_2:5;
then A35: p' - (supj - p'2) = (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) by SUPINF_2:5;
then (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) < sup (rng K) by A31, XXREAL_0:9;
then consider k being R_eal such that
A36: ( k in rng K & (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) < k ) by HAHNBAN:8;
consider n2 being set such that
A37: ( n2 in dom K & k = K . n2 ) by A36, FUNCT_1:def 5;
reconsider n2 = n2 as Element of NAT by A37;
set n = max n1,n2;
( n1 <= max n1,n2 & n2 <= max n1,n2 ) by XXREAL_0:25;
then ( J . n1 <= J . (max n1,n2) & K . n2 <= K . (max n1,n2) ) by A1, A2;
then A38: ( (sup (rng J)) - (R_EAL (p / 2)) < J . (max n1,n2) & (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) < K . (max n1,n2) ) by A32, A33, A36, A37, XXREAL_0:2;
A39: -infty < (R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2))) by A35, XXREAL_0:12;
p' = (p' - (supj - p'2)) + (supj - p'2) ;
then ((R_EAL p) - ((sup (rng J)) - (R_EAL (p / 2)))) + ((sup (rng J)) - (R_EAL (p / 2))) = p' by A34, A35, SUPINF_2:1;
then A43: R_EAL p < (J . (max n1,n2)) + (K . (max n1,n2)) by A38, A39, XXREAL_3:75;
now
let m be Nat; :: thesis: ( max n1,n2 <= m implies p <= L . m )
assume max n1,n2 <= m ; :: thesis: p <= L . m
then A44: ( J . (max n1,n2) <= J . m & K . (max n1,n2) <= K . m ) by A1, A2;
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
(J . (max n1,n2)) + (K . (max n1,n2)) <= (J . m) + (K . m) by A44, XXREAL_3:38;
then (J . (max n1,n2)) + (K . (max n1,n2)) <= L . m by A4;
hence p <= L . m by A43, XXREAL_0:2; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
p <= L . m ; :: thesis: verum
end;
then A45: L is convergent_to_+infty by Def9;
hence L is convergent by Def11; :: thesis: lim L = (sup (rng J)) + (sup (rng K))
then lim L = +infty by A45, Def12;
hence lim L = (sup (rng J)) + (sup (rng K)) by A31, A7, XXREAL_3:def 2; :: thesis: verum
end;
end;
end;
suppose A47: sup (rng J) = +infty ; :: thesis: ( L is convergent & lim L = (sup (rng J)) + (sup (rng K)) )
now
let p be real number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st m <= b3 holds
n <= L . b3 )
assume Z: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st m <= b3 holds
n <= L . b3
per cases ( sup (rng K) in REAL or sup (rng K) = +infty ) by A3, Lm9;
suppose A49: sup (rng K) in REAL ; :: thesis: ex n being Nat st
for m being Nat st m <= b3 holds
n <= L . b3
then consider k being ext-real number such that
A50: ( k in rng K & (sup (rng K)) - (R_EAL (p / 2)) < k ) by Z, MEASURE6:33;
consider n1 being set such that
A51: ( n1 in dom K & k = K . n1 ) by A50, FUNCT_1:def 5;
reconsider n1 = n1 as Element of NAT by A51;
reconsider supk = sup (rng K) as Real by A49;
reconsider p'2 = p / 2, p' = p as Real by XREAL_0:def 1;
A52: supk - p'2 = (sup (rng K)) - (R_EAL (p / 2)) by SUPINF_2:5;
then A53: p' - (supk - p'2) = (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) by SUPINF_2:5;
then (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) < sup (rng J) by A47, XXREAL_0:9;
then consider j being R_eal such that
A54: ( j in rng J & (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) < j ) by HAHNBAN:8;
consider n2 being set such that
A55: ( n2 in dom J & j = J . n2 ) by A54, FUNCT_1:def 5;
reconsider n2 = n2 as Element of NAT by A55;
set n = max n1,n2;
( n1 <= max n1,n2 & n2 <= max n1,n2 ) by XXREAL_0:25;
then ( J . n2 <= J . (max n1,n2) & K . n1 <= K . (max n1,n2) ) by A1, A2;
then A56: ( (sup (rng K)) - (R_EAL (p / 2)) < K . (max n1,n2) & (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) < J . (max n1,n2) ) by A50, A51, A54, A55, XXREAL_0:2;
A57: -infty < (R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2))) by A53, XXREAL_0:12;
p' = (p' - (supk - p'2)) + (supk - p'2) ;
then ((R_EAL p) - ((sup (rng K)) - (R_EAL (p / 2)))) + ((sup (rng K)) - (R_EAL (p / 2))) = p' by A52, A53, SUPINF_2:1;
then A61: R_EAL p < (J . (max n1,n2)) + (K . (max n1,n2)) by A56, A57, XXREAL_3:75;
now
let m be Nat; :: thesis: ( max n1,n2 <= m implies p <= L . m )
assume max n1,n2 <= m ; :: thesis: p <= L . m
then A62: ( J . (max n1,n2) <= J . m & K . (max n1,n2) <= K . m ) by A1, A2;
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;
(J . (max n1,n2)) + (K . (max n1,n2)) <= (J . m) + (K . m) by A62, XXREAL_3:38;
then (J . (max n1,n2)) + (K . (max n1,n2)) <= L . m by A4;
hence p <= L . m by A61, XXREAL_0:2; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
p <= L . m ; :: thesis: verum
end;
suppose sup (rng K) = +infty ; :: thesis: ex n being Nat st
for m being Nat st m <= b3 holds
n <= L . b3
then consider n1 being Nat such that
A63: R_EAL (p / 2) < K . n1 by A3, Z, Th65;
consider n2 being Nat such that
A64: R_EAL (p / 2) < J . n2 by A3, A47, Z, Th65;
reconsider n1 = n1, n2 = n2 as Element of NAT by ORDINAL1:def 13;
set n = max n1,n2;
( n1 <= max n1,n2 & n2 <= max n1,n2 ) by XXREAL_0:25;
then ( J . n2 <= J . (max n1,n2) & K . n1 <= K . (max n1,n2) ) by A1, A2;
then A65: ( R_EAL (p / 2) < J . (max n1,n2) & R_EAL (p / 2) < K . (max n1,n2) ) by A63, A64, XXREAL_0:2;
-infty < R_EAL (p / 2) by XXREAL_0:12;
then A66: (R_EAL (p / 2)) + (R_EAL (p / 2)) < (J . (max n1,n2)) + (K . (max n1,n2)) by A65, XXREAL_3:75;
(p / 2) + (p / 2) = p ;
then p < (J . (max n1,n2)) + (K . (max n1,n2)) by A66, SUPINF_2:1;
then A67: R_EAL p < L . (max n1,n2) by A4;
now
let m be Nat; :: thesis: ( max n1,n2 <= m implies p <= L . m )
assume max n1,n2 <= m ; :: thesis: p <= L . m
then A68: ( J . (max n1,n2) <= J . m & K . (max n1,n2) <= K . m ) by A1, A2;
(J . (max n1,n2)) + (K . (max n1,n2)) <= (J . m) + (K . m) by A68, XXREAL_3:38;
then (J . (max n1,n2)) + (K . (max n1,n2)) <= L . m by A4;
then L . (max n1,n2) <= L . m by A4;
hence p <= L . m by A67, XXREAL_0:2; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
p <= L . m ; :: thesis: verum
end;
end;
end;
then A69: L is convergent_to_+infty by Def9;
hence L is convergent by Def11; :: thesis: lim L = (sup (rng J)) + (sup (rng K))
then A70: lim L = +infty by A69, Def12;
K . 0 in rng K by A5, FUNCT_1:12;
then ( -infty < K . 0 & K . 0 <= sup (rng K) ) by A3, Def5, XXREAL_2:4;
hence lim L = (sup (rng J)) + (sup (rng K)) by A47, A70, XXREAL_3:def 2; :: thesis: verum
end;
end;
end;
hence L is convergent ; :: thesis: ( lim L = sup (rng L) & lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )
A71: now
let n, m be Nat; :: thesis: ( n <= m implies L . n <= L . m )
assume n <= m ; :: thesis: L . n <= L . m
then A72: ( J . n <= J . m & K . n <= K . m ) by A1, A2;
(J . n) + (K . n) <= (J . m) + (K . m) by A72, XXREAL_3:38;
then L . n <= (J . m) + (K . m) by A4;
hence L . n <= L . m by A4; :: thesis: verum
end;
hence lim L = sup (rng L) by Th60; :: thesis: ( lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) )
( lim J = sup (rng J) & lim K = sup (rng K) ) by A1, A2, Th60;
hence ( lim L = (lim J) + (lim K) & sup (rng L) = (sup (rng K)) + (sup (rng J)) ) by A6, A71, Th60; :: thesis: verum