What is zero?
-------------
From the field axioms, we prove:
1. ALL(a):[a e real => [a=0 <=> EXIST(b):[b e real & a+b=b]]]
2. ALL(a):[a e real => [a=0 <=> a+a=0]]
This proof was written with the aid of DC Proof 2.0
Download at http://www.dcproof.com
The Field Axioms
----------------
real is a set
1 Set(real)
Axiom
Define: + operator (addition)
2 ALL(a):ALL(b):[a e real & b e real => a+b e real]
Axiom
+ is associative
3 ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => a+b+c=a+(b+c)]
Axiom
+ is commutative
4 ALL(a):ALL(b):[a e real & b e real => a+b=b+a]
Axiom
Define: 0, the additive identity element
5 0 e real
Axiom
6 ALL(a):[a e real => a+0=a]
Axiom
Define: _ operator, the additive inverse (not be confused with subtraction)
7 ALL(a):[a e real => _a e real]
Axiom
8 ALL(a):[a e real => a+_a=0]
Axiom
Define: * operator (multiplication)
9 ALL(a):ALL(b):[a e real & b e real => a*b e real]
Axiom
* is associative
10 ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => a*b*c=a*(b*c)]
Axiom
* is commutative
11 ALL(a):ALL(b):[a e real & b e real => a*b=b*a]
Axiom
* is distributive over +
12 ALL(a):ALL(b):ALL(c):[a e real & b e real & c e real => a*(b+c)=a*b+a*c]
Axiom
Define: 1, the multiplicative identity element
13 1 e real
Axiom
14 ~0=1
Axiom
15 ALL(a):[a e real => a*1=a]
Axiom
Define: recip operator (multiplicative inverse)
16 ALL(a):[a e real & ~a=0 => recip(a) e real]
Axiom
17 ALL(a):[a e real & ~a=0 => a*recip(a)=1]
Axiom
Theorem #1
----------
Prove: ALL(a):[a e real => [a=0 <=> EXIST(b):[b e real & a+b=b]]]
Suppose...
18 x e real
Premise
Prove: x=0 => EXIST(b):[b e real & x+b=b]
Suppose...
19 x=0
Premise
Apply definition of 0
20 x e real => x+0=x
U Spec, 6
21 x+0=x
Detach, 20, 18
22 x+0=0
Substitute, 19, 21
23 0 e real & x+0=0
Join, 5, 22
24 EXIST(b):[b e real & x+b=b]
E Gen, 23
As Required:
25 x=0 => EXIST(b):[b e real & x+b=b]
4 Conclusion, 19
Prove: EXIST(b):[b e real & x+b=b] => x=0
Suppose...
26 EXIST(b):[b e real & x+b=b]
Premise
27 y e real & x+y=y
E Spec, 26
28 y e real
Split, 27
29 x+y=y
Split, 27
Add _y to both sides.
30 y+_y=y+_y
Reflex
31 x+y+_y=y+_y
Substitute, 29, 30
Apply associativity of +
32 ALL(b):ALL(c):[x e real & b e real & c e real => x+b+c=x+(b+c)]
U Spec, 3
33 ALL(c):[x e real & y e real & c e real => x+y+c=x+(y+c)]
U Spec, 32
34 x e real & y e real & _y e real => x+y+_y=x+(y+_y)
U Spec, 33
Apply definition of '_'
35 y e real => _y e real
U Spec, 7
36 _y e real
Detach, 35, 28
37 x e real & y e real
Join, 18, 28
38 x e real & y e real & _y e real
Join, 37, 36
39 x+y+_y=x+(y+_y)
Detach, 34, 38
40 x+(y+_y)=y+_y
Substitute, 39, 31
Apply definition of '_'
41 y e real => y+_y=0
U Spec, 8
42 y+_y=0
Detach, 41, 28
43 x+0=0
Substitute, 42, 40
44 x e real => x+0=x
U Spec, 6
45 x+0=x
Detach, 44, 18
46 x=0
Substitute, 45, 43
As Required:
47 EXIST(b):[b e real & x+b=b] => x=0
4 Conclusion, 26
Combining results...
48 [x=0 => EXIST(b):[b e real & x+b=b]]
& [EXIST(b):[b e real & x+b=b] => x=0]
Join, 25, 47
49 x=0 <=> EXIST(b):[b e real & x+b=b]
Iff-And, 48
Theorem #1
----------
As Required:
50 ALL(a):[a e real => [a=0 <=> EXIST(b):[b e real & a+b=b]]]
4 Conclusion, 18
Theorem #2
----------
Prove: ALL(a):[a e real => [a=0 <=> a+a=a]]
Suppose...
51 x e real
Premise
Prove: x=0 => x+x=x
Suppose...
52 x=0
Premise
Apply definition of 0
53 0 e real => 0+0=0
U Spec, 6
54 0+0=0
Detach, 53, 5
55 x+x=x
Substitute, 52, 54
As Required:
56 x=0 => x+x=x
4 Conclusion, 52
Prove: x+x=x => x=0
Suppose...
57 x+x=x
Premise
Add _x to both sides
58 x+_x=x+_x
Reflex
59 x+x+_x=x+_x
Substitute, 57, 58
Appy associativity of +
60 ALL(b):ALL(c):[x e real & b e real & c e real => x+b+c=x+(b+c)]
U Spec, 3
61 ALL(c):[x e real & x e real & c e real => x+x+c=x+(x+c)]
U Spec, 60
62 x e real & x e real & _x e real => x+x+_x=x+(x+_x)
U Spec, 61
63 x e real => _x e real
U Spec, 7
64 _x e real
Detach, 63, 51
65 x e real & x e real
Join, 51, 51
66 x e real & x e real & _x e real
Join, 65, 64
67 x+x+_x=x+(x+_x)
Detach, 62, 66
68 x+(x+_x)=x+_x
Substitute, 67, 59
Apply definition of '_'
69 x e real => x+_x=0
U Spec, 8
70 x+_x=0
Detach, 69, 51
71 x+0=0
Substitute, 70, 68
Apply definiton of 0
72 x e real => x+0=x
U Spec, 6
73 x+0=x
Detach, 72, 51
74 x=0
Substitute, 73, 71
As Required:
75 x+x=x => x=0
4 Conclusion, 57
Combining results...
76 [x=0 => x+x=x] & [x+x=x => x=0]
Join, 56, 75
77 x=0 <=> x+x=x
Iff-And, 76
Theorem #2
----------
As Required:
78 ALL(a):[a e real => [a=0 <=> a+a=a]]
4 Conclusion, 51