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;
A2: 1 <= Sum (||.z.|| rExpSeq ) by Th28;
then 0 * (Sum (||.z.|| rExpSeq )) < 4 * (Sum (||.z.|| rExpSeq )) ;
then A3: 0 / (4 * (Sum (||.z.|| rExpSeq ))) < p / (4 * (Sum (||.z.|| rExpSeq ))) by A1;
A4: 1 <= Sum (||.w.|| rExpSeq ) by Th28;
then 0 * (Sum (||.w.|| rExpSeq )) < 4 * (Sum (||.w.|| rExpSeq )) ;
then A5: 0 / (4 * (Sum (||.w.|| rExpSeq ))) < p / (4 * (Sum (||.w.|| rExpSeq ))) by A1;
set p1 = min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))));
A6: min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) > 0 by A3, A5, XXREAL_0:15;
A7: ( min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) > 0 & min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) <= p / (4 * (Sum (||.z.|| rExpSeq ))) & min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) <= p / (4 * (Sum (||.w.|| rExpSeq ))) ) by A3, A5, XXREAL_0:15, XXREAL_0:17;
||.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
A8: 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 A6, COMSEQ_3:4;
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
A9: 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 A6, CSSPACE3:10;
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

A10: 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 A11: l <= k ; :: thesis: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).||
A12: ||.(((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;
A13: 0 <= ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by CLVECT_1:106;
||.((z ExpSeq ) . l).|| <= (||.z.|| rExpSeq ) . l by Th13;
then A14: ||.((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 A13, XREAL_1:66;
||.(Conj k,z,w).|| . l = ||.((Conj k,z,w) . l).|| by CLVECT_1:def 17
.= ||.(((z ExpSeq ) . l) * (((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l)))).|| by A11, Def7 ;
hence ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by A12, A14, 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;

A15: 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 ))) )
assume l <= k ; :: thesis: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq )))
then A16: ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by A10;
A17: ||.(((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).|| <= Sum (||.w.|| rExpSeq ) by Th27;
then A18: ||.((Partial_Sums (w ExpSeq )) . k).|| + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq )) + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| by XREAL_1:8;
||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| <= Sum (||.w.|| rExpSeq ) by Th27;
then (Sum (||.w.|| rExpSeq )) + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq )) + (Sum (||.w.|| rExpSeq )) by XREAL_1:8;
then ||.((Partial_Sums (w ExpSeq )) . k).|| + ||.((Partial_Sums (w ExpSeq )) . (k -' l)).|| <= 2 * (Sum (||.w.|| rExpSeq )) by A18, XXREAL_0:2;
then A19: ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| <= 2 * (Sum (||.w.|| rExpSeq )) by A17, XXREAL_0:2;
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 A19, XREAL_1:66;
hence ||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * (2 * (Sum (||.w.|| rExpSeq ))) by A16, 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

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 A22: n1 + n2 <= k by A20, XXREAL_0:2;
0 <= n2 by NAT_1:2;
then A23: n1 + 0 <= n1 + n2 by XREAL_1:8;
then A24: n1 <= k by A22, 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 A25: l <= n1 + n2 ; :: thesis: ||.(Conj k,z,w).|| . l <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * ((||.z.|| rExpSeq ) . l)
then A26: l <= k by A22, XXREAL_0:2;
A27: k -' l = k - l by A22, A25, XREAL_1:235, XXREAL_0:2;
0 <= n1 by NAT_1:2;
then A28: 0 + n2 <= n1 + n2 by XREAL_1:8;
A29: n4 - l <= k - l by A20, XREAL_1:11;
((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by A25, XREAL_1:12;
then n1 + n2 <= k - l by A29, XXREAL_0:2;
then A30: n2 <= k -' l by A27, A28, XXREAL_0:2;
0 <= n1 + n2 by NAT_1:2;
then 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:8;
then n2 <= n4 by A28, XXREAL_0:2;
then n2 <= k by A20, XXREAL_0:2;
then A31: ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| < min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A9, A30;
0 <= (||.z.|| rExpSeq ) . l by Th26;
then A32: ((||.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 A31, XREAL_1:66;
||.(Conj k,z,w).|| . l <= ((||.z.|| rExpSeq ) . l) * ||.(((Partial_Sums (w ExpSeq )) . k) - ((Partial_Sums (w ExpSeq )) . (k -' l))).|| by A10, A26;
hence ||.(Conj k,z,w).|| . l <= (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) * ((||.z.|| rExpSeq ) . l) by A32, XXREAL_0:2; :: thesis: verum

end;

then A33: (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;
(Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2) <= Sum (||.z.|| rExpSeq ) by Th27;
then ((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 A6, XREAL_1:66;
then A34: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) <= (Sum (||.z.|| rExpSeq )) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) by A33, XXREAL_0:2;
A35: (Sum (||.z.|| rExpSeq )) * (min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq ))))) <= (Sum (||.z.|| rExpSeq )) * (p / (4 * (Sum (||.z.|| rExpSeq )))) by A2, A7, XREAL_1:66;
A36: ( 0 <> Sum (||.z.|| rExpSeq ) & 4 <> 0 ) by Th28;
(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 A36, XCMPLX_1:92 ;
then A37: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) <= p / 4 by A34, A35, XXREAL_0:2;
( 0 < p / 4 & 0 < p / 2 ) by A1;
then 0 + (p / 4) < (p / 4) + (p / 4) by XREAL_1:8;
then A38: (Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2) < p / 2 by A37, XXREAL_0:2;
k -' (n1 + n2) = k - (n1 + n2) by A20, A21, XREAL_1:235, XXREAL_0:2;
then A39: k = (k -' (n1 + n2)) + (n1 + n2) ;
for l being Element of NAT st l <= k holds
||.(Conj k,z,w).|| . l <= (2 * (Sum (||.w.|| rExpSeq ))) * ((||.z.|| rExpSeq ) . l) by A15;
then A40: ((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, A39, COMSEQ_3:8;
abs (((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2))) <= min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A8, A23, A24;
then A41: ((Partial_Sums (||.z.|| rExpSeq )) . k) - ((Partial_Sums (||.z.|| rExpSeq )) . (n1 + n2)) <= min (pp / (4 * (Sum (||.z.|| rExpSeq )))),(pp / (4 * (Sum (||.w.|| rExpSeq )))) by A22, Th29;
A42: 0 * (Sum (||.w.|| rExpSeq )) < 2 * (Sum (||.w.|| rExpSeq )) by A4;
then (((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 A41, XREAL_1:66;
then A43: ((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 A40, XXREAL_0:2;
A44: (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 A7, A42, XREAL_1:66;
A45: ( 0 <> Sum (||.w.|| rExpSeq ) & 4 <> 0 ) by Th28;
(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 A45, XCMPLX_1:92
.= p / 2 ;
then ((Partial_Sums ||.(Conj k,z,w).||) . k) - ((Partial_Sums ||.(Conj k,z,w).||) . (n1 + n2)) <= p / 2 by A43, A44, 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 A38, 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