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

shows \( a\cdot b \in \mathbb{C} \)
lemma (in complex0) axdistr:

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

shows \( a\cdot (b + c) = a\cdot b + a\cdot c \)
lemma (in complex0) axaddcom:

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

shows \( a + b = b + a \)
lemma (in complex0) axaddass:

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

shows \( a + b + c = a + (b + c) \)
lemma (in complex0) axmulass:

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

shows \( a \cdot b \cdot c = a \cdot (b \cdot c) \)
lemma (in complex0) ax1re: shows \( 1 \in \mathbb{R} \)
lemma (in complex0) axi2m1: shows \( \imath \cdot \imath + 1 = 0 \)
lemma (in complex0) ax0id:

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

shows \( a + 0 = a \)
lemma (in complex0) axicn: shows \( \imath \in \mathbb{C} \)
lemma (in complex0) axnegex:

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

shows \( \exists x\in \mathbb{C} .\ a + x = 0 \)
lemma (in complex0) axrecex:

assumes \( a \in \mathbb{C} \) and \( a\neq 0 \)

shows \( \exists x\in \mathbb{C} .\ a\cdot x = 1 \)
lemma (in complex0) ax1id:

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

shows \( a\cdot 1 = a \)
lemma (in complex0) axaddrcl:

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

shows \( a + b \in \mathbb{R} \)
lemma (in complex0) axmulrcl:

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

shows \( a \cdot b \in \mathbb{R} \)
lemma (in complex0) axrnegex:

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

shows \( \exists x \in \mathbb{R} .\ a + x = 0 \)
lemma (in complex0) axrrecex:

assumes \( a \in \mathbb{R} \), \( a \neq 0 \)

shows \( \exists x\in \mathbb{R} .\ a \cdot x = 1 \)