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
qed
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
}
moreover 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
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
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 \)
This page by Slawomir Kolodynski is licensed under a Creative Commons Attribution 3.0 License. BTC: 1JzFajFtGwiKiRHbZyCB1KtASgsM1kFU2h