xcmplx_1.miz



    begin

    reserve a,b,c,d,e for Complex;

    theorem :: XCMPLX_1:1

    (a + (b + c)) = ((a + b) + c);

    theorem :: XCMPLX_1:2

    (a + c) = (b + c) implies a = b;

    theorem :: XCMPLX_1:3

    a = (a + b) implies b = 0 ;

    theorem :: XCMPLX_1:4

    

     Th4: (a * (b * c)) = ((a * b) * c);

    theorem :: XCMPLX_1:5

    c <> 0 & (a * c) = (b * c) implies a = b

    proof

      assume

       A1: c <> 0 ;

      assume (a * c) = (b * c);

      then (a * (c * (c " ))) = ((b * c) * (c " )) by Th4;

      then (a * 1) = ((b * c) * (c " )) by A1, XCMPLX_0:def 7;

      then a = (b * (c * (c " )));

      then a = (b * 1) by A1, XCMPLX_0:def 7;

      hence thesis;

    end;

    theorem :: XCMPLX_1:6

    (a * b) = 0 implies a = 0 or b = 0 ;

    theorem :: XCMPLX_1:7

    

     Th7: b <> 0 & (a * b) = b implies a = 1

    proof

      assume that

       A1: b <> 0 and

       A2: (a * b) = b;

      ((a * b) * (b " )) = 1 by A1, A2, XCMPLX_0:def 7;

      then (a * 1) = 1 by A2, Th4;

      hence thesis;

    end;

    theorem :: XCMPLX_1:8

    (a * (b + c)) = ((a * b) + (a * c));

    theorem :: XCMPLX_1:9

    (((a + b) + c) * d) = (((a * d) + (b * d)) + (c * d));

    theorem :: XCMPLX_1:10

    ((a + b) * (c + d)) = ((((a * c) + (a * d)) + (b * c)) + (b * d));

    theorem :: XCMPLX_1:11

    (2 * a) = (a + a);

    theorem :: XCMPLX_1:12

    (3 * a) = ((a + a) + a);

    theorem :: XCMPLX_1:13

    (4 * a) = (((a + a) + a) + a);

    theorem :: XCMPLX_1:14

    (a - a) = 0 ;

    theorem :: XCMPLX_1:15

    (a - b) = 0 implies a = b;

    theorem :: XCMPLX_1:16

    (b - a) = b implies a = 0 ;

    theorem :: XCMPLX_1:17

    a = (a - (b - b));

    theorem :: XCMPLX_1:18

    (a - (a - b)) = b;

    theorem :: XCMPLX_1:19

    (a - c) = (b - c) implies a = b;

    theorem :: XCMPLX_1:20

    (c - a) = (c - b) implies a = b;

    theorem :: XCMPLX_1:21

    ((a - b) - c) = ((a - c) - b);

    theorem :: XCMPLX_1:22

    (a - c) = ((a - b) - (c - b));

    theorem :: XCMPLX_1:23

    ((c - a) - (c - b)) = (b - a);

    theorem :: XCMPLX_1:24

    (a - b) = (c - d) implies (a - c) = (b - d);

    

     Lm1: ((a " ) * (b " )) = ((a * b) " )

    proof

      per cases ;

        suppose

         A1: a = 0 or b = 0 ;

        then (a " ) = 0 or (b " ) = 0 ;

        hence thesis by A1;

      end;

        suppose that

         A2: a <> 0 and

         A3: b <> 0 ;

        

        thus ((a " ) * (b " )) = (((a " ) * (b " )) * 1)

        .= (((a " ) * (b " )) * ((a * b) * ((a * b) " ))) by A2, A3, XCMPLX_0:def 7

        .= ((((a " ) * a) * ((b " ) * b)) * ((a * b) " ))

        .= ((1 * ((b " ) * b)) * ((a * b) " )) by A2, XCMPLX_0:def 7

        .= (1 * ((a * b) " )) by A3, XCMPLX_0:def 7

        .= ((a * b) " );

      end;

    end;

    

     Lm2: (a / (b / c)) = ((a * c) / b)

    proof

      

      thus (a / (b / c)) = (a / (b * (c " ))) by XCMPLX_0:def 9

      .= (a * ((b * (c " )) " )) by XCMPLX_0:def 9

      .= (a * ((b " ) * ((c " ) " ))) by Lm1

      .= ((a * c) * (b " ))

      .= ((a * c) / b) by XCMPLX_0:def 9;

    end;

    

     Lm3: b <> 0 implies ((a / b) * b) = a

    proof

      assume

       A1: b <> 0 ;

      

      thus ((a / b) * b) = ((a * (b " )) * b) by XCMPLX_0:def 9

      .= (a * ((b " ) * b))

      .= (a * 1) by A1, XCMPLX_0:def 7

      .= a;

    end;

    

     Lm4: (1 / a) = (a " )

    proof

      

      thus (1 / a) = (1 * (a " )) by XCMPLX_0:def 9

      .= (a " );

    end;

    

     Lm5: a <> 0 implies (a / a) = 1

    proof

      assume

       A1: a <> 0 ;

      

      thus (a / a) = (a * (a " )) by XCMPLX_0:def 9

      .= 1 by A1, XCMPLX_0:def 7;

    end;

    theorem :: XCMPLX_1:25

    a = (a + (b - b));

    theorem :: XCMPLX_1:26

    a = ((a + b) - b);

    theorem :: XCMPLX_1:27

    a = ((a - b) + b);

    theorem :: XCMPLX_1:28

    (a + c) = ((a + b) + (c - b));

    theorem :: XCMPLX_1:29

    ((a + b) - c) = ((a - c) + b);

    theorem :: XCMPLX_1:30

    ((a - b) + c) = ((c - b) + a);

    theorem :: XCMPLX_1:31

    (a + c) = ((a + b) - (b - c));

    theorem :: XCMPLX_1:32

    (a - c) = ((a + b) - (c + b));

    theorem :: XCMPLX_1:33

    (a + b) = (c + d) implies (a - c) = (d - b);

    theorem :: XCMPLX_1:34

    (a - c) = (d - b) implies (a + b) = (c + d);

    theorem :: XCMPLX_1:35

    (a + b) = (c - d) implies (a + d) = (c - b);

    theorem :: XCMPLX_1:36

    (a - (b + c)) = ((a - b) - c);

    theorem :: XCMPLX_1:37

    (a - (b - c)) = ((a - b) + c);

    theorem :: XCMPLX_1:38

    (a - (b - c)) = (a + (c - b));

    theorem :: XCMPLX_1:39

    (a - c) = ((a - b) + (b - c));

    theorem :: XCMPLX_1:40

    (a * (b - c)) = ((a * b) - (a * c));

    theorem :: XCMPLX_1:41

    ((a - b) * (c - d)) = ((b - a) * (d - c));

    theorem :: XCMPLX_1:42

    (((a - b) - c) * d) = (((a * d) - (b * d)) - (c * d));

    theorem :: XCMPLX_1:43

    (((a + b) - c) * d) = (((a * d) + (b * d)) - (c * d));

    theorem :: XCMPLX_1:44

    (((a - b) + c) * d) = (((a * d) - (b * d)) + (c * d));

    theorem :: XCMPLX_1:45

    ((a + b) * (c - d)) = ((((a * c) - (a * d)) + (b * c)) - (b * d));

    theorem :: XCMPLX_1:46

    ((a - b) * (c + d)) = ((((a * c) + (a * d)) - (b * c)) - (b * d));

    theorem :: XCMPLX_1:47

    ((a - b) * (e - d)) = ((((a * e) - (a * d)) - (b * e)) + (b * d));

    theorem :: XCMPLX_1:48

    ((a / b) / c) = ((a / c) / b)

    proof

      

      thus ((a / b) / c) = ((a * (b " )) / c) by XCMPLX_0:def 9

      .= ((a * (b " )) * (c " )) by XCMPLX_0:def 9

      .= ((a * (c " )) * (b " ))

      .= ((a / c) * (b " )) by XCMPLX_0:def 9

      .= ((a / c) / b) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:49

    

     Th49: (a / 0 ) = 0

    proof

      

      thus (a / 0 ) = (a * ( 0 " )) by XCMPLX_0:def 9

      .= 0 ;

    end;

    theorem :: XCMPLX_1:50

    a <> 0 & b <> 0 implies (a / b) <> 0 ;

    theorem :: XCMPLX_1:51

    b <> 0 implies a = (a / (b / b))

    proof

      

       A1: a = (a / 1);

      assume b <> 0 ;

      hence thesis by A1, Lm5;

    end;

    

     Lm6: ((a / b) * (c / d)) = ((a * c) / (b * d))

    proof

      

      thus ((a / b) * (c / d)) = ((a * (b " )) * (c / d)) by XCMPLX_0:def 9

      .= ((a * (b " )) * (c * (d " ))) by XCMPLX_0:def 9

      .= ((a * c) * ((b " ) * (d " )))

      .= ((a * c) * ((b * d) " )) by Lm1

      .= ((a * c) / (b * d)) by XCMPLX_0:def 9;

    end;

    

     Lm7: ((a / b) " ) = (b / a)

    proof

      per cases ;

        suppose

         A1: a = 0 ;

        

        hence ((a / b) " ) = (b * ( 0 " ))

        .= (b / a) by A1, XCMPLX_0:def 9;

      end;

        suppose

         A2: b = 0 ;

        

        hence ((a / b) " ) = ((a * ( 0 " )) " ) by XCMPLX_0:def 9

        .= (b / a) by A2;

      end;

        suppose

         A3: a <> 0 & b <> 0 ;

        ((a / b) * (b / a)) = ((a * b) / (a * b)) by Lm6;

        then ((a / b) * (b / a)) = 1 by A3, Lm5;

        hence thesis by A3, XCMPLX_0:def 7;

      end;

    end;

    

     Lm8: (a * (b / c)) = ((a * b) / c)

    proof

      

      thus (a * (b / c)) = ((a / 1) * (b / c))

      .= ((a * b) / (1 * c)) by Lm6

      .= ((a * b) / c);

    end;

    theorem :: XCMPLX_1:52

    a <> 0 implies (a / (a / b)) = b

    proof

      assume

       A1: a <> 0 ;

      

      thus (a / (a / b)) = (a * ((a / b) " )) by XCMPLX_0:def 9

      .= (a * (b / a)) by Lm7

      .= ((a * b) / a) by Lm8

      .= ((a / a) * b) by Lm8

      .= (1 * b) by A1, Lm5

      .= b;

    end;

    theorem :: XCMPLX_1:53

    c <> 0 & (a / c) = (b / c) implies a = b

    proof

      assume that

       A1: c <> 0 and

       A2: (a / c) = (b / c);

      a = ((b / c) * c) by A1, A2, Lm3;

      hence thesis by A1, Lm3;

    end;

    

     Lm9: b <> 0 implies a = ((a * b) / b)

    proof

      

       A1: a = (a * 1);

      assume b <> 0 ;

      then a = (a * (b / b)) by A1, Lm5;

      then a = (a * (b * (b " ))) by XCMPLX_0:def 9;

      then a = ((a * b) * (b " ));

      hence thesis by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:54

    (a / b) <> 0 implies b = (a / (a / b))

    proof

      assume

       A1: (a / b) <> 0 ;

      then b <> 0 by Th49;

      then ((a / b) * b) = a by Lm3;

      hence thesis by A1, Lm9;

    end;

    

     Lm10: c <> 0 implies (a / b) = ((a * c) / (b * c))

    proof

      assume

       A1: c <> 0 ;

      

      thus (a / b) = ((a * (b " )) * 1) by XCMPLX_0:def 9

      .= ((a * (b " )) * (c * (c " ))) by A1, XCMPLX_0:def 7

      .= ((a * c) * ((b " ) * (c " )))

      .= ((a * c) * ((b * c) " )) by Lm1

      .= ((a * c) / (b * c)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:55

    c <> 0 implies (a / b) = ((a / c) / (b / c))

    proof

      assume c <> 0 ;

      

      hence (a / b) = ((a * (c " )) / (b * (c " ))) by Lm10

      .= ((a / c) / (b * (c " ))) by XCMPLX_0:def 9

      .= ((a / c) / (b / c)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:56

    (1 / (1 / a)) = a

    proof

      

      thus (1 / (1 / a)) = ((1 * a) / 1) by Lm2

      .= a;

    end;

    

     Lm11: ((a * (b " )) " ) = ((a " ) * b)

    proof

      

      thus ((a * (b " )) " ) = ((a " ) * ((b " ) " )) by Lm1

      .= ((a " ) * b);

    end;

    theorem :: XCMPLX_1:57

    (1 / (a / b)) = (b / a)

    proof

      

      thus (1 / (a / b)) = (1 / (a * (b " ))) by XCMPLX_0:def 9

      .= ((a * (b " )) " ) by Lm4

      .= (b * (a " )) by Lm11

      .= (b / a) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:58

    

     Th58: (a / b) = 1 implies a = b

    proof

      assume

       A1: (a / b) = 1;

      then b <> 0 by Th49;

      then a = (1 * b) by A1, Lm3;

      hence thesis;

    end;

    

     Lm12: (a " ) = (b " ) implies a = b

    proof

      assume (a " ) = (b " );

      then a = ((b " ) " );

      hence thesis;

    end;

    theorem :: XCMPLX_1:59

    

     Th59: (1 / a) = (1 / b) implies a = b

    proof

      assume (1 / a) = (1 / b);

      then (a " ) = (1 / b) by Lm4;

      then (a " ) = (b " ) by Lm4;

      hence thesis by Lm12;

    end;

    theorem :: XCMPLX_1:60

    a <> 0 implies (a / a) = 1 by Lm5;

    theorem :: XCMPLX_1:61

    b <> 0 & (b / a) = b implies a = 1

    proof

      assume that

       A1: b <> 0 and

       A2: (b / a) = b;

      a <> 0 by A1, A2, Th49;

      then b = (b * a) by A2, Lm3;

      hence thesis by A1, Th7;

    end;

    theorem :: XCMPLX_1:62

    

     Th62: ((a / c) + (b / c)) = ((a + b) / c)

    proof

      

      thus ((a / c) + (b / c)) = ((a * (c " )) + (b / c)) by XCMPLX_0:def 9

      .= ((a * (c " )) + (b * (c " ))) by XCMPLX_0:def 9

      .= ((a + b) * (c " ))

      .= ((a + b) / c) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:63

    (((a + b) + e) / d) = (((a / d) + (b / d)) + (e / d))

    proof

      

      thus (((a + b) + e) / d) = (((a + b) / d) + (e / d)) by Th62

      .= (((a / d) + (b / d)) + (e / d)) by Th62;

    end;

    theorem :: XCMPLX_1:64

    ((a + a) / 2) = a;

    theorem :: XCMPLX_1:65

    ((a / 2) + (a / 2)) = a;

    theorem :: XCMPLX_1:66

    a = ((a + b) / 2) implies a = b;

    theorem :: XCMPLX_1:67

    (((a + a) + a) / 3) = a;

    theorem :: XCMPLX_1:68

    (((a / 3) + (a / 3)) + (a / 3)) = a;

    theorem :: XCMPLX_1:69

    ((((a + a) + a) + a) / 4) = a;

    theorem :: XCMPLX_1:70

    ((((a / 4) + (a / 4)) + (a / 4)) + (a / 4)) = a;

    theorem :: XCMPLX_1:71

    ((a / 4) + (a / 4)) = (a / 2);

    theorem :: XCMPLX_1:72

    ((a + a) / 4) = (a / 2);

    theorem :: XCMPLX_1:73

    (a * b) = 1 implies a = (1 / b)

    proof

      assume

       A1: (a * b) = 1;

      then b <> 0 ;

      then (a * 1) = (1 * (b " )) by A1, XCMPLX_0:def 7;

      hence thesis by Lm4;

    end;

    theorem :: XCMPLX_1:74

    (a * (b / c)) = ((a * b) / c) by Lm8;

    theorem :: XCMPLX_1:75

    ((a / b) * e) = ((e / b) * a)

    proof

      

      thus ((a / b) * e) = ((a * e) / b) by Lm8

      .= ((e / b) * a) by Lm8;

    end;

    theorem :: XCMPLX_1:76

    ((a / b) * (c / d)) = ((a * c) / (b * d)) by Lm6;

    theorem :: XCMPLX_1:77

    (a / (b / c)) = ((a * c) / b) by Lm2;

    

     Lm13: ((a / b) / (c / d)) = ((a * d) / (b * c))

    proof

      

      thus ((a / b) / (c / d)) = ((a / b) * ((c / d) " )) by XCMPLX_0:def 9

      .= ((a / b) * (d / c)) by Lm7

      .= ((a * d) / (b * c)) by Lm6;

    end;

    theorem :: XCMPLX_1:78

    

     Th78: (a / (b * c)) = ((a / b) / c)

    proof

      

      thus (a / (b * c)) = ((a * 1) / (b * c))

      .= ((a / b) / (c / 1)) by Lm13

      .= ((a / b) / c);

    end;

    theorem :: XCMPLX_1:79

    (a / (b / c)) = (a * (c / b))

    proof

      

      thus (a / (b / c)) = ((a * c) / b) by Lm2

      .= ((a * c) * (b " )) by XCMPLX_0:def 9

      .= (a * (c * (b " )))

      .= (a * (c / b)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:80

    (a / (b / c)) = ((c / b) * a)

    proof

      (a / (b / c)) = ((a * c) / b) by Lm2

      .= ((a * c) * (b " )) by XCMPLX_0:def 9

      .= (a * (c * (b " )))

      .= (a * (c / b)) by XCMPLX_0:def 9;

      hence thesis;

    end;

    theorem :: XCMPLX_1:81

    

     Th81: (a / (b / e)) = (e * (a / b))

    proof

      

      thus (a / (b / e)) = ((a * e) / b) by Lm2

      .= ((e * a) * (b " )) by XCMPLX_0:def 9

      .= (e * (a * (b " )))

      .= (e * (a / b)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:82

    (a / (b / c)) = ((a / b) * c)

    proof

      (a / (b / c)) = ((a * c) / b) by Lm2

      .= ((c * a) * (b " )) by XCMPLX_0:def 9

      .= (c * (a * (b " )))

      .= (c * (a / b)) by XCMPLX_0:def 9;

      hence thesis;

    end;

    

     Lm14: (a * (1 / b)) = (a / b)

    proof

      

      thus (a / b) = (a * (b " )) by XCMPLX_0:def 9

      .= (a * (1 / b)) by Lm4;

    end;

    

     Lm15: ((1 / c) * (a / b)) = (a / (b * c))

    proof

      ((a / b) / c) = ((c " ) * (a / b)) by XCMPLX_0:def 9

      .= ((1 / c) * (a / b)) by Lm4;

      hence thesis by Th78;

    end;

    theorem :: XCMPLX_1:83

    ((a * b) / (c * d)) = (((a / c) * b) / d)

    proof

      

      thus ((a * b) / (c * d)) = ((1 / c) * ((a * b) / d)) by Lm15

      .= (((1 / c) * (a * b)) / d) by Lm8

      .= ((((1 / c) * a) * b) / d)

      .= (((a / c) * b) / d) by Lm14;

    end;

    theorem :: XCMPLX_1:84

    ((a / b) / (c / d)) = ((a * d) / (b * c)) by Lm13;

    theorem :: XCMPLX_1:85

    ((a / c) * (b / d)) = ((a / d) * (b / c))

    proof

      

      thus ((a / c) * (b / d)) = ((a * b) / (d * c)) by Lm6

      .= ((a / d) * (b / c)) by Lm6;

    end;

    theorem :: XCMPLX_1:86

    (a / ((b * c) * (d / e))) = ((e / c) * (a / (b * d)))

    proof

      

      thus (a / ((b * c) * (d / e))) = (a / ((b * c) * (d * (e " )))) by XCMPLX_0:def 9

      .= (a / (c * ((b * d) * (e " ))))

      .= (a / (c * ((b * d) / e))) by XCMPLX_0:def 9

      .= (a / ((b * d) / (e / c))) by Th81

      .= ((e / c) * (a / (b * d))) by Th81;

    end;

    theorem :: XCMPLX_1:87

    b <> 0 implies ((a / b) * b) = a by Lm3;

    theorem :: XCMPLX_1:88

    b <> 0 implies a = (a * (b / b))

    proof

      

       A1: a = (a * 1);

      assume b <> 0 ;

      hence thesis by A1, Lm5;

    end;

    theorem :: XCMPLX_1:89

    b <> 0 implies a = ((a * b) / b) by Lm9;

    theorem :: XCMPLX_1:90

    b <> 0 implies (a * c) = ((a * b) * (c / b))

    proof

      assume

       A1: b <> 0 ;

      

      thus (a * c) = ((a * 1) * c)

      .= ((a * (b * (b " ))) * c) by A1, XCMPLX_0:def 7

      .= ((a * b) * ((b " ) * c))

      .= ((a * b) * (c / b)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:91

    c <> 0 implies (a / b) = ((a * c) / (b * c)) by Lm10;

    theorem :: XCMPLX_1:92

    c <> 0 implies (a / b) = ((a / (b * c)) * c)

    proof

      assume

       A1: c <> 0 ;

      (c * (a / (b * c))) = (c * ((a * 1) / (b * c)))

      .= (c * ((1 / c) * (a / b))) by Lm6

      .= (((1 / c) * c) * (a / b))

      .= (1 * (a / b)) by A1, Lm3

      .= (a / b);

      hence thesis;

    end;

    theorem :: XCMPLX_1:93

    b <> 0 implies (a * c) = ((a * b) / (b / c))

    proof

      assume

       A1: b <> 0 ;

      

      thus (a * c) = ((a * 1) * c)

      .= ((a * (b * (b " ))) * c) by A1, XCMPLX_0:def 7

      .= ((a * b) * ((b " ) * c))

      .= ((a * b) * ((b * (c " )) " )) by Lm11

      .= ((a * b) / (b * (c " ))) by XCMPLX_0:def 9

      .= ((a * b) / (b / c)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:94

    

     Th94: c <> 0 & d <> 0 & (a * c) = (b * d) implies (a / d) = (b / c)

    proof

      assume that

       A1: c <> 0 and

       A2: d <> 0 ;

      assume (a * c) = (b * d);

      then a = ((b * d) / c) by A1, Lm9;

      then a = (d * (b / c)) by Lm8;

      hence thesis by A2, Lm9;

    end;

    theorem :: XCMPLX_1:95

    

     Th95: c <> 0 & d <> 0 & (a / d) = (b / c) implies (a * c) = (b * d)

    proof

      assume that

       A1: c <> 0 and

       A2: d <> 0 and

       A3: (a / d) = (b / c);

      (c * (a / d)) = b by A1, A3, Lm3;

      then ((a * c) / d) = b by Lm8;

      hence thesis by A2, Lm3;

    end;

    theorem :: XCMPLX_1:96

    c <> 0 & d <> 0 & (a * c) = (b / d) implies (a * d) = (b / c)

    proof

      assume that

       A1: c <> 0 and

       A2: d <> 0 ;

      assume (a * c) = (b / d);

      then ((a * c) * d) = b by A2, Lm3;

      then ((a * d) * c) = b;

      hence thesis by A1, Lm9;

    end;

    theorem :: XCMPLX_1:97

    c <> 0 implies (a / b) = (c * ((a / c) / b))

    proof

      assume

       A1: c <> 0 ;

      

      thus (a / b) = (a * (b " )) by XCMPLX_0:def 9

      .= ((c * (a / c)) * (b " )) by A1, Lm3

      .= (c * ((a / c) * (b " )))

      .= (c * ((a / c) / b)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:98

    c <> 0 implies (a / b) = ((a / c) * (c / b))

    proof

      assume

       A1: c <> 0 ;

      

      thus (a / b) = (a * (b " )) by XCMPLX_0:def 9

      .= (((a / c) * c) * (b " )) by A1, Lm3

      .= ((a / c) * (c * (b " )))

      .= ((a / c) * (c / b)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:99

    (a * (1 / b)) = (a / b) by Lm14;

    

     Lm16: (1 / (a " )) = a

    proof

      (1 / (a " )) = ((a " ) " ) by Lm4

      .= a;

      hence thesis;

    end;

    theorem :: XCMPLX_1:100

    (a / (1 / b)) = (a * b)

    proof

      

      thus (a / (1 / b)) = (a / (b " )) by Lm4

      .= (a * (1 / (b " ))) by Lm14

      .= (a * b) by Lm16;

    end;

    theorem :: XCMPLX_1:101

    ((a / b) * c) = (((1 / b) * c) * a)

    proof

      ((a / b) * c) = (((1 / b) * a) * c) by Lm14;

      hence thesis;

    end;

    theorem :: XCMPLX_1:102

    ((1 / a) * (1 / b)) = (1 / (a * b))

    proof

      

      thus ((1 / a) * (1 / b)) = ((a " ) * (1 / b)) by Lm4

      .= ((a " ) * (b " )) by Lm4

      .= ((a * b) " ) by Lm1

      .= (1 / (a * b)) by Lm4;

    end;

    theorem :: XCMPLX_1:103

    ((1 / c) * (a / b)) = (a / (b * c)) by Lm15;

    theorem :: XCMPLX_1:104

    ((a / b) / c) = ((1 / b) * (a / c))

    proof

      ((a / b) / c) = ((a * (b " )) / c) by XCMPLX_0:def 9

      .= ((a * (b " )) * (c " )) by XCMPLX_0:def 9

      .= ((a * (c " )) * (b " ))

      .= ((a / c) * (b " )) by XCMPLX_0:def 9

      .= ((a / c) / b) by XCMPLX_0:def 9;

      

      hence ((a / b) / c) = ((b " ) * (a / c)) by XCMPLX_0:def 9

      .= ((1 / b) * (a / c)) by Lm4;

    end;

    theorem :: XCMPLX_1:105

    ((a / b) / c) = ((1 / c) * (a / b))

    proof

      

      thus ((a / b) / c) = ((c " ) * (a / b)) by XCMPLX_0:def 9

      .= ((1 / c) * (a / b)) by Lm4;

    end;

    theorem :: XCMPLX_1:106

    

     Th106: a <> 0 implies (a * (1 / a)) = 1

    proof

      assume

       A1: a <> 0 ;

      

      thus (a * (1 / a)) = (a * (a " )) by Lm4

      .= 1 by A1, XCMPLX_0:def 7;

    end;

    theorem :: XCMPLX_1:107

    b <> 0 implies a = ((a * b) * (1 / b))

    proof

      

       A1: a = (a * 1);

      assume b <> 0 ;

      then a = (a * (b / b)) by A1, Lm5;

      

      then a = (a * (b * (b " ))) by XCMPLX_0:def 9

      .= (a * (b * (1 / b))) by Lm4;

      hence thesis;

    end;

    theorem :: XCMPLX_1:108

    b <> 0 implies a = (a * ((1 / b) * b))

    proof

      assume

       A1: b <> 0 ;

      

      thus a = (a * 1)

      .= (a * ((1 / b) * b)) by A1, Lm3;

    end;

    theorem :: XCMPLX_1:109

    b <> 0 implies a = ((a * (1 / b)) * b)

    proof

      assume

       A1: b <> 0 ;

      a = (a * 1)

      .= (a * ((1 / b) * b)) by A1, Lm3;

      hence thesis;

    end;

    theorem :: XCMPLX_1:110

    b <> 0 implies a = (a / (b * (1 / b)))

    proof

      assume

       A1: b <> 0 ;

      

      thus a = (a / 1)

      .= (a / (b * (1 / b))) by A1, Th106;

    end;

    theorem :: XCMPLX_1:111

    a <> 0 & b <> 0 implies (1 / (a * b)) <> 0 ;

    theorem :: XCMPLX_1:112

    a <> 0 & b <> 0 implies ((a / b) * (b / a)) = 1

    proof

      assume

       A1: a <> 0 & b <> 0 ;

      (b / a) = ((a / b) " ) by Lm7;

      hence thesis by A1, XCMPLX_0:def 7;

    end;

    theorem :: XCMPLX_1:113

    

     Th113: b <> 0 implies ((a / b) + c) = ((a + (b * c)) / b)

    proof

      assume

       A1: b <> 0 ;

      ((a / b) + c) = ((a / b) + (1 * c))

      .= ((a / b) + ((b * (b " )) * c)) by A1, XCMPLX_0:def 7

      .= ((a / b) + ((b * c) * (b " )))

      .= ((a / b) + ((c * b) / b)) by XCMPLX_0:def 9

      .= ((a + (c * b)) / b) by Th62;

      hence thesis;

    end;

    theorem :: XCMPLX_1:114

    

     Th114: c <> 0 implies (a + b) = (c * ((a / c) + (b / c)))

    proof

      assume

       A1: c <> 0 ;

      

      hence (a + b) = ((c * (a / c)) + b) by Lm3

      .= ((c * (a / c)) + (c * (b / c))) by A1, Lm3

      .= (c * ((a / c) + (b / c)));

    end;

    theorem :: XCMPLX_1:115

    

     Th115: c <> 0 implies (a + b) = (((a * c) + (b * c)) / c)

    proof

      assume

       A1: c <> 0 ;

      

      hence (a + b) = (((a * c) / c) + b) by Lm9

      .= (((a * c) / c) + ((b * c) / c)) by A1, Lm9

      .= (((a * c) + (b * c)) / c) by Th62;

    end;

    theorem :: XCMPLX_1:116

    

     Th116: b <> 0 & d <> 0 implies ((a / b) + (c / d)) = (((a * d) + (c * b)) / (b * d))

    proof

      assume

       A1: b <> 0 ;

      assume d <> 0 ;

      

      hence ((a / b) + (c / d)) = (((a * d) / (b * d)) + (c / d)) by Lm10

      .= (((a * d) / (b * d)) + ((c * b) / (b * d))) by A1, Lm10

      .= (((a * d) + (c * b)) / (b * d)) by Th62;

    end;

    theorem :: XCMPLX_1:117

    

     Th117: a <> 0 implies (a + b) = (a * (1 + (b / a)))

    proof

      assume

       A1: a <> 0 ;

      

      hence (a + b) = (a * ((a / a) + (b / a))) by Th114

      .= (a * (1 + (b / a))) by A1, Lm5;

    end;

    theorem :: XCMPLX_1:118

    ((a / (2 * b)) + (a / (2 * b))) = (a / b)

    proof

      

      thus ((a / (2 * b)) + (a / (2 * b))) = ((a + a) / (2 * b)) by Th62

      .= ((2 * a) / (2 * b))

      .= (a / b) by Lm10;

    end;

    theorem :: XCMPLX_1:119

    (((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b))) = (a / b)

    proof

      

      thus (((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b))) = (((a + a) / (3 * b)) + (a / (3 * b))) by Th62

      .= (((a + a) + a) / (3 * b)) by Th62

      .= ((3 * a) / (3 * b))

      .= (a / b) by Lm10;

    end;

    

     Lm17: ( - (a / b)) = (( - a) / b)

    proof

      

      thus ( - (a / b)) = ( - (a * (b " ))) by XCMPLX_0:def 9

      .= (( - a) * (b " ))

      .= (( - a) / b) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:120

    

     Th120: ((a / c) - (b / c)) = ((a - b) / c)

    proof

      

      thus ((a / c) - (b / c)) = ((a / c) + ( - (b / c)))

      .= ((a / c) + (( - b) / c)) by Lm17

      .= ((a + ( - b)) / c) by Th62

      .= ((a - b) / c);

    end;

    theorem :: XCMPLX_1:121

    (a - (a / 2)) = (a / 2);

    theorem :: XCMPLX_1:122

    (((a - b) - c) / d) = (((a / d) - (b / d)) - (c / d))

    proof

      

      thus (((a - b) - c) / d) = (((a - b) / d) - (c / d)) by Th120

      .= (((a / d) - (b / d)) - (c / d)) by Th120;

    end;

    theorem :: XCMPLX_1:123

    b <> 0 & d <> 0 & b <> d & (a / b) = (e / d) implies (a / b) = ((a - e) / (b - d))

    proof

      assume that

       A1: b <> 0 and

       A2: d <> 0 and

       A3: b <> d and

       A4: (a / b) = (e / d);

      (a * d) = (e * b) by A1, A2, A4, Th95;

      then

       A5: (a * (b - d)) = ((a - e) * b);

      (b - d) <> 0 by A3;

      hence thesis by A1, A5, Th94;

    end;

    theorem :: XCMPLX_1:124

    (((a + b) - e) / d) = (((a / d) + (b / d)) - (e / d))

    proof

      

      thus (((a + b) - e) / d) = (((a + b) / d) - (e / d)) by Th120

      .= (((a / d) + (b / d)) - (e / d)) by Th62;

    end;

    theorem :: XCMPLX_1:125

    (((a - b) + e) / d) = (((a / d) - (b / d)) + (e / d))

    proof

      

      thus (((a - b) + e) / d) = (((a - b) / d) + (e / d)) by Th62

      .= (((a / d) - (b / d)) + (e / d)) by Th120;

    end;

    theorem :: XCMPLX_1:126

    

     Th126: b <> 0 implies ((a / b) - e) = ((a - (e * b)) / b)

    proof

      assume

       A1: b <> 0 ;

      

      thus ((a / b) - e) = ((a / b) + ( - e))

      .= ((a + (( - e) * b)) / b) by A1, Th113

      .= ((a - (e * b)) / b);

    end;

    theorem :: XCMPLX_1:127

    b <> 0 implies (c - (a / b)) = (((c * b) - a) / b)

    proof

      assume

       A1: b <> 0 ;

      

      thus (c - (a / b)) = ( - ((a / b) - c))

      .= ( - ((a - (c * b)) / b)) by A1, Th126

      .= (( - (a - (c * b))) / b) by Lm17

      .= (((c * b) - a) / b);

    end;

    theorem :: XCMPLX_1:128

    c <> 0 implies (a - b) = (c * ((a / c) - (b / c)))

    proof

      assume

       A1: c <> 0 ;

      

      hence (a - b) = ((c * (a / c)) - b) by Lm3

      .= ((c * (a / c)) - (c * (b / c))) by A1, Lm3

      .= (c * ((a / c) - (b / c)));

    end;

    theorem :: XCMPLX_1:129

    c <> 0 implies (a - b) = (((a * c) - (b * c)) / c)

    proof

      assume

       A1: c <> 0 ;

      

      thus (a - b) = (a + ( - b))

      .= (((a * c) + (( - b) * c)) / c) by A1, Th115

      .= (((a * c) - (b * c)) / c);

    end;

    theorem :: XCMPLX_1:130

    b <> 0 & d <> 0 implies ((a / b) - (c / d)) = (((a * d) - (c * b)) / (b * d))

    proof

      assume

       A1: b <> 0 ;

      assume

       A2: d <> 0 ;

      

      thus ((a / b) - (c / d)) = ((a / b) + ( - (c / d)))

      .= ((a / b) + (( - c) / d)) by Lm17

      .= (((a * d) + (( - c) * b)) / (b * d)) by A1, A2, Th116

      .= (((a * d) - (c * b)) / (b * d));

    end;

    theorem :: XCMPLX_1:131

    a <> 0 implies (a - b) = (a * (1 - (b / a)))

    proof

      assume

       A1: a <> 0 ;

      

      thus (a - b) = (a + ( - b))

      .= (a * (1 + (( - b) / a))) by A1, Th117

      .= (a * (1 + ( - (b / a)))) by Lm17

      .= (a * (1 - (b / a)));

    end;

    theorem :: XCMPLX_1:132

    a <> 0 implies c = ((((a * c) + b) - b) / a) by Lm9;

    theorem :: XCMPLX_1:133

    ( - a) = ( - b) implies a = b;

    theorem :: XCMPLX_1:134

    ( - a) = 0 implies a = 0 ;

    theorem :: XCMPLX_1:135

    (a + ( - b)) = 0 implies a = b;

    theorem :: XCMPLX_1:136

    a = ((a + b) + ( - b));

    theorem :: XCMPLX_1:137

    a = (a + (b + ( - b)));

    theorem :: XCMPLX_1:138

    a = ((( - b) + a) + b);

    theorem :: XCMPLX_1:139

    ( - (a + b)) = (( - a) + ( - b));

    theorem :: XCMPLX_1:140

    ( - (( - a) + b)) = (a + ( - b));

    theorem :: XCMPLX_1:141

    (a + b) = ( - (( - a) + ( - b)));

    theorem :: XCMPLX_1:142

    ( - (a - b)) = (b - a);

    theorem :: XCMPLX_1:143

    (( - a) - b) = (( - b) - a);

    theorem :: XCMPLX_1:144

    a = (( - b) - (( - a) - b));

    theorem :: XCMPLX_1:145

    ((( - a) - b) - c) = ((( - a) - c) - b);

    theorem :: XCMPLX_1:146

    ((( - a) - b) - c) = ((( - b) - c) - a);

    theorem :: XCMPLX_1:147

    ((( - a) - b) - c) = ((( - c) - b) - a);

    theorem :: XCMPLX_1:148

    ((c - a) - (c - b)) = ( - (a - b));

    theorem :: XCMPLX_1:149

    ( 0 - a) = ( - a);

    theorem :: XCMPLX_1:150

    (a + b) = (a - ( - b));

    theorem :: XCMPLX_1:151

    a = (a - (b + ( - b)));

    theorem :: XCMPLX_1:152

    (a - c) = (b + ( - c)) implies a = b;

    theorem :: XCMPLX_1:153

    (c - a) = (c + ( - b)) implies a = b;

    theorem :: XCMPLX_1:154

    ((a + b) - c) = ((( - c) + a) + b);

    theorem :: XCMPLX_1:155

    ((a - b) + c) = ((( - b) + c) + a);

    theorem :: XCMPLX_1:156

    (a - (( - b) - c)) = ((a + b) + c);

    theorem :: XCMPLX_1:157

    ((a - b) - c) = ((( - b) - c) + a);

    theorem :: XCMPLX_1:158

    ((a - b) - c) = ((( - c) + a) - b);

    theorem :: XCMPLX_1:159

    ((a - b) - c) = ((( - c) - b) + a);

    theorem :: XCMPLX_1:160

    ( - (a + b)) = (( - b) - a);

    theorem :: XCMPLX_1:161

    ( - (a - b)) = (( - a) + b);

    theorem :: XCMPLX_1:162

    ( - (( - a) + b)) = (a - b);

    theorem :: XCMPLX_1:163

    (a + b) = ( - (( - a) - b));

    theorem :: XCMPLX_1:164

    ((( - a) + b) - c) = ((( - c) + b) - a);

    theorem :: XCMPLX_1:165

    ((( - a) + b) - c) = ((( - c) - a) + b);

    theorem :: XCMPLX_1:166

    ( - ((a + b) + c)) = ((( - a) - b) - c);

    theorem :: XCMPLX_1:167

    ( - ((a + b) - c)) = ((( - a) - b) + c);

    theorem :: XCMPLX_1:168

    ( - ((a - b) + c)) = ((( - a) + b) - c);

    theorem :: XCMPLX_1:169

    ( - ((a - b) - c)) = ((( - a) + b) + c);

    theorem :: XCMPLX_1:170

    ( - ((( - a) + b) + c)) = ((a - b) - c);

    theorem :: XCMPLX_1:171

    ( - ((( - a) + b) - c)) = ((a - b) + c);

    theorem :: XCMPLX_1:172

    ( - ((( - a) - b) + c)) = ((a + b) - c);

    theorem :: XCMPLX_1:173

    ( - ((( - a) - b) - c)) = ((a + b) + c);

    theorem :: XCMPLX_1:174

    (( - a) * b) = ( - (a * b));

    theorem :: XCMPLX_1:175

    (( - a) * b) = (a * ( - b));

    theorem :: XCMPLX_1:176

    (( - a) * ( - b)) = (a * b);

    theorem :: XCMPLX_1:177

    ( - (a * ( - b))) = (a * b);

    theorem :: XCMPLX_1:178

    ( - (( - a) * b)) = (a * b);

    theorem :: XCMPLX_1:179

    (( - 1) * a) = ( - a);

    theorem :: XCMPLX_1:180

    (( - a) * ( - 1)) = a;

    theorem :: XCMPLX_1:181

    

     Th181: b <> 0 & (a * b) = ( - b) implies a = ( - 1)

    proof

      assume that

       A1: b <> 0 and

       A2: (a * b) = ( - b);

      (a * (b * (b " ))) = (( - b) * (b " )) by A2, Th4;

      then (a * 1) = (( - b) * (b " )) by A1, XCMPLX_0:def 7;

      

      hence a = ( - (b * (b " )))

      .= ( - 1) by A1, XCMPLX_0:def 7;

    end;

    theorem :: XCMPLX_1:182

    

     Th182: (a * a) = 1 implies a = 1 or a = ( - 1)

    proof

      assume (a * a) = 1;

      then ((a - 1) * (a + 1)) = 0 ;

      then (a - 1) = 0 or (a + 1) = 0 ;

      hence thesis;

    end;

    theorem :: XCMPLX_1:183

    (( - a) + (2 * a)) = a;

    theorem :: XCMPLX_1:184

    ((a - b) * c) = ((b - a) * ( - c));

    theorem :: XCMPLX_1:185

    ((a - b) * c) = ( - ((b - a) * c));

    theorem :: XCMPLX_1:186

    (a - (2 * a)) = ( - a);

    theorem :: XCMPLX_1:187

    ( - (a / b)) = (( - a) / b) by Lm17;

    theorem :: XCMPLX_1:188

    

     Th188: (a / ( - b)) = ( - (a / b))

    proof

      (a / ( - b)) = ((a * ( - 1)) / (( - b) * ( - 1))) by Lm10;

      

      then (a / ( - b)) = (( - a) / (( - ( - b)) * 1))

      .= ( - (a / b)) by Lm17;

      hence thesis;

    end;

    theorem :: XCMPLX_1:189

    ( - (a / ( - b))) = (a / b)

    proof

      

      thus ( - (a / ( - b))) = ( - ( - (a / b))) by Th188

      .= (a / b);

    end;

    theorem :: XCMPLX_1:190

    

     Th190: ( - (( - a) / b)) = (a / b)

    proof

      

      thus ( - (( - a) / b)) = ( - ( - (a / b))) by Lm17

      .= (a / b);

    end;

    theorem :: XCMPLX_1:191

    (( - a) / ( - b)) = (a / b)

    proof

      ( - (( - a) / b)) = (a / b) by Th190;

      hence thesis by Th188;

    end;

    theorem :: XCMPLX_1:192

    (( - a) / b) = (a / ( - b))

    proof

      

      thus (( - a) / b) = ( - (a / b)) by Lm17

      .= (a / ( - b)) by Th188;

    end;

    theorem :: XCMPLX_1:193

    ( - a) = (a / ( - 1));

    theorem :: XCMPLX_1:194

    a = (( - a) / ( - 1));

    theorem :: XCMPLX_1:195

    (a / b) = ( - 1) implies a = ( - b) & b = ( - a)

    proof

      assume

       A1: (a / b) = ( - 1);

      then b <> 0 by Th49;

      then a = (( - 1) * b) by A1, Lm3;

      hence thesis;

    end;

    theorem :: XCMPLX_1:196

    b <> 0 & (b / a) = ( - b) implies a = ( - 1)

    proof

      assume that

       A1: b <> 0 and

       A2: (b / a) = ( - b);

      a <> 0 by A1, A2, Th49;

      then b = (( - b) * a) by A2, Lm3;

      then b = ( - (b * a));

      hence thesis by A1, A2, Th181;

    end;

    theorem :: XCMPLX_1:197

    a <> 0 implies (( - a) / a) = ( - 1)

    proof

      assume

       A1: a <> 0 ;

      

      thus (( - a) / a) = ( - (a / a)) by Lm17

      .= ( - 1) by A1, Lm5;

    end;

    theorem :: XCMPLX_1:198

    a <> 0 implies (a / ( - a)) = ( - 1)

    proof

      assume

       A1: a <> 0 ;

      

      thus (a / ( - a)) = ( - (a / a)) by Th188

      .= ( - 1) by A1, Lm5;

    end;

    

     Lm18: a <> 0 & a = (a " ) implies a = 1 or a = ( - 1)

    proof

      assume

       A1: a <> 0 ;

      assume a = (a " );

      then (a * a) = 1 by A1, XCMPLX_0:def 7;

      hence thesis by Th182;

    end;

    theorem :: XCMPLX_1:199

    a <> 0 & a = (1 / a) implies a = 1 or a = ( - 1)

    proof

      assume a <> 0 ;

      then a = (a " ) implies a = 1 or a = ( - 1) by Lm18;

      hence thesis by Lm4;

    end;

    theorem :: XCMPLX_1:200

    b <> 0 & d <> 0 & b <> ( - d) & (a / b) = (e / d) implies (a / b) = ((a + e) / (b + d))

    proof

      assume that

       A1: b <> 0 and

       A2: d <> 0 and

       A3: b <> ( - d) and

       A4: (a / b) = (e / d);

      (a * d) = (e * b) by A1, A2, A4, Th95;

      then

       A5: (a * (b + d)) = ((a + e) * b);

      (b + d) <> 0 by A3;

      hence thesis by A1, A5, Th94;

    end;

    theorem :: XCMPLX_1:201

    (a " ) = (b " ) implies a = b by Lm12;

    theorem :: XCMPLX_1:202

    ( 0 " ) = 0 ;

    theorem :: XCMPLX_1:203

    b <> 0 implies a = ((a * b) * (b " ))

    proof

      

       A1: (a * (b * (b " ))) = ((a * b) * (b " ));

      assume b <> 0 ;

      then (a * 1) = ((a * b) * (b " )) by A1, XCMPLX_0:def 7;

      hence thesis;

    end;

    theorem :: XCMPLX_1:204

    ((a " ) * (b " )) = ((a * b) " ) by Lm1;

    theorem :: XCMPLX_1:205

    ((a * (b " )) " ) = ((a " ) * b) by Lm11;

    theorem :: XCMPLX_1:206

    (((a " ) * (b " )) " ) = (a * b)

    proof

      

      thus (((a " ) * (b " )) " ) = (((a " ) " ) * ((b " ) " )) by Lm1

      .= (a * b);

    end;

    theorem :: XCMPLX_1:207

    a <> 0 & b <> 0 implies (a * (b " )) <> 0 ;

    theorem :: XCMPLX_1:208

    a <> 0 & b <> 0 implies ((a " ) * (b " )) <> 0 ;

    theorem :: XCMPLX_1:209

    (a * (b " )) = 1 implies a = b

    proof

      assume (a * (b " )) = 1;

      then (a / b) = 1 by XCMPLX_0:def 9;

      hence thesis by Th58;

    end;

    theorem :: XCMPLX_1:210

    (a * b) = 1 implies a = (b " )

    proof

      assume

       A1: (a * b) = 1;

      then b <> 0 ;

      hence thesis by A1, XCMPLX_0:def 7;

    end;

    theorem :: XCMPLX_1:211

    

     Th211: a <> 0 & b <> 0 implies ((a " ) + (b " )) = ((a + b) * ((a * b) " ))

    proof

      assume that

       A1: a <> 0 and

       A2: b <> 0 ;

      (b " ) = ((b " ) * 1);

      then (b " ) = ((b " ) * ((a " ) * a)) by A1, XCMPLX_0:def 7;

      then (b " ) = (((a " ) * (b " )) * a);

      then

       A3: (b " ) = (((a * b) " ) * a) by Lm1;

      (a " ) = ((a " ) * 1);

      then (a " ) = ((a " ) * ((b " ) * b)) by A2, XCMPLX_0:def 7;

      then (a " ) = (((a " ) * (b " )) * b);

      then (a " ) = (((a * b) " ) * b) by Lm1;

      hence thesis by A3;

    end;

    

     Lm19: (( - a) " ) = ( - (a " ))

    proof

      

      thus (( - a) " ) = (1 / ( - a)) by Lm4

      .= ( - (1 / a)) by Th188

      .= ( - (a " )) by Lm4;

    end;

    theorem :: XCMPLX_1:212

    a <> 0 & b <> 0 implies ((a " ) - (b " )) = ((b - a) * ((a * b) " ))

    proof

      assume

       A1: a <> 0 & b <> 0 ;

      

      thus ((a " ) - (b " )) = ((a " ) + ( - (b " )))

      .= ((a " ) + (( - b) " )) by Lm19

      .= ((a + ( - b)) * ((a * ( - b)) " )) by A1, Th211

      .= ((a + ( - b)) * (( - (a * b)) " ))

      .= ((a + ( - b)) * ( - ((a * b) " ))) by Lm19

      .= ((b - a) * ((a * b) " ));

    end;

    theorem :: XCMPLX_1:213

    ((a / b) " ) = (b / a) by Lm7;

    theorem :: XCMPLX_1:214

    ((a " ) / (b " )) = (b / a)

    proof

      

      thus ((a " ) / (b " )) = ((a " ) * ((b " ) " )) by XCMPLX_0:def 9

      .= (b / a) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:215

    (1 / a) = (a " ) by Lm4;

    theorem :: XCMPLX_1:216

    (1 / (a " )) = a by Lm16;

    theorem :: XCMPLX_1:217

    ((1 / a) " ) = a

    proof

      (1 / a) = (a " ) implies ((1 / a) " ) = a;

      hence thesis by Lm4;

    end;

    theorem :: XCMPLX_1:218

    (1 / a) = (b " ) implies a = b

    proof

      (1 / a) = (1 / b) implies a = b by Th59;

      hence thesis by Lm4;

    end;

    theorem :: XCMPLX_1:219

    (a / (b " )) = (a * b)

    proof

      

      thus (a / (b " )) = (a * ((b " ) " )) by XCMPLX_0:def 9

      .= (a * b);

    end;

    theorem :: XCMPLX_1:220

    ((a " ) * (c / b)) = (c / (a * b))

    proof

      

      thus ((a " ) * (c / b)) = ((a " ) * (c * (b " ))) by XCMPLX_0:def 9

      .= (c * ((a " ) * (b " )))

      .= (c * ((a * b) " )) by Lm1

      .= (c / (a * b)) by XCMPLX_0:def 9;

    end;

    theorem :: XCMPLX_1:221

    ((a " ) / b) = ((a * b) " )

    proof

      

      thus ((a " ) / b) = ((a " ) * (b " )) by XCMPLX_0:def 9

      .= ((a * b) " ) by Lm1;

    end;

    theorem :: XCMPLX_1:222

    (( - a) " ) = ( - (a " )) by Lm19;

    theorem :: XCMPLX_1:223

    a <> 0 & a = (a " ) implies a = 1 or a = ( - 1) by Lm18;

    begin

    theorem :: XCMPLX_1:224

    (((a + b) + c) - b) = (a + c);

    theorem :: XCMPLX_1:225

    (((a - b) + c) + b) = (a + c);

    theorem :: XCMPLX_1:226

    (((a + b) - c) - b) = (a - c);

    theorem :: XCMPLX_1:227

    (((a - b) - c) + b) = (a - c);

    theorem :: XCMPLX_1:228

    ((a - a) - b) = ( - b);

    theorem :: XCMPLX_1:229

    ((( - a) + a) - b) = ( - b);

    theorem :: XCMPLX_1:230

    ((a - b) - a) = ( - b);

    theorem :: XCMPLX_1:231

    ((( - a) - b) + a) = ( - b);

    begin

    theorem :: XCMPLX_1:232

    for a, b st b <> 0 holds ex e st a = (b / e)

    proof

      let a, b;

      assume

       A1: b <> 0 ;

      per cases ;

        suppose

         A2: a = 0 ;

        take 0 ;

        (b / 0 ) = (b * ( 0 " )) by XCMPLX_0:def 9;

        hence thesis by A2;

      end;

        suppose

         A3: a <> 0 ;

        take e = (b / a);

        

        thus a = (a * 1)

        .= (a * (e * (e " ))) by A1, A3, XCMPLX_0:def 7

        .= ((a * e) * (e " ))

        .= ((a * ((a " ) * b)) * (e " )) by XCMPLX_0:def 9

        .= (((a * (a " )) * b) * (e " ))

        .= ((1 * b) * (e " )) by A3, XCMPLX_0:def 7

        .= (b / e) by XCMPLX_0:def 9;

      end;

    end;

    theorem :: XCMPLX_1:233

    (a / ((b * c) * (d / e))) = ((e / c) * (a / (b * d)))

    proof

      

      thus (a / ((b * c) * (d / e))) = (a / ((b * c) * (d * (e " )))) by XCMPLX_0:def 9

      .= (a / (c * ((b * d) * (e " ))))

      .= (a / (c * ((b * d) / e))) by XCMPLX_0:def 9

      .= (a / ((b * d) / (e / c))) by Th81

      .= ((e / c) * (a / (b * d))) by Th81;

    end;

    theorem :: XCMPLX_1:234

    ((((d - c) / b) * a) + c) = (((1 - (a / b)) * c) + ((a / b) * d))

    proof

      per cases ;

        suppose

         A1: b = 0 ;

        

         A2: (a / b) = (a * (b " )) by XCMPLX_0:def 9

        .= (a * 0 ) by A1;

        

        thus ((((d - c) / b) * a) + c) = ((((d - c) * (b " )) * a) + c) by XCMPLX_0:def 9

        .= ((((d - c) * 0 ) * a) + c) by A1

        .= (((1 - (a / b)) * c) + ((a / b) * d)) by A2;

      end;

        suppose

         A3: b <> 0 ;

        ((((d - c) / b) * a) + c) = ((((d - c) / b) * a) + (c * 1))

        .= ((((d - c) / b) * a) + (c * (b / b))) by A3, Lm5

        .= ((((d - c) / b) * a) + ((c * b) / b)) by Lm8

        .= ((((d - c) * a) / b) + ((c * b) / b)) by Lm8

        .= ((((d - c) * a) + (c * b)) / b) by Th62

        .= ((((b - a) * c) + (a * d)) / b)

        .= ((((b - a) * c) / b) + ((a * d) / b)) by Th62

        .= ((((b - a) * c) / b) + ((a / b) * d)) by Lm8

        .= ((((b - a) / b) * c) + ((a / b) * d)) by Lm8

        .= ((((b / b) - (a / b)) * c) + ((a / b) * d)) by Th120

        .= (((1 - (a / b)) * c) + ((a / b) * d)) by A3, Lm5;

        hence thesis;

      end;

    end;

    theorem :: XCMPLX_1:235

    a <> 0 implies ((a * b) + c) = (a * (b + (c / a)))

    proof

      assume a <> 0 ;

      

      hence ((a * b) + c) = ((a * b) + (a * (c / a))) by Lm3

      .= (a * (b + (c / a)));

    end;