let z be Complex; :: thesis: z P_dt is absolutely_summable
ex r being Real st
for n being Nat holds (Partial_Sums |.(z P_dt).|) . n < r
proof
A1: for n being Nat holds (Partial_Sums |.(z P_dt).|) . n < (Partial_Sums |.(z ExpSeq).|) . (n + 1)
proof
let n be 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) !)).| by Def24
.= |.(z / 2).| by NEWTON:14 ;
then A2: (Partial_Sums |.(z P_dt).|) . 0 = |.z.| / 2 by Lm13;
(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 Lm8
.= 1 + |.z.| by Lm8, COMPLEX1:48 ;
then A3: ((Partial_Sums |.(z ExpSeq).|) . (0 + 1)) - ((Partial_Sums |.(z P_dt).|) . 0) = 1 + (|.z.| - (|.z.| / 2)) by A2;
defpred S1[ Nat] means (Partial_Sums |.(z P_dt).|) . $1 < (Partial_Sums |.(z ExpSeq).|) . ($1 + 1);
0 <= |.z.| by COMPLEX1:46;
then A4: S1[ 0 ] by A3, XREAL_1:47;
A5: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A6: (Partial_Sums |.(z P_dt).|) . n < (Partial_Sums |.(z ExpSeq).|) . (n + 1) ; :: thesis: S1[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) !)).| by Def24
.= ((Partial_Sums |.(z P_dt).|) . n) + |.((z |^ (n + 2)) / ((n + 3) !)).| ;
then A7: (Partial_Sums |.(z P_dt).|) . (n + 1) = ((Partial_Sums |.(z P_dt).|) . n) + (|.(z |^ (n + 2)).| / ((n + 3) !)) by Lm13;
(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) !)).| by Def4
.= ((Partial_Sums |.(z ExpSeq).|) . (n + 1)) + |.((z |^ (n + 2)) / ((n + 2) !)).| ;
then A8: (Partial_Sums |.(z ExpSeq).|) . ((n + 1) + 1) = ((Partial_Sums |.(z ExpSeq).|) . (n + 1)) + (|.(z |^ (n + 2)).| / ((n + 2) !)) by Lm13;
n + 2 < n + 3 by XREAL_1:6;
then A9: (n + 2) ! <= (n + 3) ! by Th38;
|.(z |^ (n + 2)).| >= 0 by COMPLEX1:46;
then |.(z |^ (n + 2)).| / ((n + 2) !) >= |.(z |^ (n + 2)).| / ((n + 3) !) by A9, XREAL_1:118;
then A10: ((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:6;
((Partial_Sums |.(z P_dt).|) . n) + (|.(z |^ (n + 2)).| / ((n + 2) !)) < ((Partial_Sums |.(z ExpSeq).|) . (n + 1)) + (|.(z |^ (n + 2)).| / ((n + 2) !)) by A6, XREAL_1:6;
hence S1[n + 1] by A7, A8, A10, XXREAL_0:2; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A5);
 hence (Partial_Sums |.(z P_dt).|) . n < (Partial_Sums |.(z ExpSeq).|) . (n + 1) ; :: thesis: verum
end;
consider r being Real such that
A11: for n being Nat holds (Partial_Sums |.(z ExpSeq).|) . n < r by SEQ_2:def 3;
A12: for n being Nat holds (Partial_Sums |.(z P_dt).|) . n < r
proof
let n be 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 A11, XXREAL_0:2; :: thesis: verum
end;
take r ; :: thesis: for n being Nat holds (Partial_Sums |.(z P_dt).|) . n < r
thus for n being Nat holds (Partial_Sums |.(z P_dt).|) . n < r by A12; :: 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:61; :: thesis: verum