let X be Complex_Banach_Algebra; :: thesis: for z, w being Element of X
for p being real number st p > 0 holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
let z, w be Element of X; :: thesis: for p being real number st p > 0 holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
let p be real number ; :: thesis: ( p > 0 implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p )
assume A1: p > 0 ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
reconsider pp = p as Real by XREAL_0:def 1;
set p1 = min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))));
A2: 1 <= Sum (||.w.|| rExpSeq ) by Th28;
A3: 1 <= Sum (||.z.|| rExpSeq ) by Th28;
then A4: min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) > 0 by A1, A2, XXREAL_0:15;
Partial_Sums (w ExpSeq ) is convergent by CLOPBAN3:def 2;
then for s being Real st 0 < s holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((Partial_Sums (w ExpSeq )) . m) - ((Partial_Sums (w ExpSeq )) . n)).|| < s by CLOPBAN3:4;
then Partial_Sums (w ExpSeq ) is CCauchy by CLOPBAN3:5;
then consider n2 being Element of NAT such that
A5: for k, l being Element of NAT st n2 <= k & n2 <= l holds
||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . l)).|| < min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A4, CSSPACE3:10;
||.z.|| rExpSeq is summable by SIN_COS:49;
then Partial_Sums (||.z.|| rExpSeq ) is convergent by SERIES_1:def 2;
then consider n1 being Element of NAT such that
A6: for k, l being Element of NAT st n1 <= k & n1 <= l holds
abs (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . l)) < min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A4, COMSEQ_3:4;
set n3 = n1 + n2;
take n4 = (n1 + n2) + (n1 + n2); :: thesis: for k being Element of NAT st n4 <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p

A7: now

let n, k be Element of NAT ; :: thesis: for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).||

now

let l be Element of NAT ; :: thesis: ( l <= k implies ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| )
assume A8: l <= k ; :: thesis: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).||
A9: ||.(((z ExpSeq ) . l) * (((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l)))).|| <= ||.((z ExpSeq ) . l).|| * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by CLOPBAN3:42;
0 <= ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by CLVECT_1:106;
then A10: ||.((z ExpSeq ) . l).|| * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by Th13, XREAL_1:66;
||.(Conj k,z,w).|| . l = ||.((Conj k,z,w) . l).|| by NORMSP_0:def 4
.= ||.(((z ExpSeq ) . l) * (((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l)))).|| by A8, Def7 ;
hence ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by A9, A10, XXREAL_0:2; :: thesis: verum

end;

hence for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| ; :: thesis: verum

end;

A11: now

let k be Element of NAT ; :: thesis: for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq )))

now

let l be Element of NAT ; :: thesis: ( l <= k implies ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) )
A12: ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| <= ||.((Partial_Sums (w ExpSeq )) . k).|| + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| by CLVECT_1:105;
||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| <= Sum (||.w.|| rExpSeq ) by Th27;
then A13: (Sum (||.w.|| rExpSeq )) + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq )) + (Sum (||.w.|| rExpSeq )) by XREAL_1:8;
||.((Partial_Sums (w ExpSeq )) . k).|| <= Sum (||.w.|| rExpSeq ) by Th27;
then ||.((Partial_Sums (w ExpSeq )) . k).|| + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq )) + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| by XREAL_1:8;
then ||.((Partial_Sums (w ExpSeq )) . k).|| + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| <= 2 * (Sum (||.w.|| rExpSeq )) by A13, XXREAL_0:2;
then A14: ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| <= 2 * (Sum (||.w.|| rExpSeq )) by A12, XXREAL_0:2;
assume l <= k ; :: thesis: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq )))
then A15: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by A7;
0 <= (||.z.|| rExpSeq ) . l by Th26;
then ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) by A14, XREAL_1:66;
hence ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) by A15, XXREAL_0:2; :: thesis: verum

end;

hence for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) ; :: thesis: verum

end;

now

A16: 0 <> Sum (||.w.|| rExpSeq ) by Th28;
A17: (2 * (Sum (||.w.|| rExpSeq ))) * (p / (4 * (Sum (||.w.|| rExpSeq )))) = (2 * (Sum (||.w.|| rExpSeq ))) * (p * ((4 * (Sum (||.w.|| rExpSeq ))) " )) by XCMPLX_0:def 9
.= ((2 * (Sum (||.w.|| rExpSeq ))) * p) * ((4 * (Sum (||.w.|| rExpSeq ))) " )
.= ((2 * p) * (Sum (||.w.|| rExpSeq ))) / (4 * (Sum (||.w.|| rExpSeq ))) by XCMPLX_0:def 9
.= (2 * p) / 4 by A16, XCMPLX_1:92
.= p / 2 ;
A18: 0 <> Sum (||.z.|| rExpSeq ) by Th28;
A19: (Sum (||.z.|| rExpSeq )) * (p / (4 * (Sum (||.z.|| rExpSeq )))) = (Sum (||.z.|| rExpSeq )) * (p * ((4 * (Sum (||.z.|| rExpSeq ))) " )) by XCMPLX_0:def 9
.= ((Sum (||.z.|| rExpSeq )) * p) * ((4 * (Sum (||.z.|| rExpSeq ))) " )
.= ((Sum (||.z.|| rExpSeq )) * p) / (4 * (Sum (||.z.|| rExpSeq ))) by XCMPLX_0:def 9
.= p / 4 by A18, XCMPLX_1:92 ;
let k be Element of NAT ; :: thesis: ( n4 <= k implies abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p )
assume A20: n4 <= k ; :: thesis: abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p
0 <= n1 + n2 by NAT_1:2;
then A21: 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:8;
then k -' (n1 + n2) = k - (n1 + n2) by A20, XREAL_1:235, XXREAL_0:2;
then A22: k = (k -' (n1 + n2)) + (n1 + n2) ;
A23: n1 + n2 <= k by A20, A21, XXREAL_0:2;

now

let l be Element of NAT ; :: thesis: ( l <= n1 + n2 implies ||.(Conj k,z,w).|| . l <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * ((||.z.|| rExpSeq ) . l) )
assume A24: l <= n1 + n2 ; :: thesis: ||.(Conj k,z,w).|| . l <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * ((||.z.|| rExpSeq ) . l)
then A25: ((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by XREAL_1:12;
n4 - l <= k - l by A20, XREAL_1:11;
then A26: n1 + n2 <= k - l by A25, XXREAL_0:2;
0 <= n1 by NAT_1:2;
then A27: 0 + n2 <= n1 + n2 by XREAL_1:8;
l <= k by A23, A24, XXREAL_0:2;
then A28: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by A7;
A29: 0 <= (||.z.|| rExpSeq ) . l by Th26;
0 <= n1 + n2 by NAT_1:2;
then 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:8;
then n2 <= n4 by A27, XXREAL_0:2;
then A30: n2 <= k by A20, XXREAL_0:2;
k -' l = k - l by A23, A24, XREAL_1:235, XXREAL_0:2;
then n2 <= k -' l by A27, A26, XXREAL_0:2;
then ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| < min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A5, A30;
then ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| <= ((||.z.|| rExpSeq ) . l) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by A29, XREAL_1:66;
hence ||.(Conj k,z,w).|| . l <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * ((||.z.|| rExpSeq ) . l) by A28, XXREAL_0:2; :: thesis: verum

end;

then A31: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) <= ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2)) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by COMSEQ_3:7;
0 <= n2 by NAT_1:2;
then A32: n1 + 0 <= n1 + n2 by XREAL_1:8;
then n1 <= k by A23, XXREAL_0:2;
then abs (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2))) <= min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A6, A32;
then ((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2)) <= min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A20, A21, Th29, XXREAL_0:2;
then A33: (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq ))) <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * (2 * (Sum (||.w.|| rExpSeq ))) by A2, XREAL_1:66;
for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= (2 * (Sum (||.w.|| rExpSeq ))) * ((||.z.|| rExpSeq ) . l) by A11;
then ((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) <= (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2))) * (2 * (Sum (||.w.|| rExpSeq ))) by A22, COMSEQ_3:8;
then A34: ((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * (2 * (Sum (||.w.|| rExpSeq ))) by A33, XXREAL_0:2;
A35: 0 + (p / 4) < (p / 4) + (p / 4) by A1, XREAL_1:8;
((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2)) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) <= (Sum (||.z.|| rExpSeq )) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by A4, Th27, XREAL_1:66;
then A36: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) <= (Sum (||.z.|| rExpSeq )) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by A31, XXREAL_0:2;
(Sum (||.z.|| rExpSeq )) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) <= (Sum (||.z.|| rExpSeq )) * (p / (4 * (Sum (||.z.|| rExpSeq )))) by A3, XREAL_1:66, XXREAL_0:17;
then (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) <= p / 4 by A36, A19, XXREAL_0:2;
then A37: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) < p / 2 by A35, XXREAL_0:2;
(2 * (Sum (||.w.|| rExpSeq ))) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) <= (2 * (Sum (||.w.|| rExpSeq ))) * (p / (4 * (Sum (||.w.|| rExpSeq )))) by A2, XREAL_1:66, XXREAL_0:17;
then ((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) <= p / 2 by A34, A17, XXREAL_0:2;
then (((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2))) + ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) < (p / 2) + (p / 2) by A37, XREAL_1:10;
hence abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p by Th30; :: thesis: verum

end;

hence for k being Element of NAT st n4 <= k holds
abs ((Partial_Sums ||.(Conj k,z,w).||) . k) < p ; :: thesis: verum