:: TAYLOR_2 semantic presentation begin theorem Th1: :: TAYLOR_2:1 for x being Real for n being Element of NAT holds abs (x |^ n) = (abs x) |^ n proof let x be Real; ::_thesis: for n being Element of NAT holds abs (x |^ n) = (abs x) |^ n let n be Element of NAT ; ::_thesis: abs (x |^ n) = (abs x) |^ n defpred S1[ Element of NAT ] means abs (x |^ \$1) = (abs x) |^ \$1; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] abs (x |^ (k + 1)) = abs (x * (x |^ k)) by NEWTON:6 .= (abs x) * (abs (x |^ k)) by COMPLEX1:65 .= (abs x) |^ (k + 1) by A2, NEWTON:6 ; hence S1[k + 1] ; ::_thesis: verum end; abs (x |^ 0) = abs 1 by NEWTON:4 .= 1 by ABSVALUE:def_1 ; then A3: S1[ 0 ] by NEWTON:4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence abs (x |^ n) = (abs x) |^ n ; ::_thesis: verum end; definition let f be PartFunc of REAL,REAL; let Z be Subset of REAL; let a be real number ; func Maclaurin (f,Z,a) -> Real_Sequence equals :: TAYLOR_2:def 1 Taylor (f,Z,0,a); coherence Taylor (f,Z,0,a) is Real_Sequence ; end; :: deftheorem defines Maclaurin TAYLOR_2:def_1_:_ for f being PartFunc of REAL,REAL for Z being Subset of REAL for a being real number holds Maclaurin (f,Z,a) = Taylor (f,Z,0,a); theorem Th2: :: TAYLOR_2:2 for n being Element of NAT for f being PartFunc of REAL,REAL for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds for x being Real st x in ].(- r),r.[ holds ex s being 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 Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds for x being Real st x in ].(- r),r.[ holds ex s being 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) !)) ) let f be PartFunc of REAL,REAL; ::_thesis: for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds for x being Real st x in ].(- r),r.[ holds ex s being 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) !)) ) let r be Real; ::_thesis: ( 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ implies for x being Real st x in ].(- r),r.[ holds ex s being 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) !)) ) ) assume A1: ( 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ ) ; ::_thesis: for x being Real st x in ].(- r),r.[ holds ex s being 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) !)) ) let x be Real; ::_thesis: ( x in ].(- r),r.[ implies ex s being 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) !)) ) ) assume x in ].(- r),r.[ ; ::_thesis: ex s being 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) !)) ) then consider s being 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 ; ::_thesis: ( 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) !)) ) thus ( 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 A2; ::_thesis: verum end; theorem :: TAYLOR_2:3 for n being Element of NAT for f being PartFunc of REAL,REAL for x0, r being Real st 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for x0, r being Real st 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) let f be PartFunc of REAL,REAL; ::_thesis: for x0, r being Real st 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ holds for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) let x0, r be Real; ::_thesis: ( 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ implies for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ) assume A1: ( 0 < r & ].(x0 - r),(x0 + r).[ c= dom f & f is_differentiable_on n + 1,].(x0 - r),(x0 + r).[ ) ; ::_thesis: for x being Real st x in ].(x0 - r),(x0 + r).[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) let x be Real; ::_thesis: ( x in ].(x0 - r),(x0 + r).[ implies ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ) assume x in ].(x0 - r),(x0 + r).[ ; ::_thesis: ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) then ex s being 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 ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Taylor (f,].(x0 - r),(x0 + r).[,x0,x))) . n)) = abs (((((diff (f,].(x0 - r),(x0 + r).[)) . (n + 1)) . (x0 + (s * (x - x0)))) * ((x - x0) |^ (n + 1))) / ((n + 1) !)) ) ; ::_thesis: verum end; theorem Th4: :: TAYLOR_2:4 for n being Element of NAT for f being PartFunc of REAL,REAL for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds for x being Real st x in ].(- r),r.[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,REAL for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds for x being Real st x in ].(- r),r.[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) ) let f be PartFunc of REAL,REAL; ::_thesis: for r being Real st 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ holds for x being Real st x in ].(- r),r.[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) ) let r be Real; ::_thesis: ( 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ implies for x being Real st x in ].(- r),r.[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) ) ) assume A1: ( 0 < r & ].(- r),r.[ c= dom f & f is_differentiable_on n + 1,].(- r),r.[ ) ; ::_thesis: for x being Real st x in ].(- r),r.[ holds ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) ) let x be Real; ::_thesis: ( x in ].(- r),r.[ implies ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) ) ) assume x in ].(- r),r.[ ; ::_thesis: ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) ) then ex s being 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 ex s being Real st ( 0 < s & s < 1 & abs ((f . x) - ((Partial_Sums (Maclaurin (f,].(- r),r.[,x))) . n)) = abs (((((diff (f,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) ) ; ::_thesis: verum end; Lm1: for Z being open Subset of REAL for f being Function of REAL,REAL holds dom (f | Z) = Z proof let Z be open Subset of REAL; ::_thesis: for f being Function of REAL,REAL holds dom (f | Z) = Z let f be Function of REAL,REAL; ::_thesis: dom (f | Z) = Z 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 ; ::_thesis: verum end; theorem Th5: :: TAYLOR_2:5 for Z being open Subset of REAL holds ( exp_R `| Z = exp_R | Z & dom (exp_R | Z) = Z ) proof let Z be open Subset of REAL; ::_thesis: ( exp_R `| Z = exp_R | Z & dom (exp_R | Z) = Z ) 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 being Real st x in Z holds (exp_R `| Z) . x = (exp_R | Z) . x proof let x be Real; ::_thesis: ( x in Z implies (exp_R `| Z) . x = (exp_R | Z) . x ) assume A4: x in Z ; ::_thesis: (exp_R `| Z) . x = (exp_R | Z) . x 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 ; ::_thesis: verum end; dom (exp_R `| Z) = Z by A1, FDIFF_1:def_7; hence ( exp_R `| Z = exp_R | Z & dom (exp_R | Z) = Z ) by A2, A3, PARTFUN1:5; ::_thesis: verum end; theorem Th6: :: TAYLOR_2:6 for Z being open Subset of REAL for n being Element of NAT holds (diff (exp_R,Z)) . n = exp_R | Z proof let Z be open Subset of REAL; ::_thesis: for n being Element of NAT holds (diff (exp_R,Z)) . n = exp_R | Z let n be Element of NAT ; ::_thesis: (diff (exp_R,Z)) . n = exp_R | Z defpred S1[ Element of NAT ] means (diff (exp_R,Z)) . \$1 = exp_R | Z; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] 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 S1[k + 1] ; ::_thesis: verum end; A4: S1[ 0 ] by TAYLOR_1:def_5; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A1); hence (diff (exp_R,Z)) . n = exp_R | Z ; ::_thesis: verum end; theorem Th7: :: TAYLOR_2:7 for Z being open Subset of REAL for n being Element of NAT for x being Real st x in Z holds ((diff (exp_R,Z)) . n) . x = exp_R . x proof let Z be open Subset of REAL; ::_thesis: for n being Element of NAT for x being Real st x in Z holds ((diff (exp_R,Z)) . n) . x = exp_R . x let n be Element of NAT ; ::_thesis: for x being Real st x in Z holds ((diff (exp_R,Z)) . n) . x = exp_R . x let x be Real; ::_thesis: ( x in Z implies ((diff (exp_R,Z)) . n) . x = exp_R . x ) assume x in Z ; ::_thesis: ((diff (exp_R,Z)) . n) . x = exp_R . x 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 ((diff (exp_R,Z)) . n) . x = exp_R . x ; ::_thesis: verum end; theorem :: TAYLOR_2:8 for n being Element of NAT for r, x being Real st 0 < r holds (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !) proof let n be Element of NAT ; ::_thesis: for r, x being Real st 0 < r holds (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !) A1: abs (0 - 0) = 0 by ABSVALUE:2; let r, x be Real; ::_thesis: ( 0 < r implies (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !) ) assume r > 0 ; ::_thesis: (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !) 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 (Maclaurin (exp_R,].(- r),r.[,x)) . n = (x |^ n) / (n !) ; ::_thesis: verum end; theorem :: TAYLOR_2:9 for n being Element of NAT for r, x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !) proof let n be Element of NAT ; ::_thesis: for r, x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !) let r, x, s be Real; ::_thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !) ) assume that A1: x in ].(- r),r.[ and A2: 0 < s and A3: s < 1 ; ::_thesis: abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !) A4: abs ((s * x) - 0) = (abs s) * (abs x) by COMPLEX1:65 .= s * (abs x) by A2, ABSVALUE:def_1 ; x in ].(0 - r),(0 + r).[ by A1; then A5: abs (x - 0) < r by RCOMP_1:1; abs x >= 0 by COMPLEX1:46; then (abs 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; (n + 1) ! > 0 by NEWTON:17; then A7: abs ((n + 1) !) = (n + 1) ! by ABSVALUE:def_1; abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) = abs ((((exp_R | ].(- r),r.[) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) by Th6 .= abs (((exp_R . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) by A6, FUNCT_1:47 .= (abs ((exp_R . (s * x)) * (x |^ (n + 1)))) / (abs ((n + 1) !)) by COMPLEX1:67 .= ((abs (exp_R . (s * x))) * (abs (x |^ (n + 1)))) / ((n + 1) !) by A7, COMPLEX1:65 ; hence abs (((((diff (exp_R,].(- r),r.[)) . (n + 1)) . (s * x)) * (x |^ (n + 1))) / ((n + 1) !)) <= ((abs (exp_R . (s * x))) * ((abs x) |^ (n + 1))) / ((n + 1) !) by Th1; ::_thesis: verum end; theorem Th10: :: TAYLOR_2:10 for Z being open Subset of REAL for n being Element of NAT holds exp_R is_differentiable_on n,Z proof let Z be open Subset of REAL; ::_thesis: for n being Element of NAT holds exp_R is_differentiable_on n,Z let n be Element of NAT ; ::_thesis: exp_R is_differentiable_on n,Z let i be Element of NAT ; :: according to TAYLOR_1:def_6 ::_thesis: ( not i <= n - 1 or (diff (exp_R,Z)) . i is_differentiable_on Z ) assume i <= n - 1 ; ::_thesis: (diff (exp_R,Z)) . i is_differentiable_on Z reconsider i = i as Element of NAT ; A1: for x being 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; ::_thesis: ( x in Z implies ((diff (exp_R,Z)) . i) | Z is_differentiable_in x ) assume x in Z ; ::_thesis: ((diff (exp_R,Z)) . i) | Z is_differentiable_in x hence ((diff (exp_R,Z)) . i) | Z is_differentiable_in x by A2, A3, FDIFF_1:def_6; ::_thesis: verum end; dom ((diff (exp_R,Z)) . i) = dom (exp_R | Z) by Th6 .= Z by Th5 ; hence (diff (exp_R,Z)) . i is_differentiable_on Z by A1, FDIFF_1:def_6; ::_thesis: verum end; theorem Th11: :: TAYLOR_2:11 for r being Real st 0 < r holds ex M, L being Real st ( 0 <= M & 0 <= L & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex M, L being Real st ( 0 <= M & 0 <= L & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ) ) ) assume A1: r > 0 ; ::_thesis: ex M, L being Real st ( 0 <= M & 0 <= L & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ) ) take M = exp_R . r; ::_thesis: ex L being Real st ( 0 <= M & 0 <= L & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ) ) take L = r; ::_thesis: ( 0 <= M & 0 <= L & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ) ) now__::_thesis:_for_n_being_Element_of_NAT_ for_x,_s_being_Real_st_x_in_].(-_r),r.[_&_0_<_s_&_s_<_1_holds_ abs_(((((diff_(exp_R,].(-_r),r.[))_._n)_._(s_*_x))_*_(x_|^_n))_/_(n_!))_<=_(M_*_(L_|^_n))_/_(n_!) let n be Element of NAT ; ::_thesis: for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) now__::_thesis:_for_x,_s_being_Real_st_x_in_].(-_r),r.[_&_0_<_s_&_s_<_1_holds_ abs_(((((diff_(exp_R,].(-_r),r.[))_._n)_._(s_*_x))_*_(x_|^_n))_/_(n_!))_<=_(M_*_(L_|^_n))_/_(n_!) A2: for a, b being Real st 0 <= a & a <= b holds for n being Element of NAT holds ( 0 <= a |^ n & a |^ n <= b |^ n ) proof let a, b be Real; ::_thesis: ( 0 <= a & a <= b implies for n being Element of NAT holds ( 0 <= a |^ n & a |^ n <= b |^ n ) ) assume that A3: 0 <= a and A4: a <= b ; ::_thesis: for n being Element of NAT holds ( 0 <= a |^ n & a |^ n <= b |^ n ) defpred S1[ Element of NAT ] means ( 0 <= a |^ \$1 & a |^ \$1 <= b |^ \$1 ); A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] 0 * a <= (a |^ k) * a by A3, A6; hence a |^ (k + 1) >= 0 by NEWTON:6; ::_thesis: a |^ (k + 1) <= b |^ (k + 1) ( b |^ (k + 1) = (b |^ k) * b & (a |^ k) * a <= (b |^ k) * b ) by A3, A4, A6, NEWTON:6, XREAL_1:66; hence a |^ (k + 1) <= b |^ (k + 1) by NEWTON:6; ::_thesis: verum end; b |^ 0 = 1 by NEWTON:4; then A7: S1[ 0 ] by NEWTON:4; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A5); hence for n being Element of NAT holds ( 0 <= a |^ n & a |^ n <= b |^ n ) ; ::_thesis: verum end; let x, s be Real; ::_thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ) assume that A8: x in ].(- r),r.[ and A9: 0 < s and A10: s < 1 ; ::_thesis: abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) x in ].(0 - r),(0 + r).[ by A8; then A11: abs (x - 0) < r by RCOMP_1:1; abs x >= 0 by COMPLEX1:46; then A12: (abs x) |^ n <= L |^ n by A11, A2; A13: n ! > 0 by NEWTON:17; abs x >= 0 by COMPLEX1:46; then s * (abs x) < 1 * r by A9, A10, A11, XREAL_1:97; then (abs s) * (abs x) < r by A9, ABSVALUE:def_1; then abs ((s * x) - 0) < r by COMPLEX1:65; then A14: s * x in ].(0 - r),(0 + r).[ by RCOMP_1:1; then A15: abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) = abs (((exp_R . (s * x)) * (x |^ n)) / (n !)) by Th7 .= abs ((exp_R . (s * x)) * ((x |^ n) / (n !))) by XCMPLX_1:74 .= (abs (exp_R . (s * x))) * (abs ((x |^ n) / (n !))) by COMPLEX1:65 ; exp_R . (s * x) >= 0 by SIN_COS:54; then A16: ( r in ([#] REAL) /\ (dom exp_R) & abs (exp_R . (s * x)) = exp_R . (s * x) ) by ABSVALUE:def_1, TAYLOR_1:16; for x0 being Real holds 0 <= diff (exp_R,x0) by TAYLOR_1:16; then A17: exp_R | ([#] REAL) is non-decreasing by FDIFF_2:39, TAYLOR_1:16; abs ((x |^ n) / (n !)) = (abs (x |^ n)) / (abs (n !)) by COMPLEX1:67 .= (abs (x |^ n)) / (n !) by A13, ABSVALUE:def_1 .= ((abs x) |^ n) / (n !) by Th1 ; then A18: abs ((x |^ n) / (n !)) <= (L |^ n) / (n !) by A13, A12, XREAL_1:72; A19: ( abs (exp_R . (s * x)) >= 0 & abs ((x |^ n) / (n !)) >= 0 ) by COMPLEX1:46; s * x in { p where p is Real : ( - r < p & p < r ) } by A14, RCOMP_1:def_2; then ex g being Real st ( g = s * x & - r < g & g < r ) ; then abs (exp_R . (s * x)) <= M by A17, A16, RFUNCT_2:24, TAYLOR_1:16; then abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= M * ((L |^ n) / (n !)) by A19, A18, A15, XREAL_1:66; hence abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) by XCMPLX_1:74; ::_thesis: verum end; hence for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ; ::_thesis: verum end; hence ( 0 <= M & 0 <= L & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) ) ) by A1, SIN_COS:54; ::_thesis: verum end; theorem Th12: :: TAYLOR_2:12 for M, L being Real st M >= 0 & L >= 0 holds 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 proof 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__::_thesis:_for_m_being_Element_of_NAT_st_n_<=_m_holds_ (M_*_(L_|^_m))_/_(m_!)_<_p 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 end; theorem Th13: :: TAYLOR_2:13 for r, e being Real st 0 < r & 0 < e holds ex n being Element of NAT st for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e proof let r, e be Real; ::_thesis: ( 0 < r & 0 < e implies ex n being Element of NAT st for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) assume that A1: 0 < r and A2: 0 < e ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e consider M, L being Real such that A3: ( M >= 0 & L >= 0 ) and A4: for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (M * (L |^ n)) / (n !) by A1, Th11; consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds (M * (L |^ m)) / (m !) < e by A2, A3, Th12; take n ; ::_thesis: for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e let m be Element of NAT ; ::_thesis: ( n <= m implies for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) assume n <= m ; ::_thesis: for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e then A6: (M * (L |^ m)) / (m !) < e by A5; let x, s be Real; ::_thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) assume ( x in ].(- r),r.[ & 0 < s & s < 1 ) ; ::_thesis: abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e then abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) <= (M * (L |^ m)) / (m !) by A4; hence abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e by A6, XXREAL_0:2; ::_thesis: verum end; theorem :: TAYLOR_2:14 for r, e being Real st 0 < r & 0 < e holds ex n being Element of NAT st for m being Element of NAT st n <= m holds for x being real number st x in ].(- r),r.[ holds abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e proof let r, e be Real; ::_thesis: ( 0 < r & 0 < e implies ex n being Element of NAT st for m being Element of NAT st n <= m holds for x being real number st x in ].(- r),r.[ holds abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e ) assume that A1: r > 0 and A2: e > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds for x being real number st x in ].(- r),r.[ holds abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds abs (((((diff (exp_R,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e by A1, A2, Th13; take n ; ::_thesis: for m being Element of NAT st n <= m holds for x being real number st x in ].(- r),r.[ holds abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e let m be Element of NAT ; ::_thesis: ( n <= m implies for x being real number st x in ].(- r),r.[ holds abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e ) assume A4: n <= m ; ::_thesis: for x being real number st x in ].(- r),r.[ holds abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e now__::_thesis:_for_x_being_Real_st_x_in_].(-_r),r.[_holds_ abs_((exp_R_._x)_-_((Partial_Sums_(Maclaurin_(exp_R,].(-_r),r.[,x)))_._m))_<_e m <= m + 1 by NAT_1:11; then A5: n <= m + 1 by A4, XXREAL_0:2; let x be Real; ::_thesis: ( x in ].(- r),r.[ implies abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e ) assume A6: x in ].(- r),r.[ ; ::_thesis: abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e ex s being Real st ( 0 < s & s < 1 & abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) = abs (((((diff (exp_R,].(- r),r.[)) . (m + 1)) . (s * x)) * (x |^ (m + 1))) / ((m + 1) !)) ) by A1, A6, Th4, Th10, SIN_COS:47; hence abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e by A3, A6, A5; ::_thesis: verum end; hence for x being real number st x in ].(- r),r.[ holds abs ((exp_R . x) - ((Partial_Sums (Maclaurin (exp_R,].(- r),r.[,x))) . m)) < e ; ::_thesis: verum end; theorem Th15: :: TAYLOR_2:15 for x being Real holds x rExpSeq is absolutely_summable proof let x be Real; ::_thesis: x rExpSeq is absolutely_summable for n being Element of NAT holds abs ((x rExpSeq) . n) = ((abs x) rExpSeq) . n proof let n be Element of NAT ; ::_thesis: abs ((x rExpSeq) . n) = ((abs x) rExpSeq) . n A1: n ! > 0 by NEWTON:17; abs ((x rExpSeq) . n) = abs ((x |^ n) / (n !)) by SIN_COS:def_5 .= (abs (x |^ n)) / (abs (n !)) by COMPLEX1:67 .= (abs (x |^ n)) / (n !) by A1, ABSVALUE:def_1 .= ((abs x) |^ n) / (n !) by Th1 .= ((abs x) rExpSeq) . n by SIN_COS:def_5 ; hence abs ((x rExpSeq) . n) = ((abs x) rExpSeq) . n ; ::_thesis: verum end; then (abs x) rExpSeq = abs (x rExpSeq) by SEQ_1:12; then abs (x rExpSeq) is summable by SIN_COS:45; hence x rExpSeq is absolutely_summable by SERIES_1:def_4; ::_thesis: verum end; theorem :: TAYLOR_2:16 for r, x being 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: abs (0 - 0) = 0 by ABSVALUE:2; let r, x be Real; ::_thesis: ( 0 < r implies ( 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)) ) ) assume r > 0 ; ::_thesis: ( 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)) ) then 0 in ].(0 - r),(0 + r).[ by A1, RCOMP_1:1; then A2: 0 in dom (exp_R | ].(- r),r.[) by Th5; now__::_thesis:_for_t_being_set_st_t_in_NAT_holds_ (Maclaurin_(exp_R,].(-_r),r.[,x))_._t_=_(x_rExpSeq)_._t let t be set ; ::_thesis: ( t in NAT implies (Maclaurin (exp_R,].(- r),r.[,x)) . t = (x rExpSeq) . t ) assume t in NAT ; ::_thesis: (Maclaurin (exp_R,].(- r),r.[,x)) . t = (x rExpSeq) . t 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 ; ::_thesis: verum end; then Maclaurin (exp_R,].(- r),r.[,x) = x rExpSeq by FUNCT_2:12; hence ( 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)) ) by Th15, SIN_COS:def_22; ::_thesis: verum end; theorem Th17: :: TAYLOR_2:17 for Z being open Subset of REAL holds ( sin `| Z = cos | Z & cos `| Z = (- sin) | Z & dom (sin | Z) = Z & dom (cos | Z) = Z ) proof let Z be open Subset of REAL; ::_thesis: ( sin `| Z = cos | Z & cos `| Z = (- sin) | Z & dom (sin | Z) = Z & dom (cos | Z) = Z ) 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 being Real st x in Z holds (sin `| Z) . x = (cos | Z) . x proof let x be Real; ::_thesis: ( x in Z implies (sin `| Z) . x = (cos | Z) . x ) assume A5: x in Z ; ::_thesis: (sin `| Z) . x = (cos | Z) . x (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 (sin `| Z) . x = (cos | Z) . x ; ::_thesis: verum 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 being Real st x in Z holds (cos `| Z) . x = ((- sin) | Z) . x proof let x be Real; ::_thesis: ( x in Z implies (cos `| Z) . x = ((- sin) | Z) . x ) assume A10: x in Z ; ::_thesis: (cos `| Z) . x = ((- sin) | Z) . x 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 (cos `| Z) . x = ((- sin) | Z) . x ; ::_thesis: verum end; dom (sin `| Z) = Z by A3, FDIFF_1:def_7; hence ( sin `| Z = cos | Z & cos `| Z = (- sin) | Z & dom (sin | Z) = Z & dom (cos | Z) = Z ) by A8, A1, A2, A4, A7, A9, PARTFUN1:5; ::_thesis: verum end; theorem :: TAYLOR_2:18 for f being PartFunc of REAL,REAL for Z being Subset of REAL st f is_differentiable_on Z holds (- f) `| Z = - (f `| Z) proof let f be PartFunc of REAL,REAL; ::_thesis: for Z being Subset of REAL st f is_differentiable_on Z holds (- f) `| Z = - (f `| Z) let Z be Subset of REAL; ::_thesis: ( f is_differentiable_on Z implies (- f) `| Z = - (f `| Z) ) assume A1: f is_differentiable_on Z ; ::_thesis: (- f) `| Z = - (f `| 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 (- f) `| Z = - (f `| Z) ; ::_thesis: verum end; theorem Th19: :: TAYLOR_2:19 for Z being open Subset of REAL for n being Element of 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 Z be open Subset of REAL; ::_thesis: for n being Element of 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) ) let n be Element of NAT ; ::_thesis: ( (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) ) A1: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; defpred S1[ Element of 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 being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] 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 S1[k + 1] by A6, A8, A9; ::_thesis: verum 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: S1[ 0 ] by A11, A12, A10; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A13, A3); hence ( (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) ) ; ::_thesis: verum end; theorem Th20: :: TAYLOR_2:20 for n being Element of NAT for r, x being 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: abs (0 - 0) = 0 by ABSVALUE:2; let n be Element of NAT ; ::_thesis: for r, x being 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 ) let r, x be Real; ::_thesis: ( r > 0 implies ( (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 ) ) assume r > 0 ; ::_thesis: ( (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 ) 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 ( (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 ) by A5, A8, A10; ::_thesis: verum end; theorem Th21: :: TAYLOR_2:21 for Z being open Subset of REAL for n being Element of NAT holds ( sin is_differentiable_on n,Z & cos is_differentiable_on n,Z ) proof let Z be open Subset of REAL; ::_thesis: for n being Element of NAT holds ( sin is_differentiable_on n,Z & cos is_differentiable_on n,Z ) let n be Element of NAT ; ::_thesis: ( sin is_differentiable_on n,Z & cos is_differentiable_on n,Z ) now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_n_-_1_holds_ (diff_(sin,Z))_._i_is_differentiable_on_Z let i be Element of NAT ; ::_thesis: ( i <= n - 1 implies (diff (sin,Z)) . i is_differentiable_on Z ) assume i <= n - 1 ; ::_thesis: (diff (sin,Z)) . i is_differentiable_on Z A1: now__::_thesis:_dom_((diff_(sin,Z))_._i)_=_Z percases ( i is even or i is odd ) ; suppose i is even ; ::_thesis: dom ((diff (sin,Z)) . i) = Z then consider j being Element of 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 ; ::_thesis: verum end; suppose i is odd ; ::_thesis: dom ((diff (sin,Z)) . i) = Z then consider j being Element of 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 ; ::_thesis: verum end; end; end; for x being Real st x in Z holds ((diff (sin,Z)) . i) | Z is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ((diff (sin,Z)) . i) | Z is_differentiable_in x ) assume A4: x in Z ; ::_thesis: ((diff (sin,Z)) . i) | Z is_differentiable_in x now__::_thesis:_(diff_(sin,Z))_._i_is_differentiable_in_x percases ( i is even or i is odd ) ; suppose i is even ; ::_thesis: (diff (sin,Z)) . i is_differentiable_in x then consider j being Element of 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; ::_thesis: verum end; suppose i is odd ; ::_thesis: (diff (sin,Z)) . i is_differentiable_in x then consider j being Element of 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; ::_thesis: verum end; end; end; hence ((diff (sin,Z)) . i) | Z is_differentiable_in x by A1, RELAT_1:68; ::_thesis: verum end; hence (diff (sin,Z)) . i is_differentiable_on Z by A1, FDIFF_1:def_6; ::_thesis: verum end; hence sin is_differentiable_on n,Z by TAYLOR_1:def_6; ::_thesis: cos is_differentiable_on n,Z now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_n_-_1_holds_ (diff_(cos,Z))_._i_is_differentiable_on_Z let i be Element of NAT ; ::_thesis: ( i <= n - 1 implies (diff (cos,Z)) . i is_differentiable_on Z ) assume i <= n - 1 ; ::_thesis: (diff (cos,Z)) . i is_differentiable_on Z A9: now__::_thesis:_dom_((diff_(cos,Z))_._i)_=_Z percases ( i is even or i is odd ) ; suppose i is even ; ::_thesis: dom ((diff (cos,Z)) . i) = Z then consider j being Element of 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 ; ::_thesis: verum end; suppose i is odd ; ::_thesis: dom ((diff (cos,Z)) . i) = Z then consider j being Element of 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 ; ::_thesis: verum end; end; end; for x being Real st x in Z holds ((diff (cos,Z)) . i) | Z is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ((diff (cos,Z)) . i) | Z is_differentiable_in x ) assume A12: x in Z ; ::_thesis: ((diff (cos,Z)) . i) | Z is_differentiable_in x now__::_thesis:_(diff_(cos,Z))_._i_is_differentiable_in_x percases ( i is even or i is odd ) ; suppose i is even ; ::_thesis: (diff (cos,Z)) . i is_differentiable_in x then consider j being Element of 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; ::_thesis: verum end; suppose i is odd ; ::_thesis: (diff (cos,Z)) . i is_differentiable_in x then consider j being Element of 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; ::_thesis: verum end; end; end; hence ((diff (cos,Z)) . i) | Z is_differentiable_in x by A9, RELAT_1:68; ::_thesis: verum end; hence (diff (cos,Z)) . i is_differentiable_on Z by A9, FDIFF_1:def_6; ::_thesis: verum end; hence cos is_differentiable_on n,Z by TAYLOR_1:def_6; ::_thesis: verum end; theorem Th22: :: TAYLOR_2:22 for r being Real st r > 0 holds ex r1, r2 being Real st ( r1 >= 0 & r2 >= 0 & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) ) proof let r be Real; ::_thesis: ( r > 0 implies ex r1, r2 being Real st ( r1 >= 0 & r2 >= 0 & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) ) ) assume A1: r > 0 ; ::_thesis: ex r1, r2 being Real st ( r1 >= 0 & r2 >= 0 & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) ) take r1 = 1; ::_thesis: ex r2 being Real st ( r1 >= 0 & r2 >= 0 & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) ) take r2 = r; ::_thesis: ( r1 >= 0 & r2 >= 0 & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) ) now__::_thesis:_for_n_being_Element_of_NAT_ for_x,_s_being_Real_st_x_in_].(-_r),r.[_&_s_>_0_&_s_<_1_holds_ (_abs_(((((diff_(sin,].(-_r),r.[))_._n)_._(s_*_x))_*_(x_|^_n))_/_(n_!))_<=_(r1_*_(r2_|^_n))_/_(n_!)_&_abs_(((((diff_(cos,].(-_r),r.[))_._n)_._(s_*_x))_*_(x_|^_n))_/_(n_!))_<=_(r1_*_(r2_|^_n))_/_(n_!)_) let n be Element of NAT ; ::_thesis: for x, s being Real st x in ].(- r),r.[ & s > 0 & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) let x, s be Real; ::_thesis: ( x in ].(- r),r.[ & s > 0 & s < 1 implies ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) assume that A2: x in ].(- r),r.[ and A3: s > 0 and A4: s < 1 ; ::_thesis: ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) x in ].(0 - r),(0 + r).[ by A2; then A5: abs (x - 0) < r by RCOMP_1:1; A6: ((abs x) |^ n) / (n !) <= (r2 |^ n) / (n !) proof defpred S1[ Element of NAT ] means ((abs x) |^ \$1) / (\$1 !) <= (r2 |^ \$1) / (\$1 !); A7: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A8: S1[k] ; ::_thesis: S1[k + 1] A9: ((abs x) |^ (k + 1)) / ((k + 1) !) = (((abs x) |^ k) * (abs x)) / ((k + 1) !) by NEWTON:6 .= (((abs x) |^ k) * (abs x)) / ((k !) * (k + 1)) by NEWTON:15 .= ((abs x) |^ k) * ((abs x) / ((k !) * (k + 1))) by XCMPLX_1:74 .= ((abs x) |^ k) * (((abs x) / (k !)) / (k + 1)) by XCMPLX_1:78 .= ((abs x) |^ k) * ((1 / ((k !) / (abs x))) / (k + 1)) by XCMPLX_1:57 .= ((abs x) |^ k) * (((1 / (k !)) * (abs x)) / (k + 1)) by XCMPLX_1:82 .= (((abs x) |^ k) * ((1 / (k !)) * (abs x))) / (k + 1) by XCMPLX_1:74 .= ((((abs x) |^ k) * (1 / (k !))) * (abs x)) / (k + 1) .= (((((abs x) |^ k) * 1) / (k !)) * (abs x)) / (k + 1) by XCMPLX_1:74 .= ((((abs x) |^ k) / (k !)) * (abs x)) / (k + 1) ; A10: k ! > 0 by NEWTON:17; ((abs x) |^ k) / (k !) = (abs (x |^ k)) / (k !) by Th1 .= (abs (x |^ k)) / (abs (k !)) by A10, ABSVALUE:def_1 .= abs ((x |^ k) / (k !)) by COMPLEX1:67 ; then A11: ((abs x) |^ k) / (k !) >= 0 by COMPLEX1:46; A12: (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) ; abs x >= 0 by COMPLEX1:46; then (((abs x) |^ k) / (k !)) * (abs x) <= ((r2 |^ k) / (k !)) * r2 by A5, A8, A11, XREAL_1:66; hence S1[k + 1] by A9, A12, XREAL_1:72; ::_thesis: verum end; ((abs x) |^ 0) / (0 !) = 1 / (0 !) by NEWTON:4 .= (r2 |^ 0) / (0 !) by NEWTON:4 ; then A13: S1[ 0 ] ; for i being Element of NAT holds S1[i] from NAT_1:sch_1(A13, A7); hence ((abs x) |^ n) / (n !) <= (r2 |^ n) / (n !) ; ::_thesis: verum end; abs x >= 0 by COMPLEX1:46; then s * (abs x) < 1 * r by A3, A4, A5, XREAL_1:97; then (abs s) * (abs x) < r by A3, ABSVALUE:def_1; then abs ((s * x) - 0) < r by COMPLEX1:65; then A14: s * x in ].(0 - r),(0 + r).[ by RCOMP_1:1; A15: for k being Element of NAT holds abs ((- 1) |^ k) = 1 proof let k be Element of NAT ; ::_thesis: abs ((- 1) |^ k) = 1 percases ( k is even or k is odd ) ; suppose k is even ; ::_thesis: abs ((- 1) |^ k) = 1 then consider j being Element of NAT such that A16: k = 2 * j by ABIAN:def_2; thus abs ((- 1) |^ k) = abs (((- 1) |^ (1 + 1)) |^ j) by A16, NEWTON:9 .= abs ((((- 1) |^ 1) * (- 1)) |^ j) by NEWTON:6 .= abs (((- 1) * (- 1)) |^ j) by NEWTON:5 .= abs 1 by NEWTON:10 .= 1 by ABSVALUE:def_1 ; ::_thesis: verum end; suppose k is odd ; ::_thesis: abs ((- 1) |^ k) = 1 then consider j being Element of NAT such that A17: k = (2 * j) + 1 by ABIAN:9; thus abs ((- 1) |^ k) = abs (((- 1) |^ (2 * j)) * (- 1)) by A17, NEWTON:6 .= abs ((((- 1) |^ (1 + 1)) |^ j) * (- 1)) by NEWTON:9 .= abs (((((- 1) |^ 1) * (- 1)) |^ j) * (- 1)) by NEWTON:6 .= abs ((((- 1) * (- 1)) |^ j) * (- 1)) by NEWTON:5 .= abs (1 * (- 1)) by NEWTON:10 .= abs 1 by COMPLEX1:52 .= 1 by ABSVALUE:def_1 ; ::_thesis: verum end; end; end; A18: abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1 proof percases ( n is even or n is odd ) ; suppose n is even ; ::_thesis: abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1 then consider k being Element of NAT such that A19: n = 2 * k by ABIAN:def_2; A20: dom (((- 1) |^ k) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def_5 .= ].(- r),r.[ by Th17 ; A21: s * x in dom (sin | ].(- r),r.[) by A14, Th17; A22: abs (sin (s * x)) <= 1 by SIN_COS:27; abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (sin | ].(- r),r.[)) . (s * x)) by A19, Th19 .= abs (((- 1) |^ k) * ((sin | ].(- r),r.[) . (s * x))) by A14, A20, VALUED_1:def_5 .= (abs ((- 1) |^ k)) * (abs ((sin | ].(- r),r.[) . (s * x))) by COMPLEX1:65 .= 1 * (abs ((sin | ].(- r),r.[) . (s * x))) by A15 .= abs (sin . (s * x)) by A21, FUNCT_1:47 ; hence abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1 by A22, SIN_COS:def_17; ::_thesis: verum end; suppose n is odd ; ::_thesis: abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1 then consider k being Element of NAT such that A23: n = (2 * k) + 1 by ABIAN:9; A24: dom (((- 1) |^ k) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def_5 .= ].(- r),r.[ by Th17 ; A25: s * x in dom (cos | ].(- r),r.[) by A14, Th17; A26: abs (cos (s * x)) <= 1 by SIN_COS:27; abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)) by A23, Th19 .= abs (((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))) by A14, A24, VALUED_1:def_5 .= (abs ((- 1) |^ k)) * (abs ((cos | ].(- r),r.[) . (s * x))) by COMPLEX1:65 .= 1 * (abs ((cos | ].(- r),r.[) . (s * x))) by A15 .= abs (cos . (s * x)) by A25, FUNCT_1:47 ; hence abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) <= r1 by A26, SIN_COS:def_19; ::_thesis: verum end; end; end; A27: abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1 proof percases ( n is even or n is odd ) ; suppose n is even ; ::_thesis: abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1 then consider k being Element of NAT such that A28: n = 2 * k by ABIAN:def_2; A29: dom (((- 1) |^ k) (#) (cos | ].(- r),r.[)) = dom (cos | ].(- r),r.[) by VALUED_1:def_5 .= ].(- r),r.[ by Th17 ; A30: s * x in dom (cos | ].(- r),r.[) by A14, Th17; A31: abs (cos (s * x)) <= 1 by SIN_COS:27; abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) = abs ((((- 1) |^ k) (#) (cos | ].(- r),r.[)) . (s * x)) by A28, Th19 .= abs (((- 1) |^ k) * ((cos | ].(- r),r.[) . (s * x))) by A14, A29, VALUED_1:def_5 .= (abs ((- 1) |^ k)) * (abs ((cos | ].(- r),r.[) . (s * x))) by COMPLEX1:65 .= 1 * (abs ((cos | ].(- r),r.[) . (s * x))) by A15 .= abs (cos . (s * x)) by A30, FUNCT_1:47 ; hence abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1 by A31, SIN_COS:def_19; ::_thesis: verum end; suppose n is odd ; ::_thesis: abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1 then consider k being Element of NAT such that A32: n = (2 * k) + 1 by ABIAN:9; A33: dom (((- 1) |^ (k + 1)) (#) (sin | ].(- r),r.[)) = dom (sin | ].(- r),r.[) by VALUED_1:def_5 .= ].(- r),r.[ by Th17 ; A34: s * x in dom (sin | ].(- r),r.[) by A14, Th17; A35: abs (sin (s * x)) <= 1 by SIN_COS:27; abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) = abs ((((- 1) |^ (k + 1)) (#) (sin | ].(- r),r.[)) . (s * x)) by A32, Th19 .= abs (((- 1) |^ (k + 1)) * ((sin | ].(- r),r.[) . (s * x))) by A14, A33, VALUED_1:def_5 .= (abs ((- 1) |^ (k + 1))) * (abs ((sin | ].(- r),r.[) . (s * x))) by COMPLEX1:65 .= 1 * (abs ((sin | ].(- r),r.[) . (s * x))) by A15 .= abs (sin . (s * x)) by A34, FUNCT_1:47 ; hence abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) <= r1 by A35, SIN_COS:def_17; ::_thesis: verum end; end; end; A36: n ! > 0 by NEWTON:17; A37: abs ((x |^ n) / (n !)) = (abs (x |^ n)) / (abs (n !)) by COMPLEX1:67 .= (abs (x |^ n)) / (n !) by A36, ABSVALUE:def_1 .= ((abs x) |^ n) / (n !) by Th1 ; then A38: ((abs x) |^ n) / (n !) >= 0 by COMPLEX1:46; A39: abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) = abs ((((diff (cos,].(- r),r.[)) . n) . (s * x)) * ((x |^ n) / (n !))) by XCMPLX_1:74 .= (abs (((diff (cos,].(- r),r.[)) . n) . (s * x))) * (abs ((x |^ n) / (n !))) by COMPLEX1:65 .= ((abs (((diff (cos,].(- r),r.[)) . n) . (s * x))) * ((abs x) |^ n)) / (n !) by A37, XCMPLX_1:74 ; A40: abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) = abs ((((diff (sin,].(- r),r.[)) . n) . (s * x)) * ((x |^ n) / (n !))) by XCMPLX_1:74 .= (abs (((diff (sin,].(- r),r.[)) . n) . (s * x))) * (abs ((x |^ n) / (n !))) by COMPLEX1:65 .= ((abs (((diff (sin,].(- r),r.[)) . n) . (s * x))) * ((abs x) |^ n)) / (n !) by A37, XCMPLX_1:74 ; abs (((diff (cos,].(- r),r.[)) . n) . (s * x)) >= 0 by COMPLEX1:46; then A41: (abs (((diff (cos,].(- r),r.[)) . n) . (s * x))) * (((abs x) |^ n) / (n !)) <= r1 * ((r2 |^ n) / (n !)) by A38, A27, A6, XREAL_1:66; abs (((diff (sin,].(- r),r.[)) . n) . (s * x)) >= 0 by COMPLEX1:46; then (abs (((diff (sin,].(- r),r.[)) . n) . (s * x))) * (((abs x) |^ n) / (n !)) <= r1 * ((r2 |^ n) / (n !)) by A38, A18, A6, XREAL_1:66; hence ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) by A40, A39, A41, XCMPLX_1:74; ::_thesis: verum end; hence ( r1 >= 0 & r2 >= 0 & ( for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) ) ) by A1; ::_thesis: verum end; theorem Th23: :: TAYLOR_2:23 for r, e being Real st 0 < r & 0 < e holds ex n being Element of NAT st for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) proof let r, e be Real; ::_thesis: ( 0 < r & 0 < e implies ex n being Element of NAT st for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) ) assume that A1: r > 0 and A2: e > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) consider r1, r2 being Real such that A3: ( r1 >= 0 & r2 >= 0 ) and A4: for n being Element of NAT for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) & abs (((((diff (cos,].(- r),r.[)) . n) . (s * x)) * (x |^ n)) / (n !)) <= (r1 * (r2 |^ n)) / (n !) ) by A1, Th22; consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds (r1 * (r2 |^ m)) / (m !) < e by A2, A3, Th12; take n ; ::_thesis: for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) let m be Element of NAT ; ::_thesis: ( n <= m implies for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) ) assume n <= m ; ::_thesis: for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) then A6: (r1 * (r2 |^ m)) / (m !) < e by A5; let x, s be Real; ::_thesis: ( x in ].(- r),r.[ & 0 < s & s < 1 implies ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) ) assume ( x in ].(- r),r.[ & 0 < s & s < 1 ) ; ::_thesis: ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) then ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) <= (r1 * (r2 |^ m)) / (m !) & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) <= (r1 * (r2 |^ m)) / (m !) ) by A4; hence ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) by A6, XXREAL_0:2; ::_thesis: verum end; theorem :: TAYLOR_2:24 for r, e being Real st 0 < r & 0 < e holds ex n being Element of NAT st for m being Element of NAT st n <= m holds for x being real number st x in ].(- r),r.[ holds ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) proof let r, e be Real; ::_thesis: ( 0 < r & 0 < e implies ex n being Element of NAT st for m being Element of NAT st n <= m holds for x being real number st x in ].(- r),r.[ holds ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) ) assume that A1: r > 0 and A2: e > 0 ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds for x being real number st x in ].(- r),r.[ holds ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) consider n being Element of NAT such that A3: for m being Element of NAT st n <= m holds for x, s being Real st x in ].(- r),r.[ & 0 < s & s < 1 holds ( abs (((((diff (sin,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e & abs (((((diff (cos,].(- r),r.[)) . m) . (s * x)) * (x |^ m)) / (m !)) < e ) by A1, A2, Th23; take n ; ::_thesis: for m being Element of NAT st n <= m holds for x being real number st x in ].(- r),r.[ holds ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) let m be Element of NAT ; ::_thesis: ( n <= m implies for x being real number st x in ].(- r),r.[ holds ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) ) assume A4: n <= m ; ::_thesis: for x being real number st x in ].(- r),r.[ holds ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) 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__::_thesis:_for_x_being_Real_st_x_in_].(-_r),r.[_holds_ (_abs_((sin_._x)_-_((Partial_Sums_(Maclaurin_(sin,].(-_r),r.[,x)))_._m))_<_e_&_abs_((cos_._x)_-_((Partial_Sums_(Maclaurin_(cos,].(-_r),r.[,x)))_._m))_<_e_) m <= m + 1 by NAT_1:11; then A7: n <= m + 1 by A4, XXREAL_0:2; let x be Real; ::_thesis: ( x in ].(- r),r.[ implies ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) ) assume A8: x in ].(- r),r.[ ; ::_thesis: ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) ex s being Real st ( 0 < s & s < 1 & abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) = abs (((((diff (sin,].(- r),r.[)) . (m + 1)) . (s * x)) * (x |^ (m + 1))) / ((m + 1) !)) ) by A1, A6, A8, Th4; hence abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e by A3, A8, A7; ::_thesis: abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ex s being Real st ( 0 < s & s < 1 & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) = abs (((((diff (cos,].(- r),r.[)) . (m + 1)) . (s * x)) * (x |^ (m + 1))) / ((m + 1) !)) ) by A1, A5, A8, Th4; hence abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e by A3, A8, A7; ::_thesis: verum end; hence for x being real number st x in ].(- r),r.[ holds ( abs ((sin . x) - ((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m)) < e & abs ((cos . x) - ((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m)) < e ) ; ::_thesis: verum end; theorem Th25: :: TAYLOR_2:25 for r, x being Real for m being Element of 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; ::_thesis: for m being Element of 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 ) let m be Element of NAT ; ::_thesis: ( 0 < r implies ( (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 ) ) assume A1: r > 0 ; ::_thesis: ( (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 ) thus (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) + 1) = (Partial_Sums (x P_sin)) . m ::_thesis: (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) + 1) = (Partial_Sums (x P_cos)) . m proof defpred S1[ Element of NAT ] means (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * \$1) + 1) = (Partial_Sums (x P_sin)) . \$1; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] (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 S1[k + 1] ; ::_thesis: verum 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: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2); hence (Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . ((2 * m) + 1) = (Partial_Sums (x P_sin)) . m ; ::_thesis: verum end; defpred S1[ Element of NAT ] means (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * \$1) + 1) = (Partial_Sums (x P_cos)) . \$1; A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: S1[k] ; ::_thesis: S1[k + 1] (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 S1[k + 1] ; ::_thesis: verum 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: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A7, A5); hence (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . ((2 * m) + 1) = (Partial_Sums (x P_cos)) . m ; ::_thesis: verum end; theorem Th26: :: TAYLOR_2:26 for r, x being Real for m being Element of 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; ::_thesis: for m being Element of 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 ) let m be Element of NAT ; ::_thesis: ( 0 < r & m > 0 implies ( (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 ) ) assume that A1: r > 0 and A2: m > 0 ; ::_thesis: ( (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 ) 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 ( (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 ) by A5; ::_thesis: verum end; theorem Th27: :: TAYLOR_2:27 for r, x being Real for m being Element of 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; ::_thesis: for m being Element of NAT st 0 < r holds (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m let m be Element of NAT ; ::_thesis: ( 0 < r implies (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m ) assume A1: r > 0 ; ::_thesis: (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m defpred S1[ Element of NAT ] means (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * \$1) = (Partial_Sums (x P_cos)) . \$1; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] 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 ; ::_thesis: verum 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: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A2); hence (Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . (2 * m) = (Partial_Sums (x P_cos)) . m ; ::_thesis: verum end; theorem :: TAYLOR_2:28 for r, x being 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; ::_thesis: ( r > 0 implies ( 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)) ) ) assume A1: r > 0 ; ::_thesis: ( 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)) ) 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 number st p > 0 holds ex n1 being Element of NAT st for m1 being Element of NAT st m1 >= n1 holds abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p proof let p be real number ; ::_thesis: ( p > 0 implies ex n1 being Element of NAT st for m1 being Element of NAT st m1 >= n1 holds abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p ) assume p > 0 ; ::_thesis: ex n1 being Element of NAT st for m1 being Element of NAT st m1 >= n1 holds abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p then consider n being Element of NAT such that A5: for m being Element of NAT st n <= m holds abs (((Partial_Sums (x P_sin)) . m) - (sin . x)) < p by A2, A3, SEQ_2:def_7; set n1 = (2 * n) + 2; for m1 being Element of NAT st m1 >= (2 * n) + 2 holds abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p proof let m1 be Element of NAT ; ::_thesis: ( m1 >= (2 * n) + 2 implies abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p ) assume A6: m1 >= (2 * n) + 2 ; ::_thesis: abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p percases ( m1 is even or m1 is odd ) ; suppose m1 is even ; ::_thesis: abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p then consider j being Element of 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 abs (((Partial_Sums (x P_sin)) . (j - 1)) - (sin . x)) < p by A5, A9; hence abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p by A1, A7, A8, Th26; ::_thesis: verum end; suppose m1 is odd ; ::_thesis: abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p then consider j being Element of 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, XREAL_1:9; then n * 2 <= j * 2 by XXREAL_0:2; then (n * 2) / 2 <= (j * 2) / 2 by XREAL_1:72; then abs (((Partial_Sums (x P_sin)) . j) - (sin . x)) < p by A5; hence abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p by A1, A10, Th25; ::_thesis: verum end; end; end; hence ex n1 being Element of NAT st for m1 being Element of NAT st m1 >= n1 holds abs (((Partial_Sums (Maclaurin (sin,].(- r),r.[,x))) . m1) - (sin . x)) < p ; ::_thesis: verum 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 number st p > 0 holds ex n1 being Element of NAT st for m1 being Element of NAT st m1 >= n1 holds abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p proof let p be real number ; ::_thesis: ( p > 0 implies ex n1 being Element of NAT st for m1 being Element of NAT st m1 >= n1 holds abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p ) assume p > 0 ; ::_thesis: ex n1 being Element of NAT st for m1 being Element of NAT st m1 >= n1 holds abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p then consider n being Element of NAT such that A15: for m being Element of NAT st n <= m holds abs (((Partial_Sums (x P_cos)) . m) - (cos . x)) < p by A12, A13, SEQ_2:def_7; set n1 = (2 * n) + 1; for m1 being Element of NAT st m1 >= (2 * n) + 1 holds abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p proof let m1 be Element of NAT ; ::_thesis: ( m1 >= (2 * n) + 1 implies abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p ) assume A16: m1 >= (2 * n) + 1 ; ::_thesis: abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p percases ( m1 is even or m1 is odd ) ; suppose m1 is even ; ::_thesis: abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p then consider j being Element of 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 abs (((Partial_Sums (x P_cos)) . j) - (cos . x)) < p by A15; hence abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p by A1, A17, Th27; ::_thesis: verum end; suppose m1 is odd ; ::_thesis: abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p then consider j being Element of 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 abs (((Partial_Sums (x P_cos)) . j) - (cos . x)) < p by A15; hence abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p by A1, A18, Th25; ::_thesis: verum end; end; end; hence ex n1 being Element of NAT st for m1 being Element of NAT st m1 >= n1 holds abs (((Partial_Sums (Maclaurin (cos,].(- r),r.[,x))) . m1) - (cos . x)) < p ; ::_thesis: verum 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 ( 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)) ) by A4, A11, A14, SEQ_2:def_6, SERIES_1:def_3; ::_thesis: verum end;