let n be Nat; :: thesis: ( (Partial_Sums Leibniz_Series) . ((2 * n) + 1) <= Sum Leibniz_Series & Sum Leibniz_Series <= (Partial_Sums Leibniz_Series) . (2 * n) )
set L = Leibniz_Series ;
set A = abs Leibniz_Series;
set aa = alternating_series (abs Leibniz_Series);
1 in [.(- 1),1.] by XXREAL_1:1;
then A1: ( abs Leibniz_Series is nonnegative-yielding & abs Leibniz_Series is non-increasing & abs Leibniz_Series is convergent & lim (abs Leibniz_Series) = 0 ) by Th9;
alternating_series (abs Leibniz_Series) = Leibniz_Series by Th10;
hence ( (Partial_Sums Leibniz_Series) . ((2 * n) + 1) <= Sum Leibniz_Series & Sum Leibniz_Series <= (Partial_Sums Leibniz_Series) . (2 * n) ) by A1, Th8; :: thesis: verum