set L = Leibniz_Series ;
set P = Partial_Sums Leibniz_Series;
deffunc H1( Nat) -> set = 2 / ((((4 * $1) * $1) + (16 * $1)) + 15);
deffunc H2( Nat) -> set = (((H1($1) + H1($1 + 2)) + H1($1 + 4)) + H1($1 + 6)) + H1($1 + 8);
deffunc H3( Nat) -> set = (((H2($1) + H2($1 + 10)) + H2($1 + 20)) + H2($1 + 30)) + H2($1 + 40);
A1: for n being Nat st n is odd holds
(Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + H1(n)
proof
let n be Nat; :: thesis: ( n is odd implies (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + H1(n) )
assume n is odd ; :: thesis: (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + H1(n)
then (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + (2 / (((4 * (n ^2)) + (16 * n)) + 15)) by Th16;
hence (Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + H1(n) ; :: thesis: verum
end;
A2: for n being Nat st n is odd holds
(Partial_Sums Leibniz_Series) . (n + 10) = ((Partial_Sums Leibniz_Series) . n) + H2(n)
proof
let n be Nat; :: thesis: ( n is odd implies (Partial_Sums Leibniz_Series) . (n + 10) = ((Partial_Sums Leibniz_Series) . n) + H2(n) )
assume A3: n is odd ; :: thesis: (Partial_Sums Leibniz_Series) . (n + 10) = ((Partial_Sums Leibniz_Series) . n) + H2(n)
8 = 4 * 2 ;
then A4: (Partial_Sums Leibniz_Series) . ((n + 8) + 2) = ((Partial_Sums Leibniz_Series) . (n + 8)) + H1(n + 8) by A1, A3;
6 = 3 * 2 ;
then A5: (Partial_Sums Leibniz_Series) . ((n + 6) + 2) = ((Partial_Sums Leibniz_Series) . (n + 6)) + H1(n + 6) by A1, A3;
4 = 2 * 2 ;
then A6: (Partial_Sums Leibniz_Series) . ((n + 4) + 2) = ((Partial_Sums Leibniz_Series) . (n + 4)) + H1(n + 4) by A1, A3;
A7: (Partial_Sums Leibniz_Series) . ((n + 2) + 2) = ((Partial_Sums Leibniz_Series) . (n + 2)) + H1(n + 2) by A3, A1;
(Partial_Sums Leibniz_Series) . (n + 2) = ((Partial_Sums Leibniz_Series) . n) + H1(n) by A3, A1;
hence (Partial_Sums Leibniz_Series) . (n + 10) = ((Partial_Sums Leibniz_Series) . n) + H2(n) by A4, A5, A6, A7; :: thesis: verum
end;
A8: for n being Nat st n is odd holds
(Partial_Sums Leibniz_Series) . (n + 50) = ((Partial_Sums Leibniz_Series) . n) + H3(n)
proof
let n be Nat; :: thesis: ( n is odd implies (Partial_Sums Leibniz_Series) . (n + 50) = ((Partial_Sums Leibniz_Series) . n) + H3(n) )
assume A9: n is odd ; :: thesis: (Partial_Sums Leibniz_Series) . (n + 50) = ((Partial_Sums Leibniz_Series) . n) + H3(n)
40 = 20 * 2 ;
then A10: (Partial_Sums Leibniz_Series) . ((n + 40) + 10) = ((Partial_Sums Leibniz_Series) . (n + 40)) + H2(n + 40) by A2, A9;
30 = 15 * 2 ;
then A11: (Partial_Sums Leibniz_Series) . ((n + 30) + 10) = ((Partial_Sums Leibniz_Series) . (n + 30)) + H2(n + 30) by A2, A9;
20 = 10 * 2 ;
then A12: (Partial_Sums Leibniz_Series) . ((n + 20) + 10) = ((Partial_Sums Leibniz_Series) . (n + 20)) + H2(n + 20) by A2, A9;
10 = 5 * 2 ;
then A13: (Partial_Sums Leibniz_Series) . ((n + 10) + 10) = ((Partial_Sums Leibniz_Series) . (n + 10)) + H2(n + 10) by A2, A9;
(Partial_Sums Leibniz_Series) . (n + 10) = ((Partial_Sums Leibniz_Series) . n) + H2(n) by A9, A2;
hence (Partial_Sums Leibniz_Series) . (n + 50) = ((Partial_Sums Leibniz_Series) . n) + H3(n) by A10, A11, A12, A13; :: thesis: verum
end;
A14: 2 * 25 = 50 ;
A15: 1 = 1 + (2 * 0) ;
reconsider I = 1 as Nat ;
A16: 50 + 1 is odd by A14;
then A17: 51 + 50 is odd by A14;
A18: (Partial_Sums Leibniz_Series) . (1 + 50) = (2 / 3) + H3(1) by Th16, A15, A8;
A19: (Partial_Sums Leibniz_Series) . (51 + 50) = ((Partial_Sums Leibniz_Series) . 51) + H3(51) by A16, A8;
A20: (Partial_Sums Leibniz_Series) . (101 + 50) = ((Partial_Sums Leibniz_Series) . 101) + H3(101) by A8, A17;
Leibniz_Series . 152 = (((- 1) |^ (76 * 2)) * (1 |^ ((2 * 152) + 1))) / ((2 * 152) + 1) by Def2
.= 1 / 305 ;
then A21: (Partial_Sums Leibniz_Series) . (151 + 1) = ((Partial_Sums Leibniz_Series) . 151) + (1 / 305) by SERIES_1:def 1;
A22: 313 / 400 < (Partial_Sums Leibniz_Series) . 101 by A18, A19;
A23: (Partial_Sums Leibniz_Series) . 152 < 315 / 400 by A18, A19, A21, A20;
( (Partial_Sums Leibniz_Series) . ((50 * 2) + 1) <= PI / 4 & PI / 4 <= (Partial_Sums Leibniz_Series) . (76 * 2) ) by Th14, Th15;
then ( 313 / 400 < PI / 4 & PI / 4 < 315 / 400 ) by A22, A23, XXREAL_0:2;
then ( (313 / 400) * 4 < (PI / 4) * 4 & (PI / 4) * 4 < (315 / 400) * 4 ) by XREAL_1:68;
hence ( 313 / 100 < PI & PI < 315 / 100 ) ; :: thesis: verum