Theory MMI_Complex_ZF_1

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

    Copyright (C) 2006  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 1› 

theory MMI_Complex_ZF_1 imports MMI_examples

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 full atribution.
  This theory contains about 200 theorems.
›

(********211-220*************************)

lemma (in MMIsar0) MMI_recrect: 
   shows "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ 
 ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) = A"
proof -
   have S1: "A = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( 𝟭 \<cdiv> A ) = 
 ( 𝟭 \<cdiv> if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) )" by (rule MMI_opreq2)
   from S1 have S2: "A = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) = 
 ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ) )" 
     by (rule MMI_opreq2d)
   have S3: "A = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 A = if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 )" by (rule MMI_id)
   from S2 S3 have S4: "A = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) = 
 A ⟷ 
 ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ) ) = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) )" by (rule MMI_eqeq12d)
   have S5: "A = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( A ∈ ℂ ⟷ 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ∈ ℂ )" by (rule MMI_eleq1)
   have S6: "A = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( A ≠ 𝟬 ⟷ 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ≠ 𝟬 )" by (rule MMI_neeq1)
   from S5 S6 have S7: "A = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟷ 
 ( if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ∈ ℂ ∧ if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ≠ 𝟬 ) )" by (rule MMI_anbi12d)
   have S8: "𝟭 = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( 𝟭 ∈ ℂ ⟷ 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ∈ ℂ )" by (rule MMI_eleq1)
   have S9: "𝟭 = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( 𝟭 ≠ 𝟬 ⟷ 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ≠ 𝟬 )" by (rule MMI_neeq1)
   from S8 S9 have S10: "𝟭 = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ⟶ 
 ( ( 𝟭 ∈ ℂ ∧ 𝟭 ≠ 𝟬 ) ⟷ 
 ( if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ∈ ℂ ∧ if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ≠ 𝟬 ) )" by (rule MMI_anbi12d)
   have S11: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   have S12: "𝟭 ≠ 𝟬" by (rule MMI_ax1ne0)
   from S11 S12 have S13: "𝟭 ∈ ℂ ∧ 𝟭 ≠ 𝟬" by (rule MMI_pm3_2i)
   from S7 S10 S13 have S14: "if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ∈ ℂ ∧ if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ≠ 𝟬" by (rule MMI_elimhyp)
   from S14 have S15: "if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ∈ ℂ" by (rule MMI_pm3_26i)
   from S14 have S16: "if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ∈ ℂ ∧ if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ≠ 𝟬" .
   from S16 have S17: "if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ≠ 𝟬" by (rule MMI_pm3_27i)
   from S15 S17 have S18: "( 𝟭 \<cdiv> ( 𝟭 \<cdiv> if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 ) ) ) = 
 if ( ( A ∈ ℂ ∧ A ≠ 𝟬 ) , A , 𝟭 )" by (rule MMI_recrec)
   from S4 S18 show "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ 
 ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) = A" by (rule MMI_dedth)
qed

lemma (in MMIsar0) MMI_rec11i: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ" and
    A3: "A ≠ 𝟬" and
    A4: "B ≠ 𝟬"   
   shows "( 𝟭 \<cdiv> A ) = ( 𝟭 \<cdiv> B ) ⟷ A = B"
proof -
   have S1: "( 𝟭 \<cdiv> A ) = 
 ( 𝟭 \<cdiv> B ) ⟶ 
 ( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> A ) ) = 
 ( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> B ) )" by (rule MMI_opreq2)
   from A1 have S2: "A ∈ ℂ".
   from A2 have S3: "B ∈ ℂ".
   from A1 have S4: "A ∈ ℂ".
   from A3 have S5: "A ≠ 𝟬".
   from S4 S5 have S6: "( 𝟭 \<cdiv> A ) ∈ ℂ" by (rule MMI_reccl)
   from S2 S3 S6 have S7: "( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> A ) ) = 
 ( ( A ⋅ ( 𝟭 \<cdiv> A ) ) ⋅ B )" by (rule MMI_mul23)
   from A1 have S8: "A ∈ ℂ".
   from A3 have S9: "A ≠ 𝟬".
   from S8 S9 have S10: "( A ⋅ ( 𝟭 \<cdiv> A ) ) = 𝟭" by (rule MMI_recid)
   from S10 have S11: "( ( A ⋅ ( 𝟭 \<cdiv> A ) ) ⋅ B ) = ( 𝟭 ⋅ B )" by (rule MMI_opreq1i)
   from A2 have S12: "B ∈ ℂ".
   from S12 have S13: "( 𝟭 ⋅ B ) = B" by (rule MMI_mulid2)
   from S7 S11 S13 have S14: "( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> A ) ) = B" by (rule MMI_3eqtr)
   from A1 have S15: "A ∈ ℂ".
   from A2 have S16: "B ∈ ℂ".
   from A2 have S17: "B ∈ ℂ".
   from A4 have S18: "B ≠ 𝟬".
   from S17 S18 have S19: "( 𝟭 \<cdiv> B ) ∈ ℂ" by (rule MMI_reccl)
   from S15 S16 S19 have S20: "( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> B ) ) = 
 ( A ⋅ ( B ⋅ ( 𝟭 \<cdiv> B ) ) )" by (rule MMI_mulass)
   from A2 have S21: "B ∈ ℂ".
   from A4 have S22: "B ≠ 𝟬".
   from S21 S22 have S23: "( B ⋅ ( 𝟭 \<cdiv> B ) ) = 𝟭" by (rule MMI_recid)
   from S23 have S24: "( A ⋅ ( B ⋅ ( 𝟭 \<cdiv> B ) ) ) = ( A ⋅ 𝟭 )" by (rule MMI_opreq2i)
   from A1 have S25: "A ∈ ℂ".
   from S25 have S26: "( A ⋅ 𝟭 ) = A" by (rule MMI_mulid1)
   from S20 S24 S26 have S27: "( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> B ) ) = A" by (rule MMI_3eqtr)
   from S14 S27 have S28: "( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> A ) ) = 
 ( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> B ) ) ⟷ B = A" by (rule MMI_eqeq12i)
   have S29: "B = A ⟷ A = B" by (rule MMI_eqcom)
   from S28 S29 have S30: "( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> A ) ) = 
 ( ( A ⋅ B ) ⋅ ( 𝟭 \<cdiv> B ) ) ⟷ A = B" by (rule MMI_bitr)
   from S1 S30 have S31: "( 𝟭 \<cdiv> A ) = ( 𝟭 \<cdiv> B ) ⟶ A = B" by (rule MMI_sylib)
   have S32: "A = B ⟶ ( 𝟭 \<cdiv> A ) = ( 𝟭 \<cdiv> B )" by (rule MMI_opreq2)
   from S31 S32 show "( 𝟭 \<cdiv> A ) = ( 𝟭 \<cdiv> B ) ⟷ A = B" by (rule MMI_impbi)
qed

lemma (in MMIsar0) MMI_rec11: assumes A1: "A ∈ ℂ" and
    A2: "B ∈ ℂ"   
   shows "( A ≠ 𝟬 ∧ B ≠ 𝟬 ) ⟶ 
 ( ( 𝟭 \<cdiv> A ) = ( 𝟭 \<cdiv> B ) ⟷ A = B )"
proof -
   have S1: "A = 
 if ( A ≠ 𝟬 , A , 𝟭 ) ⟶ 
 ( 𝟭 \<cdiv> A ) = 
 ( 𝟭 \<cdiv> if ( A ≠ 𝟬 , A , 𝟭 ) )" by (rule MMI_opreq2)
   from S1 have S2: "A = 
 if ( A ≠ 𝟬 , A , 𝟭 ) ⟶ 
 ( ( 𝟭 \<cdiv> A ) = 
 ( 𝟭 \<cdiv> B ) ⟷ 
 ( 𝟭 \<cdiv> if ( A ≠ 𝟬 , A , 𝟭 ) ) = 
 ( 𝟭 \<cdiv> B ) )" by (rule MMI_eqeq1d)
   have S3: "A = 
 if ( A ≠ 𝟬 , A , 𝟭 ) ⟶ 
 ( A = B ⟷ if ( A ≠ 𝟬 , A , 𝟭 ) = B )" by (rule MMI_eqeq1)
   from S2 S3 have S4: "A = 
 if ( A ≠ 𝟬 , A , 𝟭 ) ⟶ 
 ( ( ( 𝟭 \<cdiv> A ) = ( 𝟭 \<cdiv> B ) ⟷ A = B ) ⟷ 
 ( ( 𝟭 \<cdiv> if ( A ≠ 𝟬 , A , 𝟭 ) ) = 
 ( 𝟭 \<cdiv> B ) ⟷ 
 if ( A ≠ 𝟬 , A , 𝟭 ) = B ) )" by (rule MMI_bibi12d)
   have S5: "B = 
 if ( B ≠ 𝟬 , B , 𝟭 ) ⟶ 
 ( 𝟭 \<cdiv> B ) = 
 ( 𝟭 \<cdiv> if ( B ≠ 𝟬 , B , 𝟭 ) )" by (rule MMI_opreq2)
   from S5 have S6: "B = 
 if ( B ≠ 𝟬 , B , 𝟭 ) ⟶ 
 ( ( 𝟭 \<cdiv> if ( A ≠ 𝟬 , A , 𝟭 ) ) = 
 ( 𝟭 \<cdiv> B ) ⟷ 
 ( 𝟭 \<cdiv> if ( A ≠ 𝟬 , A , 𝟭 ) ) = 
 ( 𝟭 \<cdiv> if ( B ≠ 𝟬 , B , 𝟭 ) ) )" by (rule MMI_eqeq2d)
   have S7: "B = 
 if ( B ≠ 𝟬 , B , 𝟭 ) ⟶ 
 ( if ( A ≠ 𝟬 , A , 𝟭 ) = 
 B ⟷ 
 if ( A ≠ 𝟬 , A , 𝟭 ) = 
 if ( B ≠ 𝟬 , B , 𝟭 ) )" by (rule MMI_eqeq2)
   from S6 S7 have S8: "B = 
 if ( B ≠ 𝟬 , B , 𝟭 ) ⟶ 
 ( ( ( 𝟭 \<cdiv> if ( A ≠ 𝟬 , A , 𝟭 ) ) = ( 𝟭 \<cdiv> B ) ⟷ if ( A ≠ 𝟬 , A , 𝟭 ) = B ) ⟷ 
 ( ( 𝟭 \<cdiv> if ( A ≠ 𝟬 , A , 𝟭 ) ) = 
 ( 𝟭 \<cdiv> if ( B ≠ 𝟬 , B , 𝟭 ) ) ⟷ 
 if ( A ≠ 𝟬 , A , 𝟭 ) = 
 if ( B ≠ 𝟬 , B , 𝟭 ) ) )" by (rule MMI_bibi12d)
   from A1 have S9: "A ∈ ℂ".
   have S10: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   from S9 S10 have S11: "if ( A ≠ 𝟬 , A , 𝟭 ) ∈ ℂ" by (rule MMI_keepel)
   from A2 have S12: "B ∈ ℂ".
   have S13: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   from S12 S13 have S14: "if ( B ≠ 𝟬 , B , 𝟭 ) ∈ ℂ" by (rule MMI_keepel)
   have S15: "if ( A ≠ 𝟬 , A , 𝟭 ) ≠ 𝟬" by (rule MMI_elimne0)
   have S16: "if ( B ≠ 𝟬 , B , 𝟭 ) ≠ 𝟬" by (rule MMI_elimne0)
   from S11 S14 S15 S16 have S17: "( 𝟭 \<cdiv> if ( A ≠ 𝟬 , A , 𝟭 ) ) = 
 ( 𝟭 \<cdiv> if ( B ≠ 𝟬 , B , 𝟭 ) ) ⟷ 
 if ( A ≠ 𝟬 , A , 𝟭 ) = 
 if ( B ≠ 𝟬 , B , 𝟭 )" by (rule MMI_rec11i)
   from S4 S8 S17 show "( A ≠ 𝟬 ∧ B ≠ 𝟬 ) ⟶ 
 ( ( 𝟭 \<cdiv> A ) = ( 𝟭 \<cdiv> B ) ⟷ A = B )" by (rule MMI_dedth2h)
qed

lemma (in MMIsar0) MMI_divmuldivt: 
   shows "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) )"
proof -
   have S1: "( ( B ⋅ D ) ∈ ℂ ∧ ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ∈ ℂ ∧ ( B ⋅ D ) ≠ 𝟬 ) ⟶ 
 ( ( ( B ⋅ D ) ⋅ ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) )" by (rule MMI_divcan3t)
   have S2: "( B ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( B ⋅ D ) ∈ ℂ" by (rule MMI_axmulcl)
   from S2 have S3: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( B ⋅ D ) ∈ ℂ" by (rule MMI_ad2ant2l)
   from S3 have S4: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( B ⋅ D ) ∈ ℂ" by (rule MMI_adantr)
   have S5: "( ( A \<cdiv> B ) ∈ ℂ ∧ ( C \<cdiv> D ) ∈ ℂ ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ∈ ℂ" by (rule MMI_axmulcl)
   have S6: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_divclt)
   from S6 have S7: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_3expa)
   have S8: "( C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 𝟬 ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" by (rule MMI_divclt)
   from S8 have S9: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" by (rule MMI_3expa)
   from S5 S7 S9 have S10: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ∧ ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ∈ ℂ" by (rule MMI_syl2an)
   from S10 have S11: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ∈ ℂ" by (rule MMI_an4s)
   have S12: "( B ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
 ( ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟷ ( B ⋅ D ) ≠ 𝟬 )" by (rule MMI_muln0bt)
   from S12 have S13: "( B ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
 ( ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟶ ( B ⋅ D ) ≠ 𝟬 )" by (rule MMI_biimpd)
   from S13 have S14: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟶ ( B ⋅ D ) ≠ 𝟬 )" by (rule MMI_ad2ant2l)
   from S14 have S15: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( B ⋅ D ) ≠ 𝟬" by (rule MMI_imp)
   from S1 S4 S11 S15 have S16: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( ( B ⋅ D ) ⋅ ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) )" by (rule MMI_syl3anc)
   have S17: "( ( B ∈ ℂ ∧ ( A \<cdiv> B ) ∈ ℂ ) ∧ ( D ∈ ℂ ∧ ( C \<cdiv> D ) ∈ ℂ ) ) ⟶ 
 ( ( B ⋅ ( A \<cdiv> B ) ) ⋅ ( D ⋅ ( C \<cdiv> D ) ) ) = 
 ( ( B ⋅ D ) ⋅ ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) )" by (rule MMI_mul4t)
   have S18: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ B ∈ ℂ" by (rule MMI_3simp2)
   from S6 have S19: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" .
   from S18 S19 have S20: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( B ∈ ℂ ∧ ( A \<cdiv> B ) ∈ ℂ )" by (rule MMI_jca)
   from S20 have S21: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ⟶ 
 ( B ∈ ℂ ∧ ( A \<cdiv> B ) ∈ ℂ )" by (rule MMI_3expa)
   have S22: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ D ∈ ℂ" by (rule MMI_pm3_27)
   from S22 have S23: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ⟶ D ∈ ℂ" by (rule MMI_adantr)
   from S9 have S24: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" .
   from S23 S24 have S25: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ⟶ 
 ( D ∈ ℂ ∧ ( C \<cdiv> D ) ∈ ℂ )" by (rule MMI_jca)
   from S17 S21 S25 have S26: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ∧ ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( B ⋅ ( A \<cdiv> B ) ) ⋅ ( D ⋅ ( C \<cdiv> D ) ) ) = 
 ( ( B ⋅ D ) ⋅ ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) )" by (rule MMI_syl2an)
   have S27: "( B ∈ ℂ ∧ A ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( B ⋅ ( A \<cdiv> B ) ) = A" by (rule MMI_divcan2t)
   from S27 have S28: "B ∈ ℂ ⟶ 
 ( A ∈ ℂ ⟶ 
 ( B ≠ 𝟬 ⟶ ( B ⋅ ( A \<cdiv> B ) ) = A ) )" by (rule MMI_3exp)
   from S28 have S29: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ 
 ( B ≠ 𝟬 ⟶ ( B ⋅ ( A \<cdiv> B ) ) = A )" by (rule MMI_impcom)
   from S29 have S30: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ⟶ 
 ( B ⋅ ( A \<cdiv> B ) ) = A" by (rule MMI_imp)
   have S31: "( D ∈ ℂ ∧ C ∈ ℂ ∧ D ≠ 𝟬 ) ⟶ 
 ( D ⋅ ( C \<cdiv> D ) ) = C" by (rule MMI_divcan2t)
   from S31 have S32: "( C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 𝟬 ) ⟶ 
 ( D ⋅ ( C \<cdiv> D ) ) = C" by (rule MMI_3com12)
   from S32 have S33: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ⟶ 
 ( D ⋅ ( C \<cdiv> D ) ) = C" by (rule MMI_3expa)
   from S30 S33 have S34: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ∧ ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( B ⋅ ( A \<cdiv> B ) ) ⋅ ( D ⋅ ( C \<cdiv> D ) ) ) = 
 ( A ⋅ C )" by (rule MMI_opreqan12d)
   from S26 S34 have S35: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ∧ ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( B ⋅ D ) ⋅ ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ) = 
 ( A ⋅ C )" by (rule MMI_eqtr3d)
   from S35 have S36: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( B ⋅ D ) ⋅ ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ) = 
 ( A ⋅ C )" by (rule MMI_an4s)
   from S36 have S37: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( ( B ⋅ D ) ⋅ ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_opreq1d)
   from S16 S37 show "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_eqtr3d)
qed

lemma (in MMIsar0) MMI_divcan5t: 
   shows "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( C ⋅ A ) \<cdiv> ( C ⋅ B ) ) = ( A \<cdiv> B )"
proof -
   have S1: "( C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ ( C \<cdiv> C ) = 𝟭" by (rule MMI_dividt)
   from S1 have S2: "( C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( ( C \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) = 
 ( 𝟭 ⋅ ( A \<cdiv> B ) )" by (rule MMI_opreq1d)
   from S2 have S3: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( C \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) = 
 ( 𝟭 ⋅ ( A \<cdiv> B ) )" by (rule MMI_3ad2ant3)
   have S4: "( ( ( C ∈ ℂ ∧ C ∈ ℂ ) ∧ ( A ∈ ℂ ∧ B ∈ ℂ ) ) ∧ ( C ≠ 𝟬 ∧ B ≠ 𝟬 ) ) ⟶ 
 ( ( C \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) = 
 ( ( C ⋅ A ) \<cdiv> ( C ⋅ B ) )" by (rule MMI_divmuldivt)
   have S5: "( C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ C ∈ ℂ" by (rule MMI_pm3_26)
   from S5 have S6: "( C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ C ∈ ℂ" .
   from S5 S6 have S7: "( C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ ( C ∈ ℂ ∧ C ∈ ℂ )" by (rule MMI_jca)
   have S8: "( B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ B ∈ ℂ" by (rule MMI_pm3_26)
   from S8 have S9: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ) ⟶ 
 ( A ∈ ℂ ∧ B ∈ ℂ )" by (rule MMI_anim2i)
   from S7 S9 have S10: "( ( C ∈ ℂ ∧ C ≠ 𝟬 ) ∧ ( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ) ) ⟶ 
 ( ( C ∈ ℂ ∧ C ∈ ℂ ) ∧ ( A ∈ ℂ ∧ B ∈ ℂ ) )" by (rule MMI_anim12i)
   from S10 have S11: "( ( C ∈ ℂ ∧ C ≠ 𝟬 ) ∧ A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ) ⟶ 
 ( ( C ∈ ℂ ∧ C ∈ ℂ ) ∧ ( A ∈ ℂ ∧ B ∈ ℂ ) )" by (rule MMI_3impb)
   from S11 have S12: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( C ∈ ℂ ∧ C ∈ ℂ ) ∧ ( A ∈ ℂ ∧ B ∈ ℂ ) )" by (rule MMI_3coml)
   have S13: "( C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ C ≠ 𝟬" by (rule MMI_pm3_27)
   have S14: "( B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ B ≠ 𝟬" by (rule MMI_pm3_27)
   from S13 S14 have S15: "( ( C ∈ ℂ ∧ C ≠ 𝟬 ) ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ) ⟶ 
 ( C ≠ 𝟬 ∧ B ≠ 𝟬 )" by (rule MMI_anim12i)
   from S15 have S16: "( ( B ∈ ℂ ∧ B ≠ 𝟬 ) ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( C ≠ 𝟬 ∧ B ≠ 𝟬 )" by (rule MMI_ancoms)
   from S16 have S17: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( C ≠ 𝟬 ∧ B ≠ 𝟬 )" by (rule MMI_3adant1)
   from S4 S12 S17 have S18: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( C \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) = 
 ( ( C ⋅ A ) \<cdiv> ( C ⋅ B ) )" by (rule MMI_sylanc)
   have S19: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_divclt)
   from S19 have S20: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_3expb)
   have S21: "( A \<cdiv> B ) ∈ ℂ ⟶ 
 ( 𝟭 ⋅ ( A \<cdiv> B ) ) = ( A \<cdiv> B )" by (rule MMI_mulid2t)
   from S20 S21 have S22: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ) ⟶ 
 ( 𝟭 ⋅ ( A \<cdiv> B ) ) = ( A \<cdiv> B )" by (rule MMI_syl)
   from S22 have S23: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( 𝟭 ⋅ ( A \<cdiv> B ) ) = ( A \<cdiv> B )" by (rule MMI_3adant3)
   from S3 S18 S23 show "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( C ⋅ A ) \<cdiv> ( C ⋅ B ) ) = ( A \<cdiv> B )" by (rule MMI_3eqtr3d)
qed

lemma (in MMIsar0) MMI_divmul13t: 
   shows "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( C \<cdiv> B ) ⋅ ( A \<cdiv> D ) )"
proof -
   have S1: "( A ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
 ( A ⋅ C ) = ( C ⋅ A )" by (rule MMI_axmulcom)
   from S1 have S2: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( A ⋅ C ) = ( C ⋅ A )" by (rule MMI_ad2ant2r)
   from S2 have S3: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( C ⋅ A ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_opreq1d)
   from S3 have S4: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( C ⋅ A ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_adantr)
   have S5: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_divmuldivt)
   have S6: "( ( ( C ∈ ℂ ∧ B ∈ ℂ ) ∧ ( A ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( C \<cdiv> B ) ⋅ ( A \<cdiv> D ) ) = 
 ( ( C ⋅ A ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_divmuldivt)
   have S7: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟷ ( B ∈ ℂ ∧ A ∈ ℂ )" by (rule MMI_ancom)
   from S7 have S8: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟷ 
 ( ( B ∈ ℂ ∧ A ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) )" by (rule MMI_anbi1i)
   have S9: "( ( B ∈ ℂ ∧ A ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟷ 
 ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( B ∈ ℂ ∧ A ∈ ℂ ) )" by (rule MMI_ancom)
   have S10: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( B ∈ ℂ ∧ A ∈ ℂ ) ) ⟷ 
 ( ( C ∈ ℂ ∧ B ∈ ℂ ) ∧ ( A ∈ ℂ ∧ D ∈ ℂ ) )" by (rule MMI_an42)
   from S8 S9 S10 have S11: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟷ 
 ( ( C ∈ ℂ ∧ B ∈ ℂ ) ∧ ( A ∈ ℂ ∧ D ∈ ℂ ) )" by (rule MMI_3bitr)
   from S6 S11 have S12: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( C \<cdiv> B ) ⋅ ( A \<cdiv> D ) ) = 
 ( ( C ⋅ A ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_sylanb)
   from S4 S5 S12 show "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( C \<cdiv> B ) ⋅ ( A \<cdiv> D ) )" by (rule MMI_3eqtr4d)
qed

lemma (in MMIsar0) MMI_divmul24t: 
   shows "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( A \<cdiv> D ) ⋅ ( C \<cdiv> B ) )"
proof -
   have S1: "( B ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
 ( B ⋅ D ) = ( D ⋅ B )" by (rule MMI_axmulcom)
   from S1 have S2: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( B ⋅ D ) = ( D ⋅ B )" by (rule MMI_ad2ant2l)
   from S2 have S3: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( D ⋅ B ) )" by (rule MMI_opreq2d)
   from S3 have S4: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( D ⋅ B ) )" by (rule MMI_adantr)
   have S5: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_divmuldivt)
   have S6: "( ( ( A ∈ ℂ ∧ D ∈ ℂ ) ∧ ( C ∈ ℂ ∧ B ∈ ℂ ) ) ∧ ( D ≠ 𝟬 ∧ B ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> D ) ⋅ ( C \<cdiv> B ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( D ⋅ B ) )" by (rule MMI_divmuldivt)
   have S7: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟷ 
 ( ( A ∈ ℂ ∧ C ∈ ℂ ) ∧ ( D ∈ ℂ ∧ B ∈ ℂ ) )" by (rule MMI_an42)
   have S8: "( ( A ∈ ℂ ∧ C ∈ ℂ ) ∧ ( D ∈ ℂ ∧ B ∈ ℂ ) ) ⟷ 
 ( ( A ∈ ℂ ∧ D ∈ ℂ ) ∧ ( C ∈ ℂ ∧ B ∈ ℂ ) )" by (rule MMI_an4)
   from S7 S8 have S9: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟷ 
 ( ( A ∈ ℂ ∧ D ∈ ℂ ) ∧ ( C ∈ ℂ ∧ B ∈ ℂ ) )" by (rule MMI_bitr)
   have S10: "( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟷ ( D ≠ 𝟬 ∧ B ≠ 𝟬 )" by (rule MMI_ancom)
   from S6 S9 S10 have S11: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> D ) ⋅ ( C \<cdiv> B ) ) = 
 ( ( A ⋅ C ) \<cdiv> ( D ⋅ B ) )" by (rule MMI_syl2anb)
   from S4 S5 S11 show "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( A \<cdiv> D ) ⋅ ( C \<cdiv> B ) )" by (rule MMI_3eqtr4d)
qed

lemma (in MMIsar0) MMI_divadddivt: 
   shows "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) \<ca> ( C \<cdiv> D ) ) = 
 ( ( ( A ⋅ D ) \<ca> ( B ⋅ C ) ) \<cdiv> ( B ⋅ D ) )"
proof -
   have S1: "( B ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
 ( ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟷ ( B ⋅ D ) ≠ 𝟬 )" by (rule MMI_muln0bt)
   from S1 have S2: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟷ ( B ⋅ D ) ≠ 𝟬 )" by (rule MMI_ad2ant2l)
   have S3: "( ( ( A ⋅ D ) ∈ ℂ ∧ ( B ⋅ C ) ∈ ℂ ∧ ( B ⋅ D ) ∈ ℂ ) ∧ ( B ⋅ D ) ≠ 𝟬 ) ⟶ 
 ( ( ( A ⋅ D ) \<ca> ( B ⋅ C ) ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) ) \<ca> ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) ) )" by (rule MMI_divdirt)
   from S3 have S4: "( ( A ⋅ D ) ∈ ℂ ∧ ( B ⋅ C ) ∈ ℂ ∧ ( B ⋅ D ) ∈ ℂ ) ⟶ 
 ( ( B ⋅ D ) ≠ 𝟬 ⟶ 
 ( ( ( A ⋅ D ) \<ca> ( B ⋅ C ) ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) ) \<ca> ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) ) ) )" by (rule MMI_ex)
   have S5: "( A ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( A ⋅ D ) ∈ ℂ" by (rule MMI_axmulcl)
   from S5 have S6: "( A ∈ ℂ ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( A ⋅ D ) ∈ ℂ" by (rule MMI_adantrl)
   from S6 have S7: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( A ⋅ D ) ∈ ℂ" by (rule MMI_adantlr)
   have S8: "( B ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( B ⋅ C ) ∈ ℂ" by (rule MMI_axmulcl)
   from S8 have S9: "( B ∈ ℂ ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( B ⋅ C ) ∈ ℂ" by (rule MMI_adantrr)
   from S9 have S10: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( B ⋅ C ) ∈ ℂ" by (rule MMI_adantll)
   have S11: "( B ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( B ⋅ D ) ∈ ℂ" by (rule MMI_axmulcl)
   from S11 have S12: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( B ⋅ D ) ∈ ℂ" by (rule MMI_ad2ant2l)
   from S4 S7 S10 S12 have S13: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( ( B ⋅ D ) ≠ 𝟬 ⟶ 
 ( ( ( A ⋅ D ) \<ca> ( B ⋅ C ) ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) ) \<ca> ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) ) ) )" by (rule MMI_syl3anc)
   from S2 S13 have S14: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟶ 
 ( ( ( A ⋅ D ) \<ca> ( B ⋅ C ) ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) ) \<ca> ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) ) ) )" by (rule MMI_sylbid)
   from S14 have S15: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( ( A ⋅ D ) \<ca> ( B ⋅ C ) ) \<cdiv> ( B ⋅ D ) ) = 
 ( ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) ) \<ca> ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) ) )" by (rule MMI_imp)
   have S16: "( D ∈ ℂ ∧ D ≠ 𝟬 ) ⟶ ( D \<cdiv> D ) = 𝟭" by (rule MMI_dividt)
   from S16 have S17: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( D \<cdiv> D ) = 𝟭" by (rule MMI_ad2ant2l)
   from S17 have S18: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( D \<cdiv> D ) = 𝟭" by (rule MMI_adantll)
   from S18 have S19: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( D \<cdiv> D ) ) = 
 ( ( A \<cdiv> B ) ⋅ 𝟭 )" by (rule MMI_opreq2d)
   have S20: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( D ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( D \<cdiv> D ) ) = 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_divmuldivt)
   have S21: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ D ∈ ℂ" by (rule MMI_pm3_27)
   from S21 have S22: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ D ∈ ℂ" .
   from S21 S22 have S23: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( D ∈ ℂ ∧ D ∈ ℂ )" by (rule MMI_jca)
   from S20 S23 have S24: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( D \<cdiv> D ) ) = 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_sylanl2)
   have S25: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_divclt)
   from S25 have S26: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_3expa)
   have S27: "( A \<cdiv> B ) ∈ ℂ ⟶ 
 ( ( A \<cdiv> B ) ⋅ 𝟭 ) = ( A \<cdiv> B )" by (rule MMI_ax1id)
   from S26 S27 have S28: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ 𝟭 ) = ( A \<cdiv> B )" by (rule MMI_syl)
   from S28 have S29: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ 𝟭 ) = ( A \<cdiv> B )" by (rule MMI_ad2ant2r)
   from S19 S24 S29 have S30: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) ) = ( A \<cdiv> B )" by (rule MMI_3eqtr3d)
   have S31: "( B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ ( B \<cdiv> B ) = 𝟭" by (rule MMI_dividt)
   from S31 have S32: "( B ∈ ℂ ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( B \<cdiv> B ) = 𝟭" by (rule MMI_adantrr)
   from S32 have S33: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( B \<cdiv> B ) = 𝟭" by (rule MMI_adantll)
   from S33 have S34: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( B \<cdiv> B ) = 𝟭" by (rule MMI_adantlr)
   from S34 have S35: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( B \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( 𝟭 ⋅ ( C \<cdiv> D ) )" by (rule MMI_opreq1d)
   have S36: "( ( ( B ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( B \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_divmuldivt)
   have S37: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ B ∈ ℂ" by (rule MMI_pm3_27)
   from S37 have S38: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ B ∈ ℂ" .
   from S37 S38 have S39: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ ( B ∈ ℂ ∧ B ∈ ℂ )" by (rule MMI_jca)
   from S36 S39 have S40: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( B \<cdiv> B ) ⋅ ( C \<cdiv> D ) ) = 
 ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_sylanl1)
   have S41: "( C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 𝟬 ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" by (rule MMI_divclt)
   from S41 have S42: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" by (rule MMI_3expa)
   have S43: "( C \<cdiv> D ) ∈ ℂ ⟶ 
 ( 𝟭 ⋅ ( C \<cdiv> D ) ) = ( C \<cdiv> D )" by (rule MMI_mulid2t)
   from S42 S43 have S44: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ⟶ 
 ( 𝟭 ⋅ ( C \<cdiv> D ) ) = ( C \<cdiv> D )" by (rule MMI_syl)
   from S44 have S45: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( 𝟭 ⋅ ( C \<cdiv> D ) ) = ( C \<cdiv> D )" by (rule MMI_ad2ant2l)
   from S35 S40 S45 have S46: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) ) = ( C \<cdiv> D )" by (rule MMI_3eqtr3d)
   from S30 S46 have S47: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( ( A ⋅ D ) \<cdiv> ( B ⋅ D ) ) \<ca> ( ( B ⋅ C ) \<cdiv> ( B ⋅ D ) ) ) = 
 ( ( A \<cdiv> B ) \<ca> ( C \<cdiv> D ) )" by (rule MMI_opreq12d)
   from S15 S47 show "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) \<ca> ( C \<cdiv> D ) ) = 
 ( ( ( A ⋅ D ) \<ca> ( B ⋅ C ) ) \<cdiv> ( B ⋅ D ) )" by (rule MMI_eqtr2d)
qed

lemma (in MMIsar0) MMI_divdivdivt: 
   shows "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) \<cdiv> ( C \<cdiv> D ) ) = 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) )"
proof -
   have S1: "( ( D \<cdiv> C ) ∈ ℂ ∧ ( A \<cdiv> B ) ∈ ℂ ) ⟶ 
 ( ( D \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) = 
 ( ( A \<cdiv> B ) ⋅ ( D \<cdiv> C ) )" by (rule MMI_axmulcom)
   have S2: "( D ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( D \<cdiv> C ) ∈ ℂ" by (rule MMI_divclt)
   from S2 have S3: "( C ∈ ℂ ∧ D ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( D \<cdiv> C ) ∈ ℂ" by (rule MMI_3com12)
   from S3 have S4: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( D \<cdiv> C ) ∈ ℂ" by (rule MMI_3expa)
   from S4 have S5: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( D \<cdiv> C ) ∈ ℂ" by (rule MMI_adantrr)
   from S5 have S6: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( D \<cdiv> C ) ∈ ℂ" by (rule MMI_ad2ant2l)
   have S7: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_divclt)
   from S7 have S8: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_3expa)
   from S8 have S9: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" by (rule MMI_ad2ant2r)
   from S1 S6 S9 have S10: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( D \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) = 
 ( ( A \<cdiv> B ) ⋅ ( D \<cdiv> C ) )" by (rule MMI_sylanc)
   have S11: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( D ∈ ℂ ∧ C ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( D \<cdiv> C ) ) = 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) )" by (rule MMI_divmuldivt)
   have S12: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( D ∈ ℂ ∧ C ∈ ℂ )" by (rule MMI_pm3_22)
   from S12 have S13: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( D ∈ ℂ ∧ C ∈ ℂ ) )" by (rule MMI_anim2i)
   have S14: "( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟶ C ≠ 𝟬" by (rule MMI_pm3_26)
   from S14 have S15: "( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( B ≠ 𝟬 ∧ C ≠ 𝟬 )" by (rule MMI_anim2i)
   from S11 S13 S15 have S16: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( A \<cdiv> B ) ⋅ ( D \<cdiv> C ) ) = 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) )" by (rule MMI_syl2an)
   from S10 S16 have S17: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( D \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) = 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) )" by (rule MMI_eqtrd)
   from S17 have S18: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( C \<cdiv> D ) ⋅ ( ( D \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) ) = 
 ( ( C \<cdiv> D ) ⋅ ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) ) )" by (rule MMI_opreq2d)
   from S12 have S19: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( D ∈ ℂ ∧ C ∈ ℂ )" .
   from S19 have S20: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
 ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( D ∈ ℂ ∧ C ∈ ℂ ) )" by (rule MMI_ancli)
   have S21: "( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟶ ( D ≠ 𝟬 ∧ C ≠ 𝟬 )" by (rule MMI_pm3_22)
   from S21 have S22: "( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( D ≠ 𝟬 ∧ C ≠ 𝟬 )" by (rule MMI_adantl)
   from S20 S22 have S23: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( D ∈ ℂ ∧ C ∈ ℂ ) ) ∧ ( D ≠ 𝟬 ∧ C ≠ 𝟬 ) )" by (rule MMI_anim12i)
   from S23 have S24: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( D ∈ ℂ ∧ C ∈ ℂ ) ) ∧ ( D ≠ 𝟬 ∧ C ≠ 𝟬 ) )" by (rule MMI_adantll)
   have S25: "( ( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( D ∈ ℂ ∧ C ∈ ℂ ) ) ∧ ( D ≠ 𝟬 ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( C \<cdiv> D ) ⋅ ( D \<cdiv> C ) ) = 
 ( ( C ⋅ D ) \<cdiv> ( D ⋅ C ) )" by (rule MMI_divmuldivt)
   from S24 S25 have S26: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( C \<cdiv> D ) ⋅ ( D \<cdiv> C ) ) = 
 ( ( C ⋅ D ) \<cdiv> ( D ⋅ C ) )" by (rule MMI_syl)
   have S27: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
 ( C ⋅ D ) = ( D ⋅ C )" by (rule MMI_axmulcom)
   from S27 have S28: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( C ⋅ D ) = ( D ⋅ C )" by (rule MMI_ad2antlr)
   from S28 have S29: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( C ⋅ D ) \<cdiv> ( D ⋅ C ) ) = 
 ( ( D ⋅ C ) \<cdiv> ( D ⋅ C ) )" by (rule MMI_opreq1d)
   have S30: "( ( D ⋅ C ) ∈ ℂ ∧ ( D ⋅ C ) ≠ 𝟬 ) ⟶ 
 ( ( D ⋅ C ) \<cdiv> ( D ⋅ C ) ) = 𝟭" by (rule MMI_dividt)
   have S31: "( D ∈ ℂ ∧ C ∈ ℂ ) ⟶ ( D ⋅ C ) ∈ ℂ" by (rule MMI_axmulcl)
   from S31 have S32: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( D ⋅ C ) ∈ ℂ" by (rule MMI_ancoms)
   from S32 have S33: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( D ⋅ C ) ∈ ℂ" by (rule MMI_ad2antlr)
   have S34: "( D ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
 ( ( D ≠ 𝟬 ∧ C ≠ 𝟬 ) ⟷ ( D ⋅ C ) ≠ 𝟬 )" by (rule MMI_muln0bt)
   have S35: "( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟷ ( D ≠ 𝟬 ∧ C ≠ 𝟬 )" by (rule MMI_ancom)
   from S34 S35 have S36: "( D ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
 ( ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟷ ( D ⋅ C ) ≠ 𝟬 )" by (rule MMI_syl5bb)
   from S36 have S37: "( C ∈ ℂ ∧ D ∈ ℂ ) ⟶ 
 ( ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ⟷ ( D ⋅ C ) ≠ 𝟬 )" by (rule MMI_ancoms)
   from S37 have S38: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( D ⋅ C ) ≠ 𝟬" by (rule MMI_biimpa)
   from S38 have S39: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( D ⋅ C ) ≠ 𝟬" by (rule MMI_ad2ant2l)
   from S30 S33 S39 have S40: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( D ⋅ C ) \<cdiv> ( D ⋅ C ) ) = 𝟭" by (rule MMI_sylanc)
   from S26 S29 S40 have S41: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( C \<cdiv> D ) ⋅ ( D \<cdiv> C ) ) = 𝟭" by (rule MMI_3eqtrd)
   from S41 have S42: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( ( C \<cdiv> D ) ⋅ ( D \<cdiv> C ) ) ⋅ ( A \<cdiv> B ) ) = 
 ( 𝟭 ⋅ ( A \<cdiv> B ) )" by (rule MMI_opreq1d)
   have S43: "( ( C \<cdiv> D ) ∈ ℂ ∧ ( D \<cdiv> C ) ∈ ℂ ∧ ( A \<cdiv> B ) ∈ ℂ ) ⟶ 
 ( ( ( C \<cdiv> D ) ⋅ ( D \<cdiv> C ) ) ⋅ ( A \<cdiv> B ) ) = 
 ( ( C \<cdiv> D ) ⋅ ( ( D \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) )" by (rule MMI_axmulass)
   have S44: "( C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 𝟬 ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" by (rule MMI_divclt)
   from S44 have S45: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ D ≠ 𝟬 ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" by (rule MMI_3expa)
   from S45 have S46: "( ( C ∈ ℂ ∧ D ∈ ℂ ) ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" by (rule MMI_adantrl)
   from S46 have S47: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" by (rule MMI_ad2ant2l)
   from S6 have S48: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( D \<cdiv> C ) ∈ ℂ" .
   from S9 have S49: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" .
   from S43 S47 S48 S49 have S50: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( ( C \<cdiv> D ) ⋅ ( D \<cdiv> C ) ) ⋅ ( A \<cdiv> B ) ) = 
 ( ( C \<cdiv> D ) ⋅ ( ( D \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) )" by (rule MMI_syl3anc)
   from S9 have S51: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" .
   have S52: "( A \<cdiv> B ) ∈ ℂ ⟶ 
 ( 𝟭 ⋅ ( A \<cdiv> B ) ) = ( A \<cdiv> B )" by (rule MMI_mulid2t)
   from S51 S52 have S53: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( 𝟭 ⋅ ( A \<cdiv> B ) ) = ( A \<cdiv> B )" by (rule MMI_syl)
   from S42 S50 S53 have S54: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( C \<cdiv> D ) ⋅ ( ( D \<cdiv> C ) ⋅ ( A \<cdiv> B ) ) ) = 
 ( A \<cdiv> B )" by (rule MMI_3eqtr3d)
   from S18 S54 have S55: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( ( C \<cdiv> D ) ⋅ ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) ) ) = 
 ( A \<cdiv> B )" by (rule MMI_eqtr3d)
   have S56: "( ( ( A \<cdiv> B ) ∈ ℂ ∧ ( C \<cdiv> D ) ∈ ℂ ∧ ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) ) ∈ ℂ ) ∧ ( C \<cdiv> D ) ≠ 𝟬 ) ⟶ 
 ( ( ( A \<cdiv> B ) \<cdiv> ( C \<cdiv> D ) ) = 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) ) ⟷ 
 ( ( C \<cdiv> D ) ⋅ ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) ) ) = 
 ( A \<cdiv> B ) )" by (rule MMI_divmult)
   from S9 have S57: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( A \<cdiv> B ) ∈ ℂ" .
   from S47 have S58: "( ( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ∧ ( B ≠ 𝟬 ∧ ( C ≠ 𝟬 ∧ D ≠ 𝟬 ) ) ) ⟶ 
 ( C \<cdiv> D ) ∈ ℂ" .
   have S59: "( ( A ⋅ D ) ∈ ℂ ∧ ( B ⋅ C ) ∈ ℂ ∧ ( B ⋅ C ) ≠ 𝟬 ) ⟶ 
 ( ( A ⋅ D ) \<cdiv> ( B ⋅ C ) ) ∈ ℂ" by (rule MMI_divclt)
   have S60: "( A ∈ ℂ ∧ D ∈ ℂ ) ⟶ ( A ⋅ D ) ∈ ℂ" by (rule MMI_axmulcl)
   from S60 have S61: "( A ∈ ℂ ∧ ( C ∈ ℂ ∧ D ∈ ℂ ) ) ⟶ 
 ( A ⋅ D ) ∈ ℂ" by (rule MMI_adantrl)
   from S61 have S62: "( ( A ∈ ℂ ∧ B ∈ ℂ ) ∧ ( C ∈ ℂ ∧ D ∈ ℂ )