let w, z be Complex; :: 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 ;
A2: 1 <= Sum (|.z.| rExpSeq) by Th17;
A3: 0 < Sum (|.w.| rExpSeq) by Th17;
set p1 = min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))));
A4: min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) > 0 by A1, A2, A3, XXREAL_0:15;
now :: thesis: for k being object st k in NAT holds
|.(z ExpSeq).| . k = (|.z.| rExpSeq) . k
let k be object ; :: thesis: ( k in NAT implies |.(z ExpSeq).| . k = (|.z.| rExpSeq) . k )
assume A5: k in NAT ; :: thesis: |.(z ExpSeq).| . k = (|.z.| rExpSeq) . k
thus |.(z ExpSeq).| . k = |.((z ExpSeq) . k).| by VALUED_1:18
.= (|.z.| rExpSeq) . k by A5, Th3 ; :: thesis: verum
end;
then |.(z ExpSeq).| = |.z.| rExpSeq ;
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;
consider n2 being Nat such that
A7: 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, COMSEQ_3:47;
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 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 A9: l <= k ; :: thesis: |.(Conj (k,z,w)).| . l = ((|.z.| rExpSeq) . l) * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).|
thus |.(Conj (k,z,w)).| . l = |.((Conj (k,z,w)) . l).| by VALUED_1:18
.= |.(((z ExpSeq) . l) * (((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l)))).| by A9, Def13
.= |.((z ExpSeq) . l).| * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| by COMPLEX1:65
.= ((|.z.| rExpSeq) . l) * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| by Th3 ; :: 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;
A10: 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))) )
assume l <= k ; :: thesis: |.(Conj (k,z,w)).| . l <= ((|.z.| rExpSeq) . l) * (2 * (Sum (|.w.| rExpSeq)))
then A11: |.(Conj (k,z,w)).| . l = ((|.z.| rExpSeq) . l) * |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| by A8;
|.((Partial_Sums (w ExpSeq)) . k).| <= Sum (|.w.| rExpSeq) by Th16;
then A12: |.((Partial_Sums (w ExpSeq)) . k).| + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| <= (Sum (|.w.| rExpSeq)) + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| by XREAL_1:6;
|.((Partial_Sums (w ExpSeq)) . (k -' l)).| <= Sum (|.w.| rExpSeq) by Th16;
then (Sum (|.w.| rExpSeq)) + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| <= (Sum (|.w.| rExpSeq)) + (Sum (|.w.| rExpSeq)) by XREAL_1:6;
then ( |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| <= |.((Partial_Sums (w ExpSeq)) . k).| + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| & |.((Partial_Sums (w ExpSeq)) . k).| + |.((Partial_Sums (w ExpSeq)) . (k -' l)).| <= 2 * (Sum (|.w.| rExpSeq)) ) by A12, COMPLEX1:57, XXREAL_0:2;
then A13: |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| <= 2 * (Sum (|.w.| rExpSeq)) by XXREAL_0:2;
0 <= (|.z.| rExpSeq) . l by Th18;
hence |.(Conj (k,z,w)).| . l <= ((|.z.| rExpSeq) . l) * (2 * (Sum (|.w.| rExpSeq))) by A11, A13, XREAL_1:64; :: 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
let k be Nat; :: thesis: ( n4 <= k implies |.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p )
assume A14: n4 <= k ; :: thesis: |.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p
A15: 0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:6;
then A16: n1 + n2 <= k by A14, XXREAL_0:2;
A17: n1 + 0 <= n1 + n2 by XREAL_1:6;
then A18: n1 <= k by A16, 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 A19: l <= n1 + n2 ; :: thesis: |.(Conj (k,z,w)).| . l <= (min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))))) * ((|.z.| rExpSeq) . l)
then A20: k -' l = k - l by A16, XREAL_1:233, XXREAL_0:2;
A21: 0 + n2 <= n1 + n2 by XREAL_1:6;
A22: n4 - l <= k - l by A14, XREAL_1:9;
((n1 + n2) + (n1 + n2)) - (n1 + n2) <= ((n1 + n2) + (n1 + n2)) - l by A19, XREAL_1:10;
then n1 + n2 <= k - l by A22, XXREAL_0:2;
then A23: n2 <= k -' l by A20, A21, XXREAL_0:2;
0 + (n1 + n2) <= (n1 + n2) + (n1 + n2) by XREAL_1:6;
then n2 <= n4 by A21, XXREAL_0:2;
then n2 <= k by A14, XXREAL_0:2;
then A24: |.(((Partial_Sums (w ExpSeq)) . k) - ((Partial_Sums (w ExpSeq)) . (k -' l))).| < min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) by A7, A23;
0 <= (|.z.| rExpSeq) . l by Th18;
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 A24, XREAL_1:64;
hence |.(Conj (k,z,w)).| . l <= (min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))))) * ((|.z.| rExpSeq) . l) by A8, A16, A19, XXREAL_0:2; :: thesis: verum
end;
then A25: (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)) * (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, Th16, XREAL_1:64;
then A26: (Partial_Sums |.(Conj (k,z,w)).|) . (n1 + n2) <= (Sum (|.z.| rExpSeq)) * (min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq)))))) by A25, XXREAL_0:2;
A27: (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;
A28: 0 <> Sum (|.z.| rExpSeq) by Th17;
(Sum (|.z.| rExpSeq)) * (p / (4 * (Sum (|.z.| rExpSeq)))) = ((Sum (|.z.| rExpSeq)) * p) / (4 * (Sum (|.z.| rExpSeq)))
.= p / 4 by A28, XCMPLX_1:91 ;
then A29: (Partial_Sums |.(Conj (k,z,w)).|) . (n1 + n2) <= p / 4 by A26, A27, XXREAL_0:2;
0 + (p / 4) < (p / 4) + (p / 4) by A1, XREAL_1:6;
then A30: (Partial_Sums |.(Conj (k,z,w)).|) . (n1 + n2) < p / 2 by A29, XXREAL_0:2;
k -' (n1 + n2) = k - (n1 + n2) by A14, A15, XREAL_1:233, XXREAL_0:2;
then A31: k = (k -' (n1 + n2)) + (n1 + n2) ;
for l being Nat st l <= k holds
|.(Conj (k,z,w)).| . l <= (2 * (Sum (|.w.| rExpSeq))) * ((|.z.| rExpSeq) . l) by A10;
then A32: ((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 A31, COMSEQ_3:8;
|.(((Partial_Sums (|.z.| rExpSeq)) . k) - ((Partial_Sums (|.z.| rExpSeq)) . (n1 + n2))).| <= min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) by A6, A17, A18;
then ((Partial_Sums (|.z.| rExpSeq)) . k) - ((Partial_Sums (|.z.| rExpSeq)) . (n1 + n2)) <= min ((pp / (4 * (Sum (|.z.| rExpSeq)))),(pp / (4 * (Sum (|.w.| rExpSeq))))) by A14, A15, Th19, XXREAL_0:2;
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 A3, XREAL_1:64;
then A33: ((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 A32, XXREAL_0:2;
A34: (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 A3, XREAL_1:64, XXREAL_0:17;
A35: 0 <> Sum (|.w.| rExpSeq) by Th17;
(2 * (Sum (|.w.| rExpSeq))) * (p / (4 * (Sum (|.w.| rExpSeq)))) = ((2 * p) * (Sum (|.w.| rExpSeq))) / (4 * (Sum (|.w.| rExpSeq)))
.= (p + 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 A33, A34, 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 A30, XREAL_1:8;
hence |.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p by Th20; :: thesis: verum
end;
hence for k being Nat st n4 <= k holds
|.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p ; :: thesis: verum