THEOREM
*******
ALL(a):[a e n => [~a=0 => 0^a=0]]
By Dan Christensen
October 2013
(This proof was written with the aid of the author's DC Proof 2.0 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 ALL(a):[a e n => a*0=0]
Axiom
Existence of a predecessor
7 ALL(a):[a e n => [~a=0 => EXIST(b):[b e n & b+1=a]]]
Axiom
Define: ^ (0^0 is an uspecified natural number)
*********
8 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
9 ALL(a):ALL(b):[a e n & b e n => a^b e n]
Split, 8
10 ALL(a):[a e n => [~a=0 => a^0=1]]
Split, 8
11 ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Split, 8
PROOF
*****
Prove: ALL(a):[a e n => [~a=0 => 0^a=0]]
Suppose...
12 y e n
Premise
Prove: ~y=0 => 0^y=0
Suppose...
13 ~y=0
Premise
14 0^y=0^y
Reflex
Apply Existence of Predecessor
15 y e n => [~y=0 => EXIST(b):[b e n & b+1=y]]
U Spec, 7
16 ~y=0 => EXIST(b):[b e n & b+1=y]
Detach, 15, 12
17 EXIST(b):[b e n & b+1=y]
Detach, 16, 13
18 z e n & z+1=y
E Spec, 17
Define: z (the predecessor of y)
19 z e n
Split, 18
20 z+1=y
Split, 18
21 0^y=0^(z+1)
Substitute, 20, 14
Apply definition of ^
22 ALL(b):[0 e n & b e n => 0^(b+1)=0^b*0]
U Spec, 11
23 0 e n & z e n => 0^(z+1)=0^z*0
U Spec, 22
24 0 e n & z e n
Join, 4, 19
25 0^(z+1)=0^z*0
Detach, 23, 24
26 0^y=0^z*0
Substitute, 25, 21
27 0^z e n => 0^z*0=0
U Spec, 6
Apply definition of ^
28 ALL(b):[0 e n & b e n => 0^b e n]
U Spec, 9
29 0 e n & z e n => 0^z e n
U Spec, 28
30 0^z e n
Detach, 29, 24
31 0^z*0=0
Detach, 27, 30
32 0^y=0
Substitute, 31, 26
As Required:
33 ~y=0 => 0^y=0
4 Conclusion, 13
As Required:
34 ALL(a):[a e n => [~a=0 => 0^a=0]]
4 Conclusion, 12