let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; ( Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) & Partial_Sums Rseq2 is P-convergent implies Partial_Sums Rseq1 is P-convergent )
set RPS1 = Partial_Sums Rseq1;
set RPS2 = Partial_Sums Rseq2;
assume that
a2:
( Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) )
and
a1:
Partial_Sums Rseq2 is P-convergent
; Partial_Sums Rseq1 is P-convergent
for n, m being Nat holds 0 <= Rseq2 . (n,m)
proof
let n,
m be
Nat;
0 <= Rseq2 . (n,m)
(
0 <= Rseq1 . (
n,
m) &
Rseq1 . (
n,
m)
<= Rseq2 . (
n,
m) )
by a2;
hence
0 <= Rseq2 . (
n,
m)
;
verum
end;
then
Rseq2 is nonnegative-yielding
;
then
Partial_Sums Rseq2 is non-decreasing
by th80a;
then
Partial_Sums Rseq2 is bounded_above
by a1;
then consider M being Real such that
a3:
M is UpperBound of (Partial_Sums Rseq2) .: [:NAT,NAT:]
by XXREAL_2:def 10;
now for a being ExtReal st a in (Partial_Sums Rseq1) .: [:NAT,NAT:] holds
a <= Mlet a be
ExtReal;
( a in (Partial_Sums Rseq1) .: [:NAT,NAT:] implies a <= M )assume
a in (Partial_Sums Rseq1) .: [:NAT,NAT:]
;
a <= Mthen consider x being
Element of
[:NAT,NAT:] such that a5:
(
x in [:NAT,NAT:] &
a = (Partial_Sums Rseq1) . x )
by FUNCT_2:65;
consider n,
m being
object such that a6:
(
n in NAT &
m in NAT &
x = [n,m] )
by ZFMISC_1:def 2;
reconsider n =
n,
m =
m as
Element of
NAT by a6;
a7:
(Partial_Sums Rseq1) . (
n,
m)
<= (Partial_Sums Rseq2) . (
n,
m)
by a2, lm84;
(Partial_Sums Rseq2) . (
n,
m)
<= M
by a3, XXREAL_2:def 1, a6, FUNCT_2:35;
hence
a <= M
by a5, a6, a7, XXREAL_0:2;
verum end;
then
M is UpperBound of (Partial_Sums Rseq1) .: [:NAT,NAT:]
by XXREAL_2:def 1;
then a8:
Partial_Sums Rseq1 is bounded_above
by XXREAL_2:def 10;
Partial_Sums Rseq1 is non-decreasing
by a2, th80a;
hence
Partial_Sums Rseq1 is P-convergent
by a8; verum