let w, z be Complex; 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; ( 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
; 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;
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); for k being Nat st n4 <= k holds
|.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p
A10:
now 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;
for l being Nat st l <= k holds
|.(Conj (k,z,w)).| . l <= ((|.z.| rExpSeq) . l) * (2 * (Sum (|.w.| rExpSeq)))now for l being Nat st l <= k holds
|.(Conj (k,z,w)).| . l <= ((|.z.| rExpSeq) . l) * (2 * (Sum (|.w.| rExpSeq)))let l be
Nat;
( l <= k implies |.(Conj (k,z,w)).| . l <= ((|.z.| rExpSeq) . l) * (2 * (Sum (|.w.| rExpSeq))) )assume
l <= k
;
|.(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;
verum end; hence
for
l being
Nat st
l <= k holds
|.(Conj (k,z,w)).| . l <= ((|.z.| rExpSeq) . l) * (2 * (Sum (|.w.| rExpSeq)))
;
verum end;
now for k being Nat st n4 <= k holds
|.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < plet k be
Nat;
( n4 <= k implies |.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p )assume A14:
n4 <= k
;
|.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < pA15:
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 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;
( 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
;
|.(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;
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;
verum end;
hence
for k being Nat st n4 <= k holds
|.((Partial_Sums |.(Conj (k,z,w)).|) . k).| < p
; verum