let n be Nat; :: thesis: ( (Partial_Sums Leibniz_Series) . 1 = 2 / 3 & ( n is odd implies (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + (2 / (((4 * (n ^2)) + (16 * n)) + 15)) ) )
set L = Leibniz_Series ;
set P = Partial_Sums Leibniz_Series;
set n1 = n + 1;
set n2 = n + 2;
A1: (Partial_Sums Leibniz_Series) . 0 = Leibniz_Series . 0 by SERIES_1:def 1
.= (((- 1) |^ 0) * (1 |^ ((2 * 0) + 1))) / ((2 * 0) + 1) by Def2
.= 1 ;
Leibniz_Series . 1 = (((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / ((2 * 1) + 1) by Def2
.= - (1 / 3) ;
then (Partial_Sums Leibniz_Series) . (0 + 1) = (- (1 / 3)) + 1 by A1, SERIES_1:def 1;
hence (Partial_Sums Leibniz_Series) . 1 = 2 / 3 ; :: thesis: ( n is odd implies (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + (2 / (((4 * (n ^2)) + (16 * n)) + 15)) )
assume A2: n is odd ; :: thesis: (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + (2 / (((4 * (n ^2)) + (16 * n)) + 15))
A3: (Partial_Sums Leibniz_Series) . ((n + 1) + 1) = ((Partial_Sums Leibniz_Series) . (n + 1)) + (Leibniz_Series . (n + 2)) by SERIES_1:def 1
.= (((Partial_Sums Leibniz_Series) . n) + (Leibniz_Series . (n + 1))) + (Leibniz_Series . (n + 2)) by SERIES_1:def 1 ;
A4: Leibniz_Series . (n + 1) = (((- 1) |^ (n + 1)) * (1 |^ ((2 * (n + 1)) + 1))) / ((2 * (n + 1)) + 1) by Def2
.= (1 * (1 |^ ((2 * (n + 1)) + 1))) / ((2 * (n + 1)) + 1) by A2, POLYFORM:8
.= (1 * ((2 * (n + 2)) + 1)) / (((2 * (n + 1)) + 1) * ((2 * (n + 2)) + 1)) by XCMPLX_1:91 ;
Leibniz_Series . (n + 2) = (((- 1) |^ (n + 2)) * (1 |^ ((2 * (n + 2)) + 1))) / ((2 * (n + 2)) + 1) by Def2
.= ((- 1) * (1 |^ ((2 * (n + 2)) + 1))) / ((2 * (n + 2)) + 1) by A2, POLYFORM:9
.= - (1 / ((2 * (n + 2)) + 1))
.= - ((1 * ((2 * (n + 1)) + 1)) / (((2 * (n + 2)) + 1) * ((2 * (n + 1)) + 1))) by XCMPLX_1:91 ;
hence (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + (2 / (((4 * (n ^2)) + (16 * n)) + 15)) by A3, A4; :: thesis: verum