THEOREM
*******
0*0 = 0
This machine-verified formal proof was written with the aid of
the author's DC Proof 2.0 software available at http://www.dcproof.com
AXIOMS / DEFINITIONS USED
*************************
Define: *
*********
1 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
2 ALL(a):[a e n => a*2=a+a]
Axiom
3 ALL(a):ALL(b):[a e n & b e n => a*(b+1)=a*b+a]
Axiom
Established Properties of +
***************************
+ is a binary function on n
4 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Adding 0
5 ALL(a):[a e n => a+0=a]
Axiom
+ is commutative
6 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
+ is right-cancelable
7 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=c+b => a=c]]
Axiom
Define: 0, 1, 2
***************
8 0 e n
Axiom
9 1 e n
Axiom
10 2 e n
Axiom
11 2=1+1
Axiom
PROOF
*****
First...
Prove: 0*1=0
Apply definition of *
12 0 e n => 0*2=0+0
U Spec, 2
13 0*2=0+0
Detach, 12, 8
Apply definition of *
14 ALL(b):[0 e n & b e n => 0*(b+1)=0*b+0]
U Spec, 3
15 0 e n & 1 e n => 0*(1+1)=0*1+0
U Spec, 14
16 0 e n & 1 e n
Join, 8, 9
17 0*(1+1)=0*1+0
Detach, 15, 16
18 0*2=0*1+0
Substitute, 11, 17
19 0+0=0*1+0
Substitute, 13, 18
Apply cancelability of +
20 ALL(b):ALL(c):[0 e n & b e n & c e n => [0+b=c+b => 0=c]]
U Spec, 7
21 ALL(c):[0 e n & 0 e n & c e n => [0+0=c+0 => 0=c]]
U Spec, 20
22 0 e n & 0 e n & 0*1 e n => [0+0=0*1+0 => 0=0*1]
U Spec, 21
Apply definition of *
23 ALL(b):[0 e n & b e n => 0*b e n]
U Spec, 1
24 0 e n & 1 e n => 0*1 e n
U Spec, 23
25 0 e n & 1 e n
Join, 8, 9
26 0*1 e n
Detach, 24, 25
27 0 e n & 0 e n
Join, 8, 8
28 0 e n & 0 e n & 0*1 e n
Join, 27, 26
29 0+0=0*1+0 => 0=0*1
Detach, 22, 28
30 0=0*1
Detach, 29, 19
As Required:
31 0*1=0
Sym, 30
Prove: 0*0 = 0
32 ALL(b):[0 e n & b e n => 0*(b+1)=0*b+0]
U Spec, 3
Apply definition of *
33 0 e n & 0 e n => 0*(0+1)=0*0+0
U Spec, 32
34 0 e n & 0 e n
Join, 8, 8
35 0*(0+1)=0*0+0
Detach, 33, 34
Apply property of +
36 1 e n => 1+0=1
U Spec, 5
37 1+0=1
Detach, 36, 9
Apply commutativity of +
38 ALL(b):[0 e n & b e n => 0+b=b+0]
U Spec, 6
39 0 e n & 1 e n => 0+1=1+0
U Spec, 38
40 0 e n & 1 e n
Join, 8, 9
41 0+1=1+0
Detach, 39, 40
42 0+1=1
Substitute, 41, 37
43 0*1=0*0+0
Substitute, 42, 35
44 0=0*0+0
Substitute, 30, 43
45 0 e n => 0+0=0
U Spec, 5
46 0+0=0
Detach, 45, 8
47 0+0=0*0+0
Substitute, 46, 44
Apply cancelability of +
48 ALL(b):ALL(c):[0 e n & b e n & c e n => [0+b=c+b => 0=c]]
U Spec, 7
49 ALL(c):[0 e n & 0 e n & c e n => [0+0=c+0 => 0=c]]
U Spec, 48
50 0 e n & 0 e n & 0*0 e n => [0+0=0*0+0 => 0=0*0]
U Spec, 49
Apply definition of *
51 ALL(b):[0 e n & b e n => 0*b e n]
U Spec, 1
52 0 e n & 0 e n => 0*0 e n
U Spec, 51
53 0 e n & 0 e n
Join, 8, 8
54 0*0 e n
Detach, 52, 53
55 0 e n & 0 e n
Join, 8, 8
56 0 e n & 0 e n & 0*0 e n
Join, 55, 54
57 0+0=0*0+0 => 0=0*0
Detach, 50, 56
58 0=0*0
Detach, 57, 47
As Required:
59 0*0=0
Sym, 58