Theory Metamath_sampler

theory Metamath_sampler
imports Metamath_interface MMI_Complex_ZF_2
(* 
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 "\<real> ∩ {\<cpnf>,\<cmnf>} = 0"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 "\<real> ∩ {\<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 \<real>*"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 \<real>*" 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 ∈ \<real>*"
shows "x ∈ \<real> <-> ( \<cmnf> \<ls> x ∧ x \<ls> \<cpnf> )"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 ∈ \<real> ∪ {\<complex>, {\<complex>}} -->
x ∈ \<real> <-> ⟨{\<complex>}, x⟩ ∈ ?lessrrel ∩ \<real> × \<real> ∪ {⟨{\<complex>}, \<complex>⟩} ∪
\<real> × {\<complex>} ∪ {{\<complex>}} × \<real> ∧
⟨x, \<complex>⟩ ∈ ?lessrrel ∩ \<real> × \<real> ∪ {⟨{\<complex>}, \<complex>⟩} ∪
\<real> × {\<complex>} ∪ {{\<complex>}} × \<real>"

by (rule MMIsar0.MMI_xrrebndt);
then have "x ∈ \<real>* --> ( x ∈ \<real> <-> ( \<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 ∈ \<real>" "b ∈ \<real>" "c ∈ \<real>" "d ∈ \<real>" and
A2: "\<zero> \<ls> b" "\<zero> \<ls> d"
shows "a·b \<ls> c·d <-> a\<cdiv>d \<ls> c\<cdiv>b"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 <->
⟨\<Union>{x ∈ ?complex . ?cmulset ` ⟨d, x⟩ = a},
\<Union>{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 ∈ \<real>"
shows "\<zero> \<ls> a <-> a\<cdiv>\<two> \<ls> a"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 <->
⟨\<Union>{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 ∈ \<real>" "b ∈ \<real>" and
A2: "\<zero> \<lsq> a" "\<zero> \<lsq> b"
shows "(a\<cdiv>(b \<ca> \<one>))·b \<lsq> a"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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`⟨\<Union>{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 ∈ \<nat>" "k ∈ \<nat>"
shows
"n\<lsq>k <-> n \<ls> k\<ca>\<one>"
"n \<ls> k <-> n \<ca> \<one> \<lsq> k"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 ∈ \<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧
(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)} ∧
k ∈ \<Inter>{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 ∈ \<nat> ∧ k ∈ \<nat> --> n \<lsq> k <-> n \<ls> k \<ca> \<one>"
by simp;
with A1 show "n\<lsq>k <-> n \<ls> k\<ca>\<one>" by simp;
from I have
"n ∈ \<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧
(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)} ∧
k ∈ \<Inter>{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 ∈ \<nat> ∧ k ∈ \<nat> --> n \<ls> k <-> n \<ca> \<one> \<lsq> k"
by simp;
with A1 show "n \<ls> k <-> n \<ca> \<one> \<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: "ψ(\<one>)" and
A2: "∀k ∈ \<nat>. ψ(k) --> ψ(k\<ca>\<one>)" and
A3: "n ∈ \<nat>"
shows "ψ(n)"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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∈\<Inter>{N ∈ Pow(?real) . ?one ∈ N ∧
(∀n. n ∈ N --> ?caddset ` ⟨n, ?one⟩ ∈ N)}.
ψ(k) --> ψ(?caddset ` ⟨k, ?one⟩)"

"n ∈ \<Inter>{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
"\<two> \<ca> \<two> = \<four>"
"\<two>·\<two> = \<four>"
"\<three>·\<two> = \<six>"
"\<three>·\<three> = \<nine>"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 "\<two> \<ca> \<two> = \<four>" 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 "\<two>·\<two> = \<four>" 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 "\<three>·\<two> = \<six>" 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 "\<three>·\<three> = \<nine>" 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 ⊆ \<real>" and
A2: "∃x∈S. ∀y∈S. x \<lsq> y"
shows "Infim(S,\<real>,\<cltrrset>) ∈ S"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 ⊆\<real> ∧ ( ∃x∈S. ∀y∈S. x \<lsq> y) -->
Sup(S,\<real>,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 ⊆ \<real> " and "A ≠ 0" and "∃x∈\<real>. ∀y∈A. y \<lsq> x"
shows "Sup(A,\<real>,\<cltrrset>) ∈ \<real>"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 ⊆\<real>" and "A ≠ 0" and "∃x∈\<real>. ∀y∈A. y \<lsq> x"
and "B ∈ \<real>" and "B \<ls> Sup(A,\<real>,\<cltrrset>)"
shows "∃z∈A. B \<ls> z"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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 ⊆ \<real>" and "A ≠ 0" and "∃x∈\<real>. ∀y∈A. x \<lsq> y"
shows
"Infim(A,\<real>,\<cltrrset>) ∈ \<real>"
"Infim(A,\<real>,\<cltrrset>) = ( \<cn>Sup({z ∈ \<real>. (\<cn>z) ∈ A },\<real>,\<cltrrset>) )"
proof -
let ?real = "\<real>"
let ?complex = "\<complex>"
let ?one = "\<one>"
let ?zero = "\<zero>"
let ?iunit = "\<i>"
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)) =
\<Union>{x ∈ ?complex . ?caddset`
⟨Sup({z ∈ ?real . \<Union>{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 ⊆\<real> ∧ ¬(A = 0) ∧ ( ∃x∈\<real>. ∀y∈A. x \<lsq> y) -->
Sup(A,\<real>,converse(\<cltrrset>)) = ( \<cn>Sup({z ∈ \<real>. (\<cn>z) ∈ A },\<real>,\<cltrrset>) )"

by simp;
with assms show
"Infim(A,\<real>,\<cltrrset>) = ( \<cn>Sup({z ∈ \<real>. (\<cn>z) ∈ A },\<real>,\<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,\<real>,\<cltrrset>) ∈ \<real>"
using Infim_def by simp;
qed;

end