I am working on the formal construction of the positive real numbers. I have the positive real number 2 as the set of positive rational numbers less than 2. I have $\sqrt{2}$ as the set of positive rational numbers the squares of which are less than 2.
Multiplication of positive real numbers x and y is defined as the set of all positive rational numbers $z=a\times b$ such that $a\in x$ and $b\in y$.
Question: Using these constructions, how can I prove that the $\sqrt{2}\times\sqrt{2} = 2$?
Any help -- hints or online references -- would be appreciated.
Restating question: If $x$ is a positive rational number less than 2, how can I prove there exists positive rational numbers $a$ and $b$ such that $a\times a\lt 2$, $b\times b \lt 2$ and $x=a\times b$ ?