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