let n be Nat; :: thesis: for r being Real
for A being non empty closed_interval Subset of REAL st A = [.0,r.] & r >= 0 holds
arctan . r = ((Partial_Sums (Leibniz_Series_of r)) . n) + (integral ((((- 1) |^ (n + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A))
let r be Real; :: thesis: for A being non empty closed_interval Subset of REAL st A = [.0,r.] & r >= 0 holds
arctan . r = ((Partial_Sums (Leibniz_Series_of r)) . n) + (integral ((((- 1) |^ (n + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A))
let A be non empty closed_interval Subset of REAL; :: thesis: ( 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)) )
set Z0 = #Z 0;
set Z2 = #Z 2;
set rL = Leibniz_Series_of r;
assume ( A = [.0,r.] & r >= 0 ) ; :: thesis: arctan . r = ((Partial_Sums (Leibniz_Series_of r)) . n) + (integral ((((- 1) |^ (n + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A))
then A1: ( upper_bound A = r & lower_bound A = 0 ) by JORDAN5A:19;
defpred S₁[ Nat] means arctan . r = ((Partial_Sums (Leibniz_Series_of r)) . $1) + (integral ((((- 1) |^ ($1 + 1)) (#) ((#Z (2 * ($1 + 1))) / ((#Z 0) + (#Z 2)))),A));
A2: S₁[ 0 ]

proof

A3: integral (((#Z 0) / ((#Z 0) + (#Z 2))),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)
.= (Leibniz_Series_of r) . 0 by A4, Def2 ;
(- 1) |^ 0 = 1 by NEWTON:4;
then ((- 1) |^ 0) (#) ((#Z 0) / ((#Z 0) + (#Z 2))) = (#Z 0) / ((#Z 0) + (#Z 2)) by RFUNCT_1:21;
then arctan . r = ((Leibniz_Series_of r) . 0) + (integral ((((- 1) |^ (0 + 1)) (#) ((#Z (2 * (0 + 1))) / ((#Z 0) + (#Z 2)))),A)) by A3, A1, A4, Th6, A5;
hence S₁[ 0 ] by SERIES_1:def 1; :: thesis: verum

end;

A6: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
set i1 = i + 1;
set i11 = (i + 1) + 1;
assume A7: S₁[i] ; :: thesis: S₁[i + 1]
A8: 0 |^ ((2 * (i + 1)) + 1) = 0 by NEWTON:11, NAT_1:11;
((- 1) |^ (i + 1)) * (((1 / ((2 * (i + 1)) + 1)) * (r |^ ((2 * (i + 1)) + 1))) - ((1 / ((2 * (i + 1)) + 1)) * 0)) = (((- 1) |^ (i + 1)) * (r |^ ((2 * (i + 1)) + 1))) / ((2 * (i + 1)) + 1)
.= (Leibniz_Series_of r) . (i + 1) by Def2 ;
then integral ((((- 1) |^ (i + 1)) (#) ((#Z (2 * (i + 1))) / ((#Z 0) + (#Z 2)))),A) = ((Leibniz_Series_of r) . (i + 1)) + (integral ((((- 1) |^ ((i + 1) + 1)) (#) ((#Z (2 * ((i + 1) + 1))) / ((#Z 0) + (#Z 2)))),A)) by A8, Th6, A1;
then arctan . r = (((Partial_Sums (Leibniz_Series_of r)) . i) + ((Leibniz_Series_of r) . (i + 1))) + (integral ((((- 1) |^ ((i + 1) + 1)) (#) ((#Z (2 * ((i + 1) + 1))) / ((#Z 0) + (#Z 2)))),A)) by A7;
hence S₁[i + 1] by SERIES_1:def 1; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A6);
hence arctan . r = ((Partial_Sums (Leibniz_Series_of r)) . n) + (integral ((((- 1) |^ (n + 1)) (#) ((#Z (2 * (n + 1))) / ((#Z 0) + (#Z 2)))),A)) ; :: thesis: verum