Sum of Computable Real Sequences is Computable/Corollary

Corollary to Sum of Computable Real Sequences is Computable

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

Let $c \in \R$ be a computable real number.

Then, $\sequence {x_n + c}$ is a computable real sequence.

Proof

By Constant Sequence of Computable Real Number is Computable, the sequence $\sequence {y_n}$ defined as:

$y_n = c$

is computable.

Then, by Sum of Computable Real Sequences is Computable:

$\sequence {x_n + y_n}$

is computable.

But:

$x_n + y_n = x_n + c$

for all $n \in \N$.

The result follows.

$\blacksquare$