let r be Real; :: thesis: ( ( r >= 0 implies alternating_series (abs (Leibniz_Series_of r)) = Leibniz_Series_of r ) & ( r < 0 implies (- 1) (#) (alternating_series (abs (Leibniz_Series_of r))) = Leibniz_Series_of r ) )
set rL = Leibniz_Series_of r;
set A = abs (Leibniz_Series_of r);
set aA = alternating_series (abs (Leibniz_Series_of r));
A1: ( 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;
A2: for n being Nat holds (alternating_series (abs (Leibniz_Series_of r))) . n = ((- 1) |^ n) * ((|.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1))

proof

let n be Nat; :: thesis: (alternating_series (abs (Leibniz_Series_of r))) . n = ((- 1) |^ n) * ((|.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1))
- (- 1) = 1 ;
then |.(- 1).| = 1 by ABSVALUE:def 1;
then A3: |.((- 1) |^ n).| = 1 |^ n by TAYLOR_2:1;
A4: (abs (Leibniz_Series_of r)) . n = |.((Leibniz_Series_of r) . n).| by A1, VALUED_1:def 11, ORDINAL1:def 12;
(Leibniz_Series_of r) . n = (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1) by Def2;
then (abs (Leibniz_Series_of r)) . n = |.(((- 1) |^ n) * (r |^ ((2 * n) + 1))).| / |.((2 * n) + 1).| by COMPLEX1:67, A4
.= (1 * |.(r |^ ((2 * n) + 1)).|) / |.((2 * n) + 1).| by A3, 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 ;
hence (alternating_series (abs (Leibniz_Series_of r))) . n = ((- 1) |^ n) * ((|.r.| |^ ((2 * n) + 1)) / ((2 * n) + 1)) by Def1; :: thesis: verum

end;

thus ( r >= 0 implies alternating_series (abs (Leibniz_Series_of r)) = Leibniz_Series_of r ) :: thesis: ( r < 0 implies (- 1) (#) (alternating_series (abs (Leibniz_Series_of r))) = Leibniz_Series_of r )

proof

assume r >= 0 ; :: thesis: alternating_series (abs (Leibniz_Series_of r)) = Leibniz_Series_of r
then A5: |.r.| = r by ABSVALUE:def 1;

now :: thesis: for n being Nat holds (alternating_series (abs (Leibniz_Series_of r))) . n = (Leibniz_Series_of r) . n

let n be Nat; :: thesis: (alternating_series (abs (Leibniz_Series_of r))) . n = (Leibniz_Series_of r) . n
thus (alternating_series (abs (Leibniz_Series_of r))) . n = ((- 1) |^ n) * ((r |^ ((2 * n) + 1)) / ((2 * n) + 1)) by A2, A5
.= (((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1)
.= (Leibniz_Series_of r) . n by Def2 ; :: thesis: verum

end;

hence alternating_series (abs (Leibniz_Series_of r)) = Leibniz_Series_of r ; :: thesis: verum

end;

assume r < 0 ; :: thesis: (- 1) (#) (alternating_series (abs (Leibniz_Series_of r))) = Leibniz_Series_of r
then A6: |.r.| = - r by ABSVALUE:def 1;

now :: thesis: for n being Nat holds (Leibniz_Series_of r) . n = ((- 1) (#) (alternating_series (abs (Leibniz_Series_of r)))) . n

let n be Nat; :: thesis: (Leibniz_Series_of r) . n = ((- 1) (#) (alternating_series (abs (Leibniz_Series_of r)))) . n
|.r.| |^ ((2 * n) + 1) = - (r |^ ((2 * n) + 1)) by A6, POWER:2;
then (alternating_series (abs (Leibniz_Series_of r))) . n = ((- 1) |^ n) * ((- (r |^ ((2 * n) + 1))) / ((2 * n) + 1)) by A2
.= - ((((- 1) |^ n) * (r |^ ((2 * n) + 1))) / ((2 * n) + 1))
.= - ((Leibniz_Series_of r) . n) by Def2 ;
hence (Leibniz_Series_of r) . n = (- 1) * ((alternating_series (abs (Leibniz_Series_of r))) . n)
.= ((- 1) (#) (alternating_series (abs (Leibniz_Series_of r)))) . n by SEQ_1:9 ;
:: thesis: verum

end;

hence (- 1) (#) (alternating_series (abs (Leibniz_Series_of r))) = Leibniz_Series_of r ; :: thesis: verum