:: The {M}aclaurin Expansions :: by Akira Nishino and Yasunari Shidama :: :: Received July 6, 2005 :: Copyright (c) 2005-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, RCOMP_1, SUBSET_1, REAL_1, COMPLEX1, NEWTON, ARYTM_3, RELAT_1, CARD_1, PARTFUN1, SEQ_1, TAYLOR_1, XXREAL_1, ARYTM_1, TARSKI, FDIFF_1, FUNCT_1, SERIES_1, REALSET1, XBOOLE_0, SIN_COS, XXREAL_0, VALUED_0, VALUED_1, SEQ_2, ORDINAL2, CARD_3, ABIAN, TAYLOR_2, NAT_1; notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, RFUNCT_2, RCOMP_1, XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, NUMBERS, COMPLEX1, REAL_1, NAT_1, FUNCT_2, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SERIES_1, FDIFF_1, SEQFUNC, NEWTON, SIN_COS, TAYLOR_1, ABIAN; constructors ARYTM_0, REAL_1, NAT_1, SEQ_2, RCOMP_1, RFUNCT_2, LIMFUNC1, FDIFF_1, COMSEQ_3, SIN_COS, ABIAN, TAYLOR_1, SEQFUNC, SERIES_1, VALUED_1, RELSET_1, COMSEQ_2; registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, NEWTON, SIN_COS, INT_1, ORDINAL1; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions TAYLOR_1; equalities VALUED_1, SUBSET_1; expansions TAYLOR_1; theorems XBOOLE_1, ABSVALUE, PARTFUN1, XCMPLX_1, RELAT_1, RCOMP_1, SEQ_1, SEQ_2, SIN_COS, SERIES_1, FUNCT_1, RFUNCT_2, NAT_1, NEWTON, POWER, FDIFF_1, FDIFF_2, TAYLOR_1, SIN_COS2, XREAL_1, RFUNCT_1, ABIAN, COMPLEX1, XXREAL_0, VALUED_1, FUNCT_2, XREAL_0, ORDINAL1; schemes NAT_1; begin reserve Z for open Subset of REAL; theorem Th1: for x be Real, n be Nat holds |.x |^ n.| = |.x.| |^ n proof let x be Real, n be Nat; defpred P[Nat] means |.x |^ $1.| = |.x.| |^ $1; A1: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A2: P[k]; |.x |^ (k+1).| = |.x * x |^ k.| by NEWTON:6 .= |.x.| * |.x |^ k.| by COMPLEX1:65 .= |.x.| |^ (k+1) by A2,NEWTON:6; hence thesis; end; |.x |^ 0.| = |.1.| by NEWTON:4 .= 1 by ABSVALUE:def 1; then A3: P[0] by NEWTON:4; for n be Nat holds P[n] from NAT_1:sch 2(A3,A1); hence thesis; end; definition let f be PartFunc of REAL,REAL, Z be Subset of REAL, a be Real; func Maclaurin(f,Z,a) -> Real_Sequence equals Taylor(f,Z,0,a); coherence; end; theorem Th2: for n be Nat, f be PartFunc of REAL,REAL, r be Real st 0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1,].-r,r.[ for x be Real st x in ].-r, r.[ ex s be Real st 0 < s & s < 1 & f.x = Partial_Sums( Maclaurin(f,].-r,r.[,x)).n + (diff(f,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n+ 1)!) proof let n be Nat, f be PartFunc of REAL,REAL, r be Real such that A1: 0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1, ].-r,r.[; let x be Real; assume x in ].-r, r.[; then consider s be Real such that A2: 0 < s & s < 1 & f.x=Partial_Sums(Taylor(f, ].0-r,0+r.[,0,x)).n + ( diff(f,].0-r,0+r.[).(n+1)).(0+s*(x-0)) * (x-0) |^ (n+1) / ((n+1)!) by A1, TAYLOR_1:33; take s; thus thesis by A2; end; theorem for n be Nat, f be PartFunc of REAL,REAL, x0, r be Real st 0 < r & ].x0-r,x0+r.[ c= dom f & f is_differentiable_on n+1, ].x0-r,x0+r.[ for x be Real st x in ].x0-r, x0+r.[ ex s be Real st 0 < s & s < 1 & |.f.x- Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n.| = |. (diff(f,].x0-r,x0+r.[).(n +1)).(x0+s*(x-x0)) * (x-x0) |^ (n+1) / ((n+1)!).| proof let n be Nat; let f be PartFunc of REAL,REAL; let x0,r be Real such that A1: 0 < r & ].x0-r,x0+r.[ c= dom f & f is_differentiable_on n+1, ].x0-r, x0+r .[; let x be Real; assume x in ].x0-r,x0+r.[; then ex s be Real st 0 < s & s < 1 & f.x=Partial_Sums(Taylor( f, ].x0-r,x0+r.[ ,x0,x)).n + (diff(f,].x0-r,x0+r.[).(n+1)).(x0+s*(x-x0)) * (x-x0 ) |^ (n+1) /((n +1)!) by A1,TAYLOR_1:33; hence thesis; end; theorem Th4: for n be Nat, f be PartFunc of REAL,REAL, r be Real st 0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1, ].-r,r.[ for x be Real st x in ].-r, r.[ ex s be Real st 0 < s & s < 1 & |.f.x-Partial_Sums( Maclaurin(f,].-r,r.[,x)).n.| = |. (diff(f,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n+1)!).| proof let n be Nat; let f be PartFunc of REAL,REAL; let r be Real such that A1: 0 < r & ].-r,r.[ c= dom f & f is_differentiable_on n+1, ].-r,r.[; let x be Real; assume x in ].-r,r.[; then ex s be Real st 0 < s & s < 1 & f.x=Partial_Sums( Maclaurin(f, ].-r,r.[,x )).n + (diff(f,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n +1)!) by A1,Th2; hence thesis; end; Lm1: for f being Function of REAL, REAL holds dom (f | Z) = Z proof let f be Function of REAL, REAL; A1: dom f = REAL by FUNCT_2:def 1; thus dom (f|Z) = dom f /\ Z by RELAT_1:61 .= Z by A1,XBOOLE_1:28; end; theorem Th5: exp_R `| Z = exp_R | Z & dom(exp_R | Z) = Z proof A1: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; A2: dom (exp_R | Z) = Z by Lm1; A3: for x be Element of REAL st x in Z holds (exp_R `| Z).x=(exp_R | Z).x proof let x be Element of REAL such that A4: x in Z; thus (exp_R `| Z).x=diff(exp_R,x) by A1,A4,FDIFF_1:def 7 .=exp_R.x by TAYLOR_1:16 .=(exp_R | Z).x by A2,A4,FUNCT_1:47; end; dom (exp_R `| Z) = Z by A1,FDIFF_1:def 7; hence thesis by A2,A3,PARTFUN1:5; end; theorem Th6: for n be Nat holds diff(exp_R,Z).n=exp_R | Z proof let n be Nat; defpred P[Nat] means diff(exp_R,Z).$1 = exp_R | Z; A1: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A2: P[k]; A3: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; diff(exp_R,Z).(k+1)=(diff(exp_R,Z).k) `| Z by TAYLOR_1:def 5 .=exp_R `| Z by A2,A3,FDIFF_2:16 .=exp_R | Z by Th5; hence thesis; end; A4: P[0] by TAYLOR_1:def 5; for n be Nat holds P[n] from NAT_1:sch 2(A4,A1); hence thesis; end; theorem Th7: for n be Nat, x be Real st x in Z holds (diff(exp_R,Z) .n).x = exp_R.x proof let n be Nat; let x be Real; assume x in Z; then A1: x in dom(exp_R | Z) by Th5; (diff(exp_R,Z).n).x=(exp_R | Z).x by Th6 .=exp_R.x by A1,FUNCT_1:47; hence thesis; end; theorem for n be Element of NAT, r,x be Real st 0 < r holds Maclaurin(exp_R, ].-r,r.[,x).n = x |^ n / (n!) proof let n be Element of NAT; A1: |.0-0.|=0 by ABSVALUE:2; let r,x be Real; assume r > 0; then 0 in ].0-r,0+r.[ by A1,RCOMP_1:1; then A2: 0 in dom(exp_R | ].-r,r.[) by Th5; Maclaurin(exp_R, ].-r,r.[,x).n = (diff(exp_R,].-r,r.[).n).0 * (x-0) |^ n / (n!) by TAYLOR_1:def 7 .=(exp_R | ].-r,r.[).0 * x |^ n / (n!) by Th6 .=exp_R.0 * x |^ n / (n!) by A2,FUNCT_1:47 .=x |^ n / (n!) by SIN_COS2:13; hence thesis; end; theorem for n be Element of NAT, r,x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(exp_R,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) / ((n+1)!) .| <= |.exp_R.(s*x).| * |.x.| |^ (n+1) / ((n+1)!) proof let n be Element of NAT; let r,x,s be Real such that A1: x in ].-r,r.[ and A2: 0 < s and A3: s < 1; A4: |.s*x-0.| = |.s.| * |.x.| by COMPLEX1:65 .= s * |.x.| by A2,ABSVALUE:def 1; x in ].0-r,0+r.[ by A1; then A5: |.x-0.| < r by RCOMP_1:1; |.x.|>=0 by COMPLEX1:46; then |.x.| * s < r * 1 by A2,A3,A5,XREAL_1:97; then (s*x) in ].0-r,0+r.[ by A4,RCOMP_1:1; then A6: (s*x) in dom(exp_R | ].-r,r.[) by Th5; A7: |.(n+1)!.| = ((n+1)!) by ABSVALUE:def 1; |. (diff(exp_R,].-r,r.[).(n+1)).(s*x) * x |^ (n+1) /((n+1)!).| = |. (exp_R | ].-r,r.[).(s*x) * x |^ (n+1) /((n+1)!).| by Th6 .= |.exp_R.(s*x) * x |^ (n+1) /((n+1)!).| by A6,FUNCT_1:47 .= |.exp_R.(s*x) * x |^ (n+1).| /|.(n+1)!.| by COMPLEX1:67 .= |.exp_R.(s*x).| * |.x |^ (n+1).| /((n+1)!) by A7,COMPLEX1:65; hence thesis by Th1; end; theorem Th10: for n be Element of NAT holds exp_R is_differentiable_on n, Z proof let n be Element of NAT; let i be Nat such that i <= n-1; reconsider i as Element of NAT by ORDINAL1:def 12; A1: for x be Real st x in Z holds diff(exp_R,Z).i | Z is_differentiable_in x proof A2: diff(exp_R,Z).i | Z = exp_R | Z | Z by Th6 .= exp_R | Z by FUNCT_1:51; A3: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; let x be Real; assume x in Z; hence thesis by A2,A3,FDIFF_1:def 6; end; dom(diff(exp_R,Z).i) = dom(exp_R | Z) by Th6 .= Z by Th5; hence thesis by A1,FDIFF_1:def 6; end; theorem Th11: for r be Real st 0 < r ex M,L be Real st 0 <= M & 0 <= L & for n be Nat for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n /(n!).| <= M * L |^ n / (n!) proof let r be Real such that A1: r > 0; take M = exp_R.r; take L = r; now let n be Nat; now A2: for a,b be Real st 0 <=a & a<=b for n be Nat holds 0<= a |^ n & a |^ n <= b |^ n proof let a,b be Real such that A3: 0 <= a and A4: a <= b; defpred P[Nat] means 0 <= a |^ $1 & a |^ $1 <= b |^ $1; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A6: P[k]; 0*a <= a |^ k*a by A3,A6; hence a |^ (k+1) >= 0 by NEWTON:6; b |^ (k+1) = b |^ k*b & a |^ k*a <= b |^ k*b by A3,A4,A6,NEWTON:6 ,XREAL_1:66; hence thesis by NEWTON:6; end; b |^ 0 = 1 by NEWTON:4; then A7: P[0] by NEWTON:4; for n be Nat holds P[n] from NAT_1:sch 2(A7,A5); hence thesis; end; let x,s be Real such that A8: x in ].-r,r.[ and A9: 0 < s and A10: s < 1; x in ].0-r,0+r.[ by A8; then A11: |.x-0.| < r by RCOMP_1:1; |.x.| >= 0 by COMPLEX1:46; then A12: |.x.| |^ n <= L |^ n by A11,A2; |.x.| >= 0 by COMPLEX1:46; then s * |.x.| < 1 * r by A9,A10,A11,XREAL_1:97; then |.s.| * |.x.| < r by A9,ABSVALUE:def 1; then |.s*x - 0.| < r by COMPLEX1:65; then A13: (s*x) in ].0-r,0+r.[ by RCOMP_1:1; then A14: |.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n / (n!).| =|.exp_R.(s*x )* x |^ n / (n!).| by Th7 .=|.exp_R.(s*x)* (x |^ n / (n!)).| by XCMPLX_1:74 .=|.exp_R.(s*x).|*|.x |^ n / (n!).| by COMPLEX1:65; exp_R.(s*x) >= 0 by SIN_COS:54; then A15: r in [#](REAL) /\ dom exp_R & |.exp_R.(s*x).| = exp_R.(s*x) by ABSVALUE:def 1,TAYLOR_1:16, XREAL_0:def 1; for x0 be Real holds 0 <= diff(exp_R,x0) by TAYLOR_1:16; then A16: exp_R|[#](REAL) is non-decreasing by FDIFF_2:39,TAYLOR_1:16; |.x |^ n /(n!).| =|.x |^ n.| / |.n!.| by COMPLEX1:67 .=|.x |^ n.| / (n!) by ABSVALUE:def 1 .=|.x.| |^ n /(n!) by Th1; then A17: |.x |^ n /(n!).| <=L |^ n / (n!) by A12,XREAL_1:72; A18: |.exp_R.(s*x).| >= 0 & |.x |^ n /(n!).| >= 0 by COMPLEX1:46; (s*x) in {p where p is Real : -r
= 0 & L >= 0 for e be Real st e > 0 ex n be Nat st for m be Nat st n <= m holds (M*L |^ m / (m!)) < e proof let M,L be Real such that A1: M >=0 and A2: L >= 0; 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; assume p > 0; then consider n be Nat such that A6: for m be Nat st n<=m holds |.(M(#)(L rExpSeq)).m - 0.| < p by A4,A5,SEQ_2:def 7; take n; A7: for n be Element of NAT holds M*(L |^ n /(n!))=(M(#)(L rExpSeq)).n proof let n be Element of NAT; M*(L |^ n /(n!)) = M*((L rExpSeq).n) by SIN_COS:def 5 .= (M(#)(L rExpSeq)).n by SEQ_1:9; hence thesis; end; now let m be Nat such that A8: n <= m; A9: m in NAT by ORDINAL1:def 12; A10: L |^ m >= 0 & m! > 0 by A2,POWER:3; |.(M(#)(L rExpSeq)).m - 0.| = |.M*(L |^ m /(m!)).| by A7,A9 .=|.M.|*|.L |^ m /(m!).| by COMPLEX1:65 .=M*|.L |^ m /(m!).| by A1,ABSVALUE:def 1 .=M*(L |^ m /(m!)) by A10,ABSVALUE:def 1 .=M*L |^ m /(m!) by XCMPLX_1:74; hence (M*L |^ m /(m!)) < p by A6,A8; end; hence thesis; end; theorem Th13: for r, e be Real st 0 < r & 0 < e ex n be Nat st for m be Nat st n <= m for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(exp_R,].-r,r.[).m).(s*x) * x |^ m / (m!).|< e proof let r, e be Real such that A1: 0 < r and A2: 0 < e; consider M, L be Real such that A3: M >= 0 & L >= 0 and A4: for n be Nat holds for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(exp_R,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= M*L |^ n / (n!) by A1,Th11; consider n be Nat such that A5: for m be Nat st n <= m holds (M*L |^ m / (m!)) < e by A2,A3,Th12; take n; let m be Nat; assume n <= m; then A6: (M*L |^ m / (m!)) < e by A5; let x,s be Real; assume x in ].-r,r.[ & 0 < s & s < 1; then |.(diff(exp_R,].-r,r.[).m).(s*x) * x |^ m /(m!).| <= M*L |^ m /(m!) by A4; hence thesis by A6,XXREAL_0:2; end; theorem for r, e be Real st 0 < r & 0 < e ex n be Nat st for m be Nat st n <= m holds for x being Real st x in ].-r,r.[ holds |.exp_R.x-Partial_Sums(Maclaurin(exp_R,].-r,r.[,x)).m.| < e proof let r, e be Real such that A1: r > 0 and A2: e > 0; consider n be Nat such that A3: for m be Nat st n <= m for x,s be Real st x in ].-r ,r.[ & 0 < s & s < 1 holds |. (diff(exp_R,].-r,r.[).m).(s*x) * x |^ m / (m!) .|< e by A1,A2,Th13; take n; let m be Nat such that A4: n <= m; now m <= m+1 by NAT_1:11; then A5: n <= m+1 by A4,XXREAL_0:2; let x be Real such that A6: x in ].-r,r.[; ex s be Real st 0 < s & s < 1 & |.exp_R.x-Partial_Sums (Maclaurin( exp_R,].-r,r.[,x)).m.| =|. (diff(exp_R,].-r,r.[).(m+1)).(s*x) * x |^ (m+1) / ( (m+1)!).| by A1,A6,Th4,Th10,SIN_COS:47; hence |.exp_R.x-Partial_Sums(Maclaurin(exp_R,].-r,r.[,x)).m.| < e by A3,A6,A5; end; hence thesis; end; theorem Th15: for x be Real holds x rExpSeq is absolutely_summable proof let x be Real; for n be Nat holds |.x rExpSeq.n.| = (|.x.| rExpSeq).n proof let n be Nat; |.x rExpSeq.n.| = |.x |^ n / (n!).| by SIN_COS:def 5 .= |.x |^ n.| / |.n!.| by COMPLEX1:67 .= |.x |^ n.| / (n!) by ABSVALUE:def 1 .= |.x.| |^ n / (n!) by Th1 .= (|.x.| rExpSeq).n by SIN_COS:def 5; hence thesis; end; then |.x.| rExpSeq = |.x rExpSeq.| by SEQ_1:12; then |.x rExpSeq.| is summable by SIN_COS:45; hence thesis by SERIES_1:def 4; end; theorem for r, x be Real st 0 < r holds Maclaurin(exp_R,].-r,r.[,x) = (x rExpSeq) & Maclaurin(exp_R,].-r,r.[,x) is absolutely_summable & exp_R.x=Sum( Maclaurin(exp_R,].-r,r.[,x)) proof A1: |.0-0.|=0 by ABSVALUE:2; let r, x be Real; assume r > 0; then 0 in ].0-r,0+r.[ by A1,RCOMP_1:1; then A2: 0 in dom(exp_R | ].-r,r.[) by Th5; now let t be object; assume t in NAT; then reconsider n=t as Element of NAT; thus Maclaurin(exp_R,].-r,r.[,x).t = (diff(exp_R,].-r,r.[).n).0 * (x-0) |^ n / (n!) by TAYLOR_1:def 7 .= (exp_R | ].-r,r.[).0 * x |^ n / (n!) by Th6 .= exp_R.0 * x |^ n / (n!) by A2,FUNCT_1:47 .= (x rExpSeq).t by SIN_COS:def 5,SIN_COS2:13; end; then Maclaurin(exp_R,].-r,r.[,x) = (x rExpSeq) by FUNCT_2:12; hence thesis by Th15,SIN_COS:def 22; end; theorem Th17: sin `| Z = cos | Z & cos `| Z = (-sin) | Z & dom(sin | Z) = Z & dom(cos | Z) = Z proof A1: dom (sin | Z) = dom(sin) /\ Z by RELAT_1:61 .= Z by SIN_COS:24,XBOOLE_1:28; A2: dom (cos | Z) = dom(cos) /\ Z by RELAT_1:61 .= Z by SIN_COS:24,XBOOLE_1:28; A3: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68; A4: for x be Element of REAL st x in Z holds (sin `| Z).x = (cos | Z).x proof let x be Element of REAL such that A5: x in Z; (sin `| Z).x=diff(sin,x) by A3,A5,FDIFF_1:def 7 .=cos.x by SIN_COS:64 .=(cos | Z).x by A2,A5,FUNCT_1:47; hence thesis; end; A6: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67; then A7: dom (cos `| Z) = Z by FDIFF_1:def 7; A8: dom ((-sin) | Z) = dom((-1)(#)sin) /\ Z by RELAT_1:61 .= dom(sin) /\ Z by VALUED_1:def 5 .= Z by SIN_COS:24,XBOOLE_1:28; A9: for x be Element of REAL st x in Z holds (cos `| Z).x = ((-sin) | Z).x proof let x be Element of REAL such that A10: x in Z; x in dom (sin) by SIN_COS:24; then A11: x in dom ((-1)(#)sin) by VALUED_1:def 5; (cos `| Z).x=diff(cos,x) by A6,A10,FDIFF_1:def 7 .=-sin.x by SIN_COS:63 .=(-1)*sin.x .=(-sin).x by A11,VALUED_1:def 5 .=((-sin) | Z).x by A8,A10,FUNCT_1:47; hence thesis; end; dom (sin `| Z) = Z by A3,FDIFF_1:def 7; hence thesis by A8,A1,A2,A4,A7,A9,PARTFUN1:5; end; theorem for f be PartFunc of REAL,REAL, Z be Subset of REAL st f is_differentiable_on Z holds (-f) `| Z = -f `| Z proof let f be PartFunc of REAL,REAL, Z be Subset of REAL such that A1: f is_differentiable_on Z; Z is open Subset of REAL by A1,FDIFF_1:10; then (-f) `| Z = (-1)(#) (f `| Z) by A1,FDIFF_2:19 .= -f `| Z; hence thesis; end; theorem Th19: for n be Nat holds diff(sin,Z).(2*n) = (-1) |^ n (#) sin | Z & diff(sin,Z).(2*n+1) = (-1) |^ n (#) cos | Z & diff(cos,Z).(2*n) = (-1 ) |^ n (#)cos | Z & diff(cos,Z).(2*n+1) = (-1) |^ (n+1) (#)sin | Z proof let n be Nat; A1: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67; defpred P[Nat] means diff(sin,Z).(2*$1) = (-1) |^ $1 (#) sin | Z & diff(sin,Z).(2*$1+1) = (-1) |^ $1 (#) cos | Z & diff(cos,Z).(2*$1) = (-1) |^ $1 (#) cos | Z & diff(cos,Z).(2*$1+1) = (-1) |^ ($1+1) (#) sin | Z; A2: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68; A3: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A4: P[k]; A5: (cos | Z) is_differentiable_on Z by A1,FDIFF_2:16; A6: diff(sin,Z).(2*(k+1)) = diff(sin,Z).((2*k+1)+1) .= diff(sin,Z).(2*k+1) `| Z by TAYLOR_1:def 5 .= ((-1) |^ k) (#) ((cos | Z) `| Z) by A4,A5,FDIFF_2:19 .= ((-1) |^ k) (#) (cos `| Z) by A1,FDIFF_2:16 .= ((-1) |^ k) (#) (((-1) (#) sin) | Z) by Th17 .= ((-1) |^ k) (#) ((-1) (#) sin | Z) by RFUNCT_1:49 .= (((-1) |^ k) * (-1)) (#) (sin | Z) by RFUNCT_1:17 .= (-1) |^ (k+1) (#) sin | Z by NEWTON:6; A7: (sin | Z) is_differentiable_on Z by A2,FDIFF_2:16; A8: diff(cos,Z).(2*(k+1)) = diff(cos,Z).((2*k+1)+1) .= diff(cos,Z).(2*k+1) `| Z by TAYLOR_1:def 5 .= ((-1) |^ (k+1)) (#) ((sin | Z) `| Z) by A4,A7,FDIFF_2:19 .= (-1) |^ (k+1) (#) (sin `| Z) by A2,FDIFF_2:16 .= (-1) |^ (k+1) (#) cos | Z by Th17; A9: diff(cos,Z).(2*(k+1)+1) = diff(cos,Z).(2*(k+1)) `| Z by TAYLOR_1:def 5 .= ((-1) |^ (k+1)) (#) ((cos | Z) `| Z) by A5,A8,FDIFF_2:19 .= ((-1) |^ (k+1)) (#) (cos `| Z) by A1,FDIFF_2:16 .= ((-1) |^ (k+1)) (#) ((-1) (#) sin) | Z by Th17 .= ((-1) |^ (k+1)) (#) ((-1) (#) sin | Z) by RFUNCT_1:49 .= (((-1) |^ (k+1)) * (-1)) (#) sin | Z by RFUNCT_1:17 .= (-1) |^ ((k+1)+1) (#) sin | Z by NEWTON:6; diff(sin,Z).(2*(k+1)+1) = diff(sin,Z).(2*(k+1)) `| Z by TAYLOR_1:def 5 .= ((-1) |^ (k+1)) (#) ((sin | Z) `| Z) by A7,A6,FDIFF_2:19 .= ((-1) |^ (k+1)) (#) (sin `| Z) by A2,FDIFF_2:16 .= (-1) |^ (k+1) (#) cos | Z by Th17; hence thesis by A6,A8,A9; end; A10: diff(cos,Z).(2*0+1) = diff(cos,Z).0 `| Z by TAYLOR_1:def 5 .= cos | Z `| Z by TAYLOR_1:def 5 .= cos `| Z by A1,FDIFF_2:16 .= (-sin) | Z by Th17 .= 1 (#) (-sin) | Z by RFUNCT_1:21 .= ((-1) |^ 0) (#) ((-1) (#) sin) | Z by NEWTON:4 .= ((-1) |^ 0) (#) ((-1) (#) sin | Z) by RFUNCT_1:49 .= (((-1) |^ 0) * (-1)) (#) sin | Z by RFUNCT_1:17 .= (-1) |^ (0+1) (#) sin | Z by NEWTON:6; A11: diff(sin,Z).(2*0) = sin | Z by TAYLOR_1:def 5 .= 1 (#) (sin | Z) by RFUNCT_1:21 .= (-1) |^ 0 (#) (sin | Z) by NEWTON:4; A12: diff(cos,Z).(2*0) = cos | Z by TAYLOR_1:def 5 .= 1 (#) (cos | Z) by RFUNCT_1:21 .= (-1) |^ 0 (#) (cos | Z) by NEWTON:4; diff(sin,Z).(2*0+1) = diff(sin,Z).0 `| Z by TAYLOR_1:def 5 .= sin | Z `| Z by TAYLOR_1:def 5 .= sin `| Z by A2,FDIFF_2:16 .= cos | Z by Th17 .= 1 (#) (cos | Z) by RFUNCT_1:21 .= (-1) |^ 0 (#) (cos | Z) by NEWTON:4; then A13: P[0] by A11,A12,A10; for n be Nat holds P[n] from NAT_1:sch 2(A13,A3); hence thesis; end; theorem Th20: for n be Nat, r,x be Real st r > 0 holds Maclaurin( sin, ].-r,r.[,x).(2*n) = 0 & Maclaurin(sin, ].-r,r.[,x).(2*n+1) = (-1) |^ n * x |^ (2*n+1) / ((2*n+1)!) & Maclaurin(cos, ].-r,r.[,x).(2*n) = (-1) |^ n * x |^ ( 2*n) / ((2*n)!) & Maclaurin(cos, ].-r,r.[,x).(2*n+1) = 0 proof A1: |.0-0.|=0 by ABSVALUE:2; let n be Nat, r,x be Real; assume r > 0; then A2: 0 in ].0-r,0+r.[ by A1,RCOMP_1:1; then A3: 0 in dom(cos | ].-r,r.[) by Th17; A4: dom(((-1) |^ n) (#) (cos | ].-r,r.[)) = dom(cos | ].-r,r.[) by VALUED_1:def 5 .= ].-r,r.[ by Th17; A5: Maclaurin(sin, ].-r,r.[,x).(2*n+1) = (diff(sin,].-r,r.[).(2*n+1)).0 * ( x-0) |^ (2*n+1) / ((2*n+1)!) by TAYLOR_1:def 7 .= ((-1) |^ n (#) cos | ].-r,r.[).0 * x |^ (2*n+1) / ((2*n+1)!) by Th19 .= (((-1) |^ n) * (cos | ].-r,r.[).0) * x |^ (2*n+1) / ((2*n+1)!) by A2,A4, VALUED_1:def 5 .= ((-1) |^ n) * cos.0 * x |^ (2*n+1) / ((2*n+1)!) by A3,FUNCT_1:47 .= (-1) |^ n * x |^ (2*n+1) / ((2*n+1)!) by SIN_COS:30; A6: dom(((-1) |^ n) (#) (sin | ].-r,r.[)) = dom(sin | ].-r,r.[) by VALUED_1:def 5 .= ].-r,r.[ by Th17; A7: 0 in dom(sin | ].-r,r.[) by A2,Th17; A8: Maclaurin(cos, ].-r,r.[,x).(2*n) = (diff(cos,].-r,r.[).(2*n)).0 * (x-0) |^ (2*n) / ((2*n)!) by TAYLOR_1:def 7 .= ((-1) |^ n (#) cos | ].-r,r.[).0 * x |^ (2*n) / ((2*n)!) by Th19 .= (((-1) |^ n) * (cos | ].-r,r.[).0) * x |^ (2*n) / ((2*n)!) by A2,A4, VALUED_1:def 5 .= ((-1) |^ n) * cos.0 * x |^ (2*n) / ((2*n)!) by A3,FUNCT_1:47 .= (-1) |^ n * x |^ (2*n) / ((2*n)!) by SIN_COS:30; A9: dom(((-1) |^ (n+1)) (#) (sin | ].-r,r.[)) = dom(sin | ].-r,r.[) by VALUED_1:def 5 .= ].-r,r.[ by Th17; A10: Maclaurin(cos, ].-r,r.[,x).(2*n+1) = (diff(cos,].-r,r.[).(2*n+1)).0 * ( x-0) |^ (2*n+1) / ((2*n+1)!) by TAYLOR_1:def 7 .= ((-1) |^ (n+1) (#) sin | ].-r,r.[).0 * x |^ (2*n+1) / ((2*n+1)!) by Th19 .= (((-1) |^ (n+1)) * (sin | ].-r,r.[).0) * x |^ (2*n+1) / ((2*n+1)!) by A2 ,A9,VALUED_1:def 5 .= ((-1) |^ (n+1)) * sin.0 * x |^ (2*n+1) / ((2*n+1)!) by A7,FUNCT_1:47 .= 0 by SIN_COS:30; Maclaurin(sin, ].-r,r.[,x).(2*n) = (diff(sin,].-r,r.[).(2*n)).0 * (x-0) |^ (2*n) / ((2*n)!) by TAYLOR_1:def 7 .= ((-1) |^ n (#) sin | ].-r,r.[).0 * x |^ (2*n) / ((2*n)!) by Th19 .= (((-1) |^ n) * (sin | ].-r,r.[).0) * x |^ (2*n) / ((2*n)!) by A2,A6, VALUED_1:def 5 .= ((-1) |^ n) * sin.0 * x |^ (2*n) / ((2*n)!) by A7,FUNCT_1:47 .= 0 by SIN_COS:30; hence thesis by A5,A8,A10; end; theorem Th21: for n be Element of NAT holds sin is_differentiable_on n, Z & cos is_differentiable_on n, Z proof let n be Element of NAT; now let i be Nat such that i <= n-1; A1: now per cases; suppose i is even; then consider j be Nat such that A2: i=2*j by ABIAN:def 2; thus dom(diff(sin,Z).i) = dom((-1) |^ j (#) sin | Z) by A2,Th19 .= dom((sin | Z)) by VALUED_1:def 5 .= Z by Th17; end; suppose i is odd; then consider j be Nat such that A3: i=2*j+1 by ABIAN:9; thus dom(diff(sin,Z).i) = dom((-1) |^ j (#) cos | Z) by A3,Th19 .= dom((cos | Z)) by VALUED_1:def 5 .= Z by Th17; end; end; for x be Real st x in Z holds diff(sin,Z).i | Z is_differentiable_in x proof let x be Real such that A4: x in Z; now per cases; suppose i is even; then consider j be Nat such that A5: i = 2*j by ABIAN:def 2; sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68; then A6: (sin | Z) is_differentiable_in x by A4,FDIFF_1:def 6; diff(sin,Z).i = (-1) |^ j (#) sin | Z by A5,Th19; hence diff(sin,Z).i is_differentiable_in x by A6,FDIFF_1:15; end; suppose i is odd; then consider j be Nat such that A7: i = 2*j+1 by ABIAN:9; cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67; then A8: (cos | Z) is_differentiable_in x by A4,FDIFF_1:def 6; diff(sin,Z).i = (-1) |^ j (#) cos | Z by A7,Th19; hence diff(sin,Z).i is_differentiable_in x by A8,FDIFF_1:15; end; end; hence thesis by A1,RELAT_1:68; end; hence diff(sin,Z).i is_differentiable_on Z by A1,FDIFF_1:def 6; end; hence sin is_differentiable_on n, Z; now let i be Nat such that i <= n-1; A9: now per cases; suppose i is even; then consider j be Nat such that A10: i = 2*j by ABIAN:def 2; thus dom(diff(cos,Z).i) = dom((-1) |^ j (#) cos | Z) by A10,Th19 .= dom((cos | Z)) by VALUED_1:def 5 .= Z by Th17; end; suppose i is odd; then consider j be Nat such that A11: i = 2*j+1 by ABIAN:9; thus dom(diff(cos,Z).i) = dom((-1) |^ (j+1) (#) sin | Z) by A11,Th19 .= dom((sin | Z)) by VALUED_1:def 5 .= Z by Th17; end; end; for x be Real st x in Z holds diff(cos,Z).i | Z is_differentiable_in x proof let x be Real such that A12: x in Z; now per cases; suppose i is even; then consider j be Nat such that A13: i = 2*j by ABIAN:def 2; cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67; then A14: (cos | Z) is_differentiable_in x by A12,FDIFF_1:def 6; diff(cos,Z).i = (-1) |^ j (#) cos | Z by A13,Th19; hence diff(cos,Z).i is_differentiable_in x by A14,FDIFF_1:15; end; suppose i is odd; then consider j be Nat such that A15: i = 2*j+1 by ABIAN:9; sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68; then A16: (sin | Z) is_differentiable_in x by A12,FDIFF_1:def 6; diff(cos,Z).i = (-1) |^ (j+1) (#) sin | Z by A15,Th19; hence diff(cos,Z).i is_differentiable_in x by A16,FDIFF_1:15; end; end; hence thesis by A9,RELAT_1:68; end; hence diff(cos,Z).i is_differentiable_on Z by A9,FDIFF_1:def 6; end; hence thesis; end; theorem Th22: for r be Real st r > 0 ex r1,r2 be Real st r1 >= 0 & r2 >= 0 & for n be Nat for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1 * r2 |^ n / (n!) & |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1 * r2 |^ n / (n!) proof let r be Real such that A1: r > 0; take r1 = 1; take r2 = r; thus r1 >= 0 & r2 >= 0 by A1; let n be Nat; let x,s be Real such that A2: x in ].-r,r.[ and A3: s > 0 and A4: s < 1; x in ].0-r,0+r.[ by A2; then A5: |.x-0.| < r by RCOMP_1:1; A6: |.x.| |^ n / (n!) <= r2 |^ n / (n!) proof defpred P[Nat] means |.x.| |^ $1 / ($1!) <= r2 |^ $1 / ($1!); A7: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A8: P[k]; A9: |.x.| |^ (k+1) / ((k+1)!) = |.x.| |^ k * |.x.| / ((k+1)!) by NEWTON:6 .= |.x.| |^ k * |.x.| / (k! * (k+1)) by NEWTON:15 .= |.x.| |^ k * (|.x.| / (k! * (k+1))) by XCMPLX_1:74 .= |.x.| |^ k * (|.x.| / (k!) / (k+1)) by XCMPLX_1:78 .= |.x.| |^ k * (1 / ((k!) / |.x.|) / (k+1)) by XCMPLX_1:57 .= |.x.| |^ k * (1 / (k!) * |.x.| / (k+1)) by XCMPLX_1:82 .= (|.x.| |^ k * (1 / (k!) * |.x.|)) / (k+1) by XCMPLX_1:74 .= (|.x.| |^ k * (1 / (k!))) * |.x.| / (k+1) .= (|.x.| |^ k * 1) / (k!) * |.x.| / (k+1) by XCMPLX_1:74 .= |.x.| |^ k / (k!) * |.x.| / (k+1); |.x.| |^ k / (k!) = |.x |^ k.| / (k!) by Th1 .= |.x |^ k.| / |.k!.| by ABSVALUE:def 1 .= |.x |^ k / (k!).| by COMPLEX1:67; then A10: |.x.| |^ k / (k!) >= 0 by COMPLEX1:46; A11: r2 |^ (k+1) / ((k+1)!) = r2 |^ k * r2 / ((k+1)!) by NEWTON:6 .= r2 |^ k * r2 / (k! * (k+1)) by NEWTON:15 .= r2 |^ k * (r2 / (k! * (k+1))) by XCMPLX_1:74 .= r2 |^ k * (r2 / (k!) / (k+1)) by XCMPLX_1:78 .= r2 |^ k * (1 / ((k!) / r2) / (k+1)) by XCMPLX_1:57 .= r2 |^ k * (1 / (k!) * r2 / (k+1)) by XCMPLX_1:82 .= (r2 |^ k * (1 / (k!) * r2)) / (k+1) by XCMPLX_1:74 .= (r2 |^ k * (1 / (k!))) * r2 / (k+1) .= (r2 |^ k * 1) / (k!) * r2 / (k+1) by XCMPLX_1:74 .= r2 |^ k / (k!) * r2 / (k+1); |.x.| >= 0 by COMPLEX1:46; then |.x.| |^ k / (k!) * |.x.| <= r2 |^ k / (k!) * r2 by A5,A8,A10, XREAL_1:66; hence thesis by A9,A11,XREAL_1:72; end; |.x.| |^ 0 / (0!) = 1 / (0!) by NEWTON:4 .= r2 |^ 0 / (0!) by NEWTON:4; then A12: P[0]; for i be Nat holds P[i] from NAT_1:sch 2(A12,A7); hence thesis; end; |.x.| >= 0 by COMPLEX1:46; then s * |.x.| < 1 * r by A3,A4,A5,XREAL_1:97; then |.s.| * |.x.| < r by A3,ABSVALUE:def 1; then |.s*x - 0.| < r by COMPLEX1:65; then A13: (s*x) in ].0-r,0+r.[ by RCOMP_1:1; A14: for k be Nat holds |.(-1) |^ k.| = 1 proof let k be Nat; per cases; suppose k is even; then consider j be Nat such that A15: k = 2*j by ABIAN:def 2; thus |.(-1) |^ k.| = |.((-1) |^ (1+1)) |^ j.| by A15,NEWTON:9 .= |.((-1) |^ 1 * (-1)) |^ j.| by NEWTON:6 .= |.((-1) * (-1)) |^ j.| .= |.1.| .= 1 by ABSVALUE:def 1; end; suppose k is odd; then consider j be Nat such that A16: k = 2*j+1 by ABIAN:9; thus |.(-1) |^ k.| = |.(-1) |^ (2*j) * (-1).| by A16,NEWTON:6 .= |.((-1) |^ (1+1)) |^ j * (-1).| by NEWTON:9 .= |.((-1) |^ 1 * (-1)) |^ j * (-1).| by NEWTON:6 .= |.((-1) * (-1)) |^ j * (-1).| .= |.1 * (-1).| .= |.1.| by COMPLEX1:52 .= 1 by ABSVALUE:def 1; end; end; A17: |.(diff(sin,].-r,r.[).n).(s*x).| <= r1 proof per cases; suppose n is even; then consider k be Nat such that A18: n = 2*k by ABIAN:def 2; A19: dom(((-1) |^ k) (#) (sin | ].-r,r.[)) = dom(sin | ].-r,r.[) by VALUED_1:def 5 .= ].-r,r.[ by Th17; A20: (s*x) in dom(sin | ].-r,r.[) by A13,Th17; A21: |.sin (s*x).| <= 1 by SIN_COS:27; |.(diff(sin,].-r,r.[).n).(s*x).| = |.((-1) |^ k (#) sin | ].-r ,r.[).(s*x).| by A18,Th19 .= |.((-1) |^ k) * ((sin | ].-r,r.[).(s*x)).| by A13,A19, VALUED_1:def 5 .= |.(-1) |^ k.| * |.(sin | ].-r,r.[).(s*x).| by COMPLEX1:65 .= 1 * |.(sin | ].-r,r.[).(s*x).| by A14 .= |.sin.(s*x).| by A20,FUNCT_1:47; hence thesis by A21,SIN_COS:def 17; end; suppose n is odd; then consider k be Nat such that A22: n = 2*k+1 by ABIAN:9; A23: dom(((-1) |^ k) (#) (cos | ].-r,r.[)) = dom(cos | ].-r,r.[) by VALUED_1:def 5 .= ].-r,r.[ by Th17; A24: (s*x) in dom(cos | ].-r,r.[) by A13,Th17; A25: |.cos (s*x).| <= 1 by SIN_COS:27; |.(diff(sin,].-r,r.[).n).(s*x).| = |.((-1) |^ k (#) cos | ].-r ,r.[).(s*x).| by A22,Th19 .= |.((-1) |^ k) * ((cos | ].-r,r.[).(s*x)).| by A13,A23, VALUED_1:def 5 .= |.(-1) |^ k.| * |.(cos | ].-r,r.[).(s*x).| by COMPLEX1:65 .= 1 * |.(cos | ].-r,r.[).(s*x).| by A14 .= |.cos.(s*x).| by A24,FUNCT_1:47; hence thesis by A25,SIN_COS:def 19; end; end; A26: |.(diff(cos,].-r,r.[).n).(s*x).| <= r1 proof per cases; suppose n is even; then consider k be Nat such that A27: n = 2*k by ABIAN:def 2; A28: dom(((-1) |^ k) (#) (cos | ].-r,r.[)) = dom(cos | ].-r,r.[) by VALUED_1:def 5 .= ].-r,r.[ by Th17; A29: (s*x) in dom(cos | ].-r,r.[) by A13,Th17; A30: |.cos (s*x).| <= 1 by SIN_COS:27; |.(diff(cos,].-r,r.[).n).(s*x).| = |.((-1) |^ k (#) cos | ].-r ,r.[).(s*x).| by A27,Th19 .= |.((-1) |^ k) * ((cos | ].-r,r.[).(s*x)).| by A13,A28, VALUED_1:def 5 .= |.(-1) |^ k.| * |.(cos | ].-r,r.[).(s*x).| by COMPLEX1:65 .= 1 * |.(cos | ].-r,r.[).(s*x).| by A14 .= |.cos.(s*x).| by A29,FUNCT_1:47; hence thesis by A30,SIN_COS:def 19; end; suppose n is odd; then consider k be Nat such that A31: n = 2*k+1 by ABIAN:9; A32: dom(((-1) |^ (k+1)) (#) (sin | ].-r,r.[)) = dom(sin | ].-r,r.[) by VALUED_1:def 5 .= ].-r,r.[ by Th17; A33: (s*x) in dom(sin | ].-r,r.[) by A13,Th17; A34: |.sin (s*x).| <= 1 by SIN_COS:27; |.(diff(cos,].-r,r.[).n).(s*x).| = |.((-1) |^ (k+1) (#) sin | ].-r,r.[).(s*x).| by A31,Th19 .= |.((-1) |^ (k+1)) * ((sin | ].-r,r.[).(s*x)).| by A13,A32, VALUED_1:def 5 .= |.(-1) |^ (k+1).| * |.(sin | ].-r,r.[).(s*x).| by COMPLEX1:65 .= 1 * |.(sin | ].-r,r.[).(s*x).| by A14 .= |.sin.(s*x).| by A33,FUNCT_1:47; hence thesis by A34,SIN_COS:def 17; end; end; A35: |.x |^ n / (n!).| = |.x |^ n.| / |.n!.| by COMPLEX1:67 .= |.x |^ n.| / (n!) by ABSVALUE:def 1 .= |.x.| |^ n / (n!) by Th1; then A36: |.x.| |^ n / (n!) >= 0 by COMPLEX1:46; A37: |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| = |.(diff(cos,].- r,r.[).n).(s*x) * (x |^ n / (n!)).| by XCMPLX_1:74 .= |.(diff(cos,].-r,r.[).n).(s*x).| * |.x |^ n / (n!).| by COMPLEX1:65 .= |.(diff(cos,].-r,r.[).n).(s*x).| * |.x.| |^ n / (n!) by A35, XCMPLX_1:74; A38: |.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| = |.(diff(sin,].- r,r.[).n).(s*x) * (x |^ n / (n!)).| by XCMPLX_1:74 .= |.(diff(sin,].-r,r.[).n).(s*x).| * |.x |^ n / (n!).| by COMPLEX1:65 .= |.(diff(sin,].-r,r.[).n).(s*x).| * |.x.| |^ n / (n!) by A35, XCMPLX_1:74; |.(diff(cos,].-r,r.[).n).(s*x).| >= 0 by COMPLEX1:46; then A39: |.(diff(cos,].-r,r.[).n).(s*x).| * (|.x.| |^ n / (n!)) <= r1*(r2 |^ n / (n!)) by A36,A26,A6,XREAL_1:66; |.(diff(sin,].-r,r.[).n).(s*x).| >= 0 by COMPLEX1:46; then |.(diff(sin,].-r,r.[).n).(s*x).| * (|.x.| |^ n / (n!)) <= r1*(r2 |^ n / (n!)) by A36,A17,A6,XREAL_1:66; hence |.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1*r2 |^ n / (n! ) & |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1*r2 |^ n / (n!) by A38,A37,A39,XCMPLX_1:74; end; theorem Th23: for r, e be Real st 0 < r & 0 < e ex n be Nat st for m be Nat st n <= m for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(sin,].-r,r.[).m).(s*x) * x |^ m / (m!).| < e & |.( diff(cos,].-r,r.[).m).(s*x) * x |^ m / (m!).| < e proof let r, e be Real such that A1: r > 0 and A2: e > 0; consider r1,r2 be Real such that A3: r1 >= 0 & r2 >= 0 and A4: for n be Nat holds for x,s be Real st x in ].-r,r.[ & 0 < s & s < 1 holds |.(diff(sin,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1*r2 |^ n / (n!) & |.(diff(cos,].-r,r.[).n).(s*x) * x |^ n / (n!).| <= r1*r2 |^ n / (n!) by A1,Th22; consider n be Nat such that A5: for m be Nat st n <= m holds (r1 * r2 |^ m / (m!)) < e by A2,A3 ,Th12; take n; let m be Nat; assume n <= m; then A6: (r1*r2 |^ m /(m!)) < e by A5; let x,s be Real; assume x in ].-r,r.[ & 0 < s & s < 1; then |.(diff(sin,].-r,r.[).m).(s*x) * x |^ m /(m!).| <= r1*r2 |^ m /(m!) & |.( diff(cos,].-r,r.[).m).(s*x) * x |^ m /(m!).| <= r1*r2 |^ m /(m!) by A4; hence thesis by A6,XXREAL_0:2; end; theorem for r, e be Real st 0 < r & 0 < e ex n be Nat st for m be Nat st n <= m for x being Real st x in ].-r,r.[ holds |.sin.x-Partial_Sums(Maclaurin(sin,].-r,r.[,x)).m.| < e & |.cos.x- Partial_Sums(Maclaurin(cos,].-r,r.[,x)).m.| < e proof let r, e be Real such that A1: r > 0 and A2: e > 0; consider n be Nat such that A3: for m be Nat st n <= m for x,s be Real st x in ].-r ,r.[ & 0 < s & s < 1 holds |.(diff(sin,].-r,r.[).m).(s*x) * x |^ m /(m!).|< e & |.(diff(cos,].-r,r.[).m).(s*x) * x |^ m /(m!).|< e by A1,A2,Th23; take n; let m be Nat such that A4: n <= m; A5: cos is_differentiable_on m+1, ].-r,r.[ & dom cos =REAL by Th21, FUNCT_2:def 1; A6: sin is_differentiable_on m+1, ].-r,r.[ & dom sin = REAL by Th21, FUNCT_2:def 1; now m <= m+1 by NAT_1:11; then A7: n <= m+1 by A4,XXREAL_0:2; let x be Real such that A8: x in ].-r,r.[; ex s be Real st 0 < s & s < 1 & |.sin.x-Partial_Sums( Maclaurin(sin, ].-r,r.[,x)).m.| =|.(diff(sin,].-r,r.[).(m+1)).(s*x) * x |^ (m+1 ) / ((m+1)!).| by A1,A6,A8,Th4; hence |.sin.x-Partial_Sums(Maclaurin(sin,].-r,r.[,x)).m.| < e by A3,A8,A7; ex s be Real st 0 < s & s < 1 & |.cos.x-Partial_Sums( Maclaurin(cos, ].-r,r.[,x)).m.| =|.(diff(cos,].-r,r.[).(m+1)).(s*x) * x |^ (m+1 ) / ((m+1)!).| by A1,A5,A8,Th4; hence |.cos.x-Partial_Sums(Maclaurin(cos,].-r,r.[,x)).m.| < e by A3,A8,A7; end; hence thesis; end; theorem Th25: for r, x be Real, m be Nat st 0 < r holds Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m+1) = Partial_Sums(x P_sin).m & Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m+1) = Partial_Sums(x P_cos).m proof let r, x be Real, m be Nat such that A1: r > 0; thus Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m+1) = Partial_Sums(x P_sin) .m proof defpred P[Nat] means Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2 *$1+1) = Partial_Sums(x P_sin).$1; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A3: P[k]; Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*(k+1)+1) = Partial_Sums( Maclaurin(sin,].-r,r.[,x)).(2*k+2) + Maclaurin(sin,].-r,r.[,x).(2*k+3) by SERIES_1:def 1 .= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*k+2) + (-1) |^ (k+1) * x |^ (2*(k+1)+1) / ((2*(k+1)+1)!) by A1,Th20 .= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).((2*k+1)+1) + (x P_sin).( k+1) by SIN_COS:def 20 .= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*k+1) + Maclaurin(sin, ].-r,r.[,x).(2*(k+1)) + (x P_sin).(k+1) by SERIES_1:def 1 .= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*k+1) + 0 + (x P_sin).( k+1) by A1,Th20 .= Partial_Sums(x P_sin).(k+1) by A3,SERIES_1:def 1; hence thesis; end; Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*0+1) = Partial_Sums( Maclaurin(sin,].-r,r.[,x)).(2*0) + Maclaurin(sin,].-r,r.[,x).((2*0)+1) by SERIES_1:def 1 .= Maclaurin(sin,].-r,r.[,x).(2*0) + Maclaurin(sin,].-r,r.[,x).(2*0+1) by SERIES_1:def 1 .= 0 + Maclaurin(sin,].-r,r.[,x).(2*0+1) by A1,Th20 .= (-1) |^ 0 * x |^ (2*0+1) / ((2*0+1)!) by A1,Th20 .= (x P_sin).0 by SIN_COS:def 20 .= Partial_Sums(x P_sin).0 by SERIES_1:def 1; then A4: P[0]; for n be Nat holds P[n] from NAT_1:sch 2(A4,A2); hence thesis; end; defpred P[Nat] means Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2* $1+1) = Partial_Sums(x P_cos).$1; A5: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that A6: P[k]; Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*(k+1)+1) = Partial_Sums( Maclaurin(cos,].-r,r.[,x)).(2*k+2) + Maclaurin(cos,].-r,r.[,x).(2*(k+1)+1) by SERIES_1:def 1 .= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*k+2) + 0 by A1,Th20 .= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).((2*k+1)+1) .= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*k+1) + Maclaurin(cos,].- r,r.[,x).(2*k+2) by SERIES_1:def 1 .= Partial_Sums(x P_cos).k + (-1) |^ (k+1) * x |^ (2*(k+1)) / ((2*(k+1 ))!) by A1,A6,Th20 .= Partial_Sums(x P_cos).k + (x P_cos).(k+1) by SIN_COS:def 21 .= Partial_Sums(x P_cos).(k+1) by SERIES_1:def 1; hence thesis; end; Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*0+1) = Partial_Sums(Maclaurin (cos,].-r,r.[,x)).(2*0) + Maclaurin(cos,].-r,r.[,x).((2*0)+1) by SERIES_1:def 1 .= Maclaurin(cos,].-r,r.[,x).(2*0) + Maclaurin(cos,].-r,r.[,x).(2*0+1) by SERIES_1:def 1 .= Maclaurin(cos,].-r,r.[,x).(2*0) + 0 by A1,Th20 .= (-1) |^ 0 * x |^ (2*0) / ((2*0)!) by A1,Th20 .= (x P_cos).0 by SIN_COS:def 21 .= Partial_Sums(x P_cos).0 by SERIES_1:def 1; then A7: P[0]; for n be Nat holds P[n] from NAT_1:sch 2(A7,A5); hence thesis; end; theorem Th26: for r, x be Real, m being Nat st 0 < r & m > 0 holds Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m) = Partial_Sums(x P_sin).(m-1) & Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m) = Partial_Sums(x P_cos).m proof let r, x be Real, m be Nat such that A1: r > 0 and A2: m > 0; A3: m-1 is Element of NAT by A2,NAT_1:20; 2*m > 2*0 by A2,XREAL_1:68; then A4: 2*m-1 is Element of NAT by NAT_1:20; then A5: Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m) = Partial_Sums(Maclaurin( sin,].-r,r.[,x)).(2*m-1) + Maclaurin(sin,].-r,r.[,x).((2*m-1)+1) by SERIES_1:def 1 .= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*m-1) + 0 by A1,Th20 .= Partial_Sums(Maclaurin(sin,].-r,r.[,x)).(2*(m-1)+1) .= Partial_Sums(x P_sin).(m-1) by A1,A3,Th25; Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m) = Partial_Sums(Maclaurin( cos,].-r,r.[,x)).(2*m-1) + Maclaurin(cos,].-r,r.[,x).((2*m-1)+1) by A4, SERIES_1:def 1 .= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m-1) + (-1) |^ m * x |^ (2 *m) / ((2*m)!) by A1,Th20 .= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*(m-1)+1) + (x P_cos).m by SIN_COS:def 21 .= Partial_Sums(x P_cos).((m-1)) + (x P_cos).((m-1)+1) by A1,A3,Th25 .= Partial_Sums(x P_cos).m by A3,SERIES_1:def 1; hence thesis by A5; end; theorem Th27: for r, x be Real, m be Nat st 0 < r holds Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*m) = Partial_Sums(x P_cos).m proof let r, x be Real, m be Nat such that A1: r > 0; defpred P[Nat] means Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2* $1) = Partial_Sums(x P_cos).$1; A2: for k be Nat st P[k] holds P[k+1] proof let k be Nat such that P[k]; thus Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*(k+1)) = Partial_Sums( Maclaurin(cos,].-r,r.[,x)).(2*k+1) + Maclaurin(cos,].-r,r.[,x).((2*k+1)+1) by SERIES_1:def 1 .= Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*k+1) + (-1) |^ (k+1) * x |^ (2*(k+1)) / ((2*(k+1))!) by A1,Th20 .= Partial_Sums(x P_cos).k + (-1) |^ (k+1) * x |^ (2*(k+1)) / ((2*(k+1 ))!) by A1,Th25 .= Partial_Sums(x P_cos).k + (x P_cos).(k+1) by SIN_COS:def 21 .= Partial_Sums(x P_cos).(k+1) by SERIES_1:def 1; end; Partial_Sums(Maclaurin(cos,].-r,r.[,x)).(2*0) = Maclaurin(cos,].-r,r.[,x ).(2*0) by SERIES_1:def 1 .= (-1) |^ 0 * x |^ (2*0) / ((2*0)!) by A1,Th20 .= (x P_cos).0 by SIN_COS:def 21 .= Partial_Sums(x P_cos).0 by SERIES_1:def 1; then A3: P[0]; for n be Nat holds P[n] from NAT_1:sch 2(A3,A2); hence thesis; end; theorem for r, x be Real st r > 0 holds Partial_Sums(Maclaurin(sin,].-r,r.[,x) ) is convergent & sin.x = Sum(Maclaurin(sin,].-r,r.[,x)) & Partial_Sums( Maclaurin(cos,].-r,r.[,x)) is convergent & cos.x = Sum(Maclaurin(cos,].-r,r.[,x )) proof let r, x be Real such that A1: r > 0; set g = sin.x; Sum(x P_sin) = sin.x by SIN_COS:37; then A2: lim Partial_Sums(x P_sin) = sin.x by SERIES_1:def 3; A3: Partial_Sums(x P_sin) is convergent by SIN_COS:36; A4: for p being Real st p>0 ex n1 being Nat st for m1 be Nat st m1>=n1 holds |.Partial_Sums(Maclaurin(sin,].-r,r.[,x) ).m1-g.|
0; then consider n be Nat such that A5: for m being Nat st n<=m holds |.Partial_Sums(x P_sin) .m-g.| < p by A2,A3,SEQ_2:def 7; reconsider n1=2*n+2 as Nat; take n1; let m1 be Nat such that A6: m1>=n1; per cases; suppose m1 is even; then consider j be Nat such that A7: m1=2*j by ABIAN:def 2; A8: ((n+1)*2)/2 <= (j*2)/2 by A6,A7,XREAL_1:72; then A9: (n+1)-1 <= j-1 by XREAL_1:9; n+1 >= 0+1 by XREAL_1:6; then j-1 is Element of NAT by A8,NAT_1:20; then |.Partial_Sums(x P_sin).(j-1)-g.| < p by A5,A9; hence thesis by A1,A7,A8,Th26; end; suppose m1 is odd; then consider j be Nat such that A10: m1=2*j+1 by ABIAN:9; n*2+0 <= n*2+1 & (n*2+2)-1 <= (2*j+1)-1 by A6,A10,XREAL_1:6,9; then n*2 <= j*2 by XXREAL_0:2; then (n*2)/2 <= (j*2)/2 by XREAL_1:72; then |.Partial_Sums(x P_sin).j-g.| < p by A5; hence thesis by A1,A10,Th25; end; end; then Partial_Sums(Maclaurin(sin,].-r,r.[,x)) is convergent by SEQ_2:def 6; then A11: lim Partial_Sums(Maclaurin(sin,].-r,r.[,x)) = sin.x by A4,SEQ_2:def 7; Sum(x P_cos) = cos.x by SIN_COS:37; then A12: lim Partial_Sums(x P_cos) = cos.x by SERIES_1:def 3; set g = cos.x; A13: Partial_Sums(x P_cos) is convergent by SIN_COS:36; A14: for p being Real st p>0 holds ex n1 being Nat st for m1 be Nat st m1>=n1 holds |.Partial_Sums(Maclaurin(cos,].-r,r.[,x) ).m1-g.|
0; then consider n be Nat such that A15: for m being Nat st n<=m holds |.Partial_Sums(x P_cos ).m-g.| < p by A12,A13,SEQ_2:def 7; reconsider n1=2*n+1 as Nat; take n1; let m1 be Nat such that A16: m1>=n1; per cases; suppose m1 is even; then consider j be Nat such that A17: m1=2*j by ABIAN:def 2; (n*2)+1 >= n*2 by XREAL_1:29; then n*2 <= j*2 by A16,A17,XXREAL_0:2; then (n*2)/2 <= (j*2)/2 by XREAL_1:72; then |.Partial_Sums(x P_cos).j-g.| < p by A15; hence thesis by A1,A17,Th27; end; suppose m1 is odd; then consider j be Nat such that A18: m1=2*j+1 by ABIAN:9; (n*2+1)-1 <= (j*2+1)-1 by A16,A18,XREAL_1:9; then (n*2)/2 <= (j*2)/2 by XREAL_1:72; then |.Partial_Sums(x P_cos).j-g.| < p by A15; hence thesis by A1,A18,Th25; end; end; then Partial_Sums(Maclaurin(cos,].-r,r.[,x)) is convergent by SEQ_2:def 6; then lim Partial_Sums(Maclaurin(cos,].-r,r.[,x)) = cos.x by A14,SEQ_2:def 7; hence thesis by A4,A11,A14,SEQ_2:def 6,SERIES_1:def 3; end;