THEOREM 3
*********
3^0 = 1, 3^1 = 3, 3^2 = 9
By Dan Christensen
October 2013
(This proof was written with the aid of the author's DC Proof software available at http://www.dcproof.com )
BASIC PRINCIPLES OF ARITHMETIC USED
***********************************
n is a set (the set of natural numbers)
1 Set(n)
Axiom
+ is a binary function on n
2 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
* is a binary function on n
3 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
4 0 e n
Axiom
5 1 e n
Axiom
6 2 e n
Axiom
7 2=1+1
Axiom
8 3 e n
Axiom
9 ~3=0
Axiom
10 3=2+1
Axiom
11 9 e n
Axiom
12 9=3*3
Axiom
13 ALL(a):[a e n => a+0=a]
Axiom
14 ALL(a):[a e n => a*0=0]
Axiom
15 ALL(a):[a e n => a*1=a]
Axiom
The principle of mathematical induction (PMI)
16 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
Associativity of +
17 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a+b+c=a+(b+c)]
Axiom
Commutativity of +
18 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
Distributivity of * over +
19 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*(b+c)=a*b+a*c]
Axiom
Associativity of *
20 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a*b*c=a*(b*c)]
Axiom
Commutativity of *
21 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Right cancelability of +
22 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=c+b => a=c]]
Axiom
0 has no predecessor
23 ALL(a):[a e n => ~a+1=0]
Axiom
Existence of a predecessor
24 ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & b+1=a]]]
Axiom
Product of Powers Rule (previous result)
25 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~a=0 => a^(b+c)=a^b*a^c]]
Axiom
Power of a non-zero base (previous result)
26 ALL(a):ALL(b):[a e n & b e n => [~a=0 => ~a^b=0]]
Axiom
Define: ^ (0^0 is an unspecified natural number)
*********
27 ALL(a):ALL(b):[a e n & b e n => a^b e n]
& ALL(a):[a e n => [~a=0 => a^0=1]]
& ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Premise
28 ALL(a):ALL(b):[a e n & b e n => a^b e n]
Split, 27
29 ALL(a):[a e n => [~a=0 => a^0=1]]
Split, 27
30 ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Split, 27
Prove: 3^0=1
Apply definition of ^
31 3 e n => [~3=0 => 3^0=1]
U Spec, 29
32 ~3=0 => 3^0=1
Detach, 31, 8
As Required:
33 3^0=1
Detach, 32, 9
Prove: 3^1=3
Apply definition of ^
34 ALL(b):[3 e n & b e n => 3^(b+1)=3^b*3]
U Spec, 30
35 3 e n & 0 e n => 3^(0+1)=3^0*3
U Spec, 34
36 3 e n & 0 e n
Join, 8, 4
37 3^(0+1)=3^0*3
Detach, 35, 36
38 3^(0+1)=1*3
Substitute, 33, 37
39 1 e n => 1+0=1
U Spec, 13
40 1+0=1
Detach, 39, 5
Apply commutativity of +
41 ALL(b):[1 e n & b e n => 1+b=b+1]
U Spec, 18
42 1 e n & 0 e n => 1+0=0+1
U Spec, 41
43 1 e n & 0 e n
Join, 5, 4
44 1+0=0+1
Detach, 42, 43
45 0+1=1
Substitute, 44, 40
46 3^1=1*3
Substitute, 45, 38
47 3 e n => 3*1=3
U Spec, 15
48 3*1=3
Detach, 47, 8
Apply commutativity of *
49 ALL(b):[3 e n & b e n => 3*b=b*3]
U Spec, 21
50 3 e n & 1 e n => 3*1=1*3
U Spec, 49
51 3 e n & 1 e n
Join, 8, 5
52 3*1=1*3
Detach, 50, 51
53 1*3=3
Substitute, 52, 48
As Required:
54 3^1=3
Substitute, 53, 46
Prove: 3^2=9
Apply definition of ^
55 ALL(b):[3 e n & b e n => 3^(b+1)=3^b*3]
U Spec, 30
56 3 e n & 1 e n => 3^(1+1)=3^1*3
U Spec, 55
57 3 e n & 1 e n
Join, 8, 5
58 3^(1+1)=3^1*3
Detach, 56, 57
59 3^2=3^1*3
Substitute, 7, 58
60 3^2=3*3
Substitute, 54, 59
As Required:
61 3^2=9
Substitute, 12, 60