The original and some subsequent proofs of the irrationality of $\pi$ implicitly use the following lemma:

If there is a sequence $P_n(x) \in \mathbb{Z}$ such that $P_n(\alpha)>0$ and $P_n(\alpha)=o(c^{\deg{P_n} })$ for all $0<c<1$, then $\alpha$ is irrational.

The original and some subsequent proofs of the irrationality of $\pi$ implicitly use the following lemma:

If there is a sequence $P_n(x) \in \mathbb{Z}[x]$ such that $P_n(\alpha)>0$ and $P_n(\alpha)=o(c^{\deg{P_n} })$ for all $0<c<1$, then $\alpha$ is irrational.