let n be Nat; 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; 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; ( 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 )
; 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 S1[ 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:
S1[ 0 ]
A6:
for i being Nat st S1[i] holds
S1[i + 1]
for i being Nat holds S1[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))
; verum