let r be Real; :: thesis: ( 0 <= r & r <= 1 implies arctan . r = Sum (Leibniz_Series_of r) )
set rL = Leibniz_Series_of r;
set P = Partial_Sums (Leibniz_Series_of r);
set A = arctan . r;
deffunc H₁( Nat) -> Element of K10(K11(REAL,REAL)) = (#Z (2 * $1)) / ((#Z 0) + (#Z 2));
assume A1: ( 0 <= r & r <= 1 ) ; :: thesis: arctan . r = Sum (Leibniz_Series_of r)
then r in [.(- 1),1.] by XXREAL_1:1;
then A2: Partial_Sums (Leibniz_Series_of r) is convergent by Th11, SERIES_1:def 2;
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| < s

proof

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| < s )
assume A3: 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| < s
consider n being Nat such that
A4: 1 / s < n by SEQ_4:3;
take n ; :: thesis: for m being Nat st n <= m holds
|.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| < s
let m be Nat; :: thesis: ( n <= m implies |.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| < s )
assume A5: n <= m ; :: thesis: |.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| < s
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: ( H₁(m + 1) is continuous & dom H₁(m + 1) = REAL ) by Th4;
then H₁(m + 1) | R is continuous ;
then A7: ( H₁(m + 1) is_integrable_on R & H₁(m + 1) | R is bounded ) by A6, INTEGRA5:11, INTEGRA5:10;
A8: arctan . r = ((Partial_Sums (Leibniz_Series_of r)) . m) + (integral ((((- 1) |^ (m + 1)) (#) H₁(m + 1)),R)) by A1, Th12;
integral ((((- 1) |^ (m + 1)) (#) H₁(m + 1)),R) = ((- 1) |^ (m + 1)) * (integral (H₁(m + 1),R)) by A7, A6, INTEGRA6:9;
then A9: |.(- (integral ((((- 1) |^ (m + 1)) (#) H₁(m + 1)),R))).| = |.(((- 1) |^ (m + 1)) * (integral (H₁(m + 1),R))).| by COMPLEX1:52
.= |.((- 1) |^ (m + 1)).| * |.(integral (H₁(m + 1),R)).| by COMPLEX1:65
.= 1 * |.(integral (H₁(m + 1),R)).| by SERIES_2:1 ;
A10: |.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| <= (1 / ((2 * (m + 1)) + 1)) * (r |^ ((2 * (m + 1)) + 1)) by A1, Th7, A8, A9;
( 0 |^ ((2 * (m + 1)) + 1) = 0 & 1 |^ ((2 * (m + 1)) + 1) = 1 & ( r = 0 or r > 0 ) ) by NAT_1:11, A1, NEWTON:11;
then r |^ ((2 * (m + 1)) + 1) <= 1 by PREPOWER:9, A1;
then (1 / ((2 * (m + 1)) + 1)) * (r |^ ((2 * (m + 1)) + 1)) <= (1 / ((2 * (m + 1)) + 1)) * 1 by XREAL_1:64;
then A11: |.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| <= 1 / ((2 * (m + 1)) + 1) by A10, XXREAL_0:2;
m + 1 <= (1 + (m + 1)) + (m + 1) by NAT_1:11;
then m < (2 * (m + 1)) + 1 by NAT_1:13;
then n < (2 * (m + 1)) + 1 by A5, XXREAL_0:2;
then 1 / s < (2 * (m + 1)) + 1 by A4, XXREAL_0:2;
then ( (1 / s) * s < ((2 * (m + 1)) + 1) * s & (1 / s) * s = 1 ) by XREAL_1:68, A3, XCMPLX_1:87;
then s > 1 / ((2 * (m + 1)) + 1) by XREAL_1:83;
hence |.(((Partial_Sums (Leibniz_Series_of r)) . m) - (arctan . r)).| < s by A11, XXREAL_0:2; :: thesis: verum

end;

then arctan . r = lim (Partial_Sums (Leibniz_Series_of r)) by A2, SEQ_2:def 7;
hence arctan . r = Sum (Leibniz_Series_of r) by SERIES_1:def 3; :: thesis: verum