Fungrim entry: 4c0698

\left|\frac{1}{\pi} - \left(12 \sum_{n=0}^{N - 1} \frac{{\left(-1\right)}^{n} \left(6 n\right)! \left(13591409 + 545140134 n\right)}{\left(3 n\right)! {\left(n !\right)}^{3} \cdot {640320}^{3 n + 3 / 2}}\right)\right| < \frac{1}{{151931373056000}^{N}}

Assumptions:

N \in \mathbb{Z}_{\ge 0}

TeX:

\left|\frac{1}{\pi} - \left(12 \sum_{n=0}^{N - 1} \frac{{\left(-1\right)}^{n} \left(6 n\right)! \left(13591409 + 545140134 n\right)}{\left(3 n\right)! {\left(n !\right)}^{3} \cdot  {640320}^{3 n + 3 / 2}}\right)\right| < \frac{1}{{151931373056000}^{N}}

N \in \mathbb{Z}_{\ge 0}

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`Pi`	$\pi$	The constant pi (3.14...)
`Sum`	$\sum_{n} f(n)$	Sum
`Pow`	${a}^{b}$	Power
`Factorial`	$n !$	Factorial
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("4c0698"),
    Formula(Less(Abs(Sub(Div(1, Pi), Parentheses(Mul(12, Sum(Div(Mul(Mul(Pow(-1, n), Factorial(Mul(6, n))), Add(13591409, Mul(545140134, n))), Mul(Mul(Factorial(Mul(3, n)), Pow(Factorial(n), 3)), Pow(640320, Add(Mul(3, n), Div(3, 2))))), For(n, 0, Sub(N, 1))))))), Div(1, Pow(151931373056000, N)))),
    Variables(N),
    Assumptions(Element(N, ZZGreaterEqual(0))))

Fungrim entry: 4c0698

Topics using this entry