THEOREM

*******

In the context of exponentiation on N, starting with exponent 0 is equivalent to starting with exponent 2.

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

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

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

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

Dan Christensen

2019-10-16

AXIOMS/DEFINITIONS

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

Define: n, 0, 1, 2

1 Set(n)

Axiom

2 0 e n

Axiom

3 1 e n

Axiom

4 2 e n

Axiom

5 2=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

Properties of *

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

Closed on n

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

Axiom

Multplying by 0

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

Axiom

Multiplying by 1

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

Axiom

Commutative

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

Axiom

Right cancelability of non-zero factors for *

13 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~b=0 => [a*b=c*b => a=c]]]

Axiom

PROOF

*****

Suppose exp is a binary function n

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

Premise

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

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

Suppose...

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

Premise

'=>'

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

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

Premise

Prove: ALL(a):[a e n => exp(a,2)=a*a]

Let x be the base

17 x e n

Premise

Two cases to consider:

18 x=0 | ~x=0

Or Not

Case 1

Prove: x=0 => exp(x,2)=x*x

Suppose...

19 x=0

Premise

Apply definition of exp

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

U Spec, 15

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

U Spec, 20

22 0 e n & 0 e n

Join, 2, 2

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

Detach, 21, 22

24 1 e n => 1+0=1

U Spec, 7

25 1+0=1

Detach, 24, 3

26 1 e n => 1+0=1

U Spec, 7

27 1+0=1

Detach, 26, 3

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

U Spec, 8

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

U Spec, 28

30 1 e n & 0 e n

Join, 3, 2

31 1+0=0+1

Detach, 29, 30

32 0+1=1

Substitute, 31, 27

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

Substitute, 32, 23

Apply definition of exp

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

U Spec, 14

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

U Spec, 34

36 0 e n & 0 e n

Join, 2, 2

37 exp(0,0) e n

Detach, 35, 36

Apply definition of exp

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

U Spec, 10, 37

39 exp(0,0)*0=0

Detach, 38, 37

40 exp(0,1)=0

Substitute, 39, 33

Apply defintion of exp

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

U Spec, 15

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

U Spec, 41

43 0 e n & 1 e n

Join, 2, 3

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

Detach, 42, 43

45 exp(0,2)=exp(0,1)*0

Substitute, 5, 44

46 exp(0,2)=0*0

Substitute, 40, 45

47 exp(x,2)=x*x

Substitute, 19, 46

Case 1

As Required:

48 x=0 => exp(x,2)=x*x

4 Conclusion, 19

Case 2

Prove: ~x=0 => exp(x,2)=x*x

Suppose...

49 ~x=0

Premise

Apply definition of exp

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

U Spec, 16

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

Detach, 50, 17

52 exp(x,0)=1

Detach, 51, 49

Apply definition of exp

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

U Spec, 15

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

U Spec, 53

55 x e n & 0 e n

Join, 17, 2

56 exp(x,0+1)=exp(x,0)*x

Detach, 54, 55

Apply axiom

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

U Spec, 8

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

U Spec, 57

59 0 e n & 1 e n

Join, 2, 3

60 0+1=1+0

Detach, 58, 59

61 1 e n => 1+0=1

U Spec, 7

62 1+0=1

Detach, 61, 3

63 0+1=1

Substitute, 62, 60

64 exp(x,1)=exp(x,0)*x

Substitute, 63, 56

65 exp(x,1)=1*x

Substitute, 52, 64

Apply axiom

66 ALL(b):[1 e n & b e n => 1*b=b*1]

U Spec, 12

67 1 e n & x e n => 1*x=x*1

U Spec, 66

68 1 e n & x e n

Join, 3, 17

69 1*x=x*1

Detach, 67, 68

70 x e n => x*1=x

U Spec, 11

71 x*1=x

Detach, 70, 17

72 1*x=x

Substitute, 71, 69

73 exp(x,1)=x

Substitute, 72, 65

Apply definition of exp

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

U Spec, 15

75 x e n & 1 e n => exp(x,1+1)=exp(x,1)*x

U Spec, 74

76 x e n & 1 e n

Join, 17, 3

77 exp(x,1+1)=exp(x,1)*x

Detach, 75, 76

78 exp(x,2)=exp(x,1)*x

Substitute, 5, 77

79 exp(x,2)=x*x

Substitute, 73, 78

Case 2:

As Required:

80 ~x=0 => exp(x,2)=x*x

4 Conclusion, 49

81 [x=0 => exp(x,2)=x*x] & [~x=0 => exp(x,2)=x*x]

Join, 48, 80

82 exp(x,2)=x*x

Cases, 18, 81

As Required:

83 ALL(a):[a e n => exp(a,2)=a*a]

4 Conclusion, 17

As Required:

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

=> ALL(a):[a e n => exp(a,2)=a*a]

4 Conclusion, 16

'<='

Prove: ALL(a):[a e n => exp(a,2)=a*a]

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

Suppose...

85 ALL(a):[a e n => exp(a,2)=a*a]

Premise

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

Suppose...

86 x e n

Premise

Apply definition of exp

87 x e n => exp(x,2)=x*x

U Spec, 85

88 exp(x,2)=x*x

Detach, 87, 86

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

Suppose...

89 ~x=0

Premise

Apply definition of exp

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

U Spec, 15

91 x e n & 1 e n => exp(x,1+1)=exp(x,1)*x

U Spec, 90

92 x e n & 1 e n

Join, 86, 3

93 exp(x,1+1)=exp(x,1)*x

Detach, 91, 92

94 exp(x,2)=exp(x,1)*x

Substitute, 5, 93

95 x*x=exp(x,1)*x

Substitute, 88, 94

Apply axiom

96 ALL(b):ALL(c):[x e n & b e n & c e n => [~b=0 => [x*b=c*b => x=c]]]

U Spec, 13

97 ALL(c):[x e n & x e n & c e n => [~x=0 => [x*x=c*x => x=c]]]

U Spec, 96

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

U Spec, 14

99 x e n & 1 e n => exp(x,1) e n

U Spec, 98

100 x e n & 1 e n

Join, 86, 3

101 exp(x,1) e n

Detach, 99, 100

102 x e n & x e n & exp(x,1) e n => [~x=0 => [x*x=exp(x,1)*x => x=exp(x,1)]]

U Spec, 97, 101

103 x e n & x e n

Join, 86, 86

104 x e n & x e n & exp(x,1) e n

Join, 103, 101

105 ~x=0 => [x*x=exp(x,1)*x => x=exp(x,1)]

Detach, 102, 104

106 x*x=exp(x,1)*x => x=exp(x,1)

Detach, 105, 89

107 x=exp(x,1)

Detach, 106, 95

108 exp(x,1)=x

Sym, 107

Apply definition of exp

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

U Spec, 15

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

U Spec, 109

111 x e n & 0 e n

Join, 86, 2

112 exp(x,0+1)=exp(x,0)*x

Detach, 110, 111

Apply axiom

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

U Spec, 8

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

U Spec, 113

115 0 e n & 1 e n

Join, 2, 3

116 0+1=1+0

Detach, 114, 115

117 1 e n => 1+0=1

U Spec, 7

118 1+0=1

Detach, 117, 3

119 0+1=1

Substitute, 118, 116

120 exp(x,1)=exp(x,0)*x

Substitute, 119, 112

121 x=exp(x,0)*x

Substitute, 108, 120

122 x e n => x*1=x

U Spec, 11

123 x*1=x

Detach, 122, 86

Apply axiom

124 ALL(b):[x e n & b e n => x*b=b*x]

U Spec, 12

125 x e n & 1 e n => x*1=1*x

U Spec, 124

126 x e n & 1 e n

Join, 86, 3

127 x*1=1*x

Detach, 125, 126

128 1*x=x

Substitute, 127, 123

129 1*x=exp(x,0)*x

Substitute, 128, 121

Apply axiom

130 ALL(b):ALL(c):[1 e n & b e n & c e n => [~b=0 => [1*b=c*b => 1=c]]]

U Spec, 13

131 ALL(c):[1 e n & x e n & c e n => [~x=0 => [1*x=c*x => 1=c]]]

U Spec, 130

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

U Spec, 14

133 x e n & 0 e n => exp(x,0) e n

U Spec, 132

134 x e n & 0 e n

Join, 86, 2

135 exp(x,0) e n

Detach, 133, 134

136 1 e n & x e n & exp(x,0) e n => [~x=0 => [1*x=exp(x,0)*x => 1=exp(x,0)]]

U Spec, 131, 135

137 1 e n & x e n

Join, 3, 86

138 1 e n & x e n & exp(x,0) e n

Join, 137, 135

139 ~x=0 => [1*x=exp(x,0)*x => 1=exp(x,0)]

Detach, 136, 138

140 1*x=exp(x,0)*x => 1=exp(x,0)

Detach, 139, 89

141 1=exp(x,0)

Detach, 140, 129

142 exp(x,0)=1

Sym, 141

As Required:

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

4 Conclusion, 89

As Required:

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

4 Conclusion, 86

As Required:

145 ALL(a):[a e n => exp(a,2)=a*a]

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

4 Conclusion, 85

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

=> ALL(a):[a e n => exp(a,2)=a*a]]

& [ALL(a):[a e n => exp(a,2)=a*a]

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

Join, 84, 145

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

<=> ALL(a):[a e n => exp(a,2)=a*a]

Iff-And, 146

As Required:

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

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

<=> ALL(a):[a e n => exp(a,2)=a*a]]

4 Conclusion, 15

As Required:

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

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

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

<=> ALL(a):[a e n => exp(a,2)=a*a]]]]

4 Conclusion, 14