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