taylor_2.miz



    begin

    reserve Z for open Subset of REAL ;

    theorem :: TAYLOR_2:1

    

     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;

      :: TAYLOR_2:def1

      func Maclaurin (f,Z,a) -> Real_Sequence equals ( Taylor (f,Z, 0 ,a));

      coherence ;

    end

    theorem :: TAYLOR_2:2

    

     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.[) holds for x be Real st x in ].( - r), r.[ holds 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 :: TAYLOR_2:3

    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).[) holds for x be Real st x in ].(x0 - r), (x0 + r).[ holds 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 :: TAYLOR_2:4

    

     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.[) holds for x be Real st x in ].( - r), r.[ holds 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 be 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 :: TAYLOR_2:5

    

     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 :: TAYLOR_2:6

    

     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 :: TAYLOR_2:7

    

     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 :: TAYLOR_2:8

    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 :: TAYLOR_2:9

    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 :: TAYLOR_2:10

    

     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 :: TAYLOR_2:11

    

     Th11: for r be Real st 0 < r holds ex M,L be Real st 0 <= M & 0 <= L & 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 ! ))

    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 holds 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 be Real : ( - r) < p & p < r } by A13, RCOMP_1:def 2;

          then

          consider g be Real such that

           A19: g = (s * x) & ( - r) < g & g < r;

          reconsider g as Element of REAL by XREAL_0:def 1;

          g = (s * x) & ( - r) < g & g < r by A19;

          then |.( exp_R . (s * x)).| <= M by A16, A15, RFUNCT_2: 24, TAYLOR_1: 16;

          then |.((((( diff ( exp_R , ].( - r), r.[)) . n) . (s * x)) * (x |^ n)) / (n ! )).| <= (M * ((L |^ n) / (n ! ))) by A18, A17, A14, XREAL_1: 66;

          hence |.((((( diff ( exp_R , ].( - r), r.[)) . n) . (s * x)) * (x |^ n)) / (n ! )).| <= ((M * (L |^ n)) / (n ! )) by XCMPLX_1: 74;

        end;

        hence 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 ! ));

      end;

      hence thesis by A1, SIN_COS: 54;

    end;

    theorem :: TAYLOR_2:12

    

     Th12: for M,L be Real st M >= 0 & L >= 0 holds for e be Real st e > 0 holds 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 :: TAYLOR_2:13

    

     Th13: for r,e be Real st 0 < r & 0 < e holds ex n be Nat st for m be Nat st n <= m holds 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 :: TAYLOR_2:14

    for r,e be Real st 0 < r & 0 < e holds ex n be Nat st for m be Nat st n <= m holds for x be 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 holds 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 :: TAYLOR_2:15

    

     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 :: TAYLOR_2:16

    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 :: TAYLOR_2:17

    

     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 :: TAYLOR_2:18

    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 :: TAYLOR_2:19

    

     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 :: TAYLOR_2:20

    

     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 :: TAYLOR_2:21

    

     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 :: TAYLOR_2:22

    

     Th22: for r be Real st r > 0 holds ex r1,r2 be Real st r1 >= 0 & r2 >= 0 & 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 ! ))

    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 :: TAYLOR_2:23

    

     Th23: for r,e be Real st 0 < r & 0 < e holds ex n be Nat st for m be Nat st n <= m holds 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 :: TAYLOR_2:24

    for r,e be Real st 0 < r & 0 < e holds ex n be Nat st for m be Nat st n <= m holds for x be 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 holds 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 :: TAYLOR_2:25

    

     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 :: TAYLOR_2:26

    

     Th26: for r,x be Real, m be 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 :: TAYLOR_2:27

    

     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 :: TAYLOR_2:28

    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 be Real st p > 0 holds ex n1 be Nat st for m1 be Nat st m1 >= n1 holds |.((( Partial_Sums ( Maclaurin ( sin , ].( - r), r.[,x))) . m1) - g).| < p

      proof

        let p be Real;

        assume p > 0 ;

        then

        consider n be Nat such that

         A5: for m be 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, XREAL_1: 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 be Real st p > 0 holds ex n1 be Nat st for m1 be Nat st m1 >= n1 holds |.((( Partial_Sums ( Maclaurin ( cos , ].( - r), r.[,x))) . m1) - g).| < p

      proof

        let p be Real;

        assume p > 0 ;

        then

        consider n be Nat such that

         A15: for m be 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;