THEOREM 1

*********

 

There exists infinitely many exponent-like functions on the natural numbers. Here we show that, for every

natural number x0, there exists a function pow such that:

 

pow(0,0)   = x0             (0^0 = x0)

pow(a,0)   = 1  for ~a=0    (a^1 = 1)

pow(a,b+1) = pow(a,b) * a   (a^(b+1) = a^b * a)

 

Formally, we prove:

 

ALL(x0):[x0 e n

=> EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

& pow(0,0)=x0

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

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

 

 

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 )

 

 

OUTLINE

*******

 

Lines 1-8       The basic principles of arithematic assumed here

 

Lines 9-18      Constructing the set n3 of ordered triples of natural number using the Cartesian Product Axiom

 

Lines 19-24     Constructing the set pn3, the power set of n3, using the Power Set Axiom

 

Lines 25-29     Constructing a subset pow of n3 using the Subset Axiom

 

Line3 30-490    Establishing some useful properties of the pow set

 

Lines 491-960   Proving that pow is a function

 

Lines 961-1038  Establishing the required properties of the pow function

 

 

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

 

The principle of mathematical induction (starting at 0)

 

6     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

 

Right cancelability of +

 

7     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

 

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

      Axiom

 

 

PROOF

*****

 

Construct the set of ordered triples of n

 

Apply Cartesian Product Axiom

 

9     ALL(a1):ALL(a2):ALL(a3):[Set(a1) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e a1 & c2 e a2 & c3 e a3]]]

      Cart Prod

 

10    ALL(a2):ALL(a3):[Set(n) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e a2 & c3 e a3]]]

      U Spec, 9

 

11    ALL(a3):[Set(n) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e a3]]]

      U Spec, 10

 

12    Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]

      U Spec, 11

 

13    Set(n) & Set(n)

      Join, 1, 1

 

14    Set(n) & Set(n) & Set(n)

      Join, 13, 1

 

15    EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]

      Detach, 12, 14

 

16    Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

      E Spec, 15

 

 

Define: n3  (the set of ordered triples of n)

**********

 

17    Set''(n3)

      Split, 16

 

18    ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]

      Split, 16

 

 

Construct the powerset of n3

 

Apply the Power Set Axiom

 

19    ALL(a):[Set''(a) => EXIST(b):[Set(b)

     & ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e a]]]]

      Power Set

 

20    Set''(n3) => EXIST(b):[Set(b)

     & ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]]

      U Spec, 19

 

21    EXIST(b):[Set(b)

     & ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]]

      Detach, 20, 17

 

22    Set(pn3)

     & ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]

      E Spec, 21

 

 

Define: pn3  (the power set of n3)

***********

 

23    Set(pn3)

      Split, 22

 

24    ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]

      Split, 22

 

    

     Prove: ALL(x0):[x0 e n

           => EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

           & pow(0,0)=x0

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

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

    

     Suppose...

 

      25    x0 e n

            Premise

 

     Construct the set pow, a subset of n3

    

     Apply the Subset Axiom

 

      26    EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

          <=> (a,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (a,b,c) e d]]]

            Subset, 17

 

      27    Set''(pow) & ALL(a):ALL(b):ALL(c):[(a,b,c) e pow

          <=> (a,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (a,b,c) e d]]

            E Spec, 26

 

    

     Define: pow

     ***********

 

      28    Set''(pow)

            Split, 27

 

      29    ALL(a):ALL(b):ALL(c):[(a,b,c) e pow

          <=> (a,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (a,b,c) e d]]

            Split, 27

 

     Establish some useful properties of pow

    

     Prove: (0,0,x0) e pow

    

     Apply definition of pow

 

      30    ALL(b):ALL(c):[(0,b,c) e pow

          <=> (0,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,b,c) e d]]

            U Spec, 29

 

      31    ALL(c):[(0,0,c) e pow

          <=> (0,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,0,c) e d]]

            U Spec, 30

 

      32    (0,0,x0) e pow

          <=> (0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,0,x0) e d]

            U Spec, 31

 

      33    [(0,0,x0) e pow => (0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,0,x0) e d]]

          & [(0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,0,x0) e d] => (0,0,x0) e pow]

            Iff-And, 32

 

      34    (0,0,x0) e pow => (0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,0,x0) e d]

            Split, 33

 

     Sufficient: (0,0,x0) e pow

 

      35    (0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,0,x0) e d] => (0,0,x0) e pow

            Split, 33

 

     Prove: (0,0,x0) e n3

 

      36    ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]

            U Spec, 18

 

      37    ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]

            U Spec, 36

 

      38    (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n

            U Spec, 37

 

      39    [(0,0,x0) e n3 => 0 e n & 0 e n & x0 e n]

          & [0 e n & 0 e n & x0 e n => (0,0,x0) e n3]

            Iff-And, 38

 

      40    (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n

            Split, 39

 

      41    0 e n & 0 e n & x0 e n => (0,0,x0) e n3

            Split, 39

 

      42    0 e n & 0 e n

            Join, 4, 4

 

      43    0 e n & 0 e n & x0 e n

            Join, 42, 25

 

      44    (0,0,x0) e n3

            Detach, 41, 43

 

          Prove: ALL(d):[d e pn3 & (0,0,x0) e d

                 & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

         

          Suppose...

 

            45    q e pn3 & (0,0,x0) e q

              & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                  Premise

 

            46    q e pn3

                  Split, 45

 

            47    (0,0,x0) e q

                  Split, 45

 

      48    ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,0,x0) e d]

            4 Conclusion, 45

 

      49    (0,0,x0) e n3

          & ALL(d):[d e pn3 & (0,0,x0) e d

          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

          => (0,0,x0) e d]

            Join, 44, 48

 

     As Required:

 

      50    (0,0,x0) e pow

            Detach, 35, 49

 

         

          Prove: ALL(a):[a e n => [~a=0 => (a,0,1) e pow]]

         

          Suppose...

 

            51    x e n

                  Premise

 

             

              Prove: ~x=0 => (x,0,1) e pow

             

              Suppose...

 

                  52    ~x=0

                        Premise

 

              Apply definition of pow

 

                  53    ALL(b):ALL(c):[(x,b,c) e pow

                   <=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,b,c) e d]]

                        U Spec, 29

 

                  54    ALL(c):[(x,0,c) e pow

                   <=> (x,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,0,c) e d]]

                        U Spec, 53

 

                  55    (x,0,1) e pow

                   <=> (x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,0,1) e d]

                        U Spec, 54

 

                  56    [(x,0,1) e pow => (x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,0,1) e d]]

                   & [(x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,0,1) e d] => (x,0,1) e pow]

                        Iff-And, 55

 

                  57    (x,0,1) e pow => (x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,0,1) e d]

                        Split, 56

 

              Sufficient: (x,0,1) e pow

 

                  58    (x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,0,1) e d] => (x,0,1) e pow

                        Split, 56

 

              Prove: (x,0,1) e n3

             

              Apply definition of n3

 

                  59    ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                        U Spec, 18

 

                  60    ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]

                        U Spec, 59

 

                  61    (x,0,1) e n3 <=> x e n & 0 e n & 1 e n

                        U Spec, 60

 

                  62    [(x,0,1) e n3 => x e n & 0 e n & 1 e n]

                   & [x e n & 0 e n & 1 e n => (x,0,1) e n3]

                        Iff-And, 61

 

                  63    (x,0,1) e n3 => x e n & 0 e n & 1 e n

                        Split, 62

 

                  64    x e n & 0 e n & 1 e n => (x,0,1) e n3

                        Split, 62

 

                  65    x e n & 0 e n

                        Join, 51, 4

 

                  66    x e n & 0 e n & 1 e n

                        Join, 65, 5

 

                  67    (x,0,1) e n3

                        Detach, 64, 66

 

                        68    q e pn3 & (0,0,x0) e q

                        & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                              Premise

 

                        69    q e pn3

                              Split, 68

 

                        70    (0,0,x0) e q

                              Split, 68

 

                        71    ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                              Split, 68

 

                        72    ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                              Split, 68

 

                        73    x e n => [~x=0 => (x,0,1) e q]

                              U Spec, 71

 

                        74    ~x=0 => (x,0,1) e q

                              Detach, 73, 51

 

                        75    (x,0,1) e q

                              Detach, 74, 52

 

                  76    ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,0,1) e d]

                        4 Conclusion, 68

 

                  77    (x,0,1) e n3

                   & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,0,1) e d]

                        Join, 67, 76

 

                  78    (x,0,1) e pow

                        Detach, 58, 77

 

          As Required:

 

            79    ~x=0 => (x,0,1) e pow

                  4 Conclusion, 52

 

     As Required:

 

      80    ALL(a):[a e n => [~a=0 => (a,0,1) e pow]]

            4 Conclusion, 51

 

         

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

                 => [(a,b,c) e pow => (a,b+1,c*a) e pow]]

         

          Suppose...

 

            81    x e n & y e n & z e n

                  Premise

 

            82    x e n

                  Split, 81

 

            83    y e n

                  Split, 81

 

            84    z e n

                  Split, 81

 

             

              Prove: (x,y,z) e pow => (x,y+1,z*x) e pow

             

              Suppose...

 

                  85    (x,y,z) e pow

                        Premise

 

              Apply definition of pow

 

                  86    ALL(b):ALL(c):[(x,b,c) e pow

                   <=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,b,c) e d]]

                        U Spec, 29

 

                  87    ALL(c):[(x,y,c) e pow

                   <=> (x,y,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y,c) e d]]

                        U Spec, 86

 

                  88    (x,y,z) e pow

                   <=> (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y,z) e d]

                        U Spec, 87

 

                  89    [(x,y,z) e pow => (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y,z) e d]]

                   & [(x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y,z) e d] => (x,y,z) e pow]

                        Iff-And, 88

 

                  90    (x,y,z) e pow => (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y,z) e d]

                        Split, 89

 

                  91    (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y,z) e d] => (x,y,z) e pow

                        Split, 89

 

                  92    (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y,z) e d]

                        Detach, 90, 85

 

                  93    (x,y,z) e n3

                        Split, 92

 

                  94    ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y,z) e d]

                        Split, 92

 

              Apply definition of pow

 

                  95    ALL(b):ALL(c):[(x,b,c) e pow

                   <=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,b,c) e d]]

                        U Spec, 29

 

                  96    ALL(c):[(x,y+1,c) e pow

                   <=> (x,y+1,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y+1,c) e d]]

                        U Spec, 95

 

                  97    (x,y+1,z*x) e pow

                   <=> (x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y+1,z*x) e d]

                        U Spec, 96

 

                  98    [(x,y+1,z*x) e pow => (x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y+1,z*x) e d]]

                   & [(x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y+1,z*x) e d] => (x,y+1,z*x) e pow]

                        Iff-And, 97

 

                  99    (x,y+1,z*x) e pow => (x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y+1,z*x) e d]

                        Split, 98

 

              Sufficient: (x,y+1,z*x) e pow

 

                  100  (x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y+1,z*x) e d] => (x,y+1,z*x) e pow

                        Split, 98

 

              Prove: (x,y+1,z*x) e n3

             

              Apply definition of n3

 

                  101  ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                        U Spec, 18

 

                  102  ALL(c3):[(x,y+1,c3) e n3 <=> x e n & y+1 e n & c3 e n]

                        U Spec, 101

 

                  103  (x,y+1,z*x) e n3 <=> x e n & y+1 e n & z*x e n

                        U Spec, 102

 

                  104  [(x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n]

                   & [x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3]

                        Iff-And, 103

 

                  105  (x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n

                        Split, 104

 

                  106  x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3

                        Split, 104

 

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

                        U Spec, 2

 

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

                        U Spec, 107

 

                  109  y e n & 1 e n

                        Join, 83, 5

 

                  110  y+1 e n

                        Detach, 108, 109

 

                  111  ALL(b):[z e n & b e n => z*b e n]

                        U Spec, 3

 

                  112  z e n & x e n => z*x e n

                        U Spec, 111

 

                  113  z e n & x e n

                        Join, 84, 82

 

                  114  z*x e n

                        Detach, 112, 113

 

                  115  x e n & y+1 e n

                        Join, 82, 110

 

                  116  x e n & y+1 e n & z*x e n

                        Join, 115, 114

 

                  117  (x,y+1,z*x) e n3

                        Detach, 106, 116

 

                  

                   Prove: ALL(d):[d e pn3 & (0,0,x0) e d

                          & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                          & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                          => (x,y+1,z*x) e d]

                  

                   Suppose...

 

                        118  q e pn3 & (0,0,x0) e q

                        & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                              Premise

 

                        119  q e pn3

                              Split, 118

 

                        120  (0,0,x0) e q

                              Split, 118

 

                        121  ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                              Split, 118

 

                    Apply definition of q

 

                        122  ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                              Split, 118

 

                        123  ALL(f):ALL(g):[(x,f,g) e q => (x,f+1,g*x) e q]

                              U Spec, 122

 

                        124  ALL(g):[(x,y,g) e q => (x,y+1,g*x) e q]

                              U Spec, 123

 

                        125  (x,y,z) e q => (x,y+1,z*x) e q

                              U Spec, 124

 

                        126  q e pn3 & (0,0,x0) e q

                        & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                        & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                        => (x,y,z) e q

                              U Spec, 94

 

                        127  (x,y,z) e q

                              Detach, 126, 118

 

                        128  (x,y+1,z*x) e q

                              Detach, 125, 127

 

              As Required:

 

                  129  ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y+1,z*x) e d]

                        4 Conclusion, 118

 

                  130  (x,y+1,z*x) e n3

                   & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (x,y+1,z*x) e d]

                        Join, 117, 129

 

                  131  (x,y+1,z*x) e pow

                        Detach, 100, 130

 

          As Required:

 

            132  (x,y,z) e pow => (x,y+1,z*x) e pow

                  4 Conclusion, 85

 

     As Required:

 

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

          => [(a,b,c) e pow => (a,b+1,c*a) e pow]]

            4 Conclusion, 81

 

         

          Prove: ALL(a):[a e n => [(0,0,a) e pow => a=x0]]

         

          Suppose...

 

            134  z e n

                  Premise

 

             

              Prove: ~[(0,0,z) e pow & ~z=x0]

             

              Suppose to contrary...

 

                  135  (0,0,z) e pow & ~z=x0

                        Premise

 

                  136  (0,0,z) e pow

                        Split, 135

 

                  137  ~z=x0

                        Split, 135

 

              Apply definition of pow

 

                  138  ALL(b):ALL(c):[(0,b,c) e pow

                   <=> (0,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,b,c) e d]]

                        U Spec, 29

 

                  139  ALL(c):[(0,0,c) e pow

                   <=> (0,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,c) e d]]

                        U Spec, 138

 

                  140  (0,0,z) e pow

                   <=> (0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,z) e d]

                        U Spec, 139

 

                  141  [(0,0,z) e pow => (0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,z) e d]]

                   & [(0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,z) e d] => (0,0,z) e pow]

                        Iff-And, 140

 

                  142  (0,0,z) e pow => (0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,z) e d]

                        Split, 141

 

                  143  (0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,z) e d] => (0,0,z) e pow

                        Split, 141

 

                  144  ~[(0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,z) e d]] => ~(0,0,z) e pow

                        Contra, 142

 

                  145  ~~[~(0,0,z) e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,z) e d]] => ~(0,0,z) e pow

                        DeMorgan, 144

 

                  146  ~(0,0,z) e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   => (0,0,z) e d] => ~(0,0,z) e pow

                        Rem DNeg, 145

 

                  147  ~(0,0,z) e n3 | ~ALL(d):~[d e pn3 & (0,0,x0) e d

                    & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e pow

                        Imply-And, 146

 

                  148  ~(0,0,z) e n3 | ~~EXIST(d):~~[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e pow

                        Quant, 147

 

                  149  ~(0,0,z) e n3 | EXIST(d):~~[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e pow

                        Rem DNeg, 148

 

              Sufficient: ~(0,0,z) e pow  (to obtain contradiction)

 

                  150  ~(0,0,z) e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e pow

                        Rem DNeg, 149

 

                  151  EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

                   <=> (a,b,c) e n3 & ~[a=0 & b=0 & c=z]]]

                        Subset, 17

 

                  152  Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                   <=> (a,b,c) e n3 & ~[a=0 & b=0 & c=z]]

                        E Spec, 151

 

              Define: q

 

                  153  Set''(q)

                        Split, 152

 

                  154  ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                   <=> (a,b,c) e n3 & ~[a=0 & b=0 & c=z]]

                        Split, 152

 

                  155  q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                        U Spec, 24

 

                  156  [q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]]

                   & [Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]

                        Iff-And, 155

 

                  157  q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                        Split, 156

 

                  158  Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3

                        Split, 156

 

                  

                   Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                  

                   Suppose...

 

                        159  (t,u,v) e q

                              Premise

 

                   Apply definition of q

 

                        160  ALL(b):ALL(c):[(t,b,c) e q

                        <=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]

                              U Spec, 154

 

                        161  ALL(c):[(t,u,c) e q

                        <=> (t,u,c) e n3 & ~[t=0 & u=0 & c=z]]

                              U Spec, 160

 

                        162  (t,u,v) e q

                        <=> (t,u,v) e n3 & ~[t=0 & u=0 & v=z]

                              U Spec, 161

 

                        163  [(t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]]

                        & [(t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q]

                              Iff-And, 162

 

                        164  (t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]

                              Split, 163

 

                        165  (t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q

                              Split, 163

 

                        166  (t,u,v) e n3 & ~[t=0 & u=0 & v=z]

                              Detach, 164, 159

 

                        167  (t,u,v) e n3

                              Split, 166

 

              As Required:

 

                  168  ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                        4 Conclusion, 159

 

                  169  Set''(q)

                   & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                        Join, 153, 168

 

              As Required:

 

                  170  q e pn3

                        Detach, 158, 169

 

             

              Prove: (0,0,x0) e q

             

              Apply definition of q

 

                  171  ALL(b):ALL(c):[(0,b,c) e q

                   <=> (0,b,c) e n3 & ~[0=0 & b=0 & c=z]]

                        U Spec, 154

 

                  172  ALL(c):[(0,0,c) e q

                   <=> (0,0,c) e n3 & ~[0=0 & 0=0 & c=z]]

                        U Spec, 171

 

                  173  (0,0,x0) e q

                   <=> (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]

                        U Spec, 172

 

                  174  [(0,0,x0) e q => (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]]

                   & [(0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q]

                        Iff-And, 173

 

                  175  (0,0,x0) e q => (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]

                        Split, 174

 

                  176  (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q

                        Split, 174

 

                  177  ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]

                        U Spec, 18

 

                  178  ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]

                        U Spec, 177

 

                  179  (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n

                        U Spec, 178

 

                  180  [(0,0,x0) e n3 => 0 e n & 0 e n & x0 e n]

                   & [0 e n & 0 e n & x0 e n => (0,0,x0) e n3]

                        Iff-And, 179

 

                  181  (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n

                        Split, 180

 

                  182  0 e n & 0 e n & x0 e n => (0,0,x0) e n3

                        Split, 180

 

                  183  0 e n & 0 e n

                        Join, 4, 4

 

                  184  0 e n & 0 e n & x0 e n

                        Join, 183, 25

 

                  185  (0,0,x0) e n3

                        Detach, 182, 184

 

                  

                   Prove: ~[0=0 & 0=0 & x0=z]

                  

                   Suppose to the contrary...

 

                        186  0=0 & 0=0 & x0=z

                              Premise

 

                        187  0=0

                              Split, 186

 

                        188  0=0

                              Split, 186

 

                        189  x0=z

                              Split, 186

 

                        190  ~x0=z

                              Sym, 137

 

                        191  x0=z & ~x0=z

                              Join, 189, 190

 

              As Required:

 

                  192  ~[0=0 & 0=0 & x0=z]

                        4 Conclusion, 186

 

                  193  (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]

                        Join, 185, 192

 

              As Required:

 

                  194  (0,0,x0) e q

                        Detach, 176, 193

 

             

              Prove: ~(0,0,z) e q

             

              Apply definition of q

 

                  195  ALL(b):ALL(c):[(0,b,c) e q

                   <=> (0,b,c) e n3 & ~[0=0 & b=0 & c=z]]

                        U Spec, 154

 

                  196  ALL(c):[(0,0,c) e q

                   <=> (0,0,c) e n3 & ~[0=0 & 0=0 & c=z]]

                        U Spec, 195

 

                  197  (0,0,z) e q

                   <=> (0,0,z) e n3 & ~[0=0 & 0=0 & z=z]

                        U Spec, 196

 

                  198  [(0,0,z) e q => (0,0,z) e n3 & ~[0=0 & 0=0 & z=z]]

                   & [(0,0,z) e n3 & ~[0=0 & 0=0 & z=z] => (0,0,z) e q]

                        Iff-And, 197

 

                  199  (0,0,z) e q => (0,0,z) e n3 & ~[0=0 & 0=0 & z=z]

                        Split, 198

 

                  200  (0,0,z) e n3 & ~[0=0 & 0=0 & z=z] => (0,0,z) e q

                        Split, 198

 

                  201  ~[(0,0,z) e n3 & ~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q

                        Contra, 199

 

                  202  ~~[~(0,0,z) e n3 | ~~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q

                        DeMorgan, 201

 

                  203  ~(0,0,z) e n3 | ~~[0=0 & 0=0 & z=z] => ~(0,0,z) e q

                        Rem DNeg, 202

 

                  204  ~(0,0,z) e n3 | 0=0 & 0=0 & z=z => ~(0,0,z) e q

                        Rem DNeg, 203

 

                  205  0=0

                        Reflex

 

                  206  z=z

                        Reflex

 

                  207  0=0 & 0=0

                        Join, 205, 205

 

                  208  0=0 & 0=0 & z=z

                        Join, 207, 206

 

                  209  ~(0,0,z) e n3 | 0=0 & 0=0 & z=z

                        Arb Or, 208

 

              As Required:

 

                  210  ~(0,0,z) e q

                        Detach, 204, 209

 

                        211  t e n

                              Premise

 

                       

                        Prove: ~t=0 => (t,0,1) e q

                       

                        Suppose...

 

                              212  ~t=0

                                    Premise

 

                        Apply definition of q

 

                              213  ALL(b):ALL(c):[(t,b,c) e q

                             <=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]

                                    U Spec, 154

 

                              214  ALL(c):[(t,0,c) e q

                             <=> (t,0,c) e n3 & ~[t=0 & 0=0 & c=z]]

                                    U Spec, 213

 

                              215  (t,0,1) e q

                             <=> (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]

                                    U Spec, 214

 

                              216  [(t,0,1) e q => (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]]

                             & [(t,0,1) e n3 & ~[t=0 & 0=0 & 1=z] => (t,0,1) e q]

                                    Iff-And, 215

 

                              217  (t,0,1) e q => (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]

                                    Split, 216

 

                        Sufficient: (t,0,1) e q

 

                              218  (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z] => (t,0,1) e q

                                    Split, 216

 

                              219  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                                    U Spec, 18

 

                              220  ALL(c3):[(t,0,c3) e n3 <=> t e n & 0 e n & c3 e n]

                                    U Spec, 219

 

                              221  (t,0,1) e n3 <=> t e n & 0 e n & 1 e n

                                    U Spec, 220

 

                              222  [(t,0,1) e n3 => t e n & 0 e n & 1 e n]

                             & [t e n & 0 e n & 1 e n => (t,0,1) e n3]

                                    Iff-And, 221

 

                              223  (t,0,1) e n3 => t e n & 0 e n & 1 e n

                                    Split, 222

 

                              224  t e n & 0 e n & 1 e n => (t,0,1) e n3

                                    Split, 222

 

                              225  t e n & 0 e n

                                    Join, 211, 4

 

                              226  t e n & 0 e n & 1 e n

                                    Join, 225, 5

 

                              227  (t,0,1) e n3

                                    Detach, 224, 226

 

                            

                             Prove: ~[t=0 & 0=0 & 1=z]

                            

                             Suppose to the contrary...

 

                                    228  t=0 & 0=0 & 1=z

                                          Premise

 

                                    229  t=0

                                          Split, 228

 

                                    230  0=0

                                          Split, 228

 

                                    231  1=z

                                          Split, 228

 

                                    232  t=0 & ~t=0

                                          Join, 229, 212

 

                        As Required:

 

                              233  ~[t=0 & 0=0 & 1=z]

                                    4 Conclusion, 228

 

                              234  (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]

                                    Join, 227, 233

 

                              235  (t,0,1) e q

                                    Detach, 218, 234

 

                   As Required:

 

                        236  ~t=0 => (t,0,1) e q

                              4 Conclusion, 212

 

              As Required:

 

                  237  ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                        4 Conclusion, 211

 

                  

                   Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                  

                   Suppose...

 

                        238  (t,u,v) e q

                              Premise

 

                        239  ALL(b):ALL(c):[(t,b,c) e q

                        <=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]

                              U Spec, 154

 

                        240  ALL(c):[(t,u,c) e q

                        <=> (t,u,c) e n3 & ~[t=0 & u=0 & c=z]]

                              U Spec, 239

 

                        241  (t,u,v) e q

                        <=> (t,u,v) e n3 & ~[t=0 & u=0 & v=z]

                              U Spec, 240

 

                        242  [(t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]]

                        & [(t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q]

                              Iff-And, 241

 

                        243  (t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]

                              Split, 242

 

                        244  (t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q

                              Split, 242

 

                        245  (t,u,v) e n3 & ~[t=0 & u=0 & v=z]

                              Detach, 243, 238

 

                        246  (t,u,v) e n3

                              Split, 245

 

                        247  ~[t=0 & u=0 & v=z]

                              Split, 245

 

                        248  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                              U Spec, 18

 

                        249  ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]

                              U Spec, 248

 

                        250  (t,u,v) e n3 <=> t e n & u e n & v e n

                              U Spec, 249

 

                        251  [(t,u,v) e n3 => t e n & u e n & v e n]

                        & [t e n & u e n & v e n => (t,u,v) e n3]

                              Iff-And, 250

 

                        252  (t,u,v) e n3 => t e n & u e n & v e n

                              Split, 251

 

                        253  t e n & u e n & v e n => (t,u,v) e n3

                              Split, 251

 

                        254  t e n & u e n & v e n

                              Detach, 252, 246

 

                        255  t e n

                              Split, 254

 

                        256  u e n

                              Split, 254

 

                        257  v e n

                              Split, 254

 

                        258  ALL(b):ALL(c):[(t,b,c) e q

                        <=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]

                              U Spec, 154

 

                        259  ALL(c):[(t,u+1,c) e q

                        <=> (t,u+1,c) e n3 & ~[t=0 & u+1=0 & c=z]]

                              U Spec, 258

 

                        260  (t,u+1,v*t) e q

                        <=> (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]

                              U Spec, 259

 

                        261  [(t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]]

                        & [(t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q]

                              Iff-And, 260

 

                        262  (t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]

                              Split, 261

 

                        263  (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q

                              Split, 261

 

                        264  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                              U Spec, 18

 

                        265  ALL(c3):[(t,u+1,c3) e n3 <=> t e n & u+1 e n & c3 e n]

                              U Spec, 264

 

                        266  (t,u+1,v*t) e n3 <=> t e n & u+1 e n & v*t e n

                              U Spec, 265

 

                        267  [(t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n]

                        & [t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3]

                              Iff-And, 266

 

                        268  (t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n

                              Split, 267

 

                        269  t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3

                              Split, 267

 

                        270  ALL(b):[u e n & b e n => u+b e n]

                              U Spec, 2

 

                        271  u e n & 1 e n => u+1 e n

                              U Spec, 270

 

                        272  u e n & 1 e n

                              Join, 256, 5

 

                        273  u+1 e n

                              Detach, 271, 272

 

                        274  ALL(b):[v e n & b e n => v*b e n]

                              U Spec, 3

 

                        275  v e n & t e n => v*t e n

                              U Spec, 274

 

                        276  v e n & t e n

                              Join, 257, 255

 

                        277  v*t e n

                              Detach, 275, 276

 

                        278  t e n & u+1 e n

                              Join, 255, 273

 

                        279  t e n & u+1 e n & v*t e n

                              Join, 278, 277

 

                        280  (t,u+1,v*t) e n3

                              Detach, 269, 279

 

                              281  t=0 & u+1=0 & v*t=z

                                    Premise

 

                              282  t=0

                                    Split, 281

 

                              283  u+1=0

                                    Split, 281

 

                              284  v*t=z

                                    Split, 281

 

                              285  u e n => ~u+1=0

                                    U Spec, 8

 

                              286  ~u+1=0

                                    Detach, 285, 256

 

                              287  u+1=0 & ~u+1=0

                                    Join, 283, 286

 

                        288  ~[t=0 & u+1=0 & v*t=z]

                              4 Conclusion, 281

 

                        289  (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]

                              Join, 280, 288

 

                        290  (t,u+1,v*t) e q

                              Detach, 263, 289

 

              As Required:

 

                  291  ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                        4 Conclusion, 238

 

                  292  q e pn3 & (0,0,x0) e q

                        Join, 170, 194

 

                  293  q e pn3 & (0,0,x0) e q

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                        Join, 292, 237

 

                  294  q e pn3 & (0,0,x0) e q

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                        Join, 293, 291

 

                  295  q e pn3 & (0,0,x0) e q

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                   & ~(0,0,z) e q

                        Join, 294, 210

 

                  296  EXIST(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   & ~(0,0,z) e d]

                        E Gen, 295

 

                  297  ~(0,0,z) e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d

                   & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                   & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                   & ~(0,0,z) e d]

                        Arb Or, 296

 

                  298  ~(0,0,z) e pow

                        Detach, 150, 297

 

                  299  (0,0,z) e pow & ~(0,0,z) e pow

                        Join, 136, 298

 

          As Required:

 

            300  ~[(0,0,z) e pow & ~z=x0]

                  4 Conclusion, 135

 

            301  ~~[(0,0,z) e pow => ~~z=x0]

                  Imply-And, 300

 

            302  (0,0,z) e pow => ~~z=x0

                  Rem DNeg, 301

 

            303  (0,0,z) e pow => z=x0

                  Rem DNeg, 302

 

     As Required:

 

      304  ALL(a):[a e n => [(0,0,a) e pow => a=x0]]

            4 Conclusion, 134

 

         

          Prove: ALL(a):[a e n

                 => [~a=0 => ALL(b):[b e n => [(a,0,b) e pow => b=1]]]]

         

          Suppose...

 

            305  x e n

                  Premise

 

             

               Prove: ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]

             

              Suppose...

 

                  306  ~x=0

                        Premise

 

                  

                   Prove: ALL(b):[b e n => [(x,0,b) e pow => b=1]]

                  

                   Suppose...

 

                        307  z e n

                              Premise

 

                       

                        Prove: ~[(x,0,z) e pow & ~z=1]

                       

                        Suppose to the contrary...

 

                              308  (x,0,z) e pow & ~z=1

                                    Premise

 

                              309  (x,0,z) e pow

                                    Split, 308

 

                              310  ~z=1

                                    Split, 308

 

                              311  ALL(b):ALL(c):[(x,b,c) e pow

                             <=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,b,c) e d]]

                                    U Spec, 29

 

                              312  ALL(c):[(x,0,c) e pow

                             <=> (x,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,c) e d]]

                                    U Spec, 311

 

                              313  (x,0,z) e pow

                             <=> (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]

                                    U Spec, 312

 

                              314  [(x,0,z) e pow => (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]]

                             & [(x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d] => (x,0,z) e pow]

                                    Iff-And, 313

 

                              315  (x,0,z) e pow => (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]

                                    Split, 314

 

                              316  (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d] => (x,0,z) e pow

                                    Split, 314

 

                              317  (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]

                                    Detach, 315, 309

 

                              318  (x,0,z) e n3

                                    Split, 317

 

                              319  ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]

                                    Split, 317

 

                              320  ALL(b):ALL(c):[(x,b,c) e pow

                             <=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,b,c) e d]]

                                    U Spec, 29

 

                              321  ALL(c):[(x,0,c) e pow

                             <=> (x,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,c) e d]]

                                    U Spec, 320

 

                              322  (x,0,z) e pow

                             <=> (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]

                                    U Spec, 321

 

                              323  [(x,0,z) e pow => (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]]

                             & [(x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d] => (x,0,z) e pow]

                                    Iff-And, 322

 

                              324  (x,0,z) e pow => (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]

                                    Split, 323

 

                              325  (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d] => (x,0,z) e pow

                                    Split, 323

 

                              326  ~[(x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]] => ~(x,0,z) e pow

                                    Contra, 324

 

                              327  ~~[~(x,0,z) e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d]] => ~(x,0,z) e pow

                                    DeMorgan, 326

 

                              328  ~(x,0,z) e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,0,z) e d] => ~(x,0,z) e pow

                                    Rem DNeg, 327

 

                              329  ~(x,0,z) e n3 | ~ALL(d):~[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e pow

                                    Imply-And, 328

 

                              330  ~(x,0,z) e n3 | ~~EXIST(d):~~[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e pow

                                    Quant, 329

 

                              331  ~(x,0,z) e n3 | EXIST(d):~~[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e pow

                                    Rem DNeg, 330

 

                        Sufficient: ~(x,0,z) e pow  (to obtain contradiction)

 

                              332  ~(x,0,z) e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e pow

                                    Rem DNeg, 331

 

                              333  EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

                             <=> (a,b,c) e n3 & ~[a=x & b=0 & c=z]]]

                                    Subset, 17

 

                              334  Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                             <=> (a,b,c) e n3 & ~[a=x & b=0 & c=z]]

                                    E Spec, 333

 

                       

                        Define: q

                        *********

 

                              335  Set''(q)

                                    Split, 334

 

                              336  ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                             <=> (a,b,c) e n3 & ~[a=x & b=0 & c=z]]

                                    Split, 334

 

                              337  q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                                    U Spec, 24

 

                              338  [q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]]

                             & [Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]

                                    Iff-And, 337

 

                              339  q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                                    Split, 338

 

                              340  Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3

                                    Split, 338

 

                                    341  (t,u,v) e q

                                          Premise

 

                                    342  ALL(b):ALL(c):[(t,b,c) e q

                                  <=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]

                                          U Spec, 336

 

                                    343  ALL(c):[(t,u,c) e q

                                  <=> (t,u,c) e n3 & ~[t=x & u=0 & c=z]]

                                          U Spec, 342

 

                                    344  (t,u,v) e q

                                  <=> (t,u,v) e n3 & ~[t=x & u=0 & v=z]

                                          U Spec, 343

 

                                    345  [(t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]]

                                  & [(t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q]

                                          Iff-And, 344

 

                                    346  (t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]

                                          Split, 345

 

                                    347  (t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q

                                          Split, 345

 

                                    348  (t,u,v) e n3 & ~[t=x & u=0 & v=z]

                                          Detach, 346, 341

 

                                    349  (t,u,v) e n3

                                          Split, 348

 

                              350  ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                                    4 Conclusion, 341

 

                              351  Set''(q)

                             & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                                    Join, 335, 350

 

                              352  q e pn3

                                    Detach, 340, 351

 

                              353  ALL(b):ALL(c):[(x,b,c) e q

                             <=> (x,b,c) e n3 & ~[x=x & b=0 & c=z]]

                                    U Spec, 336

 

                              354  ALL(c):[(x,0,c) e q

                             <=> (x,0,c) e n3 & ~[x=x & 0=0 & c=z]]

                                    U Spec, 353

 

                              355  (x,0,z) e q

                             <=> (x,0,z) e n3 & ~[x=x & 0=0 & z=z]

                                    U Spec, 354

 

                              356  [(x,0,z) e q => (x,0,z) e n3 & ~[x=x & 0=0 & z=z]]

                             & [(x,0,z) e n3 & ~[x=x & 0=0 & z=z] => (x,0,z) e q]

                                    Iff-And, 355

 

                              357  (x,0,z) e q => (x,0,z) e n3 & ~[x=x & 0=0 & z=z]

                                    Split, 356

 

                              358  (x,0,z) e n3 & ~[x=x & 0=0 & z=z] => (x,0,z) e q

                                    Split, 356

 

                              359  ~[(x,0,z) e n3 & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e q

                                    Contra, 357

 

                              360  ~~[~(x,0,z) e n3 | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e q

                                    DeMorgan, 359

 

                              361  ~(x,0,z) e n3 | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e q

                                    Rem DNeg, 360

 

                              362  ~(x,0,z) e n3 | x=x & 0=0 & z=z => ~(x,0,z) e q

                                    Rem DNeg, 361

 

                              363  x=x

                                    Reflex

 

                              364  0=0

                                    Reflex

 

                              365  z=z

                                    Reflex

 

                              366  x=x & 0=0

                                    Join, 363, 364

 

                              367  x=x & 0=0 & z=z

                                    Join, 366, 365

 

                              368  ~(x,0,z) e n3 | x=x & 0=0 & z=z

                                    Arb Or, 367

 

                        As Required:

 

                              369  ~(x,0,z) e q

                                    Detach, 362, 368

 

                                    370  t e n

                                          Premise

 

                                          371  ~t=0

                                                Premise

 

                                          372  ALL(b):ALL(c):[(t,b,c) e q

                                      <=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]

                                                U Spec, 336

 

                                          373  ALL(c):[(t,0,c) e q

                                      <=> (t,0,c) e n3 & ~[t=x & 0=0 & c=z]]

                                                U Spec, 372

 

                                          374  (t,0,1) e q

                                      <=> (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]

                                                U Spec, 373

 

                                          375  [(t,0,1) e q => (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]]

                                      & [(t,0,1) e n3 & ~[t=x & 0=0 & 1=z] => (t,0,1) e q]

                                                Iff-And, 374

 

                                          376  (t,0,1) e q => (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]

                                                Split, 375

 

                                  Sufficient: (t,0,1) e q

 

                                          377  (t,0,1) e n3 & ~[t=x & 0=0 & 1=z] => (t,0,1) e q

                                                Split, 375

 

                                          378  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                                                U Spec, 18

 

                                          379  ALL(c3):[(t,0,c3) e n3 <=> t e n & 0 e n & c3 e n]

                                                U Spec, 378

 

                                          380  (t,0,1) e n3 <=> t e n & 0 e n & 1 e n

                                                U Spec, 379

 

                                          381  [(t,0,1) e n3 => t e n & 0 e n & 1 e n]

                                      & [t e n & 0 e n & 1 e n => (t,0,1) e n3]

                                                Iff-And, 380

 

                                          382  (t,0,1) e n3 => t e n & 0 e n & 1 e n

                                                Split, 381

 

                                          383  t e n & 0 e n & 1 e n => (t,0,1) e n3

                                                Split, 381

 

                                          384  t e n & 0 e n

                                                Join, 370, 4

 

                                          385  t e n & 0 e n & 1 e n

                                                Join, 384, 5

 

                                          386  (t,0,1) e n3

                                                Detach, 383, 385

 

                                                387  t=x & 0=0 & 1=z

                                                      Premise

 

                                                388  t=x

                                                      Split, 387

 

                                                389  0=0

                                                      Split, 387

 

                                                390  1=z

                                                      Split, 387

 

                                                391  z=1

                                                      Sym, 390

 

                                                392  z=1 & ~z=1

                                                      Join, 391, 310

 

                                          393  ~[t=x & 0=0 & 1=z]

                                                4 Conclusion, 387

 

                                          394  (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]

                                                Join, 386, 393

 

                                          395  (t,0,1) e q

                                                Detach, 377, 394

 

                                    396  ~t=0 => (t,0,1) e q

                                          4 Conclusion, 371

 

                        As Required:

 

                              397  ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                                    4 Conclusion, 370

 

                            

                             Suppose...

 

                                    398  (t,u,v) e q

                                          Premise

 

                                    399  ALL(b):ALL(c):[(t,b,c) e q

                                  <=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]

                                          U Spec, 336

 

                                    400  ALL(c):[(t,u,c) e q

                                  <=> (t,u,c) e n3 & ~[t=x & u=0 & c=z]]

                                          U Spec, 399

 

                                    401  (t,u,v) e q

                                  <=> (t,u,v) e n3 & ~[t=x & u=0 & v=z]

                                          U Spec, 400

 

                                    402  [(t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]]

                                  & [(t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q]

                                          Iff-And, 401

 

                                    403  (t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]

                                          Split, 402

 

                                    404  (t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q

                                          Split, 402

 

                                    405  (t,u,v) e n3 & ~[t=x & u=0 & v=z]

                                          Detach, 403, 398

 

                                    406  (t,u,v) e n3

                                          Split, 405

 

                                    407  ~[t=x & u=0 & v=z]

                                          Split, 405

 

                                    408  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                                          U Spec, 18

 

                                    409  ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]

                                          U Spec, 408

 

                                    410  (t,u,v) e n3 <=> t e n & u e n & v e n

                                          U Spec, 409

 

                                    411  [(t,u,v) e n3 => t e n & u e n & v e n]

                                  & [t e n & u e n & v e n => (t,u,v) e n3]

                                          Iff-And, 410

 

                                    412  (t,u,v) e n3 => t e n & u e n & v e n

                                          Split, 411

 

                                    413  t e n & u e n & v e n => (t,u,v) e n3

                                          Split, 411

 

                                    414  t e n & u e n & v e n

                                          Detach, 412, 406

 

                                    415  t e n

                                          Split, 414

 

                                    416  u e n

                                          Split, 414

 

                                    417  v e n

                                          Split, 414

 

                                    418  ALL(b):ALL(c):[(t,b,c) e q

                                  <=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]

                                          U Spec, 336

 

                                    419  ALL(c):[(t,u+1,c) e q

                                  <=> (t,u+1,c) e n3 & ~[t=x & u+1=0 & c=z]]

                                          U Spec, 418

 

                                    420  (t,u+1,v*t) e q

                                  <=> (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]

                                          U Spec, 419

 

                                    421  [(t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]]

                                  & [(t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q]

                                          Iff-And, 420

 

                                    422  (t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]

                                          Split, 421

 

                             Sufficient: (t,u+1,v*t) e q

 

                                    423  (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q

                                          Split, 421

 

                                    424  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                                          U Spec, 18

 

                                    425  ALL(c3):[(t,u+1,c3) e n3 <=> t e n & u+1 e n & c3 e n]

                                          U Spec, 424

 

                                    426  (t,u+1,v*t) e n3 <=> t e n & u+1 e n & v*t e n

                                          U Spec, 425

 

                                    427  [(t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n]

                                  & [t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3]

                                          Iff-And, 426

 

                                    428  (t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n

                                          Split, 427

 

                                    429  t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3

                                          Split, 427

 

                                    430  ALL(b):[u e n & b e n => u+b e n]

                                          U Spec, 2

 

                                    431  u e n & 1 e n => u+1 e n

                                          U Spec, 430

 

                                    432  u e n & 1 e n

                                          Join, 416, 5

 

                                    433  u+1 e n

                                          Detach, 431, 432

 

                                    434  ALL(b):[v e n & b e n => v*b e n]

                                          U Spec, 3

 

                                    435  v e n & t e n => v*t e n

                                          U Spec, 434

 

                                    436  v e n & t e n

                                          Join, 417, 415

 

                                    437  v*t e n

                                          Detach, 435, 436

 

                                    438  t e n & u+1 e n

                                          Join, 415, 433

 

                                    439  t e n & u+1 e n & v*t e n

                                          Join, 438, 437

 

                                    440  (t,u+1,v*t) e n3

                                          Detach, 429, 439

 

                                          441  t=x & u+1=0 & v*t=z

                                                Premise

 

                                          442  t=x

                                                Split, 441

 

                                          443  u+1=0

                                                Split, 441

 

                                          444  v*t=z

                                                Split, 441

 

                                          445  u e n => ~u+1=0

                                                U Spec, 8

 

                                          446  ~u+1=0

                                                Detach, 445, 416

 

                                          447  u+1=0 & ~u+1=0

                                                Join, 443, 446

 

                                    448  ~[t=x & u+1=0 & v*t=z]

                                          4 Conclusion, 441

 

                                    449  (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]

                                          Join, 440, 448

 

                                    450  (t,u+1,v*t) e q

                                          Detach, 423, 449

 

                        As Required:

 

                              451  ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                                    4 Conclusion, 398

 

                              452  ALL(b):ALL(c):[(0,b,c) e q

                             <=> (0,b,c) e n3 & ~[0=x & b=0 & c=z]]

                                    U Spec, 336

 

                              453  ALL(c):[(0,0,c) e q

                             <=> (0,0,c) e n3 & ~[0=x & 0=0 & c=z]]

                                    U Spec, 452

 

                              454  (0,0,x0) e q

                             <=> (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]

                                    U Spec, 453

 

                              455  [(0,0,x0) e q => (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]]

                             & [(0,0,x0) e n3 & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q]

                                    Iff-And, 454

 

                              456  (0,0,x0) e q => (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]

                                    Split, 455

 

                              457  (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q

                                    Split, 455

 

                              458  ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]

                                    U Spec, 18

 

                              459  ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]

                                    U Spec, 458

 

                              460  (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n

                                    U Spec, 459

 

                              461  [(0,0,x0) e n3 => 0 e n & 0 e n & x0 e n]

                             & [0 e n & 0 e n & x0 e n => (0,0,x0) e n3]

                                    Iff-And, 460

 

                              462  (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n

                                    Split, 461

 

                              463  0 e n & 0 e n & x0 e n => (0,0,x0) e n3

                                    Split, 461

 

                              464  0 e n & 0 e n

                                    Join, 4, 4

 

                              465  0 e n & 0 e n & x0 e n

                                    Join, 464, 25

 

                              466  (0,0,x0) e n3

                                    Detach, 463, 465

 

                                    467  0=x & 0=0 & x0=z

                                          Premise

 

                                    468  0=x

                                          Split, 467

 

                                    469  0=0

                                          Split, 467

 

                                    470  x0=z

                                          Split, 467

 

                                    471  x=0

                                          Sym, 468

 

                                    472  x=0 & ~x=0

                                          Join, 471, 306

 

                              473  ~[0=x & 0=0 & x0=z]

                                    4 Conclusion, 467

 

                              474  (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]

                                    Join, 466, 473

 

                        As Required:

 

                              475  (0,0,x0) e q

                                    Detach, 457, 474

 

                              476  q e pn3 & (0,0,x0) e q

                                    Join, 352, 475

 

                              477  q e pn3 & (0,0,x0) e q

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                                    Join, 476, 397

 

                              478  q e pn3 & (0,0,x0) e q

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                                    Join, 477, 451

 

                              479  q e pn3 & (0,0,x0) e q

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                             & ~(x,0,z) e q

                                    Join, 478, 369

 

                              480  EXIST(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             & ~(x,0,z) e d]

                                    E Gen, 479

 

                              481  ~(x,0,z) e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             & ~(x,0,z) e d]

                                    Arb Or, 480

 

                              482  ~(x,0,z) e pow

                                    Detach, 332, 481

 

                              483  (x,0,z) e pow & ~(x,0,z) e pow

                                    Join, 309, 482

 

                   As Required:

 

                        484  ~[(x,0,z) e pow & ~z=1]

                              4 Conclusion, 308

 

                        485  ~~[(x,0,z) e pow => ~~z=1]

                              Imply-And, 484

 

                        486  (x,0,z) e pow => ~~z=1

                              Rem DNeg, 485

 

                        487  (x,0,z) e pow => z=1

                              Rem DNeg, 486

 

              As Required:

 

                  488  ALL(b):[b e n => [(x,0,b) e pow => b=1]]

                        4 Conclusion, 307

 

          As Required:

 

            489  ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]

                  4 Conclusion, 306

 

     As Required:

 

      490  ALL(a):[a e n

          => [~a=0 => ALL(b):[b e n => [(a,0,b) e pow => b=1]]]]

            4 Conclusion, 305

 

     Prove: pow is a function

    

     Apply Function Axiom

 

      491      ALL(f):ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => c1 e a1 & c2 e a2 & d e b]

          & ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e f]]

          & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e f & (c1,c2,d2) e f => d1=d2]

          => ALL(c1):ALL(c2):ALL(d):[d=f(c1,c2) <=> (c1,c2,d) e f]]

            Function

 

      492  ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e a1 & c2 e a2 & d e b]

          & ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e pow]]

          & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]

          => ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]]

            U Spec, 491

 

      493  ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e a2 & d e b]

          & ALL(c1):ALL(c2):[c1 e n & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e pow]]

          & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]

          => ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]]

            U Spec, 492

 

      494  ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e b]

          & ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e b & (c1,c2,d) e pow]]

          & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]

          => ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]]

            U Spec, 493

 

    

     Sufficient: For functionality of pow

 

      495  ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]

          & ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e n & (c1,c2,d) e pow]]

          & ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]

          => ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]

            U Spec, 494

 

         

          Prove: ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]

         

          Suppose...

 

            496  (x,y,z) e pow

                  Premise

 

            497  ALL(b):ALL(c):[(x,b,c) e pow

              <=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,b,c) e d]]

                  U Spec, 29

 

            498  ALL(c):[(x,y,c) e pow

              <=> (x,y,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,c) e d]]

                  U Spec, 497

 

            499  (x,y,z) e pow

              <=> (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z) e d]

                  U Spec, 498

 

            500  [(x,y,z) e pow => (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z) e d]]

              & [(x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z) e d] => (x,y,z) e pow]

                  Iff-And, 499

 

            501  (x,y,z) e pow => (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z) e d]

                  Split, 500

 

            502  (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z) e d] => (x,y,z) e pow

                  Split, 500

 

            503  (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z) e d]

                  Detach, 501, 496

 

            504  (x,y,z) e n3

                  Split, 503

 

            505  ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z) e d]

                  Split, 503

 

            506  ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                  U Spec, 18

 

            507  ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

                  U Spec, 506

 

            508  (x,y,z) e n3 <=> x e n & y e n & z e n

                  U Spec, 507

 

            509  [(x,y,z) e n3 => x e n & y e n & z e n]

              & [x e n & y e n & z e n => (x,y,z) e n3]

                  Iff-And, 508

 

            510  (x,y,z) e n3 => x e n & y e n & z e n

                  Split, 509

 

            511  x e n & y e n & z e n => (x,y,z) e n3

                  Split, 509

 

            512  x e n & y e n & z e n

                  Detach, 510, 504

 

     Functionality of pow, Part 1

 

      513  ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]

            4 Conclusion, 496

 

         

          Prove: ALL(a):[a e n

                 => ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e pow]]]

         

          Suppose...

 

            514  x e n

                  Premise

 

            515  EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]]

                  Subset, 1

 

            516  Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]

                  E Spec, 515

 

         

          Define: p1

          **********

 

            517  Set(p1)

                  Split, 516

 

            518  ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]

                  Split, 516

 

            519  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, 6

 

             

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

             

              Suppose...

 

                  520  y e p1

                        Premise

 

                  521  y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        U Spec, 518

 

                  522  [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]]

                   & [y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1]

                        Iff-And, 521

 

                  523  y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        Split, 522

 

                  524  y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1

                        Split, 522

 

                  525  y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        Detach, 523, 520

 

                  526  y e n

                        Split, 525

 

          As Required:

 

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

                  4 Conclusion, 520

 

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

                  Join, 517, 527

 

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

 

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

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

                  Detach, 519, 528

 

            530  0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e pow]

                  U Spec, 518

 

            531  [0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e pow]]

              & [0 e n & EXIST(c):[c e n & (x,0,c) e pow] => 0 e p1]

                  Iff-And, 530

 

            532  0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e pow]

                  Split, 531

 

            533  0 e n & EXIST(c):[c e n & (x,0,c) e pow] => 0 e p1

                  Split, 531

 

          2 Cases:

 

            534  x=0 | ~x=0

                  Or Not

 

             

              Prove: x=0 => 0 e p1

             

              Suppose...

 

                  535  x=0

                        Premise

 

                  536  (x,0,x0) e pow

                        Substitute, 535, 50

 

                  537  x0 e n & (x,0,x0) e pow

                        Join, 25, 536

 

                  538  EXIST(c):[c e n & (x,0,c) e pow]

                        E Gen, 537

 

                  539  0 e n & EXIST(c):[c e n & (x,0,c) e pow]

                        Join, 4, 538

 

                  540  0 e p1

                        Detach, 533, 539

 

          As Required:

 

            541  x=0 => 0 e p1

                  4 Conclusion, 535

 

             

              Prove: ~x=0 => 0 e p1

             

              Suppose...

 

                  542  ~x=0

                        Premise

 

                  543  x e n => [~x=0 => (x,0,1) e pow]

                        U Spec, 80

 

                  544  ~x=0 => (x,0,1) e pow

                        Detach, 543, 514

 

                  545  (x,0,1) e pow

                        Detach, 544, 542

 

                  546  1 e n & (x,0,1) e pow

                        Join, 5, 545

 

                  547  EXIST(c):[c e n & (x,0,c) e pow]

                        E Gen, 546

 

                  548  0 e n & EXIST(c):[c e n & (x,0,c) e pow]

                        Join, 4, 547

 

                  549  0 e p1

                        Detach, 533, 548

 

          As Required:

 

            550  ~x=0 => 0 e p1

                  4 Conclusion, 542

 

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

                  Join, 541, 550

 

          As Required:

 

            552  0 e p1

                  Cases, 534, 551

 

             

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

             

              Suppose...

 

                  553  y e p1

                        Premise

 

                  554  y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        U Spec, 518

 

                  555  [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]]

                   & [y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1]

                        Iff-And, 554

 

                  556  y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        Split, 555

 

                  557  y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1

                        Split, 555

 

                  558  y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        Detach, 556, 553

 

                  559  y e n

                        Split, 558

 

                  560  EXIST(c):[c e n & (x,y,c) e pow]

                        Split, 558

 

                  561  z e n & (x,y,z) e pow

                        E Spec, 560

 

                  562  z e n

                        Split, 561

 

                  563  (x,y,z) e pow

                        Split, 561

 

                  564  y+1 e p1 <=> y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]

                        U Spec, 518

 

                  565  [y+1 e p1 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]]

                   & [y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow] => y+1 e p1]

                        Iff-And, 564

 

                  566  y+1 e p1 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]

                        Split, 565

 

              Sufficient: y+1 e p1

 

                  567  y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow] => y+1 e p1

                        Split, 565

 

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

                        U Spec, 2

 

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

                        U Spec, 568

 

                  570  y e n & 1 e n

                        Join, 559, 5

 

                  571  y+1 e n

                        Detach, 569, 570

 

                  572  ALL(b):ALL(c):[x e n & b e n & c e n

                   => [(x,b,c) e pow => (x,b+1,c*x) e pow]]

                        U Spec, 133

 

                  573  ALL(c):[x e n & y e n & c e n

                   => [(x,y,c) e pow => (x,y+1,c*x) e pow]]

                        U Spec, 572

 

                  574  x e n & y e n & z e n

                   => [(x,y,z) e pow => (x,y+1,z*x) e pow]

                        U Spec, 573

 

                  575  x e n & y e n

                        Join, 514, 559

 

                  576  x e n & y e n & z e n

                        Join, 575, 562

 

                  577  (x,y,z) e pow => (x,y+1,z*x) e pow

                        Detach, 574, 576

 

                  578  (x,y+1,z*x) e pow

                        Detach, 577, 563

 

                  579  ALL(b):[z e n & b e n => z*b e n]

                        U Spec, 3

 

                  580  z e n & x e n => z*x e n

                        U Spec, 579

 

                  581  z e n & x e n

                        Join, 562, 514

 

                  582  z*x e n

                        Detach, 580, 581

 

                  583  z*x e n & (x,y+1,z*x) e pow

                        Join, 582, 578

 

                  584  EXIST(c):[c e n & (x,y+1,c) e pow]

                        E Gen, 583

 

                  585  y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]

                        Join, 571, 584

 

                  586  y+1 e p1

                        Detach, 567, 585

 

          As Required:

 

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

                  4 Conclusion, 553

 

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

                  Join, 552, 587

 

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

                  Detach, 529, 588

 

             

              Prove: ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]

             

              Suppose...

 

                  590  t e n

                        Premise

 

                  591  t e n => t e p1

                        U Spec, 589

 

                  592  t e p1

                        Detach, 591, 590

 

                  593  t e p1 <=> t e n & EXIST(c):[c e n & (x,t,c) e pow]

                        U Spec, 518

 

                  594  [t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e pow]]

                   & [t e n & EXIST(c):[c e n & (x,t,c) e pow] => t e p1]

                        Iff-And, 593

 

                  595  t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e pow]

                        Split, 594

 

                  596  t e n & EXIST(c):[c e n & (x,t,c) e pow] => t e p1

                        Split, 594

 

                  597  t e n & EXIST(c):[c e n & (x,t,c) e pow]

                        Detach, 595, 592

 

                  598  t e n

                        Split, 597

 

                  599  EXIST(c):[c e n & (x,t,c) e pow]

                        Split, 597

 

          As Required:

 

            600  ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  4 Conclusion, 590

 

     As Required:

 

      601  ALL(a):[a e n

          => ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e pow]]]

            4 Conclusion, 514

 

         

          Prove: ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]

         

          Suppose...

 

            602  x e n & y e n

                  Premise

 

            603  x e n

                  Split, 602

 

            604  y e n

                  Split, 602

 

            605  x e n

              => ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  U Spec, 601

 

            606  ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  Detach, 605, 603

 

            607  y e n => EXIST(c):[c e n & (x,y,c) e pow]

                  U Spec, 606

 

            608  EXIST(c):[c e n & (x,y,c) e pow]

                  Detach, 607, 604

 

     Functionality of pow, Part 2

 

      609  ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]

            4 Conclusion, 602

 

         

          Prove: ALL(a):[a e n

                 => ALL(b):[b e n

                 => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]]]]

         

          Suppose...

 

            610  x e n

                  Premise

 

            611  EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]]

                  Subset, 1

 

            612  Set(p2) & ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]

                  E Spec, 611

 

         

          Define: p2

          **********

 

            613  Set(p2)

                  Split, 612

 

            614  ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]

                  Split, 612

 

            615  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, 6

 

                  616  y e p2

                        Premise

 

                  617  y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        U Spec, 614

 

                  618  [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]]

                   & [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2]

                        Iff-And, 617

 

                  619  y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Split, 618

 

                  620  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2

                        Split, 618

 

                  621  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Detach, 619, 616

 

                  622  y e n

                        Split, 621

 

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

                  4 Conclusion, 616

 

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

                  Join, 613, 623

 

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

 

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

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

                  Detach, 615, 624

 

            626  0 e p2 <=> 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]

                  U Spec, 614

 

            627  [0 e p2 => 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]]

              & [0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]] => 0 e p2]

                  Iff-And, 626

 

            628  0 e p2 => 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]

                  Split, 627

 

          Sufficient: 0 e p2

 

            629  0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]] => 0 e p2

                  Split, 627

 

                  630  z1 e n & z2 e n

                        Premise

 

                  631  z1 e n

                        Split, 630

 

                  632  z2 e n

                        Split, 630

 

                        633  (x,0,z1) e pow & (x,0,z2) e pow

                              Premise

 

                        634  (x,0,z1) e pow

                              Split, 633

 

                        635  (x,0,z2) e pow

                              Split, 633

 

                   2 cases:

 

                        636  x=0 | ~x=0

                              Or Not

 

                              637  x=0

                                    Premise

 

                              638  z1 e n => [(0,0,z1) e pow => z1=x0]

                                    U Spec, 304

 

                              639  (0,0,z1) e pow => z1=x0

                                    Detach, 638, 631

 

                              640  (x,0,z1) e pow => z1=x0

                                    Substitute, 637, 639

 

                              641  z1=x0

                                    Detach, 640, 634

 

                              642  z2 e n => [(0,0,z2) e pow => z2=x0]

                                    U Spec, 304

 

                              643  (0,0,z2) e pow => z2=x0

                                    Detach, 642, 632

 

                              644  (x,0,z2) e pow => z2=x0

                                    Substitute, 637, 643

 

                              645  z2=x0

                                    Detach, 644, 635

 

                              646  z1=z2

                                    Substitute, 645, 641

 

                        647  x=0 => z1=z2

                              4 Conclusion, 637

 

                              648  ~x=0

                                    Premise

 

                              649  x e n

                             => [~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]]

                                    U Spec, 490

 

                              650  ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]

                                    Detach, 649, 610

 

                              651  ALL(b):[b e n => [(x,0,b) e pow => b=1]]

                                    Detach, 650, 648

 

                              652  z1 e n => [(x,0,z1) e pow => z1=1]

                                    U Spec, 651

 

                              653  (x,0,z1) e pow => z1=1

                                    Detach, 652, 631

 

                              654  z1=1

                                    Detach, 653, 634

 

                              655  z2 e n => [(x,0,z2) e pow => z2=1]

                                    U Spec, 651

 

                              656  (x,0,z2) e pow => z2=1

                                    Detach, 655, 632

 

                              657  z2=1

                                    Detach, 656, 635

 

                              658  z1=z2

                                    Substitute, 657, 654

 

                        659  ~x=0 => z1=z2

                              4 Conclusion, 648

 

                        660  [x=0 => z1=z2] & [~x=0 => z1=z2]

                              Join, 647, 659

 

                        661  z1=z2

                              Cases, 636, 660

 

                  662  (x,0,z1) e pow & (x,0,z2) e pow => z1=z2

                        4 Conclusion, 633

 

            663  ALL(c1):ALL(c2):[c1 e n & c2 e n

              => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]

                  4 Conclusion, 630

 

            664  0 e n

              & ALL(c1):ALL(c2):[c1 e n & c2 e n

              => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]

                  Join, 4, 663

 

          As Required:

 

            665  0 e p2

                  Detach, 629, 664

 

             

              Suppose...

 

                  666  y e p2

                        Premise

 

                  667  y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        U Spec, 614

 

                  668  [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]]

                   & [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2]

                        Iff-And, 667

 

                  669  y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Split, 668

 

                  670  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2

                        Split, 668

 

                  671  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Detach, 669, 666

 

                  672  y e n

                        Split, 671

 

                  673  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Split, 671

 

                  674  ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                        U Spec, 609

 

                  675  x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]

                        U Spec, 674

 

                  676  x e n & y e n

                        Join, 610, 672

 

                  677  EXIST(c):[c e n & (x,y,c) e pow]

                        Detach, 675, 676

 

                  678  z e n & (x,y,z) e pow

                        E Spec, 677

 

                  679  z e n

                        Split, 678

 

                  680  (x,y,z) e pow

                        Split, 678

 

                  681  ALL(c2):[z e n & c2 e n => [(x,y,z) e pow & (x,y,c2) e pow => z=c2]]

                        U Spec, 673

 

                        682  z' e n

                              Premise

 

                        683  z e n & z' e n => [(x,y,z) e pow & (x,y,z') e pow => z=z']

                              U Spec, 681

 

                        684  z e n & z' e n

                              Join, 679, 682

 

                        685  (x,y,z) e pow & (x,y,z') e pow => z=z'

                              Detach, 683, 684

 

                              686  (x,y,z') e pow

                                    Premise

 

                              687  (x,y,z) e pow & (x,y,z') e pow

                                    Join, 680, 686

 

                              688  z=z'

                                    Detach, 685, 687

 

                        689  (x,y,z') e pow => z=z'

                              4 Conclusion, 686

 

              z is unique

 

                  690  ALL(c):[c e n => [(x,y,c) e pow => z=c]]

                        4 Conclusion, 682

 

                  

                   Prove: ALL(a):[aen => [(x,y+1,a) => a=z*x]]

                    

                   Suppose...

 

                        691  z' e n

                              Premise

 

                       

                        Suppose to the contrary...

 

                              692  (x,y+1,z') e pow & ~z'=z*x

                                    Premise

 

                              693  (x,y+1,z') e pow

                                    Split, 692

 

                              694  ~z'=z*x

                                    Split, 692

 

                              695  ALL(b):ALL(c):[(x,b,c) e pow

                             <=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,b,c) e d]]

                                    U Spec, 29

 

                              696  ALL(c):[(x,y+1,c) e pow

                             <=> (x,y+1,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,c) e d]]

                                    U Spec, 695

 

                              697  (x,y+1,z') e pow

                             <=> (x,y+1,z') e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,z') e d]

                                    U Spec, 696

 

                              698  [(x,y+1,z') e pow => (x,y+1,z') e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,z') e d]]

                             & [(x,y+1,z') e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,z') e d] => (x,y+1,z') e pow]

                                    Iff-And, 697

 

                              699  (x,y+1,z') e pow => (x,y+1,z') e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,z') e d]

                                    Split, 698

 

                              700  (x,y+1,z') e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,z') e d] => (x,y+1,z') e pow

                                    Split, 698

 

                              701  ~[(x,y+1,z') e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,z') e d]] => ~(x,y+1,z') e pow

                                    Contra, 699

 

                              702  ~~[~(x,y+1,z') e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,z') e d]] => ~(x,y+1,z') e pow

                                    DeMorgan, 701

 

                              703  ~(x,y+1,z') e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             => (x,y+1,z') e d] => ~(x,y+1,z') e pow

                                    Rem DNeg, 702

 

                              704  ~(x,y+1,z') e n3 | ~ALL(d):~[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e pow

                                    Imply-And, 703

 

                              705  ~(x,y+1,z') e n3 | ~~EXIST(d):~~[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e pow

                                    Quant, 704

 

                              706  ~(x,y+1,z') e n3 | EXIST(d):~~[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e pow

                                    Rem DNeg, 705

 

                        Sufficient: ~(x,y+1,z') e pow   (to obtain a contradiction)

 

                              707  ~(x,y+1,z') e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e pow

                                    Rem DNeg, 706

 

                              708  EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub

                             <=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]]

                                    Subset, 28

 

                              709  Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                             <=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]

                                    E Spec, 708

 

                       

                        Define: q

                        *********

 

                              710  Set''(q)

                                    Split, 709

 

                              711  ALL(a):ALL(b):ALL(c):[(a,b,c) e q

                             <=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]

                                    Split, 709

 

                              712  q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                                    U Spec, 24

 

                              713  [q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]]

                             & [Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]

                                    Iff-And, 712

 

                              714  q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]

                                    Split, 713

 

                        Sufficient: q e pn3

 

                              715  Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3

                                    Split, 713

 

                            

                             Suppose...

 

                                    716  (t,u,v) e q

                                          Premise

 

                                    717  ALL(b):ALL(c):[(t,b,c) e q

                                  <=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 711

 

                                    718  ALL(c):[(t,u,c) e q

                                  <=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]

                                          U Spec, 717

 

                                    719  (t,u,v) e q

                                  <=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          U Spec, 718

 

                                    720  [(t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']]

                                  & [(t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]

                                          Iff-And, 719

 

                                    721  (t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          Split, 720

 

                                    722  (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q

                                          Split, 720

 

                                    723  (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          Detach, 721, 716

 

                                    724  (t,u,v) e pow

                                          Split, 723

 

                                    725  ~[t=x & u=y+1 & v=z']

                                          Split, 723

 

                                    726  ALL(b):ALL(c):[(t,b,c) e pow

                                  <=> (t,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,b,c) e d]]

                                          U Spec, 29

 

                                    727  ALL(c):[(t,u,c) e pow

                                  <=> (t,u,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,c) e d]]

                                          U Spec, 726

 

                                    728  (t,u,v) e pow

                                  <=> (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]

                                          U Spec, 727

 

                                    729  [(t,u,v) e pow => (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]]

                                  & [(t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d] => (t,u,v) e pow]

                                          Iff-And, 728

 

                                    730  (t,u,v) e pow => (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]

                                          Split, 729

 

                                    731  (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                 & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d] => (t,u,v) e pow

                                          Split, 729

 

                                    732  (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]

                                          Detach, 730, 724

 

                                    733  (t,u,v) e n3

                                          Split, 732

 

                              734  ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]

                                    4 Conclusion, 716

 

                              735  Set''(q)

                             & ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]

                                    Join, 710, 734

 

                        As Required:

 

                              736  q e pn3

                                    Detach, 715, 735

 

                              737  ALL(b):ALL(c):[(0,b,c) e q

                             <=> (0,b,c) e pow & ~[0=x & b=y+1 & c=z']]

                                    U Spec, 711

 

                              738  ALL(c):[(0,0,c) e q

                             <=> (0,0,c) e pow & ~[0=x & 0=y+1 & c=z']]

                                    U Spec, 737

 

                              739  (0,0,x0) e q

                             <=> (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']

                                    U Spec, 738

 

                              740  [(0,0,x0) e q => (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']]

                             & [(0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q]

                                    Iff-And, 739

 

                              741  (0,0,x0) e q => (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']

                                    Split, 740

 

                              742  (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q

                                    Split, 740

 

                                    743  0=x & 0=y+1 & x0=z'

                                          Premise

 

                                    744  0=x

                                          Split, 743

 

                                    745  0=y+1

                                          Split, 743

 

                                    746  x0=z'

                                          Split, 743

 

                                    747  y e n => ~y+1=0

                                          U Spec, 8

 

                                    748  ~y+1=0

                                          Detach, 747, 672

 

                                    749  y+1=0

                                          Sym, 745

 

                                    750  y+1=0 & ~y+1=0

                                          Join, 749, 748

 

                              751  ~[0=x & 0=y+1 & x0=z']

                                    4 Conclusion, 743

 

                              752  (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']

                                    Join, 50, 751

 

                        As Required:

 

                              753  (0,0,x0) e q

                                    Detach, 742, 752

 

                              754  ALL(b):ALL(c):[(x,b,c) e q

                             <=> (x,b,c) e pow & ~[x=x & b=y+1 & c=z']]

                                    U Spec, 711

 

                              755  ALL(c):[(x,y+1,c) e q

                             <=> (x,y+1,c) e pow & ~[x=x & y+1=y+1 & c=z']]

                                    U Spec, 754

 

                              756  (x,y+1,z') e q

                             <=> (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']

                                    U Spec, 755

 

                              757  [(x,y+1,z') e q => (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']]

                             & [(x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q]

                                    Iff-And, 756

 

                              758  (x,y+1,z') e q => (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']

                                    Split, 757

 

                              759  (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q

                                    Split, 757

 

                              760  ~[(x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q

                                    Contra, 758

 

                              761  ~~[~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q

                                    DeMorgan, 760

 

                              762  ~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z'] => ~(x,y+1,z') e q

                                    Rem DNeg, 761

 

                              763  ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z' => ~(x,y+1,z') e q

                                    Rem DNeg, 762

 

                              764  x=x

                                    Reflex

 

                              765  y+1=y+1

                                    Reflex

 

                              766  z'=z'

                                    Reflex

 

                              767  x=x & y+1=y+1

                                    Join, 764, 765

 

                              768  x=x & y+1=y+1 & z'=z'

                                    Join, 767, 766

 

                              769  ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z'

                                    Arb Or, 768

 

                        As Required:

 

                              770  ~(x,y+1,z') e q

                                    Detach, 763, 769

 

                            

                             Suppose...

 

                                    771  (t,u,v) e q

                                          Premise

 

                                    772  ALL(b):ALL(c):[(t,b,c) e q

                                  <=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 711

 

                                    773  ALL(c):[(t,u,c) e q

                                  <=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]

                                          U Spec, 772

 

                                    774  (t,u,v) e q

                                  <=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          U Spec, 773

 

                                    775  [(t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']]

                                  & [(t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]

                                          Iff-And, 774

 

                                    776  (t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          Split, 775

 

                                    777  (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q

                                          Split, 775

 

                                    778  (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          Detach, 776, 771

 

                                    779  (t,u,v) e pow

                                          Split, 778

 

                                    780  ~[t=x & u=y+1 & v=z']

                                          Split, 778

 

                                    781  ALL(b):ALL(c):[(t,b,c) e pow

                                  <=> (t,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,b,c) e d]]

                                          U Spec, 29

 

                                    782  ALL(c):[(t,u,c) e pow

                                  <=> (t,u,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,c) e d]]

                                          U Spec, 781

 

                                    783  (t,u,v) e pow

                                  <=> (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]

                                          U Spec, 782

 

                                    784  [(t,u,v) e pow => (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]]

                                  & [(t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d] => (t,u,v) e pow]

                                          Iff-And, 783

 

                                    785  (t,u,v) e pow => (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]

                                          Split, 784

 

                                    786  (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d] => (t,u,v) e pow

                                          Split, 784

 

                                    787  (t,u,v) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]

                                          Detach, 785, 779

 

                                    788  (t,u,v) e n3

                                          Split, 787

 

                                    789  ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]

                                          U Spec, 18

 

                                    790  ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]

                                          U Spec, 789

 

                                    791  (t,u,v) e n3 <=> t e n & u e n & v e n

                                          U Spec, 790

 

                                    792  [(t,u,v) e n3 => t e n & u e n & v e n]

                                  & [t e n & u e n & v e n => (t,u,v) e n3]

                                          Iff-And, 791

 

                                    793  (t,u,v) e n3 => t e n & u e n & v e n

                                          Split, 792

 

                                    794  t e n & u e n & v e n => (t,u,v) e n3

                                          Split, 792

 

                                    795  t e n & u e n & v e n

                                          Detach, 793, 788

 

                                    796  t e n

                                          Split, 795

 

                                    797  u e n

                                          Split, 795

 

                                    798  v e n

                                          Split, 795

 

                                    799  ALL(d):[d e pn3 & (0,0,x0) e d

                                  & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                                  & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                                  => (t,u,v) e d]

                                          Split, 787

 

                                    800  ALL(b):ALL(c):[(t,b,c) e q

                                  <=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 711

 

                                    801  ALL(c):[(t,u+1,c) e q

                                  <=> (t,u+1,c) e pow & ~[t=x & u+1=y+1 & c=z']]

                                          U Spec, 800

 

                                    802  (t,u+1,v*t) e q

                                  <=> (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']

                                          U Spec, 801

 

                                    803  [(t,u+1,v*t) e q => (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']]

                                  & [(t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q]

                                          Iff-And, 802

 

                                    804  (t,u+1,v*t) e q => (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']

                                          Split, 803

 

                                    805  (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q

                                          Split, 803

 

                                    806  ALL(b):ALL(c):[t e n & b e n & c e n

                                  => [(t,b,c) e pow => (t,b+1,c*t) e pow]]

                                          U Spec, 133

 

                                    807  ALL(c):[t e n & u e n & c e n

                                  => [(t,u,c) e pow => (t,u+1,c*t) e pow]]

                                          U Spec, 806

 

                                    808  t e n & u e n & v e n

                                  => [(t,u,v) e pow => (t,u+1,v*t) e pow]

                                          U Spec, 807

 

                                    809  (t,u,v) e pow => (t,u+1,v*t) e pow

                                          Detach, 808, 795

 

                                    810  (t,u+1,v*t) e pow

                                          Detach, 809, 779

 

                                 

                                  Suppose to the contrary...

 

                                          811  t=x & u+1=y+1 & v*t=z'

                                                Premise

 

                                          812  t=x

                                                Split, 811

 

                                          813  u+1=y+1

                                                Split, 811

 

                                          814  v*t=z'

                                                Split, 811

 

                                          815  v*x=z'

                                                Substitute, 812, 814

 

                                          816  ALL(b):ALL(c):[u e n & b e n & c e n => [u+b=c+b => u=c]]

                                                U Spec, 7

 

                                          817  ALL(c):[u e n & 1 e n & c e n => [u+1=c+1 => u=c]]

                                                U Spec, 816

 

                                          818  u e n & 1 e n & y e n => [u+1=y+1 => u=y]

                                                U Spec, 817

 

                                          819  u e n & 1 e n

                                                Join, 797, 5

 

                                          820  u e n & 1 e n & y e n

                                                Join, 819, 672

 

                                          821  u+1=y+1 => u=y

                                                Detach, 818, 820

 

                                          822  u=y

                                                Detach, 821, 813

 

                                          823  (x,u,v) e pow

                                                Substitute, 812, 779

 

                                          824  (x,y,v) e pow

                                                Substitute, 822, 823

 

                                          825  v e n => [(x,y,v) e pow => z=v]

                                                U Spec, 690

 

                                          826  (x,y,v) e pow => z=v

                                                Detach, 825, 798

 

                                          827  z=v

                                                Detach, 826, 824

 

                                          828  z*x=z'

                                                Substitute, 827, 815

 

                                          829  z'=z*x

                                                Sym, 828

 

                                          830  z'=z*x & ~z'=z*x

                                                Join, 829, 694

 

                                    831  ~[t=x & u+1=y+1 & v*t=z']

                                          4 Conclusion, 811

 

                                    832  (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']

                                          Join, 810, 831

 

                                    833  (t,u+1,v*t) e q

                                          Detach, 805, 832

 

                        As Required:

 

                              834  ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                                    4 Conclusion, 771

 

                                    835  t e n

                                          Premise

 

                                          836  ~t=0

                                                Premise

 

                                          837  ALL(b):ALL(c):[(t,b,c) e q

                                      <=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]

                                                U Spec, 711

 

                                          838  ALL(c):[(t,0,c) e q

                                      <=> (t,0,c) e pow & ~[t=x & 0=y+1 & c=z']]

                                                U Spec, 837

 

                                          839  (t,0,1) e q

                                      <=> (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']

                                                U Spec, 838

 

                                          840  [(t,0,1) e q => (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']]

                                      & [(t,0,1) e pow & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q]

                                                Iff-And, 839

 

                                          841  (t,0,1) e q => (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']

                                                Split, 840

 

                                  Sufficient: (t,0,1) e q

 

                                          842  (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q

                                                Split, 840

 

                                          843  t e n => [~t=0 => (t,0,1) e pow]

                                                U Spec, 80

 

                                          844  ~t=0 => (t,0,1) e pow

                                                Detach, 843, 835

 

                                          845  (t,0,1) e pow

                                                Detach, 844, 836

 

                                                846  t=x & 0=y+1 & 1=z'

                                                      Premise

 

                                                847  t=x

                                                      Split, 846

 

                                                848  0=y+1

                                                      Split, 846

 

                                                849  1=z'

                                                      Split, 846

 

                                                850  y e n => ~y+1=0

                                                      U Spec, 8

 

                                                851  ~y+1=0

                                                      Detach, 850, 672

 

                                                852  y+1=0

                                                      Sym, 848

 

                                                853  y+1=0 & ~y+1=0

                                                      Join, 852, 851

 

                                          854  ~[t=x & 0=y+1 & 1=z']

                                                4 Conclusion, 846

 

                                          855  (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']

                                                Join, 845, 854

 

                                          856  (t,0,1) e q

                                                Detach, 842, 855

 

                                    857  ~t=0 => (t,0,1) e q

                                          4 Conclusion, 836

 

                        As Required:

 

                              858  ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                                    4 Conclusion, 835

 

                              859  q e pn3 & (0,0,x0) e q

                                    Join, 736, 753

 

                              860  q e pn3 & (0,0,x0) e q

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                                    Join, 859, 858

 

                              861  q e pn3 & (0,0,x0) e q

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                                    Join, 860, 834

 

                              862  q e pn3 & (0,0,x0) e q

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e q]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]

                             & ~(x,y+1,z') e q

                                    Join, 861, 770

 

                              863  EXIST(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             & ~(x,y+1,z') e d]

                                    E Gen, 862

 

                              864  ~(x,y+1,z') e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d

                             & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

                             & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

                             & ~(x,y+1,z') e d]

                                    Arb Or, 863

 

                              865  ~(x,y+1,z') e pow

                                    Detach, 707, 864

 

                              866  (x,y+1,z') e pow & ~(x,y+1,z') e pow

                                    Join, 693, 865

 

                        867  ~[(x,y+1,z') e pow & ~z'=z*x]

                              4 Conclusion, 692

 

                        868  ~~[(x,y+1,z') e pow => ~~z'=z*x]

                              Imply-And, 867

 

                        869  (x,y+1,z') e pow => ~~z'=z*x

                              Rem DNeg, 868

 

                        870  (x,y+1,z') e pow => z'=z*x

                              Rem DNeg, 869

 

              As Required:

 

                  871  ALL(d):[d e n => [(x,y+1,d) e pow => d=z*x]]

                        4 Conclusion, 691

 

                  872  y+1 e p2 <=> y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]

                        U Spec, 614

 

                  873  [y+1 e p2 => y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]]

                   & [y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]] => y+1 e p2]

                        Iff-And, 872

 

                  874  y+1 e p2 => y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]

                        Split, 873

 

              Sufficient: y+1 e p2

 

                  875  y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]] => y+1 e p2

                        Split, 873

 

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

                        U Spec, 2

 

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

                        U Spec, 876

 

                  878  y e n & 1 e n

                        Join, 672, 5

 

                  879  y+1 e n

                        Detach, 877, 878

 

                        880  z1 e n & z2 e n

                              Premise

 

                        881  z1 e n

                              Split, 880

 

                        882  z2 e n

                              Split, 880

 

                              883  (x,y+1,z1) e pow & (x,y+1,z2) e pow

                                    Premise

 

                              884  (x,y+1,z1) e pow

                                    Split, 883

 

                              885  (x,y+1,z2) e pow

                                    Split, 883

 

                              886  z1 e n => [(x,y+1,z1) e pow => z1=z*x]

                                    U Spec, 871

 

                              887  (x,y+1,z1) e pow => z1=z*x

                                    Detach, 886, 881

 

                              888  z1=z*x

                                    Detach, 887, 884

 

                              889  z2 e n => [(x,y+1,z2) e pow => z2=z*x]

                                    U Spec, 871

 

                              890  (x,y+1,z2) e pow => z2=z*x

                                    Detach, 889, 882

 

                              891  z2=z*x

                                    Detach, 890, 885

 

                              892  z1=z2

                                    Substitute, 891, 888

 

                        893  (x,y+1,z1) e pow & (x,y+1,z2) e pow => z1=z2

                              4 Conclusion, 883

 

              As Required:

 

                  894  ALL(c1):ALL(c2):[c1 e n & c2 e n

                   => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]

                        4 Conclusion, 880

 

                  895  y+1 e n

                   & ALL(c1):ALL(c2):[c1 e n & c2 e n

                   => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]

                        Join, 879, 894

 

                  896  y+1 e p2

                        Detach, 875, 895

 

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

                  4 Conclusion, 666

 

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

                  Join, 665, 897

 

          As Required:

 

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

                  Detach, 625, 898

 

                  900  y e n

                        Premise

 

                  901  y e n => y e p2

                        U Spec, 899

 

                  902  y e p2

                        Detach, 901, 900

 

                  903  y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        U Spec, 614

 

                  904  [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]]

                   & [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2]

                        Iff-And, 903

 

                  905  y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Split, 904

 

                  906  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2

                        Split, 904

 

                  907  y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Detach, 905, 902

 

                  908  y e n

                        Split, 907

 

                  909  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Split, 907

 

            910  ALL(b):[b e n

              => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]

                  4 Conclusion, 900

 

     As Required:

 

      911  ALL(a):[a e n

          => ALL(b):[b e n

          => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]]]]

            4 Conclusion, 610

 

         

          Prove: ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]

         

          Suppose...

 

            912  (x,y,z1) e pow & (x,y,z2) e pow

                  Premise

 

            913  (x,y,z1) e pow

                  Split, 912

 

            914  (x,y,z2) e pow

                  Split, 912

 

            915  ALL(b):ALL(c):[(x,b,c) e pow

              <=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,b,c) e d]]

                  U Spec, 29

 

            916  ALL(c):[(x,y,c) e pow

              <=> (x,y,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,c) e d]]

                  U Spec, 915

 

            917  (x,y,z1) e pow

              <=> (x,y,z1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z1) e d]

                  U Spec, 916

 

            918  [(x,y,z1) e pow => (x,y,z1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z1) e d]]

              & [(x,y,z1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z1) e d] => (x,y,z1) e pow]

                  Iff-And, 917

 

            919  (x,y,z1) e pow => (x,y,z1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z1) e d]

                  Split, 918

 

            920  (x,y,z1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z1) e d] => (x,y,z1) e pow

                  Split, 918

 

            921  (x,y,z1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z1) e d]

                  Detach, 919, 913

 

            922  (x,y,z1) e n3

                  Split, 921

 

            923  ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z1) e d]

                  Split, 921

 

            924  ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]

                  U Spec, 18

 

            925  ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]

                  U Spec, 924

 

            926  (x,y,z1) e n3 <=> x e n & y e n & z1 e n

                  U Spec, 925

 

            927  [(x,y,z1) e n3 => x e n & y e n & z1 e n]

              & [x e n & y e n & z1 e n => (x,y,z1) e n3]

                  Iff-And, 926

 

            928  (x,y,z1) e n3 => x e n & y e n & z1 e n

                  Split, 927

 

            929  x e n & y e n & z1 e n => (x,y,z1) e n3

                  Split, 927

 

            930  x e n & y e n & z1 e n

                  Detach, 928, 922

 

            931  x e n

                  Split, 930

 

            932  y e n

                  Split, 930

 

            933  z1 e n

                  Split, 930

 

            934  (x,y,z2) e pow

              <=> (x,y,z2) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z2) e d]

                  U Spec, 916

 

            935  [(x,y,z2) e pow => (x,y,z2) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z2) e d]]

              & [(x,y,z2) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z2) e d] => (x,y,z2) e pow]

                  Iff-And, 934

 

            936  (x,y,z2) e pow => (x,y,z2) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z2) e d]

                  Split, 935

 

            937  (x,y,z2) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z2) e d] => (x,y,z2) e pow

                  Split, 935

 

            938  (x,y,z2) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z2) e d]

                  Detach, 936, 914

 

            939  (x,y,z2) e n3

                  Split, 938

 

            940  ALL(d):[d e pn3 & (0,0,x0) e d

              & ALL(e):[e e n => [~e=0 => (e,0,1) e d]]

              & ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]

              => (x,y,z2) e d]

                  Split, 938

 

            941  (x,y,z2) e n3 <=> x e n & y e n & z2 e n

                  U Spec, 925

 

            942  [(x,y,z2) e n3 => x e n & y e n & z2 e n]

              & [x e n & y e n & z2 e n => (x,y,z2) e n3]

                  Iff-And, 941

 

            943  (x,y,z2) e n3 => x e n & y e n & z2 e n

                  Split, 942

 

            944  x e n & y e n & z2 e n => (x,y,z2) e n3

                  Split, 942

 

            945  x e n & y e n & z2 e n

                  Detach, 943, 939

 

            946  x e n

                  Split, 945

 

            947  y e n

                  Split, 945

 

            948  z2 e n

                  Split, 945

 

            949  x e n

              => ALL(b):[b e n

              => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]

                  U Spec, 911

 

            950  ALL(b):[b e n

              => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]

                  Detach, 949, 931

 

            951  y e n

              => ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                  U Spec, 950

 

            952  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                  Detach, 951, 932

 

            953  ALL(c2):[z1 e n & c2 e n => [(x,y,z1) e pow & (x,y,c2) e pow => z1=c2]]

                  U Spec, 952

 

            954  z1 e n & z2 e n => [(x,y,z1) e pow & (x,y,z2) e pow => z1=z2]

                  U Spec, 953

 

            955  z1 e n & z2 e n

                  Join, 933, 948

 

            956  (x,y,z1) e pow & (x,y,z2) e pow => z1=z2

                  Detach, 954, 955

 

            957  z1=z2

                  Detach, 956, 912

 

     Functionality of pow, Part 3

 

      958  ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]

            4 Conclusion, 912

 

      959  ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]

          & ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]

            Join, 513, 609

 

      960  ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]

          & ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]

          & ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]

            Join, 959, 958

 

    

     pow is a function!

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

 

      961  ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]

            Detach, 495, 960

 

         

          Prove: ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

         

          Suppose...

 

            962  x e n & y e n

                  Premise

 

            963  x e n

                  Split, 962

 

            964  y e n

                  Split, 962

 

            965  ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  U Spec, 609

 

            966  x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]

                  U Spec, 965

 

            967  EXIST(c):[c e n & (x,y,c) e pow]

                  Detach, 966, 962

 

            968  z e n & (x,y,z) e pow

                  E Spec, 967

 

            969  z e n

                  Split, 968

 

            970  (x,y,z) e pow

                  Split, 968

 

            971  ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]

                  U Spec, 961

 

            972  ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]

                  U Spec, 971

 

            973  z=pow(x,y) <=> (x,y,z) e pow

                  U Spec, 972

 

            974  [z=pow(x,y) => (x,y,z) e pow]

              & [(x,y,z) e pow => z=pow(x,y)]

                  Iff-And, 973

 

            975  z=pow(x,y) => (x,y,z) e pow

                  Split, 974

 

            976  (x,y,z) e pow => z=pow(x,y)

                  Split, 974

 

            977  z=pow(x,y)

                  Detach, 976, 970

 

            978  pow(x,y) e n

                  Substitute, 977, 969

 

     As Required:

 

      979  ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

            4 Conclusion, 962

 

     Prove: pow(0,0)=x0

 

      980  ALL(c2):ALL(d):[d=pow(0,c2) <=> (0,c2,d) e pow]

            U Spec, 961

 

      981  ALL(d):[d=pow(0,0) <=> (0,0,d) e pow]

            U Spec, 980

 

      982  x0=pow(0,0) <=> (0,0,x0) e pow

            U Spec, 981

 

      983  [x0=pow(0,0) => (0,0,x0) e pow]

          & [(0,0,x0) e pow => x0=pow(0,0)]

            Iff-And, 982

 

      984  x0=pow(0,0) => (0,0,x0) e pow

            Split, 983

 

      985  (0,0,x0) e pow => x0=pow(0,0)

            Split, 983

 

      986  x0=pow(0,0)

            Detach, 985, 50

 

     As Required:

 

      987  pow(0,0)=x0

            Sym, 986

 

         

          Prove: ALL(a):[a e n => [~a=0 => pow(a,0)=1]]

         

          Suppose...

 

            988  x e n

                  Premise

 

            989  x e n => [~x=0 => (x,0,1) e pow]

                  U Spec, 80

 

            990  ~x=0 => (x,0,1) e pow

                  Detach, 989, 988

 

             

              Prove: ~x=0 => pow(x,0)=1

             

              Suppose...

 

                  991  ~x=0

                        Premise

 

                  992  (x,0,1) e pow

                        Detach, 990, 991

 

                  993  ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]

                        U Spec, 961

 

                  994  ALL(d):[d=pow(x,0) <=> (x,0,d) e pow]

                        U Spec, 993

 

                  995  1=pow(x,0) <=> (x,0,1) e pow

                        U Spec, 994

 

                  996  [1=pow(x,0) => (x,0,1) e pow]

                   & [(x,0,1) e pow => 1=pow(x,0)]

                        Iff-And, 995

 

                  997  1=pow(x,0) => (x,0,1) e pow

                        Split, 996

 

                  998  (x,0,1) e pow => 1=pow(x,0)

                        Split, 996

 

                  999  1=pow(x,0)

                        Detach, 998, 992

 

                  1000 pow(x,0)=1

                        Sym, 999

 

          As Required:

 

            1001 ~x=0 => pow(x,0)=1

                  4 Conclusion, 991

 

     As Required:

 

      1002 ALL(a):[a e n => [~a=0 => pow(a,0)=1]]

            4 Conclusion, 988

 

         

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

         

          Suppose...

 

            1003 x e n & y e n

                  Premise

 

            1004 x e n

                  Split, 1003

 

            1005 y e n

                  Split, 1003

 

            1006 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  U Spec, 609

 

            1007 x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]

                  U Spec, 1006

 

            1008 EXIST(c):[c e n & (x,y,c) e pow]

                  Detach, 1007, 1003

 

            1009 z1 e n & (x,y,z1) e pow

                  E Spec, 1008

 

            1010 z1 e n

                  Split, 1009

 

            1011 (x,y,z1) e pow

                  Split, 1009

 

            1012 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]

                  U Spec, 961

 

            1013 ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]

                  U Spec, 1012

 

            1014 z1=pow(x,y) <=> (x,y,z1) e pow

                  U Spec, 1013

 

            1015 [z1=pow(x,y) => (x,y,z1) e pow]

              & [(x,y,z1) e pow => z1=pow(x,y)]

                  Iff-And, 1014

 

            1016 z1=pow(x,y) => (x,y,z1) e pow

                  Split, 1015

 

            1017 (x,y,z1) e pow => z1=pow(x,y)

                  Split, 1015

 

            1018 z1=pow(x,y)

                  Detach, 1017, 1011

 

            1019 ALL(b):ALL(c):[x e n & b e n & c e n

              => [(x,b,c) e pow => (x,b+1,c*x) e pow]]

                  U Spec, 133

 

            1020 ALL(c):[x e n & y e n & c e n

              => [(x,y,c) e pow => (x,y+1,c*x) e pow]]

                  U Spec, 1019

 

            1021 x e n & y e n & z1 e n

              => [(x,y,z1) e pow => (x,y+1,z1*x) e pow]

                  U Spec, 1020

 

            1022 x e n & y e n & z1 e n

                  Join, 1003, 1010

 

            1023 (x,y,z1) e pow => (x,y+1,z1*x) e pow

                  Detach, 1021, 1022

 

            1024 (x,y+1,z1*x) e pow

                  Detach, 1023, 1011

 

            1025 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]

                  U Spec, 961

 

            1026 ALL(d):[d=pow(x,y+1) <=> (x,y+1,d) e pow]

                  U Spec, 1025

 

            1027 z1*x=pow(x,y+1) <=> (x,y+1,z1*x) e pow

                  U Spec, 1026

 

            1028 [z1*x=pow(x,y+1) => (x,y+1,z1*x) e pow]

              & [(x,y+1,z1*x) e pow => z1*x=pow(x,y+1)]

                  Iff-And, 1027

 

            1029 z1*x=pow(x,y+1) => (x,y+1,z1*x) e pow

                  Split, 1028

 

            1030 (x,y+1,z1*x) e pow => z1*x=pow(x,y+1)

                  Split, 1028

 

            1031 z1*x=pow(x,y+1)

                  Detach, 1030, 1024

 

            1032 pow(x,y+1)=z1*x

                  Sym, 1031

 

            1033 pow(x,y+1)=pow(x,y)*x

                  Substitute, 1018, 1032

 

     As Required:

 

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

            4 Conclusion, 1003

 

      1035 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

          & pow(0,0)=x0

            Join, 979, 987

 

      1036 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

          & pow(0,0)=x0

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

            Join, 1035, 1002

 

      1037 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

          & pow(0,0)=x0

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

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

            Join, 1036, 1034

 

As Required:

 

1038 ALL(x0):[x0 e n

     => EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]

     & pow(0,0)=x0

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

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

      4 Conclusion, 25