let n be Nat; :: thesis: ( (1 / PI) - (1 / ((1 + (1 / (2 * (n + 1)))) * PI)) > 0 & (1 + (1 / (2 * (n + 1)))) * PI > 0 & 1 / ((1 + (1 / (2 * (n + 1)))) * PI) > 0 )
set s = (1 + (1 / (2 * (n + 1)))) * PI;
(1 + (1 / (2 * (n + 1)))) * PI = PI + ((1 / (2 * (n + 1))) * PI) ;
then 1 * PI < 1 * ((1 + (1 / (2 * (n + 1)))) * PI) by COMPTRIG:5, XREAL_1:39;
then 1 / ((1 + (1 / (2 * (n + 1)))) * PI) < 1 / PI by COMPTRIG:5, XREAL_1:106;
hence ( (1 / PI) - (1 / ((1 + (1 / (2 * (n + 1)))) * PI)) > 0 & (1 + (1 / (2 * (n + 1)))) * PI > 0 & 1 / ((1 + (1 / (2 * (n + 1)))) * PI) > 0 ) by COMPTRIG:5, XREAL_1:50; :: thesis: verum