let seq be Complex_Sequence; :: thesis: for n, m being Nat holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|
let n, m be Nat; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|
A1: for n, k being Nat holds 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
proof
let n be Nat; :: thesis: for k being Nat holds 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
defpred S1[ Nat] means 0 <= ((Partial_Sums |.seq.|) . (n + $1)) - ((Partial_Sums |.seq.|) . n);
A2: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A3: ((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n) = (((Partial_Sums |.seq.|) . (n + k)) + (|.seq.| . ((n + k) + 1))) - ((Partial_Sums |.seq.|) . n) by SERIES_1:def 1
.= (((Partial_Sums |.seq.|) . (n + k)) + |.(seq . ((n + k) + 1)).|) - ((Partial_Sums |.seq.|) . n) by VALUED_1:18
.= (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).| ;
A4: 0 <= |.(seq . ((n + k) + 1)).| by COMPLEX1:46;
assume S1[k] ; :: thesis: S1[k + 1]
hence S1[k + 1] by A3, A4; :: thesis: verum
end;
A5: S1[ 0 ] ;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A5, A2); :: thesis: verum
end;
A6: for n, k being Nat holds |.(((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)).| = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) by A1, ABSVALUE:def 1;
A7: for n, m being Nat st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|
proof
let n, m be Nat; :: thesis: ( n <= m implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| )
assume n <= m ; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|
then consider k being Nat such that
A8: m = n + k by NAT_1:10;
A9: for k being Nat holds |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)).|
proof
defpred S1[ Nat] means |.(((Partial_Sums seq) . (n + $1)) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . (n + $1)) - ((Partial_Sums |.seq.|) . n)).|;
A10: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then A11: ( |.((((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).| <= |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).| & |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).| <= |.(((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)).| + |.(seq . ((n + k) + 1)).| ) by COMPLEX1:56, XREAL_1:6;
A12: |.(((Partial_Sums seq) . (n + (k + 1))) - ((Partial_Sums seq) . n)).| = |.((((Partial_Sums seq) . (n + k)) + (seq . ((n + k) + 1))) - ((Partial_Sums seq) . n)).| by SERIES_1:def 1
.= |.((((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).| ;
|.(((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)).| + |.(seq . ((n + k) + 1)).| = (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).| by A6
.= (((Partial_Sums |.seq.|) . (n + k)) + |.(seq . ((n + k) + 1)).|) - ((Partial_Sums |.seq.|) . n)
.= (((Partial_Sums |.seq.|) . (n + k)) + (|.seq.| . ((n + k) + 1))) - ((Partial_Sums |.seq.|) . n) by VALUED_1:18
.= ((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n) by SERIES_1:def 1
.= |.(((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n)).| by A6 ;
hence S1[k + 1] by A12, A11, XXREAL_0:2; :: thesis: verum
end;
A13: S1[ 0 ] ;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A13, A10); :: thesis: verum
end;
thus |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| by A9, A8; :: thesis: verum
end;
for n, m being Nat holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|
proof
let n, m be Nat; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|
( m <= n implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| )
proof
assume m <= n ; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).|
then A14: |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= |.(((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m)).| by A7;
|.(((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m)).| = |.(- (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m))).| by COMPLEX1:52
.= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| ;
hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| by A14, COMPLEX1:60; :: thesis: verum
end;
hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| by A7; :: thesis: verum
end;
hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= |.(((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)).| ; :: thesis: verum