First order irrationality criteria for series

by LEE A. BUTLER

Corollary 2.2 in the paper is inspired by some work of Viggo Brun. It is mentioned that Corollary 2.2 applies to the sequence qₙ below. We verify that fact in corollary_2_2_example below. In fact, the assumption n ≥ 1 is not needed.

def q : ℕ → ℕ

Equations

• q n = 2 ^ 2 ^ n

theorem all_positive (n : ℕ) : 0 < q n

theorem quad (a : ℕ) (h : 2 ≤ a) : a ^ 2 - a + 1 < a ^ 2

theorem corollary_2_2_example (n : ℕ) : q (n + 1) > q n ^ 2 - q n + 1