let z be complex number ; :: thesis: z P_dt is absolutely_summable
ex r being Real st
for n being Element of NAT holds (Partial_Sums |.(z P_dt ).|) . n < r

proof

A2: 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 A4: (Partial_Sums |.(z P_dt ).|) . 0 = |.z.| / 2 by Lm14;
(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 Lm9
.= 1 + |.z.| by Lm9, COMPLEX1:134 ;
then A6: ((Partial_Sums |.(z ExpSeq ).|) . (0 + 1)) - ((Partial_Sums |.(z P_dt ).|) . 0 ) = 1 + (|.z.| - (|.z.| / 2)) by A4;
defpred S₁[ Element of NAT ] means (Partial_Sums |.(z P_dt ).|) . $1 < (Partial_Sums |.(z ExpSeq ).|) . ($1 + 1);
0 <= |.z.| by COMPLEX1:132;
then A8: S₁[ 0 ] by A6, XREAL_1:49;
A9: 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 A10: (Partial_Sums |.(z P_dt ).|) . n < (Partial_Sums |.(z ExpSeq ).|) . (n + 1) ; :: thesis: S₁[n + 1]
(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 ;
then A13: (Partial_Sums |.(z P_dt ).|) . (n + 1) = ((Partial_Sums |.(z P_dt ).|) . n) + (|.(z #N (n + 2)).| / ((n + 3) ! )) by Lm14;
(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 ;
then A16: (Partial_Sums |.(z ExpSeq ).|) . ((n + 1) + 1) = ((Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + (|.(z #N (n + 2)).| / ((n + 2) ! )) by Lm14;
n + 2 < n + 3 by XREAL_1:8;
then A18: (n + 2) ! <= (n + 3) ! by Th42;
|.(z |^ (n + 2)).| >= 0 by COMPLEX1:132;
then |.(z |^ (n + 2)).| / ((n + 2) ! ) >= |.(z |^ (n + 2)).| / ((n + 3) ! ) by A18, XREAL_1:120;
then A21: ((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 A10, XREAL_1:8;
hence S₁[n + 1] by A13, A16, A21, XXREAL_0:2; :: thesis: verum

end;

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

end;

consider r being real number such that
A24: for n being Element of NAT holds (Partial_Sums |.(z ExpSeq ).|) . n < r by SEQ_2:def 3;
A25: 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 A2;
hence (Partial_Sums |.(z P_dt ).|) . n < r by A24, 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 A25, XREAL_0:def 1; :: thesis: verum

end;

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