Term of Computable Real Sequence is Computable

Theorem

Let $\sequence {x_i}$ be a computable real sequence.

Then, for each $i \in \N$:

$x_i$ is a computable real number.

Proof

By definition of computable real sequence, there exists a total recursive function $f : \N^2 \to \N$ such that:

For every $m,n \in \N$, $\map f {m, n}$ codes an integer $k$ such that:

$\dfrac {k - 1} {n + 1} < x_m < \dfrac {k + 1} {n + 1}$

Let $g : \N \to \N$ be defined as:

$\map g n = \map f {i, n}$

By:

• Constant Function is Primitive Recursive
• Primitive Recursive Function is Total Recursive Function

it follows that $g$ is a total recursive function.

Additionally, for every $n \in \N$, $\map g n$ codes an integer $k$ such that:

$\dfrac {k - 1} {n + 1} < x_i < \dfrac {k + 1} {n + 1}$

Thus, by definition, $x_i$ is a computable real number.

$\blacksquare$