THEOREM

*******

 

EXIST(subt):ALL(a):ALL(b):[a e n & b e n => [b<=a => subt(a,b) e n & a=b+subt(a,b)]]

 

where subt is a partial function (subtraction) on the set of natural numbers.

 

 

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  

 

 

REQUIRED AXIOMS

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

 

Proposed Axiom for Partial Functions where:

 

func = function

dom  = domain of function

cod  = codomain of function

 

1     ALL(func):ALL(a1):ALL(a2):ALL(dom):ALL(cod):[Set''(func) & Set(a1) & Set(a2) & Set'(dom) & Set(cod)

    => [ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e a1 & b2 e a2]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e func => (b1,b2) e dom & c e cod]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod & (b1,b2,c) e func]]

    & ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e func & (b1,b2,c2) e func => c1=c2]

    => ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [func(b1,b2)=c <=> (b1,b2,c) e func]]]]

      Axiom

 

 

Properties of addition and <= on n

 

2     Set(n)

      Axiom

 

 

Define: + on n

 

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

      Axiom

 

 

Define: <= on n

 

4     ALL(a):ALL(b):[a e n & b e n => [a<=b <=> EXIST(c):[c e n & a+c=b]]]

      Axiom

 

 

Left cancelability of + on n

 

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

      Axiom

 

 

PROOF

*****

 

Construct Cartesian product n2

 

Apply Cartesian Product Axiom

 

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

      Cart Prod

 

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

      U Spec, 6

 

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

      U Spec, 7

 

9     Set(n) & Set(n)

      Join, 2, 2

 

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

      Detach, 8, 9

 

11   Set'(n2) & ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

      E Spec, 10

 

 

Define: n2  (Order pairs of n)

 

12   Set'(n2)

      Split, 11

 

13   ALL(c1):ALL(c2):[(c1,c2) e n2 <=> c1 e n & c2 e n]

      Split, 11

 

 

Construct domain of function

 

14   EXIST(sub):[Set'(sub) & ALL(a):ALL(b):[(a,b) e sub <=> (a,b) e n2 & b<=a]]

      Subset, 12

 

15   Set'(dom) & ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & b<=a]

      E Spec, 14

 

 

Define: dom  (The domain of the subtraction function)

 

16   Set'(dom)

      Split, 15

 

17   ALL(a):ALL(b):[(a,b) e dom <=> (a,b) e n2 & b<=a]

      Split, 15

 

 

Construct Cartesian product n3

 

Apply Cartesian Product Axiom

 

18   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

 

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

 

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

 

21   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, 20

 

22   Set(n) & Set(n) & Set(n)

      Join, 9, 2

 

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

 

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

      E Spec, 23

 

 

Define: n3  (Ordered triples of n)

 

25   Set''(n3)

      Split, 24

 

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

      Split, 24

 

 

Construct subt  (Subset of n3)

 

Apply Subset Axiom

 

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

    <=> (a,b,c) e n3 & [(a,b) e dom & a=b+c]]]

      Subset, 25

 

28   Set''(subt) & ALL(a):ALL(b):ALL(c):[(a,b,c) e subt

    <=> (a,b,c) e n3 & [(a,b) e dom & a=b+c]]

      E Spec, 27

 

 

Define: subt

 

29   Set''(subt)

      Split, 28

 

30   ALL(a):ALL(b):ALL(c):[(a,b,c) e subt

    <=> (a,b,c) e n3 & [(a,b) e dom & a=b+c]]

      Split, 28

 

Apply Partial Function Axiom

 

31   ALL(a1):ALL(a2):ALL(dom):ALL(cod):[Set''(subt) & Set(a1) & Set(a2) & Set'(dom) & Set(cod)

    => [ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e a1 & b2 e a2]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e cod]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod & (b1,b2,c) e subt]]

    & ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

    => ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [subt(b1,b2)=c <=> (b1,b2,c) e subt]]]]

      U Spec, 1

 

32   ALL(a2):ALL(dom):ALL(cod):[Set''(subt) & Set(n) & Set(a2) & Set'(dom) & Set(cod)

    => [ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e a2]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e cod]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod & (b1,b2,c) e subt]]

    & ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

    => ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [subt(b1,b2)=c <=> (b1,b2,c) e subt]]]]

      U Spec, 31

 

33   ALL(dom):ALL(cod):[Set''(subt) & Set(n) & Set(n) & Set'(dom) & Set(cod)

    => [ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e cod]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod & (b1,b2,c) e subt]]

    & ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

    => ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [subt(b1,b2)=c <=> (b1,b2,c) e subt]]]]

      U Spec, 32

 

34   ALL(cod):[Set''(subt) & Set(n) & Set(n) & Set'(dom) & Set(cod)

    => [ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e cod]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e cod & (b1,b2,c) e subt]]

    & ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

    => ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e cod => [subt(b1,b2)=c <=> (b1,b2,c) e subt]]]]

      U Spec, 33

 

35   Set''(subt) & Set(n) & Set(n) & Set'(dom) & Set(n)

    => [ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]

    & ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

    => ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e n => [subt(b1,b2)=c <=> (b1,b2,c) e subt]]]

      U Spec, 34

 

36   Set''(subt) & Set(n)

      Join, 29, 2

 

37   Set''(subt) & Set(n) & Set(n)

      Join, 36, 2

 

38   Set''(subt) & Set(n) & Set(n) & Set'(dom)

      Join, 37, 16

 

39   Set''(subt) & Set(n) & Set(n) & Set'(dom)

    & Set(n)

      Join, 38, 2

 

 

Sufficient: For functionality of subt

 

40   ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]

    & ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

    => ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e n => [subt(b1,b2)=c <=> (b1,b2,c) e subt]]

      Detach, 35, 39

 

   

    Part 1

   

    Prove: ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

   

    Suppose...

 

      41   (x,y) e dom

            Premise

 

      42   ALL(b):[(x,b) e dom <=> (x,b) e n2 & b<=x]

            U Spec, 17

 

      43   (x,y) e dom <=> (x,y) e n2 & y<=x

            U Spec, 42

 

      44   [(x,y) e dom => (x,y) e n2 & y<=x]

         & [(x,y) e n2 & y<=x => (x,y) e dom]

            Iff-And, 43

 

      45   (x,y) e dom => (x,y) e n2 & y<=x

            Split, 44

 

      46   (x,y) e n2 & y<=x => (x,y) e dom

            Split, 44

 

      47   (x,y) e n2 & y<=x

            Detach, 45, 41

 

      48   (x,y) e n2

            Split, 47

 

      49   y<=x

            Split, 47

 

      50   ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

            U Spec, 13

 

      51   (x,y) e n2 <=> x e n & y e n

            U Spec, 50

 

      52   [(x,y) e n2 => x e n & y e n]

         & [x e n & y e n => (x,y) e n2]

            Iff-And, 51

 

      53   (x,y) e n2 => x e n & y e n

            Split, 52

 

      54   x e n & y e n => (x,y) e n2

            Split, 52

 

      55   x e n & y e n

            Detach, 53, 48

 

Part 1

 

56   ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

      4 Conclusion, 41

 

   

    Part 2

   

    Prove: ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]

   

    Suppose...

 

      57   (x,y,z) e subt

            Premise

 

      58   ALL(b):ALL(c):[(x,b,c) e subt

         <=> (x,b,c) e n3 & [(x,b) e dom & x=b+c]]

            U Spec, 30

 

      59   ALL(c):[(x,y,c) e subt

         <=> (x,y,c) e n3 & [(x,y) e dom & x=y+c]]

            U Spec, 58

 

      60   (x,y,z) e subt

         <=> (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            U Spec, 59

 

      61   [(x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]]

         & [(x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt]

            Iff-And, 60

 

      62   (x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            Split, 61

 

      63   (x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt

            Split, 61

 

      64   (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            Detach, 62, 57

 

      65   (x,y,z) e n3

            Split, 64

 

      66   (x,y) e dom & x=y+z

            Split, 64

 

      67   (x,y) e dom

            Split, 66

 

      68   x=y+z

            Split, 66

 

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

            U Spec, 26

 

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

            U Spec, 69

 

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

            U Spec, 70

 

      72   [(x,y,z) e n3 => x e n & y e n & z e n]

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

            Iff-And, 71

 

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

            Split, 72

 

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

            Split, 72

 

      75   x e n & y e n & z e n

            Detach, 73, 65

 

      76   x e n

            Split, 75

 

      77   y e n

            Split, 75

 

      78   z e n

            Split, 75

 

      79   (x,y) e dom & z e n

            Join, 67, 78

 

Part 2

 

80   ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]

      4 Conclusion, 57

 

   

    Part 3

   

    Prove: ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]

   

    Suppose...

 

      81   (x,y) e dom

            Premise

 

      82   ALL(b):[(x,b) e dom <=> (x,b) e n2 & b<=x]

            U Spec, 17

 

      83   (x,y) e dom <=> (x,y) e n2 & y<=x

            U Spec, 82

 

      84   [(x,y) e dom => (x,y) e n2 & y<=x]

         & [(x,y) e n2 & y<=x => (x,y) e dom]

            Iff-And, 83

 

      85   (x,y) e dom => (x,y) e n2 & y<=x

            Split, 84

 

      86   (x,y) e n2 & y<=x => (x,y) e dom

            Split, 84

 

      87   (x,y) e n2 & y<=x

            Detach, 85, 81

 

      88   (x,y) e n2

            Split, 87

 

      89   y<=x

            Split, 87

 

      90   ALL(b):[y e n & b e n => [y<=b <=> EXIST(c):[c e n & y+c=b]]]

            U Spec, 4

 

      91   y e n & x e n => [y<=x <=> EXIST(c):[c e n & y+c=x]]

            U Spec, 90

 

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

            U Spec, 13

 

      93   (x,y) e n2 <=> x e n & y e n

            U Spec, 92

 

      94   [(x,y) e n2 => x e n & y e n]

         & [x e n & y e n => (x,y) e n2]

            Iff-And, 93

 

      95   (x,y) e n2 => x e n & y e n

            Split, 94

 

      96   x e n & y e n => (x,y) e n2

            Split, 94

 

      97   x e n & y e n

            Detach, 95, 88

 

      98   x e n

            Split, 97

 

      99   y e n

            Split, 97

 

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

            U Spec, 4

 

      101  y e n & x e n => [y<=x <=> EXIST(c):[c e n & y+c=x]]

            U Spec, 100

 

      102  y e n & x e n

            Join, 99, 98

 

      103  y<=x <=> EXIST(c):[c e n & y+c=x]

            Detach, 101, 102

 

      104  [y<=x => EXIST(c):[c e n & y+c=x]]

         & [EXIST(c):[c e n & y+c=x] => y<=x]

            Iff-And, 103

 

      105  y<=x => EXIST(c):[c e n & y+c=x]

            Split, 104

 

      106  EXIST(c):[c e n & y+c=x] => y<=x

            Split, 104

 

      107  EXIST(c):[c e n & y+c=x]

            Detach, 105, 89

 

      108  z e n & y+z=x

            E Spec, 107

 

      109  z e n

            Split, 108

 

      110  y+z=x

            Split, 108

 

      111  ALL(b):ALL(c):[(x,b,c) e subt

         <=> (x,b,c) e n3 & [(x,b) e dom & x=b+c]]

            U Spec, 30

 

      112  ALL(c):[(x,y,c) e subt

         <=> (x,y,c) e n3 & [(x,y) e dom & x=y+c]]

            U Spec, 111

 

      113  (x,y,z) e subt

         <=> (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            U Spec, 112

 

      114  [(x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]]

         & [(x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt]

            Iff-And, 113

 

      115  (x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            Split, 114

 

      116  (x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt

            Split, 114

 

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

            U Spec, 26

 

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

            U Spec, 117

 

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

            U Spec, 118

 

      120  [(x,y,z) e n3 => x e n & y e n & z e n]

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

            Iff-And, 119

 

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

            Split, 120

 

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

            Split, 120

 

      123  x e n & y e n

            Join, 98, 99

 

      124  x e n & y e n & z e n

            Join, 123, 109

 

      125  (x,y,z) e n3

            Detach, 122, 124

 

      126  x=y+z

            Sym, 110

 

      127  (x,y) e dom & x=y+z

            Join, 81, 126

 

      128  (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            Join, 125, 127

 

      129  (x,y,z) e subt

            Detach, 116, 128

 

      130  z e n & (x,y,z) e subt

            Join, 109, 129

 

Part 3

 

131  ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]

      4 Conclusion, 81

 

   

    Part 4

   

    Prove: ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

   

    Suppose...

 

      132  (x,y,z1) e subt & (x,y,z2) e subt

            Premise

 

      133  (x,y,z1) e subt

            Split, 132

 

      134  (x,y,z2) e subt

            Split, 132

 

      135  ALL(b):ALL(c):[(x,b,c) e subt

         <=> (x,b,c) e n3 & [(x,b) e dom & x=b+c]]

            U Spec, 30

 

      136  ALL(c):[(x,y,c) e subt

         <=> (x,y,c) e n3 & [(x,y) e dom & x=y+c]]

            U Spec, 135

 

      137  (x,y,z1) e subt

         <=> (x,y,z1) e n3 & [(x,y) e dom & x=y+z1]

            U Spec, 136

 

      138  [(x,y,z1) e subt => (x,y,z1) e n3 & [(x,y) e dom & x=y+z1]]

         & [(x,y,z1) e n3 & [(x,y) e dom & x=y+z1] => (x,y,z1) e subt]

            Iff-And, 137

 

      139  (x,y,z1) e subt => (x,y,z1) e n3 & [(x,y) e dom & x=y+z1]

            Split, 138

 

      140  (x,y,z1) e n3 & [(x,y) e dom & x=y+z1] => (x,y,z1) e subt

            Split, 138

 

      141  (x,y,z1) e n3 & [(x,y) e dom & x=y+z1]

            Detach, 139, 133

 

      142  (x,y,z1) e n3

            Split, 141

 

      143  (x,y) e dom & x=y+z1

            Split, 141

 

      144  (x,y) e dom

            Split, 143

 

      145  x=y+z1

            Split, 143

 

      146  (x,y,z2) e subt

         <=> (x,y,z2) e n3 & [(x,y) e dom & x=y+z2]

            U Spec, 136

 

      147  [(x,y,z2) e subt => (x,y,z2) e n3 & [(x,y) e dom & x=y+z2]]

         & [(x,y,z2) e n3 & [(x,y) e dom & x=y+z2] => (x,y,z2) e subt]

            Iff-And, 146

 

      148  (x,y,z2) e subt => (x,y,z2) e n3 & [(x,y) e dom & x=y+z2]

            Split, 147

 

      149  (x,y,z2) e n3 & [(x,y) e dom & x=y+z2] => (x,y,z2) e subt

            Split, 147

 

      150  (x,y,z2) e n3 & [(x,y) e dom & x=y+z2]

            Detach, 148, 134

 

      151  (x,y,z2) e n3

            Split, 150

 

      152  (x,y) e dom & x=y+z2

            Split, 150

 

      153  (x,y) e dom

            Split, 152

 

      154  x=y+z2

            Split, 152

 

      155  y+z1=y+z2

            Substitute, 145, 154

 

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

            U Spec, 5

 

      157  ALL(c):[y e n & z1 e n & c e n => [y+z1=y+c => z1=c]]

            U Spec, 156

 

      158  y e n & z1 e n & z2 e n => [y+z1=y+z2 => z1=z2]

            U Spec, 157

 

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

            U Spec, 26

 

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

            U Spec, 159

 

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

            U Spec, 160

 

      162  [(x,y,z1) e n3 => x e n & y e n & z1 e n]

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

            Iff-And, 161

 

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

            Split, 162

 

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

            Split, 162

 

      165  x e n & y e n & z1 e n

            Detach, 163, 142

 

      166  x e n

            Split, 165

 

      167  y e n

            Split, 165

 

      168  z1 e n

            Split, 165

 

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

            U Spec, 160

 

      170  [(x,y,z2) e n3 => x e n & y e n & z2 e n]

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

            Iff-And, 169

 

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

            Split, 170

 

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

            Split, 170

 

      173  x e n & y e n & z2 e n

            Detach, 171, 151

 

      174  x e n

            Split, 173

 

      175  y e n

            Split, 173

 

      176  z2 e n

            Split, 173

 

      177  y e n & z1 e n

            Join, 167, 168

 

      178  y e n & z1 e n & z2 e n

            Join, 177, 176

 

      179  y+z1=y+z2 => z1=z2

            Detach, 158, 178

 

      180  z1=z2

            Detach, 179, 155

 

Part 4

 

181  ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

      4 Conclusion, 132

 

182  ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]

      Join, 56, 80

 

183  ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]

      Join, 182, 131

 

184  ALL(b1):ALL(b2):[(b1,b2) e dom => b1 e n & b2 e n]

    & ALL(b1):ALL(b2):ALL(c):[(b1,b2,c) e subt => (b1,b2) e dom & c e n]

    & ALL(b1):ALL(b2):[(b1,b2) e dom => EXIST(c):[c e n & (b1,b2,c) e subt]]

    & ALL(b1):ALL(b2):ALL(c1):ALL(c2):[(b1,b2,c1) e subt & (b1,b2,c2) e subt => c1=c2]

      Join, 183, 181

 

 

As Required: subt is a function

 

185  ALL(b1):ALL(b2):ALL(c):[(b1,b2) e dom & c e n => [subt(b1,b2)=c <=> (b1,b2,c) e subt]]

      Detach, 40, 184

 

   

    Prove: ALL(a):ALL(b):[(a,b) e dom => subt(a,b) e n]

   

    Suppose...

 

      186  (x,y) e dom

            Premise

 

      187  ALL(b2):[(x,b2) e dom => EXIST(c):[c e n & (x,b2,c) e subt]]

            U Spec, 131

 

      188  (x,y) e dom => EXIST(c):[c e n & (x,y,c) e subt]

            U Spec, 187

 

      189  EXIST(c):[c e n & (x,y,c) e subt]

            Detach, 188, 186

 

      190  z e n & (x,y,z) e subt

            E Spec, 189

 

      191  z e n

            Split, 190

 

      192  (x,y,z) e subt

            Split, 190

 

      193  ALL(b2):ALL(c):[(x,b2) e dom & c e n => [subt(x,b2)=c <=> (x,b2,c) e subt]]

            U Spec, 185

 

      194  ALL(c):[(x,y) e dom & c e n => [subt(x,y)=c <=> (x,y,c) e subt]]

            U Spec, 193

 

      195  (x,y) e dom & z e n => [subt(x,y)=z <=> (x,y,z) e subt]

            U Spec, 194

 

      196  (x,y) e dom & z e n

            Join, 186, 191

 

      197  subt(x,y)=z <=> (x,y,z) e subt

            Detach, 195, 196

 

      198  [subt(x,y)=z => (x,y,z) e subt]

         & [(x,y,z) e subt => subt(x,y)=z]

            Iff-And, 197

 

      199  subt(x,y)=z => (x,y,z) e subt

            Split, 198

 

      200  (x,y,z) e subt => subt(x,y)=z

            Split, 198

 

      201  subt(x,y)=z

            Detach, 200, 192

 

      202  subt(x,y) e n

            Substitute, 201, 191

 

As Required:

 

203  ALL(a):ALL(b):[(a,b) e dom => subt(a,b) e n]

      4 Conclusion, 186

 

   

    Prove: ALL(a):ALL(b):[(a,b) e dom => a=b+subt(a,b)]

   

    Suppose...

 

      204  (x,y) e dom

            Premise

 

      205  ALL(b2):[(x,b2) e dom => EXIST(c):[c e n & (x,b2,c) e subt]]

            U Spec, 131

 

      206  (x,y) e dom => EXIST(c):[c e n & (x,y,c) e subt]

            U Spec, 205

 

      207  EXIST(c):[c e n & (x,y,c) e subt]

            Detach, 206, 204

 

      208  z e n & (x,y,z) e subt

            E Spec, 207

 

      209  z e n

            Split, 208

 

      210  (x,y,z) e subt

            Split, 208

 

      211  ALL(b2):ALL(c):[(x,b2) e dom & c e n => [subt(x,b2)=c <=> (x,b2,c) e subt]]

            U Spec, 185

 

      212  ALL(c):[(x,y) e dom & c e n => [subt(x,y)=c <=> (x,y,c) e subt]]

            U Spec, 211

 

      213  (x,y) e dom & z e n => [subt(x,y)=z <=> (x,y,z) e subt]

            U Spec, 212

 

      214  (x,y) e dom & z e n

            Join, 204, 209

 

      215  subt(x,y)=z <=> (x,y,z) e subt

            Detach, 213, 214

 

      216  [subt(x,y)=z => (x,y,z) e subt]

         & [(x,y,z) e subt => subt(x,y)=z]

            Iff-And, 215

 

      217  subt(x,y)=z => (x,y,z) e subt

            Split, 216

 

      218  (x,y,z) e subt => subt(x,y)=z

            Split, 216

 

      219  subt(x,y)=z

            Detach, 218, 210

 

      220  ALL(b):ALL(c):[(x,b,c) e subt

         <=> (x,b,c) e n3 & [(x,b) e dom & x=b+c]]

            U Spec, 30

 

      221  ALL(c):[(x,y,c) e subt

         <=> (x,y,c) e n3 & [(x,y) e dom & x=y+c]]

            U Spec, 220

 

      222  (x,y,z) e subt

         <=> (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            U Spec, 221

 

      223  [(x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]]

         & [(x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt]

            Iff-And, 222

 

      224  (x,y,z) e subt => (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            Split, 223

 

      225  (x,y,z) e n3 & [(x,y) e dom & x=y+z] => (x,y,z) e subt

            Split, 223

 

      226  (x,y,z) e n3 & [(x,y) e dom & x=y+z]

            Detach, 224, 210

 

      227  (x,y,z) e n3

            Split, 226

 

      228  (x,y) e dom & x=y+z

            Split, 226

 

      229  (x,y) e dom

            Split, 228

 

      230  x=y+z

            Split, 228

 

      231  x=y+subt(x,y)

            Substitute, 219, 230

 

As Required:

 

232  ALL(a):ALL(b):[(a,b) e dom => a=b+subt(a,b)]

      4 Conclusion, 204

 

   

    Prove: ALL(a):ALL(b):[a e n & b e n => [b<=a => a=b+subt(a,b)]]

   

    Suppose...

 

      233  x e n & y e n

            Premise

 

      234  x e n

            Split, 233

 

      235  y e n

            Split, 233

 

        

         Prove: y<=x => x=y+subt(x,y)

        

         Suppose...

 

            236  y<=x

                  Premise

 

            237  ALL(b):[(x,b) e dom => x=b+subt(x,b)]

                  U Spec, 232

 

            238  (x,y) e dom => x=y+subt(x,y)

                  U Spec, 237

 

            239  ALL(b):[(x,b) e dom <=> (x,b) e n2 & b<=x]

                  U Spec, 17

 

            240  (x,y) e dom <=> (x,y) e n2 & y<=x

                  U Spec, 239

 

            241  [(x,y) e dom => (x,y) e n2 & y<=x]

             & [(x,y) e n2 & y<=x => (x,y) e dom]

                  Iff-And, 240

 

            242  (x,y) e dom => (x,y) e n2 & y<=x

                  Split, 241

 

            243  (x,y) e n2 & y<=x => (x,y) e dom

                  Split, 241

 

            244  ALL(c2):[(x,c2) e n2 <=> x e n & c2 e n]

                  U Spec, 13

 

            245  (x,y) e n2 <=> x e n & y e n

                  U Spec, 244

 

            246  [(x,y) e n2 => x e n & y e n]

             & [x e n & y e n => (x,y) e n2]

                  Iff-And, 245

 

            247  (x,y) e n2 => x e n & y e n

                  Split, 246

 

            248  x e n & y e n => (x,y) e n2

                  Split, 246

 

            249  (x,y) e n2

                  Detach, 248, 233

 

            250  (x,y) e n2 & y<=x

                  Join, 249, 236

 

            251  (x,y) e dom

                  Detach, 243, 250

 

            252  x=y+subt(x,y)

                  Detach, 238, 251

 

            253  ALL(b):[(x,b) e dom => subt(x,b) e n]

                  U Spec, 203

 

            254  (x,y) e dom => subt(x,y) e n

                  U Spec, 253

 

            255  subt(x,y) e n

                  Detach, 254, 251

 

            256  subt(x,y) e n & x=y+subt(x,y)

                  Join, 255, 252

 

    As Required:

 

      257  y<=x => subt(x,y) e n & x=y+subt(x,y)

            4 Conclusion, 236

 

As Required:

 

258  ALL(a):ALL(b):[a e n & b e n

    => [b<=a => subt(a,b) e n & a=b+subt(a,b)]]

      4 Conclusion, 233

 

As Required:

 

259  EXIST(subt):ALL(a):ALL(b):[a e n & b e n

    => [b<=a => subt(a,b) e n & a=b+subt(a,b)]]

      E Gen, 258