The Earlier and the New Versions of the Definitions of the Natural Numbers, the Complex Numbers, the Conjugate and the Modulus Agree, and the Two Versions of Real Correspond

In the setting of The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers.

(i) Natural numbers. The set $\mathbb{N}$ of natural numbers and the number $1$ of The Set of Natural Numbers and the Number One (ii) are the set $\mathbb{N}$ of natural numbers and the number $1$ of The Set of Natural Numbers and the Number One (ii).

(ii) Complex numbers. The set $\mathbb{C}$ of complex numbers of the earlier version, its sum and product and its imaginary unit $i$ are the set of complex numbers of the new version, its sum and product and its imaginary unit.

(iii) Complex conjugate. For every complex number $z$, the complex conjugate $\overline{z}$ of $z$ in the earlier version is the complex conjugate of $z$ in the new version.

(iv) Modulus. For every complex number $z$, the modulus $|z|$ of $z$ in the earlier version and the modulus of $z$ in the new version are the same real number.

(v) The two versions of Real. For an element $x$ of $\mathrm{Real}$ in the sense of The Real Numbers as a Type (i), let $\hat{x}$ be the element of $\mathrm{Real}$ in the sense of The Real Numbers as a Type (i) with the same set. Then $x\mapsto\hat{x}$ is a one-to-one correspondence between the two, and, with $0$, $1$, $+$, $\cdot$, $-$, $\le$ and $<$ on each side as in The Real Numbers as a Type (ii) and The Real Numbers as a Type (ii), for all $x$ and $y$

$$\hat{0}=0,\quad \hat{1}=1,\quad \widehat{x+y}=\hat{x}+\hat{y},\quad \widehat{x\cdot y}=\hat{x}\cdot\hat{y},\quad \widehat{-x}=-\hat{x},\quad \widehat{x-y}=\hat{x}-\hat{y},\quad x\le y\iff\hat{x}\le\hat{y},\quad x<y\iff\hat{x}<\hat{y};$$

hence the correspondence also preserves numerals and powers, read as in The Real Numbers as a Type (iii) and The Real Numbers as a Type (iii): for every natural number $n$, every integer $i$ and every $x$, it maps $n$ to $n$, $i$ to $i$, $x^{n}$ to $\hat{x}^{n}$, $n\cdot x$ to $n\cdot\hat{x}$ and $i\cdot x$ to $i\cdot\hat{x}$. For $x\ne0$, the reciprocal of $x$ is mapped to the reciprocal of $\hat{x}$.