let seq be Complex_Sequence; :: thesis: for m, n being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
let m, n be Element of NAT ; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
A1: for n, k being Element of NAT holds 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
proof
let n be Element of NAT ; :: thesis: for k being Element of NAT holds 0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
defpred S1[ Element of NAT ] means 0 <= ((Partial_Sums |.seq.|) . (n + $1)) - ((Partial_Sums |.seq.|) . n);
A2: S1[ 0 ] ;
A3: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
A5: ((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)).| ;
0 <= |.(seq . ((n + k) + 1)).| by COMPLEX1:132;
then 0 + 0 <= (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) + |.(seq . ((n + k) + 1)).| by A4;
hence S1[k + 1] by A5; :: thesis: verum
end;
thus for k being Element of NAT holds S1[k] from NAT_1:sch 1(A2, A3); :: thesis: verum
end;
A6: for n, k being Element of NAT holds abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
proof
let n, k be Element of NAT ; :: thesis: abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)
0 <= ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) by A1;
hence abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n)) = ((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n) by ABSVALUE:def 1; :: thesis: verum
end;
A7: for n, m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
proof
let n be Element of NAT ; :: thesis: for m being Element of NAT st n <= m holds
|.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
A8: for k being Element of NAT holds |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n))
proof
defpred S1[ Element of NAT ] means |.(((Partial_Sums seq) . (n + $1)) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . (n + $1)) - ((Partial_Sums |.seq.|) . n));
A9: S1[ 0 ] ;
A10: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; :: thesis: S1[k + 1]
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 Def7
.= |.((((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)) + (seq . ((n + k) + 1))).| ;
A13: |.((((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:142;
A14: |.(((Partial_Sums seq) . (n + k)) - ((Partial_Sums seq) . n)).| + |.(seq . ((n + k) + 1)).| <= (abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n))) + |.(seq . ((n + k) + 1)).| by A11, XREAL_1:8;
(abs (((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
.= abs (((Partial_Sums |.seq.|) . (n + (k + 1))) - ((Partial_Sums |.seq.|) . n)) by A6 ;
hence S1[k + 1] by A12, A13, A14, XXREAL_0:2; :: thesis: verum
end;
thus for k being Element of NAT holds S1[k] from NAT_1:sch 1(A9, A10); :: thesis: verum
end;
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) )
assume n <= m ; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
then consider k being Nat such that
A15: m = n + k by NAT_1:10;
k in NAT by ORDINAL1:def 13;
hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A8, A15; :: thesis: verum
end;
for n, m being Element of NAT holds |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
proof
let n, m be Element of NAT ; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
( m <= n implies |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) )
proof
assume m <= n ; :: thesis: |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n))
then A16: |.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . m)).| <= abs (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m)) by A7;
abs (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m)) = abs (- (((Partial_Sums |.seq.|) . n) - ((Partial_Sums |.seq.|) . m))) by COMPLEX1:138
.= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ;
hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A16, COMPLEX1:146; :: thesis: verum
end;
hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) by A7; :: thesis: verum
end;
hence |.(((Partial_Sums seq) . m) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . m) - ((Partial_Sums |.seq.|) . n)) ; :: thesis: verum