THEOREM 4

*********

 

The Product of Powers Rule: x^y * x^z = x^(y+z+)

 

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

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

 

By Dan Christensen

October 2013

 

(This proof was written with the aid the author's DC Proof software available 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

 

Associativity of +

 

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

      Axiom

 

Associativity of *

 

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

      Axiom

 

Commutativity of *

 

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

      Axiom

 

Right cancelability of +

 

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

      Axiom

 

0 has no predecessor

 

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

      Axiom

 

Existence of a predecessor

 

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

      Axiom

 

 

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

*********

 

16    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

 

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

      Split, 16

 

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

      Split, 16

 

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

      Split, 16

 

    

     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...

 

      20    x e n & y e n

            Premise

 

      21    x e n

            Split, 20

 

      22    y e n

            Split, 20

 

         

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

         

          Suppose...

 

            23    ~x=0

                  Premise

 

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

                  Subset, 1

 

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

                  E Spec, 24

 

          Define: p

 

            26    Set(p)

                  Split, 25

 

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

                  Split, 25

 

            28    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...

 

                  29    t e p

                        Premise

 

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

                        U Spec, 27

 

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

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

                        Iff-And, 30

 

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

                        Split, 31

 

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

                        Split, 31

 

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

                        Detach, 32, 29

 

                  35    t e n

                        Split, 34

 

          As Required:

 

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

                  4 Conclusion, 29

 

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

                  Join, 26, 36

 

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

 

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

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

                  Detach, 28, 37

 

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

                  U Spec, 27

 

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

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

                  Iff-And, 39

 

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

                  Split, 40

 

          Sufficient: 0 e p

 

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

                  Split, 40

 

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

                  Reflex

 

            44    y e n => y+0=y

                  U Spec, 6

 

            45    y+0=y

                  Detach, 44, 22

 

          LHS

 

            46    x^(y+0)=x^y

                  Substitute, 45, 43

 

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

                  Reflex

 

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

                  U Spec, 18

 

            49    ~x=0 => x^0=1

                  Detach, 48, 21

 

            50    x^0=1

                  Detach, 49, 23

 

            51    x^y*x^0=x^y*1

                  Substitute, 50, 47

 

            52    x^y e n => x^y*1=x^y

                  U Spec, 8

 

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

                  U Spec, 17

 

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

                  U Spec, 53

 

            55    x^y e n

                  Detach, 54, 20

 

            56    x^y*1=x^y

                  Detach, 52, 55

 

          RHS

 

            57    x^y*x^0=x^y

                  Substitute, 56, 51

 

            58    x^(y+0)=x^y*x^0

                  Substitute, 57, 46

 

            59    0 e n & x^(y+0)=x^y*x^0

                  Join, 4, 58

 

          As Required:

 

            60    0 e p

                  Detach, 42, 59

 

             

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

             

              Suppose...

 

                  61    t e p

                        Premise

 

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

                        U Spec, 27

 

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

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

                        Iff-And, 62

 

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

                        Split, 63

 

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

                        Split, 63

 

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

                        Detach, 64, 61

 

                  67    t e n

                        Split, 66

 

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

                        Split, 66

 

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

                        U Spec, 27

 

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

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

                        Iff-And, 69

 

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

                        Split, 70

 

              Sufficient: t+1 e p

 

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

                        Split, 70

 

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

                        U Spec, 2

 

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

                        U Spec, 73

 

                  75    t e n & 1 e n

                        Join, 67, 5

 

                  76    t+1 e n

                        Detach, 74, 75

 

                  77    x^(y+(t+1))=x^(y+(t+1))

                        Reflex

 

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

                        U Spec, 10

 

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

                        U Spec, 78

 

                  80    y e n & t e n & 1 e n => y+t+1=y+(t+1)

                        U Spec, 79

 

                  81    y e n & t e n

                        Join, 22, 67

 

                  82    y e n & t e n & 1 e n

                        Join, 81, 5

 

                  83    y+t+1=y+(t+1)

                        Detach, 80, 82

 

                  84    x^(y+(t+1))=x^(y+t+1)

                        Substitute, 83, 77

 

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

                        U Spec, 19

 

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

                        U Spec, 85

 

                  87    ALL(b):[y e n & b e n => y+b e n]

                        U Spec, 2

 

                  88    y e n & t e n => y+t e n

                        U Spec, 87

 

                  89    y e n & t e n

                        Join, 22, 67

 

                  90    y+t e n

                        Detach, 88, 89

 

                  91    x e n & y+t e n

                        Join, 21, 90

 

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

                        Detach, 86, 91

 

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

                        Substitute, 92, 84

 

              LHS

 

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

                        Substitute, 68, 93

 

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

                        Reflex

 

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

                        U Spec, 19

 

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

                        U Spec, 96

 

                  98    x e n & t e n

                        Join, 21, 67

 

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

                        Detach, 97, 98

 

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

                        Substitute, 99, 95

 

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

                        U Spec, 11

 

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

                        U Spec, 101

 

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

                        U Spec, 102

 

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

                        U Spec, 17

 

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

                        U Spec, 104

 

                  106  x^y e n

                        Detach, 105, 20

 

                  107  x e n & t e n => x^t e n

                        U Spec, 104

 

                  108  x e n & t e n

                        Join, 21, 67

 

                  109  x^t e n

                        Detach, 107, 108

 

                  110  x^y e n & x^t e n

                        Join, 106, 109

 

                  111  x^y e n & x^t e n & x e n

                        Join, 110, 21

 

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

                        Detach, 103, 111

 

              RHS

 

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

                        Substitute, 112, 100

 

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

                        Substitute, 113, 94

 

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

                        Join, 76, 114

 

                  116  t+1 e p

                        Detach, 72, 115

 

          As Required:

 

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

                  4 Conclusion, 61

 

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

                  Join, 60, 117

 

          As Required:

 

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

                  Detach, 38, 118

 

             

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

             

              Suppose...

 

                  120  t e n

                        Premise

 

                  121  t e n => t e p

                        U Spec, 119

 

                  122  t e p

                        Detach, 121, 120

 

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

                        U Spec, 27

 

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

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

                        Iff-And, 123

 

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

                        Split, 124

 

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

                        Split, 124

 

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

                        Detach, 125, 122

 

                  128  t e n

                        Split, 127

 

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

                        Split, 127

 

          As Required:

 

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

                  4 Conclusion, 120

 

     As Required:

 

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

            4 Conclusion, 23

 

As Required:

 

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

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

      4 Conclusion, 20

 

    

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

    

     Suppose...

 

      133  x e n & y e n & z e n

            Premise

 

      134  x e n

            Split, 133

 

      135  y e n

            Split, 133

 

      136  z e n

            Split, 133

 

         

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

         

          Suppose...

 

            137  ~x=0

                  Premise

 

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

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

                  U Spec, 132

 

            139  x e n & y e n

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

                  U Spec, 138

 

            140  x e n & y e n

                  Join, 134, 135

 

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

                  Detach, 139, 140

 

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

                  Detach, 141, 137

 

            143  z e n => x^(y+z)=x^y*x^z

                  U Spec, 142

 

            144  x^(y+z)=x^y*x^z

                  Detach, 143, 136

 

     As Required:

 

      145  ~x=0 => x^(y+z)=x^y*x^z

            4 Conclusion, 137

 

As Required:

 

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

      4 Conclusion, 133

 

As Required:

 

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

      Sym, 146