On page 26 of Bishop and Bridges "Constructive Analysis", in a proof of "If $x_1,…,x_n$ are real numbers such that $x_1 + …+x_n$>0, then for some $i$, $x_i>0$", it seems to me this lemma is used without proof:
If for each $a_i$, $a_i\in \mathbb{Q}$ and $p \in \mathbb{Q}$, then $\sum_{i=1}^n a_i > \frac{1}{2}p \Rightarrow \exists i: a_i > \frac{1}{2n}p$.
This is classically obvious but seems to use LEM/proof by contradiction, and is therefore non-constructive. I would (classically) prove the statement by assuming $\forall i : a_i\leq\frac{1}{2n}p$ and show that implies $\sum_{i=1}^n a_i \leq \frac{1}{2}p$. So $\sum_{i=1}^n a_i > \frac{1}{2}p \Rightarrow \neg \forall i : a_i\leq\frac{1}{2n}p \Rightarrow \exists i: a_i > \frac{1}{2n}p$ but it is my understanding that the last step is nonconstructive. What is the constructive way to do this?
Further in the very next proof, he asserts "For each n in $\mathbb{Z}^+$, either $x_n \leq n^{-1}$ or $x_n > n^{-1}$," where $n \in \mathbb{N}$ and $x_n \in \mathbb{Q}$. This seems like classic LEM: how is it not?
I'm very new to constructive math so sorry if the answer is obvious.
Best Answer
Two constructively valid facts are being used here. First, inequality between rational numbers is decidable. Thus, if $x$ and $y$ are rational then $x<y$ or $x=y$ or $x>y$. The (constructive) proof of this proceeds by using the definition of $<$ and $=$ for rational numbers in terms of the corresponding relations on natural numbers; the fact that natural numbers satisfy $x<y$ or $x=y$ or $x>y$ is proved by induction.
Second, although decidability is not generally preserved by quantification, it is preserved by quantification over finite sets. In particular, if one has, for all natural numbers $i\leq n$, that $\phi(i)\lor\neg\phi(i)$, then it follows that $[(\exists i\leq n)\,\phi(i)]\lor[(\forall i\leq n)\,\neg\phi(i)]$. Again, the (constructive) proof of this is by induction on $n$.