 Recursively inseparable-set proof of Tennenbaum theorem

Let $A,B$ be disjoint computably enumerable recursively inseparable sets, represented by existential arithmetic formulas with bounded computation witnesses $\alpha (x,y)$ and $\beta (x,z)$. In a non-standard model of arithmetic $M\models \mathsf{PA}$, the assertionholds at every standard bound $c$. The overspill lemma gives a nonstandard bound where it still holds. This no-clash condition matters: an arbitrarily chosen nonstandard computation stage need not preserve the external disjointness of the two enumerations.

Inside $M$, form the internally finite set $C=\{x<c:\exists y<c\alpha (x,y)\}$ and code it by the product of its corresponding prime numbers. Its standard trace contains $A$ and avoids $B$, since the finite standard witnesses for either enumeration lie below $c$. If the arithmetic operations of $M$ were computable, division by each standard prime would decide membership in this trace: search for $q$ and a standard remainder $r<p$ satisfying $a=pq+r$, where $a$ is the fixed code. The division algorithm in Peano arithmetic guarantees termination. This would give a computable set separating $A$ from $B$, a contradiction.^[ref]