Theory MMI_Complex_ZF_2

(* 
    This file is a part of MMIsar - a translation of Metamath's set.mm to Isabelle 2005 (ZF logic).

    Copyright (C) 2007  Slawomir Kolodynski

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

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›
›

  (** proven by hand, really the definition of natural numbers *)

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

    (** a helper lemma that is needed bc. in Isabelle the intersection
    of empty set is pretty much undefined. To use the definition
    of natural numbers we need to show that we are intersecting a nonempty
    collection of sets. *)

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

(** this corresponds to Metamath's 1nn. Proven by Isabelle.**)

lemma (in MMIsar0) MMI_1nn: shows "𝟭 ∈ ℕ"
  using MMI_df_n MMI_Ndef_nonempty by auto

(** 501, 502 ******************************************)

(*lemma (in MMIsar0) MMI_nnex: shows "ℕ = ℕ" by simp;

lemma (in MMIsar0) MMI_peano2nn: 
   shows "A ∈ ℕ ⟶ A \<ca> 𝟭 ∈ ℕ"
  using MMI_df_n MMI_Ndef_nonempty by auto;

proof -
   have S1: "z = A ⟶ 
   z \<ca> 𝟭 = A \<ca> 𝟭" by (rule MMI_opreq1)
   from S1 have S2: "z = A ⟶ 
   z \<ca> 𝟭 ∈ ℕ ⟷ A \<ca> 𝟭 ∈ ℕ" by (rule MMI_eleq1d)
   have S3: "y = z ⟶ 
   y \<ca> 𝟭 = z \<ca> 𝟭" by (rule MMI_opreq1)
   from S3 have S4: "y = z ⟶ 
   y \<ca> 𝟭 ∈ x ⟷ z \<ca> 𝟭 ∈ x" by (rule MMI_eleq1d)
   from S4 have S5: "(∀y∈x. y \<ca> 𝟭 ∈ x) ⟶ 
   z ∈ x ⟶ z \<ca> 𝟭 ∈ x" by (rule MMI_rcla4cv)
   from S5 have S6: "𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) ⟶ 
   z ∈ x ⟶ z \<ca> 𝟭 ∈ x" by (rule MMI_adantl)
   from S6 have S7: "(𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) ⟶ z ∈ x) ⟶ 
   𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) ⟶ z \<ca> 𝟭 ∈ x" by (rule MMI_a2i)
   from S7 have S8: "(∀x. 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) ⟶ z ∈ x) ⟶ 
   (∀x. 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) ⟶ z \<ca> 𝟭 ∈ x)" by (rule MMI_19_20i)
   have S9: "z = z" by (rule MMI_visset)
   from S9 have S10: "z ∈ ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) } ⟷ 
   (∀x. 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) ⟶ z ∈ x)" by (rule MMI_elintab)
   have S11: "z \<ca> 𝟭 = z \<ca> 𝟭" by (rule MMI_oprex)
   from S11 have S12: "z \<ca> 𝟭 ∈ ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) } ⟷ 
   (∀x. 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) ⟶ z \<ca> 𝟭 ∈ x)" by (rule MMI_elintab)
   from S8 S10 S12 have S13: "z ∈ ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) } ⟶ 
   z \<ca> 𝟭 ∈ ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) }" by (rule MMI_3imtr4)
   have S14: "ℕ = ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) }" by (rule MMI_df_n)
   from S14 have S15: "z ∈ ℕ ⟷ 
   z ∈ ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) }" by (rule MMI_eleq2i)
   from S14 have S16: "ℕ = ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) }" .
   from S16 have S17: "z \<ca> 𝟭 ∈ ℕ ⟷ 
   z \<ca> 𝟭 ∈ ⋂ {x∈ Pow(ℝ). 𝟭 ∈ x ∧ (∀y∈x. y \<ca> 𝟭 ∈ x) }" by (rule MMI_eleq2i)
   from S13 S15 S17 have S18: "z ∈ ℕ ⟶ z \<ca> 𝟭 ∈ ℕ" by (rule MMI_3imtr4)
   from S2 S18 show "A ∈ ℕ ⟶ A \<ca> 𝟭 ∈ ℕ" by (rule MMI_vtoclga)
qed the original proof **)

(** first attempt, true, but not what needed **)
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

(** this version is needed, at least in nnaddclt **************)
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
(* I have no idea what this theorem even means

lemma (in MMIsar0) MMI_nn1suc: assumes A1: "x = 𝟭 ⟶ 
   φ ⟷ ψ" and
    A3: "x = y \<ca> 𝟭 ⟶ 
   φ ⟷ ch" and
    A4: "x = A ⟶ 
   φ ⟷ θ" and
    A5: "ψ" and
    A6: "y ∈ ℕ ⟶ ch"   
   shows "A ∈ ℕ ⟶ θ"
proof -
   have S1: "z = 𝟭 ⟶ 
   [ z / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   [ 𝟭 / x ] (A ∈ ℕ ⟶ φ)" by (rule MMI_dfsbcq)
   have S2: "z = y ⟶ 
   [ z / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   [ y / x ] (A ∈ ℕ ⟶ φ)" by (rule MMI_sbequ)
   have S3: "z = y \<ca> 𝟭 ⟶ 
   [ z / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   [ y \<ca> 𝟭 / x ] (A ∈ ℕ ⟶ φ)" by (rule MMI_dfsbcq)
   have S4: "z = A ⟶ 
   [ z / x ] φ ⟷ [ A / x ] φ" by (rule MMI_dfsbcq)
   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 ] φ) ⟶ 
   (∀x. A ∈ ℕ ⟶ [ A / x ] φ)" by (rule MMI_hbsbc1)
   have S8: "(A ∈ ℕ ⟶ θ) ⟶ 
   (∀x. A ∈ ℕ ⟶ θ)" by (rule MMI_ax_17)
   from S7 S8 have S9: "(A ∈ ℕ ⟶ [ A / x ] φ) ⟷ 
   (A ∈ ℕ ⟶ θ) ⟶ 
   (∀x. (A ∈ ℕ ⟶ [ A / x ] φ) ⟷ 
   (A ∈ ℕ ⟶ θ))" by (rule MMI_hbbi)
   have S10: "x = A ⟶ 
   φ ⟷ [ A / x ] φ" by (rule MMI_sbceq1a)
   from A4 have S11: "x = A ⟶ 
   φ ⟷ θ".
   from S10 S11 have S12: "x = A ⟶ 
   [ A / x ] φ ⟷ θ" by (rule MMI_bitr3d)
   from S12 have S13: "x = A ⟶ 
   (A ∈ ℕ ⟶ [ A / x ] φ) ⟷ 
   (A ∈ ℕ ⟶ θ)" by (rule MMI_imbi2d)
   from S9 S13 have S14: "( ∃x. x = A) ⟶ 
   (A ∈ ℕ ⟶ [ A / x ] φ) ⟷ 
   (A ∈ ℕ ⟶ θ)" by (rule MMI_19_23ai)
   from S5 S14 have S15: "A ∈ ℕ ⟶ 
   (A ∈ ℕ ⟶ [ A / x ] φ) ⟷ 
   (A ∈ ℕ ⟶ θ)" by (rule MMI_syl)
   from S15 have S16: "A ∈ ℕ ⟶ 
   A ∈ ℕ ⟶ 
   [ A / x ] φ ⟷ θ" by (rule MMI_pm5_74rd)
   from S16 have S17: "A ∈ ℕ ⟶ 
   [ A / x ] φ ⟷ θ" by (rule MMI_pm2_43i)
   from S4 S17 have S18: "A ∈ ℕ ∧ z = A ⟶ 
   [ z / x ] φ ⟷ θ" by (rule MMI_sylan9bbr)
   from S18 have S19: "z = A ⟶ 
   A ∈ ℕ ⟶ 
   [ z / x ] φ ⟷ θ" by (rule MMI_expcom)
   from S19 have S20: "z = A ⟶ 
   (A ∈ ℕ ⟶ [ z / x ] φ) ⟷ 
   (A ∈ ℕ ⟶ θ)" by (rule MMI_pm5_74d)
   have S21: "A ∈ ℕ ⟶ (∀x. A ∈ ℕ)" by (rule MMI_ax_17)
   from S21 have S22: "[ z / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   (A ∈ ℕ ⟶ [ z / x ] φ)" by (rule MMI_sb19_21)
   from S20 S22 have S23: "z = A ⟶ 
   [ z / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   (A ∈ ℕ ⟶ θ)" by (rule MMI_syl5bb)
   have S24: "𝟭 ∈ ℕ" by (rule MMI_1nn)
   from S24 have S25: "𝟭 = 𝟭" by (rule MMI_elisseti)
   from S25 have S26: " ∃x. x = 𝟭" by (rule MMI_isseti)
   from S25 have S27: "𝟭 = 𝟭" .
   from S27 have S28: "[ 𝟭 / x ] φ ⟶ 
   (∀x. [ 𝟭 / x ] φ)" by (rule MMI_hbsbc1v)
   from A5 have S29: "ψ".
   from A1 have S30: "x = 𝟭 ⟶ 
   φ ⟷ ψ".
   from S29 S30 have S31: "x = 𝟭 ⟶ φ" by (rule MMI_mpbiri)
   have S32: "x = 𝟭 ⟶ 
   φ ⟷ [ 𝟭 / x ] φ" by (rule MMI_sbceq1a)
   from S31 S32 have S33: "x = 𝟭 ⟶ [ 𝟭 / x ] φ" by (rule MMI_mpbid)
   from S28 S33 have S34: "( ∃x. x = 𝟭) ⟶ [ 𝟭 / x ] φ" by (rule MMI_19_23ai)
   from S26 S34 have S35: "[ 𝟭 / x ] φ" by (rule MMI_ax_mp)
   from S35 have S36: "A ∈ ℕ ⟶ [ 𝟭 / x ] φ" by (rule MMI_a1i)
   from S25 have S37: "𝟭 = 𝟭" .
   from S21 have S38: "A ∈ ℕ ⟶ (∀x. A ∈ ℕ)" .
   from S38 have S39: "𝟭 = 𝟭 ⟶ 
   [ 𝟭 / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   (A ∈ ℕ ⟶ [ 𝟭 / x ] φ)" by (rule MMI_sbc19_21g)
   from S37 S39 have S40: "[ 𝟭 / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   (A ∈ ℕ ⟶ [ 𝟭 / x ] φ)" by (rule MMI_ax_mp)
   from S36 S40 have S41: "[ 𝟭 / x ] (A ∈ ℕ ⟶ φ)" by (rule MMI_mpbir)
   from A6 have S42: "y ∈ ℕ ⟶ ch".
   have S43: "y \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_oprex)
   from S43 have S44: " ∃x. x = y \<ca> 𝟭" by (rule MMI_isseti)
   have S45: "ch ⟶ (∀x. ch)" by (rule MMI_ax_17)
   from S43 have S46: "y \<ca> 𝟭 = y \<ca> 𝟭" .
   from S46 have S47: "[ y \<ca> 𝟭 / x ] φ ⟶ 
   (∀x. [ y \<ca> 𝟭 / x ] φ)" by (rule MMI_hbsbc1v)
   from S45 S47 have S48: "ch ⟷ [ y \<ca> 𝟭 / x ] φ ⟶ 
   (∀x. ch ⟷ [ y \<ca> 𝟭 / x ] φ)" by (rule MMI_hbbi)
   from A3 have S49: "x = y \<ca> 𝟭 ⟶ 
   φ ⟷ ch".
   have S50: "x = y \<ca> 𝟭 ⟶ 
   φ ⟷ [ y \<ca> 𝟭 / x ] φ" by (rule MMI_sbceq1a)
   from S49 S50 have S51: "x = y \<ca> 𝟭 ⟶ 
   ch ⟷ [ y \<ca> 𝟭 / x ] φ" by (rule MMI_bitr3d)
   from S48 S51 have S52: "( ∃x. x = y \<ca> 𝟭) ⟶ 
   ch ⟷ [ y \<ca> 𝟭 / x ] φ" by (rule MMI_19_23ai)
   from S44 S52 have S53: "ch ⟷ [ y \<ca> 𝟭 / x ] φ" by (rule MMI_ax_mp)
   from S42 S53 have S54: "y ∈ ℕ ⟶ [ y \<ca> 𝟭 / x ] φ" by (rule MMI_sylib)
   from S54 have S55: "y ∈ ℕ ⟶ 
   A ∈ ℕ ⟶ [ y \<ca> 𝟭 / x ] φ" by (rule MMI_a1d)
   from S43 have S56: "y \<ca> 𝟭 = y \<ca> 𝟭" .
   from S21 have S57: "A ∈ ℕ ⟶ (∀x. A ∈ ℕ)" .
   from S57 have S58: "y \<ca> 𝟭 = y \<ca> 𝟭 ⟶ 
   [ y \<ca> 𝟭 / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   (A ∈ ℕ ⟶ [ y \<ca> 𝟭 / x ] φ)" by (rule MMI_sbc19_21g)
   from S56 S58 have S59: "[ y \<ca> 𝟭 / x ] (A ∈ ℕ ⟶ φ) ⟷ 
   (A ∈ ℕ ⟶ [ y \<ca> 𝟭 / x ] φ)" by (rule MMI_ax_mp)
   from S55 S59 have S60: "y ∈ ℕ ⟶ 
   [ y \<ca> 𝟭 / x ] (A ∈ ℕ ⟶ φ)" by (rule MMI_sylibr)
   from S60 have S61: "y ∈ ℕ ⟶ 
   [ y / x ] (A ∈ ℕ ⟶ φ) ⟶ 
   [ y \<ca> 𝟭 / x ] (A ∈ ℕ ⟶ φ)" by (rule MMI_a1d)
   from S1 S2 S3 S23 S41 S61 have S62: "A ∈ ℕ ⟶ 
   A ∈ ℕ ⟶ θ" by (rule MMI_nnind)
   from S62 show "A ∈ ℕ ⟶ θ" by (rule MMI_pm2_43i)
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(*(rule MMI_dfsbcq);*)
  have S2: "∀z y. z = y ⟶ (A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ φ(y))" by auto (*(rule MMI_sbequ);*)
  have S3: "∀z y. z = y \<ca> 𝟭 ⟶  (A ∈ ℕ ⟶ φ(z)) ⟷ (A ∈ ℕ ⟶ φ(y\<ca>𝟭))" 
    by auto (*(rule MMI_dfsbcq)*)
  { fix z 
    have S4: "z = A ⟶  φ(z) ⟷ φ(A)" by auto (*(rule MMI_dfsbcq)*)
    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 (*(rule MMI_hbsbc1)*)
    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 (*(rule MMI_sbceq1a)*)
    from A4 have S11: "∀x. x = A ⟶ φ(x) ⟷ θ(A)".
    from S10 S11 have S12: "∀ x. x = A ⟶ φ(x) ⟷ θ(A)" by auto (*(rule MMI_bitr3d);*)
    from S12 have S13: "∀x. x = A ⟶ (A ∈ ℕ ⟶ φ(x)) ⟷ (A ∈ ℕ ⟶ θ(A))" by auto (*(rule MMI_imbi2d);*)
    from S9 S13 have S14: "( ∃x. x = A) ⟶  (A ∈ ℕ ⟶ φ(A)) ⟷ (A ∈ ℕ ⟶ θ(A))" 
      by auto (*(rule MMI_19_23ai)*)
    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 (*(rule MMI_sb19_21)*)
    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 (*(rule MMI_elisseti);*)
   from S25 have S26: " ∃x. x = 𝟭" by (rule MMI_isseti)
   from S25 have S27: "𝟭 = 𝟭" .
   from S27 have S28: "φ(𝟭) ⟶  (∀x. φ(𝟭))" by simp (*(rule MMI_hbsbc1v);*)
   from A5 have S29: "ψ(𝟭)".
   from A1 have S30: "∀ x. x = 𝟭 ⟶ φ(x) ⟷ ψ(𝟭)".
   from S29 S30 have S31: "∀x. x = 𝟭 ⟶ φ(x)" by simp (*(rule MMI_mpbiri);*)
   have S32: "∀ x. x = 𝟭 ⟶ φ(x) ⟷ φ(𝟭)" by simp (*(rule MMI_sbceq1a);*)
   from S31 S32 have S33: "∀x. x = 𝟭 ⟶ φ(𝟭)" by blast (*(rule MMI_mpbid);*)
   from S28 S33 have S34: "( ∃x. x = 𝟭) ⟶ φ(𝟭)" by auto (*(rule MMI_19_23ai);*)
   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 (*(rule MMI_sbc19_21g);*)
   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 (*(rule MMI_oprex);*)
     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 (*(rule MMI_hbsbc1v);*)
     from S45 S47 have S48: 
       "(ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭)) ⟶  (∀x. ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭))" by simp 
       (*(rule MMI_hbbi)*)
     from A3 have S49: "∀x y. x = y \<ca> 𝟭 ⟶ φ(x) ⟷ ch(y\<ca>𝟭)".
     have S50: "∀x. x = y \<ca> 𝟭 ⟶  φ(x) ⟷ φ(y \<ca> 𝟭)" by simp (*(rule MMI_sbceq1a);*)
     from S49 S50 have S51: "∀ x. x = y \<ca> 𝟭 ⟶  ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭)" 
       by simp (*(rule MMI_bitr3d)*)
     from S48 S51 have S52: "( ∃x. x = y \<ca> 𝟭) ⟶ ch(y \<ca> 𝟭) ⟷ φ(y \<ca> 𝟭)" by auto
       (*(rule MMI_19_23ai);*)
     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 (*(rule MMI_sbc19_21g);*)
     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 (*by (rule MMI_rcla4ev)*)
   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 (*(rule MMI_rcla4ev)*)
   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

(*********** 511-515****************************)

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

(********* 516 - 520 *************************)
 
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

(* here is the original almost translated proof of nnleltp1t:

proof -
   have S1: "A ∈ ℝ ∧ B ∈ ℝ ⟶ 
   A \<lsq> B ⟷ A \<ls> B ∨ A = B" by (rule MMI_leloet)
   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 ⟷ A \<ls> B ∨ A = B" by (rule MMI_syl2an)
   have S5: "𝟬 \<ls> 𝟭" by (rule MMI_lt01)
   have S6: "𝟬 ∈ ℝ" by (rule MMI_0re)
   have S7: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
   from S6 S7 have S8: "𝟬 ∈ ℝ ∧ 𝟭 ∈ ℝ" by (rule MMI_pm3_2i)
   have S9: "(A ∈ ℝ ∧ 𝟬 ∈ ℝ) ∧ B ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
   A \<ls> B ∧ 𝟬 \<ls> 𝟭 ⟶ 
   A \<ca> 𝟬 \<ls> B \<ca> 𝟭" by (rule MMI_lt2addt)
   from S9 have S10: "(A ∈ ℝ ∧ B ∈ ℝ) ∧ 𝟬 ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
   A \<ls> B ∧ 𝟬 \<ls> 𝟭 ⟶ 
   A \<ca> 𝟬 \<ls> B \<ca> 𝟭" by (rule MMI_an4s)
   from S8 S10 have S11: "A ∈ ℝ ∧ B ∈ ℝ ⟶ 
   A \<ls> B ∧ 𝟬 \<ls> 𝟭 ⟶ 
   A \<ca> 𝟬 \<ls> B \<ca> 𝟭" by (rule MMI_mpan2)
   from S5 S11 have S12: "A ∈ ℝ ∧ B ∈ ℝ ⟶ 
   A \<ls> B ⟶ 
   A \<ca> 𝟬 \<ls> B \<ca> 𝟭" by (rule MMI_mpan2i)
   have S13: "A ∈ ℝ ∧ B ∈ ℝ ⟶ A ∈ ℝ" by (rule MMI_pm3_26)
   have S14: "A ∈ ℝ ⟶ A ∈ ℂ" by (rule MMI_recnt)
   have S15: "A ∈ ℂ ⟶ A \<ca> 𝟬 = A" by (rule MMI_ax0id)
   from S13 S14 S15 have S16: "A ∈ ℝ ∧ B ∈ ℝ ⟶ A \<ca> 𝟬 = A" by (rule MMI_3syl)
   from S16 have S17: "A ∈ ℝ ∧ B ∈ ℝ ⟶ 
   A \<ca> 𝟬 \<ls> B \<ca> 𝟭 ⟷ A \<ls> B \<ca> 𝟭" by (rule MMI_breq1d)
   from S12 S17 have S18: "A ∈ ℝ ∧ B ∈ ℝ ⟶ 
   A \<ls> B ⟶ A \<ls> B \<ca> 𝟭" by (rule MMI_sylibd)
   have S19: "A = B ⟶ 
   A \<ls> B \<ca> 𝟭 ⟷ B \<ls> B \<ca> 𝟭" by (rule MMI_breq1)
   have S20: "B ∈ ℝ ⟶ B \<ls> B \<ca> 𝟭" by (rule MMI_ltp1t)
   from S19 S20 have S21: "A = B ⟶ 
   B ∈ ℝ ⟶ A \<ls> B \<ca> 𝟭" by (rule MMI_syl5bir)
   from S21 have S22: "B ∈ ℝ ⟶ 
   A = B ⟶ A \<ls> B \<ca> 𝟭" by (rule MMI_com12)
   from S22 have S23: "A ∈ ℝ ∧ B ∈ ℝ ⟶ 
   A = B ⟶ A \<ls> B \<ca> 𝟭" by (rule MMI_adantl)
   from S18 S23 have S24: "A ∈ ℝ ∧ B ∈ ℝ ⟶ 
   A \<ls> B ∨ A = B ⟶ A \<ls> B \<ca> 𝟭" by (rule MMI_jaod)
   from S2 have S25: "A ∈ ℕ ⟶ A ∈ ℝ" .
   from S3 have S26: "B ∈ ℕ ⟶ B ∈ ℝ" .
   from S24 S25 S26 have S27: "A ∈ ℕ ∧ B ∈ ℕ ⟶ 
   A \<ls> B ∨ A = B ⟶ A \<ls> B \<ca> 𝟭" by (rule MMI_syl2an)
   { fix z
     have S28: "z = A ⟶ 
       z \<ls> B \<ca> 𝟭 ⟷ A \<ls> B \<ca> 𝟭" by (rule MMI_breq1)
     have S29: "z = A ⟶ 
       z \<ls> B ⟷ A \<ls> B" by (rule MMI_breq1)
     have S30: "z = A ⟶ 
       z = B ⟷ A = B" by (rule MMI_eqeq1)
     from S29 S30 have S31: "z = A ⟶ 
       z \<ls> B ∨ z = B ⟷ A \<ls> B ∨ A = B" by (rule MMI_orbi12d)
     from S28 S31 have S32: "z = A ⟶ 
       (z \<ls> B \<ca> 𝟭 ⟶ z \<ls> B ∨ z = B) ⟷ 
       (A \<ls> B \<ca> 𝟭 ⟶ A \<ls> B ∨ A = B)" by (rule MMI_imbi12d)
     from S32 have S33: "A ∈ ℕ ⟶ 
       (∀z∈ℕ. z \<ls> B \<ca> 𝟭 ⟶ z \<ls> B ∨ z = B) ⟶ 
       A \<ls> B \<ca> 𝟭 ⟶ A \<ls> B ∨ A = B" by auto; (rule MMI_rcla4v)
     { fix x
       have S34: "x = 𝟭 ⟶ 
	 x \<ca> 𝟭 = 𝟭 \<ca> 𝟭" by (rule MMI_opreq1)
       from S34 have S35: "x = 𝟭 ⟶ 
	 z \<ls> x \<ca> 𝟭 ⟷ z \<ls> 𝟭 \<ca> 𝟭" by (rule MMI_breq2d)
       have S36: "x = 𝟭 ⟶ 
	 z \<ls> x ⟷ z \<ls> 𝟭" by (rule MMI_breq2)
       have S37: "x = 𝟭 ⟶ 
	 z = x ⟷ z = 𝟭" by (rule MMI_eqeq2)
       from S36 S37 have S38: "x = 𝟭 ⟶ 
	 z \<ls> x ∨ z = x ⟷ 
	 z \<ls> 𝟭 ∨ z = 𝟭" by (rule MMI_orbi12d)
       from S35 S38 have S39: "x = 𝟭 ⟶ 
	 (z \<ls> x \<ca> 𝟭 ⟶ z \<ls> x ∨ z = x) ⟷ 
	 (z \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 z \<ls> 𝟭 ∨ z = 𝟭)" by (rule MMI_imbi12d)
       from S39 have S40: "x = 𝟭 ⟶ 
	 (∀z∈ℕ. z \<ls> x \<ca> 𝟭 ⟶ z \<ls> x ∨ z = x) ⟷ 
	 (∀z∈ℕ. z \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 z \<ls> 𝟭 ∨ z = 𝟭)" by auto; (rule MMI_ralbidv)
       have S41: "x = y ⟶ 
	 x \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_opreq1)
       from S41 have S42: "x = y ⟶ 
	 z \<ls> x \<ca> 𝟭 ⟷ z \<ls> y \<ca> 𝟭" by (rule MMI_breq2d)
       have S43: "x = y ⟶ 
	 z \<ls> x ⟷ z \<ls> y" by (rule MMI_breq2)
       have S44: "x = y ⟶ 
	 z = x ⟷ z = y" by (rule MMI_eqeq2)
       from S43 S44 have S45: "x = y ⟶ 
	 z \<ls> x ∨ z = x ⟷ z \<ls> y ∨ z = y" by (rule MMI_orbi12d)
       from S42 S45 have S46: "x = y ⟶ 
	 (z \<ls> x \<ca> 𝟭 ⟶ z \<ls> x ∨ z = x) ⟷ 
	 (z \<ls> y \<ca> 𝟭 ⟶ z \<ls> y ∨ z = y)" by (rule MMI_imbi12d)
       from S46 have S47: "x = y ⟶ 
	 (∀z∈ℕ. z \<ls> x \<ca> 𝟭 ⟶ z \<ls> x ∨ z = x) ⟷ 
	 (∀z∈ℕ. z \<ls> y \<ca> 𝟭 ⟶ z \<ls> y ∨ z = y)" by auto; (rule MMI_ralbidv)
       have S48: "x = y \<ca> 𝟭 ⟶ 
	 x \<ca> 𝟭 = y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_opreq1)
       from S48 have S49: "x = y \<ca> 𝟭 ⟶ 
	 z \<ls> x \<ca> 𝟭 ⟷ 
	 z \<ls> y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_breq2d)
       have S50: "x = y \<ca> 𝟭 ⟶ 
	 z \<ls> x ⟷ z \<ls> y \<ca> 𝟭" by (rule MMI_breq2)
       have S51: "x = y \<ca> 𝟭 ⟶ 
	 z = x ⟷ z = y \<ca> 𝟭" by (rule MMI_eqeq2)
       from S50 S51 have S52: "x = y \<ca> 𝟭 ⟶ 
	 z \<ls> x ∨ z = x ⟷ 
	 z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭" by (rule MMI_orbi12d)
       from S49 S52 have S53: "x = y \<ca> 𝟭 ⟶ 
	 (z \<ls> x \<ca> 𝟭 ⟶ z \<ls> x ∨ z = x) ⟷ 
	 (z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
	 z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭)" by (rule MMI_imbi12d)
       from S53 have S54: "x = y \<ca> 𝟭 ⟶ 
	 (∀z∈ℕ. z \<ls> x \<ca> 𝟭 ⟶ z \<ls> x ∨ z = x) ⟷ 
	 (∀z∈ℕ. z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
	 z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭)" by auto; (rule MMI_ralbidv)
       have S55: "x = B ⟶ 
	 x \<ca> 𝟭 = B \<ca> 𝟭" by (rule MMI_opreq1)
       from S55 have S56: "x = B ⟶ 
	 z \<ls> x \<ca> 𝟭 ⟷ z \<ls> B \<ca> 𝟭" by (rule MMI_breq2d)
       have S57: "x = B ⟶ 
	 z \<ls> x ⟷ z \<ls> B" by (rule MMI_breq2)
       have S58: "x = B ⟶ 
	 z = x ⟷ z = B" by (rule MMI_eqeq2)
       from S57 S58 have S59: "x = B ⟶ 
	 z \<ls> x ∨ z = x ⟷ z \<ls> B ∨ z = B" by (rule MMI_orbi12d)
       from S56 S59 have S60: "x = B ⟶ 
	 (z \<ls> x \<ca> 𝟭 ⟶ z \<ls> x ∨ z = x) ⟷ 
	 (z \<ls> B \<ca> 𝟭 ⟶ z \<ls> B ∨ z = B)" by (rule MMI_imbi12d)
       from S60 have S61: "x = B ⟶ 
	 (∀z∈ℕ. z \<ls> x \<ca> 𝟭 ⟶ z \<ls> x ∨ z = x) ⟷ 
	 (∀z∈ℕ. z \<ls> B \<ca> 𝟭 ⟶ z \<ls> B ∨ z = B)" by auto; (rule MMI_ralbidv)
       have S62: "x = 𝟭 ⟶ 
	 x \<ls> 𝟭 \<ca> 𝟭 ⟷ 
	 𝟭 \<ls> 𝟭 \<ca> 𝟭" by (rule MMI_breq1)
       have S63: "x = 𝟭 ⟶ 
	 x \<ls> 𝟭 ⟷ 𝟭 \<ls> 𝟭" by (rule MMI_breq1)
       have S64: "x = 𝟭 ⟶ 
	 x = 𝟭 ⟷ 𝟭 = 𝟭" by (rule MMI_eqeq1)
       from S63 S64 have S65: "x = 𝟭 ⟶ 
	 x \<ls> 𝟭 ∨ x = 𝟭 ⟷ 
	 𝟭 \<ls> 𝟭 ∨ 𝟭 = 𝟭" by (rule MMI_orbi12d)
       from S62 S65 have 
	 "x = 𝟭 ⟶  (x \<ls> 𝟭 \<ca> 𝟭 ⟶  x \<ls> 𝟭 ∨ x = 𝟭) ⟷  (𝟭 \<ls> 𝟭 \<ca> 𝟭 ⟶ 𝟭 \<ls> 𝟭 ∨ 𝟭 = 𝟭)" 
	 by (rule MMI_imbi12d)
     } then have S66: 
	 "∀ x. x = 𝟭 ⟶  (x \<ls> 𝟭 \<ca> 𝟭 ⟶  x \<ls> 𝟭 ∨ x = 𝟭) ⟷ 
	 (𝟭 \<ls> 𝟭 \<ca> 𝟭 ⟶ 𝟭 \<ls> 𝟭 ∨ 𝟭 = 𝟭)"
       by simp;
     { fix x y
       have S67: "x = y \<ca> 𝟭 ⟶ 
	 x \<ls> 𝟭 \<ca> 𝟭 ⟷ 
	 y \<ca> 𝟭 \<ls> 𝟭 \<ca> 𝟭" by (rule MMI_breq1);
       have S68: "x = y \<ca> 𝟭 ⟶ 
	 x \<ls> 𝟭 ⟷ y \<ca> 𝟭 \<ls> 𝟭" by (rule MMI_breq1)
       have S69: "x = y \<ca> 𝟭 ⟶ 
	 x = 𝟭 ⟷ y \<ca> 𝟭 = 𝟭" by (rule MMI_eqeq1)
       from S68 S69 have S70: "x = y \<ca> 𝟭 ⟶ 
	 x \<ls> 𝟭 ∨ x = 𝟭 ⟷ 
	 y \<ca> 𝟭 \<ls> 𝟭 ∨ y \<ca> 𝟭 = 𝟭" by (rule MMI_orbi12d);
       from S67 S70 have S71: "x = y \<ca> 𝟭 ⟶ 
	 (x \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 x \<ls> 𝟭 ∨ x = 𝟭) ⟷ 
	 (y \<ca> 𝟭 \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 y \<ca> 𝟭 \<ls> 𝟭 ∨ y \<ca> 𝟭 = 𝟭)" by (rule MMI_imbi12d)
     } then have S71: "∀x y. x = y \<ca> 𝟭 ⟶ 
	 (x \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 x \<ls> 𝟭 ∨ x = 𝟭) ⟷ 
	 (y \<ca> 𝟭 \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 y \<ca> 𝟭 \<ls> 𝟭 ∨ y \<ca> 𝟭 = 𝟭)" by simp;
     { fix x
       have S72: "x = z ⟶ 
	 x \<ls> 𝟭 \<ca> 𝟭 ⟷ z \<ls> 𝟭 \<ca> 𝟭" by (rule MMI_breq1)
       have S73: "x = z ⟶ 
	 x \<ls> 𝟭 ⟷ z \<ls> 𝟭" by (rule MMI_breq1)
       have S74: "x = z ⟶ 
	 x = 𝟭 ⟷ z = 𝟭" by (rule MMI_eqeq1)
       from S73 S74 have S75: "x = z ⟶ 
	 x \<ls> 𝟭 ∨ x = 𝟭 ⟷ 
	 z \<ls> 𝟭 ∨ z = 𝟭" by (rule MMI_orbi12d)
       from S72 S75 have "x = z ⟶ 
	 (x \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 x \<ls> 𝟭 ∨ x = 𝟭) ⟷ 
	 (z \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 z \<ls> 𝟭 ∨ z = 𝟭)" by (rule MMI_imbi12d)
     } then have S76: "∀ x. x = z ⟶ 
	 (x \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 x \<ls> 𝟭 ∨ x = 𝟭) ⟷ 
	 (z \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 z \<ls> 𝟭 ∨ z = 𝟭)" by simp;
     have S77: "𝟭 = 𝟭" by (rule MMI_eqid)
     from S77 have S78: "¬(𝟭 \<ls> 𝟭) ⟶ 𝟭 = 𝟭" by (rule MMI_a1i)
     from S78 have S79: "𝟭 \<ls> 𝟭 ∨ 𝟭 = 𝟭" by (rule MMI_orri)
     from S79 have S80: "𝟭 \<ls> 𝟭 \<ca> 𝟭 ⟶ 
       𝟭 \<ls> 𝟭 ∨ 𝟭 = 𝟭" by (rule MMI_a1i)
     { fix y
       have S81: "y ∈ ℕ ⟶ y ∈ ℝ" by (rule MMI_nnret)
       have S82: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
       have S83: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
       have S84: "y ∈ ℝ ∧ 𝟭 ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
	 y \<ls> 𝟭 ⟷ 
	 y \<ca> 𝟭 \<ls> 𝟭 \<ca> 𝟭" by (rule MMI_ltadd1t)
       from S82 S83 S84 have S85: "y ∈ ℝ ⟶ 
	 y \<ls> 𝟭 ⟷ 
	 y \<ca> 𝟭 \<ls> 𝟭 \<ca> 𝟭" by (rule MMI_mp3an23)
       from S81 S85 have S86: "y ∈ ℕ ⟶ 
	 y \<ls> 𝟭 ⟷ 
	 y \<ca> 𝟭 \<ls> 𝟭 \<ca> 𝟭" by (rule MMI_syl)
       have S87: "y ∈ ℕ ⟶ 𝟭 \<lsq> y" by (rule MMI_nnge1t)
       from S81 have S88: "y ∈ ℕ ⟶ y ∈ ℝ" .
       have S89: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
       have S90: "𝟭 ∈ ℝ ∧ y ∈ ℝ ⟶ 
	 𝟭 \<lsq> y ⟷ ¬(y \<ls> 𝟭)" by (rule MMI_lenltt)
       from S89 S90 have S91: "y ∈ ℝ ⟶ 
	 𝟭 \<lsq> y ⟷ ¬(y \<ls> 𝟭)" by (rule MMI_mpan)
       from S88 S91 have S92: "y ∈ ℕ ⟶ 
	 𝟭 \<lsq> y ⟷ ¬(y \<ls> 𝟭)" by (rule MMI_syl)
       from S87 S92 have S93: "y ∈ ℕ ⟶ ¬(y \<ls> 𝟭)" by (rule MMI_mpbid)
       from S93 have S94: "y ∈ ℕ ⟶ 
	 y \<ls> 𝟭 ⟶ 
	 y \<ca> 𝟭 \<ls> 𝟭 ∨ y \<ca> 𝟭 = 𝟭" by (rule MMI_pm2_21d)
       from S86 S94 have "y ∈ ℕ ⟶ 
	 y \<ca> 𝟭 \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 y \<ca> 𝟭 \<ls> 𝟭 ∨ y \<ca> 𝟭 = 𝟭" by (rule MMI_sylbird)
     } then have  S95: "∀ y. y ∈ ℕ ⟶ 
	 y \<ca> 𝟭 \<ls> 𝟭 \<ca> 𝟭 ⟶ 
	 y \<ca> 𝟭 \<ls> 𝟭 ∨ y \<ca> 𝟭 = 𝟭" by simp;
     from S66 S71 S76 S80 S95 have "z ∈ ℕ ⟶ 
       z \<ls> 𝟭 \<ca> 𝟭 ⟶ 
       z \<ls> 𝟭 ∨ z = 𝟭" by (rule MMI_nn1suc);
   } then have  S96: "∀z. z ∈ ℕ ⟶  z \<ls> 𝟭 \<ca> 𝟭 ⟶ z \<ls> 𝟭 ∨ z = 𝟭"
     by simp;       
   from S96 have S97: "∀z∈ℕ. z \<ls> 𝟭 \<ca> 𝟭 ⟶ 
     z \<ls> 𝟭 ∨ z = 𝟭" by (rule MMI_rgen);
   { fix x
     have S98: "x = 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟷ 
       𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_breq1)
     have S99: "x = 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ⟷ 𝟭 \<ls> y \<ca> 𝟭" by (rule MMI_breq1)
     have S100: "x = 𝟭 ⟶ 
       x = y \<ca> 𝟭 ⟷ 𝟭 = y \<ca> 𝟭" by (rule MMI_eqeq1)
     from S99 S100 have S101: "x = 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭 ⟷ 
       𝟭 \<ls> y \<ca> 𝟭 ∨ 𝟭 = y \<ca> 𝟭" by (rule MMI_orbi12d)
     from S98 S101 have S102: "x = 𝟭 ⟶ 
       (x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
       (𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 ∨ 𝟭 = y \<ca> 𝟭)" by (rule MMI_imbi12d)
     from S102 have "x = 𝟭 ⟶ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 ∨ 𝟭 = y \<ca> 𝟭)" by (rule MMI_imbi2d)
   } then have S103: "∀ x. x = 𝟭 ⟶ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 ∨ 𝟭 = y \<ca> 𝟭)" by simp;
   { fix x v
     have S104: "x = v \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_breq1)
     have S105: "x = v \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭" by (rule MMI_breq1)
     have S106: "x = v \<ca> 𝟭 ⟶ 
       x = y \<ca> 𝟭 ⟷ 
       v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_eqeq1)
     from S105 S106 have S107: "x = v \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭 ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_orbi12d)
     from S104 S107 have S108: "x = v \<ca> 𝟭 ⟶ 
       (x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
       (v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭)" by (rule MMI_imbi12d)
     from S108 have "x = v \<ca> 𝟭 ⟶ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭)" by (rule MMI_imbi2d)
   } then have S109: "∀x v. x = v \<ca> 𝟭 ⟶ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭)"
     by simp;
   { fix x
     have S110: "x = z ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟷ 
       z \<ls> y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_breq1)
     have S111: "x = z ⟶ 
       x \<ls> y \<ca> 𝟭 ⟷ z \<ls> y \<ca> 𝟭" by (rule MMI_breq1)
     have S112: "x = z ⟶ 
       x = y \<ca> 𝟭 ⟷ z = y \<ca> 𝟭" by (rule MMI_eqeq1)
     from S111 S112 have S113: "x = z ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭 ⟷ 
       z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭" by (rule MMI_orbi12d)
     from S110 S113 have S114: "x = z ⟶ 
       (x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
   (z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭)" by (rule MMI_imbi12d)
     from S114 have "x = z ⟶ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭)" by (rule MMI_imbi2d)
     } then have S115: "∀x. x = z ⟶ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       x \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       x \<ls> y \<ca> 𝟭 ∨ x = y \<ca> 𝟭) ⟷ 
       (y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭)" by simp;
     have S116: "y ∈ ℕ ⟶ 𝟬 \<ls> y" by (rule MMI_nngt0t)
     have S117: "y ∈ ℕ ⟶ y ∈ ℝ" by (rule MMI_nnret);
     have S118: "𝟬 ∈ ℝ" by (rule MMI_0re)
     have S119: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
     have S120: "𝟬 ∈ ℝ ∧ y ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
       𝟬 \<ls> y ⟷ 
       𝟬 \<ca> 𝟭 \<ls> y \<ca> 𝟭" by (rule MMI_ltadd1t)
     from S118 S119 S120 have S121: "y ∈ ℝ ⟶ 
       𝟬 \<ls> y ⟷ 
       𝟬 \<ca> 𝟭 \<ls> y \<ca> 𝟭" by (rule MMI_mp3an13)
     from S117 S121 have S122: "y ∈ ℕ ⟶ 
       𝟬 \<ls> y ⟷ 
       𝟬 \<ca> 𝟭 \<ls> y \<ca> 𝟭" by (rule MMI_syl)
     from S116 S122 have S123: "y ∈ ℕ ⟶ 
       𝟬 \<ca> 𝟭 \<ls> y \<ca> 𝟭" by (rule MMI_mpbid)
     have S124: "𝟭 ∈ ℂ" by (rule MMI_1cn)
     from S124 have S125: "𝟬 \<ca> 𝟭 = 𝟭" by (rule MMI_addid2)
     from S123 S125 have S126: "y ∈ ℕ ⟶ 𝟭 \<ls> y \<ca> 𝟭" by (rule MMI_syl5eqbrr)
     from S126 have S127: "y ∈ ℕ ⟶ 
       ¬(𝟭 \<ls> y \<ca> 𝟭) ⟶ 𝟭 = y \<ca> 𝟭" by (rule MMI_pm2_21nd)
     from S127 have S128: "y ∈ ℕ ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 ∨ 𝟭 = y \<ca> 𝟭" by (rule MMI_orrd)
     from S128 have S129: "y ∈ ℕ ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 ∨ 𝟭 = y \<ca> 𝟭" by (rule MMI_a1d)
     from S129 have S130: "y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
   𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       𝟭 \<ls> y \<ca> 𝟭 ∨ 𝟭 = y \<ca> 𝟭" by (rule MMI_adantr)
     { fix v
       have S131: "w = v ⟶ 
	 w \<ls> y \<ca> 𝟭 ⟷ v \<ls> y \<ca> 𝟭" by (rule MMI_breq1);
       have S132: "w = v ⟶ 
	 w \<ls> y ⟷ v \<ls> y" by (rule MMI_breq1)
       have S133: "w = v ⟶ 
	 w = y ⟷ v = y" by (rule MMI_eqeq1)
       from S132 S133 have S134: "w = v ⟶ 
	 w \<ls> y ∨ w = y ⟷ v \<ls> y ∨ v = y" by (rule MMI_orbi12d)
       from S131 S134 have S135: "w = v ⟶ 
	 (w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟷ 
	 (v \<ls> y \<ca> 𝟭 ⟶ v \<ls> y ∨ v = y)" by (rule MMI_imbi12d)
       from S135 have S136: "v ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
	 v \<ls> y \<ca> 𝟭 ⟶ v \<ls> y ∨ v = y" by auto; (rule MMI_rcla4va)
       from S136 have S137: "(v ∈ ℕ ∧ y ∈ ℕ) ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
	 v \<ls> y \<ca> 𝟭 ⟶ v \<ls> y ∨ v = y" by (rule MMI_adantlr)
       have S138: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
       have S139: "v ∈ ℝ ∧ y \<ca> 𝟭 ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
	 v \<ls> y \<ca> 𝟭 ⟷ 
	 v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_ltadd1t)
       from S138 S139 have S140: "v ∈ ℝ ∧ y \<ca> 𝟭 ∈ ℝ ⟶ 
	 v \<ls> y \<ca> 𝟭 ⟷ 
	 v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_mp3an3)
       have S141: "v ∈ ℕ ⟶ v ∈ ℝ" by (rule MMI_nnret)
       have S142: "y ∈ ℕ ⟶ y \<ca> 𝟭 ∈ ℕ" by (rule MMI_peano2nn)
     have S143: "y \<ca> 𝟭 ∈ ℕ ⟶ y \<ca> 𝟭 ∈ ℝ" by (rule MMI_nnret)
     from S142 S143 have S144: "y ∈ ℕ ⟶ y \<ca> 𝟭 ∈ ℝ" by (rule MMI_syl)
     from S140 S141 S144 have S145: "v ∈ ℕ ∧ y ∈ ℕ ⟶ 
       v \<ls> y \<ca> 𝟭 ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_syl2an)
     from S145 have S146: "(v ∈ ℕ ∧ y ∈ ℕ) ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       v \<ls> y \<ca> 𝟭 ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭" by (rule MMI_adantr)
     have S147: "𝟭 ∈ ℝ" by (rule MMI_ax1re)
     have S148: "v ∈ ℝ ∧ y ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
       v \<ls> y ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭" by (rule MMI_ltadd1t)
     have S149: "v ∈ ℝ ⟶ v ∈ ℂ" by (rule MMI_recnt)
     have S150: "y ∈ ℝ ⟶ y ∈ ℂ" by (rule MMI_recnt)
     have S151: "𝟭 ∈ ℝ ⟶ 𝟭 ∈ ℂ" by (rule MMI_recnt)
     from S149 S150 S151 have S152: "v ∈ ℝ ∧ y ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
       v ∈ ℂ ∧ y ∈ ℂ ∧ 𝟭 ∈ ℂ" by (rule MMI_3anim123i)
     have S153: "𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ ⟷ 
       v ∈ ℂ ∧ y ∈ ℂ ∧ 𝟭 ∈ ℂ" by (rule MMI_3anrot)
     from S152 S153 have S154: "v ∈ ℝ ∧ y ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
       𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ" by (rule MMI_sylibr)
     have S155: "𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ ⟶ 
       v ∈ ℂ ∧ y ∈ ℂ" by (rule MMI_3simpc)
     have S156: "𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ ⟶ 𝟭 ∈ ℂ" by (rule MMI_3simp1)
     from S155 S156 have S157: "𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ ⟶ 
       (v ∈ ℂ ∧ y ∈ ℂ) ∧ 𝟭 ∈ ℂ" by (rule MMI_jca)
     have S158: "(v ∈ ℂ ∧ y ∈ ℂ) ∧ 𝟭 ∈ ℂ ⟷ 
       (v ∈ ℂ ∧ 𝟭 ∈ ℂ) ∧ y ∈ ℂ ∧ 𝟭 ∈ ℂ" by (rule MMI_anandir)
     from S157 S158 have S159: "𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ ⟶ 
       (v ∈ ℂ ∧ 𝟭 ∈ ℂ) ∧ y ∈ ℂ ∧ 𝟭 ∈ ℂ" by (rule MMI_sylib)
     have S160: "v ∈ ℂ ∧ 𝟭 ∈ ℂ ⟶ 
       v \<ca> 𝟭 = 𝟭 \<ca> v" by (rule MMI_axaddcom)
     have S161: "y ∈ ℂ ∧ 𝟭 ∈ ℂ ⟶ 
       y \<ca> 𝟭 = 𝟭 \<ca> y" by (rule MMI_axaddcom)
     from S160 S161 have S162: "(v ∈ ℂ ∧ 𝟭 ∈ ℂ) ∧ y ∈ ℂ ∧ 𝟭 ∈ ℂ ⟶ 
       v \<ca> 𝟭 = y \<ca> 𝟭 ⟷ 
       𝟭 \<ca> v = 𝟭 \<ca> y" by (rule MMI_eqeqan12d);
     from S159 S162 have S163: "𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ ⟶ 
       v \<ca> 𝟭 = y \<ca> 𝟭 ⟷ 
       𝟭 \<ca> v = 𝟭 \<ca> y" by (rule MMI_syl)
     have S164: "𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ ⟶ 
       𝟭 \<ca> v = 𝟭 \<ca> y ⟷ v = y" by (rule MMI_addcant)
     from S163 S164 have S165: "𝟭 ∈ ℂ ∧ v ∈ ℂ ∧ y ∈ ℂ ⟶ 
       v = y ⟷ 
       v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_bitr2d)
     from S154 S165 have S166: "v ∈ ℝ ∧ y ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
       v = y ⟷ 
       v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_syl)
     from S148 S166 have S167: "v ∈ ℝ ∧ y ∈ ℝ ∧ 𝟭 ∈ ℝ ⟶ 
       v \<ls> y ∨ v = y ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_orbi12d)
     from S147 S167 have S168: "v ∈ ℝ ∧ y ∈ ℝ ⟶ 
       v \<ls> y ∨ v = y ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_mp3an3)
     from S141 have S169: "v ∈ ℕ ⟶ v ∈ ℝ" .
     have S170: "y ∈ ℕ ⟶ y ∈ ℝ" by (rule MMI_nnret);
     from S168 S169 S170 have S171: "v ∈ ℕ ∧ y ∈ ℕ ⟶ 
       v \<ls> y ∨ v = y ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_syl2an)
     from S171 have S172: "(v ∈ ℕ ∧ y ∈ ℕ) ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       v \<ls> y ∨ v = y ⟷ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_adantr)
     from S137 S146 S172 have S173: "(v ∈ ℕ ∧ y ∈ ℕ) ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_3imtr3d)
     from S173 have S174: "v ∈ ℕ ⟶ 
       y ∈ ℕ ⟶ 
       (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_exp31)
     from S174 have "v ∈ ℕ ⟶ 
       y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭" by (rule MMI_imp3a)
   } then have S175: "∀ v. v ∈ ℕ ⟶ 
       ( y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
       v \<ca> 𝟭 \<ls> y \<ca> 𝟭 ∨ v \<ca> 𝟭 = y \<ca> 𝟭 )" by simp;
   from S103 S109 S115 S130 S175 have S176: "z ∈ ℕ ⟶ 
   ( y ∈ ℕ ∧ (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
   z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
   z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭)" 
 ************ this is where Isabelle stops ********************
 ********* if you know how to fix it, please let me know ******
 by (rule MMI_nn1suc)

   from S176 have S177: "z ∈ ℕ ⟶ 
   y ∈ ℕ ⟶ 
   (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
   z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
   z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭" by (rule MMI_exp3a);
   from S177 have S178: "y ∈ ℕ ⟶ 
   (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
   z ∈ ℕ ⟶ 
   z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
   z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭" by (rule MMI_com3l)
   from S178 have S179: "y ∈ ℕ ⟶ 
   (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y) ⟶ 
   (∀z∈ℕ. z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
   z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭)" by (rule MMI_r19_21adv)
   have S180: "z = w ⟶ 
   z \<ls> y \<ca> 𝟭 ⟷ w \<ls> y \<ca> 𝟭" by (rule MMI_breq1)
   have S181: "z = w ⟶ 
   z \<ls> y ⟷ w \<ls> y" by (rule MMI_breq1)
   have S182: "z = w ⟶ 
   z = y ⟷ w = y" by (rule MMI_eqeq1)
   from S181 S182 have S183: "z = w ⟶ 
   z \<ls> y ∨ z = y ⟷ w \<ls> y ∨ w = y" by (rule MMI_orbi12d)
   from S180 S183 have S184: "z = w ⟶ 
   (z \<ls> y \<ca> 𝟭 ⟶ z \<ls> y ∨ z = y) ⟷ 
   (w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y)" by (rule MMI_imbi12d)
   from S184 have S185: "(∀z∈ℕ. z \<ls> y \<ca> 𝟭 ⟶ z \<ls> y ∨ z = y) ⟷ 
   (∀w∈ℕ. w \<ls> y \<ca> 𝟭 ⟶ w \<ls> y ∨ w = y)" by (rule MMI_cbvralv)
   from S179 S185 have S186: "y ∈ ℕ ⟶ 
   (∀z∈ℕ. z \<ls> y \<ca> 𝟭 ⟶ z \<ls> y ∨ z = y) ⟶ 
   (∀z∈ℕ. z \<ls> y \<ca> 𝟭 \<ca> 𝟭 ⟶ 
   z \<ls> y \<ca> 𝟭 ∨ z = y \<ca> 𝟭)" by (rule MMI_syl5ib)
   from S40 S47 S54 S61 S97 S186 have S187: "B ∈ ℕ ⟶ 
   (∀z∈ℕ. z \<ls> B \<ca> 𝟭 ⟶ z \<ls> B ∨ z = B)" by (rule MMI_nnind)
   from S33 S187 have S188: "A ∈ ℕ ⟶ 
   B ∈ ℕ ⟶ 
   A \<ls> B \<ca> 𝟭 ⟶ A \<ls> B ∨ A = B" by (rule MMI_syl5)
   from S188 have S189: "A ∈ ℕ ∧ B ∈ ℕ ⟶ 
   A \<ls> B \<ca> 𝟭 ⟶ A \<ls> B ∨ A = B" by (rule MMI_imp)
   from S27 S189 have S190: "A ∈ ℕ ∧ B ∈ ℕ ⟶ 
   A \<ls> B ∨ A = B ⟷ A \<ls> B \<ca> 𝟭" by (rule MMI_impbid)
   from S4 S190 show "A ∈ ℕ ∧ B ∈ ℕ ⟶ 
   A \<lsq> B ⟷ A \<ls> B \<ca> 𝟭" by (rule MMI_bitrd)
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 ∈ ℝ"