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

( ((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