THEOREM 5

*********

 

The Power of a Power Rule  (x^y^z =x^(y*z)

 

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

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

 

Note: In DC Proof, the order of precedence is such that x^y^z=(x^y)^z

 

By Dan Christensen

October 2013

 

(This proof was written with the aid of the author's DC Proof software available at http://www.dcproof.com )

 

 

BASIC PRINCIPLES OF ARITHMETIC USED

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

 

n is a set (the set of natural numbers)

 

1     Set(n)

      Axiom

 

+ is a binary function on n

 

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

      Axiom

 

* is a binary function on n

 

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

      Axiom

 

4     0 e n

      Axiom

 

5     1 e n

      Axiom

 

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

      Axiom

 

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

      Axiom

 

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

      Axiom

 

The principle of mathematical induction (PMI)

 

9     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

 

Distributivity of * 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 Powers Rule  (previous result)

 

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

      Axiom

 

Power of a non-zero base  (previous result)

 

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

      Axiom

 

 

Define: ^  (0^0 is an uspecified natural number)

*********

 

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

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

     & ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]

      Premise

 

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

      Split, 13

 

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

      Split, 13

 

16    ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]

      Split, 13

 

    

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

            => [~a=0 => ALL(c):[c e n => a^(b*c)=a^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 => ALL(c):[c e n => x^(y*c)=x^y^c]

         

          Suppose...

 

            20    ~x=0

                  Premise

 

          Apply Subset Axiom (to do proof by induction)

 

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

                  Subset, 1

 

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

                  E Spec, 21

 

         

          Define: p

 

            23    Set(p)

                  Split, 22

 

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

                  Split, 22

 

          Apply PMI

 

            25    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, 9

 

             

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

             

              Suppose...

 

                  26    t e p

                        Premise

 

              Apply definition of p

 

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

                        U Spec, 24

 

                  28    [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, 27

 

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

                        Split, 28

 

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

                        Split, 28

 

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

                        Detach, 29, 26

 

                  32    t e n

                        Split, 31

 

          As Required:

 

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

                  4 Conclusion, 26

 

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

                  Join, 23, 33

 

         

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

 

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

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

                  Detach, 25, 34

 

          Prove: 0 e p

         

          Apply definition of p

 

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

                  U Spec, 24

 

            37    [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, 36

 

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

                  Split, 37

 

          Sufficient: 0 e p

 

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

                  Split, 37

 

          Prove: x^(y*0)=1

 

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

                  Reflex

 

            41    y e n => y*0=0

                  U Spec, 7

 

            42    y*0=0

                  Detach, 41, 19

 

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

                  Substitute, 42, 40

 

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

                  U Spec, 15

 

            45    ~x=0 => x^0=1

                  Detach, 44, 18

 

            46    x^0=1

                  Detach, 45, 20

 

          LHS

         

          As Required:

 

            47    x^(y*0)=1

                  Substitute, 46, 43

 

            48    x^y^0=x^y^0

                  Reflex

 

          Apply previous result

 

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

                  U Spec, 12

 

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

                  U Spec, 49

 

            51    ~x=0 => ~x^y=0

                  Detach, 50, 17

 

            52    ~x^y=0

                  Detach, 51, 20

 

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

                  U Spec, 15

 

          Apply definition of ^

 

            54    ALL(b):[x e n & b e n => x^b e n]

                  U Spec, 14

 

            55    x e n & y e n => x^y e n

                  U Spec, 54

 

            56    x^y e n

                  Detach, 55, 17

 

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

                  Detach, 53, 56

 

          RHS

         

          As Required:

 

            58    x^y^0=1

                  Detach, 57, 52

 

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

                  Substitute, 58, 47

 

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

                  Join, 4, 59

 

          As Required:

 

            61    0 e p

                  Detach, 39, 60

 

             

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

             

              Suppose...

 

                  62    t e p

                        Premise

 

              Apply definition of p

 

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

                        U Spec, 24

 

                  64    [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, 63

 

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

                        Split, 64

 

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

                        Split, 64

 

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

                        Detach, 65, 62

 

                  68    t e n

                        Split, 67

 

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

                        Split, 67

 

              Apply definition of p

 

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

                        U Spec, 24

 

                  71    [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, 70

 

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

                        Split, 71

 

              Sufficient: t+1 e p

 

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

                        Split, 71

 

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

                        U Spec, 2

 

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

                        U Spec, 74

 

                  76    t e n & 1 e n

                        Join, 68, 5

 

                  77    t+1 e n

                        Detach, 75, 76

 

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

                        Reflex

 

              Apply distributitivity

 

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

                        U Spec, 10

 

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

                        U Spec, 79

 

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

                        U Spec, 80

 

                  82    y e n & t e n

                        Join, 19, 68

 

                  83    y e n & t e n & 1 e n

                        Join, 82, 5

 

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

                        Detach, 81, 83

 

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

                        Substitute, 84, 78

 

                  86    y e n => y*1=y

                        U Spec, 8

 

                  87    y*1=y

                        Detach, 86, 19

 

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

                        Substitute, 87, 85

 

              Apply previous result

 

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

                        U Spec, 11

 

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

                        U Spec, 89

 

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

                        U Spec, 90

 

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

                        U Spec, 3

 

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

                        U Spec, 92

 

                  94    y e n & t e n

                        Join, 19, 68

 

                  95    y*t e n

                        Detach, 93, 94

 

                  96    x e n & y*t e n

                        Join, 18, 95

 

                  97    x e n & y*t e n & y e n

                        Join, 96, 19

 

                  98    ~x=0 => x^(y*t+y)=x^(y*t)*x^y

                        Detach, 91, 97

 

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

                        Detach, 98, 20

 

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

                        Substitute, 99, 88

 

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

                        Substitute, 69, 100

 

              Apply definition of ^

 

                  102  ALL(b):[x^y e n & b e n => x^y^(b+1)=x^y^b*x^y]

                        U Spec, 16

 

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

                        U Spec, 102

 

                  104  ALL(b):[x e n & b e n => x^b e n]

                        U Spec, 14

 

                  105  x e n & y e n => x^y e n

                        U Spec, 104

 

                  106  x^y e n

                        Detach, 105, 17

 

                  107  x^y e n & t e n

                        Join, 106, 68

 

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

                        Detach, 103, 107

 

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

                        Substitute, 108, 101

 

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

                        Join, 77, 109

 

                  111  t+1 e p

                        Detach, 73, 110

 

          As Required:

 

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

                  4 Conclusion, 62

 

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

                  Join, 61, 112

 

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

                  Detach, 35, 113

 

             

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

             

              Suppose...

 

                  115  t e n

                        Premise

 

                  116  t e n => t e p

                        U Spec, 114

 

                  117  t e p

                        Detach, 116, 115

 

              Apply definition of p

 

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

                        U Spec, 24

 

                  119  [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, 118

 

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

                        Split, 119

 

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

                        Split, 119

 

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

                        Detach, 120, 117

 

                  123  t e n

                        Split, 122

 

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

                        Split, 122

 

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

                        Sym, 124

 

          As Required:

 

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

                  4 Conclusion, 115

 

     As Required:

 

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

            4 Conclusion, 20

 

As Required:

 

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

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

      4 Conclusion, 17

 

    

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

    

     Suppose...

 

      129  x e n & y e n & z e n

            Premise

 

      130  x e n

            Split, 129

 

      131  y e n

            Split, 129

 

      132  z e n

            Split, 129

 

      133  x e n & y e n

            Join, 130, 131

 

         

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

         

          Suppose...

 

            134  ~x=0

                  Premise

 

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

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

                  U Spec, 128

 

            136  x e n & y e n

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

                  U Spec, 135

 

            137  x e n & y e n

                  Join, 130, 131

 

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

                  Detach, 136, 137

 

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

                  Detach, 138, 134

 

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

                  U Spec, 139

 

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

                  Detach, 140, 132

 

     As Required:

 

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

            4 Conclusion, 134

 

As Required:

 

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

      4 Conclusion, 129