Elementary proof that $\Bbb Z[\sqrt d]$ is an ordered ring

I'm trying to show that $\Bbb Z[\sqrt d]$ is an ordered ring, where $d$ is a positive non-square integer. This is obviously true given that $\Bbb Z[\sqrt d]\subseteq\Bbb R$, but here the catch is that I am working in a weak axiomatic framework, barely stronger than $\sf PA$, so I am trying to work with a barebones encoding of $\Bbb Z[\sqrt d]$ and prove everything relative to the encoding.

Define $\Bbb Z[\sqrt d]:=\Bbb Z\times\Bbb Z$, and let $(x,y)+(x',y')=(x+x',y+y')$ and $(x,y)(x',y')=(xx'+dyy',xy'+yx')$. Given these definitions, it is possible to show that $\Bbb Z[\sqrt d]$ is a ring, simply by unfolding all the definitions and using ring axioms of $\Bbb Z$.

$\Bbb Z$ itself is defined as the disjoint union of two copies of $\Bbb N$, so that every integer $x$ is of the form $n$ or $-(n+1)$ where $n\in\Bbb N$. Given this, we can define $P(x,y)$ (which asserts that $(x,y)$ is nonnegative) by case analysis (where $m,n$ are variables in $\Bbb N$): \begin{align} P(m,n)&\equiv\top\\ P(m,-(n+1))&\equiv m^2\ge d(n+1)^2\\ P(-(m+1),n)&\equiv (m+1)^2\le dn^2\\ P(-(m+1),-(n+1))&\equiv \bot\\ \end{align}

and then say that $(x,y)\le(x',y')$ iff $P(x'-x,y'-y)$.

This definition is correct in the sense that under the interpretation $(x,y)\mapsto x+y\sqrt d$ we have the usual meanings of $+,\cdot,\le$, but the case analysis leads to a lot of cases to check, and I wonder if there isn't a better way. Currently, I'm stuck on showing that $P(a)\wedge P(b)\to P(ab)$, which involves roughly 64 cases (since $x,y,x',y',xx'+dyy',xy'+yx'$ can all be positive or negative), each of which involves some inequality on the natural numbers like:

$$x^2\ge d(y+1)^2,\ \ d (y+1) w+i=xz,\ \ xw+(j+1) = (y+1)z\ \vdash \ i^2\le d(j+1)^2.$$

(This is the case where $a=(x,-(y+1)), b=(z,w), ab=(i,-(j+1))$.) Is there a better way? Although I think it is possible to finish the proof in this manner, I get the strong feeling that I have made this more complicated than it needs to be, especially since the proof over the reals is so simple.

• @user1952009 The problem is that I don't know that $x+y\sqrt d$ exists in the first place. I only have $\Bbb N$ and $\Bbb Z$ (and maybe $\Bbb Q$ although I don't think that would help). I definitely don't have $\Bbb R$, so there is no number $\sqrt d$ to point to, and I have to make do with inequalities of integers. – Mario Carneiro Apr 22 '17 at 23:00
• $x+ y\sqrt{d} \ge u+ v\sqrt{d}$ iff $(y-v)\sqrt{d} \ge u-x$. Then test the sign : if $y-v$ and $u-v$ are of opposite sign it is easy, otherwise $s =\text{sign}(y-b)$, look at $s (y-v)^2d\ge s (u-x)^2$. This is just a notation : you don't need any knowledge about what it means ! Then what you need is showing it works with the addition and the multiplication in $\mathbb{Z}[\sqrt{d}]$ – reuns Apr 22 '17 at 23:07