THEOREM

*******

 

a^b^c=a^(b*c)  (for non-zero base (a) OR both non-zero exponents (b and c)

 

ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~a=0 | ~b=0 & ~c=0 => a^b^c=a^(b*c)]]

 

 

This machine-verified, formal proof was written with the aid of the author's DC Proof 2.0 freeware available at http://www.dcproof.com

 

Dan Christensen

2019-11-10

 

 

OUTLINE

*******

 

Lines     Content

*****     *******

 

1-16      Axioms/Definitions

 

17-19     Lemmas (links to proofs)

 

25-212    Case 1: Prove that ~x=0 => x^y^z=x^(y*z)  (by induction)

 

213-243   Case 2: Prove that ~y=0 & ~z=0 => x^y^z=x^(y*z)

 

 

 

AXIOMS/DEFINTITIONS

*******************

 

Define: n, 0, 1

 

1     Set(n)

      Axiom

 

2     0 e n

      Axiom

 

3     1 e n

      Axiom

 

 

Properties of +

***************

 

Closed on n

 

4     ALL(a):ALL(b):[a e n & b e n => a+b e n]

      Axiom

 

5     ALL(a):[a e n => a+0=a & 0+a=a]

      Axiom

 

 

Properties of *

***************

 

Closed on n

 

6     ALL(a):ALL(b):[a e n & b e n => a*b e n]

      Axiom

 

Multiplying by 0

 

7     ALL(a):[a e n => a*0=0]

      Axiom

 

Multiplying by 1

 

8     ALL(a):[a e n => a*1=a & 1*a=a]

      Axiom

 

Multiplying both sides

 

9     ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a=b => a*c=b*c]]

      Axiom

 

* Distributive over +

 

10   ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*(b+c)=a*b+a*c]

      Axiom

 

Product of non-zeroes

 

11   ALL(a):ALL(b):[a e n & b e n => [~a=0 & ~b=0 => ~a*b=0]]

      Axiom

 

Induction principle

 

12   ALL(a):[Set(a) & ALL(b):[b e a => b e n]

    => [0 e a & ALL(b):[b e a => b+1 e a]

    => ALL(b):[b e n => b e a]]]

      Axiom

 

 

Define: ^ on n

**************

 

13   ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => a^b e n]]

      Axiom

 

14   0^1=0

      Axiom

 

15   ALL(a):[a e n => [~a=0 => a^0=1]]

      Axiom

 

16   ALL(a):ALL(b):[a e n & b e n

    => [~[a=0 & b=0] => a^(b+1)=a^b*a]]

      Axiom

 

 

LEMMAS 

******

 

Non-zero powers of zero are zero                           Proof

 

17   ALL(a):[a e n => [~a=0 => 0^a=0]]

      Axiom

 

Powers of non-zero bases are non-zero                      Proof

 

18   ALL(a):ALL(b):[a e n & b e n => [~a=0 => ~a^b=0]]

      Axiom

 

Product of Powers                                          Proof

 

19   ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

    => [~a=0 | ~b=0 & ~c=0 => a^b*a^c=a^(b+c)]]

      Axiom

 

   

    PROOF

    *****

   

    Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

            => [~a=0 | ~b=0 & ~c=0 => a^b^c=a^(b*c)]]

   

    Suppose...

 

      20   x e n & y e n & z e n

            Premise

 

      21   x e n

            Split, 20

 

      22   y e n

            Split, 20

 

      23   z e n

            Split, 20

 

        

         Prove: ~x=0 | ~y=0 & ~z=0 => x^y^z=x^(y*z)

        

         Suppose... (two cases to consider)

 

            24   ~x=0 | ~y=0 & ~z=0

                  Premise

 

            

             Case 1

            

             Prove: ~x=0 => x^y^z=x^(y*z)           (by induction)

            

             Suppose...

 

                  25   ~x=0

                        Premise

 

            

             Construct set p for proof by induction

 

                  26   EXIST(sub):[Set(sub) & ALL(c):[c e sub <=> c e n & x^y^c=x^(y*c)]]

                        Subset, 1

 

                  27   Set(p) & ALL(c):[c e p <=> c e n & x^y^c=x^(y*c)]

                        E Spec, 26

 

            

             Define: p

 

                  28   Set(p)

                        Split, 27

 

                  29   ALL(c):[c e p <=> c e n & x^y^c=x^(y*c)]

                        Split, 27

 

             Apply principle of induction

 

                  30   Set(p) & ALL(b):[b e p => b e n]

                 => [0 e p & ALL(b):[b e p => b+1 e p]

                 => ALL(b):[b e n => b e p]]

                        U Spec, 12

 

                

                 Prove: ALL(b):[b e p => b e n]

                

                 Suppose...

 

                        31   t e p

                              Premise

 

                 Apply definition of p

 

                        32   t e p <=> t e n & x^y^t=x^(y*t)

                              U Spec, 29

 

                        33   [t e p => t e n & x^y^t=x^(y*t)]

                      & [t e n & x^y^t=x^(y*t) => t e p]

                              Iff-And, 32

 

                        34   t e p => t e n & x^y^t=x^(y*t)

                              Split, 33

 

                        35   t e n & x^y^t=x^(y*t) => t e p

                              Split, 33

 

                        36   t e n & x^y^t=x^(y*t)

                              Detach, 34, 31

 

                        37   t e n

                              Split, 36

 

             As Required:

 

                  38   ALL(b):[b e p => b e n]

                        4 Conclusion, 31

 

                  39   Set(p) & ALL(b):[b e p => b e n]

                        Join, 28, 38

 

            

             Sufficient: For ALL(b):[b e n => b e p]

 

                  40   0 e p & ALL(b):[b e p => b+1 e p]

                 => ALL(b):[b e n => b e p]

                        Detach, 30, 39

 

            

             BASE CASE

             *********

            

             Apply definition of p

 

                  41   0 e p <=> 0 e n & x^y^0=x^(y*0)

                        U Spec, 29

 

                  42   [0 e p => 0 e n & x^y^0=x^(y*0)]

                 & [0 e n & x^y^0=x^(y*0) => 0 e p]

                        Iff-And, 41

 

                  43   0 e p => 0 e n & x^y^0=x^(y*0)

                        Split, 42

 

             Sufficient: For 0 e p

 

                  44   0 e n & x^y^0=x^(y*0) => 0 e p

                        Split, 42

 

                  45   ALL(b):[x e n & b e n => [~[x=0 & b=0] => x^b e n]]

                        U Spec, 13

 

                  46   x e n & y e n => [~[x=0 & y=0] => x^y e n]

                        U Spec, 45

 

                  47   x e n & y e n

                        Join, 21, 22

 

                  48   ~[x=0 & y=0] => x^y e n

                        Detach, 46, 47

 

                 Prove: ~[x=0 & y=0]

                

                 Suppose to the contrary...

 

                        49   x=0 & y=0

                              Premise

 

                        50   x=0

                              Split, 49

 

                        51   y=0

                              Split, 49

 

                        52   x=0 & ~x=0

                              Join, 50, 25

 

             As Required:

 

                  53   ~[x=0 & y=0]

                        4 Conclusion, 49

 

                  54   x^y e n

                        Detach, 48, 53

 

             Apply axiom

 

                  55   x^y e n => [~x^y=0 => x^y^0=1]

                        U Spec, 15, 54

 

                  56   ~x^y=0 => x^y^0=1

                        Detach, 55, 54

 

             Apply lemma

 

                  57   ALL(b):[x e n & b e n => [~x=0 => ~x^b=0]]

                        U Spec, 18

 

                  58   x e n & y e n => [~x=0 => ~x^y=0]

                        U Spec, 57

 

                  59   x e n & y e n

                        Join, 21, 22

 

                  60   ~x=0 => ~x^y=0

                        Detach, 58, 59

 

                  61   ~x^y=0

                        Detach, 60, 25

 

                  62   x^y^0=1

                        Detach, 56, 61

 

             Apply axiom

 

                  63   y e n => y*0=0

                        U Spec, 7

 

                  64   y*0=0

                        Detach, 63, 22

 

                  65   0 e n & x^y^0=x^0 => 0 e p

                        Substitute, 64, 44

 

                  66   0 e n & 1=x^0 => 0 e p

                        Substitute, 62, 65

 

             Apply axiom

 

                  67   x e n => [~x=0 => x^0=1]

                        U Spec, 15

 

                  68   ~x=0 => x^0=1

                        Detach, 67, 21

 

                  69   x^0=1

                        Detach, 68, 25

 

                  70   0 e n & 1=1 => 0 e p

                        Substitute, 69, 66

 

                  71   1=1

                        Reflex

 

                  72   0 e n & 1=1

                        Join, 2, 71

 

            

             As Required:

 

                  73   0 e p

                        Detach, 70, 72

 

                

                 INDUCTIVE STEP

                 **************

                

                 Prove: ALL(b):[b e p => b+1 e p]

                

                 Suppose...

 

                        74   t e p

                              Premise

 

                 Apply definition of p

 

                        75   t e p <=> t e n & x^y^t=x^(y*t)

                              U Spec, 29

 

                        76   [t e p => t e n & x^y^t=x^(y*t)]

                      & [t e n & x^y^t=x^(y*t) => t e p]

                              Iff-And, 75

 

                        77   t e p => t e n & x^y^t=x^(y*t)

                              Split, 76

 

                        78   t e n & x^y^t=x^(y*t) => t e p

                              Split, 76

 

                        79   t e n & x^y^t=x^(y*t)

                              Detach, 77, 74

 

                        80   t e n

                              Split, 79

 

                 Multiply both sides by x^y

 

                        81   x^y^t=x^(y*t)

                              Split, 79

 

                 Apply axiom

 

                        82   ALL(b):[t e n & b e n => t+b e n]

                              U Spec, 4

 

                        83   t e n & 1 e n => t+1 e n

                              U Spec, 82

 

                        84   t e n & 1 e n

                              Join, 80, 3

 

                        85   t+1 e n

                              Detach, 83, 84

 

                 Apply definition of p

 

                        86   t+1 e p <=> t+1 e n & x^y^(t+1)=x^(y*(t+1))

                              U Spec, 29, 85

 

                        87   [t+1 e p => t+1 e n & x^y^(t+1)=x^(y*(t+1))]

                      & [t+1 e n & x^y^(t+1)=x^(y*(t+1)) => t+1 e p]

                              Iff-And, 86

 

                        88   t+1 e p => t+1 e n & x^y^(t+1)=x^(y*(t+1))

                              Split, 87

 

                

                 Sufficient: For t+1 e p

 

                        89   t+1 e n & x^y^(t+1)=x^(y*(t+1)) => t+1 e p

                              Split, 87

 

                 Apply axiom

 

                        90   ALL(b):[x e n & b e n => [~[x=0 & b=0] => x^b e n]]

                              U Spec, 13

 

                        91   x e n & y e n => [~[x=0 & y=0] => x^y e n]

                              U Spec, 90

 

                        92   x e n & y e n

                              Join, 21, 22

 

                        93   ~[x=0 & y=0] => x^y e n

                              Detach, 91, 92

 

                        94   x^y e n

                              Detach, 93, 53

 

                 Apply axiom

 

                        95   ALL(b):[x^y e n & b e n => [~[x^y=0 & b=0] => x^y^b e n]]

                              U Spec, 13, 94

 

                        96   x^y e n & t e n => [~[x^y=0 & t=0] => x^y^t e n]

                              U Spec, 95

 

                        97   x^y e n & t e n

                              Join, 94, 80

 

                        98   ~[x^y=0 & t=0] => x^y^t e n

                              Detach, 96, 97

 

                     

                      Prove: ~[x^y=0 & t=0]

                     

                      Suppose to the contrary...

 

                              99   x^y=0 & t=0

                                    Premise

 

                              100  x^y=0

                                    Split, 99

 

                              101  t=0

                                    Split, 99

 

                      Apply lemma

 

                              102  ALL(b):[x e n & b e n => [~x=0 => ~x^b=0]]

                                    U Spec, 18

 

                              103  x e n & y e n => [~x=0 => ~x^y=0]

                                    U Spec, 102

 

                              104  x e n & y e n

                                    Join, 21, 22

 

                              105  ~x=0 => ~x^y=0

                                    Detach, 103, 104

 

                              106  ~x^y=0

                                    Detach, 105, 25

 

                              107  x^y=0 & ~x^y=0

                                    Join, 100, 106

 

                 As Required:

 

                        108  ~[x^y=0 & t=0]

                              4 Conclusion, 99

 

                        109  x^y^t e n

                              Detach, 98, 108

 

                 Apply axiom

 

                        110  ALL(b):[y e n & b e n => y*b e n]

                              U Spec, 6

 

                        111  y e n & t e n => y*t e n

                              U Spec, 110

 

                        112  y e n & t e n

                              Join, 22, 80

 

                        113  y*t e n

                              Detach, 111, 112

 

                 Apply axiom

 

                        114  ALL(b):[x e n & b e n => [~[x=0 & b=0] => x^b e n]]

                              U Spec, 13

 

                        115  x e n & y*t e n => [~[x=0 & y*t=0] => x^(y*t) e n]

                              U Spec, 114, 113

 

                        116  x e n & y*t e n

                              Join, 21, 113

 

                        117  ~[x=0 & y*t=0] => x^(y*t) e n

                              Detach, 115, 116

 

                      Prove: ~[x=0 & y*t=0]

                     

                      Suppose to the contrary...

 

                              118  x=0 & y*t=0

                                    Premise

 

                              119  x=0

                                    Split, 118

 

                              120  y*t=0

                                    Split, 118

 

                              121  x=0 & ~x=0

                                    Join, 119, 25

 

                 As Required:

 

                        122  ~[x=0 & y*t=0]

                              4 Conclusion, 118

 

                        123  x^(y*t) e n

                              Detach, 117, 122

 

                 Apply axiom

 

                        124  ALL(b):ALL(c):[x^y^t e n & b e n & c e n => [x^y^t=b => x^y^t*c=b*c]]

                              U Spec, 9, 109

 

                        125  ALL(c):[x^y^t e n & x^(y*t) e n & c e n => [x^y^t=x^(y*t) => x^y^t*c=x^(y*t)*c]]

                              U Spec, 124, 123

 

                        126  x^y^t e n & x^(y*t) e n & x^y e n => [x^y^t=x^(y*t) => x^y^t*x^y=x^(y*t)*x^y]

                              U Spec, 125, 94

 

                        127  x^y^t e n & x^(y*t) e n

                              Join, 109, 123

 

                        128  x^y^t e n & x^(y*t) e n & x^y e n

                              Join, 127, 94

 

                        129  x^y^t=x^(y*t) => x^y^t*x^y=x^(y*t)*x^y

                              Detach, 126, 128

 

                        130  x^y^t*x^y=x^(y*t)*x^y

                              Detach, 129, 81

 

                        131  x^y e n => [~x^y=0 => x^y^0=1]

                              U Spec, 15, 94

 

                        132  ~x^y=0 => x^y^0=1

                              Detach, 131, 94

 

                 Apply lemma

 

                        133  ALL(b):[x e n & b e n => [~x=0 => ~x^b=0]]

                              U Spec, 18

 

                        134  x e n & y e n => [~x=0 => ~x^y=0]

                              U Spec, 133

 

                        135  x e n & y e n

                              Join, 21, 22

 

                        136  ~x=0 => ~x^y=0

                              Detach, 134, 135

 

                        137  ~x^y=0

                              Detach, 136, 25

 

                        138  x^y^0=1

                              Detach, 132, 137

 

                 Apply axiom

 

                        139  ALL(b):[x^y e n & b e n

                      => [~[x^y=0 & b=0] => x^y^(b+1)=x^y^b*x^y]]

                              U Spec, 16, 94

 

                        140  x^y e n & 0 e n

                      => [~[x^y=0 & 0=0] => x^y^(0+1)=x^y^0*x^y]

                              U Spec, 139

 

                        141  x^y e n & 0 e n

                              Join, 94, 2

 

                        142  ~[x^y=0 & 0=0] => x^y^(0+1)=x^y^0*x^y

                              Detach, 140, 141

 

                      Prove: ~[x^y=0 & 0=0]

                     

                      Suppose to the contrary...

 

                              143  x^y=0 & 0=0

                                    Premise

 

                              144  x^y=0

                                    Split, 143

 

                              145  0=0

                                    Split, 143

 

                              146  x^y=0 & ~x^y=0

                                    Join, 144, 137

 

                 As Required:

 

                        147  ~[x^y=0 & 0=0]

                              4 Conclusion, 143

 

                        148  x^y^(0+1)=x^y^0*x^y

                              Detach, 142, 147

 

                  Apply axiom

 

                        149  1 e n => 1+0=1 & 0+1=1

                              U Spec, 5

 

                        150  1+0=1 & 0+1=1

                              Detach, 149, 3

 

                        151  1+0=1

                              Split, 150

 

                        152  0+1=1

                              Split, 150

 

                        153  x^y^1=x^y^0*x^y

                              Substitute, 152, 148

 

                        154  x^y e n => [~x^y=0 => x^y^0=1]

                              U Spec, 15, 94

 

                        155  ~x^y=0 => x^y^0=1

                              Detach, 154, 54

 

                        156  x^y^0=1

                              Detach, 155, 137

 

                        157  x^y^1=1*x^y

                              Substitute, 156, 153

 

                        158  x^y e n => x^y*1=x^y & 1*x^y=x^y

                              U Spec, 8, 94

 

                        159  x^y*1=x^y & 1*x^y=x^y

                              Detach, 158, 94

 

                        160  x^y*1=x^y

                              Split, 159

 

                        161  1*x^y=x^y

                              Split, 159

 

                        162  x^y^1=x^y

                              Substitute, 161, 157

 

                        163  x^y^t*x^y^1=x^(y*t)*x^y

                              Substitute, 162, 130

 

                        164  ALL(b):ALL(c):[x^y e n & b e n & c e n

                      => [~x^y=0 | ~b=0 & ~c=0 => x^y^b*x^y^c=x^y^(b+c)]]

                              U Spec, 19, 94

 

                        165  ALL(c):[x^y e n & t e n & c e n

                      => [~x^y=0 | ~t=0 & ~c=0 => x^y^t*x^y^c=x^y^(t+c)]]

                              U Spec, 164

 

                        166  x^y e n & t e n & 1 e n

                      => [~x^y=0 | ~t=0 & ~1=0 => x^y^t*x^y^1=x^y^(t+1)]

                              U Spec, 165

 

                        167  x^y e n & t e n

                              Join, 94, 80

 

                        168  x^y e n & t e n & 1 e n

                              Join, 167, 3

 

                        169  ~x^y=0 | ~t=0 & ~1=0 => x^y^t*x^y^1=x^y^(t+1)

                              Detach, 166, 168

 

                        170  ~x^y=0 | ~t=0 & ~1=0

                              Arb Or, 137

 

                        171  x^y^t*x^y^1=x^y^(t+1)

                              Detach, 169, 170

 

                        172  x^y^(t+1)=x^(y*t)*x^y

                              Substitute, 171, 163

 

                        173  ALL(b):ALL(c):[x e n & b e n & c e n

                      => [~x=0 | ~b=0 & ~c=0 => x^b*x^c=x^(b+c)]]

                              U Spec, 19

 

                        174  ALL(c):[x e n & y*t e n & c e n

                      => [~x=0 | ~y*t=0 & ~c=0 => x^(y*t)*x^c=x^(y*t+c)]]

                              U Spec, 173, 113

 

                        175  x e n & y*t e n & y e n

                      => [~x=0 | ~y*t=0 & ~y=0 => x^(y*t)*x^y=x^(y*t+y)]

                              U Spec, 174

 

                        176  x e n & y*t e n

                              Join, 21, 113

 

                        177  x e n & y*t e n & y e n

                              Join, 176, 22

 

                        178  ~x=0 | ~y*t=0 & ~y=0 => x^(y*t)*x^y=x^(y*t+y)

                              Detach, 175, 177

 

                        179  ~x=0 | ~y*t=0 & ~y=0

                              Arb Or, 25

 

                        180  x^(y*t)*x^y=x^(y*t+y)

                              Detach, 178, 179

 

                        181  x^y^(t+1)=x^(y*t+y)

                              Substitute, 180, 172

 

                        182  ALL(b):ALL(c):[y e n & b e n & c e n => y*(b+c)=y*b+y*c]

                              U Spec, 10

 

                        183  ALL(c):[y e n & t e n & c e n => y*(t+c)=y*t+y*c]

                              U Spec, 182

 

                        184  y e n & t e n & 1 e n => y*(t+1)=y*t+y*1

                              U Spec, 183

 

                        185  y e n & t e n

                              Join, 22, 80

 

                        186  y e n & t e n & 1 e n

                              Join, 185, 3

 

                        187  y*(t+1)=y*t+y*1

                              Detach, 184, 186

 

                        188  y e n => y*1=y & 1*y=y

                              U Spec, 8

 

                        189  y*1=y & 1*y=y

                              Detach, 188, 22

 

                        190  y*1=y

                              Split, 189

 

                        191  1*y=y

                              Split, 189

 

                        192  y*(t+1)=y*t+y

                              Substitute, 190, 187

 

                        193  x^y^(t+1)=x^(y*(t+1))

                              Substitute, 192, 181

 

                        194  t+1 e n & x^y^(t+1)=x^(y*(t+1))

                              Join, 85, 193

 

                        195  t+1 e p

                              Detach, 89, 194

 

             As Required:

 

                  196  ALL(b):[b e p => b+1 e p]

                        4 Conclusion, 74

 

             Joining results

 

                  197  0 e p & ALL(b):[b e p => b+1 e p]

                        Join, 73, 196

 

             As Required:

 

                  198  ALL(b):[b e n => b e p]

                        Detach, 40, 197

 

                

                 Prove: ALL(b):[b e n => x^y^b=x^(y*b)]

                

                 Suppose...

 

                        199  t e n

                              Premise

 

                        200  t e n => t e p

                              U Spec, 198

 

                        201  t e p

                              Detach, 200, 199

 

                 Apply definition of p

 

                        202  t e p <=> t e n & x^y^t=x^(y*t)

                              U Spec, 29

 

                        203  [t e p => t e n & x^y^t=x^(y*t)]

                      & [t e n & x^y^t=x^(y*t) => t e p]

                              Iff-And, 202

 

                        204  t e p => t e n & x^y^t=x^(y*t)

                              Split, 203

 

                        205  t e n & x^y^t=x^(y*t) => t e p

                              Split, 203

 

                        206  t e n & x^y^t=x^(y*t)

                              Detach, 204, 201

 

                        207  t e n

                              Split, 206

 

                        208  x^y^t=x^(y*t)

                              Split, 206

 

             As Required:

 

                  209  ALL(b):[b e n => x^y^b=x^(y*b)]

                        4 Conclusion, 199

 

                  210  z e n => x^y^z=x^(y*z)

                        U Spec, 209

 

                  211  x^y^z=x^(y*z)

                        Detach, 210, 23

 

        

         Case 1

        

         As Required:

 

            212  ~x=0 => x^y^z=x^(y*z)

                  4 Conclusion, 25

 

            

             Case 2

            

             Prove: ~y=0 & ~z=0 => x^y^z=x^(y*z)

            

             Suppose...

 

                  213  ~y=0 & ~z=0

                        Premise

 

                  214  ~y=0

                        Split, 213

 

                  215  ~z=0

                        Split, 213

 

             Two sub-cases

 

                  216  x=0 | ~x=0

                        Or Not

 

                

                 Sub-case 1

                

                 Prove: x=0 => x^y^z=x^(y*z)

                

                 Suppose...

 

                        217  x=0

                              Premise

 

                        218  y e n => [~y=0 => 0^y=0]

                              U Spec, 17

 

                        219  ~y=0 => 0^y=0

                              Detach, 218, 22

 

                        220  0^y=0

                              Detach, 219, 214

 

                        221  x^y=0

                              Substitute, 217, 220

 

                        222  z e n => [~z=0 => 0^z=0]

                              U Spec, 17

 

                        223  ~z=0 => 0^z=0

                              Detach, 222, 23

 

                        224  0^z=0

                              Detach, 223, 215

 

                 LHS

 

                        225  x^y^z=0

                              Substitute, 221, 224

 

                        226  ALL(b):[y e n & b e n => y*b e n]

                              U Spec, 6

 

                        227  y e n & z e n => y*z e n

                              U Spec, 226

 

                        228  y e n & z e n

                              Join, 22, 23

 

                        229  y*z e n

                              Detach, 227, 228

 

                        230  y*z e n => [~y*z=0 => 0^(y*z)=0]

                              U Spec, 17, 229

 

                        231  ~y*z=0 => 0^(y*z)=0

                              Detach, 230, 229

 

                        232  ALL(b):[y e n & b e n => [~y=0 & ~b=0 => ~y*b=0]]

                              U Spec, 11

 

                        233  y e n & z e n => [~y=0 & ~z=0 => ~y*z=0]

                              U Spec, 232

 

                        234  y e n & z e n

                              Join, 22, 23

 

                        235  ~y=0 & ~z=0 => ~y*z=0

                              Detach, 233, 234

 

                        236  ~y*z=0

                              Detach, 235, 213

 

                        237  0^(y*z)=0

                              Detach, 231, 236

 

                        238  x^(y*z)=0

                              Substitute, 217, 237

 

                        239  x^y^z=x^(y*z)

                              Substitute, 238, 225

 

            

             Sub-case 1

            

             As Required:

 

                  240  x=0 => x^y^z=x^(y*z)

                        4 Conclusion, 217

 

             Joining results...

            

             Latter is sub-case 2

 

                  241  [x=0 => x^y^z=x^(y*z)] & [~x=0 => x^y^z=x^(y*z)]

                        Join, 240, 212

 

                  242  x^y^z=x^(y*z)

                        Cases, 216, 241

 

         Case 2

        

         As Required:

 

            243  ~y=0 & ~z=0 => x^y^z=x^(y*z)

                  4 Conclusion, 213

 

            244  [~x=0 => x^y^z=x^(y*z)]

             & [~y=0 & ~z=0 => x^y^z=x^(y*z)]

                  Join, 212, 243

 

            245  x^y^z=x^(y*z)

                  Cases, 24, 244

 

    As Required:

 

      246  ~x=0 | ~y=0 & ~z=0 => x^y^z=x^(y*z)

            4 Conclusion, 24

 

 

As Required:

 

247  ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n

    => [~a=0 | ~b=0 & ~c=0 => a^b^c=a^(b*c)]]

      4 Conclusion, 20