Theory Metamath_Sampler

(* 
This file is a part of IsarMathLib - 
a library of formalized mathematics for Isabelle/Isar.

Copyright (C) 2006-2009  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 ‹Metamath sampler›

theory Metamath_Sampler imports Metamath_Interface MMI_Complex_ZF_2

begin

text‹The theorems translated from Metamath reside in the ‹MMI_Complex_ZF›,
  ‹MMI_Complex_ZF_1› and ‹MMI_Complex_ZF_2› theories. 
  The proofs of these theorems are very verbose and for this
  reason the theories are not shown in the proof document or the FormaMath.org 
  site. This theory file contains some examples of theorems 
  translated from Metamath and formulated in the ‹complex0› context.
  This serves two purposes: to give an overview of the material covered in
  the translated theorems and to provide examples of how to take a translated
  theorem (proven in the ‹MMIsar0› context) and transfer it to the 
  ‹complex0› context. The typical procedure for moving a theorem from
  ‹MMIsar0› to ‹complex0› is as follows:
  First we define certain aliases that map names defined in the ‹complex0›
  to their corresponding names in the ‹MMIsar0› context. This makes it 
  easy to copy and paste the statement of the theorem as 
  displayed with ProofGeneral. Then we run the Isabelle 
  from ProofGeneral up to the theorem we want to move. When the theorem is verified
  ProofGeneral displays the statement in the raw set theory notation, stripped 
  from any notation defined in the ‹MMIsar0› locale. This is what we copy
  to the proof in the ‹complex0› locale. After that we just can write 
  "then have ?thesis by simp" and the simplifier translates the raw set 
  theory notation to the one used in ‹complex0›.
›

subsection‹Extended reals and order›

text‹In this section we import a couple of theorems about the extended 
  real line and the linear order on it.›

text‹Metamath uses the set of real numbers extended with $+\infty$ and $-\infty$. 
  The $+\infty$ and $-\infty$ symbols are defined quite arbitrarily as $\mathbb{C}$
  and $\mathbb{\{ C\} }$, respectively. The next lemma that corresponds to 
  Metamath's ‹renfdisj› states that $+\infty$ and $-\infty$ are not 
  elements of $\mathbb{R}$.›

lemma (in complex0) renfdisj: shows "ℝ ∩ {\<cpnf>,\<cmnf>} = 0"
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have "?real ∩ {?complex, {?complex}} = 0"
    by (rule MMIsar0.MMI_renfdisj)
  thus "ℝ ∩ {\<cpnf>,\<cmnf>} = 0" by simp
qed
  
text‹The order relation used most often in Metamath is defined on 
  the set of complex reals extended with   $+\infty$ and $-\infty$. 
  The next lemma
  allows to use Metamath's ‹xrltso› that states that the ‹\<ls>›
  relations is a strict linear order on the extended set.›

lemma (in complex0) xrltso: shows "\<cltrrset> Orders ℝ⇧*"
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have 
    "(?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
      {{?complex}} × ?real) Orders (?real ∪ {?complex, {?complex}})"
    by (rule MMIsar0.MMI_xrltso)
  moreover have "?lessrrel ∩ ?real × ?real = ?lessrrel"
    using cplx_strict_ord_on_cplx_reals by auto
  ultimately show "\<cltrrset> Orders ℝ⇧*" by simp
qed

text‹Metamath defines the usual $<$ and $\leq$ ordering relations for the
  extended real line, including $+\infty$ and $-\infty$.›

lemma (in complex0) xrrebndt: assumes A1: "x ∈ ℝ⇧*"
  shows "x ∈ ℝ ⟷ ( \<cmnf> \<ls> x ∧ x \<ls> \<cpnf> )"
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have "x ∈ ℝ ∪ {ℂ, {ℂ}} ⟶
    x ∈ ℝ ⟷ ⟨{ℂ}, x⟩ ∈ ?lessrrel ∩ ℝ × ℝ ∪ {⟨{ℂ}, ℂ⟩} ∪ 
    ℝ × {ℂ} ∪ {{ℂ}} × ℝ ∧
    ⟨x, ℂ⟩ ∈ ?lessrrel ∩ ℝ × ℝ ∪ {⟨{ℂ}, ℂ⟩} ∪ 
    ℝ × {ℂ} ∪ {{ℂ}} × ℝ"
    by (rule MMIsar0.MMI_xrrebndt)
  then have "x ∈ ℝ⇧* ⟶ ( x ∈ ℝ ⟷ ( \<cmnf> \<ls> x ∧ x \<ls> \<cpnf> ) )"
    by simp
  with A1 show ?thesis by simp
qed

text‹A quite involved inequality.›

lemma (in complex0) lt2mul2divt: 
  assumes A1: "a ∈ ℝ"  "b ∈ ℝ"  "c ∈ ℝ"  "d ∈ ℝ" and
  A2: "𝟬 \<ls> b"  "𝟬 \<ls> d"
  shows "a⋅b \<ls> c⋅d ⟷ a\<cdiv>d \<ls> c\<cdiv>b"
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have
    "(a ∈ ?real ∧ b ∈ ?real) ∧
    (c ∈ ?real ∧ d ∈ ?real) ∧
    ⟨?zero, b⟩ ∈ ?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪ {{?complex}} × ?real ∧
    ⟨?zero, d⟩ ∈ ?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪ {{?complex}} × ?real ⟶
    ⟨?cmulset ` ⟨a, b⟩, ?cmulset ` ⟨c, d⟩⟩ ∈
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real ⟷
    ⟨⋃{x ∈ ?complex . ?cmulset ` ⟨d, x⟩ = a}, 
    ⋃{x ∈ ?complex . ?cmulset ` ⟨b, x⟩ = c}⟩ ∈
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real" 
    by (rule MMIsar0.MMI_lt2mul2divt)
  with A1 A2 show ?thesis by simp
qed

text‹A real number is smaller than its half iff it is positive.›

lemma (in complex0) halfpos: assumes A1: "a ∈ ℝ"
  shows "𝟬 \<ls> a ⟷ a\<cdiv>𝟮 \<ls> a"
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  from A1 have "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    and "a ∈ ?real"
    using MMIsar_valid by auto
  then have
    "⟨?zero, a⟩ ∈
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real ⟷
    ⟨⋃{x ∈ ?complex . ?cmulset ` ⟨?caddset ` ⟨?one, ?one⟩, x⟩ = a}, a⟩ ∈
    ?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪ {{?complex}} × ?real"
    by (rule MMIsar0.MMI_halfpos)
  then show ?thesis by simp
qed

text‹One more inequality.›

lemma (in complex0) ledivp1t: 
  assumes A1:  "a ∈ ℝ"   "b ∈ ℝ" and
  A2: "𝟬 \<lsq> a"  "𝟬 \<lsq> b"
  shows "(a\<cdiv>(b \<ca> 𝟭))⋅b \<lsq> a"
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have
    "(a ∈ ?real ∧ ⟨a, ?zero⟩ ∉
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real) ∧ 
    b ∈ ?real ∧ ⟨b, ?zero⟩ ∉ ?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
    {{?complex}} × ?real ⟶
    ⟨a,?cmulset`⟨⋃{x ∈ ?complex . ?cmulset`⟨?caddset`⟨b, ?one⟩, x⟩ = a}, b⟩⟩ ∉
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real"
    by (rule MMIsar0.MMI_ledivp1t)
  with A1 A2 show ?thesis by simp
qed

subsection‹Natural real numbers›

text‹In standard mathematics natural numbers are treated as a subset of 
  real numbers.
  From the set theory point of view however those are quite different objects.
  In this section we talk about "real natural" numbers i.e. the conterpart of
  natural numbers that is a subset of the reals.›

text‹Two ways of saying that there are no natural numbers between $n$ and $n+1$.›

lemma (in complex0) no_nats_between: 
  assumes A1: "n ∈ ℕ"  "k ∈ ℕ"
  shows 
  "n\<lsq>k ⟷ n \<ls> k\<ca>𝟭"
  "n \<ls> k ⟷ n \<ca> 𝟭 \<lsq> k" 
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have I: "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have 
    "n ∈ ⋂{N ∈ Pow(?real) . ?one ∈ N ∧ 
    (∀n. n ∈ N ⟶ ?caddset ` ⟨n, ?one⟩ ∈ N)} ∧
    k ∈ ⋂{N ∈ Pow(?real) . ?one ∈ N ∧ 
    (∀n. n ∈ N ⟶ ?caddset ` ⟨n, ?one⟩ ∈ N)} ⟶
    ⟨k, n⟩ ∉
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
    {{?complex}} × ?real ⟷
    ⟨n, ?caddset ` ⟨k, ?one⟩⟩ ∈
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
    {{?complex}} × ?real" by (rule MMIsar0.MMI_nnleltp1t)
  then have "n ∈ ℕ ∧ k ∈ ℕ ⟶ n \<lsq> k ⟷ n \<ls> k \<ca> 𝟭"
    by simp
  with A1 show "n\<lsq>k ⟷ n \<ls> k\<ca>𝟭" by simp
  from I have
    "n ∈ ⋂{N ∈ Pow(?real) . ?one ∈ N ∧ 
    (∀n. n ∈ N ⟶ ?caddset ` ⟨n, ?one⟩ ∈ N)} ∧
    k ∈ ⋂{N ∈ Pow(?real) . ?one ∈ N ∧ 
    (∀n. n ∈ N ⟶ ?caddset ` ⟨n, ?one⟩ ∈ N)} ⟶
    ⟨n, k⟩ ∈
    ?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
    {{?complex}} × ?real ⟷  ⟨k, ?caddset ` ⟨n, ?one⟩⟩ ∉
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
    {{?complex}} × ?real" by (rule MMIsar0.MMI_nnltp1let)
  then have "n ∈ ℕ ∧ k ∈ ℕ ⟶  n \<ls> k ⟷ n \<ca> 𝟭 \<lsq> k"
    by simp
  with A1 show "n \<ls> k ⟷ n \<ca> 𝟭 \<lsq> k" by simp
qed

text‹Metamath has some very complicated and general version of induction
  on (complex) natural numbers that I can't even understand. As an exercise
  I derived a more standard version that is imported to the ‹complex0› 
  context below.›

lemma (in complex0) cplx_nat_ind: assumes A1: "ψ(𝟭)" and 
  A2: "∀k ∈ ℕ. ψ(k) ⟶ ψ(k\<ca>𝟭)" and
  A3: "n ∈ ℕ"
  shows "ψ(n)"
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have I: "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  moreover from A1 A2 A3 have
    "ψ(?one)"
    "∀k∈⋂{N ∈ Pow(?real) . ?one ∈ N ∧ 
    (∀n. n ∈ N ⟶ ?caddset ` ⟨n, ?one⟩ ∈ N)}.
    ψ(k) ⟶ ψ(?caddset ` ⟨k, ?one⟩)"
    "n ∈ ⋂{N ∈ Pow(?real) . ?one ∈ N ∧ 
    (∀n. n ∈ N ⟶ ?caddset ` ⟨n, ?one⟩ ∈ N)}"
    by auto
  ultimately show "ψ(n)" by (rule MMIsar0.nnind1)
qed

text‹Some simple arithmetics.›

lemma (in complex0) arith: shows
  "𝟮 \<ca> 𝟮 = 𝟰"
  "𝟮⋅𝟮 = 𝟰"
  "𝟯⋅𝟮 = 𝟲"
  "𝟯⋅𝟯 = 𝟵"
proof -
  let ?real = "ℝ"
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have I: "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have
    "?caddset ` ⟨?caddset ` ⟨?one, ?one⟩, ?caddset ` ⟨?one, ?one⟩⟩ =
    ?caddset ` ⟨?caddset ` ⟨?caddset ` ⟨?one, ?one⟩, ?one⟩, ?one⟩"
    by (rule MMIsar0.MMI_2p2e4)
  thus "𝟮 \<ca> 𝟮 = 𝟰" by simp
  from I have
    "?cmulset`⟨?caddset`⟨?one, ?one⟩, ?caddset`⟨?one, ?one⟩⟩ =
    ?caddset`⟨?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩, ?one⟩"
    by (rule MMIsar0.MMI_2t2e4)
  thus "𝟮⋅𝟮 = 𝟰" by simp
  from I have
    "?cmulset`⟨?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩, ?caddset`⟨?one, ?one⟩⟩ =
    ?caddset `⟨?caddset`⟨?caddset`⟨?caddset`⟨?caddset`
    ⟨?one, ?one⟩, ?one⟩, ?one⟩, ?one⟩, ?one⟩"
    by (rule MMIsar0.MMI_3t2e6)
  thus "𝟯⋅𝟮 = 𝟲" by simp
  from I have "?cmulset `
    ⟨?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩,
    ?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩⟩ =
    ?caddset`⟨?caddset`⟨?caddset `⟨?caddset `
    ⟨?caddset`⟨?caddset`⟨?caddset`⟨?caddset`⟨?one, ?one⟩, ?one⟩, ?one⟩, ?one⟩,
    ?one⟩, ?one⟩, ?one⟩, ?one⟩"
    by (rule MMIsar0.MMI_3t3e9)
  thus "𝟯⋅𝟯 = 𝟵" by simp
qed

subsection‹Infimum and supremum in real numbers›

text‹Real numbers form a complete ordered field. Here we import a couple
  of Metamath theorems about supremu and infimum.›

text‹If a set $S$ has a smallest element, then the infimum of $S$ belongs
  to it.›

lemma (in complex0) lbinfmcl: assumes A1: "S ⊆ ℝ" and 
  A2: "∃x∈S. ∀y∈S. x \<lsq> y"
  shows  "Infim(S,ℝ,\<cltrrset>) ∈ S"
proof -
  let ?real = "ℝ" 
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have I: "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have
    "S ⊆ ?real ∧ (∃x∈S. ∀y∈S. ⟨y, x⟩ ∉
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪
    ?real × {?complex} ∪ {{?complex}} × ?real) ⟶
    Sup(S, ?real,  
    converse(?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
    {{?complex}} × ?real)) ∈ S"
    by (rule MMIsar0.MMI_lbinfmcl)
  then have 
    "S ⊆ℝ ∧ ( ∃x∈S. ∀y∈S. x \<lsq> y) ⟶  
    Sup(S,ℝ,converse(\<cltrrset>)) ∈ S" by simp
  with A1 A2 show ?thesis using Infim_def by simp
qed

text‹Supremum of any subset of reals that is bounded above is real.›

lemma (in complex0) sup_is_real: 
  assumes "A ⊆ ℝ " and "A ≠ 0" and "∃x∈ℝ. ∀y∈A. y \<lsq> x"
  shows "Sup(A,ℝ,\<cltrrset>) ∈ ℝ"  
proof -
  let ?real = "ℝ" 
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have 
    "A ⊆ ?real ∧ A ≠ 0 ∧ (∃x∈?real.  ∀y∈A. ⟨x, y⟩ ∉
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real) ⟶ 
    Sup(A, ?real,
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real) ∈ ?real" 
    by (rule MMIsar0.MMI_suprcl)
  with assms show ?thesis by simp
qed

text‹If a real number is smaller that the supremum of $A$, then 
  we can find an element of $A$ greater than it.›

lemma (in complex0) suprlub: 
  assumes "A ⊆ℝ" and "A ≠ 0" and "∃x∈ℝ. ∀y∈A. y \<lsq> x" 
  and "B ∈ ℝ"  and "B \<ls> Sup(A,ℝ,\<cltrrset>)"
  shows "∃z∈A. B \<ls> z"
proof -
  let ?real = "ℝ" 
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have "(A ⊆ ?real ∧ A ≠ 0 ∧ (∃x∈?real. ∀y∈A. ⟨x, y⟩ ∉
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ 
    {{?complex}} × ?real)) ∧ B ∈ ?real ∧ ⟨B, Sup(A, ?real,
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪
    {{?complex}} × ?real)⟩ ∈ ?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
    {{?complex}} × ?real ⟶
    (∃z∈A. ⟨B, z⟩ ∈ ?lessrrel ∩ ?real × ?real ∪ 
    {⟨{?complex}, ?complex⟩} ∪ ?real × {?complex} ∪
    {{?complex}} × ?real)"
    by (rule MMIsar0.MMI_suprlub)
  with assms show ?thesis by simp
qed

text‹Something a bit more interesting: infimum of a set that is bounded
  below is real and equal to the
  minus supremum of the set flipped around zero.›

lemma (in complex0) infmsup: 
  assumes "A ⊆ ℝ" and "A ≠ 0" and "∃x∈ℝ. ∀y∈A. x \<lsq> y"
  shows
  "Infim(A,ℝ,\<cltrrset>) ∈ ℝ"
  "Infim(A,ℝ,\<cltrrset>) = ( \<cn>Sup({z ∈ ℝ. (\<cn>z) ∈ A },ℝ,\<cltrrset>) )"
proof -
  let ?real = "ℝ" 
  let ?complex = "ℂ"
  let ?one = "𝟭"
  let ?zero = "𝟬"
  let ?iunit = "𝗂"
  let ?caddset = "CplxAdd(R,A)"
  let ?cmulset = "CplxMul(R,A,M)"
  let ?lessrrel = "StrictVersion(CplxROrder(R,A,r))"
  have I: "MMIsar0
    (?real, ?complex, ?one, ?zero, ?iunit, ?caddset, ?cmulset, ?lessrrel)"
    using MMIsar_valid by simp
  then have
    "A ⊆ ?real ∧ A ≠ 0 ∧ (∃x∈?real. ∀y∈A. ⟨y, x⟩ ∉ 
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪
    {{?complex}} × ?real) ⟶ Sup(A, ?real, converse
    (?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪
    {{?complex}} × ?real)) =
    ⋃{x ∈ ?complex . ?caddset`
    ⟨Sup({z ∈ ?real . ⋃{x ∈ ?complex . ?caddset`⟨z, x⟩ = ?zero} ∈ A}, ?real,
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real), x⟩ = ?zero}"
    by (rule MMIsar0.MMI_infmsup)
  then have "A ⊆ℝ ∧ ¬(A = 0) ∧ ( ∃x∈ℝ. ∀y∈A. x \<lsq> y) ⟶ 
    Sup(A,ℝ,converse(\<cltrrset>)) = ( \<cn>Sup({z ∈ ℝ. (\<cn>z) ∈ A },ℝ,\<cltrrset>) )"
    by simp
  with assms show
    "Infim(A,ℝ,\<cltrrset>) = ( \<cn>Sup({z ∈ ℝ. (\<cn>z) ∈ A },ℝ,\<cltrrset>) )"
    using Infim_def by simp
  from I have
    "A ⊆ ?real ∧ A ≠ 0 ∧ (∃x∈?real. ∀y∈A. ⟨y, x⟩ ∉ 
    ?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪
    {{?complex}} × ?real) ⟶ Sup(A, ?real, converse
    (?lessrrel ∩ ?real × ?real ∪ {⟨{?complex}, ?complex⟩} ∪ 
    ?real × {?complex} ∪ {{?complex}} × ?real)) ∈ ?real"
    by (rule MMIsar0.MMI_infmrcl)
  with assms show "Infim(A,ℝ,\<cltrrset>) ∈ ℝ"
    using Infim_def by simp
qed

end