THEOREM

*******

 

There are infinitely many binary functions pow on N that satisfy:

 

  pow(x,2) = x*x

  pow(x,y+1) = pow(x,y) * x

 

Here, we formally 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 => pow(a,2)=a*a]

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

 

 

This machine-verified formal proof was written with the aid of

the author's DC Proof 2.0 software available at http://www.dcproof.com

 

 

AXIOMS / DEFINITIONS USED

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

 

n is a set (the set of natural numbers)

 

1     Set(n)

      Axiom

 

+ is a binary function on n

 

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

      Axiom

 

* is a binary function on n

 

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

      Axiom

 

4     0 e n

      Axiom

 

5     1 e n

      Axiom

 

6     2 e n

      Axiom

 

7     2=1+1

      Axiom

 

Adding 0

 

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

      Axiom

 

Multiplying by 0

 

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

      Axiom

 

Multiplying by 1

 

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

      Axiom

 

+ is commutative

 

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

      Axiom

 

* is commutative

 

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

      Axiom

 

The principle of mathematical induction (starting at 0)

 

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

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

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

      Axiom

 

Right cancelability of +

 

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

      Axiom

 

0 has no predecessor

 

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

      Axiom

 

 

PROOF

*****

 

Construct the set of ordered triples of n

 

Apply Cartesian Product Axiom

 

16    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

 

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

 

18    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, 17

 

19    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, 18

 

20    Set(n) & Set(n)

      Join, 1, 1

 

21    Set(n) & Set(n) & Set(n)

      Join, 20, 1

 

22    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, 19, 21

 

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

      E Spec, 22

 

 

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

**********

 

24    Set''(n3)

      Split, 23

 

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

      Split, 23

 

 

Construct the powerset of n3

 

Apply the Power Set Axiom

 

26    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

 

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

 

28    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, 27, 24

 

29    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, 28

 

 

Define: pn3  (the power set of n3)

***********

 

30    Set(pn3)

      Split, 29

 

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

      Split, 29

 

    

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

 

      32    x0 e n

            Premise

 

     Construct the set pow, a subset of n3

    

     Apply the Subset Axiom

 

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

 

      34    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, 33

 

    

     Define: pow

     ***********

 

      35    Set''(pow)

            Split, 34

 

      36    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, 34

 

     Establish some useful properties of pow

    

     Prove: (0,0,x0) e pow

    

     Apply definition of pow

 

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

 

      38    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, 37

 

      39    (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, 38

 

      40    [(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, 39

 

      41    (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, 40

 

     Sufficient: (0,0,x0) e pow

 

      42    (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, 40

 

     Prove: (0,0,x0) e n3

 

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

            U Spec, 25

 

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

            U Spec, 43

 

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

            U Spec, 44

 

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

 

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

            Split, 46

 

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

            Split, 46

 

      49    0 e n & 0 e n

            Join, 4, 4

 

      50    0 e n & 0 e n & x0 e n

            Join, 49, 32

 

     As Required:

 

      51    (0,0,x0) e n3

            Detach, 48, 50

 

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

 

            52    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

 

            53    q e pn3

                  Split, 52

 

            54    (0,0,x0) e q

                  Split, 52

 

     As Required:

 

      55    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, 52

 

      56    (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, 51, 55

 

     As Required:

 

      57    (0,0,x0) e pow

            Detach, 42, 56

 

         

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

         

          Suppose...

 

            58    x e n

                  Premise

 

             

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

             

              Suppose...

 

                  59    ~x=0

                        Premise

 

              Apply definition of pow

 

                  60    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, 36

 

                  61    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, 60

 

                  62    (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, 61

 

                  63    [(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, 62

 

                  64    (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, 63

 

              Sufficient: (x,0,1) e pow

 

                  65    (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, 63

 

              Prove: (x,0,1) e n3

             

              Apply definition of n3

 

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

                        U Spec, 25

 

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

                        U Spec, 66

 

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

                        U Spec, 67

 

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

 

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

                        Split, 69

 

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

                        Split, 69

 

                  72    x e n & 0 e n

                        Join, 58, 4

 

                  73    x e n & 0 e n & 1 e n

                        Join, 72, 5

 

                  74    (x,0,1) e n3

                        Detach, 71, 73

 

                        75    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

 

                        76    q e pn3

                              Split, 75

 

                        77    (0,0,x0) e q

                              Split, 75

 

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

                              Split, 75

 

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

                              Split, 75

 

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

                              U Spec, 78

 

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

                              Detach, 80, 58

 

                        82    (x,0,1) e q

                              Detach, 81, 59

 

                  83    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, 75

 

                  84    (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, 74, 83

 

                  85    (x,0,1) e pow

                        Detach, 65, 84

 

          As Required:

 

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

                  4 Conclusion, 59

 

     As Required:

 

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

            4 Conclusion, 58

 

         

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

 

            88    x e n & y e n & z e n

                  Premise

 

            89    x e n

                  Split, 88

 

            90    y e n

                  Split, 88

 

            91    z e n

                  Split, 88

 

             

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

             

              Suppose...

 

                  92    (x,y,z) e pow

                        Premise

 

              Apply definition of pow

 

                  93    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, 36

 

                  94    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, 93

 

                  95    (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, 94

 

                  96    [(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, 95

 

                  97    (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, 96

 

                  98    (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, 96

 

                  99    (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, 97, 92

 

                  100  (x,y,z) e n3

                        Split, 99

 

                  101  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, 99

 

              Apply definition of pow

 

                  102  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, 36

 

                  103  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, 102

 

                  104  (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, 103

 

                  105  [(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, 104

 

                  106  (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, 105

 

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

 

                  107  (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, 105

 

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

             

              Apply definition of n3

 

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

                        U Spec, 25

 

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

                        U Spec, 108

 

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

                        U Spec, 109

 

                  111  [(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, 110

 

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

                        Split, 111

 

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

                        Split, 111

 

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

                        U Spec, 2

 

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

                        U Spec, 114

 

                  116  y e n & 1 e n

                        Join, 90, 5

 

                  117  y+1 e n

                        Detach, 115, 116

 

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

                        U Spec, 3

 

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

                        U Spec, 118

 

                  120  z e n & x e n

                        Join, 91, 89

 

                  121  z*x e n

                        Detach, 119, 120

 

                  122  x e n & y+1 e n

                        Join, 89, 117

 

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

                        Join, 122, 121

 

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

                        Detach, 113, 123

 

                  

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

 

                        125  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

 

                        126  q e pn3

                              Split, 125

 

                        127  (0,0,x0) e q

                              Split, 125

 

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

                              Split, 125

 

                   Apply definition of q

 

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

                              Split, 125

 

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

                              U Spec, 129

 

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

                              U Spec, 130

 

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

                              U Spec, 131

 

                        133  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, 101

 

                        134  (x,y,z) e q

                              Detach, 133, 125

 

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

                              Detach, 132, 134

 

              As Required:

 

                  136  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, 125

 

                  137  (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, 124, 136

 

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

                        Detach, 107, 137

 

          As Required:

 

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

                  4 Conclusion, 92

 

     As Required:

 

      140  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, 88

 

         

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

         

          Suppose...

 

            141  z e n

                  Premise

 

             

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

             

              Suppose to contrary...

 

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

                        Premise

 

                  143  (0,0,z) e pow

                        Split, 142

 

                  144  ~z=x0

                        Split, 142

 

              Apply definition of pow

 

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

 

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

 

                  147  (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, 146

 

                  148  [(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, 147

 

                  149  (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, 148

 

                  150  (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, 148

 

                  151  ~[(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, 149

 

                  152  ~~[~(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, 151

 

                  153  ~(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, 152

 

                  154  ~(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, 153

 

                  155  ~(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, 154

 

                  156  ~(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, 155

 

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

 

                  157  ~(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, 156

 

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

 

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

 

              Define: q

 

                  160  Set''(q)

                        Split, 159

 

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

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

                        Split, 159

 

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

                        U Spec, 31

 

                  163  [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, 162

 

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

                        Split, 163

 

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

                        Split, 163

 

                  

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

                  

                   Suppose...

 

                        166  (t,u,v) e q

                              Premise

 

                   Apply definition of q

 

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

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

                              U Spec, 161

 

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

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

                              U Spec, 167

 

                        169  (t,u,v) e q

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

                              U Spec, 168

 

                        170  [(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, 169

 

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

                              Split, 170

 

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

                              Split, 170

 

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

                              Detach, 171, 166

 

                        174  (t,u,v) e n3

                              Split, 173

 

              As Required:

 

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

                        4 Conclusion, 166

 

                  176  Set''(q)

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

                        Join, 160, 175

 

              As Required:

 

                  177  q e pn3

                        Detach, 165, 176

 

             

              Prove: (0,0,x0) e q

             

              Apply definition of q

 

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

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

                        U Spec, 161

 

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

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

                        U Spec, 178

 

                  180  (0,0,x0) e q

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

                        U Spec, 179

 

                  181  [(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, 180

 

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

                        Split, 181

 

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

                        Split, 181

 

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

                        U Spec, 25

 

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

                        U Spec, 184

 

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

                        U Spec, 185

 

                  187  [(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, 186

 

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

                        Split, 187

 

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

                        Split, 187

 

                  190  0 e n & 0 e n

                        Join, 4, 4

 

                  191  0 e n & 0 e n & x0 e n

                        Join, 190, 32

 

                  192  (0,0,x0) e n3

                        Detach, 189, 191

 

                  

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

                  

                   Suppose to the contrary...

 

                        193  0=0 & 0=0 & x0=z

                              Premise

 

                        194  0=0

                              Split, 193

 

                        195  0=0

                              Split, 193

 

                        196  x0=z

                              Split, 193

 

                        197  ~x0=z

                              Sym, 144

 

                        198  x0=z & ~x0=z

                              Join, 196, 197

 

              As Required:

 

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

                        4 Conclusion, 193

 

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

                        Join, 192, 199

 

              As Required:

 

                  201  (0,0,x0) e q

                        Detach, 183, 200

 

             

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

             

              Apply definition of q

 

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

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

                        U Spec, 161

 

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

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

                        U Spec, 202

 

                  204  (0,0,z) e q

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

                        U Spec, 203

 

                  205  [(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, 204

 

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

                        Split, 205

 

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

                        Split, 205

 

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

                        Contra, 206

 

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

                        DeMorgan, 208

 

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

                        Rem DNeg, 209

 

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

                        Rem DNeg, 210

 

                  212  0=0

                        Reflex

 

                  213  z=z

                        Reflex

 

                  214  0=0 & 0=0

                        Join, 212, 212

 

                  215  0=0 & 0=0 & z=z

                        Join, 214, 213

 

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

                        Arb Or, 215

 

              As Required:

 

                  217  ~(0,0,z) e q

                        Detach, 211, 216

 

                        218  t e n

                              Premise

 

                       

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

                       

                        Suppose...

 

                              219  ~t=0

                                    Premise

 

                        Apply definition of q

 

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

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

                                    U Spec, 161

 

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

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

                                    U Spec, 220

 

                              222  (t,0,1) e q

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

                                    U Spec, 221

 

                              223  [(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, 222

 

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

                                    Split, 223

 

                        Sufficient: (t,0,1) e q

 

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

                                    Split, 223

 

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

                                    U Spec, 25

 

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

                                    U Spec, 226

 

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

                                    U Spec, 227

 

                              229  [(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, 228

 

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

                                    Split, 229

 

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

                                    Split, 229

 

                              232  t e n & 0 e n

                                    Join, 218, 4

 

                              233  t e n & 0 e n & 1 e n

                                    Join, 232, 5

 

                              234  (t,0,1) e n3

                                    Detach, 231, 233

 

                            

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

                            

                             Suppose to the contrary...

 

                                    235  t=0 & 0=0 & 1=z

                                          Premise

 

                                    236  t=0

                                          Split, 235

 

                                    237  0=0

                                          Split, 235

 

                                    238  1=z

                                          Split, 235

 

                                    239  t=0 & ~t=0

                                          Join, 236, 219

 

                        As Required:

 

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

                                    4 Conclusion, 235

 

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

                                    Join, 234, 240

 

                              242  (t,0,1) e q

                                    Detach, 225, 241

 

                   As Required:

 

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

                              4 Conclusion, 219

 

              As Required:

 

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

                        4 Conclusion, 218

 

                  

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

                  

                   Suppose...

 

                        245  (t,u,v) e q

                              Premise

 

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

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

                              U Spec, 161

 

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

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

                              U Spec, 246

 

                        248  (t,u,v) e q

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

                              U Spec, 247

 

                        249  [(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, 248

 

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

                              Split, 249

 

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

                              Split, 249

 

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

                              Detach, 250, 245

 

                        253  (t,u,v) e n3

                              Split, 252

 

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

                              Split, 252

 

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

                              U Spec, 25

 

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

                              U Spec, 255

 

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

                              U Spec, 256

 

                        258  [(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, 257

 

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

                              Split, 258

 

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

                              Split, 258

 

                        261  t e n & u e n & v e n

                              Detach, 259, 253

 

                        262  t e n

                              Split, 261

 

                        263  u e n

                              Split, 261

 

                        264  v e n

                              Split, 261

 

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

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

                              U Spec, 161

 

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

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

                              U Spec, 265

 

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

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

                              U Spec, 266

 

                        268  [(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, 267

 

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

                              Split, 268

 

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

                              Split, 268

 

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

                              U Spec, 25

 

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

                              U Spec, 271

 

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

                              U Spec, 272

 

                        274  [(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, 273

 

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

                              Split, 274

 

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

                              Split, 274

 

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

                              U Spec, 2

 

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

                              U Spec, 277

 

                        279  u e n & 1 e n

                              Join, 263, 5

 

                        280  u+1 e n

                              Detach, 278, 279

 

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

                              U Spec, 3

 

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

                              U Spec, 281

 

                        283  v e n & t e n

                              Join, 264, 262

 

                        284  v*t e n

                              Detach, 282, 283

 

                        285  t e n & u+1 e n

                              Join, 262, 280

 

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

                              Join, 285, 284

 

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

                              Detach, 276, 286

 

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

                                    Premise

 

                              289  t=0

                                    Split, 288

 

                              290  u+1=0

                                    Split, 288

 

                              291  v*t=z

                                    Split, 288

 

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

                                    U Spec, 15

 

                              293  ~u+1=0

                                    Detach, 292, 263

 

                              294  u+1=0 & ~u+1=0

                                    Join, 290, 293

 

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

                              4 Conclusion, 288

 

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

                              Join, 287, 295

 

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

                              Detach, 270, 296

 

              As Required:

 

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

                        4 Conclusion, 245

 

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

                        Join, 177, 201

 

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

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

                        Join, 299, 244

 

                  301  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, 300, 298

 

                  302  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, 301, 217

 

                  303  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, 302

 

                  304  ~(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, 303

 

                  305  ~(0,0,z) e pow

                        Detach, 157, 304

 

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

                        Join, 143, 305

 

          As Required:

 

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

                  4 Conclusion, 142

 

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

                  Imply-And, 307

 

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

                  Rem DNeg, 308

 

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

                  Rem DNeg, 309

 

     As Required:

 

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

            4 Conclusion, 141

 

         

          Prove: ALL(a):[a e n

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

         

          Suppose...

 

            312  x e n

                  Premise

 

             

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

             

              Suppose...

 

                  313  ~x=0

                        Premise

 

                  

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

                  

                   Suppose...

 

                        314  z e n

                              Premise

 

                       

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

                       

                        Suppose to the contrary...

 

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

                                    Premise

 

                              316  (x,0,z) e pow

                                    Split, 315

 

                              317  ~z=1

                                    Split, 315

 

                              318  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, 36

 

                              319  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, 318

 

                              320  (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, 319

 

                              321  [(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, 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]

                                    Split, 321

 

                              323  (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, 321

 

                              324  (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, 322, 316

 

                              325  (x,0,z) e n3

                                    Split, 324

 

                              326  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, 324

 

                              327  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, 36

 

                              328  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, 327

 

                              329  (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, 328

 

                              330  [(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, 329

 

                              331  (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, 330

 

                              332  (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, 330

 

                              333  ~[(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, 331

 

                              334  ~~[~(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, 333

 

                              335  ~(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, 334

 

                              336  ~(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, 335

 

                              337  ~(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, 336

 

                              338  ~(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, 337

 

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

 

                              339  ~(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, 338

 

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

 

                              341  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, 340

 

                       

                        Define: q

                        *********

 

                              342  Set''(q)

                                    Split, 341

 

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

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

                                    Split, 341

 

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

                                    U Spec, 31

 

                              345  [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, 344

 

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

                                    Split, 345

 

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

                                    Split, 345

 

                                    348  (t,u,v) e q

                                          Premise

 

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

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

                                          U Spec, 343

 

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

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

                                          U Spec, 349

 

                                    351  (t,u,v) e q

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

                                          U Spec, 350

 

                                    352  [(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, 351

 

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

                                          Split, 352

 

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

                                          Split, 352

 

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

                                          Detach, 353, 348

 

                                    356  (t,u,v) e n3

                                          Split, 355

 

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

                                    4 Conclusion, 348

 

                              358  Set''(q)

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

                                    Join, 342, 357

 

                              359  q e pn3

                                    Detach, 347, 358

 

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

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

                                    U Spec, 343

 

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

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

                                    U Spec, 360

 

                              362  (x,0,z) e q

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

                                    U Spec, 361

 

                              363  [(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, 362

 

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

                                    Split, 363

 

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

                                    Split, 363

 

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

                                    Contra, 364

 

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

                                    DeMorgan, 366

 

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

                                    Rem DNeg, 367

 

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

                                    Rem DNeg, 368

 

                              370  x=x

                                    Reflex

 

                              371  0=0

                                    Reflex

 

                              372  z=z

                                    Reflex

 

                              373  x=x & 0=0

                                    Join, 370, 371

 

                              374  x=x & 0=0 & z=z

                                    Join, 373, 372

 

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

                                    Arb Or, 374

 

                        As Required:

 

                              376  ~(x,0,z) e q

                                    Detach, 369, 375

 

                                    377  t e n

                                          Premise

 

                                          378  ~t=0

                                                Premise

 

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

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

                                                U Spec, 343

 

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

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

                                                U Spec, 379

 

                                          381  (t,0,1) e q

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

                                                U Spec, 380

 

                                          382  [(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, 381

 

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

                                                Split, 382

 

                                  Sufficient: (t,0,1) e q

 

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

                                                Split, 382

 

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

                                                U Spec, 25

 

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

                                                U Spec, 385

 

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

                                                U Spec, 386

 

                                          388  [(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, 387

 

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

                                                Split, 388

 

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

                                                Split, 388

 

                                          391  t e n & 0 e n

                                                Join, 377, 4

 

                                          392  t e n & 0 e n & 1 e n

                                                Join, 391, 5

 

                                          393  (t,0,1) e n3

                                                Detach, 390, 392

 

                                                394  t=x & 0=0 & 1=z

                                                      Premise

 

                                                395  t=x

                                                      Split, 394

 

                                                396  0=0

                                                      Split, 394

 

                                                397  1=z

                                                      Split, 394

 

                                                398  z=1

                                                      Sym, 397

 

                                                399  z=1 & ~z=1

                                                      Join, 398, 317

 

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

                                                4 Conclusion, 394

 

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

                                                Join, 393, 400

 

                                          402  (t,0,1) e q

                                                Detach, 384, 401

 

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

                                          4 Conclusion, 378

 

                        As Required:

 

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

                                    4 Conclusion, 377

 

                            

                             Suppose...

 

                                    405  (t,u,v) e q

                                          Premise

 

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

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

                                          U Spec, 343

 

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

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

                                          U Spec, 406

 

                                    408  (t,u,v) e q

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

                                          U Spec, 407

 

                                    409  [(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, 408

 

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

                                          Split, 409

 

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

                                          Split, 409

 

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

                                          Detach, 410, 405

 

                                    413  (t,u,v) e n3

                                          Split, 412

 

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

                                          Split, 412

 

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

                                          U Spec, 25

 

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

                                          U Spec, 415

 

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

                                          U Spec, 416

 

                                    418  [(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, 417

 

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

                                          Split, 418

 

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

                                          Split, 418

 

                                    421  t e n & u e n & v e n

                                          Detach, 419, 413

 

                                    422  t e n

                                          Split, 421

 

                                    423  u e n

                                          Split, 421

 

                                    424  v e n

                                          Split, 421

 

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

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

                                          U Spec, 343

 

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

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

                                          U Spec, 425

 

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

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

                                          U Spec, 426

 

                                    428  [(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, 427

 

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

                                          Split, 428

 

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

 

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

                                          Split, 428

 

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

                                          U Spec, 25

 

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

                                          U Spec, 431

 

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

                                          U Spec, 432

 

                                    434  [(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, 433

 

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

                                          Split, 434

 

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

                                          Split, 434

 

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

                                          U Spec, 2

 

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

                                          U Spec, 437

 

                                    439  u e n & 1 e n

                                          Join, 423, 5

 

                                    440  u+1 e n

                                          Detach, 438, 439

 

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

                                          U Spec, 3

 

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

                                          U Spec, 441

 

                                    443  v e n & t e n

                                          Join, 424, 422

 

                                    444  v*t e n

                                          Detach, 442, 443

 

                                    445  t e n & u+1 e n

                                          Join, 422, 440

 

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

                                          Join, 445, 444

 

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

                                          Detach, 436, 446

 

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

                                                Premise

 

                                          449  t=x

                                                Split, 448

 

                                          450  u+1=0

                                                Split, 448

 

                                          451  v*t=z

                                                Split, 448

 

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

                                                U Spec, 15

 

                                          453  ~u+1=0

                                                Detach, 452, 423

 

                                          454  u+1=0 & ~u+1=0

                                                Join, 450, 453

 

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

                                          4 Conclusion, 448

 

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

                                          Join, 447, 455

 

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

                                          Detach, 430, 456

 

                        As Required:

 

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

                                    4 Conclusion, 405

 

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

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

                                    U Spec, 343

 

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

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

                                    U Spec, 459

 

                              461  (0,0,x0) e q

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

                                    U Spec, 460

 

                              462  [(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, 461

 

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

                                    Split, 462

 

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

                                    Split, 462

 

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

                                    U Spec, 25

 

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

                                    U Spec, 465

 

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

                                    U Spec, 466

 

                              468  [(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, 467

 

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

                                    Split, 468

 

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

                                    Split, 468

 

                              471  0 e n & 0 e n

                                    Join, 4, 4

 

                              472  0 e n & 0 e n & x0 e n

                                    Join, 471, 32

 

                              473  (0,0,x0) e n3

                                    Detach, 470, 472

 

                                    474  0=x & 0=0 & x0=z

                                          Premise

 

                                    475  0=x

                                          Split, 474

 

                                    476  0=0

                                          Split, 474

 

                                    477  x0=z

                                          Split, 474

 

                                    478  x=0

                                          Sym, 475

 

                                    479  x=0 & ~x=0

                                          Join, 478, 313

 

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

                                    4 Conclusion, 474

 

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

                                    Join, 473, 480

 

                        As Required:

 

                              482  (0,0,x0) e q

                                    Detach, 464, 481

 

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

                                    Join, 359, 482

 

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

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

                                    Join, 483, 404

 

                              485  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, 484, 458

 

                              486  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, 485, 376

 

                              487  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, 486

 

                              488  ~(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, 487

 

                              489  ~(x,0,z) e pow

                                    Detach, 339, 488

 

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

                                    Join, 316, 489

 

                   As Required:

 

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

                              4 Conclusion, 315

 

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

                              Imply-And, 491

 

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

                              Rem DNeg, 492

 

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

                              Rem DNeg, 493

 

              As Required:

 

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

                        4 Conclusion, 314

 

          As Required:

 

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

                  4 Conclusion, 313

 

     As Required:

 

      497  ALL(a):[a e n

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

            4 Conclusion, 312

 

     Prove: pow is a function

    

     Apply Function Axiom

 

      498      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

 

      499  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, 498

 

      500  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, 499

 

      501  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, 500

 

    

     Sufficient: For functionality of pow

 

      502  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, 501

 

         

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

         

          Suppose...

 

            503  (x,y,z) e pow

                  Premise

 

            504  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, 36

 

            505  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, 504

 

            506  (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, 505

 

            507  [(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, 506

 

            508  (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, 507

 

            509  (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, 507

 

            510  (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, 508, 503

 

            511  (x,y,z) e n3

                  Split, 510

 

            512  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, 510

 

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

                  U Spec, 25

 

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

                  U Spec, 513

 

            515  (x,y,z) e n3 <=> x e n & y e n & z e n

                  U Spec, 514

 

            516  [(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, 515

 

            517  (x,y,z) e n3 => x e n & y e n & z e n

                  Split, 516

 

            518  x e n & y e n & z e n => (x,y,z) e n3

                  Split, 516

 

            519  x e n & y e n & z e n

                  Detach, 517, 511

 

     Functionality of pow, Part 1

 

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

            4 Conclusion, 503

 

         

          Prove: ALL(a):[a e n

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

         

          Suppose...

 

            521  x e n

                  Premise

 

            522  EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]]

                  Subset, 1

 

            523  Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]

                  E Spec, 522

 

         

          Define: p1

          **********

 

            524  Set(p1)

                  Split, 523

 

            525  ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]

                  Split, 523

 

          Apply Principle of Mathematical Induction

 

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

 

             

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

             

              Suppose...

 

                  527  y e p1

                        Premise

 

                  528  y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        U Spec, 525

 

                  529  [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, 528

 

                  530  y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        Split, 529

 

                  531  y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1

                        Split, 529

 

                  532  y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        Detach, 530, 527

 

                  533  y e n

                        Split, 532

 

          As Required:

 

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

                  4 Conclusion, 527

 

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

                  Join, 524, 534

 

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

 

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

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

                  Detach, 526, 535

 

            537  0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e pow]

                  U Spec, 525

 

            538  [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, 537

 

            539  0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e pow]

                  Split, 538

 

            540  0 e n & EXIST(c):[c e n & (x,0,c) e pow] => 0 e p1

                  Split, 538

 

          2 Cases:

 

            541  x=0 | ~x=0

                  Or Not

 

             

              Case one

             

              Prove: x=0 => 0 e p1

             

              Suppose...

 

                  542  x=0

                        Premise

 

                  543  (x,0,x0) e pow

                        Substitute, 542, 57

 

                  544  x0 e n & (x,0,x0) e pow

                        Join, 32, 543

 

                  545  EXIST(c):[c e n & (x,0,c) e pow]

                        E Gen, 544

 

                  546  0 e n & EXIST(c):[c e n & (x,0,c) e pow]

                        Join, 4, 545

 

                  547  0 e p1

                        Detach, 540, 546

 

          As Required:

 

            548  x=0 => 0 e p1

                  4 Conclusion, 542

 

             

              Case 2

             

              Prove: ~x=0 => 0 e p1

             

              Suppose...

 

                  549  ~x=0

                        Premise

 

                  550  x e n => [~x=0 => (x,0,1) e pow]

                        U Spec, 87

 

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

                        Detach, 550, 521

 

                  552  (x,0,1) e pow

                        Detach, 551, 549

 

                  553  1 e n & (x,0,1) e pow

                        Join, 5, 552

 

                  554  EXIST(c):[c e n & (x,0,c) e pow]

                        E Gen, 553

 

                  555  0 e n & EXIST(c):[c e n & (x,0,c) e pow]

                        Join, 4, 554

 

                  556  0 e p1

                        Detach, 540, 555

 

          As Required:

 

            557  ~x=0 => 0 e p1

                  4 Conclusion, 549

 

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

                  Join, 548, 557

 

          As Required:

 

            559  0 e p1

                  Cases, 541, 558

 

             

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

             

              Suppose...

 

                  560  y e p1

                        Premise

 

                  561  y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        U Spec, 525

 

                  562  [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, 561

 

                  563  y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        Split, 562

 

                  564  y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1

                        Split, 562

 

                  565  y e n & EXIST(c):[c e n & (x,y,c) e pow]

                        Detach, 563, 560

 

                  566  y e n

                        Split, 565

 

                  567  EXIST(c):[c e n & (x,y,c) e pow]

                        Split, 565

 

                  568  z e n & (x,y,z) e pow

                        E Spec, 567

 

                  569  z e n

                        Split, 568

 

                  570  (x,y,z) e pow

                        Split, 568

 

                  571  y+1 e p1 <=> y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]

                        U Spec, 525

 

                  572  [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, 571

 

                  573  y+1 e p1 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]

                        Split, 572

 

              Sufficient: y+1 e p1

 

                  574  y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow] => y+1 e p1

                        Split, 572

 

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

                        U Spec, 2

 

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

                        U Spec, 575

 

                  577  y e n & 1 e n

                        Join, 566, 5

 

                  578  y+1 e n

                        Detach, 576, 577

 

                  579  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, 140

 

                  580  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, 579

 

                  581  x e n & y e n & z e n

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

                        U Spec, 580

 

                  582  x e n & y e n

                        Join, 521, 566

 

                  583  x e n & y e n & z e n

                        Join, 582, 569

 

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

                        Detach, 581, 583

 

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

                        Detach, 584, 570

 

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

                        U Spec, 3

 

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

                        U Spec, 586

 

                  588  z e n & x e n

                        Join, 569, 521

 

                  589  z*x e n

                        Detach, 587, 588

 

                  590  z*x e n & (x,y+1,z*x) e pow

                        Join, 589, 585

 

                  591  EXIST(c):[c e n & (x,y+1,c) e pow]

                        E Gen, 590

 

                  592  y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]

                        Join, 578, 591

 

                  593  y+1 e p1

                        Detach, 574, 592

 

          As Required:

 

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

                  4 Conclusion, 560

 

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

                  Join, 559, 594

 

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

                  Detach, 536, 595

 

             

              Prove: ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]

             

              Suppose...

 

                  597  t e n

                        Premise

 

                  598  t e n => t e p1

                        U Spec, 596

 

                  599  t e p1

                        Detach, 598, 597

 

                  600  t e p1 <=> t e n & EXIST(c):[c e n & (x,t,c) e pow]

                        U Spec, 525

 

                  601  [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, 600

 

                  602  t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e pow]

                        Split, 601

 

                  603  t e n & EXIST(c):[c e n & (x,t,c) e pow] => t e p1

                        Split, 601

 

                  604  t e n & EXIST(c):[c e n & (x,t,c) e pow]

                        Detach, 602, 599

 

                  605  t e n

                        Split, 604

 

                  606  EXIST(c):[c e n & (x,t,c) e pow]

                        Split, 604

 

          As Required:

 

            607  ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  4 Conclusion, 597

 

     As Required:

 

      608  ALL(a):[a e n

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

            4 Conclusion, 521

 

         

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

         

          Suppose...

 

            609  x e n & y e n

                  Premise

 

            610  x e n

                  Split, 609

 

            611  y e n

                  Split, 609

 

            612  x e n

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

                  U Spec, 608

 

            613  ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  Detach, 612, 610

 

            614  y e n => EXIST(c):[c e n & (x,y,c) e pow]

                  U Spec, 613

 

            615  EXIST(c):[c e n & (x,y,c) e pow]

                  Detach, 614, 611

 

     Functionality of pow, Part 2

 

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

            4 Conclusion, 609

 

         

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

 

            617  x e n

                  Premise

 

            618  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

 

            619  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, 618

 

         

          Define: p2

          **********

 

            620  Set(p2)

                  Split, 619

 

            621  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, 619

 

         

          Apply Principle of Mathematical Induction

 

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

 

             

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

             

              Suppose...

 

                  623  y e p2

                        Premise

 

                  624  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, 621

 

                  625  [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, 624

 

                  626  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, 625

 

                  627  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, 625

 

                  628  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, 626, 623

 

                  629  y e n

                        Split, 628

 

          As Required:

 

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

                  4 Conclusion, 623

 

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

                  Join, 620, 630

 

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

 

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

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

                  Detach, 622, 631

 

            633  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, 621

 

            634  [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, 633

 

            635  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, 634

 

          Sufficient: 0 e p2

 

            636  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, 634

 

             

              Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n

                     => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]

             

              Suppose...

 

                  637  z1 e n & z2 e n

                        Premise

 

                  638  z1 e n

                        Split, 637

 

                  639  z2 e n

                        Split, 637

 

                  

                   Prove: (x,0,z1) e pow & (x,0,z2) e pow => z1=z2

                  

                   Suppose...

 

                        640  (x,0,z1) e pow & (x,0,z2) e pow

                              Premise

 

                        641  (x,0,z1) e pow

                              Split, 640

 

                        642  (x,0,z2) e pow

                              Split, 640

 

                   2 cases:

 

                        643  x=0 | ~x=0

                              Or Not

 

                       

                        Case one

                       

                        Prove: x=0 => z1=z2

                       

                        Suppose...

 

                              644  x=0

                                    Premise

 

                              645  z1 e n => [(0,0,z1) e pow => z1=x0]

                                    U Spec, 311

 

                              646  (0,0,z1) e pow => z1=x0

                                    Detach, 645, 638

 

                              647  (x,0,z1) e pow => z1=x0

                                    Substitute, 644, 646

 

                              648  z1=x0

                                    Detach, 647, 641

 

                              649  z2 e n => [(0,0,z2) e pow => z2=x0]

                                    U Spec, 311

 

                              650  (0,0,z2) e pow => z2=x0

                                    Detach, 649, 639

 

                              651  (x,0,z2) e pow => z2=x0

                                    Substitute, 644, 650

 

                              652  z2=x0

                                    Detach, 651, 642

 

                              653  z1=z2

                                    Substitute, 652, 648

 

                   As Required:

 

                        654  x=0 => z1=z2

                              4 Conclusion, 644

 

                       

                        Case two

                       

                        Prove: ~x=0 => z1=z2

                       

                        Suppose...

 

                              655  ~x=0

                                    Premise

 

                              656  x e n

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

                                    U Spec, 497

 

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

                                    Detach, 656, 617

 

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

                                    Detach, 657, 655

 

                              659  z1 e n => [(x,0,z1) e pow => z1=1]

                                    U Spec, 658

 

                              660  (x,0,z1) e pow => z1=1

                                    Detach, 659, 638

 

                              661  z1=1

                                    Detach, 660, 641

 

                              662  z2 e n => [(x,0,z2) e pow => z2=1]

                                    U Spec, 658

 

                              663  (x,0,z2) e pow => z2=1

                                    Detach, 662, 639

 

                              664  z2=1

                                    Detach, 663, 642

 

                              665  z1=z2

                                    Substitute, 664, 661

 

                   As Required:

 

                        666  ~x=0 => z1=z2

                              4 Conclusion, 655

 

                        667  [x=0 => z1=z2] & [~x=0 => z1=z2]

                              Join, 654, 666

 

                        668  z1=z2

                              Cases, 643, 667

 

              As Required:

 

                  669  (x,0,z1) e pow & (x,0,z2) e pow => z1=z2

                        4 Conclusion, 640

 

          As Required:

 

            670  ALL(c1):ALL(c2):[c1 e n & c2 e n

              => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]

                  4 Conclusion, 637

 

            671  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, 670

 

          As Required:

 

            672  0 e p2

                  Detach, 636, 671

 

             

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

             

              Suppose...

 

                  673  y e p2

                        Premise

 

                  674  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, 621

 

                  675  [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, 674

 

                  676  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, 675

 

                  677  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, 675

 

                  678  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, 676, 673

 

                  679  y e n

                        Split, 678

 

                  680  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Split, 678

 

                  681  ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                        U Spec, 616

 

                  682  x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]

                        U Spec, 681

 

                  683  x e n & y e n

                        Join, 617, 679

 

                  684  EXIST(c):[c e n & (x,y,c) e pow]

                        Detach, 682, 683

 

                  685  z e n & (x,y,z) e pow

                        E Spec, 684

 

                  686  z e n

                        Split, 685

 

                  687  (x,y,z) e pow

                        Split, 685

 

                  688  ALL(c2):[z e n & c2 e n => [(x,y,z) e pow & (x,y,c2) e pow => z=c2]]

                        U Spec, 680

 

                  

                   Prove: ALL(c):[c e n => [(x,y,c) e pow => z=c]]

                  

                   Suppose...

 

                        689  z' e n

                              Premise

 

                        690  z e n & z' e n => [(x,y,z) e pow & (x,y,z') e pow => z=z']

                              U Spec, 688

 

                        691  z e n & z' e n

                              Join, 686, 689

 

                        692  (x,y,z) e pow & (x,y,z') e pow => z=z'

                              Detach, 690, 691

 

                              693  (x,y,z') e pow

                                    Premise

 

                              694  (x,y,z) e pow & (x,y,z') e pow

                                    Join, 687, 693

 

                              695  z=z'

                                    Detach, 692, 694

 

                        696  (x,y,z') e pow => z=z'

                              4 Conclusion, 693

 

              As Required:

 

                  697  ALL(c):[c e n => [(x,y,c) e pow => z=c]]

                        4 Conclusion, 689

 

                  

                   Prove: ALL(d):[d e n => [(x,y+1,d) e pow => d=z*x]]

                    

                   Suppose...

 

                        698  z' e n

                              Premise

 

                       

                        Prove: ~[(x,y+1,z') e pow & ~z'=z*x]

                       

                        Suppose to the contrary...

 

                              699  (x,y+1,z') e pow & ~z'=z*x

                                    Premise

 

                              700  (x,y+1,z') e pow

                                    Split, 699

 

                              701  ~z'=z*x

                                    Split, 699

 

                              702  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, 36

 

                              703  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, 702

 

                              704  (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, 703

 

                              705  [(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, 704

 

                              706  (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, 705

 

                              707  (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, 705

 

                              708  ~[(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, 706

 

                              709  ~~[~(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, 708

 

                              710  ~(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, 709

 

                              711  ~(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, 710

 

                              712  ~(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, 711

 

                              713  ~(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, 712

 

                        Sufficient: ~(x,y+1,z') e pow   (to obtain a contradiction)

 

                              714  ~(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, 713

 

                              715  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, 35

 

                              716  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, 715

 

                       

                        Define: q

                        *********

 

                              717  Set''(q)

                                    Split, 716

 

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

                             <=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]

                                    Split, 716

 

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

                                    U Spec, 31

 

                              720  [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, 719

 

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

                                    Split, 720

 

                        Sufficient: q e pn3

 

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

                                    Split, 720

 

                            

                             Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]

                            

                             Suppose...

 

                                    723  (t,u,v) e q

                                          Premise

 

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

                                  <=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 718

 

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

                                  <=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]

                                          U Spec, 724

 

                                    726  (t,u,v) e q

                                  <=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          U Spec, 725

 

                                    727  [(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, 726

 

                                    728  (t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          Split, 727

 

                                    729  (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q

                                          Split, 727

 

                                    730  (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          Detach, 728, 723

 

                                    731  (t,u,v) e pow

                                          Split, 730

 

                                    732  ~[t=x & u=y+1 & v=z']

                                          Split, 730

 

                                    733  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, 36

 

                                    734  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, 733

 

                                    735  (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, 734

 

                                    736  [(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, 735

 

                                    737  (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, 736

 

                                    738  (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, 736

 

                                    739  (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, 737, 731

 

                                    740  (t,u,v) e n3

                                          Split, 739

 

                        As Required:

 

                              741  ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]

                                    4 Conclusion, 723

 

                              742  Set''(q)

                             & ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]

                                    Join, 717, 741

 

                        As Required:

 

                              743  q e pn3

                                    Detach, 722, 742

 

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

                             <=> (0,b,c) e pow & ~[0=x & b=y+1 & c=z']]

                                    U Spec, 718

 

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

                             <=> (0,0,c) e pow & ~[0=x & 0=y+1 & c=z']]

                                    U Spec, 744

 

                              746  (0,0,x0) e q

                             <=> (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']

                                    U Spec, 745

 

                              747  [(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, 746

 

                              748  (0,0,x0) e q => (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']

                                    Split, 747

 

                              749  (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q

                                    Split, 747

 

                            

                             Prove: ~[0=x & 0=y+1 & x0=z']

                            

                             Suppose to the contrary...

 

                                    750  0=x & 0=y+1 & x0=z'

                                          Premise

 

                                    751  0=x

                                          Split, 750

 

                                    752  0=y+1

                                          Split, 750

 

                                    753  x0=z'

                                          Split, 750

 

                                    754  y e n => ~y+1=0

                                          U Spec, 15

 

                                    755  ~y+1=0

                                          Detach, 754, 679

 

                                    756  y+1=0

                                          Sym, 752

 

                                    757  y+1=0 & ~y+1=0

                                          Join, 756, 755

 

                        As Required:

 

                              758  ~[0=x & 0=y+1 & x0=z']

                                    4 Conclusion, 750

 

                              759  (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']

                                    Join, 57, 758

 

                        As Required:

 

                              760  (0,0,x0) e q

                                    Detach, 749, 759

 

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

                             <=> (x,b,c) e pow & ~[x=x & b=y+1 & c=z']]

                                    U Spec, 718

 

                              762  ALL(c):[(x,y+1,c) e q

                             <=> (x,y+1,c) e pow & ~[x=x & y+1=y+1 & c=z']]

                                    U Spec, 761

 

                              763  (x,y+1,z') e q

                             <=> (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']

                                    U Spec, 762

 

                              764  [(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, 763

 

                              765  (x,y+1,z') e q => (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']

                                    Split, 764

 

                              766  (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q

                                    Split, 764

 

                              767  ~[(x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q

                                    Contra, 765

 

                              768  ~~[~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q

                                    DeMorgan, 767

 

                              769  ~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z'] => ~(x,y+1,z') e q

                                    Rem DNeg, 768

 

                              770  ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z' => ~(x,y+1,z') e q

                                    Rem DNeg, 769

 

                              771  x=x

                                    Reflex

 

                              772  y+1=y+1

                                    Reflex

 

                              773  z'=z'

                                    Reflex

 

                              774  x=x & y+1=y+1

                                    Join, 771, 772

 

                              775  x=x & y+1=y+1 & z'=z'

                                    Join, 774, 773

 

                              776  ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z'

                                    Arb Or, 775

 

                        As Required:

 

                              777  ~(x,y+1,z') e q

                                    Detach, 770, 776

 

                            

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

                            

                             Suppose...

 

                                    778  (t,u,v) e q

                                          Premise

 

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

                                  <=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 718

 

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

                                  <=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]

                                          U Spec, 779

 

                                    781  (t,u,v) e q

                                  <=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          U Spec, 780

 

                                    782  [(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, 781

 

                                    783  (t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          Split, 782

 

                                    784  (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q

                                          Split, 782

 

                                    785  (t,u,v) e pow & ~[t=x & u=y+1 & v=z']

                                          Detach, 783, 778

 

                                    786  (t,u,v) e pow

                                          Split, 785

 

                                    787  ~[t=x & u=y+1 & v=z']

                                          Split, 785

 

                                    788  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, 36

 

                                    789  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, 788

 

                                    790  (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, 789

 

                                    791  [(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, 790

 

                                    792  (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, 791

 

                                    793  (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, 791

 

                                    794  (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, 792, 786

 

                                    795  (t,u,v) e n3

                                          Split, 794

 

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

                                          U Spec, 25

 

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

                                          U Spec, 796

 

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

                                          U Spec, 797

 

                                    799  [(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, 798

 

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

                                          Split, 799

 

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

                                          Split, 799

 

                                    802  t e n & u e n & v e n

                                          Detach, 800, 795

 

                                    803  t e n

                                          Split, 802

 

                                    804  u e n

                                          Split, 802

 

                                    805  v e n

                                          Split, 802

 

                                    806  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, 794

 

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

                                  <=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]

                                          U Spec, 718

 

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

                                  <=> (t,u+1,c) e pow & ~[t=x & u+1=y+1 & c=z']]

                                          U Spec, 807

 

                                    809  (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, 808

 

                                    810  [(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, 809

 

                                    811  (t,u+1,v*t) e q => (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']

                                          Split, 810

 

                                    812  (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q

                                          Split, 810

 

                                    813  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, 140

 

                                    814  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, 813

 

                                    815  t e n & u e n & v e n

                                  => [(t,u,v) e pow => (t,u+1,v*t) e pow]

                                          U Spec, 814

 

                                    816  (t,u,v) e pow => (t,u+1,v*t) e pow

                                          Detach, 815, 802

 

                                    817  (t,u+1,v*t) e pow

                                          Detach, 816, 786

 

                                 

                                  Prove: ~[t=x & u+1=y+1 & v*t=z']

                                 

                                  Suppose to the contrary...

 

                                          818  t=x & u+1=y+1 & v*t=z'

                                                Premise

 

                                          819  t=x

                                                Split, 818

 

                                          820  u+1=y+1

                                                Split, 818

 

                                          821  v*t=z'

                                                Split, 818

 

                                          822  v*x=z'

                                                Substitute, 819, 821

 

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

                                                U Spec, 14

 

                                          824  ALL(c):[u e n & 1 e n & c e n => [u+1=c+1 => u=c]]

                                                U Spec, 823

 

                                          825  u e n & 1 e n & y e n => [u+1=y+1 => u=y]

                                                U Spec, 824

 

                                          826  u e n & 1 e n

                                                Join, 804, 5

 

                                          827  u e n & 1 e n & y e n

                                                Join, 826, 679

 

                                          828  u+1=y+1 => u=y

                                                Detach, 825, 827

 

                                          829  u=y

                                                Detach, 828, 820

 

                                          830  (x,u,v) e pow

                                                Substitute, 819, 786

 

                                          831  (x,y,v) e pow

                                                Substitute, 829, 830

 

                                          832  v e n => [(x,y,v) e pow => z=v]

                                                U Spec, 697

 

                                          833  (x,y,v) e pow => z=v

                                                Detach, 832, 805

 

                                          834  z=v

                                                Detach, 833, 831

 

                                          835  z*x=z'

                                                Substitute, 834, 822

 

                                          836  z'=z*x

                                                Sym, 835

 

                                          837  z'=z*x & ~z'=z*x

                                                Join, 836, 701

 

                             As Required:

 

                                    838  ~[t=x & u+1=y+1 & v*t=z']

                                          4 Conclusion, 818

 

                                    839  (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']

                                          Join, 817, 838

 

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

                                          Detach, 812, 839

 

                        As Required:

 

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

                                    4 Conclusion, 778

 

                                    842  t e n

                                          Premise

 

                                          843  ~t=0

                                                Premise

 

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

                                      <=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]

                                                U Spec, 718

 

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

                                      <=> (t,0,c) e pow & ~[t=x & 0=y+1 & c=z']]

                                                U Spec, 844

 

                                          846  (t,0,1) e q

                                      <=> (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']

                                                U Spec, 845

 

                                          847  [(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, 846

 

                                          848  (t,0,1) e q => (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']

                                                Split, 847

 

                                  Sufficient: (t,0,1) e q

 

                                          849  (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q

                                                Split, 847

 

                                          850  t e n => [~t=0 => (t,0,1) e pow]

                                                U Spec, 87

 

                                          851  ~t=0 => (t,0,1) e pow

                                                Detach, 850, 842

 

                                          852  (t,0,1) e pow

                                                Detach, 851, 843

 

                                                853  t=x & 0=y+1 & 1=z'

                                                      Premise

 

                                                854  t=x

                                                      Split, 853

 

                                                855  0=y+1

                                                      Split, 853

 

                                                856  1=z'

                                                      Split, 853

 

                                                857  y e n => ~y+1=0

                                                      U Spec, 15

 

                                                858  ~y+1=0

                                                      Detach, 857, 679

 

                                                859  y+1=0

                                                      Sym, 855

 

                                                860  y+1=0 & ~y+1=0

                                                      Join, 859, 858

 

                                          861  ~[t=x & 0=y+1 & 1=z']

                                                4 Conclusion, 853

 

                                          862  (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']

                                                Join, 852, 861

 

                                          863  (t,0,1) e q

                                                Detach, 849, 862

 

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

                                          4 Conclusion, 843

 

                        As Required:

 

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

                                    4 Conclusion, 842

 

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

                                    Join, 743, 760

 

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

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

                                    Join, 866, 865

 

                              868  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, 867, 841

 

                              869  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, 868, 777

 

                              870  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, 869

 

                              871  ~(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, 870

 

                              872  ~(x,y+1,z') e pow

                                    Detach, 714, 871

 

                              873  (x,y+1,z') e pow & ~(x,y+1,z') e pow

                                    Join, 700, 872

 

                   As Required:

 

                        874  ~[(x,y+1,z') e pow & ~z'=z*x]

                              4 Conclusion, 699

 

                        875  ~~[(x,y+1,z') e pow => ~~z'=z*x]

                              Imply-And, 874

 

                        876  (x,y+1,z') e pow => ~~z'=z*x

                              Rem DNeg, 875

 

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

                              Rem DNeg, 876

 

              As Required:

 

                  878  ALL(d):[d e n => [(x,y+1,d) e pow => d=z*x]]

                        4 Conclusion, 698

 

                  879  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, 621

 

                  880  [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, 879

 

                  881  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, 880

 

              Sufficient: y+1 e p2

 

                  882  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, 880

 

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

                        U Spec, 2

 

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

                        U Spec, 883

 

                  885  y e n & 1 e n

                        Join, 679, 5

 

                  886  y+1 e n

                        Detach, 884, 885

 

                  

                   Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n

                          => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]

                  

                   Suppose...

 

                        887  z1 e n & z2 e n

                              Premise

 

                        888  z1 e n

                              Split, 887

 

                        889  z2 e n

                              Split, 887

 

                       

                        Prove: (x,y+1,z1) e pow & (x,y+1,z2) e pow => z1=z2

                       

                        Suppose...

 

                              890  (x,y+1,z1) e pow & (x,y+1,z2) e pow

                                    Premise

 

                              891  (x,y+1,z1) e pow

                                    Split, 890

 

                              892  (x,y+1,z2) e pow

                                    Split, 890

 

                              893  z1 e n => [(x,y+1,z1) e pow => z1=z*x]

                                    U Spec, 878

 

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

                                    Detach, 893, 888

 

                              895  z1=z*x

                                    Detach, 894, 891

 

                              896  z2 e n => [(x,y+1,z2) e pow => z2=z*x]

                                    U Spec, 878

 

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

                                    Detach, 896, 889

 

                              898  z2=z*x

                                    Detach, 897, 892

 

                              899  z1=z2

                                    Substitute, 898, 895

 

                   As Required:

 

                        900  (x,y+1,z1) e pow & (x,y+1,z2) e pow => z1=z2

                              4 Conclusion, 890

 

              As Required:

 

                  901  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, 887

 

                  902  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, 886, 901

 

                  903  y+1 e p2

                        Detach, 882, 902

 

          As Required:

 

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

                  4 Conclusion, 673

 

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

                  Join, 672, 904

 

          As Required:

 

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

                  Detach, 632, 905

 

             

              Prove: 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]]]

             

              Suppose...

 

                  907  y e n

                        Premise

 

                  908  y e n => y e p2

                        U Spec, 906

 

                  909  y e p2

                        Detach, 908, 907

 

                  910  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, 621

 

                  911  [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, 910

 

                  912  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, 911

 

                  913  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, 911

 

                  914  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, 912, 909

 

                  915  y e n

                        Split, 914

 

                  916  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                        Split, 914

 

          As Required:

 

            917  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, 907

 

     As Required:

 

      918  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, 617

 

         

          Prove: ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]

         

          Suppose...

 

            919  (x,y,z1) e pow & (x,y,z2) e pow

                  Premise

 

            920  (x,y,z1) e pow

                  Split, 919

 

            921  (x,y,z2) e pow

                  Split, 919

 

            922  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, 36

 

            923  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, 922

 

            924  (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, 923

 

            925  [(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, 924

 

            926  (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, 925

 

            927  (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, 925

 

            928  (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, 926, 920

 

            929  (x,y,z1) e n3

                  Split, 928

 

            930  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, 928

 

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

                  U Spec, 25

 

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

                  U Spec, 931

 

            933  (x,y,z1) e n3 <=> x e n & y e n & z1 e n

                  U Spec, 932

 

            934  [(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, 933

 

            935  (x,y,z1) e n3 => x e n & y e n & z1 e n

                  Split, 934

 

            936  x e n & y e n & z1 e n => (x,y,z1) e n3

                  Split, 934

 

            937  x e n & y e n & z1 e n

                  Detach, 935, 929

 

            938  x e n

                  Split, 937

 

            939  y e n

                  Split, 937

 

            940  z1 e n

                  Split, 937

 

            941  (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, 923

 

            942  [(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, 941

 

            943  (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, 942

 

            944  (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, 942

 

            945  (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, 943, 921

 

            946  (x,y,z2) e n3

                  Split, 945

 

            947  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, 945

 

            948  (x,y,z2) e n3 <=> x e n & y e n & z2 e n

                  U Spec, 932

 

            949  [(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, 948

 

            950  (x,y,z2) e n3 => x e n & y e n & z2 e n

                  Split, 949

 

            951  x e n & y e n & z2 e n => (x,y,z2) e n3

                  Split, 949

 

            952  x e n & y e n & z2 e n

                  Detach, 950, 946

 

            953  x e n

                  Split, 952

 

            954  y e n

                  Split, 952

 

            955  z2 e n

                  Split, 952

 

            956  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, 918

 

            957  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, 956, 938

 

            958  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, 957

 

            959  ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]

                  Detach, 958, 939

 

            960  ALL(c2):[z1 e n & c2 e n => [(x,y,z1) e pow & (x,y,c2) e pow => z1=c2]]

                  U Spec, 959

 

            961  z1 e n & z2 e n => [(x,y,z1) e pow & (x,y,z2) e pow => z1=z2]

                  U Spec, 960

 

            962  z1 e n & z2 e n

                  Join, 940, 955

 

            963  (x,y,z1) e pow & (x,y,z2) e pow => z1=z2

                  Detach, 961, 962

 

            964  z1=z2

                  Detach, 963, 919

 

     Functionality of pow, Part 3

 

      965  ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]

            4 Conclusion, 919

 

      966  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, 520, 616

 

      967  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, 966, 965

 

    

     pow is a function!

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

 

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

            Detach, 502, 967

 

         

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

         

          Suppose...

 

            969  x e n & y e n

                  Premise

 

            970  x e n

                  Split, 969

 

            971  y e n

                  Split, 969

 

            972  ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  U Spec, 616

 

            973  x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]

                  U Spec, 972

 

            974  EXIST(c):[c e n & (x,y,c) e pow]

                  Detach, 973, 969

 

            975  z e n & (x,y,z) e pow

                  E Spec, 974

 

            976  z e n

                  Split, 975

 

            977  (x,y,z) e pow

                  Split, 975

 

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

                  U Spec, 968

 

            979  ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]

                  U Spec, 978

 

            980  z=pow(x,y) <=> (x,y,z) e pow

                  U Spec, 979

 

            981  [z=pow(x,y) => (x,y,z) e pow]

              & [(x,y,z) e pow => z=pow(x,y)]

                  Iff-And, 980

 

            982  z=pow(x,y) => (x,y,z) e pow

                  Split, 981

 

            983  (x,y,z) e pow => z=pow(x,y)

                  Split, 981

 

            984  z=pow(x,y)

                  Detach, 983, 977

 

            985  pow(x,y) e n

                  Substitute, 984, 976

 

     As Required:

 

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

            4 Conclusion, 969

 

     Prove: pow(0,0)=x0

 

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

            U Spec, 968

 

      988  ALL(d):[d=pow(0,0) <=> (0,0,d) e pow]

            U Spec, 987

 

      989  x0=pow(0,0) <=> (0,0,x0) e pow

            U Spec, 988

 

      990  [x0=pow(0,0) => (0,0,x0) e pow]

          & [(0,0,x0) e pow => x0=pow(0,0)]

            Iff-And, 989

 

      991  x0=pow(0,0) => (0,0,x0) e pow

            Split, 990

 

      992  (0,0,x0) e pow => x0=pow(0,0)

            Split, 990

 

      993  x0=pow(0,0)

            Detach, 992, 57

 

     As Required:

 

      994  pow(0,0)=x0

            Sym, 993

 

         

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

         

          Suppose...

 

            995  x e n

                  Premise

 

            996  x e n => [~x=0 => (x,0,1) e pow]

                  U Spec, 87

 

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

                  Detach, 996, 995

 

             

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

             

              Suppose...

 

                  998  ~x=0

                        Premise

 

                  999  (x,0,1) e pow

                        Detach, 997, 998

 

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

                        U Spec, 968

 

                  1001 ALL(d):[d=pow(x,0) <=> (x,0,d) e pow]

                        U Spec, 1000

 

                  1002 1=pow(x,0) <=> (x,0,1) e pow

                        U Spec, 1001

 

                  1003 [1=pow(x,0) => (x,0,1) e pow]

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

                        Iff-And, 1002

 

                  1004 1=pow(x,0) => (x,0,1) e pow

                        Split, 1003

 

                  1005 (x,0,1) e pow => 1=pow(x,0)

                        Split, 1003

 

                  1006 1=pow(x,0)

                        Detach, 1005, 999

 

                  1007 pow(x,0)=1

                        Sym, 1006

 

          As Required:

 

            1008 ~x=0 => pow(x,0)=1

                  4 Conclusion, 998

 

     As Required:

 

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

            4 Conclusion, 995

 

         

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

         

          Suppose...

 

            1010 x e n & y e n

                  Premise

 

            1011 x e n

                  Split, 1010

 

            1012 y e n

                  Split, 1010

 

            1013 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]

                  U Spec, 616

 

            1014 x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]

                  U Spec, 1013

 

            1015 EXIST(c):[c e n & (x,y,c) e pow]

                  Detach, 1014, 1010

 

            1016 z1 e n & (x,y,z1) e pow

                  E Spec, 1015

 

            1017 z1 e n

                  Split, 1016

 

            1018 (x,y,z1) e pow

                  Split, 1016

 

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

                  U Spec, 968

 

            1020 ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]

                  U Spec, 1019

 

            1021 z1=pow(x,y) <=> (x,y,z1) e pow

                  U Spec, 1020

 

            1022 [z1=pow(x,y) => (x,y,z1) e pow]

              & [(x,y,z1) e pow => z1=pow(x,y)]

                  Iff-And, 1021

 

            1023 z1=pow(x,y) => (x,y,z1) e pow

                  Split, 1022

 

            1024 (x,y,z1) e pow => z1=pow(x,y)

                  Split, 1022

 

            1025 z1=pow(x,y)

                  Detach, 1024, 1018

 

            1026 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, 140

 

            1027 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, 1026

 

            1028 x e n & y e n & z1 e n

              => [(x,y,z1) e pow => (x,y+1,z1*x) e pow]

                  U Spec, 1027

 

            1029 x e n & y e n & z1 e n

                  Join, 1010, 1017

 

            1030 (x,y,z1) e pow => (x,y+1,z1*x) e pow

                  Detach, 1028, 1029

 

            1031 (x,y+1,z1*x) e pow

                  Detach, 1030, 1018

 

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

                  U Spec, 968

 

            1033 ALL(d):[d=pow(x,y+1) <=> (x,y+1,d) e pow]

                  U Spec, 1032

 

            1034 z1*x=pow(x,y+1) <=> (x,y+1,z1*x) e pow

                  U Spec, 1033

 

            1035 [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, 1034

 

            1036 z1*x=pow(x,y+1) => (x,y+1,z1*x) e pow

                  Split, 1035

 

            1037 (x,y+1,z1*x) e pow => z1*x=pow(x,y+1)

                  Split, 1035

 

            1038 z1*x=pow(x,y+1)

                  Detach, 1037, 1031

 

            1039 pow(x,y+1)=z1*x

                  Sym, 1038

 

            1040 pow(x,y+1)=pow(x,y)*x

                  Substitute, 1025, 1039

 

     As Required:

 

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

            4 Conclusion, 1010

 

         

          Prove: ALL(a):[aen => pow(a,2)=a*a]

         

          Suppose...

 

            1042 x e n

                  Premise

 

          Two cases:

 

            1043 x=0 | ~x=0

                  Or Not

 

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

                  U Spec, 1041

 

            1045 0 e n & 0 e n => pow(0,0+1)=pow(0,0)*0

                  U Spec, 1044

 

            1046 0 e n & 0 e n

                  Join, 4, 4

 

            1047 pow(0,0+1)=pow(0,0)*0

                  Detach, 1045, 1046

 

            1048 1 e n => 1+0=1

                  U Spec, 8

 

            1049 1+0=1

                  Detach, 1048, 5

 

            1050 ALL(b):[0 e n & b e n => 0+b=b+0]

                  U Spec, 11

 

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

                  U Spec, 1050

 

            1052 0 e n & 1 e n

                  Join, 4, 5

 

            1053 0+1=1+0

                  Detach, 1051, 1052

 

            1054 0+1=1

                  Substitute, 1053, 1049

 

            1055 pow(0,1)=pow(0,0)*0

                  Substitute, 1054, 1047

 

            1056 pow(0,1)=x0*0

                  Substitute, 994, 1055

 

            1057 x0 e n => x0*0=0

                  U Spec, 9

 

            1058 x0*0=0

                  Detach, 1057, 32

 

             

              Case One

             

               Prove: x=0 => pow(x,2)=x*x

             

              Suppose...

 

                  1059 x=0

                        Premise

 

                  1060 pow(0,1)=0

                        Substitute, 1058, 1056

 

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

                        U Spec, 1041

 

                  1062 0 e n & 1 e n => pow(0,1+1)=pow(0,1)*0

                        U Spec, 1061

 

                  1063 0 e n & 1 e n

                        Join, 4, 5

 

                  1064 pow(0,1+1)=pow(0,1)*0

                        Detach, 1062, 1063

 

                  1065 pow(0,2)=pow(0,1)*0

                        Substitute, 7, 1064

 

                  1066 pow(0,2)=0*0

                        Substitute, 1060, 1065

 

                  1067 pow(x,2)=x*x

                        Substitute, 1059, 1066

 

          As Required:

 

            1068 x=0 => pow(x,2)=x*x

                  4 Conclusion, 1059

 

             

              Case Two

             

              Prove: ~x=0 => pow(x,2)=x*x

             

              Suppose...

 

                  1069 ~x=0

                        Premise

 

                  1070 x e n => [~x=0 => pow(x,0)=1]

                        U Spec, 1009

 

                  1071 ~x=0 => pow(x,0)=1

                        Detach, 1070, 1042

 

                  1072 pow(x,0)=1

                        Detach, 1071, 1069

 

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

                        U Spec, 1041

 

                  1074 x e n & 0 e n => pow(x,0+1)=pow(x,0)*x

                        U Spec, 1073

 

                  1075 x e n & 0 e n

                        Join, 1042, 4

 

                  1076 pow(x,0+1)=pow(x,0)*x

                        Detach, 1074, 1075

 

                  1077 1 e n => 1+0=1

                        U Spec, 8

 

                  1078 1+0=1

                        Detach, 1077, 5

 

                  1079 ALL(b):[0 e n & b e n => 0+b=b+0]

                        U Spec, 11

 

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

                        U Spec, 1079

 

                  1081 0 e n & 1 e n

                        Join, 4, 5

 

                  1082 0+1=1+0

                        Detach, 1080, 1081

 

                  1083 0+1=1

                        Substitute, 1082, 1078

 

                  1084 pow(x,1)=pow(x,0)*x

                        Substitute, 1083, 1076

 

                  1085 pow(x,1)=1*x

                        Substitute, 1072, 1084

 

                  1086 x e n => x*1=x

                        U Spec, 10

 

                  1087 x*1=x

                        Detach, 1086, 1042

 

                  1088 ALL(b):[1 e n & b e n => 1*b=b*1]

                        U Spec, 12

 

                  1089 1 e n & x e n => 1*x=x*1

                        U Spec, 1088

 

                  1090 1 e n & x e n

                        Join, 5, 1042

 

                  1091 1*x=x*1

                        Detach, 1089, 1090

 

                  1092 1*x=x

                        Substitute, 1091, 1087

 

                  1093 pow(x,1)=x

                        Substitute, 1092, 1085

 

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

                        U Spec, 1041

 

                  1095 x e n & 1 e n => pow(x,1+1)=pow(x,1)*x

                        U Spec, 1094

 

                  1096 x e n & 1 e n

                        Join, 1042, 5

 

                  1097 pow(x,1+1)=pow(x,1)*x

                        Detach, 1095, 1096

 

                  1098 pow(x,2)=pow(x,1)*x

                        Substitute, 7, 1097

 

                  1099 pow(x,2)=x*x

                        Substitute, 1093, 1098

 

          As Required:

 

            1100 ~x=0 => pow(x,2)=x*x

                  4 Conclusion, 1069

 

            1101 [x=0 => pow(x,2)=x*x] & [~x=0 => pow(x,2)=x*x]

                  Join, 1068, 1100

 

            1102 pow(x,2)=x*x

                  Cases, 1043, 1101

 

     As Required:

 

      1103 ALL(a):[a e n => pow(a,2)=a*a]

            4 Conclusion, 1042

 

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

          & pow(0,0)=x0

            Join, 986, 994

 

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

          & pow(0,0)=x0

          & ALL(a):[a e n => pow(a,2)=a*a]

            Join, 1104, 1103

 

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

          & pow(0,0)=x0

          & ALL(a):[a e n => pow(a,2)=a*a]

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

            Join, 1105, 1041

 

As Required:

 

1107 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 => pow(a,2)=a*a]

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

      4 Conclusion, 32