# Correct constructive proof of $0 \leq x < 1/n$, $\forall n \in \mathbb{N} \implies x = 0$.

I've set out to prove $$0 \leq x < 1/n, \ \forall n \in \mathbb{N} \implies x = 0$$ constructively. I will be using the construction of the real numbers given in Bishop's Constructive Analysis.

Bishop defines a real number $$x$$ to be a regular sequence of rational numbers, that is, $$x \equiv (x_n)$$ where $$|x_m - x_n| \leq 1/m + 1/n, \ (m,n \in \mathbb{Z^+}).$$ Further, two real numbers $$x \equiv (x_n)$$ and $$y \equiv (y_n)$$ are equal if $$|x_n - y_n| \leq 2/n, \ (n \in \mathbb{Z^+}).$$ It's trivial to show equality is an equivalence relation. Finally, Bishop gives the following lemma, for each real number $$x \equiv (x_n)$$, we have $$|x - x_n| \leq 1/n, \ (n \in \mathbb{Z^+}).$$ I will not present this proof either. My proposed proof of the initial claim follows as such: Given a real number $$x \equiv (x_m)$$ such that $$0 \leq x < 1/n, \ \forall n \in \mathbb{N}.$$ By the traiangle inequality (variation) $$|x_m| - |x| = |x_m| - |-x| \leq |x_m - x| \leq 1/m, \ (m \in \mathbb{Z^+}).$$ Together with $$|x| = x < 1/m, \ (m \in \mathbb{Z^+})$$ this implies $$|x_m - 0| = |x_m| \leq 1/m + |x| \leq 2/m, (m \in \mathbb{Z^+}).$$ Thus, $$x \equiv (x_m) = 0^* \equiv 0$$. Where $$0^*$$ is the constant sequence of zeros from the rational numbers.

Is this proof correct? And is there an easier constructive proof?

• If x is a sequence and n am integer, what is the meaning of x<1/n ? Commented Sep 18, 2021 at 3:22
• There is an order defined on real numbers. In this sense 1/n can be (1/n)* the constant sequence of 1/n (the way you imbed the rationals into the reals.) I didn’t think it was necessary to give the order definition but it is in the book. Commented Sep 18, 2021 at 17:11
• Sorry, I don't understand your answer. You use the equation x<1/n but you say it is not necessary to know what this exactly means? Commented Sep 19, 2021 at 16:55
• @miracle173 There is a technical definition of $x < 1/n$. I could easily copy it from the book. But we are taking this as an assumption and can therefore use the assumption in the proof with out reference to the technical definition. If you do not have access to the text I would be happy to share the technical definition with you, but I still feel it is not necesary for the proof. Commented Sep 20, 2021 at 17:37

\begin{align} |x_m - 0| &= |(x_m - x) + x|\\ &\leq |x_m - x| + |x| && (\text{usual triangle inequality})\\ &= |x_m - x| + x && (x \geq 0)\\ &\leq 1/m + 1/m\\ &= 2/m \end{align}