THEOREM

*******

 

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

 

ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n & ~a=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 software available at http://www.dcproof.com

 

 

AXIOMS / DEFINITIONS USED

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

 

Define: ^  (partial function on n)

 

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

      Axiom

 

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

      Axiom

 

3     0^1=0

      Axiom

 

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

      Axiom

 

n is a set (the set of natural numbers)

 

5     Set(n)

      Axiom

 

6     0 e n

      Axiom

 

Define: +

 

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

      Axiom

 

Define: *

 

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

      Axiom

 

Define: 1

 

9     1 e n

      Axiom

 

Multiplying by 0

 

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

      Axiom

 

Multiplying by 1

 

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

      Axiom

 

* is distributive over +

 

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

      Axiom

 

The principle of mathematical induction (starting at 0)

 

13    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

 

PREVIOUS RESULTS

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

 

Powers of a non-zero base are non-zero              PROOF

 

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

      Axiom

 

Product of Powers Rule                              PROOF

 

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

      Axiom

 

    

     PROOF

     *****

    

     Prove: ALL(a):ALL(b):[a e n & b e n & ~a=0

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

    

     Suppose...

 

      16    x e n & y e n & ~x=0

            Premise

 

      17    x e n

            Split, 16

 

      18    y e n

            Split, 16

 

      19    ~x=0

            Split, 16

 

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

            Subset, 5

 

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

            E Spec, 20

 

     Define: p

 

      22    Set(p)

            Split, 21

 

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

            Split, 21

 

     Apply Principle of Mathmatical Induction

 

      24    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, 13

 

         

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

         

          Suppose...

 

            25    t e p

                  Premise

 

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

                  U Spec, 23

 

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

 

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

                  Split, 27

 

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

                  Split, 27

 

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

                  Detach, 28, 25

 

            31    t e n

                  Split, 30

 

     As Required:

 

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

            4 Conclusion, 25

 

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

            Join, 22, 32

 

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

 

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

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

            Detach, 24, 33

 

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

            U Spec, 23

 

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

 

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

            Split, 36

 

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

            Split, 36

 

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

            Reflex

 

      40    y e n => y*0=0

            U Spec, 10

 

      41    y*0=0

            Detach, 40, 18

 

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

            Substitute, 41, 39

 

      43    x e n & ~x=0 => x^0=1

            U Spec, 2

 

      44    x e n & ~x=0

            Join, 17, 19

 

      45    x^0=1

            Detach, 43, 44

 

      46    x^(y*0)=1

            Substitute, 45, 42

 

      47    x^y^0=x^y^0

            Reflex

 

      48    x^y e n & ~x^y=0 => x^y^0=1

            U Spec, 2

 

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

            U Spec, 1

 

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

            U Spec, 49

 

         

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

         

          Suppose to the contrary...

 

            51    x=0 & y=0

                  Premise

 

            52    x=0

                  Split, 51

 

            53    y=0

                  Split, 51

 

            54    x=0 & ~x=0

                  Join, 52, 19

 

     As Required:

 

      55    ~[x=0 & y=0]

            4 Conclusion, 51

 

      56    x e n & y e n

            Join, 17, 18

 

      57    x e n & y e n & ~[x=0 & y=0]

            Join, 56, 55

 

      58    x^y e n

            Detach, 50, 57

 

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

            U Spec, 14

 

      60    x e n & y e n & ~x=0 => ~x^y=0

            U Spec, 59

 

      61    ~x^y=0

            Detach, 60, 16

 

      62    x^y e n & ~x^y=0

            Join, 58, 61

 

      63    x^y^0=1

            Detach, 48, 62

 

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

            Substitute, 63, 46

 

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

            Join, 6, 64

 

     As Required:

 

      66    0 e p

            Detach, 38, 65

 

         

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

         

          Suppose...

 

            67    t e p

                  Premise

 

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

                  U Spec, 23

 

            69    [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, 68

 

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

                  Split, 69

 

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

                  Split, 69

 

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

                  Detach, 70, 67

 

            73    t e n

                  Split, 72

 

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

                  Split, 72

 

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

                  U Spec, 23

 

            76    [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, 75

 

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

                  Split, 76

 

          Sufficient: t+1 e p

 

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

                  Split, 76

 

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

                  U Spec, 7

 

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

                  U Spec, 79

 

            81    t e n & 1 e n

                  Join, 73, 9

 

            82    t+1 e n

                  Detach, 80, 81

 

            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, 4

 

            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 & ~~[~x^y=0 | ~t=0] => x^y^(t+1)=x^y^t*x^y

                  DeMorgan, 84

 

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

                  Rem DNeg, 85

 

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

                  U Spec, 1

 

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

                  U Spec, 87

 

             

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

             

              Suppose to the contrary...

 

                  89    x=0 & y=0

                        Premise

 

                  90    x=0

                        Split, 89

 

                  91    y=0

                        Split, 89

 

                  92    x=0 & ~x=0

                        Join, 90, 19

 

          As Required:

 

            93    ~[x=0 & y=0]

                  4 Conclusion, 89

 

            94    x e n & y e n

                  Join, 17, 18

 

            95    x e n & y e n & ~[x=0 & y=0]

                  Join, 94, 93

 

            96    x^y e n

                  Detach, 88, 95

 

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

                  U Spec, 14

 

            98    x e n & y e n & ~x=0 => ~x^y=0

                  U Spec, 97

 

            99    x e n & y e n

                  Join, 17, 18

 

            100  x e n & y e n & ~x=0

                  Join, 99, 19

 

            101  ~x^y=0

                  Detach, 98, 100

 

            102  ~x^y=0 | ~t=0

                  Arb Or, 101

 

            103  x^y e n & t e n

                  Join, 96, 73

 

            104  x^y e n & t e n & [~x^y=0 | ~t=0]

                  Join, 103, 102

 

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

                  Detach, 86, 104

 

          RHS

 

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

                  Substitute, 74, 105

 

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

                  Reflex

 

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

                  U Spec, 12

 

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

                  U Spec, 108

 

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

                  U Spec, 109

 

            111  y e n & t e n

                  Join, 18, 73

 

            112  y e n & t e n & 1 e n

                  Join, 111, 9

 

            113  y e n & t e n & 1 e n

                  Join, 111, 9

 

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

                  Detach, 110, 113

 

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

                  Substitute, 114, 107

 

            116  y e n => y*1=y

                  U Spec, 11

 

            117  y*1=y

                  Detach, 116, 18

 

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

                  Substitute, 117, 115

 

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

                  U Spec, 15

 

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

                  U Spec, 119

 

            121  x e n & y*t e n & y e n & ~x=0 => x^(y*t)*x^y=x^(y*t+y)

                  U Spec, 120

 

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

                  U Spec, 8

 

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

                  U Spec, 122

 

            124  y e n & t e n

                  Join, 18, 73

 

            125  y*t e n

                  Detach, 123, 124

 

            126  x e n & y*t e n

                  Join, 17, 125

 

            127  x e n & y*t e n & y e n

                  Join, 126, 18

 

            128  x e n & y*t e n & y e n & ~x=0

                  Join, 127, 19

 

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

                  Detach, 121, 128

 

          LHS

 

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

                  Substitute, 129, 118

 

          LHS=RHS

 

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

                  Substitute, 106, 130

 

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

                  Join, 82, 131

 

            133  t+1 e p

                  Detach, 78, 132

 

     As Required:

 

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

            4 Conclusion, 67

 

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

            Join, 66, 134

 

     As Required:

 

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

            Detach, 34, 135

 

         

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

         

          Suppose...

 

            137  t e n

                  Premise

 

            138  t e n => t e p

                  U Spec, 136

 

            139  t e p

                  Detach, 138, 137

 

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

                  U Spec, 23

 

            141  [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, 140

 

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

                  Split, 141

 

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

                  Split, 141

 

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

                  Detach, 142, 139

 

            145  t e n

                  Split, 144

 

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

                  Split, 144

 

     As Required:

 

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

            4 Conclusion, 137

 

As Required:

 

148  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, 16

 

      149  x e n & y e n & z e n & ~x=0

            Premise

 

      150  x e n

            Split, 149

 

      151  y e n

            Split, 149

 

      152  z e n

            Split, 149

 

      153  ~x=0

            Split, 149

 

      154  ALL(b):[x e n & b e n & ~x=0

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

            U Spec, 148

 

      155  x e n & y e n & ~x=0

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

            U Spec, 154

 

      156  x e n & y e n

            Join, 150, 151

 

      157  x e n & y e n & ~x=0

            Join, 156, 153

 

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

            Detach, 155, 157

 

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

            U Spec, 158

 

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

            Detach, 159, 152

 

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

            Sym, 160

 

As Required:

 

162  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, 149