let X be Complex_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 (||.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 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 ExpSeq)) . m) - ((Partial_Sums (w ExpSeq)) . n)).|| < s by CLOPBAN3:4;
then Partial_Sums (w ExpSeq) is Cauchy_sequence_by_Norm by CLOPBAN3:5;
then consider n2 being Nat such that
A5: for k, l being 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: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
A6: 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 A4, 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
A7: now :: thesis: for n, k, l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).||
let n, k be Nat; :: thesis: for l being 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 :: thesis: for l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).||
let l be 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:38;
0 <= ||.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|| by CLVECT_1:105;
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:64;
||.(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, Def5 ;
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 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 :: thesis: for k, l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq)))
let k be Nat; :: thesis: for l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq)))
now :: thesis: for l being Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq)))
let l be 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:104;
||.((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:6;
||.((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:6;
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:64;
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 Nat st l <= k holds
||.(Conj (k,z,w)).|| . l <= ((||.z.|| rExpSeq) . l) * (2 * (Sum (||.w.|| rExpSeq))) ; :: thesis: verum
end;
now :: thesis: for k being Nat st n4 <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p
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:91
.= 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: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) )
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:10;
n4 - l <= k - l by A20, XREAL_1:9;
then A26: n1 + n2 <= k - l by A25, XXREAL_0:2;
A27: 0 + n2 <= n1 + n2 by XREAL_1:6;
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) <= (n1 + n2) + (n1 + n2) by XREAL_1:6;
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:233, 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:64;
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;
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 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:64;
for l being 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:6;
((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: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 A3, 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 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:64, 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:8;
hence |.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p by Th30; :: thesis: verum
end;
hence for k being Nat st n4 <= k holds
|.((Partial_Sums ||.(Conj (k,z,w)).||) . k).| < p ; :: thesis: verum