Pigeonhole principle in prime numbers I read a proof and there is one step which I get intuitively but I don't know how to formally justify that.
Let's consider pairs of integers $(x', y')$ where $x',y' \in \{0,1,...,\lfloor \sqrt{p} \rfloor\}$ and $p$ is a prime number. We know that number of those pairs is $(\lfloor \sqrt{p} \rfloor +1)^2$, and applying inequality $\lfloor \sqrt{x} \rfloor + 1 > \sqrt{x}$ we see that number of pairs $(x', y')$ is bigger than $p$.
Out of these facts we have corollary that:
$$\forall_{s \in \mathbb{Z}}\exists_{x', y', x'', y'' \in \{0,1,...,\lfloor{\sqrt{p}}\rfloor\}, (x', y') \neq (x'', y'')}: x'-sy' \equiv x'' - sy'' (mod \; p)$$
And my question is - how it can be formally justified ? Author says that we just need to use pigeonhole principle to obtain the result. Could you please explain to me how it was really used ?
 A: Consider $z(x,y) \equiv x-sy$ mod $p$, as $x,y$ vary over $D=P\times P$, where $P\equiv{0,1,...,\lfloor \sqrt{p} \rfloor}$. The cardinality of $D$ is larger than $p$. Since you have more than $p$ elements in the domain, you must have two tuples $x,y$ and $x',y'$ whose associated $z$ are equal mod $p$, that is $z(x,y)=z(x',y')$ mod p. This is true for any $s$.
Note that one can choose also non linear $z$ functions, e.g. $z(x,y)=x^2+sy^2$ and the result would have remained true.
UPDATE: Note that considering three value functions $z(x,y,w)$ one could rescrict $P\equiv{0,1,...,\lfloor p^{1/3} \rfloor}$, so that $D=P^3$ has again cardinality larger than $p$. One could make than similar reasons for functions like $z(x,y,w)=x-s_1y-s_2w$, even if I do not know if this may have any application.
A: There are at least $p+1$ pairs $(x',y')$ in your collection. But there are only $p$ residue classes mod $p$. If you take the difference of $x',y'$ for each one of your pairs, by the Pidgeon hole principle there should be at least two distinct pairs such that the difference lies in the same congruence class modulo $p$. More precisely, there are two distinct pairs $(x',y'),(x'',y'')$ such that $x'-y'\equiv x''-y''\mod p$. This is for the case $s=1.$ For other values of $s$, the argument is very similar.
