let a, b, r be Real; :: thesis: ( a < b & 0 < r implies ex m being Element of NAT st
( ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) < 1 & 0 < ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) ) )
assume A1: ( a < b & 0 < r ) ; :: thesis: ex m being Element of NAT st
( ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) < 1 & 0 < ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) )
set z = r * (b - a);
set s = (r * (b - a)) rExpSeq ;
(r * (b - a)) rExpSeq is summable by SIN_COS:45;
then ( (r * (b - a)) rExpSeq is convergent & lim ((r * (b - a)) rExpSeq) = 0 ) by SERIES_1:4;
then consider n being Nat such that
A3: for m being Nat st n <= m holds
|.((((r * (b - a)) rExpSeq) . m) - 0).| < 1 by SEQ_2:def 7;
reconsider m0 = max (n,1) as Element of NAT by ORDINAL1:def 12;
reconsider m = m0 - 1 as Element of NAT by INT_1:5, XXREAL_0:25;
take m ; :: thesis: ( ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) < 1 & 0 < ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) )
|.((((r * (b - a)) rExpSeq) . (m + 1)) - 0).| < 1 by A3, XXREAL_0:25;
then A4: |.(((r * (b - a)) |^ (m + 1)) / ((m + 1) !)).| < 1 by SIN_COS:def 5;
0 < b - a by A1, XREAL_1:50;
then 0 * r < r * (b - a) by A1, XREAL_1:68;
then 0 < (r * (b - a)) to_power (m + 1) by POWER:34;
hence ( ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) < 1 & 0 < ((r * (b - a)) |^ (m + 1)) / ((m + 1) !) ) by A4, ABSVALUE:def 1, XREAL_1:139; :: thesis: verum