Theory MMI_examples

(* 
    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 ‹Metamath examples›

theory MMI_examples imports MMI_Complex_ZF

begin 

text‹This theory contains 10 theorems translated from 
  Metamath (with proofs). It is included
  in the proof document as an illustration of how a translated
  Metamath proof looks like. The "known\_theorems.txt"
  file included in the IsarMathLib distribution provides
  a list of all translated facts.›

(******201-210****************************)

lemma (in MMIsar0) MMI_dividt: 
   shows "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ ( A \<cdiv> A ) = 𝟭"
proof -
   have S1: "( A ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> A ) = ( A ⋅ ( 𝟭 \<cdiv> A ) )" by (rule MMI_divrect)
   from S1 have S2: "( ( A ∈ ℂ ∧ A ∈ ℂ ) ∧ A ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> A ) = ( A ⋅ ( 𝟭 \<cdiv> A ) )" by (rule MMI_3expa)
   from S2 have S3: "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> A ) = ( A ⋅ ( 𝟭 \<cdiv> A ) )" by (rule MMI_anabsan)
   have S4: "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ 
 ( A ⋅ ( 𝟭 \<cdiv> A ) ) = 𝟭" by (rule MMI_recidt)
   from S3 S4 show "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ ( A \<cdiv> A ) = 𝟭" by (rule MMI_eqtrd)
qed

lemma (in MMIsar0) MMI_div0t: 
   shows "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ ( 𝟬 \<cdiv> A ) = 𝟬"
proof -
   have S1: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   have S2: "( 𝟬 ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ 
 ( 𝟬 \<cdiv> A ) = ( 𝟬 ⋅ ( 𝟭 \<cdiv> A ) )" by (rule MMI_divrect)
   from S1 S2 have S3: "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ 
 ( 𝟬 \<cdiv> A ) = ( 𝟬 ⋅ ( 𝟭 \<cdiv> A ) )" by (rule MMI_mp3an1)
   have S4: "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ ( 𝟭 \<cdiv> A ) ∈ ℂ" by (rule MMI_recclt)
   have S5: "( 𝟭 \<cdiv> A ) ∈ ℂ ⟶ ( 𝟬 ⋅ ( 𝟭 \<cdiv> A ) ) = 𝟬" 
     by (rule MMI_mul02t)
   from S4 S5 have S6: "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ 
 ( 𝟬 ⋅ ( 𝟭 \<cdiv> A ) ) = 𝟬" by (rule MMI_syl)
   from S3 S6 show "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ ( 𝟬 \<cdiv> A ) = 𝟬" by (rule MMI_eqtrd)
qed

lemma (in MMIsar0) MMI_diveq0t: 
   shows "( A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> C ) = 𝟬 ⟷ A = 𝟬 )"
proof -
   have S1: "( C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ ( 𝟬 \<cdiv> C ) = 𝟬" by (rule MMI_div0t)
   from S1 have S2: "( C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> C ) = 
 ( 𝟬 \<cdiv> C ) ⟷ ( A \<cdiv> C ) = 𝟬 )" by (rule MMI_eqeq2d)
   from S2 have S3: "( A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> C ) = 
 ( 𝟬 \<cdiv> C ) ⟷ ( A \<cdiv> C ) = 𝟬 )" by (rule MMI_3adant1)
   have S4: "𝟬 ∈ ℂ" by (rule MMI_0cn)
   have S5: "( A ∈ ℂ ∧ 𝟬 ∈ ℂ ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> C ) = ( 𝟬 \<cdiv> C ) ⟷ A = 𝟬 )" by (rule MMI_div11t)
   from S4 S5 have S6: "( A ∈ ℂ ∧ ( C ∈ ℂ ∧ C ≠ 𝟬 ) ) ⟶ 
 ( ( A \<cdiv> C ) = ( 𝟬 \<cdiv> C ) ⟷ A = 𝟬 )" by (rule MMI_mp3an2)
   from S6 have S7: "( A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> C ) = ( 𝟬 \<cdiv> C ) ⟷ A = 𝟬 )" by (rule MMI_3impb)
   from S3 S7 show "( A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> C ) = 𝟬 ⟷ A = 𝟬 )" by (rule MMI_bitr3d)
qed

lemma (in MMIsar0) MMI_recrec: assumes A1: "A ∈ ℂ" and
    A2: "A ≠ 𝟬"   
   shows "( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) = A"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "A ≠ 𝟬".
   from S1 S2 have S3: "( 𝟭 \<cdiv> A ) ∈ ℂ" by (rule MMI_reccl)
   have S4: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   from A1 have S5: "A ∈ ℂ".
   have S6: "𝟭 ≠ 𝟬" by (rule MMI_ax1ne0)
   from A2 have S7: "A ≠ 𝟬".
   from S4 S5 S6 S7 have S8: "( 𝟭 \<cdiv> A ) ≠ 𝟬" by (rule MMI_divne0)
   from S3 S8 have S9: "( ( 𝟭 \<cdiv> A ) ⋅ ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ) = 𝟭" 
     by (rule MMI_recid)
   from S9 have S10: "( A ⋅ ( ( 𝟭 \<cdiv> A ) ⋅ ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ) ) = 
 ( A ⋅ 𝟭 )" by (rule MMI_opreq2i)
   from A1 have S11: "A ∈ ℂ".
   from A2 have S12: "A ≠ 𝟬".
   from S11 S12 have S13: "( A ⋅ ( 𝟭 \<cdiv> A ) ) = 𝟭" by (rule MMI_recid)
   from S13 have S14: "( ( A ⋅ ( 𝟭 \<cdiv> A ) ) ⋅ ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ) = 
 ( 𝟭 ⋅ ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) )" by (rule MMI_opreq1i)
   from A1 have S15: "A ∈ ℂ".
   from S3 have S16: "( 𝟭 \<cdiv> A ) ∈ ℂ" .
   from S3 have S17: "( 𝟭 \<cdiv> A ) ∈ ℂ" .
   from S8 have S18: "( 𝟭 \<cdiv> A ) ≠ 𝟬" .
   from S17 S18 have S19: "( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ∈ ℂ" by (rule MMI_reccl)
   from S15 S16 S19 have S20: 
     "( ( A ⋅ ( 𝟭 \<cdiv> A ) ) ⋅ ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ) = 
 ( A ⋅ ( ( 𝟭 \<cdiv> A ) ⋅ ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ) )" by (rule MMI_mulass)
   from S19 have S21: "( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ∈ ℂ" .
   from S21 have S22: "( 𝟭 ⋅ ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ) = 
 ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) )" by (rule MMI_mulid2)
   from S14 S20 S22 have S23: 
     "( A ⋅ ( ( 𝟭 \<cdiv> A ) ⋅ ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) ) ) = 
 ( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) )" by (rule MMI_3eqtr3)
   from A1 have S24: "A ∈ ℂ".
   from S24 have S25: "( A ⋅ 𝟭 ) = A" by (rule MMI_mulid1)
   from S10 S23 S25 show "( 𝟭 \<cdiv> ( 𝟭 \<cdiv> A ) ) = A" by (rule MMI_3eqtr3)
qed

lemma (in MMIsar0) MMI_divid: assumes A1: "A ∈ ℂ" and
    A2: "A ≠ 𝟬"   
   shows "( A \<cdiv> A ) = 𝟭"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A1 have S2: "A ∈ ℂ".
   from A2 have S3: "A ≠ 𝟬".
   from S1 S2 S3 have S4: "( A \<cdiv> A ) = ( A ⋅ ( 𝟭 \<cdiv> A ) )" by (rule MMI_divrec)
   from A1 have S5: "A ∈ ℂ".
   from A2 have S6: "A ≠ 𝟬".
   from S5 S6 have S7: "( A ⋅ ( 𝟭 \<cdiv> A ) ) = 𝟭" by (rule MMI_recid)
   from S4 S7 show "( A \<cdiv> A ) = 𝟭" by (rule MMI_eqtr)
qed

lemma (in MMIsar0) MMI_div0: assumes A1: "A ∈ ℂ" and
    A2: "A ≠ 𝟬"   
   shows "( 𝟬 \<cdiv> A ) = 𝟬"
proof -
   from A1 have S1: "A ∈ ℂ".
   from A2 have S2: "A ≠ 𝟬".
   have S3: "( A ∈ ℂ ∧ A ≠ 𝟬 ) ⟶ ( 𝟬 \<cdiv> A ) = 𝟬" by (rule MMI_div0t)
   from S1 S2 S3 show "( 𝟬 \<cdiv> A ) = 𝟬" by (rule MMI_mp2an)
qed

lemma (in MMIsar0) MMI_div1: assumes A1: "A ∈ ℂ"   
   shows "( A \<cdiv> 𝟭 ) = A"
proof -
   from A1 have S1: "A ∈ ℂ".
   from S1 have S2: "( 𝟭 ⋅ A ) = A" by (rule MMI_mulid2)
   from A1 have S3: "A ∈ ℂ".
   have S4: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   from A1 have S5: "A ∈ ℂ".
   have S6: "𝟭 ≠ 𝟬" by (rule MMI_ax1ne0)
   from S3 S4 S5 S6 have S7: "( A \<cdiv> 𝟭 ) = A ⟷ ( 𝟭 ⋅ A ) = A" 
     by (rule MMI_divmul)
   from S2 S7 show "( A \<cdiv> 𝟭 ) = A" by (rule MMI_mpbir)
qed

lemma (in MMIsar0) MMI_div1t: 
   shows "A ∈ ℂ ⟶ ( A \<cdiv> 𝟭 ) = A"
proof -
   have S1: "A = 
 if ( A ∈ ℂ , A , 𝟭 ) ⟶ 
 ( A \<cdiv> 𝟭 ) = 
 ( if ( A ∈ ℂ , A , 𝟭 ) \<cdiv> 𝟭 )" by (rule MMI_opreq1)
   have S2: "A = 
 if ( A ∈ ℂ , A , 𝟭 ) ⟶ 
 A = if ( A ∈ ℂ , A , 𝟭 )" by (rule MMI_id)
   from S1 S2 have S3: "A = 
 if ( A ∈ ℂ , A , 𝟭 ) ⟶ 
 ( ( A \<cdiv> 𝟭 ) = 
 A ⟷ 
 ( if ( A ∈ ℂ , A , 𝟭 ) \<cdiv> 𝟭 ) = 
 if ( A ∈ ℂ , A , 𝟭 ) )" by (rule MMI_eqeq12d)
   have S4: "𝟭 ∈ ℂ" by (rule MMI_1cn)
   from S4 have S5: "if ( A ∈ ℂ , A , 𝟭 ) ∈ ℂ" by (rule MMI_elimel)
   from S5 have S6: "( if ( A ∈ ℂ , A , 𝟭 ) \<cdiv> 𝟭 ) = 
 if ( A ∈ ℂ , A , 𝟭 )" by (rule MMI_div1)
   from S3 S6 show "A ∈ ℂ ⟶ ( A \<cdiv> 𝟭 ) = A" by (rule MMI_dedth)
qed

lemma (in MMIsar0) MMI_divnegt: 
   shows "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( \<cn> ( A \<cdiv> B ) ) = ( ( \<cn> A ) \<cdiv> B )"
proof -
   have S1: "( A ∈ ℂ ∧ ( 𝟭 \<cdiv> B ) ∈ ℂ ) ⟶ 
 ( ( \<cn> A ) ⋅ ( 𝟭 \<cdiv> B ) ) = 
 ( \<cn> ( A ⋅ ( 𝟭 \<cdiv> B ) ) )" by (rule MMI_mulneg1t)
   have S2: "( B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ ( 𝟭 \<cdiv> B ) ∈ ℂ" by (rule MMI_recclt)
   from S1 S2 have S3: "( A ∈ ℂ ∧ ( B ∈ ℂ ∧ B ≠ 𝟬 ) ) ⟶ 
 ( ( \<cn> A ) ⋅ ( 𝟭 \<cdiv> B ) ) = 
 ( \<cn> ( A ⋅ ( 𝟭 \<cdiv> B ) ) )" by (rule MMI_sylan2)
   from S3 have S4: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( ( \<cn> A ) ⋅ ( 𝟭 \<cdiv> B ) ) = 
 ( \<cn> ( A ⋅ ( 𝟭 \<cdiv> B ) ) )" by (rule MMI_3impb)
   have S5: "( ( \<cn> A ) ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( ( \<cn> A ) \<cdiv> B ) = 
 ( ( \<cn> A ) ⋅ ( 𝟭 \<cdiv> B ) )" by (rule MMI_divrect)
   have S6: "A ∈ ℂ ⟶ ( \<cn> A ) ∈ ℂ" by (rule MMI_negclt)
   from S5 S6 have S7: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( ( \<cn> A ) \<cdiv> B ) = 
 ( ( \<cn> A ) ⋅ ( 𝟭 \<cdiv> B ) )" by (rule MMI_syl3an1)
   have S8: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> B ) = ( A ⋅ ( 𝟭 \<cdiv> B ) )" by (rule MMI_divrect)
   from S8 have S9: "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( \<cn> ( A \<cdiv> B ) ) = 
 ( \<cn> ( A ⋅ ( 𝟭 \<cdiv> B ) ) )" by (rule MMI_negeqd)
   from S4 S7 S9 show "( A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 𝟬 ) ⟶ 
 ( \<cn> ( A \<cdiv> B ) ) = ( ( \<cn> A ) \<cdiv> B )" by (rule MMI_3eqtr4rd)
qed

lemma (in MMIsar0) MMI_divsubdirt: 
   shows "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cs> B ) \<cdiv> C ) = 
 ( ( A \<cdiv> C ) \<cs> ( B \<cdiv> C ) )"
proof -
   have S1: "( ( A ∈ ℂ ∧ ( \<cn> B ) ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<ca> ( \<cn> B ) ) \<cdiv> C ) = 
 ( ( A \<cdiv> C ) \<ca> ( ( \<cn> B ) \<cdiv> C ) )" by (rule MMI_divdirt)
   have S2: "B ∈ ℂ ⟶ ( \<cn> B ) ∈ ℂ" by (rule MMI_negclt)
   from S1 S2 have S3: "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<ca> ( \<cn> B ) ) \<cdiv> C ) = 
 ( ( A \<cdiv> C ) \<ca> ( ( \<cn> B ) \<cdiv> C ) )" by (rule MMI_syl3anl2)
   have S4: "( A ∈ ℂ ∧ B ∈ ℂ ) ⟶ 
 ( A \<ca> ( \<cn> B ) ) = ( A \<cs> B )" by (rule MMI_negsubt)
   from S4 have S5: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
 ( A \<ca> ( \<cn> B ) ) = ( A \<cs> B )" by (rule MMI_3adant3)
   from S5 have S6: "( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ⟶ 
 ( ( A \<ca> ( \<cn> B ) ) \<cdiv> C ) = 
 ( ( A \<cs> B ) \<cdiv> C )" by (rule MMI_opreq1d)
   from S6 have S7: "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<ca> ( \<cn> B ) ) \<cdiv> C ) = 
 ( ( A \<cs> B ) \<cdiv> C )" by (rule MMI_adantr)
   have S8: "( B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( \<cn> ( B \<cdiv> C ) ) = ( ( \<cn> B ) \<cdiv> C )" by (rule MMI_divnegt)
   from S8 have S9: "( ( B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( \<cn> ( B \<cdiv> C ) ) = ( ( \<cn> B ) \<cdiv> C )" by (rule MMI_3expa)
   from S9 have S10: "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( \<cn> ( B \<cdiv> C ) ) = ( ( \<cn> B ) \<cdiv> C )" by (rule MMI_3adantl1)
   from S10 have S11: "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> C ) \<ca> ( \<cn> ( B \<cdiv> C ) ) ) = 
 ( ( A \<cdiv> C ) \<ca> ( ( \<cn> B ) \<cdiv> C ) )" by (rule MMI_opreq2d)
   have S12: "( ( A \<cdiv> C ) ∈ ℂ ∧ ( B \<cdiv> C ) ∈ ℂ ) ⟶ 
 ( ( A \<cdiv> C ) \<ca> ( \<cn> ( B \<cdiv> C ) ) ) = 
 ( ( A \<cdiv> C ) \<cs> ( B \<cdiv> C ) )" by (rule MMI_negsubt)
   have S13: "( A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> C ) ∈ ℂ" by (rule MMI_divclt)
   from S13 have S14: "( ( A ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> C ) ∈ ℂ" by (rule MMI_3expa)
   from S14 have S15: "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( A \<cdiv> C ) ∈ ℂ" by (rule MMI_3adantl2)
   have S16: "( B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 𝟬 ) ⟶ 
 ( B \<cdiv> C ) ∈ ℂ" by (rule MMI_divclt)
   from S16 have S17: "( ( B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( B \<cdiv> C ) ∈ ℂ" by (rule MMI_3expa)
   from S17 have S18: "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( B \<cdiv> C ) ∈ ℂ" by (rule MMI_3adantl1)
   from S12 S15 S18 have S19: "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> C ) \<ca> ( \<cn> ( B \<cdiv> C ) ) ) = 
 ( ( A \<cdiv> C ) \<cs> ( B \<cdiv> C ) )" by (rule MMI_sylanc)
   from S11 S19 have S20: "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cdiv> C ) \<ca> ( ( \<cn> B ) \<cdiv> C ) ) = 
 ( ( A \<cdiv> C ) \<cs> ( B \<cdiv> C ) )" by (rule MMI_eqtr3d)
   from S3 S7 S20 show "( ( A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ) ∧ C ≠ 𝟬 ) ⟶ 
 ( ( A \<cs> B ) \<cdiv> C ) = 
 ( ( A \<cdiv> C ) \<cs> ( B \<cdiv> C ) )" by (rule MMI_3eqtr3d)
qed


end