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 S₁[ Element of NAT ] means 0 <= ((Partial_Sums |.seq.|) . (n + $1)) - ((Partial_Sums |.seq.|) . n);

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[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:132;
assume S₁[k] ; :: thesis: S₁[k + 1]
hence S₁[k + 1] by A3, A4; :: thesis: verum

end;

A5: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A2); :: 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, 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
A8: m = n + k by NAT_1:10;
A9: 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 S₁[ Element of NAT ] means |.(((Partial_Sums seq) . (n + $1)) - ((Partial_Sums seq) . n)).| <= abs (((Partial_Sums |.seq.|) . (n + $1)) - ((Partial_Sums |.seq.|) . n));

A10: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[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)).| <= (abs (((Partial_Sums |.seq.|) . (n + k)) - ((Partial_Sums |.seq.|) . n))) + |.(seq . ((n + k) + 1)).| ) by COMPLEX1:142, XREAL_1:8;
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))).| ;
(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 S₁[k + 1] by A12, A11, XXREAL_0:2; :: thesis: verum

end;

A13: S₁[ 0 ] ;
thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A13, A10); :: thesis: verum

end;

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 A9, A8; :: 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 A14: |.(((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 A14, 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