let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding implies Partial_Sums Rseq is non-decreasing )
set CPS = Partial_Sums Rseq;
assume a1: Rseq is nonnegative-yielding ; :: thesis: Partial_Sums Rseq is non-decreasing
now :: thesis: for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds
(Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n2,m2)
let n1, m1, n2, m2 be Nat; :: thesis: ( n1 >= n2 & m1 >= m2 implies (Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n2,m2) )
assume b2: ( n1 >= n2 & m1 >= m2 ) ; :: thesis: (Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n2,m2)
then consider dn being Nat such that
b3: n1 = n2 + dn by NAT_1:10;
consider dm being Nat such that
b4: m1 = m2 + dm by b2, NAT_1:10;
reconsider dn = dn, dm = dm as Element of NAT by ORDINAL1:def 12;
defpred S1[ Nat] means (Partial_Sums Rseq) . ((n2 + $1),m2) >= (Partial_Sums Rseq) . (n2,m2);
b5: S1[ 0 ] ;
b6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume a7: S1[k] ; :: thesis: S1[k + 1]
b8: (Partial_Sums Rseq) . (((n2 + k) + 1),m2) = ((Partial_Sums_in_cod2 Rseq) . (((n2 + k) + 1),m2)) + ((Partial_Sums Rseq) . ((n2 + k),m2)) by ThRS;
Partial_Sums_in_cod2 Rseq is nonnegative-yielding by a1, lm80;
then (Partial_Sums Rseq) . (((n2 + k) + 1),m2) >= (Partial_Sums Rseq) . ((n2 + k),m2) by b8, XREAL_1:31;
hence S1[k + 1] by a7, XXREAL_0:2; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(b5, b6);
then b9: (Partial_Sums Rseq) . (n1,m2) >= (Partial_Sums Rseq) . (n2,m2) by b3;
defpred S2[ Nat] means (Partial_Sums Rseq) . (n1,(m2 + $1)) >= (Partial_Sums Rseq) . (n1,m2);
b10: S2[ 0 ] ;
b11: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume b12: S2[k] ; :: thesis: S2[k + 1]
b13: (Partial_Sums Rseq) . (n1,((m2 + k) + 1)) = ((Partial_Sums_in_cod1 Rseq) . (n1,((m2 + k) + 1))) + ((Partial_Sums Rseq) . (n1,(m2 + k))) by DefCS;
Partial_Sums_in_cod1 Rseq is nonnegative-yielding by a1, lm80;
then (Partial_Sums Rseq) . (n1,((m2 + k) + 1)) >= (Partial_Sums Rseq) . (n1,(m2 + k)) by b13, XREAL_1:31;
hence S2[k + 1] by b12, XXREAL_0:2; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(b10, b11);
then (Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n1,m2) by b4;
hence (Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n2,m2) by b9, XXREAL_0:2; :: thesis: verum
end;
hence Partial_Sums Rseq is non-decreasing ; :: thesis: verum