let m be positive Nat; :: thesis: for M being non zero Nat
for z0 being non zero Element of F_Real st z0 = number_e holds
ex n1 being Nat st
for n being Nat st n1 <= n holds
|.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m)))
let M be non zero Nat; :: thesis: for z0 being non zero Element of F_Real st z0 = number_e holds
ex n1 being Nat st
for n being Nat st n1 <= n holds
|.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m)))
let z0 be non zero Element of F_Real; :: thesis: ( z0 = number_e implies ex n1 being Nat st
for n being Nat st n1 <= n holds
|.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m))) )
assume A1: z0 = number_e ; :: thesis: ex n1 being Nat st
for n being Nat st n1 <= n holds
|.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m)))
A2: ( (m |^ (m + 1)) rExpSeq is convergent & lim ((m |^ (m + 1)) rExpSeq) = 0 ) by Th44;
then consider n1 being Nat such that
A3: for n being Nat st n1 <= n holds
|.((((m |^ (m + 1)) rExpSeq) . n) - (lim ((m |^ (m + 1)) rExpSeq))).| < 1 / (2 * (M * (z0 to_power m))) by A1, TAYLOR_1:11, SEQ_2:def 7;
take n1 ; :: thesis: for n being Nat st n1 <= n holds
|.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m)))
let n be Nat; :: thesis: ( n1 <= n implies |.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m))) )
assume A4: n1 <= n ; :: thesis: |.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m)))
|.((((m |^ (m + 1)) rExpSeq) . n) - (lim ((m |^ (m + 1)) rExpSeq))).| = |.((((m |^ (m + 1)) |^ n) / (n !)) - (lim ((m |^ (m + 1)) rExpSeq))).| by SIN_COS:def 5;
hence |.((((m |^ (m + 1)) |^ n) / (n !)) - 0).| < 1 / (2 * (M * (z0 to_power m))) by A2, A4, A3; :: thesis: verum