Theory MMI_Complex_ZF_2
section ‹Complex numbers in Metamatah 2›
theory MMI_Complex_ZF_2
imports MMI_logic_and_sets_1 MMI_Complex_ZF_1 InductiveSeq_ZF
begin
text‹This theory contains theorems (with proofs) about complex numbers
imported from the Metamath's set.mm database.
The original Metamath proofs were mostly written by Norman Megill,
see the Metamath Proof Explorer pages for more detailed atribution.
This theory contains about 100 theorems from ‹1nn› to ‹infmrcl›
›
lemma (in MMIsar0) MMI_df_n: shows
"ℕ = ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) }"
proof -
let ?K⇩1 = "{N ∈ Pow(ℝ). 𝟭 ∈ N ∧ (∀n. n∈N ⟶ n\<ca>𝟭 ∈ N)}"
let ?K⇩2 = "{N ∈ Pow(ℝ). 𝟭 ∈ N ∧ (∀n∈N. n\<ca>𝟭 ∈ N)}"
{ fix N assume "N ∈ ?K⇩1"
hence "N ∈ Pow(ℝ)" "𝟭 ∈ N" "∀n. n∈N ⟶ n\<ca>𝟭 ∈ N"
by auto
then have "N ∈ ?K⇩2" by auto }
moreover
{ fix N assume "N ∈ ?K⇩2"
hence "N ∈ Pow(ℝ)" "𝟭 ∈ N" "∀n∈N. n\<ca>𝟭 ∈ N"
by auto
then have "N ∈ ?K⇩1" by auto }
ultimately have "?K⇩1 = ?K⇩2" by blast
then show ?thesis using cxn_def by simp
qed
lemma (in MMIsar0) MMI_Ndef_nonempty:
shows "{x ∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) } ≠ 0"
proof -
have
"\<caddset> : ( ℂ × ℂ ) → ℂ" "ℝ ⊆ ℂ" and I: "𝟭 ∈ ℝ"
using MMI_axaddopr MMI_axresscn MMI_ax1re by auto
moreover from I have "∀y∈ℝ. \<caddset>`⟨y,𝟭⟩ ∈ ℝ"
using MMI_axaddrcl ca_def by simp
ultimately have
"{x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. \<caddset>`⟨y,𝟭⟩ ∈ x) } ≠ 0"
using binop_gen_set_ex1 by auto
then show ?thesis using ca_def by simp
qed
lemma (in MMIsar0) MMI_1nn: shows "𝟭 ∈ ℕ"
using MMI_df_n MMI_Ndef_nonempty by auto
lemma (in MMIsar0) MMI_nnind0:
assumes A1: "∀x. x = 𝟭 ⟶ φ(x) ⟷ ψ(x)" and
A2: "∀y x. x = y ⟶ φ(x) ⟷ ch(x\<ca>𝟭)" and
A3: "∀y x. x = y \<ca> 𝟭 ⟶ φ(x) ⟷ θ(x)" and
A4: "∀x. x = A ⟶ φ(x) ⟷ τ(x)" and
A5: "ψ(𝟭)" and
A6: "∀y. y ∈ ℕ ⟶ ch(y\<ca>𝟭) ⟶ θ(y\<ca>𝟭)"
shows "A ∈ ℕ ⟶ τ(A)"
proof -
from A1 have S1: "∀x. x = 𝟭 ⟶ φ(x) ⟷ ψ(x)".
from S1 have S2: "𝟭 ∈ {x ∈ ℕ. φ(x) } ⟷ 𝟭 ∈ ℕ ∧ ψ(𝟭)" by (rule MMI_elrab)
have S3: "𝟭 ∈ ℕ" by (rule MMI_1nn)
from A5 have S4: "ψ(𝟭)".
from S2 S3 S4 have S5: "𝟭 ∈ {x ∈ ℕ. φ(x) }" by (rule MMI_mpbir2an)
have S6: "{x ∈ ℕ. φ(x) } ⊆ℕ" by (rule MMI_ssrab2)
{ fix y
from S6 have S7: "y ∈ {x ∈ ℕ. φ(x) } ⟶ y ∈ ℕ" by (rule MMI_sseli)
have S8: "y ∈ ℕ ⟶ y \<ca> 𝟭 ∈ ℕ" by (rule MMI_peano2nn)
from S8 have S9: "y ∈ ℕ ⟶ y ∈ ℕ ⟶ y \<ca> 𝟭 ∈ ℕ" by (rule MMI_a1d)
from A6 have S10: "y ∈ ℕ ⟶ ch(y\<ca>𝟭) ⟶ θ(y\<ca>𝟭)" by simp
from S9 S10 have S11: "y ∈ ℕ ⟶ y ∈ ℕ ∧ ch(y\<ca>𝟭) ⟶ y \<ca> 𝟭 ∈ ℕ ∧ θ(y\<ca>𝟭)"
by (rule MMI_anim12d)
from A2 have S12: "∀ x. x = y ⟶ φ(x) ⟷ ch(x\<ca>𝟭)" by simp
from S12 have S13: "y ∈ {x ∈ ℕ. φ(x) } ⟷ y ∈ ℕ ∧ ch(y\<ca>𝟭)" by (rule MMI_elrab)
from A3 have S14: "∀ x. x = y \<ca> 𝟭 ⟶ φ(x) ⟷ θ(x)" by simp
from S14 have S15: "y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) } ⟷ y \<ca> 𝟭 ∈ ℕ ∧ θ(y\<ca>𝟭)"
by (rule MMI_elrab)
from S11 S13 S15 have S16:
"y ∈ ℕ ⟶ y ∈ {x ∈ ℕ. φ(x) } ⟶ y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }" by (rule MMI_3imtr4g)
from S7 S16 have S17: "y ∈ {x ∈ ℕ. φ(x) } ⟶ y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }"
by (rule MMI_mpcom) }
then have S17: "∀y. y ∈ {x ∈ ℕ. φ(x) } ⟶ y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }"
by simp
from S17 have S18: "∀y∈{x ∈ ℕ. φ(x) }. y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }" by (rule MMI_rgen)
have S19: "ℕ = ℕ" by (rule MMI_nnex)
from S19 have S20: "{x ∈ ℕ. φ(x) } = {x ∈ ℕ. φ(x) }" by (rule MMI_rabex)
from S20 have S21: "𝟭 ∈ {x ∈ ℕ. φ(x) } ∧ (∀y∈{x ∈ ℕ. φ(x) }. y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }) ⟶
ℕ ⊆{x ∈ ℕ. φ(x) }" by (rule MMI_peano5nn)
from S5 S18 S21 have S22: "ℕ ⊆{x ∈ ℕ. φ(x) }" by (rule MMI_mp2an)
from S22 have S23: "A ∈ ℕ ⟶ A ∈ {x ∈ ℕ. φ(x) }" by (rule MMI_sseli)
from A4 have S24: "∀x. x = A ⟶ φ(x) ⟷ τ(x)" .
from S24 have S25: "A ∈ {x ∈ ℕ. φ(x) } ⟷ A ∈ ℕ ∧ τ(A)" by (rule MMI_elrab)
from S23 S25 have S26: "A ∈ ℕ ⟶ A ∈ ℕ ∧ τ(A)" by (rule MMI_sylib)
from S26 show "A ∈ ℕ ⟶ τ(A)" by (rule MMI_pm3_27d)
qed
lemma (in MMIsar0) MMI_nnind:
assumes A1: "∀x. x = 𝟭 ⟶ φ(x) ⟷ ψ(𝟭)" and
A2: "∀x y. x = y ⟶ φ(x) ⟷ ch(y)" and
A3: "∀x y. x = y \<ca> 𝟭 ⟶ φ(x) ⟷ θ(y\<ca>𝟭)" and
A4: "∀x. x = B ⟶ φ(x) ⟷ τ(B)" and
A5: "ψ(𝟭)" and
A6: "∀y. y ∈ ℕ ⟶ ch(y) ⟶ θ(y\<ca>𝟭)"
shows "B ∈ ℕ ⟶ τ(B)"
proof -
from A1 have S1: "∀x. x = 𝟭 ⟶ φ(x) ⟷ ψ(𝟭)".
from S1 have S2: "𝟭 ∈ {x ∈ ℕ. φ(x) } ⟷ 𝟭 ∈ ℕ ∧ ψ(𝟭)" by (rule MMI_elrab)
have S3: "𝟭 ∈ ℕ" by (rule MMI_1nn)
from A5 have S4: "ψ(𝟭)".
from S2 S3 S4 have S5: "𝟭 ∈ {x ∈ ℕ. φ(x) }" by (rule MMI_mpbir2an)
have S6: "{x ∈ ℕ. φ(x) } ⊆ ℕ" by (rule MMI_ssrab2)
{ fix y
from S6 have S7: "y ∈ {x ∈ ℕ. φ(x) } ⟶ y ∈ ℕ" by (rule MMI_sseli)
have S8: "y ∈ ℕ ⟶ y \<ca> 𝟭 ∈ ℕ" by (rule MMI_peano2nn)
from S8 have S9: "y ∈ ℕ ⟶ y ∈ ℕ ⟶ y \<ca> 𝟭 ∈ ℕ" by (rule MMI_a1d)
from A6 have S10: "y ∈ ℕ ⟶ ch(y) ⟶ θ(y\<ca>𝟭)" by simp
from S9 S10 have S11: "y ∈ ℕ ⟶ y ∈ ℕ ∧ ch(y) ⟶ y \<ca> 𝟭 ∈ ℕ ∧ θ(y\<ca>𝟭)"
by (rule MMI_anim12d)
from A2 have S12: "∀ x. x = y ⟶ φ(x) ⟷ ch(y)" by simp
from S12 have S13: "y ∈ {x ∈ ℕ. φ(x) } ⟷ y ∈ ℕ ∧ ch(y)" by (rule MMI_elrab)
from A3 have S14: "∀ x. x = y \<ca> 𝟭 ⟶ φ(x) ⟷ θ(y\<ca>𝟭)" by simp
from S14 have S15: "y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) } ⟷ y \<ca> 𝟭 ∈ ℕ ∧ θ(y\<ca>𝟭)"
by (rule MMI_elrab)
from S11 S13 S15 have S16:
"y ∈ ℕ ⟶ y ∈ {x ∈ ℕ. φ(x) } ⟶ y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }" by (rule MMI_3imtr4g)
from S7 S16 have "y ∈ {x ∈ ℕ. φ(x) } ⟶ y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }"
by (rule MMI_mpcom) }
then have S17: "∀y. y ∈ {x ∈ ℕ. φ(x) } ⟶ y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }"
by simp
from S17 have S18: "∀y∈{x ∈ ℕ. φ(x) }. y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }" by (rule MMI_rgen)
have S19: "ℕ = ℕ" by (rule MMI_nnex)
from S19 have S20: "{x ∈ ℕ. φ(x) } = {x ∈ ℕ. φ(x) }" by (rule MMI_rabex)
from S20 have S21:
"𝟭 ∈ {x ∈ ℕ. φ(x) } ∧ (∀y∈{x ∈ ℕ. φ(x) }. y \<ca> 𝟭 ∈ {x ∈ ℕ. φ(x) }) ⟶
ℕ ⊆{x ∈ ℕ. φ(x) }" by (rule MMI_peano5nn)
from S5 S18 S21 have S22: "ℕ ⊆{x ∈ ℕ. φ(x) }" by (rule MMI_mp2an)
from S22 have S23: "B ∈ ℕ ⟶ B ∈ {x ∈ ℕ. φ(x) }" by (rule MMI_sseli)
from A4 have S24: "∀x. x = B ⟶ φ(x) ⟷ τ(B)" .
from S24 have S25: "B ∈ {x ∈ ℕ. φ(x) } ⟷ B ∈ ℕ ∧ τ(B)" by (rule MMI_elrab)
from S23 S25 have S26: "B ∈ ℕ ⟶ B ∈ ℕ ∧ τ(B)" by (rule MMI_sylib)
from S26 show "B ∈ ℕ ⟶ τ(B)" by (rule MMI_pm3_27d)
qed
text‹Induction - on (real) natural numbers - version for humans.›
corollary (in MMIsar0) nnind1:
assumes A1: "ψ(𝟭)" and
A2: "∀k ∈ ℕ. ψ(k) ⟶ ψ(k\<ca>𝟭)" and
A3: "n ∈ ℕ"
shows "ψ(n)"
proof -
have "∀x. x = 𝟭 ⟶ ψ(x) ⟷ ψ(𝟭)" by simp
moreover have "∀x y. x = y ⟶ ψ(x) ⟷ ψ(y)" by simp
moreover have "∀x y. x = y \<ca> 𝟭 ⟶ ψ(x) ⟷ ψ(y\<ca>𝟭)" by simp
moreover have "∀x. x = n ⟶ ψ(x) ⟷ ψ(n)" by simp
moreover note A1
moreover from A2 have "∀k. k ∈ ℕ ⟶ ψ(k) ⟶ ψ(k\<ca>𝟭)" by blast
ultimately have "n ∈ ℕ ⟶ ψ(n)" by (rule MMI_nnind)
with A3 show "ψ(n)" by simp
qed
lemma (in MMIsar0) MMI_nn1suc: assumes
A1: "∀x. x = 𝟭 ⟶ φ(x) ⟷ ψ(𝟭)" and
A3: "∀x y. x = y \<ca> 𝟭 ⟶ φ(x) ⟷ ch(y\<ca>𝟭)" and
A4: "∀x. x = A ⟶ φ(x) ⟷ θ(A)" and
A5: "ψ(𝟭)" and
A6: "∀y. y ∈ ℕ ⟶ ch(y\<ca>𝟭)"
shows "A ∈ ℕ ⟶ θ(A)"
proof -
have S1: "∀ z. z = 𝟭 ⟶ (A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ φ(𝟭))" by auto
have S2: "∀z y. z = y ⟶ (A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ φ(y))" by auto
have S3: "∀z y. z = y \<ca> 𝟭 ⟶ (A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ φ(y\<ca>𝟭))"
by auto
{ fix z
have S4: "z = A ⟶ φ(z) ⟷ φ(A)" by auto
have S5: "A ∈ ℕ ⟶ ( ∃x. x = A)" by (rule MMI_elex)
have S6: "z ∈ A ⟶ (∀x. z ∈ A)" by (rule MMI_ax_17)
from S6 have S7: "(A ∈ ℕ ⟶ φ(A)) ⟶ (∀x. A ∈ ℕ ⟶ φ(A))" by auto
have S8: "(A ∈ ℕ ⟶ θ(A)) ⟶ (∀x. A ∈ ℕ ⟶ θ(A))" by (rule MMI_ax_17)
have S9:
"((A ∈ ℕ ⟶ φ(A)) ⟷ (A ∈ ℕ ⟶ θ(A))) ⟶ (∀x. (A ∈ ℕ ⟶ φ(A)) ⟷
(A ∈ ℕ ⟶ θ(A)))" by auto
have S10: "∀x. x = A ⟶ φ(x) ⟷ φ(A)" by auto
from A4 have S11: "∀x. x = A ⟶ φ(x) ⟷ θ(A)".
from S10 S11 have S12: "∀ x. x = A ⟶ φ(x) ⟷ θ(A)" by auto
from S12 have S13: "∀x. x = A ⟶ (A ∈ ℕ ⟶ φ(x)) ⟷ (A ∈ ℕ ⟶ θ(A))" by auto
from S9 S13 have S14: "( ∃x. x = A) ⟶ (A ∈ ℕ ⟶ φ(A)) ⟷ (A ∈ ℕ ⟶ θ(A))"
by auto
from S5 S14 have S15: "A ∈ ℕ ⟶ (A ∈ ℕ ⟶ φ(A)) ⟷ (A ∈ ℕ ⟶ θ(A))" by (rule MMI_syl)
from S15 have S16: "A ∈ ℕ ⟶ A ∈ ℕ ⟶ φ(A) ⟷ θ(A)" by (rule MMI_pm5_74rd)
from S16 have S17: "A ∈ ℕ ⟶ φ(A) ⟷ θ(A)" by (rule MMI_pm2_43i)
from S4 S17 have S18: "A ∈ ℕ ∧ z = A ⟶ φ(z) ⟷ θ(A)" by (rule MMI_sylan9bbr)
from S18 have S19: "z = A ⟶ A ∈ ℕ ⟶ φ(z) ⟷ θ(A)" by (rule MMI_expcom)
from S19 have S20: "z = A ⟶ (A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ θ(A))"
by (rule MMI_pm5_74d)
have S21: "A ∈ ℕ ⟶ (∀x. A ∈ ℕ)" by (rule MMI_ax_17)
from S21 have S22: "(A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ φ(z))" by auto
from S20 S22 have "z = A ⟶ (A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ θ(A))"
by (rule MMI_syl5bb)
} then have S23: "∀z. z = A ⟶ (A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ θ(A))"
by simp
have S24: "𝟭 ∈ ℕ" by (rule MMI_1nn)
from S24 have S25: "𝟭 = 𝟭" by simp
from S25 have S26: " ∃x. x = 𝟭" by (rule MMI_isseti)
from S25 have S27: "𝟭 = 𝟭" .
from S27 have S28: "φ(𝟭) ⟶ (∀x. φ(𝟭))" by simp
from A5 have S29: "ψ(𝟭)".
from A1 have S30: "∀ x. x = 𝟭 ⟶ φ(x) ⟷ ψ(𝟭)".
from S29 S30 have S31: "∀x. x = 𝟭 ⟶ φ(x)" by simp
have S32: "∀ x. x = 𝟭 ⟶ φ(x) ⟷ φ(𝟭)" by simp
from S31 S32 have S33: "∀x. x = 𝟭 ⟶ φ(𝟭)" by blast
from S28 S33 have S34: "( ∃x. x = 𝟭) ⟶ φ(𝟭)" by auto
from S26 S34 have S35: "φ(𝟭)" by (rule MMI_ax_mp)
from S35 have S36: "A ∈ ℕ ⟶ φ(𝟭)" by (rule MMI_a1i)
from S25 have S37: "𝟭 = 𝟭" .
have S38: "A ∈ ℕ ⟶ (∀x. A ∈ ℕ)" by (rule MMI_ax_17)
from S38 have S39: "𝟭 = 𝟭 ⟶ (A ∈ ℕ ⟶ φ(𝟭)) ⟷ (A ∈ ℕ ⟶ φ(𝟭))"
by simp
from S37 S39 have S40: "(A ∈ ℕ ⟶ φ(𝟭)) ⟷ (A ∈ ℕ ⟶ φ(𝟭))"
by (rule MMI_ax_mp)
from S36 S40 have S41: "(A ∈ ℕ ⟶ φ(𝟭))" by (rule MMI_mpbir)
{ fix y
from A6 have S42: "y ∈ ℕ ⟶ ch(y\<ca>𝟭)" by simp
have S43: "y \<ca> 𝟭 = y \<ca> 𝟭" by simp
from S43 have S44: " ∃x. x = y \<ca> 𝟭" by (rule MMI_isseti)
have S45: "ch(y\<ca>𝟭) ⟶ (∀x. ch(y\<ca>𝟭))" by (rule MMI_ax_17)
from S43 have S46: "y \<ca> 𝟭 = y \<ca> 𝟭" .
from S46 have S47: "φ(y \<ca> 𝟭) ⟶ (∀x. φ(y \<ca> 𝟭))" by simp
from S45 S47 have S48:
"(ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭)) ⟶ (∀x. ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭))" by simp
from A3 have S49: "∀x y. x = y \<ca> 𝟭 ⟶ φ(x) ⟷ ch(y\<ca>𝟭)".
have S50: "∀x. x = y \<ca> 𝟭 ⟶ φ(x) ⟷ φ(y \<ca> 𝟭)" by simp
from S49 S50 have S51: "∀ x. x = y \<ca> 𝟭 ⟶ ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭)"
by simp
from S48 S51 have S52: "( ∃x. x = y \<ca> 𝟭) ⟶ ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭)" by auto
from S44 S52 have S53: "ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭)" by (rule MMI_ax_mp)
from S42 S53 have S54: "y ∈ ℕ ⟶ φ(y \<ca> 𝟭)" by (rule MMI_sylib)
from S54 have S55: "y ∈ ℕ ⟶ A ∈ ℕ ⟶ φ(y \<ca> 𝟭)" by (rule MMI_a1d)
from S43 have S56: "y \<ca> 𝟭 = y \<ca> 𝟭" .
have S57: "A ∈ ℕ ⟶ (∀x. A ∈ ℕ)" by (rule MMI_ax_17)
from S57 have S58: "y \<ca> 𝟭 = y \<ca> 𝟭 ⟶ (A ∈ ℕ ⟶ φ(y \<ca> 𝟭)) ⟷
(A ∈ ℕ ⟶ φ(y \<ca> 𝟭))" by simp
from S56 S58 have S59: "(A ∈ ℕ ⟶ φ(y \<ca> 𝟭)) ⟷ (A ∈ ℕ ⟶ φ(y \<ca> 𝟭))"
by (rule MMI_ax_mp)
from S55 S59 have S60: "y ∈ ℕ ⟶ (A ∈ ℕ ⟶ φ(y \<ca> 𝟭))" by (rule MMI_sylibr)
from S60 have S61: "y ∈ ℕ ⟶ (A ∈ ℕ ⟶ φ(y)) ⟶ (A ∈ ℕ ⟶ φ(y \<ca> 𝟭))" by (rule MMI_a1d)
} then have S61: "∀y. y ∈ ℕ ⟶ (A ∈ ℕ ⟶ φ(y)) ⟶ (A ∈ ℕ ⟶ φ(y \<ca> 𝟭))"
by simp
from S1 S2 S3 S23 S41 S61 have S62: "A ∈ ℕ ⟶ A ∈ ℕ ⟶ θ(A)" by (rule MMI_nnind)
from S62 show "A ∈ ℕ ⟶ θ(A)" by (rule MMI_pm2_43i)
qed
lemma (in MMIsar0) MMI_nnaddclt:
shows "A ∈ ℕ ∧ B ∈ ℕ ⟶ A \<ca> B ∈ ℕ"
proof -
{ fix x
have S1: "x = 𝟭 ⟶ A \<ca> x = A \<ca> 𝟭" by (rule MMI_opreq2)
from S1 have S2: "x = 𝟭 ⟶
A \<ca> x ∈ ℕ ⟷ A \<ca> 𝟭 ∈ ℕ" by (rule MMI_eleq1d)
from S2 have "x = 𝟭 ⟶
(A ∈ ℕ ⟶ A \<ca> x ∈ ℕ) ⟷
(A ∈ ℕ ⟶ A \<ca> 𝟭 ∈ ℕ)" by (rule MMI_imbi2d)
} then have S3: "∀x. x = 𝟭 ⟶
(A ∈ ℕ ⟶ A \<ca> x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A \<ca> 𝟭 ∈ ℕ)"
by simp
{ fix x y
have S4: "x = y ⟶ A \<ca> x = A \<ca> y" by (rule MMI_opreq2)
from S4 have S5: "x = y ⟶
A \<ca> x ∈ ℕ ⟷ A \<ca> y ∈ ℕ" by (rule MMI_eleq1d)
from S5 have "x = y ⟶
(A ∈ ℕ ⟶ A \<ca> x ∈ ℕ) ⟷
(A ∈ ℕ ⟶ A \<ca> y ∈ ℕ)" by (rule MMI_imbi2d)
} then have S6: "∀x y. x = y ⟶
(A ∈ ℕ ⟶ A \<ca> x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A \<ca> y ∈ ℕ)"
by simp
{ fix x y
have S7: "x = y \<ca> 𝟭 ⟶
A \<ca> x = A \<ca> (y \<ca> 𝟭)" by (rule MMI_opreq2)
from S7 have S8: "x = y \<ca> 𝟭 ⟶
A \<ca> x ∈ ℕ ⟷
A \<ca> (y \<ca> 𝟭) ∈ ℕ" by (rule MMI_eleq1d)
from S8 have "x = y \<ca> 𝟭 ⟶
(A ∈ ℕ ⟶ A \<ca> x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A \<ca> (y \<ca> 𝟭) ∈ ℕ)"
by (rule MMI_imbi2d)
} then have S9: "∀x y. x = y \<ca> 𝟭 ⟶
(A ∈ ℕ ⟶ A \<ca> x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A \<ca> (y \<ca> 𝟭) ∈ ℕ)"
by simp
{ fix x
have S10: "x = B ⟶ A \<ca> x = A \<ca> B" by (rule MMI_opreq2)
from S10 have S11: "x = B ⟶
A \<ca> x ∈ ℕ ⟷ A \<ca> B ∈ ℕ" by (rule MMI_eleq1d)
from S11 have "x = B ⟶
(A ∈ ℕ ⟶ A \<ca> x ∈ ℕ) ⟷
(A ∈ ℕ ⟶ A \<ca> B ∈ ℕ)" by (rule MMI_imbi2d)
} then have S12: "∀x. x = B ⟶
(A ∈ ℕ ⟶ A \<ca> x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A \<ca> B ∈ ℕ)"
by simp
have S13: "A ∈ ℕ ⟶ A \<ca> 𝟭 ∈ ℕ" by (rule MMI_peano2nn)
have S14: "𝟭 ∈ ℂ" by (rule MMI_1cn)
{ fix y
have S15: "A ∈ ℂ ∧ y ∈ ℂ ∧ 𝟭 ∈ ℂ ⟶
A \<ca> y \<ca> 𝟭 = A \<ca> (y \<ca> 𝟭)" by (rule MMI_axaddass)
from S14 S15 have S16: "A ∈ ℂ ∧ y ∈ ℂ ⟶
A \<ca> y \<ca> 𝟭 = A \<ca> (y \<ca> 𝟭)" by (rule MMI_mp3an3)
have S17: "A ∈ ℕ ⟶ A ∈ ℂ" by (rule MMI_nncnt)
have S18: "y ∈ ℕ ⟶ y ∈ ℂ" by (rule MMI_nncnt)
from S16 S17 S18 have S19: "A ∈ ℕ ∧ y ∈ ℕ ⟶
A \<ca> y \<ca> 𝟭 = A \<ca> (y \<ca> 𝟭)" by (rule MMI_syl2an)
from S19 have S20: "A ∈ ℕ ∧ y ∈ ℕ ⟶
A \<ca> y \<ca> 𝟭 ∈ ℕ ⟷
A \<ca> (y \<ca> 𝟭) ∈ ℕ" by (rule MMI_eleq1d)
have S21: "A \<ca> y ∈ ℕ ⟶
A \<ca> y \<ca> 𝟭 ∈ ℕ" by (rule MMI_peano2nn)
from S20 S21 have S22: "A ∈ ℕ ∧ y ∈ ℕ ⟶
A \<ca> y ∈ ℕ ⟶
A \<ca> (y \<ca> 𝟭) ∈ ℕ" by (rule MMI_syl5bi)
from S22 have S23: "y ∈ ℕ ⟶
A ∈ ℕ ⟶
A \<ca> y ∈ ℕ ⟶
A \<ca> (y \<ca> 𝟭) ∈ ℕ" by (rule MMI_expcom)
from S23 have "y ∈ ℕ ⟶
(A ∈ ℕ ⟶ A \<ca> y ∈ ℕ) ⟶ A ∈ ℕ ⟶ A \<ca> (y \<ca> 𝟭) ∈ ℕ"
by (rule MMI_a2d)
} then have S24: "∀y. y ∈ ℕ ⟶
(A ∈ ℕ ⟶ A \<ca> y ∈ ℕ) ⟶ A ∈ ℕ ⟶ A \<ca> (y \<ca> 𝟭) ∈ ℕ"
by simp
from S3 S6 S9 S12 S13 S24 have S25: "B ∈ ℕ ⟶
A ∈ ℕ ⟶ A \<ca> B ∈ ℕ" by (rule MMI_nnind)
from S25 show "A ∈ ℕ ∧ B ∈ ℕ ⟶ A \<ca> B ∈ ℕ" by (rule MMI_impcom)
qed
lemma (in MMIsar0) MMI_nnmulclt:
shows "A ∈ ℕ ∧ B ∈ ℕ ⟶ A⋅B ∈ ℕ"
proof -
{ fix x
have S1: "x = 𝟭 ⟶ A⋅x = A⋅𝟭" by (rule MMI_opreq2)
from S1 have S2: "x = 𝟭 ⟶
A⋅x ∈ ℕ ⟷ A⋅𝟭 ∈ ℕ" by (rule MMI_eleq1d)
from S2 have "x = 𝟭 ⟶
(A ∈ ℕ ⟶ A⋅x ∈ ℕ) ⟷
(A ∈ ℕ ⟶ A⋅𝟭 ∈ ℕ)" by (rule MMI_imbi2d)
} then have S3: "∀ x. x = 𝟭 ⟶
(A ∈ ℕ ⟶ A⋅x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A⋅𝟭 ∈ ℕ)"
by simp
{ fix x y
have S4: "x = y ⟶ A⋅x = A⋅y" by (rule MMI_opreq2)
from S4 have S5: "x = y ⟶
A⋅x ∈ ℕ ⟷ A⋅y ∈ ℕ" by (rule MMI_eleq1d)
from S5 have "x = y ⟶
(A ∈ ℕ ⟶ A⋅x ∈ ℕ) ⟷
(A ∈ ℕ ⟶ A⋅y ∈ ℕ)" by (rule MMI_imbi2d)
} then have S6: "∀x y. x = y ⟶
(A ∈ ℕ ⟶ A⋅x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A⋅y ∈ ℕ)"
by simp
{fix x y
have S7: "x = y \<ca> 𝟭 ⟶
A⋅x = A⋅(y \<ca> 𝟭)" by (rule MMI_opreq2)
from S7 have S8: "x = y \<ca> 𝟭 ⟶
A⋅x ∈ ℕ ⟷
A⋅(y \<ca> 𝟭) ∈ ℕ" by (rule MMI_eleq1d)
from S8 have "x = y \<ca> 𝟭 ⟶
(A ∈ ℕ ⟶ A⋅x ∈ ℕ) ⟷
(A ∈ ℕ ⟶
A⋅(y \<ca> 𝟭) ∈ ℕ)" by (rule MMI_imbi2d)
} then have S9: "∀ x y. x = y \<ca> 𝟭 ⟶
(A ∈ ℕ ⟶ A⋅x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A⋅(y \<ca> 𝟭) ∈ ℕ)"
by simp
{ fix x
have S10: "x = B ⟶ A⋅x = A⋅B" by (rule MMI_opreq2)
from S10 have S11: "x = B ⟶
A⋅x ∈ ℕ ⟷ A⋅B ∈ ℕ" by (rule MMI_eleq1d)
from S11 have "x = B ⟶
(A ∈ ℕ ⟶ A⋅x ∈ ℕ) ⟷
(A ∈ ℕ ⟶ A⋅B ∈ ℕ)" by (rule MMI_imbi2d)
} then have S12: "∀ x. x = B ⟶
(A ∈ ℕ ⟶ A⋅x ∈ ℕ) ⟷ (A ∈ ℕ ⟶ A⋅B ∈ ℕ)"
by simp
have S13: "A ∈ ℕ ⟶ A ∈ ℂ" by (rule MMI_nncnt)
have S14: "A ∈ ℂ ⟶ A⋅𝟭 = A" by (rule MMI_ax1id)
from S14 have S15: "A ∈ ℂ ⟶
A⋅𝟭 ∈ ℕ ⟷ A ∈ ℕ" by (rule MMI_eleq1d)
from S15 have S16: "A ∈ ℂ ⟶
A ∈ ℕ ⟶ A⋅𝟭 ∈ ℕ" by (rule MMI_biimprd)
from S13 S16 have S17: "A ∈ ℕ ⟶ A⋅𝟭 ∈ ℕ" by (rule MMI_mpcom)
have S18: "𝟭 ∈ ℂ" by (rule MMI_1cn)
{ fix y
have S19: "A ∈ ℂ ∧ y ∈ ℂ ∧ 𝟭 ∈ ℂ ⟶
A⋅(y \<ca> 𝟭) = A⋅y \<ca> A⋅𝟭" by (rule MMI_axdistr)
from S18 S19 have S20: "A ∈ ℂ ∧ y ∈ ℂ ⟶
A⋅(y \<ca> 𝟭) = A⋅y \<ca> A⋅𝟭" by (rule MMI_mp3an3)
from S14 have S21: "A ∈ ℂ ⟶ A⋅𝟭 = A" .
from S21 have S22: "A ∈ ℂ ⟶
A⋅y \<ca> A⋅𝟭 = A⋅y \<ca> A" by (rule MMI_opreq2d)
from S22 have S23: "A ∈ ℂ ∧ y ∈ ℂ ⟶
A⋅y \<ca> A⋅𝟭 = A⋅y \<ca> A" by (rule MMI_adantr)
from S20 S23 have S24: "A ∈ ℂ ∧ y ∈ ℂ ⟶
A⋅(y \<ca> 𝟭) = A⋅y \<ca> A" by (rule MMI_eqtrd)
from S13 have S25: "A ∈ ℕ ⟶ A ∈ ℂ" .
have S26: "y ∈ ℕ ⟶ y ∈ ℂ" by (rule MMI_nncnt)
from S24 S25 S26 have S27: "A ∈ ℕ ∧ y ∈ ℕ ⟶
A⋅(y \<ca> 𝟭) = A⋅y \<ca> A" by (rule MMI_syl2an)
from S27 have S28: "A ∈ ℕ ∧ y ∈ ℕ ⟶
A⋅(y \<ca> 𝟭) ∈ ℕ ⟷ A⋅y \<ca> A ∈ ℕ" by (rule MMI_eleq1d)
have S29: "A⋅y ∈ ℕ ∧ A ∈ ℕ ⟶ A⋅y \<ca> A ∈ ℕ" by (rule MMI_nnaddclt)
from S29 have S30: "A ∈ ℕ ∧ A⋅y ∈ ℕ ⟶ A⋅y \<ca> A ∈ ℕ" by (rule MMI_ancoms)
from S28 S30 have S31: "A ∈ ℕ ∧ y ∈ ℕ ⟶
A ∈ ℕ ∧ A⋅y ∈ ℕ ⟶
A⋅(y \<ca> 𝟭) ∈ ℕ" by (rule MMI_syl5bir)
from S31 have S32: "A ∈ ℕ ⟶
y ∈ ℕ ⟶
A ∈ ℕ ⟶
A⋅y ∈ ℕ ⟶
A⋅(y \<ca> 𝟭) ∈ ℕ" by (rule MMI_exp4b)
from S32 have S33: "y ∈ ℕ ⟶
A ∈ ℕ ⟶
A⋅y ∈ ℕ ⟶
A⋅(y \<ca> 𝟭) ∈ ℕ" by (rule MMI_pm2_43b)
from S33 have "y ∈ ℕ ⟶
(A ∈ ℕ ⟶ A⋅y ∈ ℕ) ⟶ A ∈ ℕ ⟶ A⋅(y \<ca> 𝟭) ∈ ℕ" by (rule MMI_a2d)
} then have S34: "∀ y. y ∈ ℕ ⟶
(A ∈ ℕ ⟶ A⋅y ∈ ℕ) ⟶ A ∈ ℕ ⟶ A⋅(y \<ca> 𝟭) ∈ ℕ"
by simp
from S3 S6 S9 S12 S17 S34 have S35: "B ∈ ℕ ⟶
A ∈ ℕ ⟶ A⋅B ∈ ℕ" by (rule MMI_nnind)
from S35 show "A ∈ ℕ ∧ B ∈ ℕ ⟶ A⋅B ∈ ℕ" by (rule MMI_impcom)
qed
lemma (in MMIsar0) MMI_nn2get:
shows "A ∈ ℕ ∧ B ∈ ℕ ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)"
proof -
have S1: "A ∈ ℝ ∧ B ∈ ℝ ⟶ A \<lsq> B ∨ B \<lsq> A" by (rule MMI_letrit)
have S2: "A ∈ ℕ ⟶ A ∈ ℝ" by (rule MMI_nnret)
have S3: "B ∈ ℕ ⟶ B ∈ ℝ" by (rule MMI_nnret)
from S1 S2 S3 have S4: "A ∈ ℕ ∧ B ∈ ℕ ⟶ A \<lsq> B ∨ B \<lsq> A" by (rule MMI_syl2an)
from S3 have S5: "B ∈ ℕ ⟶ B ∈ ℝ" .
have S6: "B ∈ ℝ ⟶ B \<lsq> B" by (rule MMI_leidt)
from S6 have S7: "B ∈ ℝ ⟶
A \<lsq> B ⟷ A \<lsq> B ∧ B \<lsq> B" by (rule MMI_biantrud)
from S7 have S8: "B ∈ ℝ ⟶
A \<lsq> B ⟶ A \<lsq> B ∧ B \<lsq> B" by (rule MMI_biimpd)
from S5 S8 have S9: "B ∈ ℕ ⟶
A \<lsq> B ⟶ A \<lsq> B ∧ B \<lsq> B" by (rule MMI_syl)
from S9 have S10: "B ∈ ℕ ⟶
A \<lsq> B ⟶
B ∈ ℕ ∧ A \<lsq> B ∧ B \<lsq> B" by (rule MMI_anc2li)
have S11: "x = B ⟶
A \<lsq> x ⟷ A \<lsq> B" by (rule MMI_breq2)
have S12: "x = B ⟶
B \<lsq> x ⟷ B \<lsq> B" by (rule MMI_breq2)
from S11 S12 have S13: "x = B ⟶
A \<lsq> x ∧ B \<lsq> x ⟷ A \<lsq> B ∧ B \<lsq> B" by (rule MMI_anbi12d)
from S13 have S14: "B ∈ ℕ ∧ A \<lsq> B ∧ B \<lsq> B ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)" by auto
from S10 S14 have S15: "B ∈ ℕ ⟶
A \<lsq> B ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)" by (rule MMI_syl6)
from S15 have S16: "A ∈ ℕ ∧ B ∈ ℕ ⟶
A \<lsq> B ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)" by (rule MMI_adantl)
from S2 have S17: "A ∈ ℕ ⟶ A ∈ ℝ" .
have S18: "A ∈ ℝ ⟶ A \<lsq> A" by (rule MMI_leidt)
from S18 have S19: "A ∈ ℝ ⟶
B \<lsq> A ⟷ A \<lsq> A ∧ B \<lsq> A" by (rule MMI_biantrurd)
from S19 have S20: "A ∈ ℝ ⟶
B \<lsq> A ⟶ A \<lsq> A ∧ B \<lsq> A" by (rule MMI_biimpd)
from S17 S20 have S21: "A ∈ ℕ ⟶
B \<lsq> A ⟶ A \<lsq> A ∧ B \<lsq> A" by (rule MMI_syl)
from S21 have S22: "A ∈ ℕ ⟶
B \<lsq> A ⟶
A ∈ ℕ ∧ A \<lsq> A ∧ B \<lsq> A" by (rule MMI_anc2li)
have S23: "x = A ⟶
A \<lsq> x ⟷ A \<lsq> A" by (rule MMI_breq2)
have S24: "x = A ⟶
B \<lsq> x ⟷ B \<lsq> A" by (rule MMI_breq2)
from S23 S24 have S25: "x = A ⟶
A \<lsq> x ∧ B \<lsq> x ⟷ A \<lsq> A ∧ B \<lsq> A" by (rule MMI_anbi12d)
from S25 have S26: "A ∈ ℕ ∧ A \<lsq> A ∧ B \<lsq> A ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)" by auto
from S22 S26 have S27: "A ∈ ℕ ⟶
B \<lsq> A ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)" by (rule MMI_syl6)
from S27 have S28: "A ∈ ℕ ∧ B ∈ ℕ ⟶
B \<lsq> A ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)" by (rule MMI_adantr)
from S16 S28 have S29: "A ∈ ℕ ∧ B ∈ ℕ ⟶
A \<lsq> B ∨ B \<lsq> A ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)" by (rule MMI_jaod)
from S4 S29 show "A ∈ ℕ ∧ B ∈ ℕ ⟶
( ∃x∈ℕ. A \<lsq> x ∧ B \<lsq> x)" by (rule MMI_mpd)
qed
lemma (in MMIsar0) MMI_nnge1t:
shows "A ∈ ℕ ⟶ 𝟭 \<lsq> A"
proof -
{fix x
have "x = 𝟭 ⟶
𝟭 \<lsq> x ⟷ 𝟭 \<lsq> 𝟭" by (rule MMI_breq2)
} then have S1: "∀ x. x = 𝟭 ⟶ 𝟭 \<lsq> x ⟷ 𝟭 \<lsq> 𝟭"
by simp
{ fix x y
have "x = y ⟶
𝟭 \<lsq> x ⟷ 𝟭 \<lsq> y" by (rule MMI_breq2)
} then have S2: "∀x y. x = y ⟶ 𝟭 \<lsq> x ⟷ 𝟭 \<lsq> y"
by simp
{ fix x y
have "x = y \<ca> 𝟭 ⟶
𝟭 \<lsq> x ⟷ 𝟭 \<lsq> y \<ca> 𝟭" by (rule MMI_breq2)
} then have S3:
"∀x y. x = y \<ca> 𝟭 ⟶ 𝟭 \<lsq> x ⟷ 𝟭 \<lsq> y \<ca> 𝟭"
by simp
{ fix x
have "x = A ⟶
𝟭 \<lsq> x ⟷ 𝟭 \<lsq> A" by (rule MMI_breq2)
} then have S4: "∀ x. x = A ⟶ 𝟭 \<lsq> x ⟷ 𝟭 \<lsq> A"
by simp
have S5: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
from S5 have S6: "𝟭 \<lsq> 𝟭" by (rule MMI_leid)
{ fix y
have S7: "y ∈ ℕ ⟶ y ∈ ℝ" by (rule MMI_nnret)
have S8: "y ∈ ℝ ⟶ y ∈ ℂ" by (rule MMI_recnt)
have S9: "y ∈ ℂ ⟶ y \<ca> 𝟬 = y" by (rule MMI_ax0id)
from S8 S9 have S10: "y ∈ ℝ ⟶ y \<ca> 𝟬 = y" by (rule MMI_syl)
from S10 have S11: "y ∈ ℝ ⟶
𝟭 \<lsq> y \<ca> 𝟬 ⟷ 𝟭 \<lsq> y" by (rule MMI_breq2d)
have S12: "𝟬 \<ls> 𝟭" by (rule MMI_lt01)
have S13: "𝟬 ∈ ℝ" by (rule MMI_0re)
have S14: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
have S15: "𝟬 ∈ ℝ ∧ 𝟭 ∈ ℝ ∧ y ∈ ℝ ⟶
𝟬 \<ls> 𝟭 ⟶
y \<ca> 𝟬 \<ls> y \<ca> 𝟭" by (rule MMI_axltadd)
from S13 S14 S15 have S16: "y ∈ ℝ ⟶
𝟬 \<ls> 𝟭 ⟶
y \<ca> 𝟬 \<ls> y \<ca> 𝟭" by (rule MMI_mp3an12)
from S12 S16 have S17: "y ∈ ℝ ⟶
y \<ca> 𝟬 \<ls> y \<ca> 𝟭" by (rule MMI_mpi)
have S18: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
have S19: "y \<ca> 𝟬 ∈ ℝ ∧ y \<ca> 𝟭 ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶
y \<ca> 𝟬 \<ls> y \<ca> 𝟭 ∧ y \<ca> 𝟭 \<ls> 𝟭 ⟶ y \<ca> 𝟬 \<ls> 𝟭" by (rule MMI_axlttrn)
from S18 S19 have S20: "y \<ca> 𝟬 ∈ ℝ ∧ y \<ca> 𝟭 ∈ ℝ ⟶
y \<ca> 𝟬 \<ls> y \<ca> 𝟭 ∧ y \<ca> 𝟭 \<ls> 𝟭 ⟶ y \<ca> 𝟬 \<ls> 𝟭" by (rule MMI_mp3an3)
have S21: "𝟬 ∈ ℝ" by (rule MMI_0re)
have S22: "y ∈ ℝ ∧ 𝟬 ∈ ℝ ⟶ y \<ca> 𝟬 ∈ ℝ" by (rule MMI_axaddrcl)
from S21 S22 have S23: "y ∈ ℝ ⟶ y \<ca> 𝟬 ∈ ℝ" by (rule MMI_mpan2)
have S24: "y ∈ ℝ ⟶ y \<ca> 𝟭 ∈ ℝ" by (rule MMI_peano2re)
from S20 S23 S24 have S25: "y ∈ ℝ ⟶
y \<ca> 𝟬 \<ls> y \<ca> 𝟭 ∧ y \<ca> 𝟭 \<ls> 𝟭 ⟶ y \<ca> 𝟬 \<ls> 𝟭" by (rule MMI_sylanc)
from S17 S25 have S26: "y ∈ ℝ ⟶
y \<ca> 𝟭 \<ls> 𝟭 ⟶ y \<ca> 𝟬 \<ls> 𝟭" by (rule MMI_mpand)
from S26 have S27: "y ∈ ℝ ⟶
¬(y \<ca> 𝟬 \<ls> 𝟭) ⟶
¬(y \<ca> 𝟭 \<ls> 𝟭)" by (rule MMI_con3d)
from S23 have S28: "y ∈ ℝ ⟶ y \<ca> 𝟬 ∈ ℝ" .
have S29: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
from S28 S29 have S30: "y ∈ ℝ ⟶
𝟭 ∈ ℝ ∧ y \<ca> 𝟬 ∈ ℝ" by (rule MMI_jctil)
have S31: "𝟭 ∈ ℝ ∧ y \<ca> 𝟬 ∈ ℝ ⟶
𝟭 \<lsq> y \<ca> 𝟬 ⟷
¬(y \<ca> 𝟬 \<ls> 𝟭)" by (rule MMI_lenltt)
from S30 S31 have S32: "y ∈ ℝ ⟶
𝟭 \<lsq> y \<ca> 𝟬 ⟷
¬(y \<ca> 𝟬 \<ls> 𝟭)" by (rule MMI_syl)
from S24 have S33: "y ∈ ℝ ⟶ y \<ca> 𝟭 ∈ ℝ" .
have S34: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
from S33 S34 have S35: "y ∈ ℝ ⟶
𝟭 ∈ ℝ ∧ y \<ca> 𝟭 ∈ ℝ" by (rule MMI_jctil)
have S36: "𝟭 ∈ ℝ ∧ y \<ca> 𝟭 ∈ ℝ ⟶
𝟭 \<lsq> y \<ca> 𝟭 ⟷
¬(y \<ca> 𝟭 \<ls> 𝟭)" by (rule MMI_lenltt)
from S35 S36 have S37: "y ∈ ℝ ⟶
𝟭 \<lsq> y \<ca> 𝟭 ⟷
¬(y \<ca> 𝟭 \<ls> 𝟭)" by (rule MMI_syl)
from S27 S32 S37 have S38: "y ∈ ℝ ⟶
𝟭 \<lsq> y \<ca> 𝟬 ⟶ 𝟭 \<lsq> y \<ca> 𝟭" by (rule MMI_3imtr4d)
from S11 S38 have S39: "y ∈ ℝ ⟶
𝟭 \<lsq> y ⟶ 𝟭 \<lsq> y \<ca> 𝟭" by (rule MMI_sylbird)
from S7 S39 have S40: "y ∈ ℕ ⟶
𝟭 \<lsq> y ⟶ 𝟭 \<lsq> y \<ca> 𝟭" by (rule MMI_syl)
} then have S40: "∀y. y ∈ ℕ ⟶ 𝟭 \<lsq> y ⟶ 𝟭 \<lsq> y \<ca> 𝟭"
by simp
from S1 S2 S3 S4 S6 S40 show "A ∈ ℕ ⟶ 𝟭 \<lsq> A" by (rule MMI_nnind)
qed
lemma (in MMIsar0) MMI_nngt1ne1t:
shows "A ∈ ℕ ⟶
𝟭 \<ls> A ⟷ ¬(A = 𝟭)"
proof -
have S1: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
have S2: "𝟭 ∈ ℝ ∧ A ∈ ℝ ∧ 𝟭 \<lsq> A ⟶
𝟭 \<ls> A ⟷ ¬(𝟭 = A)" by (rule MMI_leltnet)
from S1 S2 have S3: "A ∈ ℝ ∧ 𝟭 \<lsq> A ⟶
𝟭 \<ls> A ⟷ ¬(𝟭 = A)" by (rule MMI_mp3an1)
have S4: "A ∈ ℕ ⟶ A ∈ ℝ" by (rule MMI_nnret)
have S5: "A ∈ ℕ ⟶ 𝟭 \<lsq> A" by (rule MMI_nnge1t)
from S3 S4 S5 have S6: "A ∈ ℕ ⟶
𝟭 \<ls> A ⟷ ¬(𝟭 = A)" by (rule MMI_sylanc)
have S7: "𝟭 = A ⟷ A = 𝟭" by (rule MMI_eqcom)
from S7 have S8: "¬(𝟭 = A) ⟷ ¬(A = 𝟭)" by (rule MMI_negbii)
from S6 S8 show "A ∈ ℕ ⟶
𝟭 \<ls> A ⟷ ¬(A = 𝟭)" by (rule MMI_syl6bb)
qed
lemma (in MMIsar0) MMI_nnle1eq1t:
shows "A ∈ ℕ ⟶
A \<lsq> 𝟭 ⟷ A = 𝟭"
proof -
have S1: "A ∈ ℕ ⟶ 𝟭 \<lsq> A" by (rule MMI_nnge1t)
from S1 have S2: "A ∈ ℕ ⟶
A \<lsq> 𝟭 ⟷
A \<lsq> 𝟭 ∧ 𝟭 \<lsq> A" by (rule MMI_biantrud)
have S3: "A ∈ ℕ ⟶ A ∈ ℝ" by (rule MMI_nnret)
have S4: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
have S5: "A ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶
A = 𝟭 ⟷
A \<lsq> 𝟭 ∧ 𝟭 \<lsq> A" by (rule MMI_letri3t)
from S4 S5 have S6: "A ∈ ℝ ⟶
A = 𝟭 ⟷
A \<lsq> 𝟭 ∧ 𝟭 \<lsq> A" by (rule MMI_mpan2)
from S3 S6 have S7: "A ∈ ℕ ⟶
A = 𝟭 ⟷
A \<lsq> 𝟭 ∧ 𝟭 \<lsq> A" by (rule MMI_syl)
from S2 S7 show "A ∈ ℕ ⟶
A \<lsq> 𝟭 ⟷ A = 𝟭" by (rule MMI_bitr4d)
qed
lemma (in MMIsar0) MMI_nngt0t:
shows "A ∈ ℕ ⟶ 𝟬 \<ls> A"
proof -
have S1: "𝟬 \<ls> 𝟭" by (rule MMI_lt01)
have S2: "𝟬 ∈ ℝ" by (rule MMI_0re)
have S3: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
have S4: "𝟬 ∈ ℝ ∧ 𝟭 ∈ ℝ ∧ A ∈ ℝ ⟶
𝟬 \<ls> 𝟭 ∧ 𝟭 \<lsq> A ⟶ 𝟬 \<ls> A" by (rule MMI_ltletrt)
from S2 S3 S4 have S5: "A ∈ ℝ ⟶
𝟬 \<ls> 𝟭 ∧ 𝟭 \<lsq> A ⟶ 𝟬 \<ls> A" by (rule MMI_mp3an12)
from S1 S5 have S6: "A ∈ ℝ ⟶
𝟭 \<lsq> A ⟶ 𝟬 \<ls> A" by (rule MMI_mpani)
have S7: "A ∈ ℕ ⟶ A ∈ ℝ" by (rule MMI_nnret)
have S8: "A ∈ ℕ ⟶ 𝟭 \<lsq> A" by (rule MMI_nnge1t)
from S6 S7 S8 show "A ∈ ℕ ⟶ 𝟬 \<ls> A" by (rule MMI_sylc)
qed
lemma (in MMIsar0) MMI_lt1nnn:
shows "A ∈ ℝ ∧ A \<ls> 𝟭 ⟶ ¬(A ∈ ℕ)"
proof -
have S1: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
have S2: "A ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶
A \<ls> 𝟭 ⟷ ¬(𝟭 \<lsq> A)" by (rule MMI_ltnlet)
from S1 S2 have S3: "A ∈ ℝ ⟶
A \<ls> 𝟭 ⟷ ¬(𝟭 \<lsq> A)" by (rule MMI_mpan2)
have S4: "A ∈ ℕ ⟶ 𝟭 \<lsq> A" by (rule MMI_nnge1t)
from S4 have S5: "¬(𝟭 \<lsq> A) ⟶ ¬(A ∈ ℕ)" by (rule MMI_con3i)
from S3 S5 have S6: "A ∈ ℝ ⟶
A \<ls> 𝟭 ⟶ ¬(A ∈ ℕ)" by (rule MMI_syl6bi)
from S6 show "A ∈ ℝ ∧ A \<ls> 𝟭 ⟶ ¬(A ∈ ℕ)" by (rule MMI_imp)
qed
lemma (in MMIsar0) MMI_0nnn:
shows "¬(𝟬 ∈ ℕ)"
proof -
have S1: "𝟬 ∈ ℝ" by (rule MMI_0re)
have S2: "𝟬 \<ls> 𝟭" by (rule MMI_lt01)
have S3: "𝟬 ∈ ℝ ∧ 𝟬 \<ls> 𝟭 ⟶ ¬(𝟬 ∈ ℕ)" by (rule MMI_lt1nnn)
from S1 S2 S3 show "¬(𝟬 ∈ ℕ)" by (rule MMI_mp2an)
qed
lemma (in MMIsar0) MMI_nnne0t:
shows "A ∈ ℕ ⟶ A ≠ 𝟬"
proof -
have S1: "¬(𝟬 ∈ ℕ)" by (rule MMI_0nnn)
have S2: "A = 𝟬 ⟶
A ∈ ℕ ⟷ 𝟬 ∈ ℕ" by (rule MMI_eleq1)
from S1 S2 have S3: "A = 𝟬 ⟶ ¬(A ∈ ℕ)" by (rule MMI_mtbiri)
from S3 have S4: "A ∈ ℕ ⟶ ¬(A = 𝟬)" by (rule MMI_con2i)
have S5: "A ≠ 𝟬 ⟷ ¬(A = 𝟬)" by (rule MMI_df_ne)
from S4 S5 show "A ∈ ℕ ⟶ A ≠ 𝟬" by (rule MMI_sylibr)
qed
lemma (in MMIsar0) MMI_nngt0: assumes A1: "A ∈ ℕ"
shows "𝟬 \<ls> A"
proof -
from A1 have S1: "A ∈ ℕ".
have S2: "A ∈ ℕ ⟶ 𝟬 \<ls> A" by (rule MMI_nngt0t)
from S1 S2 show "𝟬 \<ls> A" by (rule MMI_ax_mp)
qed
lemma (in MMIsar0) MMI_nnne0: assumes A1: "A ∈ ℕ"
shows "A ≠ 𝟬"
proof -
from A1 have S1: "A ∈ ℕ".
from S1 have S2: "A ∈ ℝ" by (rule MMI_nnre)
from A1 have S3: "A ∈ ℕ".
from S3 have S4: "𝟬 \<ls> A" by (rule MMI_nngt0)
from S2 S4 show "A ≠ 𝟬" by (rule MMI_gt0ne0i)
qed
lemma (in MMIsar0) MMI_nnrecgt0t:
shows "A ∈ ℕ ⟶ 𝟬 \<ls> 𝟭\<cdiv>A"
proof -
have S1: "A ∈ ℕ ⟶ 𝟭 \<lsq> A" by (rule MMI_nnge1t)
have S2: "𝟬 \<ls> 𝟭" by (rule MMI_lt01)
have S3: "A ∈ ℕ ⟶ A ∈ ℝ" by (rule MMI_nnret)
have S4: "𝟬 ∈ ℝ" by (rule MMI_0re)
have S5: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
have S6: "𝟬 ∈ ℝ ∧ 𝟭 ∈ ℝ ∧ A ∈ ℝ ⟶
𝟬 \<ls> 𝟭 ∧ 𝟭 \<lsq> A ⟶ 𝟬 \<ls> A" by (rule MMI_ltletrt)
from S4 S5 S6 have S7: "A ∈ ℝ ⟶
𝟬 \<ls> 𝟭 ∧ 𝟭 \<lsq> A ⟶ 𝟬 \<ls> A" by (rule MMI_mp3an12)
have S8: "A ∈ ℝ ∧ 𝟬 \<ls> A ⟶ 𝟬 \<ls> 𝟭\<cdiv>A" by (rule MMI_recgt0t)
from S8 have S9: "A ∈ ℝ ⟶
𝟬 \<ls> A ⟶ 𝟬 \<ls> 𝟭\<cdiv>A" by (rule MMI_ex)
from S7 S9 have S10: "A ∈ ℝ ⟶
𝟬 \<ls> 𝟭 ∧ 𝟭 \<lsq> A ⟶ 𝟬 \<ls> 𝟭\<cdiv>A" by (rule MMI_syld)
from S3 S10 have S11: "A ∈ ℕ ⟶
𝟬 \<ls> 𝟭 ∧ 𝟭 \<lsq> A ⟶ 𝟬 \<ls> 𝟭\<cdiv>A" by (rule MMI_syl)
from S2 S11 have S12: "A ∈ ℕ ⟶
𝟭 \<lsq> A ⟶ 𝟬 \<ls> 𝟭\<cdiv>A" by (rule MMI_mpani)
from S1 S12 show "A ∈ ℕ ⟶ 𝟬 \<ls> 𝟭\<cdiv>A" by (rule MMI_mpd)
qed
text‹I am unable to translate the proof of Metamath's nnleltp1. Isabelle
chokes on a comlicated application of nn1suc. A couple of theorems below
are proven by hand in Isabelle to wokaround this.
In the next theorem we show that $a < a+1$.›
lemma (in MMIsar0) num_le_numplus1: assumes "a∈ℝ"
shows "a \<ls> a\<ca>𝟭"
using assms MMI_ax1re MMI_lt01 MMI_ltaddpos
by simp
text‹The next theorem
shows that of $a\leq b$, then $a< b+1$.›
lemma (in MMIsar0) lsq_imp_ls_plus1:
assumes A1: "a∈ℝ" "b∈ℝ" and A3: "a\<lsq>b"
shows "a \<ls> b\<ca>𝟭"
proof -
from A1 have "b \<ls> b\<ca>𝟭" using num_le_numplus1 by simp
with A1 A3 show "a \<ls> b\<ca>𝟭" using MMI_ax1re MMI_axaddrcl MMI_lelttr
by blast
qed
text‹There are no natural numbers between $1$ and $2$.›
lemma (in MMIsar0) no_nat_between12:
assumes A1: "n ∈ ℕ"
shows "n \<ls> 𝟭\<ca>𝟭 ⟶ n \<lsq> 𝟭"
proof -
have "𝟭 \<ls> 𝟭\<ca>𝟭 ⟶ 𝟭 \<lsq> 𝟭"
using MMI_1nn MMI_nnge1t by simp
moreover
{ fix k assume A2: "k∈ℕ"
{ assume A3: "k\<ca>𝟭 \<ls> 𝟭\<ca>𝟭"
from A2 MMI_ax1re have T: "k ∈ ℝ" "𝟭 ∈ ℝ"
using MMI_nnre by auto
with A3 have "k \<ls> 𝟭" using MMI_ltadd1 by blast
with T A2 have False using MMI_lt1nnn by simp
} then have "¬(k\<ca>𝟭 \<ls> 𝟭\<ca>𝟭)" by auto
hence
"(k \<ls> 𝟭\<ca>𝟭 ⟶ k \<lsq> 𝟭) ⟶ (k\<ca>𝟭 \<ls> 𝟭\<ca>𝟭 ⟶ k \<ca> 𝟭 \<lsq> 𝟭)"
by simp
} then have "∀k∈ℕ.
(k \<ls> 𝟭\<ca>𝟭 ⟶ k \<lsq> 𝟭) ⟶ (k\<ca>𝟭 \<ls> 𝟭\<ca>𝟭 ⟶ k \<ca> 𝟭 \<lsq> 𝟭)"
by simp
moreover note A1
ultimately show "n \<ls> 𝟭\<ca>𝟭 ⟶ n \<lsq> 𝟭"
by (rule nnind1)
qed
text‹Natural number greater than $1$ has a predecessor.›
lemma (in MMIsar0) nat_ge1_has_pred: assumes A1: "n ∈ ℕ"
shows "𝟭 \<ls> n ⟶ (∃j∈ℕ. n = j\<ca>𝟭)"
proof -
from MMI_ax1re have "¬(𝟭\<ls>𝟭)" using MMI_ltnr by simp
then have "𝟭 \<ls> 𝟭 ⟶ (∃j∈ℕ. 𝟭 = j\<ca>𝟭)" by simp
moreover
{ fix k assume A2: "k∈ℕ" and A3: "𝟭 \<ls> k ⟶ (∃j∈ℕ. k = j\<ca>𝟭)" and
A4: "𝟭 \<ls> k\<ca>𝟭"
from A2 have "k=𝟭 ∨ 𝟭\<ls>k" using MMI_nngt1ne1t by simp
moreover
{ assume "k=𝟭"
then have "𝟭∈ℕ" and "k\<ca>𝟭 = 𝟭\<ca>𝟭"
using MMI_1nn by auto
hence "∃i∈ℕ. k\<ca>𝟭 = i\<ca>𝟭" by auto }
moreover
{ assume "𝟭 \<ls> k"
with A3 obtain j where "j∈ℕ" and "k = j\<ca>𝟭"
by auto
then have "j\<ca>𝟭 ∈ ℕ" and "k\<ca>𝟭 = j\<ca>𝟭\<ca>𝟭"
using MMI_peano2nn by auto
then have "∃i∈ℕ. k\<ca>𝟭 = i\<ca>𝟭" by auto }
ultimately have "∃i∈ℕ. k\<ca>𝟭 = i\<ca>𝟭" by auto
} then have "∀k∈ℕ.
(𝟭 \<ls> k ⟶ (∃j∈ℕ. k = j\<ca>𝟭)) ⟶ (𝟭 \<ls> k\<ca>𝟭 ⟶ (∃i∈ℕ. k\<ca>𝟭 = i\<ca>𝟭))"
by auto
moreover note A1
ultimately show "𝟭 \<ls> n ⟶ (∃j∈ℕ. n = j\<ca>𝟭)"
by (rule nnind1)
qed
text‹If the successor is smaller, then the number is smaller.›
lemma (in MMIsar0) succ_le_imp_le: assumes A1: "a∈ℝ" "b∈ℝ" and A2: "a\<ca>𝟭 \<ls> b"
shows "a\<ls>b"
proof -
from A1 have T: "a∈ℝ" "a\<ca>𝟭 ∈ ℝ" "b∈ℝ"
using MMI_ax1re MMI_axaddrcl by auto
moreover from A1 A2 have
"a \<ls> a\<ca>𝟭" "a\<ca>𝟭 \<ls> b"
using num_le_numplus1 by auto
ultimately show "a\<ls>b" using MMI_axlttrn by blast
qed
text‹For natural numbers greater numbers can be obtained by adding a natural number.›
lemma (in MMIsar0) nat_ge_repr: assumes A1: "n ∈ ℕ" "m ∈ ℕ"
shows "m\<ls>n ⟶ (∃j∈ℕ. n = m \<ca> j)"
proof -
{ assume "𝟭 \<ls> n"
with A1 obtain k where I: "k∈ℕ" and II: "n = k\<ca>𝟭"
using nat_ge1_has_pred by auto
with MMI_axaddcom MMI_ax1re MMI_axresscn have "k ∈ ℂ" and "𝟭 ∈ ℂ"
using MMI_nncn by auto
with MMI_axaddcom I II have "∃k∈ℕ. n = 𝟭 \<ca> k"
by auto
} then have "𝟭 \<ls> n ⟶ (∃j∈ℕ. n = 𝟭 \<ca> j)" by simp
moreover
{ fix k assume A2: "k∈ℕ" and
A3: "k\<ls>n ⟶ (∃j∈ℕ. n = k \<ca> j)" and A4: "k\<ca>𝟭 \<ls> n"
from A1 A2 have T: "n∈ℝ" "k∈ℝ" using MMI_nnre by auto
with A3 A4 obtain j where III: "j∈ℕ" and IV: "n = k \<ca> j"
using succ_le_imp_le by auto
with A4 T III MMI_ax1re have "𝟭 \<ls> j"
using MMI_nnre MMI_ltadd2 by blast
with III obtain i where V: "i∈ℕ" and VI: "j = i\<ca>𝟭"
using nat_ge1_has_pred by auto
with IV have "n = k \<ca> (i\<ca>𝟭)" by simp
moreover from V MMI_ax1re MMI_axresscn MMI_axaddcom have
"k \<ca> (i\<ca>𝟭) = k \<ca> (𝟭\<ca>i)"
using MMI_nncn by auto
moreover from T V MMI_ax1re MMI_axresscn MMI_axaddass have
"k \<ca> 𝟭\<ca>i = k \<ca> (𝟭\<ca>i)"
using MMI_nncn by blast
ultimately have "n = k \<ca> 𝟭\<ca>i" by simp
with V have "∃i∈ℕ. n = k\<ca>𝟭 \<ca> i" by auto
} then have "∀k∈ℕ. (k\<ls>n ⟶ (∃j∈ℕ. n = k \<ca> j)) ⟶
(k\<ca>𝟭 \<ls> n ⟶ (∃i∈ℕ. n = k\<ca>𝟭 \<ca> i))" by simp
moreover from A1 have "m ∈ ℕ" by simp
ultimately show "m\<ls>n ⟶ (∃j∈ℕ. n = m \<ca> j)"
by (rule nnind1)
qed
text‹In natural numbers less $a+1$ implies less or equal $a$.›
lemma (in MMIsar0) nat_ls_plus_one_imp_lsq:
assumes A1: "n ∈ ℕ" "m ∈ ℕ" and A2: "n \<ls> m\<ca>𝟭"
shows "n \<lsq> m"
proof -
from MMI_1cn A1 have T: "m ∈ ℂ" "n ∈ ℂ" "𝟭 ∈ ℂ"
using MMI_nncn by auto
from A1 have "m\<ca>𝟭 ∈ ℕ" using MMI_peano2nn by simp
with A1 A2 obtain k where I: "k∈ℕ" and II: "m\<ca>𝟭 = n\<ca>k"
using nat_ge_repr by auto
then have "k = 𝟭 ∨ 𝟭\<ls>k" using MMI_nngt1ne1t by auto
moreover
{ assume "k=𝟭"
with II T have "m = n" using MMI_addcan2 by simp }
moreover
{ assume "𝟭\<ls>k"
with I obtain i where III: "i∈ℕ" and IV: "k = i\<ca>𝟭"
using nat_ge1_has_pred by auto
with A1 II III have "m\<ca>𝟭 = n\<ca>i \<ca> 𝟭"
using MMI_nncn MMI_1cn MMI_axaddass by simp
with MMI_axaddcl T III have "m = n\<ca>i" using MMI_nncn MMI_addcan2
by auto
moreover from A1 III have "n∈ℝ" "i∈ℝ" "𝟬 \<ls> i"
using MMI_nnre MMI_nngt0t by auto
ultimately have "n \<ls> m" using MMI_ltaddpost by auto }
ultimately have "n=m ∨ n \<ls> m" by auto
with A1 show "n \<lsq> m" using MMI_nnre MMI_leloet by auto
qed
text‹The next theorem is the reason we proved the theorems above
(see the comment to ‹num_le_numplus1›.›
lemma (in MMIsar0) MMI_nnleltp1t:
shows "A ∈ ℕ ∧ B ∈ ℕ ⟶ A \<lsq> B ⟷ A \<ls> B \<ca> 𝟭"
proof
assume A1: "A ∈ ℕ ∧ B ∈ ℕ"
then have "A \<lsq> B ⟶ A \<ls> B \<ca> 𝟭"
using MMI_nnre lsq_imp_ls_plus1 by simp
moreover from A1 have "A \<ls> B \<ca> 𝟭 ⟶ A \<lsq> B"
using nat_ls_plus_one_imp_lsq by simp
ultimately show "A \<lsq> B ⟷ A \<ls> B \<ca> 𝟭"
by blast
qed
lemma (in MMIsar0) MMI_nnltp1let:
shows "A ∈ ℕ ∧ B ∈ ℕ ⟶
A \<ls> B ⟷ A \<ca> 𝟭 \<lsq> B"
proof -
have S1: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
have S2: "A ∈ ℝ ∧ B ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶
A \<ls> B ⟷
A \<ca> 𝟭 \<ls> B \<ca> 𝟭" by (rule MMI_ltadd1t)
from S1 S2 have S3: "A ∈ ℝ ∧ B ∈ ℝ ⟶
A \<ls> B ⟷
A \<ca> 𝟭 \<ls> B \<ca> 𝟭" by (rule MMI_mp3an3)
have S4: "A ∈ ℕ ⟶ A ∈ ℝ" by (rule MMI_nnret)
have S5: "B ∈ ℕ ⟶ B ∈ ℝ" by (rule MMI_nnret)
from S3 S4 S5 have S6: "A ∈ ℕ ∧ B ∈ ℕ ⟶
A \<ls> B ⟷
A \<ca> 𝟭 \<ls> B \<ca> 𝟭" by (rule MMI_syl2an)
have S7: "A \<ca> 𝟭 ∈ ℕ ∧ B ∈ ℕ ⟶
A \<ca> 𝟭 \<lsq> B ⟷
A \<ca> 𝟭 \<ls> B \<ca> 𝟭" by (rule MMI_nnleltp1t)
have S8: "A ∈ ℕ ⟶ A \<ca> 𝟭 ∈ ℕ" by (rule MMI_peano2nn)
from S7 S8 have S9: "A ∈ ℕ ∧ B ∈ ℕ ⟶
A \<ca> 𝟭 \<lsq> B ⟷
A \<ca> 𝟭 \<ls> B \<ca> 𝟭" by (rule MMI_sylan)
from S6 S9 show "A ∈ ℕ ∧ B ∈ ℕ ⟶
A \<ls> B ⟷ A \<ca> 𝟭 \<lsq> B" by (rule MMI_bitr4d)
qed
lemma (in MMIsar0) MMI_nnsub: assumes A1: "A ∈ ℕ" and
A2: "B ∈ ℕ"
shows "A \<ls> B ⟷ B \<cs> A ∈ ℕ"
proof -
from A2 have S1: "B ∈ ℕ".
{ fix x
have S2: "x = 𝟭 ⟶
A \<ls> x ⟷ A \<ls> 𝟭" by (rule MMI_breq2)
have S3: "x = 𝟭 ⟶ x \<cs> A = 𝟭 \<cs> A" by (rule MMI_opreq1)
from S3 have S4: "x = 𝟭 ⟶
x \<cs> A ∈ ℕ ⟷ 𝟭 \<cs> A ∈ ℕ" by (rule MMI_eleq1d)
from S2 S4 have "x = 𝟭 ⟶
(A \<ls> x ⟶ x \<cs> A ∈ ℕ) ⟷
(A \<ls> 𝟭 ⟶ 𝟭 \<cs> A ∈ ℕ)" by (rule MMI_imbi12d)
} then have S5: "∀ x. x = 𝟭 ⟶
(A \<ls> x ⟶ x \<cs> A ∈ ℕ) ⟷ (A \<ls> 𝟭 ⟶ 𝟭 \<cs> A ∈ ℕ)"
by simp
{ fix x y
have S6: "x = y ⟶
A \<ls> x ⟷ A \<ls> y" by (rule MMI_breq2)
have S7: "x = y ⟶ x \<cs> A = y \<cs> A" by (rule MMI_opreq1)
from S7 have S8: "x = y ⟶
x \<cs> A ∈ ℕ ⟷ y \<cs> A ∈ ℕ" by (rule MMI_eleq1d)
from S6 S8 have "x = y ⟶
(A \<ls> x ⟶ x \<cs> A ∈ ℕ) ⟷
(A \<ls> y ⟶ y \<cs> A ∈ ℕ)" by (rule MMI_imbi12d)
} then have S9: "∀x y. x = y ⟶
(A \<ls> x ⟶ x \<cs> A ∈ ℕ) ⟷
(A \<ls> y ⟶ y \<cs> A ∈ ℕ)" by simp
{ fix x y
have S10: "x = y \<ca> 𝟭 ⟶
A \<ls> x ⟷ A \<ls> y \<ca> 𝟭" by (rule MMI_breq2)
have S11: "x = y \<ca> 𝟭 ⟶
x \<cs> A = y \<ca> 𝟭 \<cs> A" by (rule MMI_opreq1)
from S11 have S12: "x = y \<ca> 𝟭 ⟶
x \<cs> A ∈ ℕ ⟷
y \<ca> 𝟭 \<cs> A ∈ ℕ" by (rule MMI_eleq1d)
from S10 S12 have "x = y \<ca> 𝟭 ⟶
(A \<ls> x ⟶ x \<cs> A ∈ ℕ) ⟷
(A \<ls> y \<ca> 𝟭 ⟶
y \<ca> 𝟭 \<cs> A ∈ ℕ)" by (rule MMI_imbi12d)
} then have S13: "∀x y. x = y \<ca> 𝟭 ⟶ (A \<ls> x ⟶ x \<cs> A ∈ ℕ) ⟷
(A \<ls> y \<ca> 𝟭 ⟶ y \<ca> 𝟭 \<cs> A ∈ ℕ)" by simp
{ fix x
have S14: "x = B ⟶
A \<ls> x ⟷ A \<ls> B" by (rule MMI_breq2)
have S15: "x = B ⟶ x \<cs> A = B \<cs> A" by (rule MMI_opreq1)
from S15 have S16: "x = B ⟶
x \<cs> A ∈ ℕ ⟷ B \<cs> A ∈ ℕ" by (rule MMI_eleq1d)
from S14 S16 have S17: "x = B ⟶
(A \<ls> x ⟶ x \<cs> A ∈ ℕ) ⟷
(A \<ls> B ⟶ B \<cs> A ∈ ℕ)" by (rule MMI_imbi12d)
} then have S17: "∀x. x = B ⟶
(A \<ls> x ⟶ x \<cs> A ∈ ℕ) ⟷ (A \<ls> B ⟶ B \<cs> A ∈ ℕ)"
by simp
from A1 have S18: "A ∈ ℕ".
have S19: "A ∈ ℕ ⟶ 𝟭 \<lsq> A" by (rule MMI_nnge1t)
from S18 S19 have S20: "𝟭 \<lsq> A" by (rule MMI_ax_mp)
have S21: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
from A1 have S22: "A ∈ ℕ".
from S22 have S23: "A ∈ ℝ" by (rule MMI_nnre)
from S21 S23 have S24: "𝟭 \<lsq> A ⟷ ¬(A \<ls> 𝟭)" by (rule MMI_lenlt)
from S20 S24 have S25: "¬(A \<ls> 𝟭)" by (rule MMI_mpbi)
from S25 have S26: "A \<ls> 𝟭 ⟶ 𝟭 \<cs> A ∈ ℕ" by (rule MMI_pm2_21i)
{ fix y
have S27: "y ∈ ℕ ⟶ y ∈ ℝ"