A1: for z being Complex holds |.(Sum (z P_dt)).| <= Sum |.(z P_dt).|

proof

let z be Complex; :: thesis: |.(Sum (z P_dt)).| <= Sum |.(z P_dt).|
A2: for k being Nat holds |.(Partial_Sums (z P_dt)).| . k <= (Partial_Sums |.(z P_dt).|) . k

proof

let k be Nat; :: thesis: |.(Partial_Sums (z P_dt)).| . k <= (Partial_Sums |.(z P_dt).|) . k
|.((Partial_Sums (z P_dt)) . k).| = |.(Partial_Sums (z P_dt)).| . k by VALUED_1:18;
hence |.(Partial_Sums (z P_dt)).| . k <= (Partial_Sums |.(z P_dt).|) . k by COMSEQ_3:30; :: thesis: verum

end;

A3: z P_dt is absolutely_summable by Th55;
A4: z P_dt is summable by Th55, COMSEQ_3:63;
A5: lim |.(Partial_Sums (z P_dt)).| = |.(lim (Partial_Sums (z P_dt))).| by A4, SEQ_2:27;
lim |.(Partial_Sums (z P_dt)).| <= lim (Partial_Sums |.(z P_dt).|) by A2, A3, SEQ_2:18;
hence |.(Sum (z P_dt)).| <= Sum |.(z P_dt).| by A5, SERIES_1:def 3; :: thesis: verum

end;

A6: for z being Complex
for n being Nat holds |.(z P_dt).| . n <= |.z.| * ((|.z.| GeoSeq) . n)

proof

let z be Complex; :: thesis: for n being Nat holds |.(z P_dt).| . n <= |.z.| * ((|.z.| GeoSeq) . n)
let n be Nat; :: thesis: |.(z P_dt).| . n <= |.z.| * ((|.z.| GeoSeq) . n)
|.(z P_dt).| . n = |.((z P_dt) . n).| by VALUED_1:18
.= |.((z |^ (n + 1)) / ((n + 2) !)).| by Def24
.= |.((z |^ (n + 1)) / ((n + 2) !)).| ;
then A7: |.(z P_dt).| . n = |.(z |^ (n + 1)).| / ((n + 2) !) by Lm13
.= (|.z.| |^ (n + 1)) / ((n + 2) !) by Lm8 ;
A8: |.z.| * ((|.z.| GeoSeq) . n) = |.z.| * (|.z.| |^ n) by PREPOWER:def 1
.= |.z.| |^ (n + 1) by NEWTON:6 ;
( (n + 2) ! >= 1 & |.z.| |^ (n + 1) >= 0 ) by Th38, COMPLEX1:46, NEWTON:12, POWER:3;
then (|.z.| |^ (n + 1)) / 1 >= (|.z.| |^ (n + 1)) / ((n + 2) !) by XREAL_1:118;
hence |.(z P_dt).| . n <= |.z.| * ((|.z.| GeoSeq) . n) by A7, A8; :: thesis: verum

end;

let p0 be Real; :: thesis: ( p0 > 0 implies ex q being Real st
( q > 0 & ( for z being Complex st |.z.| < q holds
|.(Sum (z P_dt)).| < p0 ) ) )
assume A9: p0 > 0 ; :: thesis: ex q being Real st
( q > 0 & ( for z being Complex st |.z.| < q holds
|.(Sum (z P_dt)).| < p0 ) )
reconsider p = p0 as Real ;
consider q being Real such that
A10: q = p / (p + 1) ;
p + 1 > p by XREAL_1:29;
then A11: q < 1 by A9, A10, XREAL_1:189;
A12: for z being Complex st |.z.| < q holds
|.(Sum (z P_dt)).| < p

proof

let z be Complex; :: thesis: ( |.z.| < q implies |.(Sum (z P_dt)).| < p )
assume A13: |.z.| < q ; :: thesis: |.(Sum (z P_dt)).| < p
then A14: |.z.| < 1 by A11, XXREAL_0:2;
A15: |.|.z.|.| < 1 by A11, A13, XXREAL_0:2;
then A16: |.z.| GeoSeq is summable by SERIES_1:24;
A17: Sum (|.z.| GeoSeq) = 1 / (1 - |.z.|) by A15, SERIES_1:24;
A18: |.z.| (#) (|.z.| GeoSeq) is summable by A16, SERIES_1:10;
A19: for n being Nat holds |.(z P_dt).| . n <= (|.z.| (#) (|.z.| GeoSeq)) . n

proof

let n be Nat; :: thesis: |.(z P_dt).| . n <= (|.z.| (#) (|.z.| GeoSeq)) . n
|.(z P_dt).| . n <= |.z.| * ((|.z.| GeoSeq) . n) by A6;
hence |.(z P_dt).| . n <= (|.z.| (#) (|.z.| GeoSeq)) . n by SEQ_1:9; :: thesis: verum

end;

for n being Nat holds 0 <= |.(z P_dt).| . n

proof

let n be Nat; :: thesis: 0 <= |.(z P_dt).| . n
|.(z P_dt).| . n = |.((z P_dt) . n).| by VALUED_1:18;
hence 0 <= |.(z P_dt).| . n by COMPLEX1:46; :: thesis: verum

end;

then A20: Sum |.(z P_dt).| <= Sum (|.z.| (#) (|.z.| GeoSeq)) by A18, A19, SERIES_1:20;
A21: Sum (|.z.| (#) (|.z.| GeoSeq)) = |.z.| / (1 - |.z.|) by A16, A17, SERIES_1:10;
A22: |.z.| * (p + 1) < (p / (p + 1)) * (p + 1) by A9, A10, A13, XREAL_1:68;
(p / (p + 1)) * (p + 1) = p by A9, XCMPLX_1:87;
then A23: ((p * |.z.|) + |.z.|) - (p * |.z.|) < p - (p * |.z.|) by A22, XREAL_1:9;
A24: 1 - |.z.| > 0 by A14, XREAL_1:50;
then |.z.| / (1 - |.z.|) < (p * (1 - |.z.|)) / (1 - |.z.|) by A23, XREAL_1:74;
then |.z.| / (1 - |.z.|) < p by A24, XCMPLX_1:89;
then A25: Sum |.(z P_dt).| < p by A20, A21, XXREAL_0:2;
|.(Sum (z P_dt)).| <= Sum |.(z P_dt).| by A1;
hence |.(Sum (z P_dt)).| < p by A25, XXREAL_0:2; :: thesis: verum

end;

take q ; :: thesis: ( q > 0 & ( for z being Complex st |.z.| < q holds
|.(Sum (z P_dt)).| < p0 ) )
thus q > 0 by A9, A10; :: thesis: for z being Complex st |.z.| < q holds
|.(Sum (z P_dt)).| < p0
let z be Complex; :: thesis: ( |.z.| < q implies |.(Sum (z P_dt)).| < p0 )
thus ( |.z.| < q implies |.(Sum (z P_dt)).| < p0 ) by A12; :: thesis: verum