THEOREM

*******

 

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

 

 

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

 

 

BASIC PROPERTIES OF ARITHMETIC USED

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

 

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

 

0 is additive identity element

 

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

      Axiom

 

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

      Axiom

 

1 is the multiplicative identity element

 

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

      Axiom

 

The principle of mathematical induction (starting at 0)

 

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

 

Commutativity of +

 

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

      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

 

14    ALL(a):[a e n => [a=a*a => a=0 | a=1]]

      Axiom

 

 

Define: ^

*********

 

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

      Axiom

 

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

      Axiom

 

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

      Axiom

 

    

     PROOF

     *****

    

     '=>'

    

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

            => 0^0=0 | 0^0=1

    

     Suppose...

 

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

            Premise

 

     Apply premise

 

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

            U Spec, 18

 

      20    ALL(c):[0 e n & 0 e n & c e n => 0^0*0^c=0^(0+c)]

            U Spec, 19

 

      21    0 e n & 0 e n & 0 e n => 0^0*0^0=0^(0+0)

            U Spec, 20

 

      22    0 e n & 0 e n

            Join, 4, 4

 

      23    0 e n & 0 e n & 0 e n

            Join, 22, 4

 

      24    0^0*0^0=0^(0+0)

            Detach, 21, 23

 

      25    0 e n => 0+0=0

            U Spec, 6

 

      26    0+0=0

            Detach, 25, 4

 

      27    0^0*0^0=0^0

            Substitute, 26, 24

 

      28    0^0 e n => [0^0=0^0*0^0 => 0^0=0 | 0^0=1]

            U Spec, 14

 

      29    ALL(b):[0 e n & b e n => 0^b e n]

            U Spec, 15

 

      30    0 e n & 0 e n => 0^0 e n

            U Spec, 29

 

      31    0 e n & 0 e n

            Join, 4, 4

 

      32    0^0 e n

            Detach, 30, 31

 

      33    0^0=0^0*0^0 => 0^0=0 | 0^0=1

            Detach, 28, 32

 

      34    0^0=0^0*0^0

            Sym, 27

 

      35    0^0=0 | 0^0=1

            Detach, 33, 34

 

As Required:

 

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

     => 0^0=0 | 0^0=1

      4 Conclusion, 18

 

    

     '<='

    

     Prove: 0^0=0 | 0^0=1

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

    

     Suppose...

 

      37    0^0=0 | 0^0=1

            Premise

 

         

          Case 1

         

          Prove: f(0,0)=0

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

         

          Suppose...

 

            38    0^0=0

                  Premise

 

             

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

             

              Suppose...

 

                  39    x e n

                        Premise

 

              Construct subset of n for induction

             

              Apply Subset Axiom

 

                  40    EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & x^b*x^0=x^(b+0)]]

                        Subset, 1

 

                  41    Set(p1) & ALL(b):[b e p1 <=> b e n & x^b*x^0=x^(b+0)]

                        E Spec, 40

 

             

              Define: p1

              **********

 

                  42    Set(p1)

                        Split, 41

 

                  43    ALL(b):[b e p1 <=> b e n & x^b*x^0=x^(b+0)]

                        Split, 41

 

              Apply PMI for p1

 

                  44    Set(p1) & ALL(b):[b e p1 => b e n]

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

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

                        U Spec, 9

 

                  

                   Prove: p1 is a subset of n

                  

                   Suppose...

 

                        45    q e p1

                              Premise

 

                   Apply defintion of p1

 

                        46    q e p1 <=> q e n & x^q*x^0=x^(q+0)

                              U Spec, 43

 

                        47    [q e p1 => q e n & x^q*x^0=x^(q+0)]

                        & [q e n & x^q*x^0=x^(q+0) => q e p1]

                              Iff-And, 46

 

                        48    q e p1 => q e n & x^q*x^0=x^(q+0)

                              Split, 47

 

                        49    q e n & x^q*x^0=x^(q+0) => q e p1

                              Split, 47

 

                        50    q e n & x^q*x^0=x^(q+0)

                              Detach, 48, 45

 

                        51    q e n

                              Split, 50

 

              p1 is a subset of n

             

              As Required:

 

                  52    ALL(b):[b e p1 => b e n]

                        4 Conclusion, 45

 

                  53    Set(p1) & ALL(b):[b e p1 => b e n]

                        Join, 42, 52

 

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

 

                  54    0 e p1 & ALL(b):[b e p1 => b+1 e p1]

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

                        Detach, 44, 53

 

              Base case

             

              Prove: 0 e p1

             

              Apply definition of p1

 

                  55    0 e p1 <=> 0 e n & x^0*x^0=x^(0+0)

                        U Spec, 43

 

                  56    [0 e p1 => 0 e n & x^0*x^0=x^(0+0)]

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

                        Iff-And, 55

 

                  57    0 e p1 => 0 e n & x^0*x^0=x^(0+0)

                        Split, 56

 

              Sufficient: For 0 e p1

 

                  58    0 e n & x^0*x^0=x^(0+0) => 0 e p1

                        Split, 56

 

              Two cases:

 

                  59    x=0 | ~x=0

                        Or Not

 

                  

                   Case 1

                  

                   Prove: x=0 => 0 e p1

                  

                   Suppose...

 

                        60    x=0

                              Premise

 

                        61    x^0=0

                              Substitute, 60, 38

 

                        62    0 e n => 0+0=0

                              U Spec, 6

 

                        63    0+0=0

                              Detach, 62, 4

 

                        64    x^(0+0)=0

                              Substitute, 63, 61

 

                        65    0 e n => 0*0=0

                              U Spec, 7

 

                        66    0*0=0

                              Detach, 65, 4

 

                        67    x^0*x^0=0

                              Substitute, 61, 66

 

                        68    x^0*x^0=x^(0+0)

                              Substitute, 64, 67

 

                        69    0 e n & x^0*x^0=x^(0+0)

                              Join, 4, 68

 

                        70    0 e p1

                              Detach, 58, 69

 

              As Required:

 

                  71    x=0 => 0 e p1

                        4 Conclusion, 60

 

                  

                   Case 2

                  

                   Prove:

                  

                   Suppose...

 

                        72    ~x=0

                              Premise

 

                   Apply definiton of ^

 

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

                              U Spec, 16

 

                        74    ~x=0 => x^0=1

                              Detach, 73, 39

 

                        75    x^0=1

                              Detach, 74, 72

 

                        76    0 e n => 0+0=0

                              U Spec, 6

 

                        77    0+0=0

                              Detach, 76, 4

 

                        78    x^(0+0)=1

                              Substitute, 77, 75

 

                        79    1 e n => 1*1=1

                              U Spec, 8

 

                        80    1*1=1

                              Detach, 79, 5

 

                        81    x^0*x^0=1

                              Substitute, 75, 80

 

                        82    x^0*x^0=x^(0+0)

                              Substitute, 78, 81

 

                        83    0 e n & x^0*x^0=x^(0+0)

                              Join, 4, 82

 

                        84    0 e p1

                              Detach, 58, 83

 

              As Required:

 

                  85    ~x=0 => 0 e p1

                        4 Conclusion, 72

 

                  86    [x=0 => 0 e p1] & [~x=0 => 0 e p1]

                        Join, 71, 85

 

              As Required:

 

                  87    0 e p1

                        Cases, 59, 86

 

                  

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

                  

                   Suppose...

 

                        88    y e p1

                              Premise

 

                   Apply definition of p1

 

                        89    y e p1 <=> y e n & x^y*x^0=x^(y+0)

                              U Spec, 43

 

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

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

                              Iff-And, 89

 

                        91    y e p1 => y e n & x^y*x^0=x^(y+0)

                              Split, 90

 

                        92    y e n & x^y*x^0=x^(y+0) => y e p1

                              Split, 90

 

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

                              Detach, 91, 88

 

                        94    y e n

                              Split, 93

 

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

                              Split, 93

 

                   Apply definition of p1

 

                        96    y+1 e p1 <=> y+1 e n & x^(y+1)*x^0=x^(y+1+0)

                              U Spec, 43

 

                        97    [y+1 e p1 => y+1 e n & x^(y+1)*x^0=x^(y+1+0)]

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

                              Iff-And, 96

 

                        98    y+1 e p1 => y+1 e n & x^(y+1)*x^0=x^(y+1+0)

                              Split, 97

 

                   Sufficient: For y+1 e p1

 

                        99    y+1 e n & x^(y+1)*x^0=x^(y+1+0) => y+1 e p1

                              Split, 97

 

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

                              U Spec, 2

 

                        101  y e n & 1 e n => y+1 e n

                              U Spec, 100

 

                        102  y e n & 1 e n

                              Join, 94, 5

 

                        103  y+1 e n

                              Detach, 101, 102

 

                        104  x^(y+1)*x^0=x^(y+1)*x^0

                              Reflex

 

                   Apply definition of ^

 

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

                              U Spec, 17

 

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

                              U Spec, 105

 

                        107  x e n & y e n

                              Join, 39, 94

 

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

                              Detach, 106, 107

 

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

                              Substitute, 108, 104

 

                   Apply associativity of *

 

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

                              U Spec, 12

 

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

                              U Spec, 110

 

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

                              U Spec, 111

 

                   Apply definition of ^

 

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

                              U Spec, 15

 

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

                              U Spec, 113

 

                        115  x e n & y e n

                              Join, 39, 94

 

                        116  x^y e n

                              Detach, 114, 115

 

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

                              U Spec, 15

 

                        118  x e n & 0 e n => x^0 e n

                              U Spec, 117

 

                        119  x e n & 0 e n

                              Join, 39, 4

 

                        120  x^0 e n

                              Detach, 118, 119

 

                        121  x^y e n & x e n

                              Join, 116, 39

 

                        122  x^y e n & x e n & x^0 e n

                              Join, 121, 120

 

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

                              Detach, 112, 122

 

                        124  x^(y+1)*x^0=x^y*(x*x^0)

                              Substitute, 123, 109

 

                   Appy commutativity of *

 

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

                              U Spec, 13

 

                        126  x e n & x^0 e n => x*x^0=x^0*x

                              U Spec, 125

 

                        127  x e n & x^0 e n

                              Join, 39, 120

 

                        128  x*x^0=x^0*x

                              Detach, 126, 127

 

                        129  x^(y+1)*x^0=x^y*(x^0*x)

                              Substitute, 128, 124

 

                   Apply associativity of *

 

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

                              U Spec, 12

 

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

                              U Spec, 130

 

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

                              U Spec, 131

 

                        133  x^y e n & x^0 e n

                              Join, 116, 120

 

                        134  x^y e n & x^0 e n & x e n

                              Join, 133, 39

 

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

                              Detach, 132, 134

 

                        136  x^(y+1)*x^0=x^y*x^0*x

                              Substitute, 135, 129

 

                   LHS

 

                        137  x^(y+1)*x^0=x^(y+0)*x

                              Substitute, 95, 136

 

                        138  x^(y+1+0)=x^(y+1+0)

                              Reflex

 

                   Apply associativity of +

 

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

                              U Spec, 10

 

                        140  ALL(c):[y e n & 1 e n & c e n => y+1+c=y+(1+c)]

                              U Spec, 139

 

                        141  y e n & 1 e n & 0 e n => y+1+0=y+(1+0)

                              U Spec, 140

 

                        142  y e n & 1 e n

                              Join, 94, 5

 

                        143  y e n & 1 e n & 0 e n

                              Join, 142, 4

 

                        144  y+1+0=y+(1+0)

                              Detach, 141, 143

 

                        145  x^(y+1+0)=x^(y+(1+0))

                              Substitute, 144, 138

 

                   Apply commutativity of +

 

                        146  ALL(b):[1 e n & b e n => 1+b=b+1]

                              U Spec, 11

 

                        147  1 e n & 0 e n => 1+0=0+1

                              U Spec, 146

 

                        148  1 e n & 0 e n

                              Join, 5, 4

 

                        149  1+0=0+1

                              Detach, 147, 148

 

                        150  x^(y+1+0)=x^(y+(0+1))

                              Substitute, 149, 145

 

                   Apply associativity of +

 

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

                              U Spec, 10

 

                        152  ALL(c):[y e n & 0 e n & c e n => y+0+c=y+(0+c)]

                              U Spec, 151

 

                        153  y e n & 0 e n & 1 e n => y+0+1=y+(0+1)

                              U Spec, 152

 

                        154  y e n & 0 e n

                              Join, 94, 4

 

                        155  y e n & 0 e n & 1 e n

                              Join, 154, 5

 

                        156  y+0+1=y+(0+1)

                              Detach, 153, 155

 

                        157  x^(y+1+0)=x^(y+0+1)

                              Substitute, 156, 150

 

                   Apply definition of ^

 

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

                              U Spec, 17

 

                        159  x e n & y+0 e n => x^(y+0+1)=x^(y+0)*x

                              U Spec, 158

 

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

                              U Spec, 2

 

                        161  y e n & 0 e n => y+0 e n

                              U Spec, 160

 

                        162  y e n & 0 e n

                              Join, 94, 4

 

                        163  y+0 e n

                              Detach, 161, 162

 

                        164  x e n & y+0 e n

                              Join, 39, 163

 

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

                              Detach, 159, 164

 

                   RHS

 

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

                              Substitute, 165, 157

 

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

                              Substitute, 166, 137

 

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

                              Join, 103, 167

 

                        169  y+1 e p1

                              Detach, 99, 168

 

              As Required:

 

                  170  ALL(b):[b e p1 => b+1 e p1]

                        4 Conclusion, 88

 

                  171  0 e p1 & ALL(b):[b e p1 => b+1 e p1]

                        Join, 87, 170

 

              By induction...

             

              As Required:

 

                  172  ALL(b):[b e n => b e p1]

                        Detach, 54, 171

 

                  

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

                  

                   Suppose...

 

                        173  y e n

                              Premise

 

                        174  y e n => y e p1

                              U Spec, 172

 

                        175  y e p1

                              Detach, 174, 173

 

                   Apply definition of p1

 

                        176  y e p1 <=> y e n & x^y*x^0=x^(y+0)

                              U Spec, 43

 

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

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

                              Iff-And, 176

 

                        178  y e p1 => y e n & x^y*x^0=x^(y+0)

                              Split, 177

 

                        179  y e n & x^y*x^0=x^(y+0) => y e p1

                              Split, 177

 

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

                              Detach, 178, 175

 

                        181  y e n

                              Split, 180

 

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

                              Split, 180

 

              As Required:

 

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

                        4 Conclusion, 173

 

          As Required:

 

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

                  4 Conclusion, 39

 

             

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

             

              Suppose...

 

                  185  x e n & y e n

                        Premise

 

                  186  x e n

                        Split, 185

 

                  187  y e n

                        Split, 185

 

              Apply definition of ^

 

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

                        U Spec, 184

 

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

                        Detach, 188, 186

 

                  190  y e n => x^y*x^0=x^(y+0)

                        U Spec, 189

 

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

                        Detach, 190, 187

 

          As Required:

 

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

                  4 Conclusion, 185

 

             

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

             

              Suppose...

 

                  193  x e n & y e n

                        Premise

 

                  194  x e n

                        Split, 193

 

                  195  y e n

                        Split, 193

 

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

                        Subset, 1

 

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

                        E Spec, 196

 

             

              Define: p2

              **********

 

                  198  Set(p2)

                        Split, 197

 

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

                        Split, 197

 

                  200  Set(p2) & ALL(b):[b e p2 => b e n]

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

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

                        U Spec, 9

 

                  

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

                  

                   Suppose...

 

                        201  q e p2

                              Premise

 

                        202  q e p2 <=> q e n & x^y*x^q=x^(y+q)

                              U Spec, 199

 

                        203  [q e p2 => q e n & x^y*x^q=x^(y+q)]

                        & [q e n & x^y*x^q=x^(y+q) => q e p2]

                              Iff-And, 202

 

                        204  q e p2 => q e n & x^y*x^q=x^(y+q)

                              Split, 203

 

                        205  q e n & x^y*x^q=x^(y+q) => q e p2

                              Split, 203

 

                        206  q e n & x^y*x^q=x^(y+q)

                              Detach, 204, 201

 

                        207  q e n

                              Split, 206

 

              As Required:

 

                  208  ALL(b):[b e p2 => b e n]

                        4 Conclusion, 201

 

                  209  Set(p2) & ALL(b):[b e p2 => b e n]

                        Join, 198, 208

 

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

 

                  210  0 e p2 & ALL(b):[b e p2 => b+1 e p2]

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

                        Detach, 200, 209

 

                  211  0 e p2 <=> 0 e n & x^y*x^0=x^(y+0)

                        U Spec, 199

 

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

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

                        Iff-And, 211

 

                  213  0 e p2 => 0 e n & x^y*x^0=x^(y+0)

                        Split, 212

 

              Sufficient: For 0 e p2

 

                  214  0 e n & x^y*x^0=x^(y+0) => 0 e p2

                        Split, 212

 

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

                        U Spec, 192

 

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

                        U Spec, 215

 

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

                        Detach, 216, 193

 

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

                        Join, 4, 217

 

              As Required:

 

                  219  0 e p2

                        Detach, 214, 218

 

                  

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

                  

                   Suppose...

 

                        220  z e p2

                              Premise

 

                        221  z e p2 <=> z e n & x^y*x^z=x^(y+z)

                              U Spec, 199

 

                        222  [z e p2 => z e n & x^y*x^z=x^(y+z)]

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

                              Iff-And, 221

 

                        223  z e p2 => z e n & x^y*x^z=x^(y+z)

                              Split, 222

 

                        224  z e n & x^y*x^z=x^(y+z) => z e p2

                              Split, 222

 

                        225  z e n & x^y*x^z=x^(y+z)

                              Detach, 223, 220

 

                        226  z e n

                              Split, 225

 

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

                              Split, 225

 

                        228  z+1 e p2 <=> z+1 e n & x^y*x^(z+1)=x^(y+(z+1))

                              U Spec, 199

 

                        229  [z+1 e p2 => z+1 e n & x^y*x^(z+1)=x^(y+(z+1))]

                        & [z+1 e n & x^y*x^(z+1)=x^(y+(z+1)) => z+1 e p2]

                              Iff-And, 228

 

                        230  z+1 e p2 => z+1 e n & x^y*x^(z+1)=x^(y+(z+1))

                              Split, 229

 

                   Sufficient: For z+1 e p2

 

                        231  z+1 e n & x^y*x^(z+1)=x^(y+(z+1)) => z+1 e p2

                              Split, 229

 

                        232  ALL(b):[z e n & b e n => z+b e n]

                              U Spec, 2

 

                        233  z e n & 1 e n => z+1 e n

                              U Spec, 232

 

                        234  z e n & 1 e n

                              Join, 226, 5

 

                        235  z+1 e n

                              Detach, 233, 234

 

                        236  x^y*x^(z+1)=x^y*x^(z+1)

                              Reflex

 

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

                              U Spec, 17

 

                        238  x e n & z e n => x^(z+1)=x^z*x

                              U Spec, 237

 

                        239  x e n & z e n

                              Join, 194, 226

 

                        240  x^(z+1)=x^z*x

                              Detach, 238, 239

 

                        241  x^y*x^(z+1)=x^y*(x^z*x)

                              Substitute, 240, 236

 

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

                              U Spec, 12

 

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

                              U Spec, 242

 

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

                              U Spec, 243

 

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

                              U Spec, 15

 

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

                              U Spec, 245

 

                        247  x^y e n

                              Detach, 246, 193

 

                        248  x e n & z e n => x^z e n

                              U Spec, 245

 

                        249  x e n & z e n

                              Join, 194, 226

 

                        250  x^z e n

                              Detach, 248, 249

 

                        251  x^y e n & x^z e n

                              Join, 247, 250

 

                        252  x^y e n & x^z e n & x e n

                              Join, 251, 194

 

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

                              Detach, 244, 252

 

                        254  x^y*x^(z+1)=x^y*x^z*x

                              Substitute, 253, 241

 

                   LHS

 

                        255  x^y*x^(z+1)=x^(y+z)*x

                              Substitute, 227, 254

 

                        256  x^(y+(z+1))=x^(y+(z+1))

                              Reflex

 

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

                              U Spec, 10

 

                        258  ALL(c):[y e n & z e n & c e n => y+z+c=y+(z+c)]

                              U Spec, 257

 

                        259  y e n & z e n & 1 e n => y+z+1=y+(z+1)

                              U Spec, 258

 

                        260  y e n & z e n

                              Join, 195, 226

 

                        261  y e n & z e n & 1 e n

                              Join, 260, 5

 

                        262  y+z+1=y+(z+1)

                              Detach, 259, 261

 

                        263  x^(y+(z+1))=x^(y+z+1)

                              Substitute, 262, 256

 

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

                              U Spec, 17

 

                        265  x e n & y+z e n => x^(y+z+1)=x^(y+z)*x

                              U Spec, 264

 

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

                              U Spec, 2

 

                        267  y e n & z e n => y+z e n

                              U Spec, 266

 

                        268  y e n & z e n

                              Join, 195, 226

 

                        269  y+z e n

                              Detach, 267, 268

 

                        270  x e n & y+z e n

                              Join, 194, 269

 

                        271  x^(y+z+1)=x^(y+z)*x

                              Detach, 265, 270

 

                   RHS

 

                        272  x^(y+(z+1))=x^(y+z)*x

                              Substitute, 271, 263

 

                        273  x^y*x^(z+1)=x^(y+(z+1))

                              Substitute, 272, 255

 

                        274  z+1 e n & x^y*x^(z+1)=x^(y+(z+1))

                              Join, 235, 273

 

                        275  z+1 e p2

                              Detach, 231, 274

 

              As Required:

 

                  276  ALL(b):[b e p2 => b+1 e p2]

                        4 Conclusion, 220

 

                  277  0 e p2 & ALL(b):[b e p2 => b+1 e p2]

                        Join, 219, 276

 

                  278  ALL(b):[b e n => b e p2]

                        Detach, 210, 277

 

                  

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

                  

                   Suppose...

 

                        279  z e n

                              Premise

 

                        280  z e n => z e p2

                              U Spec, 278

 

                        281  z e p2

                              Detach, 280, 279

 

                        282  z e p2 <=> z e n & x^y*x^z=x^(y+z)

                              U Spec, 199

 

                        283  [z e p2 => z e n & x^y*x^z=x^(y+z)]

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

                              Iff-And, 282

 

                        284  z e p2 => z e n & x^y*x^z=x^(y+z)

                              Split, 283

 

                        285  z e n & x^y*x^z=x^(y+z) => z e p2

                              Split, 283

 

                        286  z e n & x^y*x^z=x^(y+z)

                              Detach, 284, 281

 

                        287  z e n

                              Split, 286

 

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

                              Split, 286

 

              As Required:

 

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

                        4 Conclusion, 279

 

          As Required:

 

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

                  4 Conclusion, 193

 

             

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

             

              Suppose...

 

                  291  x e n & y e n & z e n

                        Premise

 

                  292  x e n

                        Split, 291

 

                  293  y e n

                        Split, 291

 

                  294  z e n

                        Split, 291

 

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

                        U Spec, 290

 

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

                        U Spec, 295

 

                  297  x e n & y e n

                        Join, 292, 293

 

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

                        Detach, 296, 297

 

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

                        U Spec, 298

 

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

                        Detach, 299, 294

 

          As Required:

 

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

                  4 Conclusion, 291

 

     As Required:

 

      302  0^0=0

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

            4 Conclusion, 38

 

         

          Case 2

         

          Prove: 0^0=1

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

         

          Suppose...

 

            303  0^0=1

                  Premise

 

             

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

             

              Suppose...

 

                  304  x e n

                        Premise

 

                  305  EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & x^b*x^0=x^(b+0)]]

                        Subset, 1

 

                  306  Set(p3) & ALL(b):[b e p3 <=> b e n & x^b*x^0=x^(b+0)]

                        E Spec, 305

 

             

              Define: p3

              **********

 

                  307  Set(p3)

                        Split, 306

 

                  308  ALL(b):[b e p3 <=> b e n & x^b*x^0=x^(b+0)]

                        Split, 306

 

              Apply PMI for p3

 

                  309  Set(p3) & ALL(b):[b e p3 => b e n]

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

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

                        U Spec, 9

 

                  

                   Prove: p3 is a subset of n

                  

                   Suppose...

 

                        310  q e p3

                              Premise

 

                        311  q e p3 <=> q e n & x^q*x^0=x^(q+0)

                              U Spec, 308

 

                        312  [q e p3 => q e n & x^q*x^0=x^(q+0)]

                        & [q e n & x^q*x^0=x^(q+0) => q e p3]

                              Iff-And, 311

 

                        313  q e p3 => q e n & x^q*x^0=x^(q+0)

                              Split, 312

 

                        314  q e n & x^q*x^0=x^(q+0) => q e p3

                              Split, 312

 

                        315  q e n & x^q*x^0=x^(q+0)

                              Detach, 313, 310

 

                        316  q e n

                              Split, 315

 

              As Required:

 

                  317  ALL(b):[b e p3 => b e n]

                        4 Conclusion, 310

 

                  318  Set(p3) & ALL(b):[b e p3 => b e n]

                        Join, 307, 317

 

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

 

                  319  0 e p3 & ALL(b):[b e p3 => b+1 e p3]

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

                        Detach, 309, 318

 

                  320  0 e p3 <=> 0 e n & x^0*x^0=x^(0+0)

                        U Spec, 308

 

                  321  [0 e p3 => 0 e n & x^0*x^0=x^(0+0)]

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

                        Iff-And, 320

 

                  322  0 e p3 => 0 e n & x^0*x^0=x^(0+0)

                        Split, 321

 

              Sufficient: For 0 e p3

 

                  323  0 e n & x^0*x^0=x^(0+0) => 0 e p3

                        Split, 321

 

              Two cases:

 

                  324  x=0 | ~x=0

                        Or Not

 

                   

                   Case 1

                  

                   Prove: x=0 => 0 e p3

                  

                   Suppose...

 

                        325  x=0

                              Premise

 

                        326  x^0=1

                              Substitute, 325, 303

 

                        327  1 e n => 1*1=1

                              U Spec, 8

 

                        328  1*1=1

                              Detach, 327, 5

 

                   LHS

 

                        329  x^0*x^0=1

                              Substitute, 326, 328

 

                        330  0 e n => 0+0=0

                              U Spec, 6

 

                        331  0+0=0

                              Detach, 330, 4

 

                   RHS

 

                        332  x^(0+0)=1

                              Substitute, 331, 326

 

                        333  x^0*x^0=x^(0+0)

                              Substitute, 332, 329

 

                        334  0 e n & x^0*x^0=x^(0+0)

                              Join, 4, 333

 

                        335  0 e p3

                              Detach, 323, 334

 

              As Required:

 

                  336  x=0 => 0 e p3

                        4 Conclusion, 325

 

                  

                   Case 2

                  

                   Prove: ~x=0 => 0 e p3

                  

                   Suppose...

 

                        337  ~x=0

                              Premise

 

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

                              U Spec, 16

 

                        339  ~x=0 => x^0=1

                              Detach, 338, 304

 

                        340  x^0=1

                              Detach, 339, 337

 

                        341  1 e n => 1*1=1

                              U Spec, 8

 

                        342  1*1=1

                              Detach, 341, 5

 

                   LHS

 

                        343  x^0*x^0=1

                              Substitute, 340, 342

 

                        344  0 e n => 0+0=0

                              U Spec, 6

 

                        345  0+0=0

                              Detach, 344, 4

 

                   RHS

 

                        346  x^(0+0)=1

                              Substitute, 345, 340

 

                        347  x^0*x^0=x^(0+0)

                              Substitute, 346, 343

 

                        348  0 e n & x^0*x^0=x^(0+0)

                              Join, 4, 347

 

                        349  0 e p3

                              Detach, 323, 348

 

              As Required:

 

                  350  ~x=0 => 0 e p3

                        4 Conclusion, 337

 

                  351  [x=0 => 0 e p3] & [~x=0 => 0 e p3]

                        Join, 336, 350

 

              As Required:

 

                  352  0 e p3

                        Cases, 324, 351

 

                  

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

                  

                   Suppose...

 

                        353  y e p3

                              Premise

 

                        354  y e p3 <=> y e n & x^y*x^0=x^(y+0)

                              U Spec, 308

 

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

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

                              Iff-And, 354

 

                        356  y e p3 => y e n & x^y*x^0=x^(y+0)

                              Split, 355

 

                        357  y e n & x^y*x^0=x^(y+0) => y e p3

                              Split, 355

 

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

                              Detach, 356, 353

 

                        359  y e n

                              Split, 358

 

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

                              Split, 358

 

                        361  y+1 e p3 <=> y+1 e n & x^(y+1)*x^0=x^(y+1+0)

                              U Spec, 308

 

                        362  [y+1 e p3 => y+1 e n & x^(y+1)*x^0=x^(y+1+0)]

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

                              Iff-And, 361

 

                        363  y+1 e p3 => y+1 e n & x^(y+1)*x^0=x^(y+1+0)

                              Split, 362

 

                   Sufficient: For y+1 e p3  (as above)

 

                        364  y+1 e n & x^(y+1)*x^0=x^(y+1+0) => y+1 e p3

                              Split, 362

 

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

                              U Spec, 2

 

                        366  y e n & 1 e n => y+1 e n

                              U Spec, 365

 

                        367  y e n & 1 e n

                              Join, 359, 5

 

                        368  y+1 e n

                              Detach, 366, 367

 

                        369  x^(y+1)*x^0=x^(y+1)*x^0

                              Reflex

 

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

                              U Spec, 17

 

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

                              U Spec, 370

 

                        372  x e n & y e n

                              Join, 304, 359

 

                        373  x^(y+1)=x^y*x

                              Detach, 371, 372

 

                        374  x^(y+1)*x^0=x^y*x*x^0

                              Substitute, 373, 369

 

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

                              U Spec, 12

 

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

                              U Spec, 375

 

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

                              U Spec, 376

 

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

                              U Spec, 15

 

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

                              U Spec, 378

 

                        380  x^y e n

                              Detach, 379, 372

 

                        381  x e n & 0 e n => x^0 e n

                              U Spec, 378

 

                        382  x e n & 0 e n

                              Join, 304, 4

 

                        383  x^0 e n

                              Detach, 381, 382

 

                        384  x^y e n & x e n

                              Join, 380, 304

 

                        385  x^y e n & x e n & x^0 e n

                              Join, 384, 383

 

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

                              Detach, 377, 385

 

                        387  x^(y+1)*x^0=x^y*(x*x^0)

                              Substitute, 386, 374

 

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

                              U Spec, 13

 

                        389  x e n & x^0 e n => x*x^0=x^0*x

                              U Spec, 388

 

                        390  x e n & x^0 e n

                              Join, 304, 383

 

                        391  x*x^0=x^0*x

                              Detach, 389, 390

 

                        392  x^(y+1)*x^0=x^y*(x^0*x)

                              Substitute, 391, 387

 

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

                              U Spec, 12

 

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

                              U Spec, 393

 

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

                              U Spec, 394

 

                        396  x^y e n & x^0 e n

                              Join, 380, 383

 

                        397  x^y e n & x^0 e n & x e n

                              Join, 396, 304

 

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

                              Detach, 395, 397

 

                        399  x^(y+1)*x^0=x^y*x^0*x

                              Substitute, 398, 392

 

                   LHS

 

                        400  x^(y+1)*x^0=x^(y+0)*x

                              Substitute, 360, 399

 

                        401  x^(y+1+0)=x^(y+1+0)

                              Reflex

 

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

                              U Spec, 10

 

                        403  ALL(c):[y e n & 1 e n & c e n => y+1+c=y+(1+c)]

                              U Spec, 402

 

                        404  y e n & 1 e n & 0 e n => y+1+0=y+(1+0)

                              U Spec, 403

 

                        405  y e n & 1 e n

                              Join, 359, 5

 

                        406  y e n & 1 e n & 0 e n

                              Join, 405, 4

 

                        407  y+1+0=y+(1+0)

                              Detach, 404, 406

 

                        408  x^(y+1+0)=x^(y+(1+0))

                              Substitute, 407, 401

 

                        409  ALL(b):[1 e n & b e n => 1+b=b+1]

                              U Spec, 11

 

                        410  1 e n & 0 e n => 1+0=0+1

                              U Spec, 409

 

                        411  1 e n & 0 e n

                              Join, 5, 4

 

                        412  1+0=0+1

                              Detach, 410, 411

 

                        413  x^(y+1+0)=x^(y+(0+1))

                              Substitute, 412, 408

 

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

                              U Spec, 10

 

                        415  ALL(c):[y e n & 0 e n & c e n => y+0+c=y+(0+c)]

                              U Spec, 414

 

                        416  y e n & 0 e n & 1 e n => y+0+1=y+(0+1)

                              U Spec, 415

 

                        417  y e n & 0 e n

                              Join, 359, 4

 

                        418  y e n & 0 e n & 1 e n

                              Join, 417, 5

 

                        419  y+0+1=y+(0+1)

                              Detach, 416, 418

 

                        420  x^(y+1+0)=x^(y+0+1)

                              Substitute, 419, 413

 

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

                              U Spec, 17

 

                        422  x e n & y+0 e n => x^(y+0+1)=x^(y+0)*x

                              U Spec, 421

 

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

                              U Spec, 2

 

                        424  y e n & 0 e n => y+0 e n

                              U Spec, 423

 

                        425  y e n & 0 e n

                              Join, 359, 4

 

                        426  y+0 e n

                              Detach, 424, 425

 

                        427  x e n & y+0 e n

                              Join, 304, 426

 

                        428  x^(y+0+1)=x^(y+0)*x

                              Detach, 422, 427

 

                   RHS

 

                        429  x^(y+1+0)=x^(y+0)*x

                              Substitute, 428, 420

 

                        430  x^(y+1)*x^0=x^(y+1+0)

                              Substitute, 429, 400

 

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

                              Join, 368, 430

 

                        432  y+1 e p3

                              Detach, 364, 431

 

              As Required:

 

                  433  ALL(b):[b e p3 => b+1 e p3]

                        4 Conclusion, 353

 

                  434  0 e p3 & ALL(b):[b e p3 => b+1 e p3]

                        Join, 352, 433

 

                  435  ALL(b):[b e n => b e p3]

                        Detach, 319, 434

 

                  

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

                  

                   Suppose...

 

                        436  y e n

                              Premise

 

                        437  y e n => y e p3

                              U Spec, 435

 

                        438  y e p3

                              Detach, 437, 436

 

                        439  y e p3 <=> y e n & x^y*x^0=x^(y+0)

                              U Spec, 308

 

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

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

                              Iff-And, 439

 

                        441  y e p3 => y e n & x^y*x^0=x^(y+0)

                              Split, 440

 

                        442  y e n & x^y*x^0=x^(y+0) => y e p3

                              Split, 440

 

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

                              Detach, 441, 438

 

                        444  y e n

                              Split, 443

 

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

                              Split, 443

 

              As Required:

 

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

                        4 Conclusion, 436

 

          As Required:

 

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

                  4 Conclusion, 304

 

             

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

             

              Suppose...

 

                  448  x e n & y e n

                        Premise

 

                  449  x e n

                        Split, 448

 

                  450  y e n

                        Split, 448

 

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

                        U Spec, 447

 

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

                        Detach, 451, 449

 

                  453  y e n => x^y*x^0=x^(y+0)

                        U Spec, 452

 

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

                        Detach, 453, 450

 

          As Required:

 

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

                  4 Conclusion, 448

 

                  456  x e n & y e n

                        Premise

 

                  457  x e n

                        Split, 456

 

                  458  y e n

                        Split, 456

 

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

                        Subset, 1

 

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

                        E Spec, 459

 

             

              Define: p4

              **********

 

                  461  Set(p4)

                        Split, 460

 

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

                        Split, 460

 

                  463  Set(p4) & ALL(b):[b e p4 => b e n]

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

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

                        U Spec, 9

 

                  

                   Prove: p4 is a subset of n

                  

                   Suppose...

 

                        464  q e p4

                              Premise

 

                        465  q e p4 <=> q e n & x^y*x^q=x^(y+q)

                              U Spec, 462

 

                        466  [q e p4 => q e n & x^y*x^q=x^(y+q)]

                        & [q e n & x^y*x^q=x^(y+q) => q e p4]

                              Iff-And, 465

 

                        467  q e p4 => q e n & x^y*x^q=x^(y+q)

                              Split, 466

 

                        468  q e n & x^y*x^q=x^(y+q) => q e p4

                              Split, 466

 

                        469  q e n & x^y*x^q=x^(y+q)

                              Detach, 467, 464

 

                        470  q e n

                              Split, 469

 

              As Required:

 

                  471  ALL(b):[b e p4 => b e n]

                        4 Conclusion, 464

 

                  472  Set(p4) & ALL(b):[b e p4 => b e n]

                        Join, 461, 471

 

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

 

                  473  0 e p4 & ALL(b):[b e p4 => b+1 e p4]

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

                        Detach, 463, 472

 

                  474  0 e p4 <=> 0 e n & x^y*x^0=x^(y+0)

                        U Spec, 462

 

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

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

                        Iff-And, 474

 

                  476  0 e p4 => 0 e n & x^y*x^0=x^(y+0)

                        Split, 475

 

              Sufficient: For 0 e p4           x^0*x^0=x^(0+0)???

 

                  477  0 e n & x^y*x^0=x^(y+0) => 0 e p4

                        Split, 475

 

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

                        U Spec, 455

 

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

                        U Spec, 478

 

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

                        Detach, 479, 456

 

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

                        Join, 4, 480

 

              As Required:

 

                  482  0 e p4

                        Detach, 477, 481

 

                  

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

                  

                   Suppose...

 

                        483  z e p4

                              Premise

 

                        484  z e p4 <=> z e n & x^y*x^z=x^(y+z)

                              U Spec, 462

 

                        485  [z e p4 => z e n & x^y*x^z=x^(y+z)]

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

                              Iff-And, 484

 

                        486  z e p4 => z e n & x^y*x^z=x^(y+z)

                              Split, 485

 

                        487  z e n & x^y*x^z=x^(y+z) => z e p4

                              Split, 485

 

                        488  z e n & x^y*x^z=x^(y+z)

                              Detach, 486, 483

 

                        489  z e n

                              Split, 488

 

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

                              Split, 488

 

                        491  z+1 e p4 <=> z+1 e n & x^y*x^(z+1)=x^(y+(z+1))

                              U Spec, 462

 

                        492  [z+1 e p4 => z+1 e n & x^y*x^(z+1)=x^(y+(z+1))]

                        & [z+1 e n & x^y*x^(z+1)=x^(y+(z+1)) => z+1 e p4]

                              Iff-And, 491

 

                        493  z+1 e p4 => z+1 e n & x^y*x^(z+1)=x^(y+(z+1))

                              Split, 492

 

                   Sufficient: For z+1 e p4

 

                        494  z+1 e n & x^y*x^(z+1)=x^(y+(z+1)) => z+1 e p4

                              Split, 492

 

                        495  ALL(b):[z e n & b e n => z+b e n]

                              U Spec, 2

 

                        496  z e n & 1 e n => z+1 e n

                              U Spec, 495

 

                        497  z e n & 1 e n

                              Join, 489, 5

 

                        498  z+1 e n

                              Detach, 496, 497

 

                        499  x^y*x^(z+1)=x^y*x^(z+1)

                              Reflex

 

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

                              U Spec, 17

 

                        501  x e n & z e n => x^(z+1)=x^z*x

                              U Spec, 500

 

                        502  x e n & z e n

                              Join, 457, 489

 

                        503  x^(z+1)=x^z*x

                              Detach, 501, 502

 

                        504  x^y*x^(z+1)=x^y*(x^z*x)

                              Substitute, 503, 499

 

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

                              U Spec, 12

 

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

                              U Spec, 505

 

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

                              U Spec, 506

 

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

                              U Spec, 15

 

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

                              U Spec, 508

 

                        510  x^y e n

                              Detach, 509, 456

 

                        511  x e n & z e n => x^z e n

                              U Spec, 508

 

                        512  x e n & z e n

                              Join, 457, 489

 

                        513  x^z e n

                              Detach, 511, 512

 

                        514  x^y e n & x^z e n

                              Join, 510, 513

 

                        515  x^y e n & x^z e n & x e n

                              Join, 514, 457

 

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

                              Detach, 507, 515

 

                        517  x^y*x^(z+1)=x^y*x^z*x

                              Substitute, 516, 504

 

                   LHS

 

                        518  x^y*x^(z+1)=x^(y+z)*x

                              Substitute, 490, 517

 

                        519  x^(y+(z+1))=x^(y+(z+1))

                              Reflex

 

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

                              U Spec, 10

 

                        521  ALL(c):[y e n & z e n & c e n => y+z+c=y+(z+c)]

                              U Spec, 520

 

                        522  y e n & z e n & 1 e n => y+z+1=y+(z+1)

                              U Spec, 521

 

                        523  y e n & z e n

                              Join, 458, 489

 

                        524  y e n & z e n & 1 e n

                              Join, 523, 5

 

                        525  y+z+1=y+(z+1)

                              Detach, 522, 524

 

                        526  x^(y+(z+1))=x^(y+z+1)

                              Substitute, 525, 519

 

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

                              U Spec, 17

 

                        528  x e n & y+z e n => x^(y+z+1)=x^(y+z)*x

                              U Spec, 527

 

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

                              U Spec, 2

 

                        530  y e n & z e n => y+z e n

                              U Spec, 529

 

                        531  y e n & z e n

                              Join, 458, 489

 

                        532  y+z e n

                              Detach, 530, 531

 

                        533  x e n & y+z e n

                              Join, 457, 532

 

                        534  x^(y+z+1)=x^(y+z)*x

                              Detach, 528, 533

 

                   RHS

 

                        535  x^(y+(z+1))=x^(y+z)*x

                              Substitute, 534, 526

 

                        536  x^y*x^(z+1)=x^(y+(z+1))

                              Substitute, 535, 518

 

                        537  z+1 e n & x^y*x^(z+1)=x^(y+(z+1))

                              Join, 498, 536

 

                        538  z+1 e p4

                              Detach, 494, 537

 

              As Required:

 

                  539  ALL(b):[b e p4 => b+1 e p4]

                        4 Conclusion, 483

 

                  540  0 e p4 & ALL(b):[b e p4 => b+1 e p4]

                        Join, 482, 539

 

              As Required:

 

                  541  ALL(b):[b e n => b e p4]

                        Detach, 473, 540

 

                  

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

                  

                   Suppose...

 

                        542  z e n

                              Premise

 

                        543  z e n => z e p4

                              U Spec, 541

 

                        544  z e p4

                              Detach, 543, 542

 

                        545  z e p4 <=> z e n & x^y*x^z=x^(y+z)

                              U Spec, 462

 

                        546  [z e p4 => z e n & x^y*x^z=x^(y+z)]

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

                              Iff-And, 545

 

                        547  z e p4 => z e n & x^y*x^z=x^(y+z)

                              Split, 546

 

                        548  z e n & x^y*x^z=x^(y+z) => z e p4

                              Split, 546

 

                        549  z e n & x^y*x^z=x^(y+z)

                              Detach, 547, 544

 

                        550  z e n

                              Split, 549

 

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

                              Split, 549

 

              As Required:

 

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

                        4 Conclusion, 542

 

          As Required:

 

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

                  4 Conclusion, 456

 

             

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

             

              Suppose...

 

                  554  x e n & y e n & z e n

                        Premise

 

                  555  x e n

                        Split, 554

 

                  556  y e n

                        Split, 554

 

                  557  z e n

                        Split, 554

 

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

                        U Spec, 553

 

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

                        U Spec, 558

 

                  560  x e n & y e n

                        Join, 555, 556

 

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

                        Detach, 559, 560

 

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

                        U Spec, 561

 

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

                        Detach, 562, 557

 

          As Required:

 

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

                  4 Conclusion, 554

 

     As Required:

 

      565  0^0=1

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

            4 Conclusion, 303

 

      566  [0^0=0

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

          & [0^0=1

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

            Join, 302, 565

 

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

            Cases, 37, 566

 

As Required:

 

568  0^0=0 | 0^0=1

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

      4 Conclusion, 37

 

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

     => 0^0=0 | 0^0=1]

     & [0^0=0 | 0^0=1

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

      Join, 36, 568

 

As Required:

 

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

     <=> 0^0=0 | 0^0=1

      Iff-And, 569