THEOREM
*******
ALL(a):[a
e n => [~a=0 => 0^a=0]]
This machine-verified, formal
proof was written with the aid of the author's DC Proof 2.0 freeware available
at http://www.dcproof
Dan Christensen
2019-10-26
AXIOMS/DEFINTITIONS
*******************
Define: n, 0, 1
1 Set(n)
Axiom
2 0 e n
Axiom
3 1 e n
Axiom
Properties of +
***************
Closed 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
+ Commutative
6 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
Principle of Mathematical
Induction
***********************************
7 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
Properties of *
***************
Closed on n
8 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
Multiplying by 0
9 ALL(a):[a e n => a*0=0]
Axiom
Multiplying by 1
10 ALL(a):[a e n => a*1=a]
Axiom
* Commutative
11 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Define: ^ on n
**************
12 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => a^b e n]]
Axiom
13 0^1=0
Axiom
14 ALL(a):[a e n => [~a=0 => a^0=1]]
Axiom
15 ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => a^(b+1)=a^b*a]]
Axiom
Construct p
Apply Subset Axiom
16 EXIST(sub):[Set(sub) & ALL(a):[a e sub <=> a e n & [~a=0 => 0^a=0]]]
Subset, 1
17 Set(p) & ALL(a):[a e p <=> a e n & [~a=0 => 0^a=0]]
E Spec, 16
Define: p
*********
18 Set(p)
Split, 17
19 ALL(a):[a e p <=> a e n & [~a=0 => 0^a=0]]
Split, 17
Apply Principal of Mathematical
Induction
20 Set(p) & ALL(b):[b e p => b e n]
=>
[0 e p & ALL(b):[b e p => b+1 e p]
=>
ALL(b):[b e n => b e p]]
U Spec, 7
Prove: ALL(b):[b e p => b e n]
Suppose...
21 x e p
Premise
Apply definition of p
22 x e p <=> x e n & [~x=0 => 0^x=0]
U Spec, 19
23 [x e p => x e n & [~x=0 => 0^x=0]]
&
[x e n & [~x=0 => 0^x=0] => x e p]
Iff-And, 22
24 x e p => x e n & [~x=0 => 0^x=0]
Split, 23
25 x e n & [~x=0 => 0^x=0] => x e p
Split, 23
26 x e n & [~x=0 => 0^x=0]
Detach, 24, 21
27 x e n
Split, 26
As Required:
28 ALL(b):[b e p => b e n]
4 Conclusion, 21
29 Set(p) & ALL(b):[b e p => b e n]
Join, 18, 28
Sufficient: For ALL(b):[b e n => b e p]
30 0 e p & ALL(b):[b e p => b+1 e p]
=>
ALL(b):[b e n => b e p]
Detach, 20, 29
Base Case
*********
Prove: 0 e p
Apply definition of p
31 0 e p <=> 0 e n & [~0=0 => 0^0=0]
U Spec, 19
32 [0 e p => 0 e n & [~0=0 => 0^0=0]]
&
[0 e n & [~0=0 => 0^0=0] => 0 e p]
Iff-And, 31
33 0 e p => 0 e n & [~0=0 => 0^0=0]
Split, 32
34 0 e n & [~0=0 => 0^0=0] => 0 e p
Split, 32
35 0=0
Reflex
36 ~0=0 => 0^0=0
Arb Cons, 35
37 0 e n & [~0=0 => 0^0=0]
Join, 2, 36
As Required:
38 0 e p
Detach, 34, 37
Inductive Step
**************
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
39 x e p
Premise
Apply definition of p
40 x e p <=> x e n & [~x=0 => 0^x=0]
U Spec, 19
41 [x e p => x e n & [~x=0 => 0^x=0]]
&
[x e n & [~x=0 => 0^x=0] => x e p]
Iff-And, 40
42 x e p => x e n & [~x=0 => 0^x=0]
Split, 41
43 x e n & [~x=0 => 0^x=0] => x e p
Split, 41
44 x e n & [~x=0 => 0^x=0]
Detach, 42, 39
45 x e n
Split, 44
46 ~x=0 => 0^x=0
Split, 44
Apply axiom
47 ALL(b):[x e n & b e n => x+b e n]
U Spec, 4
48 x e n & 1 e n => x+1 e n
U Spec, 47
49 x e n & 1 e n
Join, 45, 3
50 x+1 e n
Detach, 48, 49
Apply definition of p
51 x+1 e p <=> x+1 e n & [~x+1=0 => 0^(x+1)=0]
U Spec, 19, 50
52 [x+1 e p => x+1 e n & [~x+1=0 => 0^(x+1)=0]]
&
[x+1 e n & [~x+1=0 => 0^(x+1)=0] => x+1 e p]
Iff-And, 51
53 x+1 e p => x+1 e n & [~x+1=0 => 0^(x+1)=0]
Split, 52
Sufficient: For x+1 e p
54 x+1 e n & [~x+1=0 => 0^(x+1)=0] => x+1 e p
Split, 52
55 x+1 e n & [~~x+1=0 | 0^(x+1)=0] => x+1 e p
Imply-Or, 54
56 x+1 e n & [x+1=0 | 0^(x+1)=0] => x+1 e p
Rem DNeg, 55
Two cases to consider:
57 x=0 | ~x=0
Or Not
Case 1
Prove: x=0 => x+1 e p
Suppose...
58 x=0
Premise
Apply definition of p
59 x+1 e n & [x+1=0 | 0^(0+1)=0] => x+1 e p
Substitute, 58,
56
60 1 e n => 1+0=1
U Spec, 5
61 1+0=1
Detach, 60, 3
Apply axiom
62 ALL(b):[1 e n & b e n => 1+b=b+1]
U Spec, 6
63 1 e n & 0 e n => 1+0=0+1
U Spec, 62
64 1 e n & 0 e n
Join, 3, 2
65 1+0=0+1
Detach, 63, 64
66 0+1=1
Substitute, 65,
61
67 0^(0+1)=0
Substitute, 66,
13
68 0^(x+1)=0
Substitute, 58,
67
69 x+1=0 | 0^(x+1)=0
Arb Or, 68
70 x+1 e n & [x+1=0 | 0^(x+1)=0]
Join, 50, 69
71 x+1 e p
Detach, 56, 70
Case 1
As Required:
72 x=0 => x+1 e p
4 Conclusion, 58
Case 2
Prove: ~x=0 => x+1 e p
Suppose...
73 ~x=0
Premise
74 0^x=0
Detach, 46, 73
Apply definition of ^
75 ALL(b):[0 e n & b e n
=>
[~[0=0 & b=0] => 0^(b+1)=0^b*0]]
U Spec, 15
76 0 e n & x e n
=>
[~[0=0 & x=0] => 0^(x+1)=0^x*0]
U Spec, 75
77 0 e n & x e n
Join, 2, 45
78 ~[0=0 & x=0] => 0^(x+1)=0^x*0
Detach, 76, 77
Prove: ~[0=0 & x=0]
Suppose to the contrary...
79 0=0 & x=0
Premise
80 0=0
Split, 79
81 x=0
Split, 79
82 x=0 & ~x=0
Join, 81, 73
As Required:
83 ~[0=0 & x=0]
4 Conclusion, 79
84 0^(x+1)=0^x*0
Detach, 78, 83
Apply definition of ^
85 ALL(b):[0 e n & b e n => [~[0=0 & b=0] => 0^b e n]]
U Spec, 12
86 0 e n & x e n => [~[0=0 & x=0] => 0^x e n]
U Spec, 85
87 0 e n & x e n
Join, 2, 45
88 ~[0=0 & x=0] => 0^x e n
Detach, 86, 87
89 0^x e n
Detach, 88, 83
90 0^x e n => 0^x*0=0
U Spec, 9, 89
91 0^x*0=0
Detach, 90, 89
92 0^(x+1)=0
Substitute, 91,
84
93 x+1=0 | 0^(x+1)=0
Arb Or, 92
94 x+1 e n & [x+1=0 | 0^(x+1)=0]
Join, 50, 93
95 x+1 e p
Detach, 56, 94
Case 2
As Required:
96 ~x=0 => x+1 e p
4 Conclusion, 73
97 [x=0 => x+1 e p] & [~x=0 => x+1 e p]
Join, 72, 96
98 x+1 e p
Cases, 57, 97
As Required:
99 ALL(b):[b e p => b+1 e p]
4 Conclusion, 39
100 0 e p & ALL(b):[b e p => b+1 e p]
Join, 38, 99
As Required:
101 ALL(b):[b e n => b e p]
Detach, 30, 100
Prove: ALL(a):[a e n => [~a=0 => 0^a=0]]
Suppose...
102 x e n
Premise
103 x e n => x e p
U Spec, 101
104 x e p
Detach, 103, 102
Apply definition of p
105 x e p <=> x e n & [~x=0 => 0^x=0]
U Spec, 19
106 [x e p => x e n & [~x=0 => 0^x=0]]
&
[x e n & [~x=0 => 0^x=0] => x e p]
Iff-And, 105
107 x e p => x e n & [~x=0 => 0^x=0]
Split, 106
108 x e n & [~x=0 => 0^x=0] => x e p
Split, 106
109 x e n & [~x=0 => 0^x=0]
Detach, 107, 104
110 x e n
Split, 109
111 ~x=0 => 0^x=0
Split, 109
As Required:
112 ALL(a):[a e n => [~a=0 => 0^a=0]]
4 Conclusion, 102