(* 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. *) header{*\isaheader{Metamath\_sampler.thy}*} theory Metamath_sampler imports Metamath_interface MMI_Complex_ZF_2 begin text{* The theorems translated from Metamath reside in the @{text "MMI_Complex_ZF"}, @{text "MMI_Complex_ZF_1"} and @{text "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 @{text "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 @{text "MMIsar0"} context) and transfer it to the @{text "complex0"} context. The typical procedure for moving a theorem from @{text "MMIsar0"} to @{text "complex0"} is as follows: First we define certain aliases that map names defined in the @{text "complex0"} to their corresponding names in the @{text "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 @{text "MMIsar0"} locale. This is what we copy to the proof in the @{text "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 @{text "complex0"}. *} section{*Extended reals and order*} text{*In this sectin 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 @{text "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 @{text "xrltso"} that states that the @{text "\<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 section{*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 @{text "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 section{*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