leibniz1.miz

    begin

    reserve i,n,m for Nat,

r,s for Real,

A for non empty closed_interval Subset of REAL ;



     Lm1: tan is_differentiable_on ].( - ( PI / 2)), ( PI / 2).[

    proof

      r in ].( - ( PI / 2)), ( PI / 2).[ implies tan is_differentiable_in r

      proof

        assume r in ].( - ( PI / 2)), ( PI / 2).[;

        then ( cos . r) <> 0 by COMPTRIG: 11;

        hence thesis by FDIFF_7: 46;

      end;

      hence thesis by SIN_COS9: 1, FDIFF_1: 9;

    end;



     Lm2: r in ].( - ( PI / 2)), ( PI / 2).[ implies ( diff ( tan ,r)) = (1 / (( cos . r) ^2 ))

    proof

      assume r in ].( - ( PI / 2)), ( PI / 2).[;

      then ( cos . r) <> 0 by COMPTRIG: 11;

      hence thesis by FDIFF_7: 46;

    end;



     Lm3: r > 0 implies ex s be Real st 0 <= s < ( PI / 2) & ( tan . s) = r

    proof

      assume

       A1: r > 0 ;

      set e = (1 / (2 * r));

      set P = ( PI / 2);



       A2: P in REAL by XREAL_0:def 1;

      ( dom sin ) = REAL by FUNCT_2:def 1;

      then

      consider s1 be Real such that

       A3: 0 < s1 & for x1 be Real st x1 in ( dom sin ) & |.(x1 - P).| < s1 holds |.(( sin . x1) - ( sin . P)).| < (1 / 2) by A2, FCONT_1:def 2, FCONT_1: 3;



       A4: ( dom cos ) = REAL & ( dom sin ) = REAL by FUNCT_2:def 1;

      then

      consider s2 be Real such that

       A5: 0 < s2 & for x1 be Real st x1 in ( dom cos ) & |.(x1 - P).| < s2 holds |.(( cos . x1) - ( cos . P)).| < e by A1, FCONT_1: 3, A2, FCONT_1:def 2;

      set m = ( min (s1,s2)), M = ( min (m,( PI / 2))), m2 = (M / 2);

       0 < m & 0 < ( PI / 2) by A3, A5, XXREAL_0: 21;

      then

       A6: M > 0 by XXREAL_0: 21;

      then

       A7: m2 > 0 & m2 < M by XREAL_1: 216;

      set X = (P - m2);



       A8: X in REAL by XREAL_0:def 1;



       A9: X < P by A6, XREAL_1: 37;



       A10: |.(X - P).| = ( - (X - P)) by A6, ABSVALUE:def 1;



       A11: M <= m & M <= ( PI / 2) & m <= s1 & m <= s2 by XXREAL_0: 17;

      then M <= s1 & M <= s2 by XXREAL_0: 2;

      then

       A12: m2 < s1 & m2 < s2 & m2 < ( PI / 2) by A11, A7, XXREAL_0: 2;

      then

       A13: |.(( cos . X) - ( cos . P)).| < e by A10, A4, A5, XREAL_0:def 1;



       A14: X > 0 by A12, XREAL_1: 50;

      then X in ]. 0 , P.[ by A9, XXREAL_1: 4;

      then

       A15: ( cos . X) > 0 & ( cos . P) = 0 by SIN_COS: 80, SIN_COS: 77;

      ( cos . X) < e by A15, A13, ABSVALUE:def 1;

      then

       A16: (1 / ( cos . X)) > (1 / (1 / (2 * r))) & (1 / (1 / (2 * r))) = (2 * r) by XREAL_1: 76, A15;

      ( sin X) < 1 & ( sin . P) = 1 & ( sin X) = ( sin . X) by SIN_COS6: 30, A9, A14, SIN_COS: 77;

      then |.(( sin . X) - 1).| = ( - (( sin . X) - 1)) by ABSVALUE:def 1, XREAL_1: 49;

      then (1 - ( sin . X)) < (1 / 2) by SIN_COS: 77, A10, A3, A4, XREAL_0:def 1, A12;

      then ( sin . X) > (1 - (1 / 2)) by XREAL_1: 11;

      then

       A17: (( sin . X) / ( cos . X)) > ((1 / 2) / ( cos . X)) by A15, XREAL_1: 74;

      ((1 / 2) / ( cos . X)) > ((1 / 2) * (2 * r)) by A16, XREAL_1: 68;

      then

       A18: (( sin . X) / ( cos . X)) > r by A17, XXREAL_0: 2;

       not ( cos . X) in { 0 } by A15, TARSKI:def 1;

      then not X in ( cos " { 0 }) by FUNCT_1:def 7;

      then X in (( dom cos ) \ ( cos " { 0 })) by A8, A4, XBOOLE_0:def 5;

      then X in (( dom sin ) /\ (( dom cos ) \ ( cos " { 0 }))) by A4, XBOOLE_0:def 4;

      then X in ( dom tan ) by RFUNCT_1:def 1;

      then

       A19: ( tan . X) > r by A18, RFUNCT_1:def 1;



       A20: [. 0 , X.] c= ].( - P), P.[ by A9, XXREAL_1: 47;



       A21: ( tan | [. 0 , X.]) is continuous by A9, XXREAL_1: 47, SIN_COS9: 5, FCONT_1: 16;



       A22: [. 0 , X.] c= ( dom tan ) by A20, SIN_COS9: 1;

      r in [.( tan . 0 ), ( tan . X).] by A1, A19, XXREAL_1: 1, SIN_COS9: 41;

      then r in ( [.( tan . 0 ), ( tan . X).] \/ [.( tan . X), ( tan . 0 ).]) by XBOOLE_0:def 3;

      then

      consider s be Real such that

       A23: s in [. 0 , X.] & r = ( tan . s) by A21, A22, A14, FCONT_2: 15;



       A24: 0 <= s & s <= X by A23, XXREAL_1: 1;

      then s < P by A6, XREAL_1: 37;

      hence thesis by A23, A24;

    end;

    theorem :: LEIBNIZ1:1



     Th1: ( rng ( tan | ].( - ( PI / 2)), ( PI / 2).[)) = REAL

    proof

      set P = ( PI / 2), I = ].( - P), P.[;

       REAL c= ( rng ( tan | I))

      proof

        let r be object;

        assume r in REAL ;

        then

        reconsider r as Real;

        per cases ;

          suppose

           A1: r > 0 ;

          then

          consider s be Real such that

           A2: 0 <= s < P & ( tan . s) = r by Lm3;

          s in ( dom tan ) by A1, A2, FUNCT_1:def 2;

          hence thesis by XXREAL_1: 4, A2, FUNCT_1: 50;

        end;

          suppose

           A3: r < 0 ;

          then

          consider s be Real such that

           A4: 0 <= s < P & ( tan . s) = ( - r) by Lm3;



           A5: s in ( dom tan ) by A3, A4, FUNCT_1:def 2;



           A6: ( dom sin ) = REAL & ( dom cos ) = REAL by FUNCT_2:def 1;

          then ( dom tan ) = ( REAL /\ ( REAL \ ( cos " { 0 }))) by RFUNCT_1:def 1;

          then s in ( REAL \ ( cos " { 0 })) by A5, XBOOLE_0:def 4;

          then s in REAL & not s in ( cos " { 0 }) by XBOOLE_0:def 5;

          then not ( cos . s) in { 0 } by A6, FUNCT_1:def 7;

          then ( cos . s) <> 0 & ( cos . s) = ( cos . ( - s)) by TARSKI:def 1, SIN_COS: 30;

          then ( tan . s) = ( tan s) & ( tan . ( - s)) = ( tan ( - s)) & ( - ( tan s)) = ( tan ( - s)) by SIN_COS9: 15, SIN_COS4: 1;

          then

           A7: ( - s) in ( dom tan ) & ( tan . ( - s)) = r by A3, A4, FUNCT_1:def 2;

          P > ( - s) > ( - P) by A4, XREAL_1: 24;

          hence thesis by A7, FUNCT_1: 50, XXREAL_1: 4;

        end;

          suppose r = 0 ;

          then 0 in ( dom tan ) & ( tan . 0 ) = r & 0 in I by XXREAL_1: 1, SIN_COS: 70, SIN_COS9: 41, XXREAL_1: 4;

          hence thesis by FUNCT_1: 50;

        end;

      end;

      hence thesis by XBOOLE_0:def 10;

    end;

    registration

      cluster arctan -> total;

      coherence

      proof

        ( dom arctan ) = REAL by Th1, FUNCT_1: 33;

        hence thesis by PARTFUN1:def 2;

      end;

      cluster arctan -> differentiable;

      coherence

      proof

        ( tan .: ].( - ( PI / 2)), ( PI / 2).[) = ( rng ( tan | ].( - ( PI / 2)), ( PI / 2).[)) by RELAT_1: 115

        .= ( dom arctan ) by Th1, FUNCT_2:def 1;

        hence thesis by FDIFF_1:def 8, SIN_COS9: 71;

      end;

    end

    theorem :: LEIBNIZ1:2



     Th2: ( diff ( arctan ,r)) = (1 / (1 + (r ^2 )))

    proof

      set g = arctan ;

      set f = ( tan | ].( - ( PI / 2)), ( PI / 2).[);

      set x = ( arctan . r);



       A1: ((( sin . x) ^2 ) + (( cos . x) ^2 )) = 1 by SIN_COS: 28;



       A2: f is_differentiable_on ].( - ( PI / 2)), ( PI / 2).[ by Lm1, FDIFF_2: 16;

       A3:

      now



         A4: for x0 be Real st x0 in ].( - ( PI / 2)), ( PI / 2).[ holds (1 / (( cos . x0) ^2 )) > 0

        proof

          let x0 be Real;

          assume x0 in ].( - ( PI / 2)), ( PI / 2).[;

          then 0 < ( cos . x0) by COMPTRIG: 11;

          hence thesis;

        end;

        let x0 be Real such that

         A5: x0 in ].( - ( PI / 2)), ( PI / 2).[;

        ( diff (f,x0)) = ((f `| ].( - ( PI / 2)), ( PI / 2).[) . x0) by A2, A5, FDIFF_1:def 7

        .= (( tan `| ].( - ( PI / 2)), ( PI / 2).[) . x0) by Lm1, FDIFF_2: 16

        .= ( diff ( tan ,x0)) by A5, Lm1, FDIFF_1:def 7

        .= (1 / (( cos . x0) ^2 )) by A5, Lm2;

        hence 0 < ( diff (f,x0)) by A5, A4;

      end;



       A6: ( rng g) = ( dom f) & ( dom g) = ( rng f) by FUNCT_1: 33;

      set x = ( arctan . r);



       A7: ( dom arctan ) = REAL & r in REAL by FUNCT_2:def 1, XREAL_0:def 1;

      then

       A8: x in ( dom f) by A6, FUNCT_1:def 3;

      then

       A9: x in ].( - ( PI / 2)), ( PI / 2).[ by RELAT_1: 57;



       A10: ( cos x) <> 0 by A8, RELAT_1: 57, COMPTRIG: 11;



       A11: r = (f . x) by A7, A6, FUNCT_1: 32

      .= ( tan . x) by A8, FUNCT_1: 47

      .= ( tan x) by A10, SIN_COS9: 15

      .= (( sin x) / ( cos x)) by SIN_COS4:def 1;

      ( dom f) = (( dom tan ) /\ ].( - ( PI / 2)), ( PI / 2).[) by RELAT_1: 61;

      then

       A12: ].( - ( PI / 2)), ( PI / 2).[ c= ( dom f) by SIN_COS9: 1, XBOOLE_1: 19;



       A13: (f | ].( - ( PI / 2)), ( PI / 2).[) = f;

      (r * ( cos x)) = ( sin x) by A10, A11, XCMPLX_1: 87;

      then

       A14: 1 = ((( cos x) ^2 ) * ((r ^2 ) + 1)) by A1;

      f is_differentiable_on ].( - ( PI / 2)), ( PI / 2).[ by Lm1, FDIFF_2: 16;



      then ( diff (f,x)) = ((f `| ].( - ( PI / 2)), ( PI / 2).[) . x) by A9, FDIFF_1:def 7

      .= (( tan `| ].( - ( PI / 2)), ( PI / 2).[) . x) by Lm1, FDIFF_2: 16

      .= ( diff ( tan ,x)) by A9, Lm1, FDIFF_1:def 7

      .= (1 / (( cos x) ^2 )) by A8, RELAT_1: 57, Lm2;



      then ( diff (g,r)) = (1 / (1 / (( cos x) ^2 ))) by A2, A3, A13, A12, A7, FDIFF_2: 48

      .= (1 / ((r ^2 ) + 1)) by A14, XCMPLX_1: 73;

      hence thesis;

    end;

    theorem :: LEIBNIZ1:3



     Th3: for Z be open Subset of REAL holds arctan is_differentiable_on Z & for r st r in Z holds (( arctan `| Z) . r) = (1 / (1 + (r ^2 )))

    proof

      let Z be open Subset of REAL ;



       A1: ( dom arctan ) = REAL by FUNCT_2:def 1;



       A2: arctan is_differentiable_on Z by A1, FDIFF_1: 28;

      r in Z implies (( arctan `| Z) . r) = (1 / (1 + (r ^2 )))

      proof

        assume r in Z;



        hence (( arctan `| Z) . r) = ( diff ( arctan ,r)) by A2, FDIFF_1:def 7

        .= (1 / (1 + (r ^2 ))) by Th2;

      end;

      hence thesis by A1, FDIFF_1: 28;

    end;



     Lm4: ( #Z (n + m)) = (( #Z n) (#) ( #Z m))

    proof

      now

        let r;



        thus (( #Z (n + m)) . r) = (r #Z (n + m)) by TAYLOR_1:def 1

        .= ((r #Z n) * (r #Z m)) by TAYLOR_1: 1

        .= ((( #Z n) . r) * (r #Z m)) by TAYLOR_1:def 1

        .= ((( #Z n) . r) * (( #Z m) . r)) by TAYLOR_1:def 1

        .= ((( #Z n) (#) ( #Z m)) . r) by VALUED_1: 5;

      end;

      hence thesis;

    end;

    registration

      let n;

      cluster ( #Z n) -> continuous;

      coherence

      proof

        defpred P[ Nat] means ( #Z $1) is continuous;

        now

          let r;



          thus (( #Z 0 ) . r) = (r #Z 0 ) by TAYLOR_1:def 1

          .= 1 by PREPOWER: 34

          .= (( REAL --> 1) . r) by XREAL_0:def 1, FUNCOP_1: 7;

        end;

        then ( #Z 0 ) = ( REAL --> 1);

        then

         A1: P[ 0 ];



         A2: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat;

          assume

           A3: P[n];

          set Z1 = ( #Z 1);

          r in ( dom Z1) implies (Z1 . r) = r

          proof

            (Z1 . r) = (r #Z 1) by TAYLOR_1:def 1;

            hence thesis by PREPOWER: 35;

          end;

          then Z1 is continuous by FCONT_1: 40;

          then (Z1 (#) ( #Z n)) is continuous by A3;

          hence thesis by Lm4;

        end;

        for n holds P[n] from NAT_1:sch 2( A1, A2);

        hence thesis;

      end;

    end



     Lm5: ((( #Z 0 ) + ( #Z 2)) . r) = (1 + (r * r))

    proof



       A1: (r #Z 1) = r by PREPOWER: 35;

      r in REAL by XREAL_0:def 1;



      hence ((( #Z 0 ) + ( #Z 2)) . r) = ((( #Z 0 ) . r) + (( #Z 2) . r)) by VALUED_1: 1

      .= ((r #Z 0 ) + (( #Z 2) . r)) by TAYLOR_1:def 1

      .= ((r #Z 0 ) + (r #Z 2)) by TAYLOR_1:def 1

      .= (1 + (r #Z (1 + 1))) by PREPOWER: 34

      .= (1 + (r * r)) by A1, TAYLOR_1: 1;

    end;



     Lm6: ((( #Z 0 ) + ( #Z 2)) " { 0 }) = {}

    proof

      assume ((( #Z 0 ) + ( #Z 2)) " { 0 }) <> {} ;

      then

      consider x be object such that

       A1: x in ((( #Z 0 ) + ( #Z 2)) " { 0 }) by XBOOLE_0:def 1;

      reconsider x as Element of REAL by A1;

      ((( #Z 0 ) + ( #Z 2)) . x) in { 0 } by A1, FUNCT_1:def 7;



      then 0 = ((( #Z 0 ) + ( #Z 2)) . x) by TARSKI:def 1

      .= (1 + (x * x)) by Lm5;

      hence thesis;

    end;

    theorem :: LEIBNIZ1:4



     Th4: ( dom (( #Z n) / (( #Z 0 ) + ( #Z 2)))) = REAL & (( #Z n) / (( #Z 0 ) + ( #Z 2))) is continuous & ((( #Z n) / (( #Z 0 ) + ( #Z 2))) . r) = ((r |^ n) / (1 + (r ^2 )))

    proof

      set Z0 = ( #Z 0 ), Z2 = ( #Z 2), Zn = ( #Z n), f = (Zn / (Z0 + Z2));



       A1: ( dom Zn) = REAL = ( dom (Z0 + Z2)) by FUNCT_2:def 1;



      hence

       A2: ( dom f) = ( REAL /\ ( REAL \ {} )) by Lm6, RFUNCT_1:def 1

      .= REAL ;



       A3: (Zn | REAL ) is continuous & ((Z0 + Z2) | REAL ) is continuous;

       REAL c= (( dom Zn) /\ ( dom (Z0 + Z2))) by A1;

      then (f | REAL ) is continuous by Lm6, A3, FCONT_1: 24;

      hence f is continuous;

      (Zn . r) = (r #Z n) by TAYLOR_1:def 1

      .= (r |^ n) by PREPOWER: 36;



      hence (f . r) = ((r |^ n) * (((Z0 + Z2) . r) " )) by XREAL_0:def 1, A2, RFUNCT_1:def 1

      .= ((r |^ n) / (1 + (r ^2 ))) by Lm5;

    end;

    theorem :: LEIBNIZ1:5



     Th5: ( integral ((( #Z 0 ) / (( #Z 0 ) + ( #Z 2))),A)) = (( arctan . ( upper_bound A)) - ( arctan . ( lower_bound A)))

    proof

      set Z0 = ( #Z 0 ), Z2 = ( #Z 2), f = (Z0 / (Z0 + Z2));



       A1: ( dom f) = REAL by Th4;

      f is continuous by Th4;

      then

       A2: (f | A) is continuous;



       A3: r in REAL implies (f . r) = (1 / (1 + (r ^2 )))

      proof

        (r |^ 0 ) = 1 by NEWTON: 4;

        hence thesis by Th4;

      end;



       A4: ( [#] REAL ) is open;



       A5: ( dom arctan ) = REAL by FUNCT_2:def 1;



       A6: arctan is_differentiable_on REAL by A5, FDIFF_1:def 8;



       A7: for x be Element of REAL st x in ( dom ( arctan `| REAL )) holds (( arctan `| REAL ) . x) = (f . x)

      proof

        let x be Element of REAL ;

        assume x in ( dom ( arctan `| REAL ));

        (( arctan `| REAL ) . x) = (1 / (1 + (x ^2 ))) by Th3, A4

        .= (f . x) by A3;

        hence thesis;

      end;



       A8: ( arctan `| REAL ) = f by A6, A1, FDIFF_1:def 7, A7;

      f is_integrable_on A & (f | A) is bounded by A1, A2, INTEGRA5: 10, INTEGRA5: 11;

      hence thesis by A4, A8, INTEGRA5: 13, Th3;

    end;

    theorem :: LEIBNIZ1:6



     Th6: ( integral (((( - 1) |^ i) (#) (( #Z (2 * n)) / (( #Z 0 ) + ( #Z 2)))),A)) = (((( - 1) |^ i) * (((1 / ((2 * n) + 1)) * (( upper_bound A) |^ ((2 * n) + 1))) - ((1 / ((2 * n) + 1)) * (( lower_bound A) |^ ((2 * n) + 1))))) + ( integral (((( - 1) |^ (i + 1)) (#) (( #Z (2 * (n + 1))) / (( #Z 0 ) + ( #Z 2)))),A)))

    proof

      set II = (( - 1) |^ i), i1 = (i + 1), n1 = (n + 1), II1 = (( - 1) |^ i1);

      set Z0 = ( #Z 0 ), Z2 = ( #Z 2), Z2n = ( #Z (2 * n));

      set f = (II (#) Z2n);

      set g = (II1 (#) (( #Z (2 * n1)) / (Z0 + Z2)));



       A1: ( dom (Z2n / (Z0 + Z2))) = ( dom (II (#) (Z2n / (Z0 + Z2)))) by VALUED_1:def 5;

      ( dom (( #Z (2 * n1)) / (Z0 + Z2))) = ( dom (II1 (#) (( #Z (2 * n1)) / (Z0 + Z2)))) by VALUED_1:def 5;

      then

       A2: ( dom g) = REAL by Th4;



       A3: ( dom f) = REAL by FUNCT_2:def 1;

      then

       A4: ( dom (f + g)) = ( REAL /\ REAL ) by A2, VALUED_1:def 1;

      for x be Element of REAL holds ((II (#) (Z2n / (Z0 + Z2))) . x) = ((f + g) . x)

      proof

        let x be Element of REAL ;

        (x |^ (((2 * n) + 1) + 1)) = (x * (x |^ ((2 * n) + 1))) by NEWTON: 6

        .= (x * (x * (x |^ (2 * n)))) by NEWTON: 6;

        then ((x |^ (2 * n)) + (x |^ (2 * n1))) = ((x |^ (2 * n)) * (1 + (x ^2 )));

        then

         A5: (((x |^ (2 * n)) + (x |^ (2 * n1))) / (1 + (x ^2 ))) = (x |^ (2 * n)) by XCMPLX_1: 89;



         A6: ( - (II * ((x |^ (2 * n1)) / (1 + (x ^2 ))))) = ((( - 1) * II) * ((x |^ (2 * n1)) / (1 + (x ^2 ))))

        .= (II1 * ((x |^ (2 * n1)) / (1 + (x ^2 )))) by NEWTON: 6;

        (x |^ (2 * n)) = (x #Z (2 * n)) by PREPOWER: 36

        .= (Z2n . x) by TAYLOR_1:def 1;

        then

         A7: (II * (x |^ (2 * n))) = (f . x) by VALUED_1: 6;



         A8: (II1 * ((x |^ (2 * n1)) / (1 + (x ^2 )))) = (II1 * ((( #Z (2 * n1)) / (Z0 + Z2)) . x)) by Th4

        .= (g . x) by VALUED_1: 6;



        thus ((II (#) (Z2n / (Z0 + Z2))) . x) = (II * ((Z2n / (Z0 + Z2)) . x)) by VALUED_1: 6

        .= (II * ((x |^ (2 * n)) / (1 + (x ^2 )))) by Th4

        .= (II * ((x |^ (2 * n)) - ((x |^ (2 * n1)) / (1 + (x ^2 ))))) by A5

        .= ((II * (x |^ (2 * n))) + (II1 * ((x |^ (2 * n1)) / (1 + (x ^2 ))))) by A6

        .= ((f + g) . x) by A7, A8, A4, VALUED_1:def 1;

      end;

      then

       A9: (f + g) = (II (#) (Z2n / (Z0 + Z2))) by A1, Th4, A4;



       A10: ( dom Z2n) = REAL by FUNCT_2:def 1;

      (f | A) is continuous & (Z2n | A) is continuous;

      then

       A11: f is_integrable_on A & (f | A) is bounded & Z2n is_integrable_on A & (Z2n | A) is bounded by A10, INTEGRA5: 10, INTEGRA5: 11, A3;

      (( #Z (2 * n1)) / (Z0 + Z2)) is continuous by Th4;

      then (g | A) is continuous;

      then

       A12: g is_integrable_on A & (g | A) is bounded by INTEGRA5: 10, INTEGRA5: 11, A2;



       A13: (2 * n) in NAT by ORDINAL1:def 12;



      thus ( integral ((II (#) (Z2n / (Z0 + Z2))),A)) = (( integral (f,A)) + ( integral (g,A))) by A3, A2, A11, A12, A9, INTEGRA6: 11

      .= ((II * ( integral (Z2n,A))) + ( integral (g,A))) by A10, A11, INTEGRA6: 9

      .= ((II * (((1 / ((2 * n) + 1)) * (( upper_bound A) |^ ((2 * n) + 1))) - ((1 / ((2 * n) + 1)) * (( lower_bound A) |^ ((2 * n) + 1))))) + ( integral (g,A))) by INTEGRA9: 19, A13;

    end;

    theorem :: LEIBNIZ1:7



     Th7: A = [. 0 , r.] & r >= 0 implies |.( integral ((( #Z (2 * n)) / (( #Z 0 ) + ( #Z 2))),A)).| <= ((1 / ((2 * n) + 1)) * (r |^ ((2 * n) + 1)))

    proof

      set Z0 = ( #Z 0 ), Z2 = ( #Z 2), N = (2 * n), Zn = ( #Z N), f = (Zn / (Z0 + Z2));

      assume

       A1: A = [. 0 , r.] & r >= 0 ;



       A2: f is continuous & ( dom f) = REAL by Th4;

      then ( dom (f | A)) = A by RELAT_1: 62;

      then (f | A) is total by PARTFUN1:def 2;

      then

      reconsider fA = (f || A) as Function of A, REAL ;



       A3: (f | A) is continuous by A2;

      then

       A4: (f | A) is bounded & f is_integrable_on A & (fA | A) = (f | A) by INTEGRA5: 11, INTEGRA5: 10, A2;



       A5: fA is integrable by A3, INTEGRA5:def 1, INTEGRA5: 11, A2;



       A6: Zn is continuous & ( dom Zn) = REAL by FUNCT_2:def 1;

      then ( dom (Zn | A)) = A by RELAT_1: 62;

      then (Zn | A) is total by PARTFUN1:def 2;

      then

      reconsider ZnA = (Zn || A) as Function of A, REAL ;



       A7: (Zn | A) is continuous;

      then

       A8: (Zn | A) is bounded & Zn is_integrable_on A & (ZnA | A) = (Zn | A) by INTEGRA5: 11, INTEGRA5: 10, A6;



       A9: ZnA is integrable by A7, INTEGRA5:def 1, INTEGRA5: 11, A6;

      for r st r in A holds (fA . r) <= (ZnA . r)

      proof

        let r;

        assume r in A;

        then

         A10: (fA . r) = (f . r) & (ZnA . r) = (Zn . r) by FUNCT_1: 49;



         A11: (Zn . r) = (r #Z N) by TAYLOR_1:def 1

        .= (r |^ N) by PREPOWER: 36;



         A12: (r |^ N) >= 0 by POWER: 3;

        ((r ^2 ) + 1) >= (1 + 0 ) by XREAL_1: 6;

        then (1 / (1 + (r ^2 ))) <= 1 by XREAL_1: 183;

        then (((r |^ N) * 1) / (1 + (r ^2 ))) <= ((r |^ N) * 1) by A12, XREAL_1: 64;

        hence thesis by A11, Th4, A10;

      end;

      then

       A13: ( integral fA) <= ( integral ZnA) by A4, A5, A8, A9, INTEGRA2: 34;



       A14: ( integral (f,A)) = ( integral fA) by INTEGRA5:def 2;



       A15: ( lower_bound A) = 0 & ( upper_bound A) = r by A1, JORDAN5A: 19;



       A16: N in NAT by ORDINAL1:def 12;

      ( 0 |^ (N + 1)) = 0 by NEWTON: 84;

      then

       A17: ((1 / (N + 1)) * ( 0 |^ (N + 1))) = 0 ;



       A18: ( integral ZnA) = ( integral (Zn,A)) by INTEGRA5:def 2

      .= (((1 / (N + 1)) * (r |^ (N + 1))) - 0 ) by A16, A15, A17, INTEGRA9: 19;



       A19: ( dom ( abs f)) = ( dom f) by VALUED_1:def 11;

      for x be object st x in REAL holds (f . x) = (( abs f) . x)

      proof

        let x be object;

        assume x in REAL ;

        then

        reconsider r = x as Element of REAL ;

        N = (n + n);

        then

         A20: (r |^ N) = ((r |^ n) * (r |^ n)) by NEWTON: 8;



         A21: (f . r) = ((r |^ N) / (1 + (r ^2 ))) by Th4;



        thus (( abs f) . x) = |.(f . r).| by A2, A19, VALUED_1:def 11

        .= (f . x) by A20, A21, ABSVALUE:def 1;

      end;

      then

       A22: ( abs f) = f by A19, A2;

       |.( integral (f,A)).| <= ( integral (( abs f),A)) by A2, INTEGRA6: 7, A4;

      hence thesis by A13, A14, A18, XXREAL_0: 2, A22;

    end;

    begin

    definition

      let a be Real_Sequence;

      :: LEIBNIZ1:def1

      func alternating_series a -> Real_Sequence means

      : Def1: (it . i) = ((( - 1) |^ i) * (a . i));

      existence

      proof

        defpred P[ Nat, object] means $2 = ((( - 1) |^ $1) * (a . $1));



         A1: for x be Element of NAT holds ex y be Element of REAL st P[x, y]

        proof

          let x be Element of NAT ;

          ((( - 1) |^ x) * (a . x)) in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider f be Function of NAT , REAL such that

         A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        let i be Nat;

        i in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let a1,a2 be Real_Sequence such that

         A3: for i be Nat holds (a1 . i) = ((( - 1) |^ i) * (a . i)) and

         A4: for i be Nat holds (a2 . i) = ((( - 1) |^ i) * (a . i));

        now

          let x be object;

          assume x in NAT ;

          then

          reconsider i = x as Nat;



          thus (a1 . x) = ((( - 1) |^ i) * (a . i)) by A3

          .= (a2 . x) by A4;

        end;

        hence thesis;

      end;

    end

    theorem :: LEIBNIZ1:8



     Th8: for a be Real_Sequence st a is nonnegative-yielding non-increasing convergent & ( lim a) = 0 holds ( alternating_series a) is summable & for n holds (( Partial_Sums ( alternating_series a)) . (2 * n)) >= ( Sum ( alternating_series a)) >= (( Partial_Sums ( alternating_series a)) . ((2 * n) + 1))

    proof

      let a be Real_Sequence such that

       A1: a is nonnegative-yielding non-increasing convergent & ( lim a) = 0 ;

      set A = ( alternating_series a), P = ( Partial_Sums A);

      defpred Sp[ Nat, object] means $2 = (P . (2 * $1));

      defpred Sn[ Nat, object] means $2 = (P . ((2 * $1) + 1));



       A2: for x be Element of NAT holds ex y be Element of REAL st Sp[x, y];



       A3: for x be Element of NAT holds ex y be Element of REAL st Sn[x, y];

      consider Sp be Function of NAT , REAL such that

       A4: for x be Element of NAT holds Sp[x, (Sp . x)] from FUNCT_2:sch 3( A2);

      consider Sn be Function of NAT , REAL such that

       A5: for x be Element of NAT holds Sn[x, (Sn . x)] from FUNCT_2:sch 3( A3);



       A6: for n be Nat holds (Sn . n) <= (Sn . (n + 1))

      proof

        let n be Nat;

        set n1 = (n + 1);



         A7: n1 in NAT & n in NAT by ORDINAL1:def 12;



         A8: (Sn . (n + 1)) = (P . ((2 * n1) + 1)) by A5

        .= ((P . (((2 * n) + 1) + 1)) + (A . ((2 * n1) + 1))) by SERIES_1:def 1

        .= (((P . ((2 * n) + 1)) + (A . (2 * n1))) + (A . ((2 * n1) + 1))) by SERIES_1:def 1

        .= ((P . ((2 * n) + 1)) + ((A . (2 * n1)) + (A . ((2 * n1) + 1))));



         A9: (Sn . n) = (P . ((2 * n) + 1)) by A7, A5;



         A10: ((a . (2 * n1)) - (a . ((2 * n1) + 1))) >= 0 by XREAL_1: 48, A1, VALUED_1:def 16;

        (( - 1) |^ (2 * n1)) = 1 & (( - 1) |^ ((2 * n1) + 1)) = ( - 1);

        then (A . (2 * n1)) = (1 * (a . (2 * n1))) & (A . ((2 * n1) + 1)) = (( - 1) * (a . ((2 * n1) + 1))) by Def1;

        hence thesis by A10, A9, A8, XREAL_1: 31;

      end;

      then

       A11: Sn is non-decreasing by VALUED_1:def 15;



       A12: for n be Nat holds (Sp . n) >= (Sp . (n + 1))

      proof

        let n be Nat;

        set n1 = (n + 1);



         A13: n1 in NAT & n in NAT & (2 * n1) = (((2 * n) + 1) + 1) by ORDINAL1:def 12;



        then

         A14: (Sp . (n + 1)) = (P . (((2 * n) + 1) + 1)) by A4

        .= ((P . ((2 * n) + 1)) + (A . (((2 * n) + 1) + 1))) by SERIES_1:def 1

        .= (((P . (2 * n)) + (A . ((2 * n) + 1))) + (A . (((2 * n) + 1) + 1))) by SERIES_1:def 1

        .= ((P . (2 * n)) + ((A . ((2 * n) + 1)) + (A . (2 * n1))));



         A15: (Sp . n) = (P . (2 * n)) by A13, A4;

        (a . ((2 * n) + 1)) >= (a . (((2 * n) + 1) + 1)) by A1, VALUED_1:def 16;

        then

         A16: ((a . (2 * n1)) - (a . ((2 * n) + 1))) <= 0 by XREAL_1: 47;

        (( - 1) |^ (2 * n1)) = 1 & (( - 1) |^ ((2 * n) + 1)) = ( - 1);

        then (A . (2 * n1)) = (1 * (a . (2 * n1))) & (A . ((2 * n) + 1)) = (( - 1) * (a . ((2 * n) + 1))) by Def1;

        hence thesis by A15, A14, XREAL_1: 32, A16;

      end;

      then

       A17: Sp is non-increasing by VALUED_1:def 16;



       A18: for n be Nat holds (Sp . n) >= (Sn . n)

      proof

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then (Sp . n) = (P . (2 * n)) & (Sn . n) = (P . ((2 * n) + 1)) by A4, A5;

        then

         A19: (Sn . n) = ((Sp . n) + (A . ((2 * n) + 1))) by SERIES_1:def 1;

        ( dom a) = NAT by FUNCT_2:def 1;

        then (a . ((2 * n) + 1)) in ( rng a) by FUNCT_1:def 3;

        then

         A20: (a . ((2 * n) + 1)) >= 0 by A1, PARTFUN3:def 4;

        (( - 1) |^ ((2 * n) + 1)) = ( - 1);

        then (A . ((2 * n) + 1)) = (( - 1) * (a . ((2 * n) + 1))) by Def1;

        hence thesis by A19, XREAL_1: 32, A20;

      end;

      for n be Nat holds (Sp . n) > ((Sn . 0 ) - 1)

      proof

        let n be Nat;

        (Sp . n) >= (Sn . n) >= (Sn . 0 ) by A18, A6, VALUED_1:def 15, SEQM_3: 6;

        then (Sp . n) >= (Sn . 0 ) & (Sn . 0 ) > ((Sn . 0 ) - 1) by XXREAL_0: 2, XREAL_1: 44;

        hence thesis by XXREAL_0: 2;

      end;

      then

       A21: Sp is bounded_below by SEQ_2:def 4;



       A22: for n be Nat holds (Sn . n) < ((Sp . 0 ) + 1)

      proof

        let n be Nat;

        (Sn . n) <= (Sp . n) <= (Sp . 0 ) by A18, A12, VALUED_1:def 16, SEQM_3: 8;

        then (Sn . n) <= (Sp . 0 ) & (Sp . 0 ) < ((Sp . 0 ) + 1) by XXREAL_0: 2, XREAL_1: 29;

        hence thesis by XXREAL_0: 2;

      end;

      then

       A23: Sn is bounded_above by SEQ_2:def 3;

      deffunc double( Nat) = ((2 * $1) + 1);



       A24: for x be Element of NAT holds double(x) in NAT ;

      consider Double be Function of NAT , NAT such that

       A25: for x be Element of NAT holds (Double . x) = double(x) from FUNCT_2:sch 8( A24);

      reconsider Double1 = Double as ManySortedSet of NAT ;

      for n be Nat holds (Double . n) < (Double . (n + 1))

      proof

        let n be Nat;

        set n1 = (n + 1);

        n in NAT & n1 in NAT by ORDINAL1:def 12;

        then

         A26: (Double . n) = double(n) & (Double . n1) = double(n1) by A25;

        n < n1 by NAT_1: 13;

        then (2 * n) < (2 * n1) by XREAL_1: 97;

        hence thesis by A26, XREAL_1: 8;

      end;

      then

       A27: Double1 is increasing sequence of NAT by VALUED_1:def 13;



       A28: ( rng (a * Double1)) c= REAL ;

      ( rng Double) c= NAT & ( dom a) = NAT & ( dom Double) = NAT by FUNCT_2:def 1;

      then

       A29: ( dom (a * Double1)) = NAT by RELAT_1: 27;

      then

      reconsider aD = (a * Double1) as Real_Sequence by A28, FUNCT_2: 2;

      reconsider aD as subsequence of a by VALUED_0:def 17, A27;



       A30: aD is convergent & ( lim aD) = 0 by SEQ_4: 16, SEQ_4: 17, A1;



       A31: (Sp - Sn) is convergent & ( lim (Sp - Sn)) = (( lim Sp) - ( lim Sn)) by A21, A17, A23, A11, SEQ_2: 12;

      for x be object st x in NAT holds (aD . x) = ((Sp - Sn) . x)

      proof

        let x be object such that

         A32: x in NAT ;

        reconsider n = x as Element of NAT by A32;



         A33: (Double . n) = ((2 * n) + 1) by A25;

        ( dom (Sp - Sn)) = NAT by FUNCT_2:def 1;

        then

         A34: ((Sp - Sn) . n) = ((Sp . n) - (Sn . n)) by VALUED_1: 13;

        (Sp . n) = (P . (2 * n)) & (Sn . n) = (P . ((2 * n) + 1)) by A4, A5;

        then

         A35: (Sn . n) = ((Sp . n) + (A . ((2 * n) + 1))) by SERIES_1:def 1;

        (( - 1) |^ ((2 * n) + 1)) = ( - 1);

        then (A . ((2 * n) + 1)) = (( - 1) * (a . ((2 * n) + 1))) by Def1;

        hence thesis by A29, A34, A35, FUNCT_1: 12, A33;

      end;

      then

       A36: aD = (Sp - Sn);



       A37: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((P . m) - ( lim Sp)).| < p

      proof

        let p be Real such that

         A38: 0 < p;

        consider n1 be Nat such that

         A39: for m be Nat st n1 <= m holds |.((Sp . m) - ( lim Sp)).| < p by A38, A21, A17, SEQ_2:def 7;

        consider n2 be Nat such that

         A40: for m be Nat st n2 <= m holds |.((Sn . m) - ( lim Sp)).| < p by A38, A23, A11, SEQ_2:def 7, A36, A30, A31;

        set N = ( max ((2 * n1),((2 * n2) + 1)));

        reconsider N as Nat by XXREAL_0:def 10;

        take N;

        let m be Nat such that

         A41: N <= m;

        per cases ;

          suppose m is even;

          then

          consider m2 be Nat such that

           A42: m = (2 * m2) by ABIAN:def 2;

          (2 * n1) <= N by XXREAL_0: 25;

          then (2 * n1) <= (2 * m2) by A41, A42, XXREAL_0: 2;

          then n1 <= m2 by XREAL_1: 68;

          then

           A43: |.((Sp . m2) - ( lim Sp)).| < p by A39;

          m2 in NAT by ORDINAL1:def 12;

          hence thesis by A4, A43, A42;

        end;

          suppose m is odd;

          then

          consider m2 be Nat such that

           A44: m = ((2 * m2) + 1) by ABIAN: 9;

          ((2 * n2) + 1) <= N by XXREAL_0: 25;

          then ((2 * n2) + 1) <= ((2 * m2) + 1) by A41, A44, XXREAL_0: 2;

          then (2 * n2) <= (2 * m2) by XREAL_1: 6;

          then n2 <= m2 by XREAL_1: 68;

          then

           A45: |.((Sn . m2) - ( lim Sp)).| < p by A40;

          m2 in NAT by ORDINAL1:def 12;

          hence thesis by A45, A44, A5;

        end;

      end;

      hence A is summable by SERIES_1:def 2, SEQ_2:def 6;

      let n;

      n in NAT by ORDINAL1:def 12;

      then

       A46: (Sp . n) = (P . (2 * n)) & (Sn . n) = (P . ((2 * n) + 1)) by A4, A5;

      P is convergent by A37, SEQ_2:def 6;

      then ( lim P) = ( lim Sp) & ( lim P) = ( Sum A) by A37, SEQ_2:def 7, SERIES_1:def 3;

      hence thesis by A46, A11, A12, VALUED_1:def 16, A36, A30, A31, A22, SEQ_2:def 3, A21, SEQ_4: 37, SEQ_4: 38;

    end;

    begin

    definition

      let r;

      :: LEIBNIZ1:def2

      func Leibniz_Series_of r -> Real_Sequence means

      : Def2: (it . n) = (((( - 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1));

      existence

      proof

        defpred P[ Nat, object] means $2 = (((( - 1) |^ $1) * (r |^ ((2 * $1) + 1))) / ((2 * $1) + 1));



         A1: for n be Element of NAT holds ex y be Element of REAL st P[n, y]

        proof

          let n be Element of NAT ;

          (((( - 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1)) in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider f be Function of NAT , REAL such that

         A2: for x be Element of NAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        let i be Nat;

        i in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let a1,a2 be Real_Sequence such that

         A3: for i be Nat holds (a1 . i) = (((( - 1) |^ i) * (r |^ ((2 * i) + 1))) / ((2 * i) + 1)) and

         A4: for i be Nat holds (a2 . i) = (((( - 1) |^ i) * (r |^ ((2 * i) + 1))) / ((2 * i) + 1));

        now

          let y be object;

          assume y in NAT ;

          then

          reconsider i = y as Nat;



          thus (a1 . y) = (((( - 1) |^ i) * (r |^ ((2 * i) + 1))) / ((2 * i) + 1)) by A3

          .= (a2 . y) by A4;

        end;

        hence thesis;

      end;

    end

    definition

      :: LEIBNIZ1:def3

      func Leibniz_Series -> Real_Sequence equals ( Leibniz_Series_of 1);

      coherence ;

    end

    theorem :: LEIBNIZ1:9



     Th9: r in [.( - 1), 1.] implies ( abs ( Leibniz_Series_of r)) is nonnegative-yielding non-increasing convergent & ( lim ( abs ( Leibniz_Series_of r))) = 0

    proof

      set rL = ( Leibniz_Series_of r), A = ( abs rL);

      assume

       A1: r in [.( - 1), 1.];



       A2: ( dom A) = ( dom rL) & ( dom rL) = NAT by VALUED_1:def 11, FUNCT_2:def 1;

      thus A is nonnegative-yielding;



       A3: (A . n) = (( |.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1))

      proof

        ( - ( - 1)) = 1;

        then |.( - 1).| = 1 by ABSVALUE:def 1;

        then

         A4: |.(( - 1) |^ n).| = (1 |^ n) by TAYLOR_2: 1;



         A5: (A . n) = |.(rL . n).| by A2, VALUED_1:def 11, ORDINAL1:def 12;

        (rL . n) = (((( - 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1)) by Def2;



        hence (A . n) = ( |.((( - 1) |^ n) * (r |^ ((2 * n) + 1))).| / |.((2 * n) + 1).|) by COMPLEX1: 67, A5

        .= ((1 * |.(r |^ ((2 * n) + 1)).|) / |.((2 * n) + 1).|) by A4, COMPLEX1: 65

        .= ((1 * ( |.r.| |^ ((2 * n) + 1))) / |.((2 * n) + 1).|) by TAYLOR_2: 1

        .= (( |.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1)) by ABSVALUE:def 1;

      end;

      ( - 1) <= r <= 1 by A1, XXREAL_1: 1;

      then

       A6: |.r.| <= 1 by ABSVALUE: 5;

      (A . n) >= (A . (n + 1))

      proof

        set n1 = (n + 1);



         A7: (A . n1) = ((( |.r.| |^ ((2 * n1) + 1)) * 1) / ((2 * n1) + 1)) by A3;



         A8: |.r.| >= 0 by COMPLEX1: 46;

         |.(r |^ ((2 * n) + 1)).| = ( |.r.| |^ ((2 * n) + 1)) by TAYLOR_2: 1;

        then

         A9: ( |.r.| |^ ((2 * n) + 1)) >= 0 by COMPLEX1: 46;



         A10: ( |.r.| * |.r.|) <= (1 * 1) by A8, A6, XREAL_1: 66;

        ( |.r.| |^ ((2 * n1) + 1)) = ( |.r.| * ( |.r.| |^ (((2 * n) + 1) + 1))) by NEWTON: 6

        .= ( |.r.| * ( |.r.| * ( |.r.| |^ ((2 * n) + 1)))) by NEWTON: 6

        .= (( |.r.| * |.r.|) * ( |.r.| |^ ((2 * n) + 1)));

        then

         A11: ( |.r.| |^ ((2 * n1) + 1)) <= (( |.r.| |^ ((2 * n) + 1)) * 1) by A9, A10, XREAL_1: 66;

         |.(r |^ ((2 * n1) + 1)).| = ( |.r.| |^ ((2 * n1) + 1)) by TAYLOR_2: 1;

        then

         A12: ( |.r.| |^ ((2 * n1) + 1)) >= 0 by COMPLEX1: 46;

        ((2 * n) + 1) <= (((2 * n) + 1) + 1) by NAT_1: 13;

        then ((2 * n) + 1) < ((((2 * n) + 1) + 1) + 1) by NAT_1: 13;

        then (1 / ((2 * n) + 1)) >= (1 / ((2 * n1) + 1)) by XREAL_1: 76;

        then ((( |.r.| |^ ((2 * n) + 1)) * 1) / ((2 * n) + 1)) >= ((( |.r.| |^ ((2 * n1) + 1)) * 1) / ((2 * n1) + 1)) by A12, A11, XREAL_1: 66;

        hence thesis by A3, A7;

      end;

      hence A is non-increasing by VALUED_1:def 16;

      set C = ( seq_const 0 );



       A13: ( lim C) = 0 ;

      deffunc F( Nat) = ((1 / 2) / ($1 + (1 / 2)));

      consider f be Real_Sequence such that

       A14: (f . n) = F(n) from SEQ_1:sch 1;



       A15: f is convergent & ( lim f) = 0 by A14, SEQ_4: 31;

      (C . n) <= (A . n) <= (f . n)

      proof



         A17: |.r.| >= 0 by COMPLEX1: 46;



         A18: ( 0 |^ ((2 * n) + 1)) = 0 by NEWTON: 11, NAT_1: 11;

         |.r.| > 0 implies ( |.r.| |^ ((2 * n) + 1)) <= (1 |^ ((2 * n) + 1)) by A6, PREPOWER: 9;

        then

         A19: ( |.r.| |^ ((2 * n) + 1)) <= 1 by A18, A17;

         |.(r |^ ((2 * n) + 1)).| = ( |.r.| |^ ((2 * n) + 1)) by TAYLOR_2: 1;

        then

         A20: ( |.r.| |^ ((2 * n) + 1)) >= 0 by COMPLEX1: 46;

        (((2 * n) + 1) / 2) = (n + (1 / 2));



        then

         A21: (1 / ((2 * n) + 1)) = F(n) by XCMPLX_1: 55

        .= (f . n) by A14;

        (A . n) = (( |.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1)) by A3

        .= (( |.r.| |^ ((2 * n) + 1)) * (((2 * n) + 1) " ));

        hence thesis by A19, XREAL_1: 64, A20, A21;

      end;

      hence thesis by A13, A15, SEQ_2: 19, SEQ_2: 20;

    end;

    theorem :: LEIBNIZ1:10



     Th10: (r >= 0 implies ( alternating_series ( abs ( Leibniz_Series_of r))) = ( Leibniz_Series_of r)) & (r < 0 implies (( - 1) (#) ( alternating_series ( abs ( Leibniz_Series_of r)))) = ( Leibniz_Series_of r))

    proof

      set rL = ( Leibniz_Series_of r), A = ( abs rL), aA = ( alternating_series A);



       A1: ( dom A) = ( dom rL) & ( dom rL) = NAT by VALUED_1:def 11, FUNCT_2:def 1;



       A2: (aA . n) = ((( - 1) |^ n) * (( |.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1)))

      proof

        ( - ( - 1)) = 1;

        then |.( - 1).| = 1 by ABSVALUE:def 1;

        then

         A3: |.(( - 1) |^ n).| = (1 |^ n) by TAYLOR_2: 1;



         A4: (A . n) = |.(rL . n).| by A1, VALUED_1:def 11, ORDINAL1:def 12;

        (rL . n) = (((( - 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1)) by Def2;



        then (A . n) = ( |.((( - 1) |^ n) * (r |^ ((2 * n) + 1))).| / |.((2 * n) + 1).|) by COMPLEX1: 67, A4

        .= ((1 * |.(r |^ ((2 * n) + 1)).|) / |.((2 * n) + 1).|) by A3, COMPLEX1: 65

        .= ((1 * ( |.r.| |^ ((2 * n) + 1))) / |.((2 * n) + 1).|) by TAYLOR_2: 1

        .= (( |.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1)) by ABSVALUE:def 1;

        hence thesis by Def1;

      end;

      thus r >= 0 implies aA = rL

      proof

        assume r >= 0 ;

        then

         A5: |.r.| = r by ABSVALUE:def 1;

        now

          let n;



          thus (aA . n) = ((( - 1) |^ n) * ((r |^ ((2 * n) + 1)) / ((2 * n) + 1))) by A2, A5

          .= (((( - 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1))

          .= (rL . n) by Def2;

        end;

        hence thesis;

      end;

      assume r < 0 ;

      then

       A6: |.r.| = ( - r) by ABSVALUE:def 1;

      now

        let n;

        ( |.r.| |^ ((2 * n) + 1)) = ( - (r |^ ((2 * n) + 1))) by A6, POWER: 2;



        then (aA . n) = ((( - 1) |^ n) * (( - (r |^ ((2 * n) + 1))) / ((2 * n) + 1))) by A2

        .= ( - (((( - 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1)))

        .= ( - (rL . n)) by Def2;



        hence (rL . n) = (( - 1) * (aA . n))

        .= ((( - 1) (#) aA) . n) by SEQ_1: 9;

      end;

      hence thesis;

    end;

    theorem :: LEIBNIZ1:11



     Th11: r in [.( - 1), 1.] implies ( Leibniz_Series_of r) is summable

    proof

      set rL = ( Leibniz_Series_of r), A = ( abs rL), aA = ( alternating_series A);

      assume r in [.( - 1), 1.];

      then A is nonnegative-yielding non-increasing convergent & ( lim A) = 0 by Th9;

      then

       A1: aA is summable by Th8;

      per cases ;

        suppose r >= 0 ;

        hence thesis by Th10, A1;

      end;

        suppose r < 0 ;

        then rL = (( - 1) (#) aA) by Th10;

        hence thesis by A1, SERIES_1: 10;

      end;

    end;

    theorem :: LEIBNIZ1:12



     Th12: A = [. 0 , r.] & r >= 0 implies ( arctan . r) = ((( Partial_Sums ( Leibniz_Series_of r)) . n) + ( integral (((( - 1) |^ (n + 1)) (#) (( #Z (2 * (n + 1))) / (( #Z 0 ) + ( #Z 2)))),A)))

    proof

      set Z0 = ( #Z 0 ), Z2 = ( #Z 2), rL = ( Leibniz_Series_of r);

      assume A = [. 0 , r.] & r >= 0 ;

      then

       A1: ( upper_bound A) = r & ( lower_bound A) = 0 by JORDAN5A: 19;

      defpred P[ Nat] means ( arctan . r) = ((( Partial_Sums rL) . $1) + ( integral (((( - 1) |^ ($1 + 1)) (#) (( #Z (2 * ($1 + 1))) / (Z0 + Z2))),A)));



       A2: P[ 0 ]

      proof



         A3: ( integral ((Z0 / (Z0 + Z2)),A)) = (( arctan . r) - ( arctan . 0 )) by Th5, A1

        .= ( arctan . r) by SIN_COS9: 43;



         A4: ((2 * 0 ) + 1) = 1;



         A5: ((( - 1) |^ 0 ) * ((1 * (r |^ 1)) - ((1 / 1) * ( 0 |^ 1)))) = ((( - 1) |^ 0 ) * ((r |^ 1) / 1))

        .= (rL . 0 ) by A4, Def2;

        (( - 1) |^ 0 ) = 1 by NEWTON: 4;

        then ((( - 1) |^ 0 ) (#) (Z0 / (Z0 + Z2))) = (Z0 / (Z0 + Z2)) by RFUNCT_1: 21;

        then ( arctan . r) = ((rL . 0 ) + ( integral (((( - 1) |^ ( 0 + 1)) (#) (( #Z (2 * ( 0 + 1))) / (( #Z 0 ) + ( #Z 2)))),A))) by A3, A1, A4, Th6, A5;

        hence thesis by SERIES_1:def 1;

      end;



       A6: P[i] implies P[(i + 1)]

      proof

        set i1 = (i + 1), i11 = (i1 + 1);

        assume

         A7: P[i];



         A8: ( 0 |^ ((2 * i1) + 1)) = 0 by NEWTON: 11, NAT_1: 11;

        ((( - 1) |^ i1) * (((1 / ((2 * i1) + 1)) * (r |^ ((2 * i1) + 1))) - ((1 / ((2 * i1) + 1)) * 0 ))) = (((( - 1) |^ i1) * (r |^ ((2 * i1) + 1))) / ((2 * i1) + 1))

        .= (rL . i1) by Def2;

        then ( integral (((( - 1) |^ i1) (#) (( #Z (2 * i1)) / (Z0 + Z2))),A)) = ((rL . i1) + ( integral (((( - 1) |^ i11) (#) (( #Z (2 * i11)) / (Z0 + Z2))),A))) by A8, Th6, A1;

        then ( arctan . r) = (((( Partial_Sums rL) . i) + (rL . i1)) + ( integral (((( - 1) |^ i11) (#) (( #Z (2 * i11)) / (Z0 + Z2))),A))) by A7;

        hence thesis by SERIES_1:def 1;

      end;

       P[i] from NAT_1:sch 2( A2, A6);

      hence thesis;

    end;

    theorem :: LEIBNIZ1:13



     Th13: 0 <= r <= 1 implies ( arctan . r) = ( Sum ( Leibniz_Series_of r))

    proof

      set rL = ( Leibniz_Series_of r), P = ( Partial_Sums rL), A = ( arctan . r);

      deffunc I( Nat) = (( #Z (2 * $1)) / (( #Z 0 ) + ( #Z 2)));

      assume

       A1: 0 <= r <= 1;

      then r in [.( - 1), 1.] by XXREAL_1: 1;

      then

       A2: P is convergent by Th11, SERIES_1:def 2;

      for s st 0 < s holds ex n st for m st n <= m holds |.((P . m) - A).| < s

      proof

        let s;

        assume

         A3: 0 < s;

        consider n such that

         A4: (1 / s) < n by SEQ_4: 3;

        take n;

        let m such that

         A5: n <= m;

        set m1 = (m + 1);

        reconsider R = [. 0 , r.] as non empty closed_interval Subset of REAL by MEASURE5:def 3, A1, XXREAL_1: 1;



         A6: I(m1) is continuous & ( dom I(m1)) = REAL by Th4;

        then ( I(m1) | R) is continuous;

        then

         A7: I(m1) is_integrable_on R & ( I(m1) | R) is bounded by A6, INTEGRA5: 11, INTEGRA5: 10;



         A8: A = ((P . m) + ( integral (((( - 1) |^ m1) (#) I(m1)),R))) by A1, Th12;

        ( integral (((( - 1) |^ m1) (#) I(m1)),R)) = ((( - 1) |^ m1) * ( integral ( I(m1),R))) by A7, A6, INTEGRA6: 9;



        then

         A9: |.( - ( integral (((( - 1) |^ (m + 1)) (#) I(m1)),R))).| = |.((( - 1) |^ (m + 1)) * ( integral ( I(m1),R))).| by COMPLEX1: 52

        .= ( |.(( - 1) |^ (m + 1)).| * |.( integral ( I(m1),R)).|) by COMPLEX1: 65

        .= (1 * |.( integral ( I(m1),R)).|) by SERIES_2: 1;



         A10: |.((P . m) - A).| <= ((1 / ((2 * m1) + 1)) * (r |^ ((2 * m1) + 1))) by A1, Th7, A8, A9;

        ( 0 |^ ((2 * m1) + 1)) = 0 & (1 |^ ((2 * m1) + 1)) = 1 & (r = 0 or r > 0 ) by NAT_1: 11, A1, NEWTON: 11;

        then (r |^ ((2 * m1) + 1)) <= 1 by PREPOWER: 9, A1;

        then ((1 / ((2 * m1) + 1)) * (r |^ ((2 * m1) + 1))) <= ((1 / ((2 * m1) + 1)) * 1) by XREAL_1: 64;

        then

         A11: |.((P . m) - A).| <= (1 / ((2 * m1) + 1)) by A10, XXREAL_0: 2;

        m1 <= ((1 + m1) + m1) by NAT_1: 11;

        then m < ((2 * m1) + 1) by NAT_1: 13;

        then n < ((2 * m1) + 1) by A5, XXREAL_0: 2;

        then (1 / s) < ((2 * m1) + 1) by A4, XXREAL_0: 2;

        then ((1 / s) * s) < (((2 * m1) + 1) * s) & ((1 / s) * s) = 1 by XREAL_1: 68, A3, XCMPLX_1: 87;

        then s > (1 / ((2 * m1) + 1)) by XREAL_1: 83;

        hence thesis by A11, XXREAL_0: 2;

      end;

      then A = ( lim P) by A2, SEQ_2:def 7;

      hence thesis by SERIES_1:def 3;

    end;

    ::$Notion-Name

    theorem :: LEIBNIZ1:14



     Th14: ( PI / 4) = ( Sum Leibniz_Series ) by Th13, SIN_COS9: 39;

    theorem :: LEIBNIZ1:15



     Th15: (( Partial_Sums Leibniz_Series ) . ((2 * n) + 1)) <= ( Sum Leibniz_Series ) <= (( Partial_Sums Leibniz_Series ) . (2 * n))

    proof

      set L = Leibniz_Series , A = ( abs L), aa = ( alternating_series A);

      1 in [.( - 1), 1.] by XXREAL_1: 1;

      then

       A1: A is nonnegative-yielding non-increasing convergent & ( lim A) = 0 by Th9;

      aa = L by Th10;

      hence thesis by A1, Th8;

    end;

    theorem :: LEIBNIZ1:16



     Th16: (( Partial_Sums Leibniz_Series ) . 1) = (2 / 3) & (n is odd implies (( Partial_Sums Leibniz_Series ) . (n + 2)) = ((( Partial_Sums Leibniz_Series ) . n) + (2 / (((4 * (n ^2 )) + (16 * n)) + 15))))

    proof

      set L = Leibniz_Series , P = ( Partial_Sums L);

      set n1 = (n + 1), n2 = (n + 2);



       A1: (P . 0 ) = (L . 0 ) by SERIES_1:def 1

      .= (((( - 1) |^ 0 ) * (1 |^ ((2 * 0 ) + 1))) / ((2 * 0 ) + 1)) by Def2

      .= 1;

      (L . 1) = (((( - 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / ((2 * 1) + 1)) by Def2

      .= ( - (1 / 3));

      then (P . ( 0 + 1)) = (( - (1 / 3)) + 1) by A1, SERIES_1:def 1;

      hence (P . 1) = (2 / 3);

      assume

       A2: n is odd;



       A3: (P . (n1 + 1)) = ((P . n1) + (L . n2)) by SERIES_1:def 1

      .= (((P . n) + (L . n1)) + (L . n2)) by SERIES_1:def 1;



       A4: (L . n1) = (((( - 1) |^ n1) * (1 |^ ((2 * n1) + 1))) / ((2 * n1) + 1)) by Def2

      .= ((1 * (1 |^ ((2 * n1) + 1))) / ((2 * n1) + 1)) by A2, POLYFORM: 8

      .= ((1 * ((2 * n2) + 1)) / (((2 * n1) + 1) * ((2 * n2) + 1))) by XCMPLX_1: 91;

      (L . n2) = (((( - 1) |^ n2) * (1 |^ ((2 * n2) + 1))) / ((2 * n2) + 1)) by Def2

      .= ((( - 1) * (1 |^ ((2 * n2) + 1))) / ((2 * n2) + 1)) by A2, POLYFORM: 9

      .= ( - (1 / ((2 * n2) + 1)))

      .= ( - ((1 * ((2 * n1) + 1)) / (((2 * n2) + 1) * ((2 * n1) + 1)))) by XCMPLX_1: 91;

      hence thesis by A3, A4;

    end;

    ::$Notion-Name

    theorem :: LEIBNIZ1:17

    (313 / 100) < PI < (315 / 100)

    proof

      set L = Leibniz_Series , P = ( Partial_Sums L);

      deffunc P( Nat) = (2 / ((((4 * $1) * $1) + (16 * $1)) + 15));

      deffunc P10( Nat) = (((( P($1) + P(+)) + P(+)) + P(+)) + P(+));

      deffunc P50( Nat) = (((( P10($1) + P10(+)) + P10(+)) + P10(+)) + P10(+));



       A1: n is odd implies (P . (n + 2)) = ((P . n) + P(n))

      proof

        assume n is odd;

        then (P . (n + 2)) = ((P . n) + (2 / (((4 * (n ^2 )) + (16 * n)) + 15))) by Th16;

        hence thesis;

      end;



       A2: n is odd implies (P . (n + 10)) = ((P . n) + P10(n))

      proof

        assume

         A3: n is odd;

        8 = (4 * 2);

        then

         A4: (P . ((n + 8) + 2)) = ((P . (n + 8)) + P(+)) by A1, A3;

        6 = (3 * 2);

        then

         A5: (P . ((n + 6) + 2)) = ((P . (n + 6)) + P(+)) by A1, A3;

        4 = (2 * 2);

        then

         A6: (P . ((n + 4) + 2)) = ((P . (n + 4)) + P(+)) by A1, A3;



         A7: (P . ((n + 2) + 2)) = ((P . (n + 2)) + P(+)) by A3, A1;

        (P . (n + 2)) = ((P . n) + P(n)) by A3, A1;

        hence thesis by A4, A5, A6, A7;

      end;



       A8: n is odd implies (P . (n + 50)) = ((P . n) + P50(n))

      proof

        assume

         A9: n is odd;

        40 = (20 * 2);

        then

         A10: (P . ((n + 40) + 10)) = ((P . (n + 40)) + P10(+)) by A2, A9;

        30 = (15 * 2);

        then

         A11: (P . ((n + 30) + 10)) = ((P . (n + 30)) + P10(+)) by A2, A9;

        20 = (10 * 2);

        then

         A12: (P . ((n + 20) + 10)) = ((P . (n + 20)) + P10(+)) by A2, A9;

        10 = (5 * 2);

        then

         A13: (P . ((n + 10) + 10)) = ((P . (n + 10)) + P10(+)) by A2, A9;

        (P . (n + 10)) = ((P . n) + P10(n)) by A9, A2;

        hence thesis by A10, A11, A12, A13;

      end;



       A14: (2 * 25) = 50;



       A15: 1 = (1 + (2 * 0 ));

      reconsider I = 1 as Nat;



       A16: (50 + 1) is odd by A14;

      then

       A17: (51 + 50) is odd by A14;



       A18: (P . (1 + 50)) = ((2 / 3) + P50()) by Th16, A15, A8;



       A19: (P . (51 + 50)) = ((P . 51) + P50()) by A16, A8;



       A20: (P . (101 + 50)) = ((P . 101) + P50()) by A8, A17;

      (L . 152) = (((( - 1) |^ (76 * 2)) * (1 |^ ((2 * 152) + 1))) / ((2 * 152) + 1)) by Def2

      .= (1 / 305);

      then

       A21: (P . (151 + 1)) = ((P . 151) + (1 / 305)) by SERIES_1:def 1;



       A22: (313 / 400) < (P . 101) by A18, A19;



       A23: (P . 152) < (315 / 400) by A18, A19, A21, A20;

      (P . ((50 * 2) + 1)) <= ( PI / 4) <= (P . (76 * 2)) by Th14, Th15;

      then (313 / 400) < ( PI / 4) < (315 / 400) by A22, A23, XXREAL_0: 2;

      then ((313 / 400) * 4) < (( PI / 4) * 4) < ((315 / 400) * 4) by XREAL_1: 68;

      hence thesis;

    end;