THEOREM

*******

 

(a*b)^c = a^c * b^c  (for non-zero exponent (c) OR both non-zero bases (a and b))

 

ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~c=0 | ~a=0 & ~b=0 => (a*b)^c = a^c * 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-15     Axioms/Definitions for n, 0, 1, +, *, ^

 

16       Lemma for non-zero exponents of zero  (link to proof)

 

17-201   Prove that if ~a=0 and ~b=0, then (a*b)^c=a^c*b^c for all c e n (by induction).

 

202-297  Prove that if ~c=0, then (a*b)^c=a^c*b^c for all a, b e n.

 

298-319  Combine results to obtain theorem as required.

 

 

 

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

 

 

Properties of *

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

 

Closed on n

 

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

      Axiom

 

Multiplying by 0

 

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

      Axiom

 

Multiplying by 1

 

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

      Axiom

 

* Associative

 

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

      Axiom

 

* Commutative

 

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

      Axiom

 

Product on non-zero numbers

 

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

      Axiom

 

Principle of Mathematical Induction (used for proof by induction)

 

11   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

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

 

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

      Axiom

 

13   0^1=0

      Axiom

 

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

      Axiom

 

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

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

      Axiom

 

 

LEMMA

*****

 

Non-zero exponents of zero                   Proof

 

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

      Axiom

 

   

    PROOF

    *****

   

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

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

   

    Suppose...

 

      17   x e n & y e n

            Premise

 

      18   x e n

            Split, 17

 

      19   y e n

            Split, 17

 

        

         Prove: ~x=0 & ~y=0 => ALL(c):[c e n => (x*y)^c=x^c*y^c]

        

         Suppose...

 

            20   ~x=0 & ~y=0

                  Premise

 

            21   ~x=0

                  Split, 20

 

            22   ~y=0

                  Split, 20

 

         Prove: ALL(c):[c e n => (x*y)^c=x^c*y^c]  (by induction)

        

         Construct set p

 

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

                  Subset, 1

 

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

                  E Spec, 23

 

        

         Define: p

 

            25   Set(p)

                  Split, 24

 

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

                  Split, 24

 

         Apply Principle of Induction

 

            27   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, 11

 

            

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

            

             Suppose...

 

                  28   t e p

                        Premise

 

             Apply definition of p

 

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

                        U Spec, 26

 

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

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

                        Iff-And, 29

 

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

                        Split, 30

 

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

                        Split, 30

 

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

                        Detach, 31, 28

 

                  34   t e n

                        Split, 33

 

         As Required:

 

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

                  4 Conclusion, 28

 

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

                  Join, 25, 35

 

        

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

 

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

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

                  Detach, 27, 36

 

        

         BASE CASE

         *********

        

         Apply definition of p

 

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

                  U Spec, 26

 

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

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

                  Iff-And, 38

 

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

                  Split, 39

 

        

         Sufficient: For 0 e p

 

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

                  Split, 39

 

         Apply axiom

 

            42   ALL(b):[x e n & b e n => [~x=0 & ~b=0 => ~x*b=0]]

                  U Spec, 10

 

            43   x e n & y e n => [~x=0 & ~y=0 => ~x*y=0]

                  U Spec, 42

 

            44   ~x=0 & ~y=0 => ~x*y=0

                  Detach, 43, 17

 

            45   ~x*y=0

                  Detach, 44, 20

 

         Apply axiom

 

            46   ALL(b):[x e n & b e n => x*b e n]

                  U Spec, 5

 

            47   x e n & y e n => x*y e n

                  U Spec, 46

 

            48   x*y e n

                  Detach, 47, 17

 

         Apply axiom

 

            49   x*y e n => [~x*y=0 => (x*y)^0=1]

                  U Spec, 14, 48

 

            50   ~x*y=0 => (x*y)^0=1

                  Detach, 49, 48

 

         LHS

 

            51   (x*y)^0=1

                  Detach, 50, 45

 

         Apply axiom

 

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

                  U Spec, 14

 

            53   ~x=0 => x^0=1

                  Detach, 52, 18

 

            54   x^0=1

                  Detach, 53, 21

 

         Apply axiom

 

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

                  U Spec, 14

 

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

                  Detach, 55, 19

 

            57   y^0=1

                  Detach, 56, 22

 

         Apply axiom

 

            58   1 e n => 1*1=1 & 1*1=1

                  U Spec, 7

 

            59   1*1=1 & 1*1=1

                  Detach, 58, 3

 

            60   1*1=1

                  Split, 59

 

            61   1*1=1

                  Split, 59

 

            62   x^0*1=1

                  Substitute, 54, 61

 

         RHS

 

            63   x^0*y^0=1

                  Substitute, 57, 62

 

            64   (x*y)^0=x^0*y^0

                  Substitute, 63, 51

 

            65   0 e n & (x*y)^0=x^0*y^0

                  Join, 2, 64

 

        

         As Required:

 

            66   0 e p

                  Detach, 41, 65

 

            

             INDUCTIVE STEP

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

            

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

            

             Suppose...

 

                  67   t e p

                        Premise

 

             Apply definition of p

 

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

                        U Spec, 26

 

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

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

                        Iff-And, 68

 

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

                        Split, 69

 

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

                        Split, 69

 

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

                        Detach, 70, 67

 

                  73   t e n

                        Split, 72

 

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

                        Split, 72

 

             Apply axiom

 

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

                        U Spec, 4

 

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

                        U Spec, 75

 

                  77   t e n & 1 e n

                        Join, 73, 3

 

                  78   t+1 e n

                        Detach, 76, 77

 

             Apply definition of p

 

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

                        U Spec, 26, 78

 

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

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

                        Iff-And, 79

 

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

                        Split, 80

 

            

             Sufficient: For t+1 e p

 

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

                        Split, 80

 

             Apply axiom

 

                  83   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, 15, 48

 

                  84   x*y e n & t e n

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

                        U Spec, 83

 

                  85   x*y e n & t e n

                        Join, 48, 73

 

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

                        Detach, 84, 85

 

                        87   x*y=0 & t=0

                              Premise

 

                        88   x*y=0

                              Split, 87

 

                        89   t=0

                              Split, 87

 

                        90   x*y=0 & ~x*y=0

                              Join, 88, 45

 

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

                        4 Conclusion, 87

 

             LHS

 

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

                        Detach, 86, 91

 

             Rearrange terms using associativity and commutativity

 

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

                        Substitute, 74, 92

 

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

                        U Spec, 12

 

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

                        U Spec, 94

 

                  96   x e n & t e n

                        Join, 18, 73

 

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

                        Detach, 95, 96

 

                

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

                

                 Suppose to the contrary...

 

                        98   x=0 & t=0

                              Premise

 

                        99   x=0

                              Split, 98

 

                        100  t=0

                              Split, 98

 

                        101  x=0 & ~x=0

                              Join, 99, 21

 

             As Required:

 

                  102  ~[x=0 & t=0]

                        4 Conclusion, 98

 

                  103  x^t e n

                        Detach, 97, 102

 

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

                        U Spec, 12

 

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

                        U Spec, 104

 

                  106  y e n & t e n

                        Join, 19, 73

 

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

                        Detach, 105, 106

 

                        108  y=0 & t=0

                              Premise

 

                        109  y=0

                              Split, 108

 

                        110  t=0

                              Split, 108

 

                        111  y=0 & ~y=0

                              Join, 109, 22

 

                  112  ~[y=0 & t=0]

                        4 Conclusion, 108

 

                  113  y^t e n

                        Detach, 107, 112

 

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

                        U Spec, 8, 103

 

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

                        U Spec, 114, 113

 

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

                        U Spec, 115, 48

 

                  117  x^t e n & y^t e n

                        Join, 103, 113

 

                  118  x^t e n & y^t e n & x*y e n

                        Join, 117, 48

 

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

                        Detach, 116, 118

 

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

                        Substitute, 119, 93

 

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

                        U Spec, 9, 113

 

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

                        U Spec, 121, 48

 

                  123  y^t e n & x*y e n

                        Join, 113, 48

 

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

                        Detach, 122, 123

 

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

                        Substitute, 124, 120

 

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

                        U Spec, 8, 103

 

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

                        U Spec, 126, 48

 

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

                        U Spec, 127, 113

 

                  129  x^t e n & x*y e n

                        Join, 103, 48

 

                  130  x^t e n & x*y e n & y^t e n

                        Join, 129, 113

 

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

                        Detach, 128, 130

 

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

                        Substitute, 131, 125

 

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

                        U Spec, 8, 103

 

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

                        U Spec, 133

 

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

                        U Spec, 134

 

                  136  x^t e n & x e n

                        Join, 103, 18

 

                  137  x^t e n & x e n & y e n

                        Join, 136, 19

 

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

                        Detach, 135, 137

 

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

                        Substitute, 138, 132

 

                  140  ALL(b):[x e n & b e n

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

                        U Spec, 15

 

                  141  x e n & t e n

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

                        U Spec, 140

 

                  142  x e n & t e n

                        Join, 18, 73

 

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

                        Detach, 141, 142

 

                        144  x=0 & t=0

                              Premise

 

                        145  x=0

                              Split, 144

 

                        146  t=0

                              Split, 144

 

                        147  x=0 & ~x=0

                              Join, 145, 21

 

                  148  ~[x=0 & t=0]

                        4 Conclusion, 144

 

                  149  x^(t+1)=x^t*x

                        Detach, 143, 148

 

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

                        Substitute, 149, 139

 

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

                        U Spec, 12

 

                  152  x e n & t+1 e n => [~[x=0 & t+1=0] => x^(t+1) e n]

                        U Spec, 151, 78

 

                  153  x e n & t+1 e n

                        Join, 18, 78

 

                  154  ~[x=0 & t+1=0] => x^(t+1) e n

                        Detach, 152, 153

 

                        155  x=0 & t+1=0

                              Premise

 

                        156  x=0

                              Split, 155

 

                        157  t+1=0

                              Split, 155

 

                        158  x=0 & ~x=0

                              Join, 156, 21

 

                  159  ~[x=0 & t+1=0]

                        4 Conclusion, 155

 

                  160  x^(t+1) e n

                        Detach, 154, 159

 

                  161  ALL(b):ALL(c):[x^(t+1) e n & b e n & c e n => x^(t+1)*b*c=x^(t+1)*(b*c)]

                        U Spec, 8, 160

 

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

                        U Spec, 161

 

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

                        U Spec, 162, 113

 

                  164  x^(t+1) e n & y e n

                        Join, 160, 19

 

                  165  x^(t+1) e n & y e n & y^t e n

                        Join, 164, 113

 

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

                        Detach, 163, 165

 

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

                        Substitute, 166, 150

 

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

                        U Spec, 9

 

                  169  y e n & y^t e n => y*y^t=y^t*y

                        U Spec, 168, 113

 

                  170  y e n & y^t e n

                        Join, 19, 113

 

                  171  y*y^t=y^t*y

                        Detach, 169, 170

 

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

                        Substitute, 171, 167

 

                  173  ALL(b):[y e n & b e n

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

                        U Spec, 15

 

                  174  y e n & t e n

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

                        U Spec, 173

 

                  175  y e n & t e n

                        Join, 19, 73

 

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

                        Detach, 174, 175

 

                        177  y=0 & t=0

                              Premise

 

                        178  y=0

                              Split, 177

 

                        179  t=0

                              Split, 177

 

                        180  y=0 & ~y=0

                              Join, 178, 22

 

                  181  ~[y=0 & t=0]

                        4 Conclusion, 177

 

                  182  y^(t+1)=y^t*y

                        Detach, 176, 181

 

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

                        Substitute, 182, 172

 

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

                        Join, 78, 183

 

                  185  t+1 e p

                        Detach, 82, 184

 

         As Required:

 

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

                  4 Conclusion, 67

 

         Joining results...

 

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

                  Join, 66, 186

 

         As Required:

 

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

                  Detach, 37, 187

 

            

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

            

             Suppose...

 

                  189  z e n

                        Premise

 

                  190  z e n => z e p

                        U Spec, 188

 

                  191  z e p

                        Detach, 190, 189

 

             Apply definition of p

 

                  192  z e p <=> z e n & (x*y)^z=x^z*y^z

                        U Spec, 26

 

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

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

                        Iff-And, 192

 

                  194  z e p => z e n & (x*y)^z=x^z*y^z

                        Split, 193

 

                  195  z e n & (x*y)^z=x^z*y^z => z e p

                        Split, 193

 

                  196  z e n & (x*y)^z=x^z*y^z

                        Detach, 194, 191

 

                  197  z e n

                        Split, 196

 

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

                        Split, 196

 

         As Required:

 

            199  ALL(c):[c e n => (x*y)^c=x^c*y^c]

                  4 Conclusion, 189

 

    As Required:

 

      200  ~x=0 & ~y=0 => ALL(c):[c e n => (x*y)^c=x^c*y^c]

            4 Conclusion, 20

 

 

As Required:

 

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

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

      4 Conclusion, 17

 

   

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

   

    Suppose...

 

      202  x e n & y e n & z e n

            Premise

 

      203  x e n

            Split, 202

 

      204  y e n

            Split, 202

 

      205  z e n

            Split, 202

 

    Two cases:

 

      206  x=0 | ~x=0

            Or Not

 

    Two sub-cases

 

      207  y=0 | ~y=0

            Or Not

 

        

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

        

         Suppose...

 

            208  ~z=0

                  Premise

 

         Apply lemma

 

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

                  U Spec, 16

 

            210  ~z=0 => 0^z=0

                  Detach, 209, 205

 

            211  0^z=0

                  Detach, 210, 208

 

             Case 1

            

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

            

             Suppose...

 

                  212  x=0

                        Premise

 

                 Sub-case 1

                

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

                

                 Suppose...

 

                        213  y=0

                              Premise

 

                 Apply axiom

 

                        214  0 e n => 0*0=0 & 0*0=0

                              U Spec, 6

 

                        215  0*0=0 & 0*0=0

                              Detach, 214, 2

 

                        216  0*0=0

                              Split, 215

 

                        217  0*0=0

                              Split, 215

 

                        218  x*0=0

                              Substitute, 212, 217

 

                        219  x*y=0

                              Substitute, 213, 218

 

                 LHS

 

                        220  (x*y)^z=0

                              Substitute, 219, 211

 

                        221  x^z=0

                              Substitute, 212, 211

 

                        222  y^z=0

                              Substitute, 213, 211

 

                        223  x^z*0=0

                              Substitute, 221, 217

 

                 RHS

 

                        224  x^z*y^z=0

                              Substitute, 222, 223

 

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

                              Substitute, 224, 220

 

             Sub-case 1

            

             As Required:

 

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

                        4 Conclusion, 213

 

                 Sub-case 2

                

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

                

                 Suppose...

 

                        227  ~y=0

                              Premise

 

                        228  y e n => y*0=0 & 0*y=0

                              U Spec, 6

 

                        229  y*0=0 & 0*y=0

                              Detach, 228, 204

 

                        230  y*0=0

                              Split, 229

 

                        231  0*y=0

                              Split, 229

 

                        232  x*y=0

                              Substitute, 212, 231

 

                 LHS

 

                        233  (x*y)^z=0

                              Substitute, 232, 211

 

                        234  x^z=0

                              Substitute, 212, 211

 

                 Apply axiom

 

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

                              U Spec, 12

 

                        236  y e n & z e n => [~[y=0 & z=0] => y^z e n]

                              U Spec, 235

 

                        237  y e n & z e n

                              Join, 204, 205

 

                        238  ~[y=0 & z=0] => y^z e n

                              Detach, 236, 237

 

                              239  y=0 & z=0

                                    Premise

 

                              240  y=0

                                    Split, 239

 

                              241  z=0

                                    Split, 239

 

                              242  y=0 & ~y=0

                                    Join, 240, 227

 

                        243  ~[y=0 & z=0]

                              4 Conclusion, 239

 

                        244  y^z e n

                              Detach, 238, 243

 

                        245  y^z e n => y^z*0=0 & 0*y^z=0

                              U Spec, 6, 244

 

                        246  y^z*0=0 & 0*y^z=0

                              Detach, 245, 244

 

                        247  y^z*0=0

                              Split, 246

 

                        248  0*y^z=0

                              Split, 246

 

                 RHS

 

                        249  x^z*y^z=0

                              Substitute, 234, 248

 

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

                              Substitute, 249, 233

 

             Sub-case 2

            

             As Required:

 

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

                        4 Conclusion, 227

 

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

                        Join, 226, 251

 

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

                        Cases, 207, 252

 

         Case 1

        

         As Required:

 

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

                  4 Conclusion, 212

 

             Case 2

            

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

            

             Suppose...

 

                  255  ~x=0

                        Premise

 

                 Sub-case 1

                

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

                

                 Suppose...

 

                        256  y=0

                              Premise

 

                 Apply axiom

 

                        257  x e n => x*0=0 & 0*x=0

                              U Spec, 6

 

                        258  x*0=0 & 0*x=0

                              Detach, 257, 203

 

                        259  x*0=0

                              Split, 258

 

                        260  0*x=0

                              Split, 258

 

                        261  x*y=0

                              Substitute, 256, 259

 

                 LHS

 

                        262  (x*y)^z=0

                              Substitute, 261, 211

 

                        263  y^z=0

                              Substitute, 256, 211

 

                 Apply axiom

 

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

                              U Spec, 12

 

                        265  x e n & z e n => [~[x=0 & z=0] => x^z e n]

                              U Spec, 264

 

                        266  x e n & z e n

                              Join, 203, 205

 

                        267  ~[x=0 & z=0] => x^z e n

                              Detach, 265, 266

 

                              268  x=0 & z=0

                                    Premise

 

                              269  x=0

                                    Split, 268

 

                              270  z=0

                                    Split, 268

 

                              271  x=0 & ~x=0

                                    Join, 269, 255

 

                        272  ~[x=0 & z=0]

                              4 Conclusion, 268

 

                        273  x^z e n

                              Detach, 267, 272

 

                 Apply axiom

 

                        274  x^z e n => x^z*0=0 & 0*x^z=0

                              U Spec, 6, 273

 

                        275  x^z*0=0 & 0*x^z=0

                              Detach, 274, 273

 

                        276  x^z*0=0

                              Split, 275

 

                        277  0*x^z=0

                              Split, 275

 

                 RHS

 

                        278  x^z*y^z=0

                              Substitute, 263, 276

 

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

                              Substitute, 278, 262

 

             Sub-case 1

            

             As Required:

 

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

                        4 Conclusion, 256

 

                 Sub-case 2

 

                        281  ~y=0

                              Premise

 

                 Apply previous result

 

                        282  ALL(b):[x e n & b e n

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

                              U Spec, 201

 

                        283  x e n & y e n

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

                              U Spec, 282

 

                        284  x e n & y e n

                              Join, 203, 204

 

                        285  ~x=0 & ~y=0 => ALL(c):[c e n => (x*y)^c=x^c*y^c]

                              Detach, 283, 284

 

                        286  ~x=0 & ~y=0

                              Join, 255, 281

 

                        287  ALL(c):[c e n => (x*y)^c=x^c*y^c]

                              Detach, 285, 286

 

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

                              U Spec, 287

 

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

                              Detach, 288, 205

 

             Sub-case 2

            

             As Required:

 

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

                        4 Conclusion, 281

 

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

                        Join, 280, 290

 

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

                        Cases, 207, 291

 

         Case 2

        

         As Required:

 

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

                  4 Conclusion, 255

 

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

                  Join, 254, 293

 

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

                  Cases, 206, 294

 

    As Required:

 

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

            4 Conclusion, 208

 

As Required:

 

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

      4 Conclusion, 202

 

   

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

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

   

    Suppose...

 

      298  x e n & y e n & z e n

            Premise

 

      299  x e n

            Split, 298

 

      300  y e n

            Split, 298

 

      301  z e n

            Split, 298

 

        

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

        

         Two cases to consider:

 

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

                  Premise

 

         Apply previous result

 

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

                  U Spec, 297

 

            304  ALL(c):[x e n & y e n & c e n => [~c=0 => (x*y)^c=x^c*y^c]]

                  U Spec, 303

 

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

                  U Spec, 304

 

         Case 1

        

         As Required:

 

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

                  Detach, 305, 298

 

            

             Case 2

            

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

            

             Suppose...

 

                  307  ~x=0 & ~y=0

                        Premise

 

             Apply previous result

 

                  308  ALL(b):[x e n & b e n

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

                        U Spec, 201

 

                  309  x e n & y e n

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

                        U Spec, 308

 

                  310  x e n & y e n

                        Join, 299, 300

 

                  311  ~x=0 & ~y=0 => ALL(c):[c e n => (x*y)^c=x^c*y^c]

                        Detach, 309, 310

 

                  312  ALL(c):[c e n => (x*y)^c=x^c*y^c]

                        Detach, 311, 307

 

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

                        U Spec, 312

 

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

                        Detach, 313, 301

 

         Case 2

        

         As Required:

 

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

                  4 Conclusion, 307

 

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

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

                  Join, 306, 315

 

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

                  Cases, 302, 316

 

    As Required:

 

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

            4 Conclusion, 302

 

 

As Required:

 

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

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

      4 Conclusion, 298