Chebyshev’s theorem

We note that for the proof of Chebyshev’s classical result it has been necessary to define in a Ao-way functions such as factorial and binomial coefficient, and to prove the basic recursion laws of these functions in 7Ao. In order to define factorial, the following result due to Paris, Wilkie, and Woods has been used.