IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory Metamath_Sampler imports Metamath_Interface MMI_Complex_ZF_2

begin

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.

Extended reals and order

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

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 \( \mathbb{R} \cap \{+\infty ,-\infty \} = 0 \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( real \cap \{complex, \{complex\}\} = 0 \) by (rule MMIsar0.MMI_renfdisj )

thus \( \mathbb{R} \cap \{+\infty ,-\infty \} = 0 \)

qed

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 \( \lt \) relations is a strict linear order on the extended set.

lemma (in complex0) xrltso:

shows \( \lt \text{ orders } \mathbb{R} ^* \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( (lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real) \text{ orders } (real \cup \{complex, \{complex\}\}) \) by (rule MMIsar0.MMI_xrltso )

moreover

have \( lessrrel \cap real \times real = lessrrel \) using cplx_strict_ord_on_cplx_reals

ultimately show \( \lt \text{ orders } \mathbb{R} ^* \)

qed

Metamath defines the usual \(<\) and \(\leq\) ordering relations for the extended real line, including \(+\infty\) and \(-\infty\).

lemma (in complex0) xrrebndt:

assumes A1: \( x \in \mathbb{R} ^* \)

shows \( x \in \mathbb{R} \longleftrightarrow ( -\infty \lt x \wedge x \lt +\infty ) \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( x \in \mathbb{R} \cup \{\mathbb{C} , \{\mathbb{C} \}\} \longrightarrow \) \( x \in \mathbb{R} \longleftrightarrow \langle \{\mathbb{C} \}, x\rangle \in lessrrel \cap \mathbb{R} \times \mathbb{R} \cup \{\langle \{\mathbb{C} \}, \mathbb{C} \rangle \} \cup \) \( \mathbb{R} \times \{\mathbb{C} \} \cup \{\{\mathbb{C} \}\} \times \mathbb{R} \wedge \) \( \langle x, \mathbb{C} \rangle \in lessrrel \cap \mathbb{R} \times \mathbb{R} \cup \{\langle \{\mathbb{C} \}, \mathbb{C} \rangle \} \cup \) \( \mathbb{R} \times \{\mathbb{C} \} \cup \{\{\mathbb{C} \}\} \times \mathbb{R} \) by (rule MMIsar0.MMI_xrrebndt )

then have \( x \in \mathbb{R} ^* \longrightarrow ( x \in \mathbb{R} \longleftrightarrow ( -\infty \lt x \wedge x \lt +\infty ) ) \)

with A1 show \( thesis \)

qed

A quite involved inequality.

lemma (in complex0) lt2mul2divt:

assumes A1: \( a \in \mathbb{R} \), \( b \in \mathbb{R} \), \( c \in \mathbb{R} \), \( d \in \mathbb{R} \) and A2: \( 0 \lt b \), \( 0 \lt d \)

shows \( a\cdot b \lt c\cdot d \longleftrightarrow a / d \lt c / b \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( (a \in real \wedge b \in real) \wedge \) \( (c \in real \wedge d \in real) \wedge \) \( \langle zero, b\rangle \in lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \{\{complex\}\} \times real \wedge \) \( \langle zero, d\rangle \in lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \{\{complex\}\} \times real \longrightarrow \) \( \langle cmulset \langle a, b\rangle , cmulset \langle c, d\rangle \rangle \in \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real \longleftrightarrow \) \( \langle \bigcup \{x \in complex .\ cmulset \langle d, x\rangle = a\}, \) \( \bigcup \{x \in complex .\ cmulset \langle b, x\rangle = c\}\rangle \in \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real \) by (rule MMIsar0.MMI_lt2mul2divt )

with A1, A2 show \( thesis \)

qed

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

lemma (in complex0) halfpos:

assumes A1: \( a \in \mathbb{R} \)

shows \( 0 \lt a \longleftrightarrow a / 2 \lt a \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

from A1 have \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) and \( a \in real \) using MMIsar_valid

then have \( \langle zero, a\rangle \in \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real \longleftrightarrow \) \( \langle \bigcup \{x \in complex .\ cmulset \langle caddset \langle one, one\rangle , x\rangle = a\}, a\rangle \in \) \( lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \{\{complex\}\} \times real \) by (rule MMIsar0.MMI_halfpos )

then show \( thesis \)

qed

One more inequality.

lemma (in complex0) ledivp1t:

assumes A1: \( a \in \mathbb{R} \), \( b \in \mathbb{R} \) and A2: \( 0 \leq a \), \( 0 \leq b \)

shows \( (a / (b + 1 ))\cdot b \leq a \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( (a \in real \wedge \langle a, zero\rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real) \wedge \) \( b \in real \wedge \langle b, zero\rangle \notin lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real \longrightarrow \) \( \langle a,cmulset\langle \bigcup \{x \in complex .\ cmulset\langle caddset\langle b, one\rangle , x\rangle = a\}, b\rangle \rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real \) by (rule MMIsar0.MMI_ledivp1t )

with A1, A2 show \( thesis \)

qed

Natural real numbers

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.

Two ways of saying that there are no natural numbers between \(n\) and \(n+1\).

lemma (in complex0) no_nats_between:

assumes A1: \( n \in \mathbb{N} \), \( k \in \mathbb{N} \)

shows \( n\leq k \longleftrightarrow n \lt k + 1 \), \( n \lt k \longleftrightarrow n + 1 \leq k \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have I: \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( n \in \bigcap \{N \in Pow(real) .\ one \in N \wedge \) \( (\forall n.\ n \in N \longrightarrow caddset \langle n, one\rangle \in N)\} \wedge \) \( k \in \bigcap \{N \in Pow(real) .\ one \in N \wedge \) \( (\forall n.\ n \in N \longrightarrow caddset \langle n, one\rangle \in N)\} \longrightarrow \) \( \langle k, n\rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real \longleftrightarrow \) \( \langle n, caddset \langle k, one\rangle \rangle \in \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real \) by (rule MMIsar0.MMI_nnleltp1t )

then have \( n \in \mathbb{N} \wedge k \in \mathbb{N} \longrightarrow n \leq k \longleftrightarrow n \lt k + 1 \)

with A1 show \( n\leq k \longleftrightarrow n \lt k + 1 \)

from I have \( n \in \bigcap \{N \in Pow(real) .\ one \in N \wedge \) \( (\forall n.\ n \in N \longrightarrow caddset \langle n, one\rangle \in N)\} \wedge \) \( k \in \bigcap \{N \in Pow(real) .\ one \in N \wedge \) \( (\forall n.\ n \in N \longrightarrow caddset \langle n, one\rangle \in N)\} \longrightarrow \) \( \langle n, k\rangle \in \) \( lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real \longleftrightarrow \langle k, caddset \langle n, one\rangle \rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real \) by (rule MMIsar0.MMI_nnltp1let )

then have \( n \in \mathbb{N} \wedge k \in \mathbb{N} \longrightarrow n \lt k \longleftrightarrow n + 1 \leq k \)

with A1 show \( n \lt k \longleftrightarrow n + 1 \leq k \)

qed

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: \( \psi (1 ) \) and A2: \( \forall k \in \mathbb{N} .\ \psi (k) \longrightarrow \psi (k + 1 ) \) and A3: \( n \in \mathbb{N} \)

shows \( \psi (n) \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have I: \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

moreover

from A1, A2, A3 have \( \psi (one) \), \( \forall k\in \bigcap \{N \in Pow(real) .\ one \in N \wedge \) \( (\forall n.\ n \in N \longrightarrow caddset \langle n, one\rangle \in N)\}.\ \) \( \psi (k) \longrightarrow \psi (caddset \langle k, one\rangle ) \), \( n \in \bigcap \{N \in Pow(real) .\ one \in N \wedge \) \( (\forall n.\ n \in N \longrightarrow caddset \langle n, one\rangle \in N)\} \)

ultimately show \( \psi (n) \) by (rule MMIsar0.nnind1 )

qed

Some simple arithmetics.

lemma (in complex0) arith:

shows \( 2 + 2 = 4 \), \( 2 \cdot 2 = 4 \), \( 3 \cdot 2 = 6 \), \( 3 \cdot 3 = 9 \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have I: \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( caddset \langle caddset \langle one, one\rangle , caddset \langle one, one\rangle \rangle =\) \( caddset \langle caddset \langle caddset \langle one, one\rangle , one\rangle , one\rangle \) by (rule MMIsar0.MMI_2p2e4 )

thus \( 2 + 2 = 4 \)

from I have \( cmulset\langle caddset\langle one, one\rangle , caddset\langle one, one\rangle \rangle =\) \( caddset\langle caddset\langle caddset\langle one, one\rangle , one\rangle , one\rangle \) by (rule MMIsar0.MMI_2t2e4 )

thus \( 2 \cdot 2 = 4 \)

from I have \( cmulset\langle caddset\langle caddset\langle one, one\rangle , one\rangle , caddset\langle one, one\rangle \rangle =\) \( caddset \langle caddset\langle caddset\langle caddset\langle caddset\) \( \langle one, one\rangle , one\rangle , one\rangle , one\rangle , one\rangle \) by (rule MMIsar0.MMI_3t2e6 )

thus \( 3 \cdot 2 = 6 \)

from I have \( cmulset \) \( \langle caddset\langle caddset\langle one, one\rangle , one\rangle ,\) \( caddset\langle caddset\langle one, one\rangle , one\rangle \rangle =\) \( caddset\langle caddset\langle caddset \langle caddset \) \( \langle caddset\langle caddset\langle caddset\langle caddset\langle one, one\rangle , one\rangle , one\rangle , one\rangle ,\) \( one\rangle , one\rangle , one\rangle , one\rangle \) by (rule MMIsar0.MMI_3t3e9 )

thus \( 3 \cdot 3 = 9 \)

qed

Infimum and supremum in real numbers

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

If a set \(S\) has a smallest element, then the infimum of \(S\) belongs to it.

lemma (in complex0) lbinfmcl:

assumes A1: \( S \subseteq \mathbb{R} \) and A2: \( \exists x\in S.\ \forall y\in S.\ x \leq y \)

shows \( \text{Infim}(S,\mathbb{R} , \lt ) \in S \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have I: \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( S \subseteq real \wedge (\exists x\in S.\ \forall y\in S.\ \langle y, x\rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real) \longrightarrow \) \( \text{Sup}(S, real, \) \( converse(lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real)) \in S \) by (rule MMIsar0.MMI_lbinfmcl )

then have \( S \subseteq \mathbb{R} \wedge ( \exists x\in S.\ \forall y\in S.\ x \leq y) \longrightarrow \) \( \text{Sup}(S,\mathbb{R} ,converse( \lt )) \in S \)

with A1, A2 show \( thesis \) using Infim_def

qed

Supremum of any subset of reals that is bounded above is real.

lemma (in complex0) sup_is_real:

assumes \( A \subseteq \mathbb{R} \) and \( A \neq 0 \) and \( \exists x\in \mathbb{R} .\ \forall y\in A.\ y \leq x \)

shows \( \text{Sup}(A,\mathbb{R} , \lt ) \in \mathbb{R} \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( A \subseteq real \wedge A \neq 0 \wedge (\exists x\in real.\ \forall y\in A.\ \langle x, y\rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real) \longrightarrow \) \( \text{Sup}(A, real,\) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real) \in real \) by (rule MMIsar0.MMI_suprcl )

with assms show \( thesis \)

qed

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 \subseteq \mathbb{R} \) and \( A \neq 0 \) and \( \exists x\in \mathbb{R} .\ \forall y\in A.\ y \leq x \) and \( B \in \mathbb{R} \) and \( B \lt \text{Sup}(A,\mathbb{R} , \lt ) \)

shows \( \exists z\in A.\ B \lt z \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( (A \subseteq real \wedge A \neq 0 \wedge (\exists x\in real.\ \forall y\in A.\ \langle x, y\rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \) \( \{\{complex\}\} \times real)) \wedge B \in real \wedge \langle B, \text{Sup}(A, real,\) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \) \( \{\{complex\}\} \times real)\rangle \in lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real \longrightarrow \) \( (\exists z\in A.\ \langle B, z\rangle \in lessrrel \cap real \times real \cup \) \( \{\langle \{complex\}, complex\rangle \} \cup real \times \{complex\} \cup \) \( \{\{complex\}\} \times real) \) by (rule MMIsar0.MMI_suprlub )

with assms show \( thesis \)

qed

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 \subseteq \mathbb{R} \) and \( A \neq 0 \) and \( \exists x\in \mathbb{R} .\ \forall y\in A.\ x \leq y \)

shows \( \text{Infim}(A,\mathbb{R} , \lt ) \in \mathbb{R} \), \( \text{Infim}(A,\mathbb{R} , \lt ) = ( - \text{Sup}(\{z \in \mathbb{R} .\ ( - z) \in A \},\mathbb{R} , \lt ) ) \)proof

let \( real = \mathbb{R} \)

let \( complex = \mathbb{C} \)

let \( one = 1 \)

let \( zero = 0 \)

let \( iunit = \imath \)

let \( caddset = \text{CplxAdd}(R,A) \)

let \( cmulset = \text{CplxMul}(R,A,M) \)

let \( lessrrel = \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \)

have I: \( MMIsar0\) \( (real, complex, one, zero, iunit, caddset, cmulset, lessrrel) \) using MMIsar_valid

then have \( A \subseteq real \wedge A \neq 0 \wedge (\exists x\in real.\ \forall y\in A.\ \langle y, x\rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \) \( \{\{complex\}\} \times real) \longrightarrow \text{Sup}(A, real, converse\) \( (lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \) \( \{\{complex\}\} \times real)) =\) \( \bigcup \{x \in complex .\ caddset\) \( \langle \text{Sup}(\{z \in real .\ \bigcup \{x \in complex .\ caddset\langle z, x\rangle = zero\} \in A\}, real,\) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real), x\rangle = zero\} \) by (rule MMIsar0.MMI_infmsup )

then have \( A \subseteq \mathbb{R} \wedge \neg (A = 0) \wedge ( \exists x\in \mathbb{R} .\ \forall y\in A.\ x \leq y) \longrightarrow \) \( \text{Sup}(A,\mathbb{R} ,converse( \lt )) = ( - \text{Sup}(\{z \in \mathbb{R} .\ ( - z) \in A \},\mathbb{R} , \lt ) ) \)

with assms show \( \text{Infim}(A,\mathbb{R} , \lt ) = ( - \text{Sup}(\{z \in \mathbb{R} .\ ( - z) \in A \},\mathbb{R} , \lt ) ) \) using Infim_def

from I have \( A \subseteq real \wedge A \neq 0 \wedge (\exists x\in real.\ \forall y\in A.\ \langle y, x\rangle \notin \) \( lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \) \( \{\{complex\}\} \times real) \longrightarrow \text{Sup}(A, real, converse\) \( (lessrrel \cap real \times real \cup \{\langle \{complex\}, complex\rangle \} \cup \) \( real \times \{complex\} \cup \{\{complex\}\} \times real)) \in real \) by (rule MMIsar0.MMI_infmrcl )

with assms show \( \text{Infim}(A,\mathbb{R} , \lt ) \in \mathbb{R} \) using Infim_def

qed

end

lemma (in complex0) MMIsar_valid: shows \( MMIsar0(\mathbb{R} ,\mathbb{C} ,1 , 0 ,\imath , \text{CplxAdd}(R,A), \text{CplxMul}(R,A,M),\) \( \text{StrictVersion}( \text{CplxROrder}(R,A,r))) \)

lemma (in complex0) cplx_strict_ord_on_cplx_reals: shows \( \text{StrictVersion}( \text{CplxROrder}(R,A,r)) \subseteq \mathbb{R} \times \mathbb{R} \)

Definition of Infim: \( \text{Infim}(B,A,R) \equiv \text{Sup}(B,A,converse(R)) \)