Theory Complex_ZF

theory Complex_ZF
imports func_ZF_1 OrderedField_ZF
(*   This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2006  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED 
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF 
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. 
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, 
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; 
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, 
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR 
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, 
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)


section ‹Complex numbers›


theory Complex_ZF imports func_ZF_1 OrderedField_ZF

begin

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

subsection‹From complete ordered fields to complex numbers›

text‹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\}$ ‹ComplexReals(R,A)›
  and the strict order relation ‹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 ‹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
  ‹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 ‹\<lsr>› 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.
›

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

definition
  "ReCxAdd(R,A,a,b) ≡ A`⟨fst(a),fst(b)⟩"

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

definition
  "ImCxAdd(R,A,a,b) ≡ A`⟨snd(a),snd(b)⟩"

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

definition
  "CplxAdd(R,A) ≡ 
  {⟨p, ⟨ ReCxAdd(R,A,fst(p),snd(p)),ImCxAdd(R,A,fst(p),snd(p)) ⟩ ⟩. 
  p∈(R×R)×(R×R)}" 

text‹The expression representing the imaginary part of the
  product of complex numbers.›

definition
  "ImCxMul(R,A,M,a,b) ≡ A`⟨M`⟨fst(a),snd(b)⟩, M`⟨snd(a),fst(b)⟩ ⟩"

text‹The expression representing the real part of the
  product of complex numbers.›

definition
  "ReCxMul(R,A,M,a,b) ≡ 
  A`⟨M`⟨fst(a),fst(b)⟩,GroupInv(R,A)`(M`⟨snd(a),snd(b)⟩)⟩"

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

definition
  "CplxMul(R,A,M) ≡ 
  { ⟨p, ⟨ReCxMul(R,A,M,fst(p),snd(p)),ImCxMul(R,A,M,fst(p),snd(p))⟩ ⟩. 
  p ∈ (R×R)×(R×R)}"

text‹The definition real numbers embedded in the complex plane.›

definition
  "ComplexReals(R,A) ≡ R×{TheNeutralElement(R,A)}"

text‹Definition of order relation on the real line.›

definition
  "CplxROrder(R,A,r) ≡ 
  InducedRelation(SliceProjection(ComplexReals(R,A)),r)"

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

locale complex0 =
  fixes R and A and M and r
  assumes R_are_reals: "IsAmodelOfReals(R,A,M,r)"

  fixes complex ("ℂ")
  defines complex_def[simp]: "ℂ ≡ R×R"

  fixes rone ("𝟭R")
  defines rone_def[simp]: "𝟭R ≡ TheNeutralElement(R,M)"

  fixes rzero ("𝟬R")
  defines rzero_def[simp]: "𝟬R ≡ TheNeutralElement(R,A)"

  fixes one ("𝟭")
  defines one_def[simp]: "𝟭 ≡ ⟨𝟭R, 𝟬R⟩"

  fixes zero ("𝟬")
  defines zero_def[simp]: "𝟬 ≡ ⟨𝟬R, 𝟬R⟩"

  fixes iunit ("𝗂")
  defines iunit_def[simp]: "𝗂 ≡ ⟨𝟬R,𝟭R⟩"

  fixes creal ("ℝ")
  defines creal_def[simp]: "ℝ ≡ {⟨r,𝟬R⟩. r∈R}"

  fixes rmul (infixl "\<rmu>" 71)
  defines rmul_def[simp]: "a \<rmu> b ≡ M`⟨a,b⟩"

  fixes radd (infixl "\<ra>" 69)
  defines radd_def[simp]: "a \<ra> b ≡ A`⟨a,b⟩"

  fixes rneg ("\<rm> _" 70)
  defines rneg_def[simp]: "\<rm> a ≡  GroupInv(R,A)`(a)"

  fixes ca (infixl "\<ca>" 69)
  defines ca_def[simp]: "a \<ca> b ≡ CplxAdd(R,A)`⟨a,b⟩"

  fixes cm (infixl "⋅" 71)
  defines cm_def[simp]: "a ⋅ b ≡ CplxMul(R,A,M)`⟨a,b⟩"

  fixes cdiv (infixl "\<cdiv>" 70)
  defines cdiv_def[simp]: "a \<cdiv> b ≡ ⋃ { x ∈ ℂ. b ⋅ x = a }"

  fixes sub (infixl "\<cs>" 69)
  defines sub_def[simp]: "a \<cs> b ≡ ⋃ { x ∈ ℂ. b \<ca> x = a }"

  fixes cneg ("\<cn>_" 95)
  defines cneg_def[simp]: "\<cn> a ≡ 𝟬 \<cs> a"
  
  fixes lessr (infix "\<lsr>" 68)
  defines lessr_def[simp]: 
  "a \<lsr> b ≡ ⟨a,b⟩ ∈ StrictVersion(CplxROrder(R,A,r))"

  fixes cpnf ("\<cpnf>")
  defines cpnf_def[simp]: "\<cpnf> ≡ ℂ"

  fixes cmnf ("\<cmnf>")
  defines cmnf_def[simp]: "\<cmnf> ≡ {ℂ}"

  fixes cxr ("ℝ*")
  defines cxr_def[simp]: "ℝ* ≡ ℝ ∪ {\<cpnf>,\<cmnf>}"

  fixes cxn ("ℕ")
  defines cxn_def[simp]: 
  "ℕ ≡ ⋂ {N ∈ Pow(ℝ). 𝟭 ∈ N ∧ (∀n. n∈N ⟶ n\<ca>𝟭 ∈ N)}"

  fixes cltrrset ("\<cltrrset>")
  defines cltrrset_def[simp]: 
  "\<cltrrset> ≡  StrictVersion(CplxROrder(R,A,r)) ∩ ℝ×ℝ ∪
  {⟨\<cmnf>,\<cpnf>⟩} ∪ (ℝ×{\<cpnf>}) ∪ ({\<cmnf>}×ℝ )"

  fixes cltrr (infix "\<ls>" 68)
  defines cltrr_def[simp]: "a \<ls> b ≡ ⟨a,b⟩ ∈ \<cltrrset>"

  fixes lsq (infix "\<lsq>" 68)
  defines lsq_def[simp]: "a \<lsq> b ≡ ¬ (b \<ls> a)"

  fixes two ("𝟮")
  defines two_def[simp]: "𝟮 ≡ 𝟭 \<ca> 𝟭"

  fixes three ("𝟯")
  defines three_def[simp]: "𝟯 ≡ 𝟮\<ca>𝟭"

  fixes four ("𝟰")
  defines four_def[simp]: "𝟰 ≡ 𝟯\<ca>𝟭"

  fixes five ("𝟱")
  defines five_def[simp]: "𝟱 ≡ 𝟰\<ca>𝟭"

  fixes six ("𝟲")
  defines six_def[simp]: "𝟲 ≡ 𝟱\<ca>𝟭"

  fixes seven ("𝟳")
  defines seven_def[simp]: "𝟳 ≡ 𝟲\<ca>𝟭"

  fixes eight ("𝟴")
  defines eight_def[simp]: "𝟴 ≡ 𝟳\<ca>𝟭"

  fixes nine ("𝟵")
  defines nine_def[simp]: "𝟵 ≡ 𝟴\<ca>𝟭"

subsection‹Axioms of complex numbers›

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

text‹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 {is commutative on} R"
  "group0(R,A)"
proof -
  from R_are_reals have I: "IsAnOrdField(R,A,M,r)"
    using IsAmodelOfReals_def by simp
  then show "field1(R,A,M,r)" using OrdField_ZF_1_L2 by simp
  then show "ring1(R,A,M,r)" and I: "field0(R,A,M)"
    using field1.axioms ring1_def field1.OrdField_ZF_1_L1B
    by auto
  then show "group3(R,A,r)" using ring1.OrdRing_ZF_1_L4
    by simp
  from I have "IsAfield(R,A,M)" using field0.Field_ZF_1_L1
    by simp
  then have "IsAring(R,A,M)" and "M {is commutative on} R"
    using IsAfield_def by auto
  then show "ring0(R,A,M)" and "M {is commutative on} R" 
    using ring0_def by auto
  then show "group0(R,A)" using ring0.Ring_ZF_1_L1
    by simp
qed

text‹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
  "ReCxAdd(R,A,⟨a,b⟩,⟨c,d⟩) = a \<ra> c"
  "ImCxAdd(R,A,⟨a,b⟩,⟨c,d⟩) = b \<ra> d"
  "ImCxMul(R,A,M,⟨a,b⟩,⟨c,d⟩) = a\<rmu>d \<ra> b\<rmu>c"
  "ReCxMul(R,A,M,⟨a,b⟩,⟨c,d⟩) =  a\<rmu>c \<ra> (\<rm>b\<rmu>d)"
proof -
  let ?z1 = "⟨a,b⟩"
  let ?z2 = "⟨c,d⟩"
  have "ReCxAdd(R,A,?z1,?z2) ≡  A`⟨fst(?z1),fst(?z2)⟩"
   by (rule ReCxAdd_def)
  moreover have "ImCxAdd(R,A,?z1,?z2) ≡  A`⟨snd(?z1),snd(?z2)⟩"
    by (rule ImCxAdd_def)
  moreover have 
    "ImCxMul(R,A,M,?z1,?z2) ≡ A`⟨M`<fst(?z1),snd(?z2)>,M`<snd(?z1),fst(?z2)>⟩"
    by (rule ImCxMul_def)
  moreover have
    "ReCxMul(R,A,M,?z1,?z2) ≡ 
    A`⟨M`<fst(?z1),fst(?z2)>,GroupInv(R,A)`(M`⟨snd(?z1),snd(?z2)⟩)⟩"
    by (rule ReCxMul_def)
  ultimately show 
    "ReCxAdd(R,A,?z1,?z2) =  a \<ra> c"
    "ImCxAdd(R,A,⟨a,b⟩,⟨c,d⟩) = b \<ra> d"
    "ImCxMul(R,A,M,⟨a,b⟩,⟨c,d⟩) = a\<rmu>d \<ra> b\<rmu>c"
    "ReCxMul(R,A,M,⟨a,b⟩,⟨c,d⟩) =  a\<rmu>c \<ra> (\<rm>b\<rmu>d)"
    by auto
qed

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

lemma (in complex0) cplx_mul_add_types: 
  assumes A1: "z1 ∈ ℂ"   "z2 ∈ ℂ"
  shows 
  "ReCxAdd(R,A,z1,z2) ∈ R"
  "ImCxAdd(R,A,z1,z2) ∈ R"
  "ImCxMul(R,A,M,z1,z2) ∈ R"
  "ReCxMul(R,A,M,z1,z2) ∈ R"
proof -
  let ?a = "fst(z1)"
  let ?b = "snd(z1)"
  let ?c = "fst(z2)"
  let ?d = "snd(z2)"
  from A1 have "?a ∈ R"  "?b ∈ R"  "?c ∈ R"  "?d ∈ R"
    by auto
  then have 
    "?a \<ra> ?c ∈ R"
    "?b \<ra> ?d ∈ R"
    "?a\<rmu>?d \<ra> ?b\<rmu>?c ∈ R"
    "?a\<rmu>?c \<ra> (\<rm> ?b\<rmu>?d) ∈ R"
    using valid_cntxts ring0.Ring_ZF_1_L4 by auto
  with A1 show 
    "ReCxAdd(R,A,z1,z2) ∈ R"
    "ImCxAdd(R,A,z1,z2) ∈ R"
    "ImCxMul(R,A,M,z1,z2) ∈ R"
    "ReCxMul(R,A,M,z1,z2) ∈ R"
    using cplx_mul_add_defs by auto
qed

text‹Complex reals are complex. Recall the definition of ‹ℝ›
  in the ‹complex0› locale.›
  
lemma (in complex0) axresscn: shows "ℝ ⊆ ℂ"
  using valid_cntxts group0.group0_2_L2 by auto

text‹Complex $1$ is not complex $0$.›

lemma (in complex0) ax1ne0: shows "𝟭 ≠ 𝟬"
proof -
  have "IsAfield(R,A,M)" using valid_cntxts field0.Field_ZF_1_L1
    by simp
  then show "𝟭 ≠ 𝟬" using IsAfield_def by auto
qed

text‹Complex addition is a complex valued binary
  operation on complex numbers.›

lemma (in complex0) axaddopr: shows "CplxAdd(R,A): ℂ × ℂ → ℂ"
proof -
  have "∀p ∈ ℂ×ℂ. 
    ⟨ReCxAdd(R,A,fst(p),snd(p)),ImCxAdd(R,A,fst(p),snd(p))⟩ ∈ ℂ"
    using cplx_mul_add_types by simp
  then have 
    "{⟨p,⟨ReCxAdd(R,A,fst(p),snd(p)),ImCxAdd(R,A,fst(p),snd(p))⟩ ⟩. 
    p ∈ ℂ×ℂ}: ℂ×ℂ → ℂ"
    by (rule ZF_fun_from_total)
  then show "CplxAdd(R,A): ℂ × ℂ → ℂ" using CplxAdd_def by simp
qed

text‹Complex multiplication is a complex valued binary
  operation on complex numbers.›

lemma (in complex0) axmulopr: shows "CplxMul(R,A,M): ℂ × ℂ → ℂ"
proof -
  have "∀p ∈ ℂ×ℂ. 
    ⟨ReCxMul(R,A,M,fst(p),snd(p)),ImCxMul(R,A,M,fst(p),snd(p))⟩ ∈ ℂ"
    using cplx_mul_add_types by simp
  then have
   "{⟨p,⟨ReCxMul(R,A,M,fst(p),snd(p)),ImCxMul(R,A,M,fst(p),snd(p))⟩⟩. 
    p ∈ ℂ×ℂ}: ℂ×ℂ → ℂ" by (rule ZF_fun_from_total)
  then show "CplxMul(R,A,M): ℂ × ℂ → ℂ" using CplxMul_def by simp
qed

text‹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∈R"  "b∈R"  "c∈R"  "d∈R"
  shows 
  "⟨a,b⟩ \<ca> ⟨c,d⟩ = ⟨a \<ra> c, b \<ra> d⟩"
  "⟨a,b⟩ ⋅ ⟨c,d⟩ = ⟨a\<rmu>c \<ra> (\<rm>b\<rmu>d), a\<rmu>d \<ra> b\<rmu>c⟩"
proof -
  let ?S = "CplxAdd(R,A)" 
  let ?P = "CplxMul(R,A,M)"
  let ?p = "⟨ ⟨a,b⟩, ⟨c,d⟩ ⟩"
  from A1 have "?S : ℂ × ℂ → ℂ" and "?p ∈ ℂ × ℂ" 
    using axaddopr by auto
  moreover have
    "?S = {⟨p, <ReCxAdd(R,A,fst(p),snd(p)),ImCxAdd(R,A,fst(p),snd(p))>⟩. 
    p ∈ ℂ × ℂ}"
    using CplxAdd_def by simp
  ultimately have "?S`(?p) = ⟨ReCxAdd(R,A,fst(?p),snd(?p)),ImCxAdd(R,A,fst(?p),snd(?p))⟩"
    by (rule ZF_fun_from_tot_val)
  then show "⟨a,b⟩ \<ca> ⟨c,d⟩ = ⟨a \<ra> c, b \<ra> d⟩"
    using cplx_mul_add_defs by simp
  from A1 have "?P : ℂ × ℂ → ℂ" and "?p ∈ ℂ × ℂ" 
    using axmulopr by auto
  moreover have 
    "?P = {⟨p, ⟨ReCxMul(R,A,M,fst(p),snd(p)),ImCxMul(R,A,M,fst(p),snd(p))⟩ ⟩. 
    p ∈ ℂ × ℂ}"
    using CplxMul_def by simp
  ultimately have 
    "?P`(?p) = ⟨ReCxMul(R,A,M,fst(?p),snd(?p)),ImCxMul(R,A,M,fst(?p),snd(?p))⟩"
    by (rule ZF_fun_from_tot_val)
  then show "⟨a,b⟩ ⋅ ⟨c,d⟩ = ⟨a\<rmu>c \<ra> (\<rm>b\<rmu>d), a\<rmu>d \<ra> b\<rmu>c⟩"
    using cplx_mul_add_defs by simp
qed

text‹Complex multiplication is commutative.›

lemma (in complex0) axmulcom: assumes A1: "a ∈ ℂ"  "b ∈ ℂ"
  shows "a⋅b = b⋅a"
  using assms cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L4 
      field0.field_mult_comm by auto

text‹A sum of complex numbers is complex.›

lemma (in complex0) axaddcl: assumes "a ∈ ℂ"  "b ∈ ℂ"
  shows "a\<ca>b ∈ ℂ"
  using assms axaddopr apply_funtype by simp

text‹A product of complex numbers is complex.›

lemma (in complex0) axmulcl: assumes "a ∈ ℂ"  "b ∈ ℂ"
  shows  "a⋅b ∈ ℂ"
  using assms axmulopr apply_funtype by simp

text‹Multiplication is distributive with respect to
  addition.›

lemma (in complex0) axdistr: 
  assumes A1: "a ∈ ℂ"  "b ∈ ℂ"  "c ∈ ℂ"
  shows "a⋅(b \<ca> c) = a⋅b \<ca> a⋅c"
proof -
  let ?ar = "fst(a)"
  let ?ai = "snd(a)"
  let ?br = "fst(b)"
  let ?bi = "snd(b)"
  let ?cr = "fst(c)"
  let ?ci = "snd(c)"  
  from A1 have T: 
    "?ar ∈ R"  "?ai ∈ R"  "?br ∈ R"  "?bi ∈ R"  "?cr ∈ R"  "?ci ∈ R"
    "?br\<ra>?cr ∈ R"  "?bi\<ra>?ci ∈ R"
    "?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi) ∈ R"
    "?ar\<rmu>?cr \<ra> (\<rm>?ai\<rmu>?ci) ∈ R"
    "?ar\<rmu>?bi \<ra> ?ai\<rmu>?br ∈ R"
    "?ar\<rmu>?ci \<ra> ?ai\<rmu>?cr ∈ R"
    using valid_cntxts ring0.Ring_ZF_1_L4 by auto
  with A1 have "a⋅(b \<ca> c) = 
    ⟨?ar\<rmu>(?br\<ra>?cr) \<ra> (\<rm>?ai\<rmu>(?bi\<ra>?ci)),?ar\<rmu>(?bi\<ra>?ci) \<ra> ?ai\<rmu>(?br\<ra>?cr)⟩"
    using cplx_mul_add_vals by auto
  moreover from T have
    "?ar\<rmu>(?br\<ra>?cr) \<ra> (\<rm>?ai\<rmu>(?bi\<ra>?ci)) =
    ?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi) \<ra> (?ar\<rmu>?cr \<ra> (\<rm>?ai\<rmu>?ci))"
    and
    "?ar\<rmu>(?bi\<ra>?ci) \<ra> ?ai\<rmu>(?br\<ra>?cr) =
    ?ar\<rmu>?bi \<ra> ?ai\<rmu>?br \<ra> (?ar\<rmu>?ci \<ra> ?ai\<rmu>?cr)"
    using valid_cntxts ring0.Ring_ZF_2_L6 by auto
  moreover from A1 T have 
    "⟨?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi) \<ra> (?ar\<rmu>?cr \<ra> (\<rm>?ai\<rmu>?ci)),
    ?ar\<rmu>?bi \<ra> ?ai\<rmu>?br \<ra> (?ar\<rmu>?ci \<ra> ?ai\<rmu>?cr)⟩ =
    a⋅b \<ca> a⋅c"
    using cplx_mul_add_vals by auto
  ultimately show "a⋅(b \<ca> c) = a⋅b \<ca> a⋅c"
    by simp
qed

text‹Complex addition is commutative.›

lemma (in complex0) axaddcom: assumes "a ∈ ℂ"  "b ∈ ℂ"
  shows "a\<ca>b = b\<ca>a"
  using assms cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L4
  by auto

text‹Complex addition is associative.›

lemma (in complex0) axaddass: assumes A1: "a ∈ ℂ"  "b ∈ ℂ"  "c ∈ ℂ"
  shows "a \<ca> b \<ca> c = a \<ca> (b \<ca> c)"
proof -
  let ?ar = "fst(a)"
  let ?ai = "snd(a)"
  let ?br = "fst(b)"
  let ?bi = "snd(b)"
  let ?cr = "fst(c)"
  let ?ci = "snd(c)"  
  from A1 have T: 
    "?ar ∈ R"  "?ai ∈ R"  "?br ∈ R"  "?bi ∈ R"  "?cr ∈ R"  "?ci ∈ R"
    "?ar\<ra>?br ∈ R"  "?ai\<ra>?bi ∈ R"  
    "?br\<ra>?cr ∈ R"  "?bi\<ra>?ci ∈ R"
    using valid_cntxts ring0.Ring_ZF_1_L4 by auto
  with A1 have "a \<ca> b \<ca> c = ⟨?ar\<ra>?br\<ra>?cr,?ai\<ra>?bi\<ra>?ci⟩"
    using cplx_mul_add_vals by auto
  also from A1 T have "… = a \<ca> (b \<ca> c)"
    using valid_cntxts ring0.Ring_ZF_1_L11 cplx_mul_add_vals
    by auto
  finally show "a \<ca> b \<ca> c = a \<ca> (b \<ca> c)"
    by simp
qed

text‹Complex multiplication is associative.›

lemma (in complex0) axmulass: assumes A1: "a ∈ ℂ"  "b ∈ ℂ"  "c ∈ ℂ"
  shows "a ⋅ b ⋅ c = a ⋅ (b ⋅ c)"
proof -
  let ?ar = "fst(a)"
  let ?ai = "snd(a)"
  let ?br = "fst(b)"
  let ?bi = "snd(b)"
  let ?cr = "fst(c)"
  let ?ci = "snd(c)"
  from A1 have T:
    "?ar ∈ R"  "?ai ∈ R"  "?br ∈ R"  "?bi ∈ R"  "?cr ∈ R"  "?ci ∈ R"
    "?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi) ∈ R"  
    "?ar\<rmu>?bi \<ra> ?ai\<rmu>?br ∈ R"
    "?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci) ∈ R"
    "?br\<rmu>?ci \<ra> ?bi\<rmu>?cr ∈ R" 
    using valid_cntxts ring0.Ring_ZF_1_L4  by auto
  with A1 have "a ⋅ b ⋅ c = 
    ⟨(?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi))\<rmu>?cr \<ra> (\<rm>(?ar\<rmu>?bi \<ra> ?ai\<rmu>?br)\<rmu>?ci),
    (?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi))\<rmu>?ci \<ra> (?ar\<rmu>?bi \<ra> ?ai\<rmu>?br)\<rmu>?cr⟩"
    using cplx_mul_add_vals by auto
  moreover from A1 T have 
    "⟨?ar\<rmu>(?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci)) \<ra> (\<rm>?ai\<rmu>(?br\<rmu>?ci \<ra> ?bi\<rmu>?cr)),
    ?ar\<rmu>(?br\<rmu>?ci \<ra> ?bi\<rmu>?cr) \<ra> ?ai\<rmu>(?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci))⟩ = 
    a ⋅ (b ⋅ c)"
    using cplx_mul_add_vals by auto
  moreover from T have
    "?ar\<rmu>(?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci)) \<ra> (\<rm>?ai\<rmu>(?br\<rmu>?ci \<ra> ?bi\<rmu>?cr)) =
    (?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi))\<rmu>?cr \<ra> (\<rm>(?ar\<rmu>?bi \<ra> ?ai\<rmu>?br)\<rmu>?ci)"
    and
    "?ar\<rmu>(?br\<rmu>?ci \<ra> ?bi\<rmu>?cr) \<ra> ?ai\<rmu>(?br\<rmu>?cr \<ra> (\<rm>?bi\<rmu>?ci)) =
    (?ar\<rmu>?br \<ra> (\<rm>?ai\<rmu>?bi))\<rmu>?ci \<ra> (?ar\<rmu>?bi \<ra> ?ai\<rmu>?br)\<rmu>?cr"
    using valid_cntxts ring0.Ring_ZF_2_L6 by auto
  ultimately show "a ⋅ b ⋅ c = a ⋅ (b ⋅ c)"
    by auto
qed

text‹Complex $1$ is real. This really means that the pair 
  $\langle 1,0 \rangle$ is on the real axis.›

lemma (in complex0) ax1re: shows "𝟭 ∈ ℝ"
  using valid_cntxts ring0.Ring_ZF_1_L2 by simp

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

lemma (in complex0) axi2m1: shows "𝗂⋅𝗂 \<ca> 𝟭 = 𝟬"
  using valid_cntxts ring0.Ring_ZF_1_L2 ring0.Ring_ZF_1_L3
  cplx_mul_add_vals ring0.Ring_ZF_1_L6 group0.group0_2_L6 
  by simp

text‹$0$ is the neutral element of complex addition.›

lemma (in complex0) ax0id: assumes "a ∈ ℂ"
  shows "a \<ca> 𝟬 = a"
  using assms cplx_mul_add_vals valid_cntxts 
    ring0.Ring_ZF_1_L2 ring0.Ring_ZF_1_L3
  by auto

text‹The imaginary unit is a complex number.›

lemma (in complex0) axicn: shows "𝗂 ∈ ℂ"
  using valid_cntxts ring0.Ring_ZF_1_L2 by auto

text‹All complex numbers have additive inverses.›

lemma (in complex0) axnegex: assumes A1: "a ∈ ℂ"
  shows "∃x∈ℂ. a \<ca> x  = 𝟬"
proof -
  let ?ar = "fst(a)"
  let ?ai = "snd(a)"
  let ?x = "⟨\<rm>?ar, \<rm>?ai⟩"
  from A1 have T: 
    "?ar ∈ R"   "?ai ∈ R"   "(\<rm>?ar) ∈ R"   "(\<rm>?ar) ∈ R"
    using valid_cntxts ring0.Ring_ZF_1_L3 by auto
  then have "?x ∈ ℂ" using valid_cntxts ring0.Ring_ZF_1_L3
    by auto
  moreover from A1 T have "a \<ca> ?x = 𝟬"
    using cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L3
    by auto
  ultimately show "∃x∈ℂ. a \<ca> x  = 𝟬"
    by auto
qed

text‹A non-zero complex number has a multiplicative inverse.›

lemma (in complex0) axrecex: assumes A1: "a ∈ ℂ" and A2: "a≠𝟬"
  shows "∃x∈ℂ. a⋅x = 𝟭"
proof -
  let ?ar = "fst(a)"
  let ?ai = "snd(a)"
  let ?m = "?ar\<rmu>?ar \<ra> ?ai\<rmu>?ai"
  from A1 have T1: "?ar ∈ R"   "?ai ∈ R" by auto
  moreover from A1 A2 have "?ar ≠ 𝟬R ∨ ?ai ≠ 𝟬R" 
    by auto
  ultimately have "∃c∈R. ?m\<rmu>c = 𝟭R"
    using valid_cntxts field1.OrdField_ZF_1_L10
    by auto
  then obtain c where I: "c∈R" and II: "?m\<rmu>c = 𝟭R"
    by auto
  let ?x = "⟨?ar\<rmu>c, \<rm>?ai\<rmu>c⟩"
  from T1 I have T2: "?ar\<rmu>c ∈ R"  "(\<rm>?ai\<rmu>c) ∈ R"
    using valid_cntxts ring0.Ring_ZF_1_L4 ring0.Ring_ZF_1_L3
    by auto
  then have "?x ∈ ℂ" by auto
  moreover from A1 T1 T2 I II have "a⋅?x = 𝟭"
    using cplx_mul_add_vals valid_cntxts ring0.ring_rearr_3_elemA
    by auto
  ultimately show "∃x∈ℂ. a⋅x = 𝟭" by auto
qed

text‹Complex $1$ is a right neutral element for multiplication.›

lemma (in complex0) ax1id: assumes A1: "a ∈ ℂ"
  shows "a⋅𝟭 = a"
  using assms valid_cntxts ring0.Ring_ZF_1_L2 cplx_mul_add_vals
    ring0.Ring_ZF_1_L3 ring0.Ring_ZF_1_L6 by auto

text‹A formula for sum of (complex) real numbers.›

lemma (in complex0) sum_of_reals: assumes "a∈ℝ"  "b∈ℝ"
  shows 
  "a \<ca> b = ⟨fst(a) \<ra> fst(b),𝟬R⟩"
  using assms valid_cntxts ring0.Ring_ZF_1_L2 cplx_mul_add_vals
    ring0.Ring_ZF_1_L3 by auto
  
text‹The sum of real numbers is real.›

lemma (in complex0) axaddrcl: assumes A1: "a∈ℝ"  "b∈ℝ"
  shows "a \<ca> b ∈ ℝ" 
  using assms sum_of_reals valid_cntxts ring0.Ring_ZF_1_L4
  by auto

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

lemma (in complex0) prod_of_reals: assumes A1: "a∈ℝ"  "b∈ℝ"
  shows "a ⋅ b = ⟨fst(a)\<rmu>fst(b),𝟬R⟩"
proof -
  let ?ar = "fst(a)"
  let ?br = "fst(b)"
  from A1 have T: 
    "?ar ∈ R" "?br ∈ R"  "𝟬R ∈ R"  "?ar\<rmu>?br ∈ R"
    using valid_cntxts ring0.Ring_ZF_1_L2 ring0.Ring_ZF_1_L4 
    by auto
  with A1 show "a ⋅ b = ⟨?ar\<rmu>?br,𝟬R⟩"
    using cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L2 
      ring0.Ring_ZF_1_L6 ring0.Ring_ZF_1_L3 by auto
qed

text‹The product of (complex) real numbers is real.›

lemma (in complex0) axmulrcl: assumes "a∈ℝ"  "b∈ℝ"
  shows "a ⋅ b ∈ ℝ"
  using assms prod_of_reals valid_cntxts ring0.Ring_ZF_1_L4
  by auto

text‹The existence of a real negative of a real number.›

lemma (in complex0) axrnegex: assumes A1: "a∈ℝ"
  shows "∃ x ∈ ℝ. a \<ca> x = 𝟬"
proof -
  let ?ar = "fst(a)"
  let ?x = "⟨\<rm>?ar,𝟬R⟩"
  from A1 have T: 
    "?ar ∈ R"  "(\<rm>?ar) ∈ R"  "𝟬R ∈ R" 
    using valid_cntxts ring0.Ring_ZF_1_L3 ring0.Ring_ZF_1_L2 
    by auto
  then have "?x∈ ℝ" by auto
  moreover from A1 T have "a \<ca> ?x = 𝟬"
    using cplx_mul_add_vals valid_cntxts ring0.Ring_ZF_1_L3
    by auto
  ultimately show "∃x∈ℝ. a \<ca> x = 𝟬" by auto
qed

text‹Each nonzero real number has a real inverse›

lemma (in complex0) axrrecex: 
  assumes A1:  "a ∈ ℝ"   "a ≠ 𝟬"
  shows "∃x∈ℝ. a ⋅ x = 𝟭"
proof -
  let ?R0 = "R-{𝟬R}"
  let ?ar = "fst(a)"
  let ?y = "GroupInv(?R0,restrict(M,?R0×?R0))`(?ar)"
  from A1 have T: "⟨?y,𝟬R⟩ ∈ ℝ" using valid_cntxts field0.Field_ZF_1_L5
    by auto
  moreover from A1 T have "a ⋅ ⟨?y,𝟬R⟩ = 𝟭"
    using prod_of_reals valid_cntxts
    field0.Field_ZF_1_L5 field0.Field_ZF_1_L6 by auto
  ultimately show "∃ x ∈ ℝ. a ⋅ x = 𝟭" by auto
qed
  
text‹Our ‹ℝ› symbol is the real axis on the complex plane.›

lemma (in complex0) real_means_real_axis: shows "ℝ = ComplexReals(R,A)"
  using ComplexReals_def by auto

text‹The ‹CplxROrder› thing is a relation on the complex reals.
›

lemma (in complex0) cplx_ord_on_cplx_reals:
  shows "CplxROrder(R,A,r) ⊆ ℝ×ℝ"
  using ComplexReals_def slice_proj_bij real_means_real_axis
    CplxROrder_def InducedRelation_def by auto

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

lemma (in complex0) cplx_strict_ord_on_cplx_reals:
  shows "StrictVersion(CplxROrder(R,A,r)) ⊆ ℝ×ℝ"
  using cplx_ord_on_cplx_reals strict_ver_rel by simp

text‹The ‹CplxROrder› thing is a relation on the complex reals.
  Here this is formulated as a statement that in ‹complex0› context
  $a<b$ implies that $a,b$ are complex reals›

lemma (in complex0) strict_cplx_ord_type: assumes "a \<lsr> b"
  shows "a∈ℝ"  "b∈ℝ"
  using assms CplxROrder_def def_of_strict_ver InducedRelation_def 
    slice_proj_bij ComplexReals_def real_means_real_axis 
  by auto

text‹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 
  "⟨x,𝟬R⟩ \<lsr> ⟨y,𝟬R⟩ ⟷ ⟨x,y⟩ ∈ r ∧ x≠y"
proof
  let ?f = "SliceProjection(ComplexReals(R,A))"
  assume A1: "⟨x,𝟬R⟩ \<lsr> ⟨y,𝟬R⟩"
  then have "⟨ ?f`⟨x,𝟬R⟩, ?f`⟨y,𝟬R⟩ ⟩ ∈ r ∧ x ≠ y"
    using CplxROrder_def def_of_strict_ver def_of_ind_relA
    by simp
  moreover from A1 have "⟨x,𝟬R⟩ ∈ ℝ"  "⟨y,𝟬R⟩ ∈ ℝ"
    using strict_cplx_ord_type by auto
  ultimately show "⟨x,y⟩ ∈ r ∧ x≠y"
    using slice_proj_bij ComplexReals_def by simp
next assume A1: "⟨x,y⟩ ∈ r ∧ x≠y"
  let ?f = "SliceProjection(ComplexReals(R,A))"
  have "?f : ℝ → R"
    using ComplexReals_def slice_proj_bij real_means_real_axis
    by simp
  moreover from A1 have T: "⟨x,𝟬R⟩ ∈ ℝ"   "⟨y,𝟬R⟩ ∈ ℝ"
    using valid_cntxts ring1.OrdRing_ZF_1_L3 by auto
  moreover from A1 T have "⟨ ?f`⟨x,𝟬R⟩, ?f`⟨y,𝟬R⟩ ⟩ ∈ r"
    using slice_proj_bij ComplexReals_def by simp
  ultimately have "⟨ ⟨x,𝟬R⟩, ⟨y,𝟬R⟩ ⟩ ∈ InducedRelation(?f,r)"
    using def_of_ind_relB by simp
  with A1 show "⟨x,𝟬R⟩ \<lsr> ⟨y,𝟬R⟩"
    using CplxROrder_def def_of_strict_ver
    by simp
qed

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

lemma (in complex0) cplx_ord_antsym_trans_tot: shows
  "antisym(CplxROrder(R,A,r))"
  "trans(CplxROrder(R,A,r))"
  "CplxROrder(R,A,r) {is total on} ℝ"
proof -
  let ?f = "SliceProjection(ComplexReals(R,A))"
  have "?f ∈ ord_iso(ℝ,CplxROrder(R,A,r),R,r)"
    using ComplexReals_def slice_proj_bij real_means_real_axis 
      bij_is_ord_iso CplxROrder_def by simp
  moreover have "CplxROrder(R,A,r) ⊆ ℝ×ℝ"
    using cplx_ord_on_cplx_reals by simp
  moreover have I:
    "antisym(r)"   "r {is total on} R"   "trans(r)"
    using valid_cntxts ring1.OrdRing_ZF_1_L1 IsAnOrdRing_def 
      IsLinOrder_def by auto
  ultimately show 
    "antisym(CplxROrder(R,A,r))"
    "trans(CplxROrder(R,A,r))"
    "CplxROrder(R,A,r) {is total on} ℝ"
    using ord_iso_pres_antsym ord_iso_pres_tot ord_iso_pres_trans
    by auto
qed

text‹The trichotomy law for the strict order on the complex 
  reals.›

lemma (in complex0) cplx_strict_ord_trich: 
  assumes "a ∈ ℝ"  "b ∈ ℝ"
  shows "Exactly_1_of_3_holds(a\<lsr>b, a=b, b\<lsr>a)"
  using assms cplx_ord_antsym_trans_tot strict_ans_tot_trich
  by simp

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

lemma (in complex0) pre_axlttri: assumes A1: "a ∈ ℝ"   "b ∈ ℝ"
  shows "a \<lsr> b ⟷ ¬(a=b ∨ b \<lsr> a)"
proof -
  from A1 have "Exactly_1_of_3_holds(a\<lsr>b, a=b, b\<lsr>a)"
    by (rule cplx_strict_ord_trich)
  then show "a \<lsr> b ⟷ ¬(a=b ∨ b \<lsr> a)"
    by (rule Fol1_L8A)
qed

text‹The strict order on complex reals is transitive.›

lemma (in complex0) cplx_strict_ord_trans: 
  shows "trans(StrictVersion(CplxROrder(R,A,r)))"
  using cplx_ord_antsym_trans_tot strict_of_transB by simp
  

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

lemma (in complex0) pre_axlttrn: 
  assumes A1: "a \<lsr> b"   "b \<lsr> c"
  shows "a \<lsr> c"
proof -
  let ?s = "StrictVersion(CplxROrder(R,A,r))"
  from A1 have 
    "trans(?s)"   "⟨a,b⟩ ∈ ?s ∧ ⟨b,c⟩ ∈ ?s"
    using cplx_strict_ord_trans by auto
  then have "⟨a,c⟩ ∈ ?s" by (rule Fol1_L3)
  then show "a \<lsr> c" by simp
qed
  
text‹The strict order on complex reals is preserved by translations.›

lemma (in complex0) pre_axltadd: 
  assumes A1: "a \<lsr> b" and A2: "c ∈ ℝ"
  shows "c\<ca>a \<lsr> c\<ca>b"
proof -
  from A1 have T: "a∈ℝ"  "b∈ℝ" using strict_cplx_ord_type
    by auto
  with A1 A2 show "c\<ca>a \<lsr> c\<ca>b" 
    using def_of_real_axis_order valid_cntxts 
      group3.group_strict_ord_transl_inv sum_of_reals 
    by auto
qed

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

lemma (in complex0) pre_axmulgt0: assumes A1: "𝟬 \<lsr> a"   "𝟬 \<lsr> b"
  shows "𝟬 \<lsr> a⋅b"
proof -
  from A1 have T: "a∈ℝ"  "b∈ℝ" using strict_cplx_ord_type
    by auto
  with A1 show "𝟬 \<lsr> a⋅b"
    using def_of_real_axis_order valid_cntxts field1.pos_mul_closed
      def_of_real_axis_order prod_of_reals
    by auto
qed

text‹The order on complex reals is linear and complete.›

lemma (in complex0) cmplx_reals_ord_lin_compl: shows
  "CplxROrder(R,A,r) {is complete}"
  "IsLinOrder(ℝ,CplxROrder(R,A,r))"
proof -
  have "SliceProjection(ℝ) ∈ bij(ℝ,R)"
    using slice_proj_bij ComplexReals_def real_means_real_axis 
    by simp
  moreover have "r ⊆ R×R" using valid_cntxts ring1.OrdRing_ZF_1_L1
    IsAnOrdRing_def by simp
  moreover from R_are_reals have 
    "r {is complete}" and "IsLinOrder(R,r)"
    using IsAmodelOfReals_def valid_cntxts ring1.OrdRing_ZF_1_L1
    IsAnOrdRing_def by auto
  ultimately show 
    "CplxROrder(R,A,r) {is complete}"
    "IsLinOrder(ℝ,CplxROrder(R,A,r))"
    using CplxROrder_def real_means_real_axis ind_rel_pres_compl 
      ind_rel_pres_lin by auto
qed

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

lemma (in complex0) pre_axsup: assumes A1: "X ⊆ ℝ"   "X ≠ 0" and
  A2: "∃x∈ℝ. ∀y∈X. y \<lsr> x"
  shows 
  "∃x∈ℝ. (∀y∈X. ¬(x \<lsr> y)) ∧ (∀y∈ℝ. (y \<lsr> x ⟶ (∃z∈X. y \<lsr> z)))"
proof -
  let ?s = "StrictVersion(CplxROrder(R,A,r))"
  have 
    "CplxROrder(R,A,r) ⊆ ℝ×ℝ"
    "IsLinOrder(ℝ,CplxROrder(R,A,r))"
    "CplxROrder(R,A,r) {is complete}"
    using cplx_ord_on_cplx_reals cmplx_reals_ord_lin_compl
    by auto
  moreover note A1
  moreover have "?s = StrictVersion(CplxROrder(R,A,r))"
    by simp
  moreover from A2 have "∃u∈ℝ. ∀y∈X. ⟨y,u⟩ ∈ ?s"
    by simp
  ultimately have
    "∃x∈ℝ. ( ∀y∈X. ⟨x,y⟩ ∉ ?s ) ∧ 
    (∀y∈ℝ. ⟨y,x⟩ ∈ ?s ⟶ (∃z∈X. ⟨y,z⟩ ∈ ?s))"
    by (rule strict_of_compl)
  then show "(∃x∈ℝ. (∀y∈X. ¬(x \<lsr> y)) ∧ 
    (∀y∈ℝ. (y \<lsr> x ⟶ (∃z∈X. y \<lsr> z))))"
    by simp
qed
  
end