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;

B3: z P_dt is absolutely_summable by Th61;
A4: z P_dt is summable by Th61, COMSEQ_3:64;
reconsider PS = Partial_Sums (z P_dt ) as convergent Complex_Sequence by A4;
A7: lim |.(Partial_Sums (z P_dt )).| = |.(lim (Partial_Sums (z P_dt ))).| by A4, COMSEQ_2:11;
lim |.(Partial_Sums (z P_dt )).| <= lim (Partial_Sums |.(z P_dt ).|) by A2, B3, SEQ_2:32;
hence |.(Sum (z P_dt )).| <= Sum |.(z P_dt ).| by A7, 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)
A9: |.(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 ;
(n + 2) ! > 0 by NEWTON:23;
then A10: |.(z P_dt ).| . n = |.(z #N (n + 1)).| / ((n + 2) ! ) by A9, Lm18
.= (|.z.| |^ (n + 1)) / ((n + 2) ! ) by Lm13 ;
A11: |.z.| * ((|.z.| GeoSeq ) . n) = |.z.| * (|.z.| |^ n) by PREPOWER:def 1
.= |.z.| |^ (n + 1) by NEWTON:11 ;
A12: (n + 2) ! >= 1 by Th42, NEWTON:18;
|.z.| |^ (n + 1) >= 0 by COMPLEX1:132, POWER:3;
then (|.z.| |^ (n + 1)) / 1 >= (|.z.| |^ (n + 1)) / ((n + 2) ! ) by A12, XREAL_1:120;
hence |.(z P_dt ).| . n <= |.z.| * ((|.z.| GeoSeq ) . n) by A10, A11; :: 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 A13: 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
A15: q = p / (p + 1) ;
p + 1 > p by XREAL_1:31;
then A16: q < 1 by A13, A15, XREAL_1:191;
A17: 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 A18: |.z.| < q ; :: thesis: |.(Sum (z P_dt )).| < p
then A19: |.z.| < 1 by A16, XXREAL_0:2;
abs |.z.| < 1 by A16, A18, XXREAL_0:2;
then A20: ( |.z.| GeoSeq is summable & Sum (|.z.| GeoSeq ) = 1 / (1 - |.z.|) ) by SERIES_1:28;
then A21: ( |.z.| (#) (|.z.| GeoSeq ) is summable & Sum (|.z.| (#) (|.z.| GeoSeq )) = |.z.| * (Sum (|.z.| GeoSeq )) ) by SERIES_1:13;
A22: 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 A23: ( |.(z P_dt ).| is summable & Sum |.(z P_dt ).| <= Sum (|.z.| (#) (|.z.| GeoSeq )) ) by A21, A22, SERIES_1:24;
A24: Sum (|.z.| (#) (|.z.| GeoSeq )) = |.z.| / (1 - |.z.|) by A20, SERIES_1:13;
|.z.| / (1 - |.z.|) < p

proof

A25: |.z.| * (p + 1) < (p / (p + 1)) * (p + 1) by A13, A15, A18, XREAL_1:70;
(p / (p + 1)) * (p + 1) = p by A13, XCMPLX_1:88;
then A26: ((p * |.z.|) + |.z.|) - (p * |.z.|) < p - (p * |.z.|) by A25, XREAL_1:11;
A27: 1 - |.z.| > 0 by A19, XREAL_1:52;
then |.z.| / (1 - |.z.|) < (p * (1 - |.z.|)) / (1 - |.z.|) by A26, XREAL_1:76;
hence |.z.| / (1 - |.z.|) < p by A27, XCMPLX_1:90; :: thesis: verum

end;

then ( Sum |.(z P_dt ).| < p & |.(Sum (z P_dt )).| <= Sum |.(z P_dt ).| ) by A1, A23, A24, XXREAL_0:2;
hence |.(Sum (z P_dt )).| < p by 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 A13, A15; :: 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 A17; :: thesis: verum