IsarMathLib

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

theory Metamath_Interface imports Complex_ZF MMI_prelude

begin

This theory contains some lemmas that make it possible to use the theorems translated from Metamath in a the complex0 context.

MMisar0 and complex0 contexts.

In the section we show a lemma that the assumptions in complex0 context imply the assumptions of the MMIsar0 context. The Metamath_sampler theory provides examples how this lemma can be used.

The next lemma states that we can use the theorems proven in the MMIsar0 context in the complex0 context. Unfortunately we have to use low level Isabelle methods "rule" and "unfold" in the proof, simp and blast fail on the order axioms.

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))) \)proof

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

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

let \( zero = 0 \)

let \( one = 1 \)

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 \( (\forall a b.\ a \in real \wedge b \in real \longrightarrow \) \( \langle a, b\rangle \in lessrrel \longleftrightarrow \neg (a = b \vee \langle b, a\rangle \in lessrrel)) \)proof

have I: \( \forall a b.\ a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow (a \lt _{\mathbb{R}} b \longleftrightarrow \neg (a=b \vee b \lt _{\mathbb{R}} a)) \) using pre_axlttri

{

fix \( a \) \( b \)

assume \( a \in real \wedge b \in real \)

with I have \( (a \lt _{\mathbb{R}} b \longleftrightarrow \neg (a=b \vee b \lt _{\mathbb{R}} a)) \)

hence \( \langle a, b\rangle \in lessrrel \longleftrightarrow \neg (a = b \vee \langle b, a\rangle \in lessrrel) \)

}

thus \( (\forall a b.\ a \in real \wedge b \in real \longrightarrow \) \( (\langle a, b\rangle \in lessrrel \longleftrightarrow \neg (a = b \vee \langle b, a\rangle \in lessrrel))) \)

qed

moreover

have \( (\forall a b c.\ \) \( a \in real \wedge b \in real \wedge c \in real \longrightarrow \) \( \langle a, b\rangle \in lessrrel \wedge \langle b, c\rangle \in lessrrel \longrightarrow \langle a, c\rangle \in lessrrel) \)proof

have II: \( \forall a b c.\ a \in \mathbb{R} \wedge b \in \mathbb{R} \wedge c \in \mathbb{R} \longrightarrow \) \( ((a \lt _{\mathbb{R}} b \wedge b \lt _{\mathbb{R}} c) \longrightarrow a \lt _{\mathbb{R}} c) \) using pre_axlttrn

{

fix \( a \) \( b \) \( c \)

assume \( a \in real \wedge b \in real \wedge c \in real \)

with II have \( (a \lt _{\mathbb{R}} b \wedge b \lt _{\mathbb{R}} c) \longrightarrow a \lt _{\mathbb{R}} c \)

hence \( \langle a, b\rangle \in lessrrel \wedge \langle b, c\rangle \in lessrrel \longrightarrow \langle a, c\rangle \in lessrrel \)

}

thus \( (\forall a b c.\ \) \( a \in real \wedge b \in real \wedge c \in real \longrightarrow \) \( \langle a, b\rangle \in lessrrel \wedge \langle b, c\rangle \in lessrrel \longrightarrow \langle a, c\rangle \in lessrrel) \)

qed

moreover

have \( (\forall A B C.\ \) \( A \in real \wedge B \in real \wedge C \in real \longrightarrow \) \( \langle A, B\rangle \in lessrrel \longrightarrow \) \( \langle caddset \langle C, A\rangle , caddset \langle C, B\rangle \rangle \in lessrrel) \) using pre_axltadd

moreover

have \( (\forall A B.\ A \in real \wedge B \in real \longrightarrow \) \( \langle zero, A\rangle \in lessrrel \wedge \langle zero, B\rangle \in lessrrel \longrightarrow \) \( \langle zero, cmulset \langle A, B\rangle \rangle \in lessrrel) \) using pre_axmulgt0

moreover

have \( (\forall S.\ S \subseteq real \wedge S \neq 0 \wedge (\exists x\in real.\ \forall y\in S.\ \langle y, x\rangle \in lessrrel) \longrightarrow \) \( (\exists x\in real.\ \) \( (\forall y\in S.\ \langle x, y\rangle \notin lessrrel) \wedge \) \( (\forall y\in real.\ \langle y, x\rangle \in lessrrel \longrightarrow (\exists z\in S.\ \langle y, z\rangle \in lessrrel)))) \) using pre_axsup

moreover

have \( \mathbb{R} \subseteq \mathbb{C} \) using axresscn

moreover

have \( 1 \neq 0 \) using ax1ne0

moreover

have \( \mathbb{C} \text{ is a set } \)

moreover

have \( \text{CplxAdd}(R,A) : \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) using axaddopr

moreover

have \( \text{CplxMul}(R,A,M) : \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) using axmulopr

moreover

have \( \forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow a\cdot b = b \cdot a \) using axmulcom

hence \( (\forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( cmulset \langle a, b\rangle = cmulset \langle b, a\rangle \) \( ) \)

moreover

have \( \forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow a + b \in \mathbb{C} \) using axaddcl

hence \( (\forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( caddset \langle a, b\rangle \in \mathbb{C} \) \( ) \)

moreover

have \( \forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow a \cdot b \in \mathbb{C} \) using axmulcl

hence \( (\forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( cmulset \langle a, b\rangle \in \mathbb{C} ) \)

moreover

have \( \forall a b C.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow \) \( a \cdot (b + C) = a \cdot b + a \cdot C \) using axdistr

hence \( \forall a b C.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow \) \( cmulset \langle a, caddset \langle b, C\rangle \rangle =\) \( caddset \) \( \langle cmulset \langle a, b\rangle , cmulset \langle a, C\rangle \rangle \)

moreover

have \( \forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( a + b = b + a \) using axaddcom

hence \( \forall a b.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( caddset \langle a, b\rangle = caddset \langle b, a\rangle \)

moreover

have \( \forall a b C.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow \) \( a + b + C = a + (b + C) \) using axaddass

hence \( \forall a b C.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow \) \( caddset \langle caddset \langle a, b\rangle , C\rangle =\) \( caddset \langle a, caddset \langle b, C\rangle \rangle \)

moreover

have \( \forall a b c.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge c \in \mathbb{C} \longrightarrow a\cdot b\cdot c = a\cdot (b\cdot c) \) using axmulass

hence \( \forall a b C.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow \) \( cmulset \langle cmulset \langle a, b\rangle , C\rangle =\) \( cmulset \langle a, cmulset \langle b, C\rangle \rangle \)

moreover

have \( 1 \in \mathbb{R} \) using ax1re

moreover

have \( \imath \cdot \imath + 1 = 0 \) using axi2m1

hence \( caddset \langle cmulset \langle \imath , \imath \rangle , 1 \rangle = 0 \)

moreover

have \( \forall a.\ a \in \mathbb{C} \longrightarrow a + 0 = a \) using ax0id

hence \( \forall a.\ a \in \mathbb{C} \longrightarrow caddset \langle a, 0 \rangle = a \)

moreover

have \( \imath \in \mathbb{C} \) using axicn

moreover

have \( \forall a.\ a \in \mathbb{C} \longrightarrow (\exists x\in \mathbb{C} .\ a + x = 0 ) \) using axnegex

hence \( \forall a.\ a \in \mathbb{C} \longrightarrow \) \( (\exists x\in \mathbb{C} .\ caddset \langle a, x\rangle = 0 ) \)

moreover

have \( \forall a.\ a \in \mathbb{C} \wedge a \neq 0 \longrightarrow (\exists x\in \mathbb{C} .\ a \cdot x = 1 ) \) using axrecex

hence \( \forall a.\ a \in \mathbb{C} \wedge a \neq 0 \longrightarrow \) \( ( \exists x\in \mathbb{C} .\ cmulset \langle a, x\rangle = 1 ) \)

moreover

have \( \forall a.\ a \in \mathbb{C} \longrightarrow a\cdot 1 = a \) using ax1id

hence \( \forall a.\ a \in \mathbb{C} \longrightarrow \) \( cmulset \langle a, 1 \rangle = a \)

moreover

have \( \forall a b.\ a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow a + b \in \mathbb{R} \) using axaddrcl

hence \( \forall a b.\ a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow \) \( caddset \langle a, b\rangle \in \mathbb{R} \)

moreover

have \( \forall a b.\ a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow a \cdot b \in \mathbb{R} \) using axmulrcl

hence \( \forall a b.\ a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow \) \( cmulset \langle a, b\rangle \in \mathbb{R} \)

moreover

have \( \forall a.\ a \in \mathbb{R} \longrightarrow (\exists x\in \mathbb{R} .\ a + x = 0 ) \) using axrnegex

hence \( \forall a.\ a \in \mathbb{R} \longrightarrow \) \( ( \exists x\in \mathbb{R} .\ caddset \langle a, x\rangle = 0 ) \)

moreover

have \( \forall a.\ a \in \mathbb{R} \wedge a\neq 0 \longrightarrow (\exists x\in \mathbb{R} .\ a \cdot x = 1 ) \) using axrrecex

hence \( \forall a.\ a \in \mathbb{R} \wedge a \neq 0 \longrightarrow \) \( ( \exists x\in \mathbb{R} .\ cmulset \langle a, x\rangle = 1 ) \)

ultimately have \( (\) \( (\) \( (\) \( ( \forall a b.\ \) \( a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow \) \( \langle a, b\rangle \in lessrrel \longleftrightarrow \) \( \neg (a = b \vee \langle b, a\rangle \in lessrrel)\) \( ) \wedge \) \( \) \( ( \forall a b C.\ \) \( a \in \mathbb{R} \wedge b \in \mathbb{R} \wedge C \in \mathbb{R} \longrightarrow \) \( \langle a, b\rangle \in lessrrel \wedge \) \( \langle b, C\rangle \in lessrrel \longrightarrow \) \( \langle a, C\rangle \in lessrrel\) \( ) \wedge \) \( \) \( (\forall a b C.\ \) \( a \in \mathbb{R} \wedge b \in \mathbb{R} \wedge C \in \mathbb{R} \longrightarrow \) \( \langle a, b\rangle \in lessrrel \longrightarrow \) \( \langle caddset \langle C, a\rangle , caddset \langle C, b\rangle \rangle \in \) \( lessrrel\) \( )\) \( ) \wedge \) \( \) \( (\) \( ( \forall a b.\ \) \( a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow \) \( \langle 0 , a\rangle \in lessrrel \wedge \) \( \langle 0 , b\rangle \in lessrrel \longrightarrow \) \( \langle 0 , cmulset \langle a, b\rangle \rangle \in \) \( lessrrel\) \( ) \wedge \) \( \) \( ( \forall S.\ S \subseteq \mathbb{R} \wedge S \neq 0 \wedge \) \( ( \exists x\in \mathbb{R} .\ \forall y\in S.\ \langle y, x\rangle \in lessrrel\) \( ) \longrightarrow \) \( ( \exists x\in \mathbb{R} .\ \) \( ( \forall y\in S.\ \langle x, y\rangle \notin lessrrel\) \( ) \wedge \) \( ( \forall y\in \mathbb{R} .\ \langle y, x\rangle \in lessrrel \longrightarrow \) \( ( \exists z\in S.\ \langle y, z\rangle \in lessrrel\) \( )\) \( )\) \( )\) \( )\) \( ) \wedge \) \( \) \( \mathbb{R} \subseteq \mathbb{C} \wedge \) \( 1 \neq 0 \) \( ) \wedge \) \( \) \( ( \mathbb{C} \text{ is a set } \wedge caddset \in \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \wedge \) \( cmulset \in \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \) \( ) \wedge \) \( \) \( (\) \( (\forall a b.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( cmulset \langle a, b\rangle = cmulset \langle b, a\rangle \) \( ) \wedge \) \( \) \( (\forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( caddset \langle a, b\rangle \in \mathbb{C} \) \( )\) \( \) \( ) \wedge \) \( \) \( (\forall a b.\ a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( cmulset \langle a, b\rangle \in \mathbb{C} \) \( ) \wedge \) \( \) \( (\forall a b C.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow \) \( cmulset \langle a, caddset \langle b, C\rangle \rangle =\) \( caddset \) \( \langle cmulset \langle a, b\rangle , cmulset \langle a, C\rangle \rangle \) \( )\) \() \wedge \) \(\) \(\) \((\) \( (\) \( (\forall a b.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \longrightarrow \) \( caddset \langle a, b\rangle = caddset \langle b, a\rangle \) \( ) \wedge \) \( \) \( (\forall a b C.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow \) \( caddset \langle caddset \langle a, b\rangle , C\rangle =\) \( caddset \langle a, caddset \langle b, C\rangle \rangle \) \( ) \wedge \) \( \) \( (\forall a b C.\ \) \( a \in \mathbb{C} \wedge b \in \mathbb{C} \wedge C \in \mathbb{C} \longrightarrow \) \( cmulset \langle cmulset \langle a, b\rangle , C\rangle =\) \( cmulset \langle a, cmulset \langle b, C\rangle \rangle \) \( )\) \( ) \wedge \) \( \) \( \) \( (1 \in \mathbb{R} \wedge \) \( caddset \langle cmulset \langle \imath , \imath \rangle , 1 \rangle = 0 \) \( ) \wedge \) \( \) \( (\forall a.\ a \in \mathbb{C} \longrightarrow caddset \langle a, 0 \rangle = a\) \( ) \wedge \) \( \) \( \imath \in \mathbb{C} \) \() \wedge \) \( \) \((\) \( (\forall a.\ a \in \mathbb{C} \longrightarrow \) \( (\exists x\in \mathbb{C} .\ caddset \langle a, x\rangle = 0 \) \( )\) \( ) \wedge \) \( \) \( ( \forall a.\ a \in \mathbb{C} \wedge a \neq 0 \longrightarrow \) \( ( \exists x\in \mathbb{C} .\ cmulset \langle a, x\rangle = 1 \) \( )\) \( ) \wedge \) \( \) \( ( \forall a.\ a \in \mathbb{C} \longrightarrow \) \( cmulset \langle a, 1 \rangle = a\) \( )\) \() \wedge \) \( \) \((\) \( ( \forall a b.\ a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow \) \( caddset \langle a, b\rangle \in \mathbb{R} \) \( ) \wedge \) \( \) \( ( \forall a b.\ a \in \mathbb{R} \wedge b \in \mathbb{R} \longrightarrow \) \( cmulset \langle a, b\rangle \in \mathbb{R} \) \( )\) \() \wedge \) \( \) \(( \forall a.\ a \in \mathbb{R} \longrightarrow \) \( ( \exists x\in \mathbb{R} .\ caddset \langle a, x\rangle = 0 \) \( ) \) \() \wedge \) \( \) \(( \forall a.\ a \in \mathbb{R} \wedge a \neq 0 \longrightarrow \) \( ( \exists x\in \mathbb{R} .\ cmulset \langle a, x\rangle = 1 \) \( )\) \() \)

then show \( MMIsar0(\mathbb{R} ,\mathbb{C} ,1 , 0 ,\imath , \text{CplxAdd}(R,A), \text{CplxMul}(R,A,M),\) \( \text{StrictVersion}( \text{CplxROrder}(R,A,r))) \) unfolding MMIsar0_def

qed

end

lemma (in complex0) pre_axlttri:

assumes \( a \in \mathbb{R} \), \( b \in \mathbb{R} \)

shows \( a \lt _{\mathbb{R}} b \longleftrightarrow \neg (a=b \vee b \lt _{\mathbb{R}} a) \)

lemma (in complex0) pre_axlttrn:

assumes \( a \lt _{\mathbb{R}} b \), \( b \lt _{\mathbb{R}} c \)

shows \( a \lt _{\mathbb{R}} c \)

lemma (in complex0) pre_axltadd:

assumes \( a \lt _{\mathbb{R}} b \) and \( c \in \mathbb{R} \)

shows \( c + a \lt _{\mathbb{R}} c + b \)

lemma (in complex0) pre_axmulgt0:

assumes \( 0 \lt _{\mathbb{R}} a \), \( 0 \lt _{\mathbb{R}} b \)

shows \( 0 \lt _{\mathbb{R}} a\cdot b \)

lemma (in complex0) pre_axsup:

assumes \( X \subseteq \mathbb{R} \), \( X \neq 0 \) and \( \exists x\in \mathbb{R} .\ \forall y\in X.\ y \lt _{\mathbb{R}} x \)

shows \( \exists x\in \mathbb{R} .\ (\forall y\in X.\ \neg (x \lt _{\mathbb{R}} y)) \wedge (\forall y\in \mathbb{R} .\ (y \lt _{\mathbb{R}} x \longrightarrow (\exists z\in X.\ y \lt _{\mathbb{R}} z))) \)

lemma (in complex0) axresscn: shows \( \mathbb{R} \subseteq \mathbb{C} \)

lemma (in complex0) ax1ne0: shows \( 1 \neq 0 \)

lemma (in complex0) axaddopr: shows \( \text{CplxAdd}(R,A): \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \)

lemma (in complex0) axmulopr: shows \( \text{CplxMul}(R,A,M): \mathbb{C} \times \mathbb{C} \rightarrow \mathbb{C} \)

lemma (in complex0) axmulcom:

assumes \( a \in \mathbb{C} \), \( b \in \mathbb{C} \)

shows \( a\cdot b = b\cdot a \)

lemma (in complex0) axaddcl:

assumes \( a \in \mathbb{C} \), \( b \in \mathbb{C} \)

shows \( a + b \in \mathbb{C} \)

lemma (in complex0) axmulcl:

assumes \( a \in \mathbb{C} \), \( b \in \mathbb{C} \)