let X be Banach_Algebra; :: thesis: for w, z being Element of X
for p being Real st p > 0 holds
ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
let w, z be Element of X; :: thesis: for p being Real st p > 0 holds
ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
let p be Real; :: thesis: ( p > 0 implies ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p )
assume A1: p > 0 ; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
reconsider pp = p as Real ;
set p1 = min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))));
A2: 1 <= Sum (||.z.|| rExpSeq) by Th29;
then 0 * (Sum (||.z.|| rExpSeq)) < 4 * (Sum (||.z.|| rExpSeq)) by XREAL_1:68;
then A3: 0 / (4 * (Sum (||.z.|| rExpSeq))) < p / (4 * (Sum (||.z.|| rExpSeq))) by A1, XREAL_1:74;
A4: 1 <= Sum (||.w.|| rExpSeq) by Th29;
then 0 * (Sum (||.w.|| rExpSeq)) < 4 * (Sum (||.w.|| rExpSeq)) by XREAL_1:68;
then 0 / (4 * (Sum (||.w.|| rExpSeq))) < p / (4 * (Sum (||.w.|| rExpSeq))) by A1, XREAL_1:74;
then A5: min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) > 0 by A3, XXREAL_0:15;
Partial_Sums (w rExpSeq) is convergent by LOPBAN_3:def 1;
then for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.(((Partial_Sums (w rExpSeq)) . m) - ((Partial_Sums (w rExpSeq)) . n)).|| < s by LOPBAN_3:4;
then Partial_Sums (w rExpSeq) is Cauchy_sequence_by_Norm by LOPBAN_3:5;
then consider n2 being Nat such that
A6: for k, l being Nat st n2 <= k & n2 <= l holds
||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . l)).|| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A5, RSSPACE3:8;
||.z.|| rExpSeq is summable by SIN_COS:45;
then Partial_Sums (||.z.|| rExpSeq) is convergent by SERIES_1:def 2;
then consider n1 being Nat such that
A7: for k, l being Nat st n1 <= k & n1 <= l holds
|.(((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . l)).| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A5, COMSEQ_3:4;
set n3 = n1 + n2;
take n4 = (n1 + n2) + (n1 + n2); :: thesis: for k being Nat st n4 <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p

A8: now :: thesis: for n, k, l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||

let n, k, l be Nat; :: thesis: ( l <= k implies ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| )
assume A9: l <= k ; :: thesis: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).||
A10: ||.(((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l)))).|| <= ||.((z rExpSeq) . l).|| * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by LOPBAN_3:38;
0 <= ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by NORMSP_1:4;
then A11: ||.((z rExpSeq) . l).|| * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by Th14, XREAL_1:64;
||.(Conj (k,z,w)).|| . l = ||.((Conj (k,z,w)) . l).|| by NORMSP_0:def 4
.= ||.(((z rExpSeq) . l) * (((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l)))).|| by A9, Def9 ;
hence ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by A10, A11, XXREAL_0:2; :: thesis: verum

end;

A12: now :: thesis: for k, l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq)))

let k, l be Nat; :: thesis: ( l <= k implies ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) )
A13: ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| by NORMSP_1:3;
||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= Sum (||.w.|| rExpSeq) by Th28;
then A14: (Sum (||.w.|| rExpSeq)) + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq)) + (Sum (||.w.|| rExpSeq)) by XREAL_1:6;
||.((Partial_Sums (w rExpSeq)) . k).|| <= Sum (||.w.|| rExpSeq) by Th28;
then ||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= (Sum (||.w.|| rExpSeq)) + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| by XREAL_1:6;
then ||.((Partial_Sums (w rExpSeq)) . k).|| + ||.((Partial_Sums (w rExpSeq)) . (k -' l)).|| <= 2 * (Sum (||.w.|| rExpSeq)) by A14, XXREAL_0:2;
then A15: ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= 2 * (Sum (||.w.|| rExpSeq)) by A13, XXREAL_0:2;
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 rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by A8;
0 <= (||.z.|| rExpSeq) . l by Th27;
then ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) by A15, XREAL_1:64;
hence ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) by A16, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: for k being Nat st n4 <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p

0 < p / 4 by A1, XREAL_1:224;
then A17: 0 + (p / 4) < (p / 4) + (p / 4) by XREAL_1:6;
A18: 0 <> Sum (||.z.|| rExpSeq) by Th29;
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:91 ;
let k be Nat; :: thesis: ( n4 <= k implies |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p )
assume A20: n4 <= k ; :: thesis: |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
A21: 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:6;
then k -' (n1 + n2) = k - (n1 + n2) by A20, XREAL_1:233, XXREAL_0:2;
then A22: k = (k -' (n1 + n2)) + (n1 + n2) ;
A23: n1 + n2 <= k by A20, A21, XXREAL_0:2;

now :: thesis: for l being Nat st l <= n1 + n2 holds
||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l)

let l be 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) )
A24: 0 + n2 <= n1 + n2 by XREAL_1:6;
0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:6;
then n2 <= n4 by A24, XXREAL_0:2;
then A25: n2 <= k by A20, XXREAL_0:2;
A26: 0 <= (||.z.|| rExpSeq) . l by Th27;
assume A27: l <= n1 + n2 ; :: thesis: ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l)
then A28: ((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by XREAL_1:10;
l <= k by A23, A27, XXREAL_0:2;
then A29: ||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| by A8;
n4 - l <= k - l by A20, XREAL_1:9;
then A30: n1 + n2 <= k - l by A28, XXREAL_0:2;
k -' l = k - l by A23, A27, XREAL_1:233, XXREAL_0:2;
then n2 <= k -' l by A24, A30, XXREAL_0:2;
then ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| < min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A6, A25;
then ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w rExpSeq)) . k) - ((Partial_Sums (w rExpSeq)) . (k -' l))).|| <= ((||.z.|| rExpSeq) . l) * (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) by A26, XREAL_1:64;
hence ||.(Conj (k,z,w)).|| . l <= (min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq)))))) * ((||.z.|| rExpSeq) . l) by A29, 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;
A32: n1 + 0 <= n1 + n2 by XREAL_1:6;
then n1 <= k by A23, XXREAL_0:2;
then |.(((Partial_Sums (||.z.|| rExpSeq)) . k) - ((Partial_Sums (||.z.|| rExpSeq)) . (n1 + n2))).| <= min ((pp / (4 * (Sum (||.z.|| rExpSeq)))),(pp / (4 * (Sum (||.w.|| rExpSeq))))) by A7, 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, Th30, 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 A4, XREAL_1:64;
for l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= (2 * (Sum (||.w.|| rExpSeq))) * ((||.z.|| rExpSeq) . l) by A12;
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 <> Sum (||.w.|| rExpSeq) by Th29;
((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 A5, Th28, XREAL_1:64;
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 A2, XREAL_1:64, 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 A17, XXREAL_0:2;
0 * (Sum (||.w.|| rExpSeq)) < 2 * (Sum (||.w.|| rExpSeq)) by A4, XREAL_1:68;
then A38: (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 XREAL_1:64, XXREAL_0:17;
(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 A35, XCMPLX_1:91
.= p / 2 ;
then ((Partial_Sums ||.(Conj (k,z,w)).||) . k) - ((Partial_Sums ||.(Conj (k,z,w)).||) . (n1 + n2)) <= p / 2 by A34, A38, 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:8;
hence |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p by Th31; :: thesis: verum

end;

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