let r be Real; ( r in [.(- 1),1.] implies ( abs (Leibniz_Series_of r) is nonnegative-yielding & abs (Leibniz_Series_of r) is non-increasing & abs (Leibniz_Series_of r) is convergent & lim (abs (Leibniz_Series_of r)) = 0 ) )
set rL = Leibniz_Series_of r;
set A = abs (Leibniz_Series_of r);
assume A1:
r in [.(- 1),1.]
; ( abs (Leibniz_Series_of r) is nonnegative-yielding & abs (Leibniz_Series_of r) is non-increasing & abs (Leibniz_Series_of r) is convergent & lim (abs (Leibniz_Series_of r)) = 0 )
A2:
( dom (abs (Leibniz_Series_of r)) = dom (Leibniz_Series_of r) & dom (Leibniz_Series_of r) = NAT )
by VALUED_1:def 11, FUNCT_2:def 1;
thus
abs (Leibniz_Series_of r) is nonnegative-yielding
; ( abs (Leibniz_Series_of r) is non-increasing & abs (Leibniz_Series_of r) is convergent & lim (abs (Leibniz_Series_of r)) = 0 )
A3:
for n being Nat holds (abs (Leibniz_Series_of r)) . n = (|.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1)
( - 1 <= r & r <= 1 )
by A1, XXREAL_1:1;
then A6:
|.r.| <= 1
by ABSVALUE:5;
for n being Nat holds (abs (Leibniz_Series_of r)) . n >= (abs (Leibniz_Series_of r)) . (n + 1)
hence
abs (Leibniz_Series_of r) is non-increasing
by VALUED_1:def 16; ( abs (Leibniz_Series_of r) is convergent & lim (abs (Leibniz_Series_of r)) = 0 )
set C = seq_const 0;
A13:
lim (seq_const 0) = 0
;
deffunc H1( Nat) -> set = (1 / 2) / ($1 + (1 / 2));
consider f being Real_Sequence such that
A14:
for n being Nat holds f . n = H1(n)
from SEQ_1:sch 1();
A15:
( f is convergent & lim f = 0 )
by A14, SEQ_4:31;
for n being Nat holds
( (seq_const 0) . n <= (abs (Leibniz_Series_of r)) . n & (abs (Leibniz_Series_of r)) . n <= f . n )
hence
( abs (Leibniz_Series_of r) is convergent & lim (abs (Leibniz_Series_of r)) = 0 )
by A13, A15, SEQ_2:19, SEQ_2:20; verum