IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Complex_ZF imports func_ZF_1 OrderedField_ZF
begin

The goal of this theory is to define complex numbers and prove that the Metamath complex numbers axioms hold.

From complete ordered fields to complex numbers

This section consists mostly of definitions and a proof context for talking about complex numbers. Suppose we have a set \(R\) with binary operations \(A\) and \(M\) and a relation \(r\) such that the quadruple \((R,A,M,r)\) forms a complete ordered field. The next definitions take \((R,A,M,r)\) and construct the sets that represent the structure of complex numbers: the carrier (\(\mathbb{C}=R\times R\)), binary operations of addition and multiplication of complex numbers and the order relation on \(\mathbb{R}=R\times 0\). The \( ImCxAdd, ReCxAdd, ImCxMul, ReCxMul \) are helper meta-functions representing the imaginary part of a sum of complex numbers, the real part of a sum of real numbers, the imaginary part of a product of complex numbers and the real part of a product of real numbers, respectively. The actual operations (subsets of \((R\times R)\times R\) are named CplxAdd and CplxMul. When \(R\) is an ordered field, it comes with an order relation. This induces a natural strict order relation on \(\{\langle x,0\rangle : x\in R\}\subseteq R\times R\). We call the set \(\{\langle x,0\rangle : x\in R\}\) \( \text{ComplexReals}(R,A) \) and the strict order relation \( \text{CplxROrder}(R,A,r) \). The order on the real axis of complex numbers is defined as the relation induced on it by the canonical projection on the first coordinate and the order we have on the real numbers. OK, lets repeat this slower. We start with the order relation \(r\) on a (model of) real numbers \(R\). We want to define an order relation on a subset of complex numbers, namely on \(R\times \{0\}\). To do that we use the notion of a relation induced by a mapping. The mapping here is \(f:R\times \{0\}\rightarrow R, f\langle x,0 \rangle = x\) which is defined under a name of SliceProjection in func_ZF.thy. This defines a relation \(r_1\) (called \( \text{InducedRelation}(f,r) \), see func_ZF) on \(R\times \{0\}\) such that \( \langle \langle x, 0\rangle, \langle y,0\rangle \in r_1\) iff \(\langle x,y\rangle \in r\). This way we get what we call \( \text{CplxROrder}(R,A,r) \). However, this is not the end of the story, because Metamath uses strict inequalities in its axioms, rather than weak ones like IsarMathLib (mostly). So we need to take the strict version of this order relation. This is done in the syntax definition of \( \lt _{\mathbb{R}} \) in the definition of complex0 context. Since Metamath proves a lot of theorems about the real numbers extended with \(+\infty\) and \(-\infty\), we define the notation for inequalites on the extended real line as well.

A helper expression representing the real part of the sum of two complex numbers.

definition

\( \text{ReCxAdd}(R,A,a,b) \equiv A\langle \text{fst}(a),\text{fst}(b)\rangle \)

An expression representing the imaginary part of the sum of two complex numbers.

definition

\( \text{ImCxAdd}(R,A,a,b) \equiv A\langle \text{snd}(a),\text{snd}(b)\rangle \)

The set (function) that is the binary operation that adds complex numbers.

definition

\( \text{CplxAdd}(R,A) \equiv \) \( \{\langle p, \langle \text{ReCxAdd}(R,A,\text{fst}(p),\text{snd}(p)), \text{ImCxAdd}(R,A,\text{fst}(p),\text{snd}(p)) \rangle \rangle .\ \) \( p\in (R\times R)\times (R\times R)\} \)

The expression representing the imaginary part of the product of complex numbers.

definition

\( \text{ImCxMul}(R,A,M,a,b) \equiv A\langle M\langle \text{fst}(a),\text{snd}(b)\rangle , M\langle \text{snd}(a),\text{fst}(b)\rangle \rangle \)

The expression representing the real part of the product of complex numbers.

definition

\( \text{ReCxMul}(R,A,M,a,b) \equiv \) \( A\langle M\langle \text{fst}(a),\text{fst}(b)\rangle , \text{GroupInv}(R,A)(M\langle \text{snd}(a),\text{snd}(b)\rangle )\rangle \)

The function (set) that represents the binary operation of multiplication of complex numbers.

definition

\( \text{CplxMul}(R,A,M) \equiv \) \( \{ \langle p, \langle \text{ReCxMul}(R,A,M,\text{fst}(p),\text{snd}(p)), \text{ImCxMul}(R,A,M,\text{fst}(p),\text{snd}(p))\rangle \rangle .\ \) \( p \in (R\times R)\times (R\times R)\} \)

The definition real numbers embedded in the complex plane.

definition

\( \text{ComplexReals}(R,A) \equiv R\times \{\text{ TheNeutralElement}(R,A)\} \)

Definition of order relation on the real line.

definition

\( \text{CplxROrder}(R,A,r) \equiv \) \( \text{InducedRelation}( \text{SliceProjection}( \text{ComplexReals}(R,A)),r) \)

The next locale defines proof context and notation that will be used for complex numbers.

locale complex0

assumes R_are_reals: \( \text{IsAmodelOfReals}(R,A,M,r) \)

defines \( \mathbb{C} \equiv R\times R \)

defines \( 1 _R \equiv \text{ TheNeutralElement}(R,M) \)

defines \( 0 _R \equiv \text{ TheNeutralElement}(R,A) \)

defines \( 1 \equiv \langle 1 _R, 0 _R\rangle \)

defines \( 0 \equiv \langle 0 _R, 0 _R\rangle \)

defines \( \imath \equiv \langle 0 _R,1 _R\rangle \)

defines \( \mathbb{R} \equiv \{\langle r, 0 _R\rangle .\ r\in R\} \)

defines \( a \cdot b \equiv M\langle a,b\rangle \)

defines \( a + b \equiv A\langle a,b\rangle \)

defines \( - a \equiv \text{GroupInv}(R,A)(a) \)

defines \( a + b \equiv \text{CplxAdd}(R,A)\langle a,b\rangle \)

defines \( a \cdot b \equiv \text{CplxMul}(R,A,M)\langle a,b\rangle \)

defines \( a / b \equiv \bigcup \{ x \in \mathbb{C} .\ b \cdot x = a \} \)

defines \( a - b \equiv \bigcup \{ x \in \mathbb{C} .\ b + x = a \} \)

defines \( - a \equiv 0 - a \)

defines \( a \lt _{\mathbb{R}} b \equiv \langle a,b\rangle \in \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

defines \( +\infty \equiv \mathbb{C} \)

defines \( -\infty \equiv \{\mathbb{C} \} \)

defines \( \mathbb{R} ^* \equiv \mathbb{R} \cup \{+\infty ,-\infty \} \)

defines \( \mathbb{N} \equiv \bigcap \{N \in Pow(\mathbb{R} ).\ 1 \in N \wedge (\forall n.\ n\in N \longrightarrow n + 1 \in N)\} \)

defines \( \lt \equiv \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \cap \mathbb{R} \times \mathbb{R} \cup \) \( \{\langle -\infty ,+\infty \rangle \} \cup (\mathbb{R} \times \{+\infty \}) \cup (\{-\infty \}\times \mathbb{R} ) \)

defines \( a \lt b \equiv \langle a,b\rangle \in \lt \)

defines \( a \leq b \equiv \neg (b \lt a) \)

defines \( 2 \equiv 1 + 1 \)

defines \( 3 \equiv 2 + 1 \)

defines \( 4 \equiv 3 + 1 \)

defines \( 5 \equiv 4 + 1 \)

defines \( 6 \equiv 5 + 1 \)

defines \( 7 \equiv 6 + 1 \)

defines \( 8 \equiv 7 + 1 \)

defines \( 9 \equiv 8 + 1 \)

Axioms of complex numbers

In this section we will prove that all Metamath's axioms of complex numbers hold in the complex0 context.

The next lemma lists some contexts that are valid in the complex0 context.

lemma (in complex0) valid_cntxts:

shows \( field1(R,A,M,r) \), \( field0(R,A,M) \), \( ring1(R,A,M,r) \), \( group3(R,A,r) \), \( ring0(R,A,M) \), \( M \text{ is commutative on } R \), \( group0(R,A) \)proof
from R_are_reals have I: \( \text{IsAnOrdField}(R,A,M,r) \) using IsAmodelOfReals_def
then show \( field1(R,A,M,r) \) using OrdField_ZF_1_L2
then show \( ring1(R,A,M,r) \) and I: \( field0(R,A,M) \) using field1.axioms, ring1_def, OrdField_ZF_1_L1B
then show \( group3(R,A,r) \) using OrdRing_ZF_1_L4
from I have \( \text{IsAfield}(R,A,M) \) using Field_ZF_1_L1
then have \( \text{IsAring}(R,A,M) \) and \( M \text{ is commutative on } R \) using IsAfield_def
then show \( ring0(R,A,M) \) and \( M \text{ is commutative on } R \) using ring0_def
then show \( group0(R,A) \) using Ring_ZF_1_L1
qed

The next lemma shows the definition of real and imaginary part of complex sum and product in a more readable form using notation defined in complex0 locale.

lemma (in complex0) cplx_mul_add_defs:

shows \( \text{ReCxAdd}(R,A,\langle a,b\rangle ,\langle c,d\rangle ) = a + c \), \( \text{ImCxAdd}(R,A,\langle a,b\rangle ,\langle c,d\rangle ) = b + d \), \( \text{ImCxMul}(R,A,M,\langle a,b\rangle ,\langle c,d\rangle ) = a\cdot d + b\cdot c \), \( \text{ReCxMul}(R,A,M,\langle a,b\rangle ,\langle c,d\rangle ) = a\cdot c + ( - b\cdot d) \)proof
let \( z_1 = \langle a,b\rangle \)
let \( z_2 = \langle c,d\rangle \)
have \( \text{ReCxAdd}(R,A,z_1,z_2) \equiv A\langle \text{fst}(z_1),\text{fst}(z_2)\rangle \) by (rule ReCxAdd_def )
moreover
have \( \text{ImCxAdd}(R,A,z_1,z_2) \equiv A\langle \text{snd}(z_1),\text{snd}(z_2)\rangle \) by (rule ImCxAdd_def )
moreover
have \( \text{ImCxMul}(R,A,M,z_1,z_2) \equiv A\langle M \lt \text{fst}(z_1),\text{snd}(z_2)>,M \lt \text{snd}(z_1),\text{fst}(z_2)>\rangle \) by (rule ImCxMul_def )
moreover
have \( \text{ReCxMul}(R,A,M,z_1,z_2) \equiv \) \( A\langle M \lt \text{fst}(z_1),\text{fst}(z_2)>, \text{GroupInv}(R,A)(M\langle \text{snd}(z_1),\text{snd}(z_2)\rangle )\rangle \) by (rule ReCxMul_def )
ultimately show \( \text{ReCxAdd}(R,A,z_1,z_2) = a + c \), \( \text{ImCxAdd}(R,A,\langle a,b\rangle ,\langle c,d\rangle ) = b + d \), \( \text{ImCxMul}(R,A,M,\langle a,b\rangle ,\langle c,d\rangle ) = a\cdot d + b\cdot c \), \( \text{ReCxMul}(R,A,M,\langle a,b\rangle ,\langle c,d\rangle ) = a\cdot c + ( - b\cdot d) \)
qed

Real and imaginary parts of sums and products of complex numbers are real.

lemma (in complex0) cplx_mul_add_types:

assumes A1: \( z_1 \in \mathbb{C} \), \( z_2 \in \mathbb{C} \)

shows \( \text{ReCxAdd}(R,A,z_1,z_2) \in R \), \( \text{ImCxAdd}(R,A,z_1,z_2) \in R \), \( \text{ImCxMul}(R,A,M,z_1,z_2) \in R \), \( \text{ReCxMul}(R,A,M,z_1,z_2) \in R \)proof
let \( a = \text{fst}(z_1) \)
let \( b = \text{snd}(z_1) \)
let \( c = \text{fst}(z_2) \)
let \( d = \text{snd}(z_2) \)
from A1 have \( a \in R \), \( b \in R \), \( c \in R \), \( d \in R \)
then have \( a + c \in R \), \( b + d \in R \), \( a\cdot d + b\cdot c \in R \), \( a\cdot c + ( - b\cdot d) \in R \) using valid_cntxts, Ring_ZF_1_L4
with A1 show \( \text{ReCxAdd}(R,A,z_1,z_2) \in R \), \( \text{ImCxAdd}(R,A,z_1,z_2) \in R \), \( \text{ImCxMul}(R,A,M,z_1,z_2) \in R \), \( \text{ReCxMul}(R,A,M,z_1,z_2) \in R \) using cplx_mul_add_defs
qed

Complex reals are complex. Recall the definition of \( \mathbb{R} \) in the complex0 locale.

lemma (in complex0) axresscn:

shows \( \mathbb{R} \subseteq \mathbb{C} \) using valid_cntxts, group0_2_L2

Complex \(1\) is not complex \(0\).

lemma (in complex0) ax1ne0:

shows \( 1 \neq 0 \)proof
have \( \text{IsAfield}(R,A,M) \) using valid_cntxts, Field_ZF_1_L1
then show \( 1 \neq 0 \) using IsAfield_def
qed

Complex addition is a complex valued binary operation on complex numbers.

lemma (in complex0) axaddopr:

shows \( \text{CplxAdd}(R,A): \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \)proof
have \( \forall p \in \mathbb{C} \times \mathbb{C} .\ \) \( \langle \text{ReCxAdd}(R,A,\text{fst}(p),\text{snd}(p)), \text{ImCxAdd}(R,A,\text{fst}(p),\text{snd}(p))\rangle \in \mathbb{C} \) using cplx_mul_add_types
then have \( \{\langle p,\langle \text{ReCxAdd}(R,A,\text{fst}(p),\text{snd}(p)), \text{ImCxAdd}(R,A,\text{fst}(p),\text{snd}(p))\rangle \rangle .\ \) \( p \in \mathbb{C} \times \mathbb{C} \}: \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) by (rule ZF_fun_from_total )
then show \( \text{CplxAdd}(R,A): \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) using CplxAdd_def
qed

Complex multiplication is a complex valued binary operation on complex numbers.

lemma (in complex0) axmulopr:

shows \( \text{CplxMul}(R,A,M): \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \)proof
have \( \forall p \in \mathbb{C} \times \mathbb{C} .\ \) \( \langle \text{ReCxMul}(R,A,M,\text{fst}(p),\text{snd}(p)), \text{ImCxMul}(R,A,M,\text{fst}(p),\text{snd}(p))\rangle \in \mathbb{C} \) using cplx_mul_add_types
then have \( \{\langle p,\langle \text{ReCxMul}(R,A,M,\text{fst}(p),\text{snd}(p)), \text{ImCxMul}(R,A,M,\text{fst}(p),\text{snd}(p))\rangle \rangle .\ \) \( p \in \mathbb{C} \times \mathbb{C} \}: \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) by (rule ZF_fun_from_total )
then show \( \text{CplxMul}(R,A,M): \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) using CplxMul_def
qed

What are the values of omplex addition and multiplication in terms of their real and imaginary parts?

lemma (in complex0) cplx_mul_add_vals:

assumes A1: \( a\in R \), \( b\in R \), \( c\in R \), \( d\in R \)

shows \( \langle a,b\rangle + \langle c,d\rangle = \langle a + c, b + d\rangle \), \( \langle a,b\rangle \cdot \langle c,d\rangle = \langle a\cdot c + ( - b\cdot d), a\cdot d + b\cdot c\rangle \)proof
let \( S = \text{CplxAdd}(R,A) \)
let \( P = \text{CplxMul}(R,A,M) \)
let \( p = \langle \langle a,b\rangle , \langle c,d\rangle \rangle \)
from A1 have \( S : \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) and \( p \in \mathbb{C} \times \mathbb{C} \) using axaddopr
moreover
have \( S = \{\langle p, \lt \text{ReCxAdd}(R,A,\text{fst}(p),\text{snd}(p)), \text{ImCxAdd}(R,A,\text{fst}(p),\text{snd}(p))>\rangle .\ \) \( p \in \mathbb{C} \times \mathbb{C} \} \) using CplxAdd_def
ultimately have \( S(p) = \langle \text{ReCxAdd}(R,A,\text{fst}(p),\text{snd}(p)), \text{ImCxAdd}(R,A,\text{fst}(p),\text{snd}(p))\rangle \) by (rule ZF_fun_from_tot_val )
then show \( \langle a,b\rangle + \langle c,d\rangle = \langle a + c, b + d\rangle \) using cplx_mul_add_defs
from A1 have \( P : \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) and \( p \in \mathbb{C} \times \mathbb{C} \) using axmulopr
moreover
have \( P = \{\langle p, \langle \text{ReCxMul}(R,A,M,\text{fst}(p),\text{snd}(p)), \text{ImCxMul}(R,A,M,\text{fst}(p),\text{snd}(p))\rangle \rangle .\ \) \( p \in \mathbb{C} \times \mathbb{C} \} \) using CplxMul_def
ultimately have \( P(p) = \langle \text{ReCxMul}(R,A,M,\text{fst}(p),\text{snd}(p)), \text{ImCxMul}(R,A,M,\text{fst}(p),\text{snd}(p))\rangle \) by (rule ZF_fun_from_tot_val )
then show \( \langle a,b\rangle \cdot \langle c,d\rangle = \langle a\cdot c + ( - b\cdot d), a\cdot d + b\cdot c\rangle \) using cplx_mul_add_defs
qed

Complex multiplication is commutative.

lemma (in complex0) axmulcom:

assumes A1: \( a \in \mathbb{C} \), \( b \in \mathbb{C} \)

shows \( a\cdot b = b\cdot a \) using assms, cplx_mul_add_vals, valid_cntxts, Ring_ZF_1_L4, field_mult_comm

A sum of complex numbers is complex.

lemma (in complex0) axaddcl:

assumes \( a \in \mathbb{C} \), \( b \in \mathbb{C} \)

shows \( a + b \in \mathbb{C} \) using assms, axaddopr, apply_funtype

A product of complex numbers is complex.

lemma (in complex0) axmulcl:

assumes \( a \in \mathbb{C} \), \( b \in \mathbb{C} \)

shows \( a\cdot b \in \mathbb{C} \) using assms, axmulopr, apply_funtype

Multiplication is distributive with respect to addition.

lemma (in complex0) axdistr:

assumes A1: \( a \in \mathbb{C} \), \( b \in \mathbb{C} \), \( c \in \mathbb{C} \)

shows \( a\cdot (b + c) = a\cdot b + a\cdot c \)proof
let \( a_r = \text{fst}(a) \)
let \( a_i = \text{snd}(a) \)
let \( b_r = \text{fst}(b) \)
let \( b_i = \text{snd}(b) \)
let \( c_r = \text{fst}(c) \)
let \( c_i = \text{snd}(c) \)
from A1 have T: \( a_r \in R \), \( a_i \in R \), \( b_r \in R \), \( b_i \in R \), \( c_r \in R \), \( c_i \in R \), \( b_r + c_r \in R \), \( b_i + c_i \in R \), \( a_r\cdot b_r + ( - a_i\cdot b_i) \in R \), \( a_r\cdot c_r + ( - a_i\cdot c_i) \in R \), \( a_r\cdot b_i + a_i\cdot b_r \in R \), \( a_r\cdot c_i + a_i\cdot c_r \in R \) using valid_cntxts, Ring_ZF_1_L4
with A1 have \( a\cdot (b + c) = \) \( \langle a_r\cdot (b_r + c_r) + ( - a_i\cdot (b_i + c_i)),a_r\cdot (b_i + c_i) + a_i\cdot (b_r + c_r)\rangle \) using cplx_mul_add_vals
moreover
from T have \( a_r\cdot (b_r + c_r) + ( - a_i\cdot (b_i + c_i)) =\) \( a_r\cdot b_r + ( - a_i\cdot b_i) + (a_r\cdot c_r + ( - a_i\cdot c_i)) \) and \( a_r\cdot (b_i + c_i) + a_i\cdot (b_r + c_r) =\) \( a_r\cdot b_i + a_i\cdot b_r + (a_r\cdot c_i + a_i\cdot c_r) \) using valid_cntxts, Ring_ZF_2_L6
moreover
from A1, T have \( \langle a_r\cdot b_r + ( - a_i\cdot b_i) + (a_r\cdot c_r + ( - a_i\cdot c_i)),\) \( a_r\cdot b_i + a_i\cdot b_r + (a_r\cdot c_i + a_i\cdot c_r)\rangle =\) \( a\cdot b + a\cdot c \) using cplx_mul_add_vals
ultimately show \( a\cdot (b + c) = a\cdot b + a\cdot c \)
qed

Complex addition is commutative.

lemma (in complex0) axaddcom:

assumes \( a \in \mathbb{C} \), \( b \in \mathbb{C} \)

shows \( a + b = b + a \) using assms, cplx_mul_add_vals, valid_cntxts, Ring_ZF_1_L4

Complex addition is associative.

lemma (in complex0) axaddass:

assumes A1: \( a \in \mathbb{C} \), \( b \in \mathbb{C} \), \( c \in \mathbb{C} \)

shows \( a + b + c = a + (b + c) \)proof
let \( a_r = \text{fst}(a) \)
let \( a_i = \text{snd}(a) \)
let \( b_r = \text{fst}(b) \)
let \( b_i = \text{snd}(b) \)
let \( c_r = \text{fst}(c) \)
let \( c_i = \text{snd}(c) \)
from A1 have T: \( a_r \in R \), \( a_i \in R \), \( b_r \in R \), \( b_i \in R \), \( c_r \in R \), \( c_i \in R \), \( a_r + b_r \in R \), \( a_i + b_i \in R \), \( b_r + c_r \in R \), \( b_i + c_i \in R \) using valid_cntxts, Ring_ZF_1_L4
with A1 have \( a + b + c = \langle a_r + b_r + c_r,a_i + b_i + c_i\rangle \) using cplx_mul_add_vals
also
from A1, T have \( \ldots = a + (b + c) \) using valid_cntxts, Ring_ZF_1_L11, cplx_mul_add_vals
finally show \( a + b + c = a + (b + c) \)
qed

Complex multiplication is associative.

lemma (in complex0) axmulass:

assumes A1: \( a \in \mathbb{C} \), \( b \in \mathbb{C} \), \( c \in \mathbb{C} \)

shows \( a \cdot b \cdot c = a \cdot (b \cdot c) \)proof
let \( a_r = \text{fst}(a) \)
let \( a_i = \text{snd}(a) \)
let \( b_r = \text{fst}(b) \)
let \( b_i = \text{snd}(b) \)
let \( c_r = \text{fst}(c) \)
let \( c_i = \text{snd}(c) \)
from A1 have T: \( a_r \in R \), \( a_i \in R \), \( b_r \in R \), \( b_i \in R \), \( c_r \in R \), \( c_i \in R \), \( a_r\cdot b_r + ( - a_i\cdot b_i) \in R \), \( a_r\cdot b_i + a_i\cdot b_r \in R \), \( b_r\cdot c_r + ( - b_i\cdot c_i) \in R \), \( b_r\cdot c_i + b_i\cdot c_r \in R \) using valid_cntxts, Ring_ZF_1_L4
with A1 have \( a \cdot b \cdot c = \) \( \langle (a_r\cdot b_r + ( - a_i\cdot b_i))\cdot c_r + ( - (a_r\cdot b_i + a_i\cdot b_r)\cdot c_i),\) \( (a_r\cdot b_r + ( - a_i\cdot b_i))\cdot c_i + (a_r\cdot b_i + a_i\cdot b_r)\cdot c_r\rangle \) using cplx_mul_add_vals
moreover
from A1, T have \( \langle a_r\cdot (b_r\cdot c_r + ( - b_i\cdot c_i)) + ( - a_i\cdot (b_r\cdot c_i + b_i\cdot c_r)),\) \( a_r\cdot (b_r\cdot c_i + b_i\cdot c_r) + a_i\cdot (b_r\cdot c_r + ( - b_i\cdot c_i))\rangle = \) \( a \cdot (b \cdot c) \) using cplx_mul_add_vals
moreover
from T have \( a_r\cdot (b_r\cdot c_r + ( - b_i\cdot c_i)) + ( - a_i\cdot (b_r\cdot c_i + b_i\cdot c_r)) =\) \( (a_r\cdot b_r + ( - a_i\cdot b_i))\cdot c_r + ( - (a_r\cdot b_i + a_i\cdot b_r)\cdot c_i) \) and \( a_r\cdot (b_r\cdot c_i + b_i\cdot c_r) + a_i\cdot (b_r\cdot c_r + ( - b_i\cdot c_i)) =\) \( (a_r\cdot b_r + ( - a_i\cdot b_i))\cdot c_i + (a_r\cdot b_i + a_i\cdot b_r)\cdot c_r \) using valid_cntxts, Ring_ZF_2_L6
ultimately show \( a \cdot b \cdot c = a \cdot (b \cdot c) \)
qed

Complex \(1\) is real. This really means that the pair \(\langle 1,0 \rangle\) is on the real axis.

lemma (in complex0) ax1re:

shows \( 1 \in \mathbb{R} \) using valid_cntxts, Ring_ZF_1_L2

The imaginary unit is a "square root" of \(-1\) (that is, \(i^2 +1 =0\)).

lemma (in complex0) axi2m1:

shows \( \imath \cdot \imath + 1 = 0 \) using valid_cntxts, Ring_ZF_1_L2, Ring_ZF_1_L3, cplx_mul_add_vals, Ring_ZF_1_L6, group0_2_L6

\(0\) is the neutral element of complex addition.

lemma (in complex0) ax0id:

assumes \( a \in \mathbb{C} \)

shows \( a + 0 = a \) using assms, cplx_mul_add_vals, valid_cntxts, Ring_ZF_1_L2, Ring_ZF_1_L3

The imaginary unit is a complex number.

lemma (in complex0) axicn:

shows \( \imath \in \mathbb{C} \) using valid_cntxts, Ring_ZF_1_L2

All complex numbers have additive inverses.

lemma (in complex0) axnegex:

assumes A1: \( a \in \mathbb{C} \)

shows \( \exists x\in \mathbb{C} .\ a + x = 0 \)proof
let \( a_r = \text{fst}(a) \)
let \( a_i = \text{snd}(a) \)
let \( x = \langle - a_r, - a_i\rangle \)
from A1 have T: \( a_r \in R \), \( a_i \in R \), \( ( - a_r) \in R \), \( ( - a_r) \in R \) using valid_cntxts, Ring_ZF_1_L3
then have \( x \in \mathbb{C} \) using valid_cntxts, Ring_ZF_1_L3
moreover
from A1, T have \( a + x = 0 \) using cplx_mul_add_vals, valid_cntxts, Ring_ZF_1_L3
ultimately show \( \exists x\in \mathbb{C} .\ a + x = 0 \)
qed

A non-zero complex number has a multiplicative inverse.

lemma (in complex0) axrecex:

assumes A1: \( a \in \mathbb{C} \) and A2: \( a\neq 0 \)

shows \( \exists x\in \mathbb{C} .\ a\cdot x = 1 \)proof
let \( a_r = \text{fst}(a) \)
let \( a_i = \text{snd}(a) \)
let \( m = a_r\cdot a_r + a_i\cdot a_i \)
from A1 have T1: \( a_r \in R \), \( a_i \in R \)
moreover
from A1, A2 have \( a_r \neq 0 _R \vee a_i \neq 0 _R \)
ultimately have \( \exists c\in R.\ m\cdot c = 1 _R \) using valid_cntxts, OrdField_ZF_1_L10
then obtain \( c \) where I: \( c\in R \) and II: \( m\cdot c = 1 _R \)
let \( x = \langle a_r\cdot c, - a_i\cdot c\rangle \)
from T1, I have T2: \( a_r\cdot c \in R \), \( ( - a_i\cdot c) \in R \) using valid_cntxts, Ring_ZF_1_L4, Ring_ZF_1_L3
then have \( x \in \mathbb{C} \)
moreover
from A1, T1, T2, I, II have \( a\cdot x = 1 \) using cplx_mul_add_vals, valid_cntxts, ring_rearr_3_elemA
ultimately show \( \exists x\in \mathbb{C} .\ a\cdot x = 1 \)
qed

Complex \(1\) is a right neutral element for multiplication.

lemma (in complex0) ax1id:

assumes A1: \( a \in \mathbb{C} \)

shows \( a\cdot 1 = a \) using assms, valid_cntxts, Ring_ZF_1_L2, cplx_mul_add_vals, Ring_ZF_1_L3, Ring_ZF_1_L6

A formula for sum of (complex) real numbers.

lemma (in complex0) sum_of_reals:

assumes \( a\in \mathbb{R} \), \( b\in \mathbb{R} \)

shows \( a + b = \langle \text{fst}(a) + \text{fst}(b), 0 _R\rangle \) using assms, valid_cntxts, Ring_ZF_1_L2, cplx_mul_add_vals, Ring_ZF_1_L3

The sum of real numbers is real.

lemma (in complex0) axaddrcl:

assumes A1: \( a\in \mathbb{R} \), \( b\in \mathbb{R} \)

shows \( a + b \in \mathbb{R} \) using assms, sum_of_reals, valid_cntxts, Ring_ZF_1_L4

The formula for the product of (complex) real numbers.

lemma (in complex0) prod_of_reals:

assumes A1: \( a\in \mathbb{R} \), \( b\in \mathbb{R} \)

shows \( a \cdot b = \langle \text{fst}(a)\cdot \text{fst}(b), 0 _R\rangle \)proof
let \( a_r = \text{fst}(a) \)
let \( b_r = \text{fst}(b) \)
from A1 have T: \( a_r \in R \), \( b_r \in R \), \( 0 _R \in R \), \( a_r\cdot b_r \in R \) using valid_cntxts, Ring_ZF_1_L2, Ring_ZF_1_L4
with A1 show \( a \cdot b = \langle a_r\cdot b_r, 0 _R\rangle \) using cplx_mul_add_vals, valid_cntxts, Ring_ZF_1_L2, Ring_ZF_1_L6, Ring_ZF_1_L3
qed

The product of (complex) real numbers is real.

lemma (in complex0) axmulrcl:

assumes \( a\in \mathbb{R} \), \( b\in \mathbb{R} \)

shows \( a \cdot b \in \mathbb{R} \) using assms, prod_of_reals, valid_cntxts, Ring_ZF_1_L4

The existence of a real negative of a real number.

lemma (in complex0) axrnegex:

assumes A1: \( a\in \mathbb{R} \)

shows \( \exists x \in \mathbb{R} .\ a + x = 0 \)proof
let \( a_r = \text{fst}(a) \)
let \( x = \langle - a_r, 0 _R\rangle \)
from A1 have T: \( a_r \in R \), \( ( - a_r) \in R \), \( 0 _R \in R \) using valid_cntxts, Ring_ZF_1_L3, Ring_ZF_1_L2
then have \( x\in \mathbb{R} \)
moreover
from A1, T have \( a + x = 0 \) using cplx_mul_add_vals, valid_cntxts, Ring_ZF_1_L3
ultimately show \( \exists x\in \mathbb{R} .\ a + x = 0 \)
qed

Each nonzero real number has a real inverse

lemma (in complex0) axrrecex:

assumes A1: \( a \in \mathbb{R} \), \( a \neq 0 \)

shows \( \exists x\in \mathbb{R} .\ a \cdot x = 1 \)proof
let \( R_0 = R-\{ 0 _R\} \)
let \( a_r = \text{fst}(a) \)
let \( y = \text{GroupInv}(R_0,\text{restrict}(M,R_0\times R_0))(a_r) \)
from A1 have T: \( \langle y, 0 _R\rangle \in \mathbb{R} \) using valid_cntxts, Field_ZF_1_L5
moreover
from A1, T have \( a \cdot \langle y, 0 _R\rangle = 1 \) using prod_of_reals, valid_cntxts, Field_ZF_1_L5, Field_ZF_1_L6
ultimately show \( \exists x \in \mathbb{R} .\ a \cdot x = 1 \)
qed

Our \( \mathbb{R} \) symbol is the real axis on the complex plane.

lemma (in complex0) real_means_real_axis:

shows \( \mathbb{R} = \text{ComplexReals}(R,A) \) using ComplexReals_def

The CplxROrder thing is a relation on the complex reals.

lemma (in complex0) cplx_ord_on_cplx_reals:

shows \( \text{CplxROrder}(R,A,r) \subseteq \mathbb{R} \times \mathbb{R} \) using ComplexReals_def, slice_proj_bij, real_means_real_axis, CplxROrder_def, InducedRelation_def

The strict version of the complex relation is a relation on complex reals.

lemma (in complex0) cplx_strict_ord_on_cplx_reals:

shows \( \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \subseteq \mathbb{R} \times \mathbb{R} \) using cplx_ord_on_cplx_reals, strict_ver_rel

The CplxROrder thing is a relation on the complex reals. Here this is formulated as a statement that in complex0 context \(a

lemma (in complex0) strict_cplx_ord_type:

assumes \( a \lt _{\mathbb{R}} b \)

shows \( a\in \mathbb{R} \), \( b\in \mathbb{R} \) using assms, CplxROrder_def, def_of_strict_ver, InducedRelation_def, slice_proj_bij, ComplexReals_def, real_means_real_axis

A more readable version of the definition of the strict order relation on the real axis. Recall that in the complex0 context \(r\) denotes the (non-strict) order relation on the underlying model of real numbers.

lemma (in complex0) def_of_real_axis_order:

shows \( \langle x, 0 _R\rangle \lt _{\mathbb{R}} \langle y, 0 _R\rangle \longleftrightarrow \langle x,y\rangle \in r \wedge x\neq y \)proof
let \( f = \text{SliceProjection}( \text{ComplexReals}(R,A)) \)
assume A1: \( \langle x, 0 _R\rangle \lt _{\mathbb{R}} \langle y, 0 _R\rangle \)
then have \( \langle f\langle x, 0 _R\rangle , f\langle y, 0 _R\rangle \rangle \in r \wedge x \neq y \) using CplxROrder_def, def_of_strict_ver, def_of_ind_relA
moreover
from A1 have \( \langle x, 0 _R\rangle \in \mathbb{R} \), \( \langle y, 0 _R\rangle \in \mathbb{R} \) using strict_cplx_ord_type
ultimately show \( \langle x,y\rangle \in r \wedge x\neq y \) using slice_proj_bij, ComplexReals_def
next
assume A1: \( \langle x,y\rangle \in r \wedge x\neq y \)
let \( f = \text{SliceProjection}( \text{ComplexReals}(R,A)) \)
have \( f : \mathbb{R} \rightarrow R \) using ComplexReals_def, slice_proj_bij, real_means_real_axis
moreover
from A1 have T: \( \langle x, 0 _R\rangle \in \mathbb{R} \), \( \langle y, 0 _R\rangle \in \mathbb{R} \) using valid_cntxts, OrdRing_ZF_1_L3
moreover
from A1, T have \( \langle f\langle x, 0 _R\rangle , f\langle y, 0 _R\rangle \rangle \in r \) using slice_proj_bij, ComplexReals_def
ultimately have \( \langle \langle x, 0 _R\rangle , \langle y, 0 _R\rangle \rangle \in \text{InducedRelation}(f,r) \) using def_of_ind_relB
with A1 show \( \langle x, 0 _R\rangle \lt _{\mathbb{R}} \langle y, 0 _R\rangle \) using CplxROrder_def, def_of_strict_ver
qed

The (non strict) order on complex reals is antisymmetric, transitive and total.

lemma (in complex0) cplx_ord_antsym_trans_tot:

shows \( \text{antisym}( \text{CplxROrder}(R,A,r)) \), \( \text{trans}( \text{CplxROrder}(R,A,r)) \), \( \text{CplxROrder}(R,A,r) \text{ is total on } \mathbb{R} \)proof
let \( f = \text{SliceProjection}( \text{ComplexReals}(R,A)) \)
have \( f \in ord\_iso(\mathbb{R} , \text{CplxROrder}(R,A,r),R,r) \) using ComplexReals_def, slice_proj_bij, real_means_real_axis, bij_is_ord_iso, CplxROrder_def
moreover
have \( \text{CplxROrder}(R,A,r) \subseteq \mathbb{R} \times \mathbb{R} \) using cplx_ord_on_cplx_reals
moreover
have I: \( \text{antisym}(r) \), \( r \text{ is total on } R \), \( \text{trans}(r) \) using valid_cntxts, OrdRing_ZF_1_L1, IsAnOrdRing_def, IsLinOrder_def
ultimately show \( \text{antisym}( \text{CplxROrder}(R,A,r)) \), \( \text{trans}( \text{CplxROrder}(R,A,r)) \), \( \text{CplxROrder}(R,A,r) \text{ is total on } \mathbb{R} \) using ord_iso_pres_antsym, ord_iso_pres_tot, ord_iso_pres_trans
qed

The trichotomy law for the strict order on the complex reals.

lemma (in complex0) cplx_strict_ord_trich:

assumes \( a \in \mathbb{R} \), \( b \in \mathbb{R} \)

shows \( \text{Exactly_1_of_3_holds} (a \lt _{\mathbb{R}} b, a=b, b \lt _{\mathbb{R}} a) \) using assms, cplx_ord_antsym_trans_tot, strict_ans_tot_trich

The strict order on the complex reals is kind of antisymetric.

lemma (in complex0) pre_axlttri:

assumes A1: \( a \in \mathbb{R} \), \( b \in \mathbb{R} \)

shows \( a \lt _{\mathbb{R}} b \longleftrightarrow \neg (a=b \vee b \lt _{\mathbb{R}} a) \)proof
from A1 have \( \text{Exactly_1_of_3_holds} (a \lt _{\mathbb{R}} b, a=b, b \lt _{\mathbb{R}} a) \) by (rule cplx_strict_ord_trich )
then show \( a \lt _{\mathbb{R}} b \longleftrightarrow \neg (a=b \vee b \lt _{\mathbb{R}} a) \) by (rule Fol1_L8A )
qed

The strict order on complex reals is transitive.

lemma (in complex0) cplx_strict_ord_trans:

shows \( \text{trans}( \text{StrictVersion}( \text{CplxROrder}(R,A,r))) \) using cplx_ord_antsym_trans_tot, strict_of_transB

The strict order on complex reals is transitive - the explicit version of cplx_strict_ord_trans.

lemma (in complex0) pre_axlttrn:

assumes A1: \( a \lt _{\mathbb{R}} b \), \( b \lt _{\mathbb{R}} c \)

shows \( a \lt _{\mathbb{R}} c \)proof
let \( s = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)
from A1 have \( \text{trans}(s) \), \( \langle a,b\rangle \in s \wedge \langle b,c\rangle \in s \) using cplx_strict_ord_trans
then have \( \langle a,c\rangle \in s \) by (rule Fol1_L3 )
then show \( a \lt _{\mathbb{R}} c \)
qed

The strict order on complex reals is preserved by translations.

lemma (in complex0) pre_axltadd:

assumes A1: \( a \lt _{\mathbb{R}} b \) and A2: \( c \in \mathbb{R} \)

shows \( c + a \lt _{\mathbb{R}} c + b \)proof
from A1 have T: \( a\in \mathbb{R} \), \( b\in \mathbb{R} \) using strict_cplx_ord_type
with A1, A2 show \( c + a \lt _{\mathbb{R}} c + b \) using def_of_real_axis_order, valid_cntxts, group_strict_ord_transl_inv, sum_of_reals
qed

The set of positive complex reals is closed with respect to multiplication.

lemma (in complex0) pre_axmulgt0:

assumes A1: \( 0 \lt _{\mathbb{R}} a \), \( 0 \lt _{\mathbb{R}} b \)

shows \( 0 \lt _{\mathbb{R}} a\cdot b \)proof
from A1 have T: \( a\in \mathbb{R} \), \( b\in \mathbb{R} \) using strict_cplx_ord_type
with A1 show \( 0 \lt _{\mathbb{R}} a\cdot b \) using def_of_real_axis_order, valid_cntxts, pos_mul_closed, def_of_real_axis_order, prod_of_reals
qed

The order on complex reals is linear and complete.

lemma (in complex0) cmplx_reals_ord_lin_compl:

shows \( \text{CplxROrder}(R,A,r) \text{ is complete } \), \( \text{IsLinOrder}(\mathbb{R} , \text{CplxROrder}(R,A,r)) \)proof
have \( \text{SliceProjection}(\mathbb{R} ) \in \text{bij}(\mathbb{R} ,R) \) using slice_proj_bij, ComplexReals_def, real_means_real_axis
moreover
have \( r \subseteq R\times R \) using valid_cntxts, OrdRing_ZF_1_L1, IsAnOrdRing_def
moreover
from R_are_reals have \( r \text{ is complete } \) and \( \text{IsLinOrder}(R,r) \) using IsAmodelOfReals_def, valid_cntxts, OrdRing_ZF_1_L1, IsAnOrdRing_def
ultimately show \( \text{CplxROrder}(R,A,r) \text{ is complete } \), \( \text{IsLinOrder}(\mathbb{R} , \text{CplxROrder}(R,A,r)) \) using CplxROrder_def, real_means_real_axis, ind_rel_pres_compl, ind_rel_pres_lin
qed

The property of the strict order on complex reals that corresponds to completeness.

lemma (in complex0) pre_axsup:

assumes A1: \( X \subseteq \mathbb{R} \), \( X \neq 0 \) and A2: \( \exists x\in \mathbb{R} .\ \forall y\in X.\ y \lt _{\mathbb{R}} x \)

shows \( \exists x\in \mathbb{R} .\ (\forall y\in X.\ \neg (x \lt _{\mathbb{R}} y)) \wedge (\forall y\in \mathbb{R} .\ (y \lt _{\mathbb{R}} x \longrightarrow (\exists z\in X.\ y \lt _{\mathbb{R}} z))) \)proof
let \( s = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)
have \( \text{CplxROrder}(R,A,r) \subseteq \mathbb{R} \times \mathbb{R} \), \( \text{IsLinOrder}(\mathbb{R} , \text{CplxROrder}(R,A,r)) \), \( \text{CplxROrder}(R,A,r) \text{ is complete } \) using cplx_ord_on_cplx_reals, cmplx_reals_ord_lin_compl
moreover
note A1
moreover
have \( s = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)
moreover
from A2 have \( \exists u\in \mathbb{R} .\ \forall y\in X.\ \langle y,u\rangle \in s \)
ultimately have \( \exists x\in \mathbb{R} .\ ( \forall y\in X.\ \langle x,y\rangle \notin s ) \wedge \) \( (\forall y\in \mathbb{R} .\ \langle y,x\rangle \in s \longrightarrow (\exists z\in X.\ \langle y,z\rangle \in s)) \) by (rule strict_of_compl )
then show \( (\exists x\in \mathbb{R} .\ (\forall y\in X.\ \neg (x \lt _{\mathbb{R}} y)) \wedge \) \( (\forall y\in \mathbb{R} .\ (y \lt _{\mathbb{R}} x \longrightarrow (\exists z\in X.\ y \lt _{\mathbb{R}} z)))) \)
qed
end
Definition of IsAmodelOfReals: \( \text{IsAmodelOfReals}(K,A,M,r) \equiv \text{IsAnOrdField}(K,A,M,r) \wedge (r \text{ is complete }) \)
lemma OrdField_ZF_1_L2:

assumes \( \text{IsAnOrdField}(K,A,M,r) \)

shows \( field1(K,A,M,r) \)
lemma (in field1) OrdField_ZF_1_L1B: shows \( field0(R,A,M) \)
lemma (in ring1) OrdRing_ZF_1_L4: shows \( \text{IsAnOrdGroup}(R,A,r) \), \( r \text{ is total on } R \), \( A \text{ is commutative on } R \), \( group3(R,A,r) \)
lemma (in field0) Field_ZF_1_L1: shows \( \text{IsAfield}(K,A,M) \)
Definition of IsAfield: \( \text{IsAfield}(K,A,M) \equiv \) \( ( \text{IsAring}(K,A,M) \wedge (M \text{ is commutative on } K) \wedge \) \( \text{ TheNeutralElement}(K,A) \neq \text{ TheNeutralElement}(K,M) \wedge \) \( (\forall a\in K.\ a\neq \text{ TheNeutralElement}(K,A)\longrightarrow \) \( (\exists b\in K.\ M\langle a,b\rangle = \text{ TheNeutralElement}(K,M)))) \)
lemma (in ring0) Ring_ZF_1_L1: shows \( monoid0(R,M) \), \( group0(R,A) \), \( A \text{ is commutative on } R \)
Definition of ReCxAdd: \( \text{ReCxAdd}(R,A,a,b) \equiv A\langle \text{fst}(a),\text{fst}(b)\rangle \)
Definition of ImCxAdd: \( \text{ImCxAdd}(R,A,a,b) \equiv A\langle \text{snd}(a),\text{snd}(b)\rangle \)
Definition of ImCxMul: \( \text{ImCxMul}(R,A,M,a,b) \equiv A\langle M\langle \text{fst}(a),\text{snd}(b)\rangle , M\langle \text{snd}(a),\text{fst}(b)\rangle \rangle \)
Definition of ReCxMul: \( \text{ReCxMul}(R,A,M,a,b) \equiv \) \( A\langle M\langle \text{fst}(a),\text{fst}(b)\rangle , \text{GroupInv}(R,A)(M\langle \text{snd}(a),\text{snd}(b)\rangle )\rangle \)
lemma (in complex0) valid_cntxts: shows \( field1(R,A,M,r) \), \( field0(R,A,M) \), \( ring1(R,A,M,r) \), \( group3(R,A,r) \), \( ring0(R,A,M) \), \( M \text{ is commutative on } R \), \( group0(R,A) \)
lemma (in ring0) Ring_ZF_1_L4:

assumes \( a\in R \), \( b\in R \)

shows \( a + b \in R \), \( a - b \in R \), \( a\cdot b \in R \), \( a + b = b + a \)
lemma (in complex0) cplx_mul_add_defs: shows \( \text{ReCxAdd}(R,A,\langle a,b\rangle ,\langle c,d\rangle ) = a + c \), \( \text{ImCxAdd}(R,A,\langle a,b\rangle ,\langle c,d\rangle ) = b + d \), \( \text{ImCxMul}(R,A,M,\langle a,b\rangle ,\langle c,d\rangle ) = a\cdot d + b\cdot c \), \( \text{ReCxMul}(R,A,M,\langle a,b\rangle ,\langle c,d\rangle ) = a\cdot c + ( - b\cdot d) \)
lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in complex0) cplx_mul_add_types:

assumes \( z_1 \in \mathbb{C} \), \( z_2 \in \mathbb{C} \)

shows \( \text{ReCxAdd}(R,A,z_1,z_2) \in R \), \( \text{ImCxAdd}(R,A,z_1,z_2) \in R \), \( \text{ImCxMul}(R,A,M,z_1,z_2) \in R \), \( \text{ReCxMul}(R,A,M,z_1,z_2) \in R \)
lemma ZF_fun_from_total:

assumes \( \forall x\in X.\ b(x) \in Y \)

shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)
Definition of CplxAdd: \( \text{CplxAdd}(R,A) \equiv \) \( \{\langle p, \langle \text{ReCxAdd}(R,A,\text{fst}(p),\text{snd}(p)), \text{ImCxAdd}(R,A,\text{fst}(p),\text{snd}(p)) \rangle \rangle .\ \) \( p\in (R\times R)\times (R\times R)\} \)
Definition of CplxMul: \( \text{CplxMul}(R,A,M) \equiv \) \( \{ \langle p, \langle \text{ReCxMul}(R,A,M,\text{fst}(p),\text{snd}(p)), \text{ImCxMul}(R,A,M,\text{fst}(p),\text{snd}(p))\rangle \rangle .\ \) \( p \in (R\times R)\times (R\times R)\} \)
lemma (in complex0) axaddopr: shows \( \text{CplxAdd}(R,A): \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \)
lemma ZF_fun_from_tot_val:

assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \) and \( b(x)\in Y \)
lemma (in complex0) axmulopr: shows \( \text{CplxMul}(R,A,M): \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \)
lemma (in complex0) cplx_mul_add_vals:

assumes \( a\in R \), \( b\in R \), \( c\in R \), \( d\in R \)

shows \( \langle a,b\rangle + \langle c,d\rangle = \langle a + c, b + d\rangle \), \( \langle a,b\rangle \cdot \langle c,d\rangle = \langle a\cdot c + ( - b\cdot d), a\cdot d + b\cdot c\rangle \)
lemma (in field0) field_mult_comm:

assumes \( a\in K \), \( b\in K \)

shows \( a\cdot b = b\cdot a \)
lemma (in ring0) Ring_ZF_2_L6:

assumes \( a\in R \), \( b\in R \), \( c\in R \), \( d\in R \), \( e\in R \), \( f\in R \)

shows \( a\cdot (c\cdot e - d\cdot f) - b\cdot (c\cdot f + d\cdot e) =\) \( (a\cdot c - b\cdot d)\cdot e - (a\cdot d + b\cdot c)\cdot f \), \( a\cdot (c\cdot f + d\cdot e) + b\cdot (c\cdot e - d\cdot f) =\) \( (a\cdot c - b\cdot d)\cdot f + (a\cdot d + b\cdot c)\cdot e \), \( a\cdot (c + e) - b\cdot (d + f) = a\cdot c - b\cdot d + (a\cdot e - b\cdot f) \), \( a\cdot (d + f) + b\cdot (c + e) = a\cdot d + b\cdot c + (a\cdot f + b\cdot e) \)
lemma (in ring0) Ring_ZF_1_L11:

assumes \( a\in R \), \( b\in R \), \( c\in R \)

shows \( a + b + c = a + (b + c) \), \( a\cdot b\cdot c = a\cdot (b\cdot c) \)
lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \)
lemma (in ring0) Ring_ZF_1_L3:

assumes \( a\in R \)

shows \( ( - a) \in R \), \( ( - ( - a)) = a \), \( a + 0 = a \), \( 0 + a = a \), \( a\cdot 1 = a \), \( 1 \cdot a = a \), \( a - a = 0 \), \( a - 0 = a \), \( 2 \cdot a = a + a \), \( ( - a) + a = 0 \)
lemma (in ring0) Ring_ZF_1_L6:

assumes \( x\in R \)

shows \( 0 \cdot x = 0 \), \( x\cdot 0 = 0 \)
lemma (in group0) group0_2_L6:

assumes \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)
lemma (in field1) OrdField_ZF_1_L10:

assumes \( a\in R \), \( b\in R \) and \( a \neq 0 \vee b \neq 0 \)

shows \( 0 \lt a^2 + b^2 \) and \( \exists c\in R.\ (a^2 + b^2)\cdot c = 1 \)
lemma (in ring0) ring_rearr_3_elemA:

assumes \( M \text{ is commutative on } R \) and \( a\in R \), \( b\in R \), \( c\in R \)

shows \( a\cdot (a\cdot c) - b\cdot ( - b\cdot c) = (a\cdot a + b\cdot b)\cdot c \), \( a\cdot ( - b\cdot c) + b\cdot (a\cdot c) = 0 \)
lemma (in complex0) sum_of_reals:

assumes \( a\in \mathbb{R} \), \( b\in \mathbb{R} \)

shows \( a + b = \langle \text{fst}(a) + \text{fst}(b), 0 _R\rangle \)
lemma (in complex0) prod_of_reals:

assumes \( a\in \mathbb{R} \), \( b\in \mathbb{R} \)

shows \( a \cdot b = \langle \text{fst}(a)\cdot \text{fst}(b), 0 _R\rangle \)
lemma (in field0) Field_ZF_1_L5:

assumes \( a\in K \), \( a\neq 0 \)

shows \( a^{-1} \in K_0 \), \( (a^{-1})^2 \in K_0 \), \( a^{-1} \in K \), \( a^{-1} \neq 0 \)
lemma (in field0) Field_ZF_1_L6:

assumes \( a\in K \), \( a\neq 0 \)

shows \( a\cdot a^{-1} = 1 \), \( a^{-1}\cdot a = 1 \)
Definition of ComplexReals: \( \text{ComplexReals}(R,A) \equiv R\times \{\text{ TheNeutralElement}(R,A)\} \)
lemma slice_proj_bij: shows \( \text{SliceProjection}(X\times \{y\}): X\times \{y\} \rightarrow X \), \( domain( \text{SliceProjection}(X\times \{y\})) = X\times \{y\} \), \( \forall p\in X\times \{y\}.\ \text{SliceProjection}(X\times \{y\})(p) = \text{fst}(p) \), \( \text{SliceProjection}(X\times \{y\}) \in \text{bij}(X\times \{y\},X) \)
lemma (in complex0) real_means_real_axis: shows \( \mathbb{R} = \text{ComplexReals}(R,A) \)
Definition of CplxROrder: \( \text{CplxROrder}(R,A,r) \equiv \) \( \text{InducedRelation}( \text{SliceProjection}( \text{ComplexReals}(R,A)),r) \)
Definition of InducedRelation: \( \text{InducedRelation}(f,R) \equiv \) \( \{p \in domain(f)\times domain(f).\ \langle f(\text{fst}(p)),f(\text{snd}(p))\rangle \in R\} \)
lemma (in complex0) cplx_ord_on_cplx_reals: shows \( \text{CplxROrder}(R,A,r) \subseteq \mathbb{R} \times \mathbb{R} \)
lemma strict_ver_rel:

assumes \( r \subseteq A\times A \)

shows \( \text{StrictVersion}(r) \subseteq A\times A \)
lemma def_of_strict_ver: shows \( \langle x,y\rangle \in \text{StrictVersion}(r) \longleftrightarrow \langle x,y\rangle \in r \wedge x\neq y \)
lemma def_of_ind_relA:

assumes \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \)

shows \( \langle f(x),f(y)\rangle \in R \)
lemma (in complex0) strict_cplx_ord_type:

assumes \( a \lt _{\mathbb{R}} b \)

shows \( a\in \mathbb{R} \), \( b\in \mathbb{R} \)
lemma (in ring1) OrdRing_ZF_1_L3:

assumes \( a\leq b \)

shows \( a\in R \), \( b\in R \)
lemma def_of_ind_relB:

assumes \( f:A\rightarrow B \) and \( x\in A \), \( y\in A \) and \( \langle f(x),f(y)\rangle \in R \)

shows \( \langle x,y\rangle \in \text{InducedRelation}(f,R) \)
lemma bij_is_ord_iso:

assumes \( f \in \text{bij}(A,B) \)

shows \( f \in ord\_iso(A, \text{InducedRelation}(f,R),B,R) \)
lemma (in ring1) OrdRing_ZF_1_L1: shows \( \text{IsAnOrdRing}(R,A,M,r) \)
Definition of IsAnOrdRing: \( \text{IsAnOrdRing}(R,A,M,r) \equiv \) \( ( \text{IsAring}(R,A,M) \wedge (M \text{ is commutative on } R) \wedge \) \( r\subseteq R\times R \wedge \text{IsLinOrder}(R,r) \wedge \) \( (\forall a b.\ \forall c\in R.\ \langle a,b\rangle \in r \longrightarrow \langle A\langle a,c\rangle ,A\langle b,c\rangle \rangle \in r) \wedge \) \( ( \text{Nonnegative}(R,A,r) \text{ is closed under } M)) \)
Definition of IsLinOrder: \( \text{IsLinOrder}(X,r) \equiv \text{antisym}(r) \wedge \text{trans}(r) \wedge (r \text{ is total on } X) \)
lemma ord_iso_pres_antsym:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{antisym}(R) \)

shows \( \text{antisym}(r) \)
lemma ord_iso_pres_tot:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( R \text{ is total on } B \)

shows \( r \text{ is total on } A \)
lemma ord_iso_pres_trans:

assumes \( f \in ord\_iso(A,r,B,R) \) and \( r \subseteq A\times A \) and \( \text{trans}(R) \)

shows \( \text{trans}(r) \)
lemma (in complex0) cplx_ord_antsym_trans_tot: shows \( \text{antisym}( \text{CplxROrder}(R,A,r)) \), \( \text{trans}( \text{CplxROrder}(R,A,r)) \), \( \text{CplxROrder}(R,A,r) \text{ is total on } \mathbb{R} \)
lemma strict_ans_tot_trich:

assumes \( \text{antisym}(r) \) and \( r \text{ is total on } X \) and \( a\in X \), \( b\in X \) and \( s = \text{StrictVersion}(r) \)

shows \( \text{Exactly_1_of_3_holds} (\langle a,b\rangle \in s, a=b,\langle b,a\rangle \in s) \)
lemma (in complex0) cplx_strict_ord_trich:

assumes \( a \in \mathbb{R} \), \( b \in \mathbb{R} \)

shows \( \text{Exactly_1_of_3_holds} (a \lt _{\mathbb{R}} b, a=b, b \lt _{\mathbb{R}} a) \)
lemma Fol1_L8A:

assumes \( \text{Exactly_1_of_3_holds} (p,q,r) \)

shows \( p \longleftrightarrow \neg (q \vee r) \)
lemma strict_of_transB:

assumes \( \text{trans}(r) \) and \( \text{antisym}(r) \)

shows \( \text{trans}( \text{StrictVersion}(r)) \)
lemma (in complex0) cplx_strict_ord_trans: shows \( \text{trans}( \text{StrictVersion}( \text{CplxROrder}(R,A,r))) \)
lemma Fol1_L3:

assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \)

shows \( \langle a,c\rangle \in r \)
lemma (in complex0) def_of_real_axis_order: shows \( \langle x, 0 _R\rangle \lt _{\mathbb{R}} \langle y, 0 _R\rangle \longleftrightarrow \langle x,y\rangle \in r \wedge x\neq y \)
lemma (in group3) group_strict_ord_transl_inv:

assumes \( a \lt b \) and \( c\in G \)

shows \( a\cdot c \lt b\cdot c \) and \( c\cdot a \lt c\cdot b \)
lemma (in field1) pos_mul_closed:

assumes \( 0 \lt a \), \( 0 \lt b \)

shows \( 0 \lt a\cdot b \)
lemma ind_rel_pres_compl:

assumes \( f \in \text{bij}(A,B) \) and \( R \subseteq B\times B \) and \( R \text{ is complete } \)

shows \( \text{InducedRelation}(f,R) \text{ is complete } \)
lemma ind_rel_pres_lin:

assumes \( f \in \text{bij}(A,B) \) and \( \text{IsLinOrder}(B,R) \)

shows \( \text{IsLinOrder}(A, \text{InducedRelation}(f,R)) \)
lemma (in complex0) cmplx_reals_ord_lin_compl: shows \( \text{CplxROrder}(R,A,r) \text{ is complete } \), \( \text{IsLinOrder}(\mathbb{R} , \text{CplxROrder}(R,A,r)) \)
lemma strict_of_compl:

assumes \( r \subseteq X\times X \) and \( \text{IsLinOrder}(X,r) \) and \( r \text{ is complete } \) and \( A\subseteq X \), \( A\neq 0 \) and \( s = \text{StrictVersion}(r) \) and \( \exists u\in X.\ \forall y\in A.\ \langle y,u\rangle \in s \)

shows \( \exists x\in X.\ ( \forall y\in A.\ \langle x,y\rangle \notin s ) \wedge (\forall y\in X.\ \langle y,x\rangle \in s \longrightarrow (\exists z\in A.\ \langle y,z\rangle \in s)) \)