THEOREM 6 (LEMMA)
*****************
ALL(a):ALL(b):[aen & ben => [~a=0 => ~a^b=0]]
By Dan Christensen
October 2013
(This proof was prepared 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 ~0=1
Axiom
7 ALL(a):[a e n => a+0=a]
Axiom
8 ALL(a):[a e n => a*0=0]
Axiom
9 ALL(a):[a e n => a*1=a]
Axiom
The principle of mathematical induction (PMI)
10 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
Zero product rule
11 ALL(a):ALL(b):[a e n & b e n => [a*b=0 => a=0 | b=0]]
Axiom
Define: ^ (0^0 is an uspecified natural number)
*********
12 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
13 ALL(a):ALL(b):[a e n & b e n => a^b e n]
Split, 12
14 ALL(a):[a e n => [~a=0 => a^0=1]]
Split, 12
15 ALL(a):ALL(b):[a e n & b e n => a^(b+1)=a^b*a]
Split, 12
Prove: ALL(a):[a e n => [~a=0 => ALL(b):[b e n => ~a^b=0]]]
Suppose...
16 x e n
Premise
Prove: ~x=0 => ALL(b):[b e n => ~x^b=0]
Suppose...
17 ~x=0
Premise
Apply Subset Axiom for proof by induction
18 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ~x^b=0]]
Subset, 1
19 Set(p) & ALL(b):[b e p <=> b e n & ~x^b=0]
E Spec, 18
Define: p
20 Set(p)
Split, 19
21 ALL(b):[b e p <=> b e n & ~x^b=0]
Split, 19
Apply PMI
22 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, 10
Prove: ALL(b):[b e p => b e n]
Suppose...
23 t e p
Premise
Apply definition of p
24 t e p <=> t e n & ~x^t=0
U Spec, 21
25 [t e p => t e n & ~x^t=0] & [t e n & ~x^t=0 => t e p]
Iff-And, 24
26 t e p => t e n & ~x^t=0
Split, 25
27 t e n & ~x^t=0 => t e p
Split, 25
28 t e n & ~x^t=0
Detach, 26, 23
29 t e n
Split, 28
As Required:
30 ALL(b):[b e p => b e n]
4 Conclusion, 23
31 Set(p) & ALL(b):[b e p => b e n]
Join, 20, 30
Sufficient: ALL(b):[b e n => b e p]
32 0 e p & ALL(b):[b e p => b+1 e p]
=> ALL(b):[b e n => b e p]
Detach, 22, 31
Prove: 0 e p
Apply definition of p
33 0 e p <=> 0 e n & ~x^0=0
U Spec, 21
34 [0 e p => 0 e n & ~x^0=0] & [0 e n & ~x^0=0 => 0 e p]
Iff-And, 33
35 0 e p => 0 e n & ~x^0=0
Split, 34
Sufficient: 0 e p
36 0 e n & ~x^0=0 => 0 e p
Split, 34
Apply definition of ^
37 x e n => [~x=0 => x^0=1]
U Spec, 14
38 ~x=0 => x^0=1
Detach, 37, 16
39 x^0=1
Detach, 38, 17
40 ~0=x^0
Substitute, 39, 6
41 ~x^0=0
Sym, 40
42 0 e n & ~x^0=0
Join, 4, 41
As Required:
43 0 e p
Detach, 36, 42
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
44 t e p
Premise
Apply definition of p
45 t e p <=> t e n & ~x^t=0
U Spec, 21
46 [t e p => t e n & ~x^t=0] & [t e n & ~x^t=0 => t e p]
Iff-And, 45
47 t e p => t e n & ~x^t=0
Split, 46
48 t e n & ~x^t=0 => t e p
Split, 46
49 t e n & ~x^t=0
Detach, 47, 44
50 t e n
Split, 49
51 ~x^t=0
Split, 49
Apply definition of p
52 t+1 e p <=> t+1 e n & ~x^(t+1)=0
U Spec, 21
53 [t+1 e p => t+1 e n & ~x^(t+1)=0]
& [t+1 e n & ~x^(t+1)=0 => t+1 e p]
Iff-And, 52
54 t+1 e p => t+1 e n & ~x^(t+1)=0
Split, 53
Sufficient: t+1 e p
55 t+1 e n & ~x^(t+1)=0 => t+1 e p
Split, 53
56 ALL(b):[t e n & b e n => t+b e n]
U Spec, 2
57 t e n & 1 e n => t+1 e n
U Spec, 56
58 t e n & 1 e n
Join, 50, 5
59 t+1 e n
Detach, 57, 58
Apply definition of ^
60 ALL(b):[x e n & b e n => x^(b+1)=x^b*x]
U Spec, 15
61 x e n & t e n => x^(t+1)=x^t*x
U Spec, 60
62 x e n & t e n
Join, 16, 50
63 x^(t+1)=x^t*x
Detach, 61, 62
64 ALL(b):[x^t e n & b e n => [x^t*b=0 => x^t=0 | b=0]]
U Spec, 11
65 x^t e n & x e n => [x^t*x=0 => x^t=0 | x=0]
U Spec, 64
66 ALL(b):[x e n & b e n => x^b e n]
U Spec, 13
67 x e n & t e n => x^t e n
U Spec, 66
68 x^t e n
Detach, 67, 62
69 x^t e n & x e n
Join, 68, 16
70 x^t*x=0 => x^t=0 | x=0
Detach, 65, 69
71 ~[x^t=0 | x=0] => ~x^t*x=0
Contra, 70
72 ~~[~x^t=0 & ~x=0] => ~x^t*x=0
DeMorgan, 71
73 ~x^t=0 & ~x=0 => ~x^t*x=0
Rem DNeg, 72
74 ~x^t=0 & ~x=0
Join, 51, 17
75 ~x^t*x=0
Detach, 73, 74
76 ~x^(t+1)=0
Substitute, 63, 75
77 t+1 e n & ~x^(t+1)=0
Join, 59, 76
78 t+1 e p
Detach, 55, 77
As Required:
79 ALL(b):[b e p => b+1 e p]
4 Conclusion, 44
80 0 e p & ALL(b):[b e p => b+1 e p]
Join, 43, 79
As Required:
81 ALL(b):[b e n => b e p]
Detach, 32, 80
Prove: ALL(b):[b e n => ~x^b=0]
Suppose...
82 t e n
Premise
83 t e n => t e p
U Spec, 81
84 t e p
Detach, 83, 82
85 t e p <=> t e n & ~x^t=0
U Spec, 21
86 [t e p => t e n & ~x^t=0] & [t e n & ~x^t=0 => t e p]
Iff-And, 85
87 t e p => t e n & ~x^t=0
Split, 86
88 t e n & ~x^t=0 => t e p
Split, 86
89 t e n & ~x^t=0
Detach, 87, 84
90 t e n
Split, 89
91 ~x^t=0
Split, 89
As Required:
92 ALL(b):[b e n => ~x^b=0]
4 Conclusion, 82
As Required:
93 ~x=0 => ALL(b):[b e n => ~x^b=0]
4 Conclusion, 17
As Required:
94 ALL(a):[a e n => [~a=0 => ALL(b):[b e n => ~a^b=0]]]
4 Conclusion, 16
Prove: ALL(a):ALL(b):[a e n & b e n => [~a=0 => ~a^b=0]]
Suppose...
95 x e n & y e n
Premise
96 x e n
Split, 95
97 y e n
Split, 95
Prove: ~x=0 => ~x^y=0
Suppose...
98 ~x=0
Premise
99 x e n => [~x=0 => ALL(b):[b e n => ~x^b=0]]
U Spec, 94
100 ~x=0 => ALL(b):[b e n => ~x^b=0]
Detach, 99, 96
101 ALL(b):[b e n => ~x^b=0]
Detach, 100, 98
102 y e n => ~x^y=0
U Spec, 101
103 ~x^y=0
Detach, 102, 97
104 ~x=0 => ~x^y=0
4 Conclusion, 98
As Required:
105 ALL(a):ALL(b):[a e n & b e n => [~a=0 => ~a^b=0]]
4 Conclusion, 95