let z be complex number ; :: thesis: z P_dt is absolutely_summable
Partial_Sums |.(z P_dt ).| is bounded_above

proof

ex r being Real st
for n being Element of NAT holds (Partial_Sums |.(z P_dt ).|) . n < r

proof

A1: for n being Element of NAT holds (Partial_Sums |.(z P_dt ).|) . n < (Partial_Sums |.(z ExpSeq ).|) . (n + 1)

proof

let n be Element of NAT ; :: thesis: (Partial_Sums |.(z P_dt ).|) . n < (Partial_Sums |.(z ExpSeq ).|) . (n + 1)
(Partial_Sums |.(z P_dt ).|) . 0 = |.(z P_dt ).| . 0 by SERIES_1:def 1
.= |.((z P_dt ) . 0 ).| by VALUED_1:18
.= |.((z |^ (0 + 1)) / ((0 + 2) !c )).| by Def28
.= |.(z / (2 !c )).| by NEWTON:10
.= |.(z / 2).| by Th37, NEWTON:20 ;
then A2: (Partial_Sums |.(z P_dt ).|) . 0 = |.z.| / 2 by Lm18;
(Partial_Sums |.(z ExpSeq ).|) . (0 + 1) = ((Partial_Sums |.(z ExpSeq ).|) . 0 ) + (|.(z ExpSeq ).| . (0 + 1)) by SERIES_1:def 1
.= (|.(z ExpSeq ).| . 0 ) + (|.(z ExpSeq ).| . 1) by SERIES_1:def 1
.= (|.(z ExpSeq ).| . 0 ) + |.((z ExpSeq ) . 1).| by VALUED_1:18
.= |.((z ExpSeq ) . 0 ).| + |.((z ExpSeq ) . 1).| by VALUED_1:18
.= |.((z ExpSeq ) . 0 ).| + |.z.| by Lm13
.= 1 + |.z.| by Lm13, COMPLEX1:134 ;
then A3: ((Partial_Sums |.(z ExpSeq ).|) . (0 + 1)) - ((Partial_Sums |.(z P_dt ).|) . 0 ) = 1 + (|.z.| - (|.z.| / 2)) by A2;
defpred S₁[ Element of NAT ] means (Partial_Sums |.(z P_dt ).|) . $1 < (Partial_Sums |.(z ExpSeq ).|) . ($1 + 1);
0 <= |.z.| by COMPLEX1:132;
then A5: S₁[ 0 ] by A3, XREAL_1:49;
A6: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: (Partial_Sums |.(z P_dt ).|) . n < (Partial_Sums |.(z ExpSeq ).|) . (n + 1) ; :: thesis: S₁[n + 1]
A8: (Partial_Sums |.(z P_dt ).|) . (n + 1) = ((Partial_Sums |.(z P_dt ).|) . n) + (|.(z P_dt ).| . (n + 1)) by SERIES_1:def 1
.= ((Partial_Sums |.(z P_dt ).|) . n) + |.((z P_dt ) . (n + 1)).| by VALUED_1:18
.= ((Partial_Sums |.(z P_dt ).|) . n) + |.((z |^ ((n + 1) + 1)) / (((n + 1) + 2) !c )).| by Def28
.= ((Partial_Sums |.(z P_dt ).|) . n) + |.((z |^ (n + 2)) / ((n + 3) ! )).| by Th37 ;
(n + 3) ! > 0 by NEWTON:23;
then A9: (Partial_Sums |.(z P_dt ).|) . (n + 1) = ((Partial_Sums |.(z P_dt ).|) . n) + (|.(z #N (n + 2)).| / ((n + 3) ! )) by A8, Lm18;
A10: (Partial_Sums |.(z ExpSeq ).|) . ((n + 1) + 1) = ((Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + (|.(z ExpSeq ).| . (n + (1 + 1))) by SERIES_1:def 1
.= ((Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + |.((z ExpSeq ) . (n + 2)).| by VALUED_1:18
.= ((Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + |.((z |^ (n + 2)) / ((n + 2) !c )).| by Def8
.= ((Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + |.((z |^ (n + 2)) / ((n + 2) ! )).| by Th37 ;
(n + 2) ! > 0 by NEWTON:23;
then A11: (Partial_Sums |.(z ExpSeq ).|) . ((n + 1) + 1) = ((Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + (|.(z #N (n + 2)).| / ((n + 2) ! )) by A10, Lm18;
n + 2 < n + 3 by XREAL_1:8;
then A12: ( 0 < (n + 2) ! & (n + 2) ! <= (n + 3) ! ) by Th42, NEWTON:23;
|.(z |^ (n + 2)).| >= 0 by COMPLEX1:132;
then |.(z |^ (n + 2)).| / ((n + 2) ! ) >= |.(z |^ (n + 2)).| / ((n + 3) ! ) by A12, XREAL_1:120;
then A13: ((Partial_Sums |.(z P_dt ).|) . n) + (|.(z |^ (n + 2)).| / ((n + 3) ! )) <= ((Partial_Sums |.(z P_dt ).|) . n) + (|.(z |^ (n + 2)).| / ((n + 2) ! )) by XREAL_1:8;
((Partial_Sums |.(z P_dt ).|) . n) + (|.(z |^ (n + 2)).| / ((n + 2) ! )) < ((Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + (|.(z |^ (n + 2)).| / ((n + 2) ! )) by A7, XREAL_1:8;
hence S₁[n + 1] by A9, A11, A13, XXREAL_0:2; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A6);
hence (Partial_Sums |.(z P_dt ).|) . n < (Partial_Sums |.(z ExpSeq ).|) . (n + 1) ; :: thesis: verum

end;

consider r being real number such that
A14: for n being Element of NAT holds (Partial_Sums |.(z ExpSeq ).|) . n < r by SEQ_2:def 3;
A15: for n being Element of NAT holds (Partial_Sums |.(z P_dt ).|) . n < r

proof

let n be Element of NAT ; :: thesis: (Partial_Sums |.(z P_dt ).|) . n < r
(Partial_Sums |.(z P_dt ).|) . n < (Partial_Sums |.(z ExpSeq ).|) . (n + 1) by A1;
hence (Partial_Sums |.(z P_dt ).|) . n < r by A14, XXREAL_0:2; :: thesis: verum

end;

take r ; :: thesis: ( r is Real & ( for n being Element of NAT holds (Partial_Sums |.(z P_dt ).|) . n < r ) )
thus ( r is Real & ( for n being Element of NAT holds (Partial_Sums |.(z P_dt ).|) . n < r ) ) by A15, XREAL_0:def 1; :: thesis: verum

end;

hence Partial_Sums |.(z P_dt ).| is bounded_above by SEQ_2:def 3; :: thesis: verum

end;

hence z P_dt is absolutely_summable by COMSEQ_3:62; :: thesis: verum