theorem Th12: :: LEIBNIZ1:12

for n being 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))