THEOREM

*******

 

Given the set of natural numbers n and a binary function * that is closed on set s, there exists a binary function pow

such that, for all x e s, we have: 

 

  pow(x,1) = x

  pow(x,2) = x*x

  pow(x,3) = x*x*x

  and so on.

 

This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 available at http://www.dcproof.com

 

 

REQUIRED PROPERTIES OF N

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

 

1     Set(n)

      Axiom

 

2     1 e n

      Axiom

 

Required properties of + on n

 

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

      Axiom

 

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

      Axiom

 

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

      Axiom

 

Induction property

 

6     ALL(a):[Set(a) & ALL(b):[b e a => b e n] => [1 e a & ALL(b):[b e a => b+1 e a] => ALL(b):[b e n => b e a]]]

      Axiom

 

     Prove: ALL(s):[Set(s)

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

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

            & ALL(a):[a e s => pow(a,1)=a]

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

    

     Let * be a binary function that is closed on set s

 

      7     Set(s)

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

            Premise

 

      8     Set(s)

            Split, 7

 

      9     ALL(a):ALL(b):[a e s & b e s => a*b e s]

            Split, 7

 

     Construct Cartesian product of s, n and s

    

     Apply Cartesian Product axiom

 

      10    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

 

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

            U Spec, 10

 

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

            U Spec, 11

 

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

            U Spec, 12

 

      14    Set(s) & Set(n)

            Join, 8, 1

 

      15    Set(s) & Set(n) & Set(s)

            Join, 14, 8

 

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

            Detach, 13, 15

 

      17    Set''(sns) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e sns <=> c1 e s & c2 e n & c3 e s]

            E Spec, 16

 

    

     Define: sns

    

     The Cartesian product of s, n and s

 

      18    Set''(sns)

            Split, 17

 

      19    ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e sns <=> c1 e s & c2 e n & c3 e s]

            Split, 17

 

    

     Construct the set pow

    

     Apply Subset Axiom

 

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

          <=> (a,b,c) e sns & ALL(d):[Set''(d)

          & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

          & ALL(i):[i e s => (i,1,i) e d]

          & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

            Subset, 18

 

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

          <=> (a,b,c) e sns & ALL(d):[Set''(d)

          & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

          & ALL(i):[i e s => (i,1,i) e d]

          & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

            E Spec, 20

 

    

     Define: pow

 

      22    Set''(pow)

            Split, 21

 

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

          <=> (a,b,c) e sns & ALL(d):[Set''(d)

          & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

          & ALL(i):[i e s => (i,1,i) e d]

          & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

            Split, 21

 

         

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

         

          Suppose...

 

            24    (x,y,z) e pow

                  Premise

 

          Apply definition of pow

 

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

              <=> (x,b,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 23

 

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

              <=> (x,y,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 25

 

            27    (x,y,z) e pow

              <=> (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 26

 

            28    [(x,y,z) e pow => (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

              & [(x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Iff-And, 27

 

            29    (x,y,z) e pow => (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 28

 

            30    (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 28

 

            31    (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Detach, 29, 24

 

            32    (x,y,z) e sns

                  Split, 31

 

            33    ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 31

 

          Apply definition of sns

 

            34    ALL(c2):ALL(c3):[(x,c2,c3) e sns <=> x e s & c2 e n & c3 e s]

                  U Spec, 19

 

            35    ALL(c3):[(x,y,c3) e sns <=> x e s & y e n & c3 e s]

                  U Spec, 34

 

            36    (x,y,z) e sns <=> x e s & y e n & z e s

                  U Spec, 35

 

            37    [(x,y,z) e sns => x e s & y e n & z e s]

               & [x e s & y e n & z e s => (x,y,z) e sns]

                  Iff-And, 36

 

            38    (x,y,z) e sns => x e s & y e n & z e s

                  Split, 37

 

            39    x e s & y e n & z e s => (x,y,z) e sns

                  Split, 37

 

            40    x e s & y e n & z e s

                  Detach, 38, 32

 

    

     As Required:

 

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

            4 Conclusion, 24

 

         

          Define: ALL(a):[a e s => (a,1,a) e pow]

         

          Suppose...

 

            42    x e s

                  Premise

 

          Apply definition of pow

 

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

              <=> (x,b,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 23

 

            44    ALL(c):[(x,1,c) e pow

              <=> (x,1,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 43

 

            45    (x,1,x) e pow

              <=> (x,1,x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 44

 

            46    [(x,1,x) e pow => (x,1,x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

              & [(x,1,x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Iff-And, 45

 

            47    (x,1,x) e pow => (x,1,x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 46

 

          Sufficient: For (x,1,x) e pow

 

            48    (x,1,x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 46

 

          Prove: (x,1,x) e sns

         

          Apply definition of sns

 

            49    ALL(c2):ALL(c3):[(x,c2,c3) e sns <=> x e s & c2 e n & c3 e s]

                  U Spec, 19

 

            50    ALL(c3):[(x,1,c3) e sns <=> x e s & 1 e n & c3 e s]

                  U Spec, 49

 

            51    (x,1,x) e sns <=> x e s & 1 e n & x e s

                  U Spec, 50

 

            52    [(x,1,x) e sns => x e s & 1 e n & x e s]

              & [x e s & 1 e n & x e s => (x,1,x) e sns]

                  Iff-And, 51

 

            53    (x,1,x) e sns => x e s & 1 e n & x e s

                  Split, 52

 

            54    x e s & 1 e n & x e s => (x,1,x) e sns

                  Split, 52

 

            55    x e s & 1 e n

                  Join, 42, 2

 

            56    x e s & 1 e n & x e s

                  Join, 55, 42

 

          As Required:

 

            57    (x,1,x) e sns

                  Detach, 54, 56

 

             

              Prove: ALL(d):[Set''(d)

                     & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                     & ALL(i):[i e s => (i,1,i) e d]

                     & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

             

              Suppose...

 

                  58    Set''(d)

                   & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                   & ALL(i):[i e s => (i,1,i) e d]

                   & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

                        Premise

 

                  59    Set''(d)

                        Split, 58

 

                  60    ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        Split, 58

 

                  61    ALL(i):[i e s => (i,1,i) e d]

                        Split, 58

 

                  62    ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

                        Split, 58

 

                  63    x e s => (x,1,x) e d

                        U Spec, 61

 

                  64    (x,1,x) e d

                        Detach, 63, 42

 

          As Required:

 

            65    ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  4 Conclusion, 58

 

          Joining results...

 

            66    (x,1,x) e sns

              & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Join, 57, 65

 

            67    (x,1,x) e pow

                  Detach, 48, 66

 

    

     As Required:

 

      68    ALL(a):[a e s => (a,1,a) e pow]

            4 Conclusion, 42

 

         

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

         

          Suppose...

 

            69    (x,y,z) e pow

                  Premise

 

          Apply definition of pow

 

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

              <=> (x,b,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 23

 

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

              <=> (x,y,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 70

 

            72    (x,y,z) e pow

              <=> (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 71

 

            73    [(x,y,z) e pow => (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

              & [(x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Iff-And, 72

 

            74    (x,y,z) e pow => (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 73

 

            75    (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 73

 

            76    (x,y,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Detach, 74, 69

 

            77    (x,y,z) e sns

                  Split, 76

 

            78    ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 76

 

          Prove: x e s & y e n & z e s

         

          Apply definition of sns

 

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

                  U Spec, 41

 

            80    ALL(c):[(x,y,c) e pow => x e s & y e n & c e s]

                  U Spec, 79

 

            81    (x,y,z) e pow => x e s & y e n & z e s

                  U Spec, 80

 

          As Required:

 

            82    x e s & y e n & z e s

                  Detach, 81, 69

 

            83    x e s

                  Split, 82

 

            84    y e n

                  Split, 82

 

            85    z e s

                  Split, 82

 

         

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

         

          Apply definition of pow

 

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

              <=> (x,b,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 23

 

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

              <=> (x,y+1,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 86

 

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

              <=> (x,y+1,z*x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 87

 

            89    [(x,y+1,z*x) e pow => (x,y+1,z*x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

              & [(x,y+1,z*x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Iff-And, 88

 

            90    (x,y+1,z*x) e pow => (x,y+1,z*x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 89

 

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

 

            91    (x,y+1,z*x) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 89

 

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

         

          Apply definition of sns

 

            92    ALL(c2):ALL(c3):[(x,c2,c3) e sns <=> x e s & c2 e n & c3 e s]

                  U Spec, 19

 

            93    ALL(c3):[(x,y+1,c3) e sns <=> x e s & y+1 e n & c3 e s]

                  U Spec, 92

 

            94    (x,y+1,z*x) e sns <=> x e s & y+1 e n & z*x e s

                  U Spec, 93

 

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

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

                  Iff-And, 94

 

            96    (x,y+1,z*x) e sns => x e s & y+1 e n & z*x e s

                  Split, 95

 

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

 

            97    x e s & y+1 e n & z*x e s => (x,y+1,z*x) e sns

                  Split, 95

 

          Prove: y+1 e n

         

          Apply definition of +

 

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

                  U Spec, 3

 

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

                  U Spec, 98

 

            100  y e n & 1 e n

                  Join, 84, 2

 

          As Required:

 

            101  y+1 e n

                  Detach, 99, 100

 

          Prove: z*x e s

         

          Apply definition of *

 

            102  ALL(b):[z e s & b e s => z*b e s]

                  U Spec, 9

 

            103  z e s & x e s => z*x e s

                  U Spec, 102

 

            104  z e s & x e s

                  Join, 85, 83

 

          As Required:

 

            105  z*x e s

                  Detach, 103, 104

 

            106  x e s & y+1 e n

                  Join, 83, 101

 

            107  x e s & y+1 e n & z*x e s

                  Join, 106, 105

 

          As Required:

 

            108  (x,y+1,z*x) e sns

                  Detach, 97, 107

 

             

              Prove: ALL(d):[Set''(d)

                     & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                     & ALL(i):[i e s => (i,1,i) e d]

                     & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

             

              Suppose...

 

                  109  Set''(d)

                   & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                   & ALL(i):[i e s => (i,1,i) e d]

                   & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

                        Premise

 

                  110  Set''(d)

                        Split, 109

 

                  111  ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        Split, 109

 

                  112  ALL(i):[i e s => (i,1,i) e d]

                        Split, 109

 

                  113  ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

                        Split, 109

 

                  114  ALL(j):ALL(k):[(x,j,k) e d => (x,j+1,k*x) e d]

                        U Spec, 113

 

                  115  ALL(k):[(x,y,k) e d => (x,y+1,k*x) e d]

                        U Spec, 114

 

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

                        U Spec, 115

 

                  117  Set''(d)

                   & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                   & ALL(i):[i e s => (i,1,i) e d]

                   & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

                   => (x,y,z) e d

                        U Spec, 78

 

                  118  (x,y,z) e d

                        Detach, 117, 109

 

                  119  (x,y+1,z*x) e d

                        Detach, 116, 118

 

          As Required:

 

            120  ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  4 Conclusion, 109

 

            121  (x,y+1,z*x) e sns

              & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Join, 108, 120

 

          As Required:

 

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

                  Detach, 91, 121

 

    

     As Required:

 

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

            4 Conclusion, 69

 

         

          Prove: ~EXIST(a):EXIST(c):[(a,1,c) e pow & ~c=a]

         

          Suppose to the contrary...

 

            124  (x,1,z) e pow & ~z=x

                  Premise

 

            125  (x,1,z) e pow

                  Split, 124

 

            126  ~z=x

                  Split, 124

 

          Apply definition of pow

 

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

              <=> (x,b,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 23

 

            128  ALL(c):[(x,1,c) e pow

              <=> (x,1,c) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 127

 

            129  (x,1,z) e pow

              <=> (x,1,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  U Spec, 128

 

            130  [(x,1,z) e pow => (x,1,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

               & [(x,1,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Iff-And, 129

 

            131  (x,1,z) e pow => (x,1,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 130

 

            132  (x,1,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Split, 130

 

            133  ~[(x,1,z) e sns & ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Contra, 131

 

            134  ~~[~(x,1,z) e sns | ~ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  DeMorgan, 133

 

            135  ~(x,1,z) e sns | ~ALL(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Rem DNeg, 134

 

            136  ~(x,1,z) e sns | ~~EXIST(d):~[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Quant, 135

 

            137  ~(x,1,z) e sns | EXIST(d):~[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Rem DNeg, 136

 

            138  ~(x,1,z) e sns | EXIST(d):~~[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d] & ~(x,1,z) e d] => ~(x,1,z) e pow

                  Imply-And, 137

 

         

          Sufficient: For ~(x,1,z) e pow  (to obtain a contradiction)

         

          Let d = q1 as defined below

 

            139  ~(x,1,z) e sns | EXIST(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d] & ~(x,1,z) e d] => ~(x,1,z) e pow

                  Rem DNeg, 138

 

          Construct q1

         

          Apply Subset Axiom

 

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

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

                  Subset, 22

 

            141  Set''(q1) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q1

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

                  E Spec, 140

 

          Define: q1

 

            142  Set''(q1)

                  Split, 141

 

            143  ALL(a):ALL(b):ALL(c):[(a,b,c) e q1

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

                  Split, 141

 

             

              Prove: ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]

             

              Suppose...

 

                  144  (t,u,v) e q1

                        Premise

 

              Apply definition of q1

 

                  145  ALL(b):ALL(c):[(t,b,c) e q1

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

                        U Spec, 143

 

                  146  ALL(c):[(t,u,c) e q1

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

                        U Spec, 145

 

                  147  (t,u,v) e q1

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

                        U Spec, 146

 

                  148  [(t,u,v) e q1 => (t,u,v) e pow & ~[t=x & u=1 & v=z]]

                   & [(t,u,v) e pow & ~[t=x & u=1 & v=z] => (t,u,v) e q1]

                        Iff-And, 147

 

                  149  (t,u,v) e q1 => (t,u,v) e pow & ~[t=x & u=1 & v=z]

                        Split, 148

 

                  150  (t,u,v) e pow & ~[t=x & u=1 & v=z] => (t,u,v) e q1

                        Split, 148

 

                  151  (t,u,v) e pow & ~[t=x & u=1 & v=z]

                        Detach, 149, 144

 

                  152  (t,u,v) e pow

                        Split, 151

 

                  153  ~[t=x & u=1 & v=z]

                        Split, 151

 

              Apply definition of pow

 

                  154  ALL(b):ALL(c):[(t,b,c) e pow => t e s & b e n & c e s]

                        U Spec, 41

 

                  155  ALL(c):[(t,u,c) e pow => t e s & u e n & c e s]

                        U Spec, 154

 

                  156  (t,u,v) e pow => t e s & u e n & v e s

                        U Spec, 155

 

                  157  t e s & u e n & v e s

                        Detach, 156, 152

 

          As Required:

 

            158  ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]

                  4 Conclusion, 144

 

             

              Prove: ALL(i):[i e s => (i,1,i) e q1]

             

              Suppose...

 

                  159  t e s

                        Premise

 

              Apply definition of q1

 

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

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

                        U Spec, 143

 

                  161  ALL(c):[(t,1,c) e q1

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

                        U Spec, 160

 

                  162  (t,1,t) e q1

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

                        U Spec, 161

 

                  163  [(t,1,t) e q1 => (t,1,t) e pow & ~[t=x & 1=1 & t=z]]

                   & [(t,1,t) e pow & ~[t=x & 1=1 & t=z] => (t,1,t) e q1]

                        Iff-And, 162

 

                  164  (t,1,t) e q1 => (t,1,t) e pow & ~[t=x & 1=1 & t=z]

                        Split, 163

 

              Sufficient: For (t,1,t) e q1

 

                  165  (t,1,t) e pow & ~[t=x & 1=1 & t=z] => (t,1,t) e q1

                        Split, 163

 

              Apply previous result

 

                  166  t e s => (t,1,t) e pow

                        U Spec, 68

 

                  167  (t,1,t) e pow

                        Detach, 166, 159

 

                  

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

                  

                   Suppose to the contrary...

 

                        168  t=x & 1=1 & t=z

                              Premise

 

                        169  t=x

                              Split, 168

 

                        170  1=1

                              Split, 168

 

                        171  t=z

                              Split, 168

 

                        172  z=x

                              Substitute, 171, 169

 

                   Join results to obtain a contradiction

 

                        173  z=x & ~z=x

                              Join, 172, 126

 

              As Required:

 

                  174  ~[t=x & 1=1 & t=z]

                        4 Conclusion, 168

 

                  175  (t,1,t) e pow & ~[t=x & 1=1 & t=z]

                        Join, 167, 174

 

                  176  (t,1,t) e q1

                        Detach, 165, 175

 

          As Required:

 

            177  ALL(i):[i e s => (i,1,i) e q1]

                  4 Conclusion, 159

 

             

              Prove: ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => (i,j+1,k*i) e q1]

             

              Suppose...

 

                  178  (t,u,v) e q1

                        Premise

 

              Apply definition of q1

 

                  179  ALL(b):ALL(c):[(t,b,c) e q1

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

                        U Spec, 143

 

                  180  ALL(c):[(t,u,c) e q1

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

                        U Spec, 179

 

                  181  (t,u,v) e q1

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

                        U Spec, 180

 

                  182  [(t,u,v) e q1 => (t,u,v) e pow & ~[t=x & u=1 & v=z]]

                   & [(t,u,v) e pow & ~[t=x & u=1 & v=z] => (t,u,v) e q1]

                        Iff-And, 181

 

                  183  (t,u,v) e q1 => (t,u,v) e pow & ~[t=x & u=1 & v=z]

                        Split, 182

 

                  184  (t,u,v) e pow & ~[t=x & u=1 & v=z] => (t,u,v) e q1

                        Split, 182

 

                  185  (t,u,v) e pow & ~[t=x & u=1 & v=z]

                        Detach, 183, 178

 

                  186  (t,u,v) e pow

                        Split, 185

 

                  187  ~[t=x & u=1 & v=z]

                        Split, 185

 

              Apply definition of q1

 

                  188  ALL(b):ALL(c):[(t,b,c) e q1

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

                        U Spec, 143

 

                  189  ALL(c):[(t,u+1,c) e q1

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

                        U Spec, 188

 

                  190  (t,u+1,v*t) e q1

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

                        U Spec, 189

 

                  191  [(t,u+1,v*t) e q1 => (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z]]

                   & [(t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z] => (t,u+1,v*t) e q1]

                        Iff-And, 190

 

                  192  (t,u+1,v*t) e q1 => (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z]

                        Split, 191

 

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

 

                  193  (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z] => (t,u+1,v*t) e q1

                        Split, 191

 

              Apply previous result

 

                  194  ALL(b):ALL(c):[(t,b,c) e pow => (t,b+1,c*t) e pow]

                        U Spec, 123

 

                  195  ALL(c):[(t,u,c) e pow => (t,u+1,c*t) e pow]

                        U Spec, 194

 

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

                        U Spec, 195

 

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

                        Detach, 196, 186

 

                  

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

                  

                   Suppose to the contrary...

 

                        198  t=x & u+1=1 & v*t=z

                              Premise

 

                        199  t=x

                              Split, 198

 

                        200  u+1=1

                              Split, 198

 

                        201  v*t=z

                              Split, 198

 

                   Apply property of +

 

                        202  u e n => ~u+1=1

                              U Spec, 4

 

                   Apply previous result

 

                        203  ALL(b):ALL(c):[(t,b,c) e pow => t e s & b e n & c e s]

                              U Spec, 41

 

                        204  ALL(c):[(t,u,c) e pow => t e s & u e n & c e s]

                              U Spec, 203

 

                        205  (t,u,v) e pow => t e s & u e n & v e s

                              U Spec, 204

 

                        206  t e s & u e n & v e s

                              Detach, 205, 186

 

                        207  t e s

                              Split, 206

 

                        208  u e n

                              Split, 206

 

                        209  v e s

                              Split, 206

 

                        210  ~u+1=1

                              Detach, 202, 208

 

                   Join results to obtain contradiction

 

                        211  u+1=1 & ~u+1=1

                              Join, 200, 210

 

              As Required:

 

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

                        4 Conclusion, 198

 

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

                        Join, 197, 212

 

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

                        Join, 197, 212

 

                  215  (t,u+1,v*t) e q1

                        Detach, 193, 214

 

          As Required:

 

            216  ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => (i,j+1,k*i) e q1]

                  4 Conclusion, 178

 

          Prove: ~(x,1,z) e q1

         

          Apply definition of q1

 

            217  ALL(b):ALL(c):[(x,b,c) e q1

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

                  U Spec, 143

 

            218  ALL(c):[(x,1,c) e q1

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

                  U Spec, 217

 

            219  (x,1,z) e q1

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

                  U Spec, 218

 

            220  [(x,1,z) e q1 => (x,1,z) e pow & ~[x=x & 1=1 & z=z]]

              & [(x,1,z) e pow & ~[x=x & 1=1 & z=z] => (x,1,z) e q1]

                  Iff-And, 219

 

            221  (x,1,z) e q1 => (x,1,z) e pow & ~[x=x & 1=1 & z=z]

                  Split, 220

 

            222  (x,1,z) e pow & ~[x=x & 1=1 & z=z] => (x,1,z) e q1

                  Split, 220

 

            223  ~[(x,1,z) e pow & ~[x=x & 1=1 & z=z]] => ~(x,1,z) e q1

                  Contra, 221

 

            224  ~~[~(x,1,z) e pow | ~~[x=x & 1=1 & z=z]] => ~(x,1,z) e q1

                  DeMorgan, 223

 

            225  ~(x,1,z) e pow | ~~[x=x & 1=1 & z=z] => ~(x,1,z) e q1

                  Rem DNeg, 224

 

            226  ~(x,1,z) e pow | x=x & 1=1 & z=z => ~(x,1,z) e q1

                  Rem DNeg, 225

 

            227  x=x

                  Reflex

 

            228  1=1

                  Reflex

 

            229  z=z

                  Reflex

 

            230  x=x & 1=1

                  Join, 227, 228

 

            231  x=x & 1=1 & z=z

                  Join, 230, 229

 

            232  ~(x,1,z) e pow | x=x & 1=1 & z=z

                  Arb Or, 231

 

          As Required:

 

            233  ~(x,1,z) e q1

                  Detach, 226, 232

 

          Join results

 

            234  Set''(q1)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]

                  Join, 142, 158

 

            235  Set''(q1)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e q1]

                  Join, 234, 177

 

            236  Set''(q1)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e q1]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => (i,j+1,k*i) e q1]

                  Join, 235, 216

 

            237  Set''(q1)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e q1]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => (i,j+1,k*i) e q1]

              & ~(x,1,z) e q1

                  Join, 236, 233

 

          Generalizing...

 

            238  EXIST(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  E Gen, 237

 

            239  ~(x,1,z) e sns | EXIST(d):[Set''(d)

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

              & ALL(i):[i e s => (i,1,i) e d]

              & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                  Arb Or, 238

 

            240  ~(x,1,z) e pow

                  Detach, 139, 239

 

          Join to obtain contradiction

 

            241  (x,1,z) e pow & ~(x,1,z) e pow

                  Join, 125, 240

 

     As Required:

 

      242  ~EXIST(a):EXIST(c):[(a,1,c) e pow & ~c=a]

            4 Conclusion, 124

 

     Prove: ALL(a):ALL(c):[(a,1,c) e pow => c=a]

    

     Change quantifiers, etc.

 

      243  ~~ALL(a):~EXIST(c):[(a,1,c) e pow & ~c=a]

            Quant, 242

 

      244  ALL(a):~EXIST(c):[(a,1,c) e pow & ~c=a]

            Rem DNeg, 243

 

      245  ALL(a):~~ALL(c):~[(a,1,c) e pow & ~c=a]

            Quant, 244

 

      246  ALL(a):ALL(c):~[(a,1,c) e pow & ~c=a]

            Rem DNeg, 245

 

      247  ALL(a):ALL(c):~~[(a,1,c) e pow => ~~c=a]

            Imply-And, 246

 

      248  ALL(a):ALL(c):[(a,1,c) e pow => ~~c=a]

            Rem DNeg, 247

 

    

     As Required:

 

      249  ALL(a):ALL(c):[(a,1,c) e pow => c=a]

            Rem DNeg, 248

 

    

     Prove: pow is a function

    

     Apply Function Axiom

 

      250      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

 

      251  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, 250

 

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

          & ALL(c1):ALL(c2):[c1 e s & 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, 251

 

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

          & ALL(c1):ALL(c2):[c1 e s & 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, 252

 

    

     Sufficient: For functionality of pow

 

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

          & ALL(c1):ALL(c2):[c1 e s & c2 e n => EXIST(d):[d e s & (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, 253

 

         

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

         

          Suppose...

 

            255  x e s

                  Premise

 

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

         

          First, apply Subset Axiom to get a subset p1 of n

 

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

                  Subset, 1

 

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

                  E Spec, 256

 

         

          Define: p1

 

            258  Set(p1)

                  Split, 257

 

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

                  Split, 257

 

          Apply principle of induction

 

            260  Set(p1) & ALL(b):[b e p1 => b e n] => [1 e p1 & ALL(b):[b e p1 => b+1 e p1] => ALL(b):[b e n => b e p1]]

                  U Spec, 6

 

             

              Prove: p1 is a subset of n

             

              Suppose...

 

                  261  t e p1

                        Premise

 

              Apply definition of p1

 

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

                        U Spec, 259

 

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

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

                        Iff-And, 262

 

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

                        Split, 263

 

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

                        Split, 263

 

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

                        Detach, 264, 261

 

                  267  t e n

                        Split, 266

 

          As Required:

 

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

                  4 Conclusion, 261

 

          Joining results...

 

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

                  Join, 258, 268

 

         

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

 

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

                  Detach, 260, 269

 

         

          Base case

          *********

         

          Prove: 1 e p1

         

          Apply definition of p1

 

            271  1 e p1 <=> 1 e n & EXIST(c):[c e s & (x,1,c) e pow]

                  U Spec, 259

 

            272  [1 e p1 => 1 e n & EXIST(c):[c e s & (x,1,c) e pow]]

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

                  Iff-And, 271

 

            273  1 e p1 => 1 e n & EXIST(c):[c e s & (x,1,c) e pow]

                  Split, 272

 

          Sufficient: For 1 e p1

 

            274  1 e n & EXIST(c):[c e s & (x,1,c) e pow] => 1 e p1

                  Split, 272

 

          Apply previous result

 

            275  x e s => (x,1,x) e pow

                  U Spec, 68

 

            276  (x,1,x) e pow

                  Detach, 275, 255

 

            277  x e s & (x,1,x) e pow

                  Join, 255, 276

 

            278  EXIST(c):[c e s & (x,1,c) e pow]

                  E Gen, 277

 

            279  1 e n & EXIST(c):[c e s & (x,1,c) e pow]

                  Join, 2, 278

 

         

          As Required:

 

            280  1 e p1

                  Detach, 274, 279

 

             

              Inductive Step

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

             

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

             

              Suppose...

 

                  281  y e p1

                        Premise

 

              Apply definition of p1

 

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

                        U Spec, 259

 

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

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

                        Iff-And, 282

 

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

                        Split, 283

 

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

                        Split, 283

 

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

                        Detach, 284, 281

 

                  287  y e n

                        Split, 286

 

                  288  EXIST(c):[c e s & (x,y,c) e pow]

                        Split, 286

 

                  289  z e s & (x,y,z) e pow

                        E Spec, 288

 

              Define: z

 

                  290  z e s

                        Split, 289

 

                  291  (x,y,z) e pow

                        Split, 289

 

              Apply definition of p1

 

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

                        U Spec, 259

 

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

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

                        Iff-And, 292

 

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

                        Split, 293

 

              Sufficient: For y+1 e p1

             

              Let c = z*x

 

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

                        Split, 293

 

              Prove: y+1 e n

             

              Apply definition of + on n

 

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

                        U Spec, 3

 

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

                        U Spec, 296

 

                  298  y e n & 1 e n

                        Join, 287, 2

 

              As Required:

 

                  299  y+1 e n

                        Detach, 297, 298

 

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

             

              Apply previous result

 

                  300  ALL(b):ALL(c):[(x,b,c) e pow => (x,b+1,c*x) e pow]

                        U Spec, 123

 

                  301  ALL(c):[(x,y,c) e pow => (x,y+1,c*x) e pow]

                        U Spec, 300

 

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

                        U Spec, 301

 

              As Required:

 

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

                        Detach, 302, 291

 

              Prove: z*x e s

             

              Apply definition of * on s

 

                  304  ALL(b):[z e s & b e s => z*b e s]

                        U Spec, 9

 

                  305  z e s & x e s => z*x e s

                        U Spec, 304

 

                  306  z e s & x e s

                        Join, 290, 255

 

              As Required:

 

                  307  z*x e s

                        Detach, 305, 306

 

              Joining results...

 

                  308  z*x e s & (x,y+1,z*x) e pow

                        Join, 307, 303

 

              Generalizing...

 

                  309  EXIST(c):[c e s & (x,y+1,c) e pow]

                        E Gen, 308

 

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

                        Join, 299, 309

 

              As Required:

 

                  311  y+1 e p1

                        Detach, 295, 310

 

          As Required:

 

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

                  4 Conclusion, 281

 

          Joining results...

 

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

                  Join, 280, 312

 

          As Required:

 

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

                  Detach, 270, 313

 

             

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

              

              Suppose...

 

                  315  y e n

                        Premise

 

              Apply previous result

 

                  316  y e n => y e p1

                        U Spec, 314

 

                  317  y e p1

                        Detach, 316, 315

 

              Apply definition of p1

 

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

                        U Spec, 259

 

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

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

                        Iff-And, 318

 

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

                        Split, 319

 

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

                        Split, 319

 

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

                        Detach, 320, 317

 

                  323  y e n

                        Split, 322

 

                  324  EXIST(c):[c e s & (x,y,c) e pow]

                        Split, 322

 

          As Required:

 

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

                  4 Conclusion, 315

 

     As Required:

 

      326  ALL(a):[a e s

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

            4 Conclusion, 255

 

         

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

         

          Suppose...

 

            327  x e s & y e n

                  Premise

 

            328  x e s

                  Split, 327

 

            329  y e n

                  Split, 327

 

          Apply previous result

 

            330  x e s

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

                  U Spec, 326

 

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

                  Detach, 330, 328

 

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

                  U Spec, 331

 

            333  EXIST(c):[c e s & (x,y,c) e pow]

                  Detach, 332, 329

 

     Functionality, Part 2

 

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

            4 Conclusion, 327

 

         

          Prove: ALL(a):[a e s => ALL(b):[b e n

                 => ALL(d1):ALL(d2):[(a,b,d1) e pow & (a,b,d2) e pow => d1=d2]]]

         

          Suppose...

 

            335  x e s

                  Premise

 

         

          Prove by Induction:

         

                ALL(b):[b e n => ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,bd2) e pow => d1=d2]]

         

          Construct subset p2 of n

         

          Apply Subset Axiom

 

            336  EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]]

                  Subset, 1

 

            337  Set(p2) & ALL(b):[b e p2 <=> b e n & ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]

                  E Spec, 336

 

         

          Define: p2

 

            338  Set(p2)

                  Split, 337

 

            339  ALL(b):[b e p2 <=> b e n & ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]

                  Split, 337

 

          Apply Induction Principle

 

            340  Set(p2) & ALL(b):[b e p2 => b e n] => [1 e p2 & ALL(b):[b e p2 => b+1 e p2] => ALL(b):[b e n => b e p2]]

                  U Spec, 6

 

             

              Prove: p2 is a subset of n

             

              Suppose...

 

                  341  t e p2

                        Premise

 

              Apply definition of p2

 

                  342  t e p2 <=> t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2]

                        U Spec, 339

 

                  343  [t e p2 => t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2]]

                   & [t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2] => t e p2]

                        Iff-And, 342

 

                  344  t e p2 => t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2]

                        Split, 343

 

                  345  t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2] => t e p2

                        Split, 343

 

                  346  t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2]

                        Detach, 344, 341

 

                  347  t e n

                        Split, 346

 

          As Required:

 

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

                  4 Conclusion, 341

 

          Joining results...

 

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

                  Join, 338, 348

 

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

 

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

                  Detach, 340, 349

 

         

          Base Case

          *********

         

          Prove: 1 e p2

         

          Apply definition of p2

 

            351  1 e p2 <=> 1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]

                  U Spec, 339

 

            352  [1 e p2 => 1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]]

              & [1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2] => 1 e p2]

                  Iff-And, 351

 

            353  1 e p2 => 1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]

                  Split, 352

 

          Sufficient: For 1 e p2

 

            354  1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2] => 1 e p2

                  Split, 352

 

             

              Prove: ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]

             

              Suppose...

 

                  355  (x,1,z1) e pow & (x,1,z2) e pow

                        Premise

 

                  356  (x,1,z1) e pow

                        Split, 355

 

                  357  (x,1,z2) e pow

                        Split, 355

 

              Apply previous result

 

                  358  ALL(c):[(x,1,c) e pow => c=x]

                        U Spec, 249

 

                  359  (x,1,z1) e pow => z1=x

                        U Spec, 358

 

                  360  z1=x

                        Detach, 359, 356

 

              Apply previous result

 

                  361  ALL(c):[(x,1,c) e pow => c=x]

                        U Spec, 249

 

                  362  (x,1,z2) e pow => z2=x

                        U Spec, 361

 

                  363  z2=x

                        Detach, 362, 357

 

                  364  z1=z2

                        Substitute, 363, 360

 

          As Required:

 

            365  ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]

                  4 Conclusion, 355

 

          Joining results...

 

            366  1 e n

              & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]

                  Join, 2, 365

 

          As Required:

 

            367  1 e p2

                  Detach, 354, 366

 

             

              Inductive Step

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

             

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

             

              Suppose...

 

                  368  y e p2

                        Premise

 

              Apply definition of p2

 

                  369  y e p2 <=> y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]

                        U Spec, 339

 

                  370  [y e p2 => y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]]

                   & [y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2] => y e p2]

                        Iff-And, 369

 

                  371  y e p2 => y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]

                        Split, 370

 

                  372  y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2] => y e p2

                        Split, 370

 

                  373  y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]

                        Detach, 371, 368

 

                  374  y e n

                        Split, 373

 

                  375  ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]

                        Split, 373

 

              Apply definition of p2

 

                  376  y+1 e p2 <=> y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]

                        U Spec, 339

 

                  377  [y+1 e p2 => y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]]

                   & [y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2] => y+1 e p2]

                        Iff-And, 376

 

                  378  y+1 e p2 => y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]

                        Split, 377

 

             

              Sufficient: For y+1 e p2

 

                  379  y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2] => y+1 e p2

                        Split, 377

 

              Prove: y+1 e n

             

              Apply definition of + on n

 

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

                        U Spec, 3

 

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

                        U Spec, 380

 

                  382  y e n & 1 e n

                        Join, 374, 2

 

              As Required:

 

                  383  y+1 e n

                        Detach, 381, 382

 

              Apply previous result

 

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

                        U Spec, 334

 

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

                        U Spec, 384

 

                  386  x e s & y e n

                        Join, 335, 374

 

                  387  EXIST(c):[c e s & (x,y,c) e pow]

                        Detach, 385, 386

 

                  388  z e s & (x,y,z) e pow

                        E Spec, 387

 

              Define: z

 

                  389  z e s

                        Split, 388

 

                  390  (x,y,z) e pow

                        Split, 388

 

              Apply previous result

 

                  391  ALL(d2):[(x,y,z) e pow & (x,y,d2) e pow => z=d2]

                        U Spec, 375

 

                  

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

                  

                   Suppose...

 

                        392  z' e s

                              Premise

 

                   Apply previous result

 

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

                              U Spec, 391

 

                       

                        Prove: (x,y,z') e pow => z'=z

                       

                        Suppose...

 

                              394  (x,y,z') e pow

                                    Premise

 

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

                                    Join, 390, 394

 

                              396  z=z'

                                    Detach, 393, 395

 

                              397  z'=z

                                    Sym, 396

 

                   As Required:

 

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

                              4 Conclusion, 394

 

              As Required:

 

                  399  ALL(c):[c e s => [(x,y,c) e pow => c=z]]

                        4 Conclusion, 392

 

                  

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

                  

                   Suppose to the contrary...

 

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

                              Premise

 

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

                              Split, 400

 

                        402  ~z'=z*x

                              Split, 400

 

                   Apply definition of pow

 

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

                        <=> (x,b,c) e sns & ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              U Spec, 23

 

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

                        <=> (x,y+1,c) e sns & ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              U Spec, 403

 

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

                        <=> (x,y+1,z') e sns & ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              U Spec, 404

 

                        406  [(x,y+1,z') e pow => (x,y+1,z') e sns & ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                        & [(x,y+1,z') e sns & ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              Iff-And, 405

 

                        407  (x,y+1,z') e pow => (x,y+1,z') e sns & ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              Split, 406

 

                        408  (x,y+1,z') e sns & ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              Split, 406

 

                        409  ~[(x,y+1,z') e sns & ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              Contra, 407

 

                        410  ~~[~(x,y+1,z') e sns | ~ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              DeMorgan, 409

 

                        411  ~(x,y+1,z') e sns | ~ALL(d):[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              Rem DNeg, 410

 

                        412  ~(x,y+1,z') e sns | ~~EXIST(d):~[Set''(d)

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]

                        & ALL(i):[i e s => (i,1,i) e d]

                        & ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]

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

                              Quant, 411

 

                        413  ~(x,y