let r be Real; :: thesis: ( 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.] ; :: thesis: ( 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 ; :: thesis: ( 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)
proof
let n be Nat; :: thesis: (abs (Leibniz_Series_of r)) . n = (|.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1)
- (- 1) = 1 ;
then |.(- 1).| = 1 by ABSVALUE:def 1;
then A4: |.((- 1) |^ n).| = 1 |^ n by TAYLOR_2:1;
A5: (abs (Leibniz_Series_of r)) . n = |.((Leibniz_Series_of r) . n).| by A2, VALUED_1:def 11, ORDINAL1:def 12;
(Leibniz_Series_of r) . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) by Def2;
hence (abs (Leibniz_Series_of r)) . n = |.(((- 1) |^ n) * (r |^ ((2 * n) + 1))).| / |.((2 * n) + 1).| by COMPLEX1:67, A5
.= (1 * |.(r |^ ((2 * n) + 1)).|) / |.((2 * n) + 1).| by A4, COMPLEX1:65
.= (1 * (|.r.| |^ ((2 * n) + 1))) / |.((2 * n) + 1).| by TAYLOR_2:1
.= (|.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1) by ABSVALUE:def 1 ;
:: thesis: verum
end;
( - 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)
proof
let n be Nat; :: thesis: (abs (Leibniz_Series_of r)) . n >= (abs (Leibniz_Series_of r)) . (n + 1)
set n1 = n + 1;
A7: (abs (Leibniz_Series_of r)) . (n + 1) = ((|.r.| |^ ((2 * (n + 1)) + 1)) * 1) / ((2 * (n + 1)) + 1) by A3;
A8: |.r.| >= 0 by COMPLEX1:46;
|.(r |^ ((2 * n) + 1)).| = |.r.| |^ ((2 * n) + 1) by TAYLOR_2:1;
then A9: |.r.| |^ ((2 * n) + 1) >= 0 by COMPLEX1:46;
A10: |.r.| * |.r.| <= 1 * 1 by A8, A6, XREAL_1:66;
|.r.| |^ ((2 * (n + 1)) + 1) = |.r.| * (|.r.| |^ (((2 * n) + 1) + 1)) by NEWTON:6
.= |.r.| * (|.r.| * (|.r.| |^ ((2 * n) + 1))) by NEWTON:6
.= (|.r.| * |.r.|) * (|.r.| |^ ((2 * n) + 1)) ;
then A11: |.r.| |^ ((2 * (n + 1)) + 1) <= (|.r.| |^ ((2 * n) + 1)) * 1 by A9, A10, XREAL_1:66;
|.(r |^ ((2 * (n + 1)) + 1)).| = |.r.| |^ ((2 * (n + 1)) + 1) by TAYLOR_2:1;
then A12: |.r.| |^ ((2 * (n + 1)) + 1) >= 0 by COMPLEX1:46;
(2 * n) + 1 <= ((2 * n) + 1) + 1 by NAT_1:13;
then (2 * n) + 1 < (((2 * n) + 1) + 1) + 1 by NAT_1:13;
then 1 / ((2 * n) + 1) >= 1 / ((2 * (n + 1)) + 1) by XREAL_1:76;
then ((|.r.| |^ ((2 * n) + 1)) * 1) / ((2 * n) + 1) >= ((|.r.| |^ ((2 * (n + 1)) + 1)) * 1) / ((2 * (n + 1)) + 1) by A12, A11, XREAL_1:66;
hence (abs (Leibniz_Series_of r)) . n >= (abs (Leibniz_Series_of r)) . (n + 1) by A3, A7; :: thesis: verum
end;
hence abs (Leibniz_Series_of r) is non-increasing by VALUED_1:def 16; :: thesis: ( 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 )
proof
let n be Nat; :: thesis: ( (seq_const 0) . n <= (abs (Leibniz_Series_of r)) . n & (abs (Leibniz_Series_of r)) . n <= f . n )
A17: |.r.| >= 0 by COMPLEX1:46;
A18: 0 |^ ((2 * n) + 1) = 0 by NEWTON:11, NAT_1:11;
( |.r.| > 0 implies |.r.| |^ ((2 * n) + 1) <= 1 |^ ((2 * n) + 1) ) by A6, PREPOWER:9;
then A19: |.r.| |^ ((2 * n) + 1) <= 1 by A18, A17;
|.(r |^ ((2 * n) + 1)).| = |.r.| |^ ((2 * n) + 1) by TAYLOR_2:1;
then A20: |.r.| |^ ((2 * n) + 1) >= 0 by COMPLEX1:46;
((2 * n) + 1) / 2 = n + (1 / 2) ;
then A21: 1 / ((2 * n) + 1) = H1(n) by XCMPLX_1:55
.= f . n by A14 ;
(abs (Leibniz_Series_of r)) . n = (|.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1) by A3
.= (|.r.| |^ ((2 * n) + 1)) * (((2 * n) + 1) ") ;
hence ( (seq_const 0) . n <= (abs (Leibniz_Series_of r)) . n & (abs (Leibniz_Series_of r)) . n <= f . n ) by A19, XREAL_1:64, A20, A21; :: thesis: verum
end;
hence ( abs (Leibniz_Series_of r) is convergent & lim (abs (Leibniz_Series_of r)) = 0 ) by A13, A15, SEQ_2:19, SEQ_2:20; :: thesis: verum