A1: for z being Element of COMPLEX holds |.(Sum (z P_dt )).| <= Sum |.(z P_dt ).|

proof

let z be Element of COMPLEX ; :: thesis: |.(Sum (z P_dt )).| <= Sum |.(z P_dt ).|
A2: for k being Element of NAT holds |.(Partial_Sums (z P_dt )).| . k <= (Partial_Sums |.(z P_dt ).|) . k

proof

let k be Element of 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;

A4: z P_dt is absolutely_summable by Th61;
A5: z P_dt is summable by Th61, COMSEQ_3:64;
then reconsider PS = Partial_Sums (z P_dt ) as convergent Complex_Sequence ;
A6: lim |.(Partial_Sums (z P_dt )).| = |.(lim (Partial_Sums (z P_dt ))).| by A5, COMSEQ_2:11;
lim |.(Partial_Sums (z P_dt )).| <= lim (Partial_Sums |.(z P_dt ).|) by A2, A4, SEQ_2:32;
hence |.(Sum (z P_dt )).| <= Sum |.(z P_dt ).| by A6, SERIES_1:def 3; :: thesis: verum

end;

A8: for z being Element of COMPLEX
for n being Element of NAT holds |.(z P_dt ).| . n <= |.z.| * ((|.z.| GeoSeq ) . n)

proof

let z be Element of COMPLEX ; :: thesis: for n being Element of NAT holds |.(z P_dt ).| . n <= |.z.| * ((|.z.| GeoSeq ) . n)
let n be Element of 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) !c )).| by Def28
.= |.((z |^ (n + 1)) / ((n + 2) ! )).| by Th37 ;
then A11: |.(z P_dt ).| . n = |.(z #N (n + 1)).| / ((n + 2) ! ) by Lm14
.= (|.z.| |^ (n + 1)) / ((n + 2) ! ) by Lm9 ;
A12: |.z.| * ((|.z.| GeoSeq ) . n) = |.z.| * (|.z.| |^ n) by PREPOWER:def 1
.= |.z.| |^ (n + 1) by NEWTON:11 ;
( (n + 2) ! >= 1 & |.z.| |^ (n + 1) >= 0 ) by Th42, COMPLEX1:132, NEWTON:18, POWER:3;
then (|.z.| |^ (n + 1)) / 1 >= (|.z.| |^ (n + 1)) / ((n + 2) ! ) by XREAL_1:120;
hence |.(z P_dt ).| . n <= |.z.| * ((|.z.| GeoSeq ) . n) by A11, A12; :: thesis: verum

end;

let p0 be real number ; :: thesis: ( p0 > 0 implies ex q being Real st
( q > 0 & ( for z being complex number st |.z.| < q holds
|.(Sum (z P_dt )).| < p0 ) ) )
assume A15: p0 > 0 ; :: thesis: ex q being Real st
( q > 0 & ( for z being complex number st |.z.| < q holds
|.(Sum (z P_dt )).| < p0 ) )
reconsider p = p0 as Real by XREAL_0:def 1;
consider q being Real such that
A16: q = p / (p + 1) ;
p + 1 > p by XREAL_1:31;
then A18: q < 1 by A15, A16, XREAL_1:191;
A19: for z being Element of COMPLEX st |.z.| < q holds
|.(Sum (z P_dt )).| < p

proof

let z be Element of COMPLEX ; :: thesis: ( |.z.| < q implies |.(Sum (z P_dt )).| < p )
assume A20: |.z.| < q ; :: thesis: |.(Sum (z P_dt )).| < p
then A21: |.z.| < 1 by A18, XXREAL_0:2;
A22: abs |.z.| < 1 by A18, A20, XXREAL_0:2;
then A23: |.z.| GeoSeq is summable by SERIES_1:28;
A24: Sum (|.z.| GeoSeq ) = 1 / (1 - |.z.|) by A22, SERIES_1:28;
A25: |.z.| (#) (|.z.| GeoSeq ) is summable by A23, SERIES_1:13;
A26: for n being Element of NAT holds |.(z P_dt ).| . n <= (|.z.| (#) (|.z.| GeoSeq )) . n

proof

let n be Element of NAT ; :: thesis: |.(z P_dt ).| . n <= (|.z.| (#) (|.z.| GeoSeq )) . n
|.(z P_dt ).| . n <= |.z.| * ((|.z.| GeoSeq ) . n) by A8;
hence |.(z P_dt ).| . n <= (|.z.| (#) (|.z.| GeoSeq )) . n by SEQ_1:13; :: thesis: verum

end;

for n being Element of NAT holds 0 <= |.(z P_dt ).| . n

proof

let n be Element of 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:132; :: thesis: verum

end;

then A30: Sum |.(z P_dt ).| <= Sum (|.z.| (#) (|.z.| GeoSeq )) by A25, A26, SERIES_1:24;
A31: Sum (|.z.| (#) (|.z.| GeoSeq )) = |.z.| / (1 - |.z.|) by A23, A24, SERIES_1:13;
A32: |.z.| * (p + 1) < (p / (p + 1)) * (p + 1) by A15, A16, A20, XREAL_1:70;
(p / (p + 1)) * (p + 1) = p by A15, XCMPLX_1:88;
then A34: ((p * |.z.|) + |.z.|) - (p * |.z.|) < p - (p * |.z.|) by A32, XREAL_1:11;
A35: 1 - |.z.| > 0 by A21, XREAL_1:52;
then |.z.| / (1 - |.z.|) < (p * (1 - |.z.|)) / (1 - |.z.|) by A34, XREAL_1:76;
then |.z.| / (1 - |.z.|) < p by A35, XCMPLX_1:90;
then A38: Sum |.(z P_dt ).| < p by A30, A31, XXREAL_0:2;
|.(Sum (z P_dt )).| <= Sum |.(z P_dt ).| by A1;
hence |.(Sum (z P_dt )).| < p by A38, XXREAL_0:2; :: thesis: verum

end;

take q ; :: thesis: ( q > 0 & ( for z being complex number st |.z.| < q holds
|.(Sum (z P_dt )).| < p0 ) )
thus q > 0 by A15, A16; :: thesis: for z being complex number st |.z.| < q holds
|.(Sum (z P_dt )).| < p0
let z be complex number ; :: thesis: ( |.z.| < q implies |.(Sum (z P_dt )).| < p0 )
z in COMPLEX by XCMPLX_0:def 2;
hence ( |.z.| < q implies |.(Sum (z P_dt )).| < p0 ) by A19; :: thesis: verum