Vtyjkyuk

Given a set of natural numbers $mathbbN$ in ZFC, we define $mathbbZ$ by first defining an equivalence relation $simeq$ on $mathbbNtimesmathbbN$: $(n,m) simeq (n',m') Longleftrightarrow n + m' = n' + m$. Then we consider the set $(mathbbNtimesmathbbN)/simeq$ of equivalence classes of $mathbbNtimesmathbbN$ with respect to $simeq$ as the set of integers $mathbbZ$.

However, we then need to define a linear ordering $leq$ on our newfound $mathbbZ$. The idea is to set $[(n,m)] leq [(n',m')]$ whenever $n + m' leq n' + m$. I'm having a trouble in showing that this definition doesn't depend on the choie of $(n,m) leq (n',m')$. That is, that for any natural numbers $n_1,m_1,n_2,m_2,n_3,m_3,n_4,m_4$ if we have
$$n_1 + m_3 leq n_3 + m_1,$$
$$n_1 + m_2 = n_2 + m_1,$$
$$n_3 + m_4 = n_4 + m_3,$$
then we have
$$n_2 + m_4 leq n_4 + m_2.$$
Any help would be appreciated.

Well we can go and do a straightforward verification using the definition of the equivalence relation.

Suppose $(n,m)simeq(n',m')$ and $(i,j)simeq(i',j')$, and suppose that $[(i,j)]leq[(n,m)]$. Namely, $i+mleq n+j$. We want to prove that $i'+m'leq n'+j'$.

What do we know? We know that $i+j'=i'+j$ and $n+m'=n'+m$.

$$beginalign*
i+m&leq n+j\
i+m+n'+j'&leq n+j+n'+j'\
i+j'+m+n'&leq n+n'+j+j'\
i'+j+m'+n&leq n+n'+j+j'\
i'+m'+j+n&leq n'+j'+j+ n\
i'+m'&leq n'+j'
endalign*$$
Which is what we wanted.

My preferred way is to show that every integer has a unique representative that is either $[(0, m)]$ or $[(m, 0)]$. Once you've done that, then the order's uniqueness follows immediately.

$$n_1 + m_3 leq n_3 + m_1 implies m_3-n_3le m_1 - n_1 $$

$$n_1 + m_2 = n_2 + m_1implies m_1 - n_1=m_2 - n_2 $$

$$n_3 + m_4 = n_4 + m_3 implies m_4-n_4=m_3-n_3 $$

Thus $$ m_4-n_4=m_3-n_3le m_1 - n_1=m_2 - n_2$$
Which implies

$$n_2 + m_4 leq n_4 + m_2$$.