let M, L be Real; :: thesis: ( M >= 0 & L >= 0 implies for e being Real st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m !) < e )
assume that
A1: M >= 0 and
A2: L >= 0 ; :: thesis: for e being Real st e > 0 holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m !) < e
A3: L rExpSeq is summable by SIN_COS:45;
then A4: M (#) (L rExpSeq) is convergent by SEQ_2:7, SERIES_1:4;
lim (L rExpSeq) = 0 by A3, SERIES_1:4;
then A5: lim (M (#) (L rExpSeq)) = M * 0 by A3, SEQ_2:8, SERIES_1:4;
let p be Real; :: thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m !) < p )
assume p > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m !) < p
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
abs (((M (#) (L rExpSeq)) . m) - 0) < p by A4, A5, SEQ_2:def 7;
take n ; :: thesis: for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m !) < p
A7: for n being Element of NAT holds M * ((L |^ n) / (n !)) = (M (#) (L rExpSeq)) . n

proof

let n be Element of NAT ; :: thesis: M * ((L |^ n) / (n !)) = (M (#) (L rExpSeq)) . n
M * ((L |^ n) / (n !)) = M * ((L rExpSeq) . n) by SIN_COS:def 5
.= (M (#) (L rExpSeq)) . n by SEQ_1:9 ;
hence M * ((L |^ n) / (n !)) = (M (#) (L rExpSeq)) . n ; :: thesis: verum

end;

now

let m be Element of NAT ; :: thesis: ( n <= m implies (M * (L |^ m)) / (m !) < p )
assume A8: n <= m ; :: thesis: (M * (L |^ m)) / (m !) < p
A9: ( L |^ m >= 0 & m ! > 0 ) by A2, NEWTON:17, POWER:3;
abs (((M (#) (L rExpSeq)) . m) - 0) = abs (M * ((L |^ m) / (m !))) by A7
.= (abs M) * (abs ((L |^ m) / (m !))) by COMPLEX1:65
.= M * (abs ((L |^ m) / (m !))) by A1, ABSVALUE:def 1
.= M * ((L |^ m) / (m !)) by A9, ABSVALUE:def 1
.= (M * (L |^ m)) / (m !) by XCMPLX_1:74 ;
hence (M * (L |^ m)) / (m !) < p by A6, A8; :: thesis: verum

end;

hence for m being Element of NAT st n <= m holds
(M * (L |^ m)) / (m !) < p ; :: thesis: verum