Proof of The Complex Numbers Form a Field Containing the Real Numbers: i Squared Is -1 and Not Real, the Canonical Form a + bi and Its Arithmetic, and Numerals

Each result cited is universally quantified over the data in its own statement.

Preliminaries. By The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals, $\mathbb{R}$ is an ordered field, so the rules of arithmetic and order in force there are used for real numbers without further citation; in particular $0\neq1$ in $\mathbb{R}$ by Fields §field. $\mathbb{C}=\mathbb{R}\times\mathbb{R}$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §set. For $a,b\in\mathbb{R}$ the pair $(a,b)$ lies in $\mathbb{C}$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, and every $z\in\mathbb{C}$ is $z=(a,b)$ for some $a,b\in\mathbb{R}$ by The Cartesian Product of Two Classes §product. For $a,b,c,d\in\mathbb{R}$, $(a,b)=(c,d)$ if and only if $a=c$ and $b=d$, by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; every equation between elements of $\mathbb{C}$ below is checked componentwise in this way. By The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit §operations, $+$ and $\cdot$ are binary operations on $\mathbb{C}$, given by

$$(a,b)+(c,d)=(a+c,\,b+d),\qquad (a,b)\cdot(c,d)=(ac-bd,\,ad+bc).$$

For $a\in\mathbb{R}$, since $2=1+1$ by Arithmetic and Order of the Natural Numbers §digits, $a^{2}=a^{1+1}=a^{1}a^{1}=aa$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §exponents and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product.

Clause field. Let $x=(a,b)$, $y=(c,d)$ and $z=(e,f)$ be elements of $\mathbb{C}$, with $a,b,c,d,e,f\in\mathbb{R}$; $(0,0)$ and $(1,0)$ lie in $\mathbb{C}$. We check the conditions of Commutative Rings §ring, using the commutative ring laws of $\mathbb{R}$ in each component.

Associativity of $+$: $(x+y)+z=((a+c)+e,\,(b+d)+f)=(a+(c+e),\,b+(d+f))=x+(y+z)$.

Commutativity of $+$: $x+y=(a+c,\,b+d)=(c+a,\,d+b)=y+x$.

Zero: $x+(0,0)=(a+0,\,b+0)=(a,b)=x$.

Negatives: $w=(-a,-b)\in\mathbb{C}$ and $x+w=(a+(-a),\,b+(-b))=(0,0)$.

Associativity of $\cdot$: on the one hand

$$(x\cdot y)\cdot z=(ac-bd,\,ad+bc)\cdot(e,f)=\big((ac-bd)e-(ad+bc)f,\,(ac-bd)f+(ad+bc)e\big)=(ace-bde-adf-bcf,\,acf-bdf+ade+bce);$$

on the other hand

$$x\cdot(y\cdot z)=(a,b)\cdot(ce-df,\,cf+de)=\big(a(ce-df)-b(cf+de),\,a(cf+de)+b(ce-df)\big)=(ace-adf-bcf-bde,\,acf+ade+bce-bdf).$$

The two agree componentwise.

Commutativity of $\cdot$: $y\cdot x=(ca-db,\,cb+da)=(ac-bd,\,ad+bc)=x\cdot y$.

Unit: $x\cdot(1,0)=(a\cdot1-b\cdot0,\,a\cdot0+b\cdot1)=(a,b)=x$.

Distributivity:

$$x\cdot(y+z)=(a,b)\cdot(c+e,\,d+f)=\big(a(c+e)-b(d+f),\,a(d+f)+b(c+e)\big)=\big((ac-bd)+(ae-bf),\,(ad+bc)+(af+be)\big)=x\cdot y+x\cdot z.$$

Hence $\mathbb{C}$, with $+$, $\cdot$, $(0,0)$ and $(1,0)$, is a commutative ring by Commutative Rings §ring. Moreover $(0,0)\neq(1,0)$ because $0\neq1$ in $\mathbb{R}$.

Let now $x=(a,b)\neq(0,0)$, so $a\neq0$ or $b\neq0$, and put $s=a^{2}+b^{2}=aa+bb$. In $\mathbb{R}$, $0\le aa$ and $0\le bb$, and a product of nonzero elements is nonzero; so if $a\neq0$ then $0<aa$, and if $b\neq0$ then $0<bb$. In either case $0<aa+bb=s$, so $s\neq0$. Let $y'=(a/s,\,-b/s)\in\mathbb{C}$. Then

$$x\cdot y'=\Big(a\frac{a}{s}-b\frac{-b}{s},\;a\frac{-b}{s}+b\frac{a}{s}\Big)=\Big(\frac{aa+bb}{s},\;\frac{-ab+ab}{s}\Big)=(1,0).$$

So every nonzero element of $\mathbb{C}$ has some $y'$ with $x\cdot y'=(1,0)$, and $\mathbb{C}$ is a field by Fields §field.

By Negatives, Differences, Reciprocals and Quotients §negative, the negative $-(a,b)$ is the unique $w\in\mathbb{C}$ with $(a,b)+w=(0,0)$, unique by Additive and Multiplicative Inverses Are Unique §negative; the element $(-a,-b)$ found above has this property, so $-(a,b)=(-a,-b)$. Likewise, for $(a,b)\neq(0,0)$, by Negatives, Differences, Reciprocals and Quotients §reciprocal the reciprocal $(a,b)^{-1}$ is the unique $y\in\mathbb{C}$ with $(a,b)\cdot y=(1,0)$, unique by Additive and Multiplicative Inverses Are Unique §reciprocal; the element $y'$ has this property, so $(a,b)^{-1}=(a/(a^{2}+b^{2}),\,-b/(a^{2}+b^{2}))$.

Clause embedding. For $a\in\mathbb{R}$, $(a,0)\in\mathbb{C}$, so $\iota$ is the map of Maps and Relations Given by Formulas §map, with $\iota(a)=(a,0)$. If $\iota(a)=\iota(a')$ for $a,a'\in\mathbb{R}$, then $(a,0)=(a',0)$, so $a=a'$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic; thus $\iota$ is injective by Injective, Surjective and Bijective Functions between Classes §injective. Plainly $\iota(0)=(0,0)$ and $\iota(1)=(1,0)$, the zero and the unit of $\mathbb{C}$ by the clause field. For $a,b\in\mathbb{R}$,

$$\iota(a)+\iota(b)=(a+b,\,0+0)=(a+b,\,0)=\iota(a+b),\qquad \iota(a)\cdot\iota(b)=(ab-0\cdot0,\,a\cdot0+0\cdot b)=(ab,\,0)=\iota(ab).$$

Hence $\iota(a)+\iota(-a)=\iota(a+(-a))=\iota(0)=(0,0)$, so $\iota(-a)$ is the unique $w\in\mathbb{C}$ with $\iota(a)+w=(0,0)$, that is, $\iota(-a)=-\iota(a)$ by Negatives, Differences, Reciprocals and Quotients §negative. Let moreover $a\neq0$. Then $\iota(a)\neq\iota(0)=(0,0)$ by injectivity, and $\iota(a)\cdot\iota(a^{-1})=\iota(aa^{-1})=\iota(1)=(1,0)$, so $\iota(a^{-1})$ is the unique $y\in\mathbb{C}$ with $\iota(a)\cdot y=(1,0)$, that is, $\iota(a^{-1})=\iota(a)^{-1}$ by Negatives, Differences, Reciprocals and Quotients §reciprocal.

Clause imaginary-unit. By The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit §imaginary-unit, $i=(0,1)$, so

$$i\cdot i=(0,1)\cdot(0,1)=(0\cdot0-1\cdot1,\,0\cdot1+1\cdot0)=(-1,\,0)=\iota(-1),$$

and $\iota(-1)=-\iota(1)$ by the clause embedding.

Clause not-real. Let $a\in\mathbb{R}$. If $i=\iota(a)$, then $(0,1)=(a,0)$, so $1=0$ in $\mathbb{R}$ by The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §characteristic, contradicting $0\neq1$ from the preliminaries. Hence $i\neq\iota(a)$.

Clause canonical. Let $a,b\in\mathbb{R}$. Then

$$\iota(b)\cdot i=(b,0)\cdot(0,1)=(b\cdot0-0\cdot1,\,b\cdot1+0\cdot0)=(0,\,b),\qquad \iota(a)+\iota(b)\cdot i=(a,0)+(0,b)=(a+0,\,0+b)=(a,b).$$

Let $z\in\mathbb{C}$. By the preliminaries $z=(a,b)$ for some $a,b\in\mathbb{R}$, and then $z=\iota(a)+\iota(b)\cdot i$ by what was just shown, so such a pair exists. If also $z=\iota(a')+\iota(b')\cdot i$ with $a',b'\in\mathbb{R}$, then by the same identity $(a,b)=z=(a',b')$, so the pair is the same; thus it is unique.

Clause arithmetic. Let $a,b,c,d\in\mathbb{R}$. By the clause canonical and The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit §operations,

$$\big(\iota(a)+\iota(b)\cdot i\big)+\big(\iota(c)+\iota(d)\cdot i\big)=(a,b)+(c,d)=(a+c,\,b+d),\qquad \big(\iota(a)+\iota(b)\cdot i\big)\cdot\big(\iota(c)+\iota(d)\cdot i\big)=(a,b)\cdot(c,d)=(ac-bd,\,ad+bc).$$

Since $a+c$, $b+d$, $ac-bd$ and $ad+bc$ lie in $\mathbb{R}$, the clause canonical gives $(a+c,\,b+d)=\iota(a+c)+\iota(b+d)\cdot i$ and $(ac-bd,\,ad+bc)=\iota(ac-bd)+\iota(ad+bc)\cdot i$, which proves both identities.

Clause numerals. By the clause field, $\mathbb{C}$, with $+$, $\cdot$, $(0,0)$ and $(1,0)$, is a field and so a commutative ring by Fields §field; so is $\mathbb{R}$, with its zero $0$ and unit $1$, by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness §reals. Hence The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products applies to both. We show $n_{\mathbb{C}}=\iota(n_{\mathbb{R}})$ by induction on $n\in\mathbb{N}_{0}$, by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction.

For $n=0$: by The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products §constants, $0_{\mathbb{R}}=0$ and $0_{\mathbb{C}}=(0,0)$, and $\iota(0)=(0,0)$ by the clause embedding; so $0_{\mathbb{C}}=\iota(0_{\mathbb{R}})$.

Let $n\in\mathbb{N}_{0}$ with $n_{\mathbb{C}}=\iota(n_{\mathbb{R}})$. By The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products §sum and The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products §constants, $(n+1)_{\mathbb{R}}=n_{\mathbb{R}}+1_{\mathbb{R}}=n_{\mathbb{R}}+1$ and $(n+1)_{\mathbb{C}}=n_{\mathbb{C}}+1_{\mathbb{C}}=n_{\mathbb{C}}+(1,0)$. By the clause embedding, $\iota(1)=(1,0)$ and $\iota$ preserves sums, so

$$\iota\big((n+1)_{\mathbb{R}}\big)=\iota(n_{\mathbb{R}})+\iota(1)=n_{\mathbb{C}}+(1,0)=(n+1)_{\mathbb{C}}.$$

Hence $n_{\mathbb{C}}=\iota(n_{\mathbb{R}})$ for every $n\in\mathbb{N}_{0}$.