THEOREM

*******

There exists a unique exponent function on n with 0^0 left undefined.

Existence of exp(a,b):

EXIST(exp):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]

& exp(0,1)=0

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

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

Uniqueness of exp(a,b):

ALL(exp):ALL(exp'):[ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b) e n]]

& exp(0,1)=0

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

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

=> [~[a=0 & b=0] => exp(a,b+1)=exp(a,b)*a]]

& [ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

& exp'(0,1)=0

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

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

=> [~[a=0 & b=0] => exp'(a,b+1)=exp'(a,b)*a]]]

=> ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp(a,b)=exp'(a,b)]]]

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

Dan Christensen

2019-10-17

AXIOMS/DEFINITIONS

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

Define: n, 0, 1

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

1     Set(n)

Axiom

2     0 e n

Axiom

3     1 e n

Axiom

4     ~1=0

Axiom

5     0+1=1

Axiom

Properties of +

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

Closed on n

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

Axiom

Adding 0

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

Axiom

+ Commutative

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

Axiom

+ Right cancelable

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

Axiom

0 is "first" number

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

Axiom

Principle of Mathematical Induction

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

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

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

Axiom

Properties of *

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

Closed on n

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

Axiom

Multiplying by 0

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

Axiom

Multiplying by 1

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

Axiom

* Commutative

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

Axiom

Function Axiom (2 varibles)

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

16   ALL(f):ALL(dom):ALL(cod):[Set''(f) & Set'(dom) & Set(cod)

=> [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]

& ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e f]]

& ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

=> [(a1,a2,b1) e f & (a1,a2,b2) e f => b1=b2]]

=> ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=> (a1,a2,b) e f]]]]

Function

PREVIOUS RESULT

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

There exists infinitely many exponent-like functions starting with exponent 0    Proof

17   ALL(x0):[x0 e n

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

& exp(0,0)=x0

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

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

Axiom

PROOF

*****

Suppose...

18   x0 e n

Premise

Apply previous result

19   x0 e n

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

& exp(0,0)=x0

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

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

U Spec, 17

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

& exp(0,0)=x0

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

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

Detach, 19, 18

21   ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

& exp(0,0)=x0

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

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

E Spec, 20

Define: exp

***********

22   ALL(a):ALL(b):[a e n & b e n => exp(a,b) e n]

Split, 21

23   exp(0,0)=x0

Split, 21

24   ALL(a):[a e n => [~a=0 => exp(a,0)=1]]

Split, 21

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

Split, 21

Construct n2

26   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

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

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

U Spec, 27

29   Set(n) & Set(n)

Join, 1, 1

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

Detach, 28, 29

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

E Spec, 30

Define: n2

32   Set'(n2)

Split, 31

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

Split, 31

Construct n3

34   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

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

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

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

38   Set(n) & Set(n)

Join, 1, 1

39   Set(n) & Set(n) & Set(n)

Join, 38, 1

40   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, 37, 39

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

E Spec, 40

Define: n3

42   Set''(n3)

Split, 41

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

Split, 41

Construct dom

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

Subset, 32

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

E Spec, 44

Define: dom

46   Set'(dom)

Split, 45

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

Split, 45

Construct exp'

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

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

Subset, 42

49   Set''(exp') & ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'

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

E Spec, 48

Define: exp'

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

50   Set''(exp')

Split, 49

51   ALL(a):ALL(b):ALL(c):[(a,b,c) e exp'

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

Split, 49

Apply Function Axioms (for 2 variables)

52   ALL(f):ALL(dom):ALL(cod):[Set''(f) & Set'(dom) & Set(cod)

=> [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e f => (a1,a2) e dom & b e cod]

& ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e f]]

& ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

=> [(a1,a2,b1) e f & (a1,a2,b2) e f => b1=b2]]

=> ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [f(a1,a2)=b <=> (a1,a2,b) e f]]]]

Function

53   ALL(dom):ALL(cod):[Set''(exp') & Set'(dom) & Set(cod)

=> [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e cod]

& ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e exp']]

& ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

=> [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

=> ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]]]

U Spec, 52

54   ALL(cod):[Set''(exp') & Set'(dom) & Set(cod)

=> [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e cod]

& ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e cod & (a1,a2,b) e exp']]

& ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e cod & b2 e cod

=> [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

=> ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e cod => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]]]

U Spec, 53

55   Set''(exp') & Set'(dom) & Set(n)

=> [ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

& ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

& ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

=> [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

=> ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]]

U Spec, 54

56   Set''(exp') & Set'(dom)

Join, 50, 46

57   Set''(exp') & Set'(dom) & Set(n)

Join, 56, 1

Sufficient: For functionality of exp'

58   ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

& ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

& ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

=> [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

=> ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]

Detach, 55, 57

Prove: ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

Suppose...

59   (x,y,z) e exp'

Premise

Apply definition of exp'

60   ALL(b):ALL(c):[(x,b,c) e exp'

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

U Spec, 51

61   ALL(c):[(x,y,c) e exp'

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

U Spec, 60

62   (x,y,z) e exp'

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

U Spec, 61

63   [(x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]]

& [(x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp']

Iff-And, 62

64   (x,y,z) e exp' => (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

Split, 63

65   (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)] => (x,y,z) e exp'

Split, 63

66   (x,y,z) e n3 & [~[x=0 & y=0] & z=exp(x,y)]

Detach, 64, 59

67   (x,y,z) e n3

Split, 66

68   ~[x=0 & y=0] & z=exp(x,y)

Split, 66

69   ~[x=0 & y=0]

Split, 68

70   z=exp(x,y)

Split, 68

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

U Spec, 47

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

U Spec, 71

73   [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

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

Iff-And, 72

74   (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

Split, 73

Apply definition of n3

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

U Spec, 43

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

U Spec, 75

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

U Spec, 76

78   [(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, 77

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

Split, 78

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

Split, 78

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

Detach, 79, 67

82   x e n

Split, 81

83   y e n

Split, 81

84   z e n

Split, 81

Sufficient: For (x,y) e dom

85   (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

Split, 73

Apply definition of n3

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

U Spec, 43

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

U Spec, 86

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

U Spec, 87

89   [(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, 88

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

Split, 89

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

Split, 89

92   x e n & y e n & z e n

Detach, 90, 67

93   x e n

Split, 92

94   y e n

Split, 92

95   z e n

Split, 92

Apply definition of n2

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

U Spec, 33

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

U Spec, 96

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

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

Iff-And, 97

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

Split, 98

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

Split, 98

101  x e n & y e n

Join, 82, 83

102  (x,y) e n2

Detach, 100, 101

103  (x,y) e n2 & ~[x=0 & y=0]

Join, 102, 69

104  (x,y) e dom

Detach, 85, 103

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

Join, 104, 84

Functionality of exp', Part 1

106  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

4 Conclusion, 59

Prove: ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

Suppose...

107  (x,y) e dom

Premise

Apply definition of dom

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

U Spec, 47

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

U Spec, 108

110  [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

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

Iff-And, 109

111  (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

Split, 110

112  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

Split, 110

113  (x,y) e n2 & ~[x=0 & y=0]

Detach, 111, 107

114  (x,y) e n2

Split, 113

115  ~[x=0 & y=0]

Split, 113

Apply definition of exp'

116  ALL(b):ALL(c):[(x,b,c) e exp'

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

U Spec, 51

117  ALL(c):[(x,y,c) e exp'

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

U Spec, 116

118  ALL(b):[x e n & b e n => exp(x,b) e n]

U Spec, 22

119  x e n & y e n => exp(x,y) e n

U Spec, 118

Apply definition of n2

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

U Spec, 33

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

U Spec, 120

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

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

Iff-And, 121

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

Split, 122

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

Split, 122

125  x e n & y e n

Detach, 123, 114

126  x e n

Split, 125

127  y e n

Split, 125

128  exp(x,y) e n

Detach, 119, 125

129  (x,y,exp(x,y)) e exp'

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

U Spec, 117, 128

130  [(x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]]

& [(x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp']

Iff-And, 129

131  (x,y,exp(x,y)) e exp' => (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)]

Split, 130

Sufficient: For (x,y,exp(x,y)) e exp'

132  (x,y,exp(x,y)) e n3 & [~[x=0 & y=0] & exp(x,y)=exp(x,y)] => (x,y,exp(x,y)) e exp'

Split, 130

Apply definition of n3

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

U Spec, 43

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

U Spec, 133

135  (x,y,exp(x,y)) e n3 <=> x e n & y e n & exp(x,y) e n

U Spec, 134, 128

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

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

Iff-And, 135

137  (x,y,exp(x,y)) e n3 => x e n & y e n & exp(x,y) e n

Split, 136

Sufficient: For (x,y,exp(x,y)) e n3

138  x e n & y e n & exp(x,y) e n => (x,y,exp(x,y)) e n3

Split, 136

139  x e n & y e n & exp(x,y) e n

Join, 125, 128

140  (x,y,exp(x,y)) e n3

Detach, 138, 139

141  exp(x,y)=exp(x,y)

Reflex, 128

142  ~[x=0 & y=0] & exp(x,y)=exp(x,y)

Join, 115, 141

143  (x,y,exp(x,y)) e n3

& [~[x=0 & y=0] & exp(x,y)=exp(x,y)]

Join, 140, 142

144  (x,y,exp(x,y)) e exp'

Detach, 132, 143

145  exp(x,y) e n & (x,y,exp(x,y)) e exp'

Join, 128, 144

146  EXIST(b):[b e n & (x,y,b) e exp']

E Gen, 145

Functionality of exp', Part 2

147  ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

4 Conclusion, 107

Prove: ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

=> [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

Suppose...

148  (x,y) e dom & z1 e n & z2 e n

Premise

149  (x,y) e dom

Split, 148

150  z1 e n

Split, 148

151  z2 e n

Split, 148

Suppose...

152  (x,y,z1) e exp' & (x,y,z2) e exp'

Premise

153  (x,y,z1) e exp'

Split, 152

154  (x,y,z2) e exp'

Split, 152

Apply the definition of exp'

155  ALL(b):ALL(c):[(x,b,c) e exp'

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

U Spec, 51

156  ALL(c):[(x,y,c) e exp'

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

U Spec, 155

157  (x,y,z1) e exp'

<=> (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

U Spec, 156

158  [(x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]]

& [(x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp']

Iff-And, 157

159  (x,y,z1) e exp' => (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

Split, 158

160  (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)] => (x,y,z1) e exp'

Split, 158

161  (x,y,z1) e n3 & [~[x=0 & y=0] & z1=exp(x,y)]

Detach, 159, 153

162  (x,y,z1) e n3

Split, 161

163  ~[x=0 & y=0] & z1=exp(x,y)

Split, 161

164  ~[x=0 & y=0]

Split, 163

165  z1=exp(x,y)

Split, 163

166  (x,y,z2) e exp'

<=> (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

U Spec, 156

167  [(x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]]

& [(x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp']

Iff-And, 166

168  (x,y,z2) e exp' => (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

Split, 167

169  (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)] => (x,y,z2) e exp'

Split, 167

170  (x,y,z2) e n3 & [~[x=0 & y=0] & z2=exp(x,y)]

Detach, 168, 154

171  (x,y,z2) e n3

Split, 170

172  ~[x=0 & y=0] & z2=exp(x,y)

Split, 170

173  ~[x=0 & y=0]

Split, 172

174  z2=exp(x,y)

Split, 172

175  z1=z2

Substitute, 174, 165

176  (x,y,z1) e exp' & (x,y,z2) e exp' => z1=z2

4 Conclusion, 152

Functionality of exp', Part 3

177  ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

=> [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

4 Conclusion, 148

Joining results...

178  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

& ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

Join, 106, 147

179  ALL(a1):ALL(a2):ALL(b):[(a1,a2,b) e exp' => (a1,a2) e dom & b e n]

& ALL(a1):ALL(a2):[(a1,a2) e dom => EXIST(b):[b e n & (a1,a2,b) e exp']]

& ALL(a1):ALL(a2):ALL(b1):ALL(b2):[(a1,a2) e dom & b1 e n & b2 e n

=> [(a1,a2,b1) e exp' & (a1,a2,b2) e exp' => b1=b2]]

Join, 178, 177

exp' is a partial binary function on n

As Required:

180  ALL(a1):ALL(a2):ALL(b):[(a1,a2) e dom & b e n => [exp'(a1,a2)=b <=> (a1,a2,b) e exp']]

Detach, 58, 179

Prove: ALL(x):ALL(y):[x e n & y e n => [~[x=0 & y=0] => exp'(x,y) e n]]

Suppose...

181  x e n & y e n

Premise

Prove: ~[x=0 & y=0] => exp'(x,y) e n

Suppose...

182  ~[x=0 & y=0]

Premise

Apply definition of exp'

183  ALL(a2):[(x,a2) e dom => EXIST(b):[b e n & (x,a2,b) e exp']]

U Spec, 147

184  (x,y) e dom => EXIST(b):[b e n & (x,y,b) e exp']

U Spec, 183

Apply definition of dom

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

U Spec, 47

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

U Spec, 185

187  [(x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]]

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

Iff-And, 186

188  (x,y) e dom => (x,y) e n2 & ~[x=0 & y=0]

Split, 187

189  (x,y) e n2 & ~[x=0 & y=0] => (x,y) e dom

Split, 187

Apply definition of n2

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

U Spec, 33

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

U Spec, 190

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

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

Iff-And, 191

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

Split, 192

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

Split, 192

195  (x,y) e n2

Detach, 194, 181

196  (x,y) e n2 & ~[x=0 & y=0]

Join, 195, 182

197  (x,y) e dom

Detach, 189, 196

198  EXIST(b):[b e n & (x,y,b) e exp']

Detach, 184, 197

199  z e n & (x,y,z) e exp'

E Spec, 198

200  z e n

Split, 199

201  (x,y,z) e exp'

Split, 199

Apply previous result

202  ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=> (x,a2,b) e exp']]

U Spec, 180

203  ALL(b):[(x,y) e dom & b e n => [exp'(x,y)=b <=> (x,y,b) e exp']]

U Spec, 202

204  (x,y) e dom & z e n => [exp'(x,y)=z <=> (x,y,z) e exp']

U Spec, 203

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

Join, 197, 200

206  exp'(x,y)=z <=> (x,y,z) e exp'

Detach, 204, 205

207  [exp'(x,y)=z => (x,y,z) e exp']

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

Iff-And, 206

208  exp'(x,y)=z => (x,y,z) e exp'

Split, 207

209  (x,y,z) e exp' => exp'(x,y)=z

Split, 207

210  exp'(x,y)=z

Detach, 209, 201

211  exp'(x,y) e n

Substitute, 210, 200

As Required:

212  ~[x=0 & y=0] => exp'(x,y) e n

4 Conclusion, 182

As Required:

213  ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => exp'(a,b) e n]]

4 Conclusion, 181

Prove: exp'(0,1)=0

Apply definition of exp'

214  ALL(b):ALL(c):[(0,b,c) e exp'

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

U Spec, 51

215  ALL(c):[(0,1,c) e exp'

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

U Spec, 214

216  (0,1,0) e exp'

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

U Spec, 215

217  [(0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]]

& [(0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp']

Iff-And, 216

218  (0,1,0) e exp' => (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]

Split, 217

Sufficient: For (0,1,0) e exp'

219  (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)] => (0,1,0) e exp'

Split, 217

Apply definition of n3

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

U Spec, 43

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

U Spec, 220

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

U Spec, 221

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

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

Iff-And, 222

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

Split, 223

225  0 e n & 1 e n & 0 e n => (0,1,0) e n3

Split, 223

226  0 e n & 1 e n

Join, 2, 3

227  0 e n & 1 e n & 0 e n

Join, 226, 2

228  (0,1,0) e n3

Detach, 225, 227

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

Suppose to the contrary...

229  0=0 & 1=0

Premise

230  0=0

Split, 229

231  1=0

Split, 229

232  1=0 & ~1=0

Join, 231, 4

233  ~[0=0 & 1=0]

4 Conclusion, 229

Apply definition of exp

234  ALL(b):[0 e n & b e n => exp(0,b+1)=exp(0,b)*0]

U Spec, 25

235  0 e n & 0 e n => exp(0,0+1)=exp(0,0)*0

U Spec, 234

236  0 e n & 0 e n

Join, 2, 2

237  exp(0,0+1)=exp(0,0)*0

Detach, 235, 236

238  ALL(b):[0 e n & b e n => 0+b=b+0]

U Spec, 8

239  0 e n & 1 e n => 0+1=1+0

U Spec, 238

240  0 e n & 1 e n

Join, 2, 3

241  0+1=1+0

Detach, 239, 240

242  1 e n => 1+0=1

U Spec, 7

243  1+0=1

Detach, 242, 3

244  0+1=1

Substitute, 243, 241

245  exp(0,1)=exp(0,0)*0

Substitute, 244, 237

246  ALL(b):[0 e n & b e n => exp(0,b) e n]

U Spec, 22

247  0 e n & 0 e n => exp(0,0) e n

U Spec, 246

248  0 e n & 0 e n

Join, 2, 2

249  exp(0,0) e n

Detach, 247, 248

250  exp(0,0) e n => exp(0,0)*0=0

U Spec, 13, 249

251  exp(0,0)*0=0

Detach, 250, 249

252  exp(0,1)=0

Substitute, 251, 245

253  0=exp(0,1)

Sym, 252

254  ~[0=0 & 1=0] & 0=exp(0,1)

Join, 233, 253

255  (0,1,0) e n3 & [~[0=0 & 1=0] & 0=exp(0,1)]

Join, 228, 254

256  (0,1,0) e exp'

Detach, 219, 255

Apply previous result

257  ALL(a2):ALL(b):[(0,a2) e dom & b e n => [exp'(0,a2)=b <=> (0,a2,b) e exp']]

U Spec, 180

258  ALL(b):[(0,1) e dom & b e n => [exp'(0,1)=b <=> (0,1,b) e exp']]

U Spec, 257

259  (0,1) e dom & 0 e n => [exp'(0,1)=0 <=> (0,1,0) e exp']

U Spec, 258

Apply defintion of dom

260  ALL(b):[(0,b) e dom <=> (0,b) e n2 & ~[0=0 & b=0]]

U Spec, 47

261  (0,1) e dom <=> (0,1) e n2 & ~[0=0 & 1=0]

U Spec, 260

262  [(0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]]

& [(0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom]

Iff-And, 261

263  (0,1) e dom => (0,1) e n2 & ~[0=0 & 1=0]

Split, 262

264  (0,1) e n2 & ~[0=0 & 1=0] => (0,1) e dom

Split, 262

265  ALL(c2):[(0,c2) e n2 <=> 0 e n & c2 e n]

U Spec, 33

266  (0,1) e n2 <=> 0 e n & 1 e n

U Spec, 265

267  [(0,1) e n2 => 0 e n & 1 e n]

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

Iff-And, 266

268  (0,1) e n2 => 0 e n & 1 e n

Split, 267

269  0 e n & 1 e n => (0,1) e n2

Split, 267

270  0 e n & 1 e n

Join, 2, 3

271  (0,1) e n2

Detach, 269, 270

272  0=0 & 1=0

Premise

273  0=0

Split, 272

274  1=0

Split, 272

275  1=0 & ~1=0

Join, 274, 4

276  ~[0=0 & 1=0]

4 Conclusion, 272

277  (0,1) e n2 & ~[0=0 & 1=0]

Join, 271, 276

278  (0,1) e dom

Detach, 264, 277

279  (0,1) e dom & 0 e n

Join, 278, 2

280  exp'(0,1)=0 <=> (0,1,0) e exp'

Detach, 259, 279

281  [exp'(0,1)=0 => (0,1,0) e exp']

& [(0,1,0) e exp' => exp'(0,1)=0]

Iff-And, 280

282  exp'(0,1)=0 => (0,1,0) e exp'

Split, 281

283  (0,1,0) e exp' => exp'(0,1)=0

Split, 281

As Required:

284  exp'(0,1)=0

Detach, 283, 256

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

Suppose...

285  x e n

Premise

Prove: ~x=0 => exp'(x,0)=1

Suppose...

286  ~x=0

Premise

287  ALL(b):ALL(c):[(x,b,c) e exp'

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

U Spec, 51

288  ALL(c):[(x,0,c) e exp'

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

U Spec, 287

289  (x,0,1) e exp'

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

U Spec, 288

290  [(x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]]

& [(x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp']

Iff-And, 289

291  (x,0,1) e exp' => (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]

Split, 290

Sufficient: For (x,0,1) e exp'

292  (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)] => (x,0,1) e exp'

Split, 290

Apply definition of n3

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

U Spec, 43

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

U Spec, 293

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

U Spec, 294

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

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

Iff-And, 295

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

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

Iff-And, 295

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

Split, 297

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

Split, 297

300  x e n & 0 e n

Join, 285, 2

301  x e n & 0 e n & 1 e n

Join, 300, 3

302  (x,0,1) e n3

Detach, 299, 301

303  x=0 & 0=0

Premise

304  x=0

Split, 303

305  0=0

Split, 303

306  x=0 & ~x=0

Join, 304, 286

307  ~[x=0 & 0=0]

4 Conclusion, 303

Apply definition of exp

308  x e n => [~x=0 => exp(x,0)=1]

U Spec, 24

309  ~x=0 => exp(x,0)=1

Detach, 308, 285

310  exp(x,0)=1

Detach, 309, 286

311  1=exp(x,0)

Sym, 310

312  ~[x=0 & 0=0] & 1=exp(x,0)

Join, 307, 311

313  (x,0,1) e n3 & [~[x=0 & 0=0] & 1=exp(x,0)]

Join, 302, 312

314  (x,0,1) e exp'

Detach, 292, 313

315  ALL(a2):ALL(b):[(x,a2) e dom & b e n => [exp'(x,a2)=b <=> (x,a2,b) e exp']]

U Spec, 180

316  ALL(b):[(x,0) e dom & b e n => [exp'(x,0)=b <=> (x,0,b) e exp']]

U Spec, 315

317  (x,0) e dom & 1 e n => [exp'(x,0)=1 <=> (x,0,1) e exp']

U Spec, 316

Apply definition of dom

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

U Spec, 47

319  (x,0) e dom <=> (x,0) e n2 & ~[x=0 & 0=0]

U Spec, 318

320  [(x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]]

& [(x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom]

Iff-And, 319

321  (x,0) e dom => (x,0) e n2 & ~[x=0 & 0=0]

Split, 320

322  (x,0) e n2 & ~[x=0 & 0=0] => (x,0) e dom

Split, 320

Apply definition of n2

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

U Spec, 33

324  (x,0) e n2 <=> x e n & 0 e n

U Spec, 323

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

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

Iff-And, 324

326  (x,0) e n2 => x e n & 0 e n

Split, 325

327  x e n & 0 e n => (x,0) e n2

Split, 325

328  x e n & 0 e n

Join, 285, 2

329  (x,0) e n2

Detach, 327, 328

330  x=0 & 0=0

Premise

331  x=0

Split, 330

332  0=0

Split, 330

333  x=0 & ~x=0

Join, 331, 286

334  ~[x=0 & 0=0]

4 Conclusion, 330

335  (x,0) e n2 & ~[x=0 & 0=0]

Join, 329, 334

336  (x,0) e dom

Detach, 322, 335

337  (x,0) e dom & 1 e n

Join, 336, 3

338  exp'(x,0)=1 <=> (x,0,1