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
qed
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) \)
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_L2Complex \(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
qed
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
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_commA 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_funtypeA 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_funtypeMultiplication 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
qed
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 \)
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_L4Complex 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
qed
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) \)
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
qed
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) \)
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_L2The 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_L3The imaginary unit is a complex number.
lemma (in complex0) axicn:
shows \( \imath \in \mathbb{C} \) using valid_cntxts, Ring_ZF_1_L2All 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
qed
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 \)
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
qed
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 \)
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_L6A 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_L3The 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_L4The 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_L4The 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
qed
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 \)
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
qed
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 \)
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_defThe 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_defThe 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_relThe 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_axisA 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
qed
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
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
qed
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
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_trichThe 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_transBThe 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
qed
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
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
qed
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)))) \)
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)) \)
This page by Slawomir Kolodynski is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8