let z be complex number ; :: thesis: z P_dt is absolutely_summable
A1: 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)
A3: (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 ;
A4: (Partial_Sums |.(z P_dt ).|) . 0 = |.z.| / 2 by A3, Lm14;
A5: (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 ;
A6: ((Partial_Sums |.(z ExpSeq ).|) . (0 + 1)) - ((Partial_Sums |.(z P_dt ).|) . 0 ) = 1 + (|.z.| - (|.z.| / 2)) by A4, A5;
defpred S₁[ Element of NAT ] means (Partial_Sums |.(z P_dt ).|) . $1 < (Partial_Sums |.(z ExpSeq ).|) . ($1 + 1);
A7: 0 <= |.z.| by COMPLEX1:132;
A8: S₁[ 0 ] by A6, A7, 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]
A11: (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 ;
A12: (n + 3) ! > 0 by NEWTON:23;
A13: (Partial_Sums |.(z P_dt ).|) . (n + 1) = ((Partial_Sums |.(z P_dt ).|) . n) + (|.(z #N (n + 2)).| / ((n + 3) ! )) by A11, A12, Lm14;
A14: (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 ;
A15: (n + 2) ! > 0 by NEWTON:23;
A16: (Partial_Sums |.(z ExpSeq ).|) . ((n + 1) + 1) = ((Partial_Sums |.(z ExpSeq ).|) . (n + 1)) + (|.(z #N (n + 2)).| / ((n + 2) ! )) by A14, A15, Lm14;
A17: n + 2 < n + 3 by XREAL_1:8;
A18: (n + 2) ! <= (n + 3) ! by A17, Th42;
A19: |.(z |^ (n + 2)).| >= 0 by COMPLEX1:132;
A20: |.(z |^ (n + 2)).| / ((n + 2) ! ) >= |.(z |^ (n + 2)).| / ((n + 3) ! ) by A18, A19, NEWTON:23, XREAL_1:120;
A21: ((Partial_Sums |.(z P_dt ).|) . n) + (|.(z |^ (n + 2)).| / ((n + 3) ! )) <= ((Partial_Sums |.(z P_dt ).|) . n) + (|.(z |^ (n + 2)).| / ((n + 2) ! )) by A20, XREAL_1:8;
A22: ((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;
thus S₁[n + 1] by A13, A16, A21, A22, XXREAL_0:2; :: thesis: verum

end;

A23: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A8, A9);
thus (Partial_Sums |.(z P_dt ).|) . n < (Partial_Sums |.(z ExpSeq ).|) . (n + 1) by A23; :: 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
A26: (Partial_Sums |.(z P_dt ).|) . n < (Partial_Sums |.(z ExpSeq ).|) . (n + 1) by A2;
thus (Partial_Sums |.(z P_dt ).|) . n < r by A24, A26, 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;

A27: Partial_Sums |.(z P_dt ).| is bounded_above by A1, SEQ_2:def 3;
thus z P_dt is absolutely_summable by A27, COMSEQ_3:62; :: thesis: verum