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?
Best Answer
I think your proof is fine. Your application of the triangle inequality seems overcomplicated to me, though. Here's my take.
$$ \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} $$