THEOREM 7

*********

 

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

 

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

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

  

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

 

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

 

Distributivity of * over +

 

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

      Axiom

 

Associativity of *

 

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

      Axiom

 

Commutativity of *

 

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

      Axiom

 

Right cancelability of +

 

14    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

 

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

      Axiom

 

Existence of a predecessor

 

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

      Axiom

 

Zero Product Rule

 

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

      Axiom

 

Product of Powers Rule  (previous result)

 

18    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)

 

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

      Axiom

 

 

Define: ^  (0^0 is unspecified)

*********

 

20    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

 

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

      Split, 20

 

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

      Split, 20

 

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

      Split, 20

 

    

     Prove: ALL(a):ALL(b):[aen & ben => [~a=0 & ~b=0 => ALL(c):[cen => (a*b)^c=a^c*b^c]]]

    

     Suppose...

 

      24    x e n & y e n

            Premise

 

      25    x e n

            Split, 24

 

      26    y e n

            Split, 24

 

         

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

         

          Suppose...

 

            27    ~x=0 & ~y=0

                  Premise

 

            28    ~x=0

                  Split, 27

 

            29    ~y=0

                  Split, 27

 

          Apply Subset Axiom to construct subset p of n

 

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

                  Subset, 1

 

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

                  E Spec, 30

 

         

          Define: p

 

            32    Set(p)

                  Split, 31

 

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

                  Split, 31

 

          Apply PBI

 

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

 

                  35    t e p

                        Premise

 

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

                        U Spec, 33

 

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

 

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

                        Split, 37

 

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

                        Split, 37

 

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

                        Detach, 38, 35

 

                  41    t e n

                        Split, 40

 

          As Required:

 

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

                  4 Conclusion, 35

 

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

                  Join, 32, 42

 

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

 

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

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

                  Detach, 34, 43

 

          Prove: 0ep

         

          Apply definition of p

 

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

                  U Spec, 33

 

            46    [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, 45

 

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

                  Split, 46

 

          Sufficient: 0 e p

 

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

                  Split, 46

 

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

                  Reflex

 

          Apply Zero Product Rule

 

            50    ALL(b):[x e n & b e n => [x*b=0 => x=0 | b=0]]

                  U Spec, 17

 

            51    x e n & y e n => [x*y=0 => x=0 | y=0]

                  U Spec, 50

 

            52    x*y=0 => x=0 | y=0

                  Detach, 51, 24

 

            53    ~[x=0 | y=0] => ~x*y=0

                  Contra, 52

 

            54    ~~[~x=0 & ~y=0] => ~x*y=0

                  DeMorgan, 53

 

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

                  Rem DNeg, 54

 

            56    ~x*y=0

                  Detach, 55, 27

 

          Apply definition of ^

 

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

                  U Spec, 22

 

          Apply definition of *

 

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

                  U Spec, 3

 

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

                  U Spec, 58

 

            60    x*y e n

                  Detach, 59, 24

 

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

                  Detach, 57, 60

 

            62    (x*y)^0=1

                  Detach, 61, 56

 

          LHS

 

            63    (x*y)^0=1

                  Substitute, 62, 49

 

            64    x^0*y^0=x^0*y^0

                  Reflex

 

          Apply definition of ^

 

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

                  U Spec, 22

 

            66    ~x=0 => x^0=1

                  Detach, 65, 25

 

            67    x^0=1

                  Detach, 66, 28

 

          Apply definition of ^

 

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

                  U Spec, 22

 

            69    ~y=0 => y^0=1

                  Detach, 68, 26

 

            70    y^0=1

                  Detach, 69, 29

 

            71    x^0*y^0=1*y^0

                  Substitute, 67, 64

 

            72    x^0*y^0=1*1

                  Substitute, 70, 71

 

          Apply property of *

 

            73    1 e n => 1*1=1

                  U Spec, 8

 

            74    1*1=1

                  Detach, 73, 5

 

          RHS

 

            75    x^0*y^0=1

                  Substitute, 74, 72

 

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

                  Substitute, 75, 63

 

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

                  Join, 4, 76

 

          As Required:

 

            78    0 e p

                  Detach, 48, 77

 

             

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

             

              Suppose...

 

                  79    t e p

                        Premise

 

              Apply definition of p

 

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

                        U Spec, 33

 

                  81    [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, 80

 

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

                        Split, 81

 

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

                        Split, 81

 

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

                        Detach, 82, 79

 

                  85    t e n

                        Split, 84

 

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

                        Split, 84

 

              Apply definition of p

 

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

                        U Spec, 33

 

                  88    [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, 87

 

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

                        Split, 88

 

              Sufficient: t+1 e p

 

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

                        Split, 88

 

              Apply definition of +

 

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

                        U Spec, 2

 

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

                        U Spec, 91

 

                  93    t e n & 1 e n

                        Join, 85, 5

 

                  94    t+1 e n

                        Detach, 92, 93

 

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

                        Reflex

 

              Apply definition of ^

 

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

                        U Spec, 23

 

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

                        U Spec, 96

 

                  98    x*y e n & t e n

                        Join, 60, 85

 

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

                        Detach, 97, 98

 

              LHS

 

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

                        Substitute, 86, 99

 

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

                        Reflex

 

              Apply definition of ^

 

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

                        U Spec, 23

 

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

                        U Spec, 102

 

                  104  x e n & t e n

                        Join, 25, 85

 

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

                        Detach, 103, 104

 

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

                        Substitute, 105, 101

 

              Apply definition of ^

 

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

                        U Spec, 23

 

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

                        U Spec, 107

 

                  109  y e n & t e n

                        Join, 26, 85

 

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

                        Detach, 108, 109

 

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

                        Substitute, 110, 106

 

              Apply commutativity of *

 

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

                        U Spec, 13

 

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

                        U Spec, 112

 

              Apply definition of ^

 

                  114  ALL(b):[y e n & b e n => y^b e n]

                        U Spec, 21

 

                  115  y e n & t e n => y^t e n

                        U Spec, 114

 

                  116  y e n & t e n

                        Join, 26, 85

 

                  117  y^t e n

                        Detach, 115, 116

 

                  118  y^t e n & y e n

                        Join, 117, 26

 

                  119  y^t*y=y*y^t

                        Detach, 113, 118

 

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

                        Substitute, 119, 111

 

              Apply associativity of *

 

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

                        U Spec, 12

 

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

                        U Spec, 121

 

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

                        U Spec, 122

 

              Apply definition of ^

 

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

                        U Spec, 21

 

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

                        U Spec, 124

 

                  126  x e n & t e n

                        Join, 25, 85

 

                  127  x^t e n

                        Detach, 125, 126

 

              Apply definition of ^

 

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

                        U Spec, 3

 

                  129  x^t e n & x e n => x^t*x e n

                        U Spec, 128

 

                  130  x^t e n & x e n

                        Join, 127, 25

 

                  131  x^t*x e n

                        Detach, 129, 130

 

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

                        Join, 131, 26

 

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

                        Join, 132, 117

 

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

                        Detach, 123, 133

 

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

                        Substitute, 134, 120

 

              Apply associativity of *

 

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

                        U Spec, 12

 

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

                        U Spec, 136

 

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

                        U Spec, 137

 

                  139  x^t e n & x e n

                        Join, 127, 25

 

                  140  x^t e n & x e n & y e n

                        Join, 139, 26

 

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

                        Detach, 138, 140

 

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

                        Substitute, 141, 135

 

              Apply associativity of *

 

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

                        U Spec, 12

 

                  144  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, 143

 

                  145  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, 144

 

              Apply definition of *

 

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

                        U Spec, 3

 

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

                        U Spec, 146

 

                  148  x*y e n

                        Detach, 147, 24

 

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

                        Join, 127, 148

 

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

                        Join, 149, 117

 

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

                        Detach, 145, 150

 

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

                        Substitute, 151, 142

 

              Apply associativity of *

 

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

                        U Spec, 13

 

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

                        U Spec, 153

 

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

                        Join, 148, 117

 

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

                        Detach, 154, 155

 

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

                        Substitute, 156, 152

 

              Apply associativity of *

 

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

                        U Spec, 12

 

                  159  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, 158

 

                  160  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, 159

 

                  161  x^t e n & y^t e n

                        Join, 127, 117

 

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

                        Join, 161, 148

 

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

                        Detach, 160, 162

 

              RHS

 

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

                        Substitute, 163, 157

 

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

                        Substitute, 164, 100

 

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

                        Join, 94, 165

 

                  167  t+1 e p

                        Detach, 90, 166

 

          As Required:

 

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

                  4 Conclusion, 79

 

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

                  Join, 78, 168

 

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

                  Detach, 44, 169

 

             

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

             

              Suppose...

 

                  171  t e n

                        Premise

 

                  172  t e n => t e p

                        U Spec, 170

 

                  173  t e p

                        Detach, 172, 171

 

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

                        U Spec, 33

 

                  175  [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, 174

 

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

                        Split, 175

 

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

                        Split, 175

 

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

                        Detach, 176, 173

 

                  179  t e n

                        Split, 178

 

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

                        Split, 178

 

          As Required:

 

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

                  4 Conclusion, 171

 

     As Required:

 

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

            4 Conclusion, 27

 

As Required:

 

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

 

    

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

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

    

     Suppose...

 

      184  x e n & y e n & z e n

            Premise

 

      185  x e n

            Split, 184

 

      186  y e n

            Split, 184

 

      187  z e n

            Split, 184

 

         

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

         

          Suppose...

 

            188  ~x=0 & ~y=0

                  Premise

 

            189  ~x=0

                  Split, 188

 

            190  ~y=0

                  Split, 188

 

            191  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, 183

 

            192  x e n & y e n

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

                  U Spec, 191

 

            193  x e n & y e n

                  Join, 185, 186

 

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

                  Detach, 192, 193

 

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

                  Detach, 194, 188

 

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

                  U Spec, 195

 

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

                  Detach, 196, 187

 

     As Required:

 

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

            4 Conclusion, 188

 

As Required:

 

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

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

      4 Conclusion, 184