Irrationality Criteria for Series by Erdős and Straus

We formalise certain irrationality criteria for infinite series of the form: $$\sum _{n=1}^{\mathrm{\infty }}\frac{b_n}{\prod _{i=1}^n{a}_i}$$ where $\{b_n\}$ is a sequence of integers and $\{a_n\}$ a sequence of positive integers with $a_n>1$ for all large n. The results are due to P. Erdős and E. G. Straus [1]. In particular, we formalise Theorem 2.1, Corollary 2.10 and Theorem 3.1. The latter is an application of Theorem 2.1 involving the prime numbers.