THEOREM
*******
Powers of non-zero bases are
non-zero
ALL(a):ALL(b):[a
e n & b e n => [~a=0
=> ~a^b=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.com
Dan Christensen
2019-11-10
AXIOMS/DEFINTITIONS
*******************
Define: n, 0, 1
1 Set(n)
Axiom
2 0 e n
Axiom
3 1 e n
Axiom
4 ~1=0
Axiom
Properties of +
***************
Closed on n
5 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Properties of *
***************
Closed on n
6 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
7 ALL(a):ALL(b):[a e n & b e n => [~a=0 & ~b=0 => ~a*b=0]]
Axiom
Induction principle
*******************
8 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
Define: ^ on n
**************
9 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => a^b e n]]
Axiom
10 0^1=0
Axiom
11 ALL(a):[a e n => [~a=0 => a^0=1]]
Axiom
12 ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => a^(b+1)=a^b*a]]
Axiom
PROOF
*****
Prove: ALL(a):[a e n => [~a=0 => ALL(b):[b e n => ~a^b=0]]]
Suppose...
13 x e n
Premise
Prove: ~x=0 => ALL(b):[b e n => ~x^b=0]
Suppose...
14 ~x=0
Premise
Construct set p for proof by induction
15 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ~x^b=0]]
Subset, 1
16 Set(p) & ALL(b):[b e p <=> b e n & ~x^b=0]
E Spec, 15
Define: p
17 Set(p)
Split, 16
18 ALL(b):[b e p <=> b e n & ~x^b=0]
Split, 16
Apply induction principle
19 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, 8
Prove: ALL(b):[b e p => b e n]
Suppose...
20 t e p
Premise
Apply definition of p
21 t e p <=> t e n & ~x^t=0
U Spec, 18
22 [t e p => t e n & ~x^t=0] & [t e n & ~x^t=0 => t e p]
Iff-And, 21
23 t e p => t e n & ~x^t=0
Split, 22
24 t e n & ~x^t=0 => t e p
Split, 22
25 t e n & ~x^t=0
Detach, 23, 20
26 t e n
Split, 25
As Required:
27 ALL(b):[b e p => b e n]
4 Conclusion, 20
28 Set(p) & ALL(b):[b e p => b e n]
Join, 17, 27
Sufficient: For ALL(b):[b e n => b e p]
29 0 e p & ALL(b):[b e p => b+1 e p]
=>
ALL(b):[b e n => b e p]
Detach, 19, 28
BASE CASE
*********
Apply definiton of p
30 0 e p <=> 0 e n & ~x^0=0
U Spec, 18
31 [0 e p => 0 e n & ~x^0=0] & [0 e n & ~x^0=0 => 0 e p]
Iff-And, 30
32 0 e p => 0 e n & ~x^0=0
Split, 31
Sufficient: For 0 e p
33 0 e n & ~x^0=0 => 0 e p
Split, 31
Apply axiom
34 x e n => [~x=0 => x^0=1]
U Spec, 11
35 ~x=0 => x^0=1
Detach, 34, 13
36 x^0=1
Detach, 35, 14
37 ~x^0=0
Substitute, 36, 4
38 0 e n & ~x^0=0
Join, 2, 37
As Required:
39 0 e p
Detach, 33, 38
INDUCTIVE STEP
**************
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
40 t e p
Premise
Apply definition of p
41 t e p <=> t e n & ~x^t=0
U Spec, 18
42 [t e p => t e n & ~x^t=0] & [t e n & ~x^t=0 => t e p]
Iff-And, 41
43 t e p => t e n & ~x^t=0
Split, 42
44 t e n & ~x^t=0 => t e p
Split, 42
45 t e n & ~x^t=0
Detach, 43, 40
46 t e n
Split, 45
47 ~x^t=0
Split, 45
Apply axiom
48 ALL(b):[t e n & b e n => t+b e n]
U Spec, 5
49 t e n & 1 e n => t+1 e n
U Spec, 48
50 t e n & 1 e n
Join, 46, 3
51 t+1 e n
Detach, 49, 50
Apply definition of p
52 t+1 e p <=> t+1 e n & ~x^(t+1)=0
U Spec, 18, 51
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: For t+1 e p
55 t+1 e n & ~x^(t+1)=0 => t+1 e p
Split, 53
Apply axiom
56 ALL(b):[t e n & b e n => t+b e n]
U Spec, 5
57 t e n & 1 e n => t+1 e n
U Spec, 56
58 t e n & 1 e n
Join, 46, 3
59 t+1 e n
Detach, 57, 58
Apply axiom
60 ALL(b):[x e n & b e n
=>
[~[x=0 & b=0] => x^(b+1)=x^b*x]]
U Spec, 12
61 x e n & t e n
=>
[~[x=0 & t=0] => x^(t+1)=x^t*x]
U Spec, 60
62 x e n & t e n
Join, 13, 46
63 ~[x=0 & t=0] => x^(t+1)=x^t*x
Detach, 61, 62
Prove: ~[x=0 & t=0]
Suppose to the contrary...
64 x=0 & t=0
Premise
65 x=0
Split, 64
66 t=0
Split, 64
67 x=0 & ~x=0
Join, 65, 14
As Required:
68 ~[x=0 & t=0]
4 Conclusion, 64
69 x^(t+1)=x^t*x
Detach, 63, 68
Apply axiom
70 ALL(b):[x e n & b e n => [~[x=0 & b=0] => x^b e n]]
U Spec, 9
71 x e n & t e n => [~[x=0 & t=0] => x^t e n]
U Spec, 70
72 x e n & t e n
Join, 13, 46
73 ~[x=0 & t=0] => x^t e n
Detach, 71, 72
Prove: ~[x=0 & t=0]
Suppose...
74 x=0 & t=0
Premise
75 x=0
Split, 74
76 t=0
Split, 74
77 x=0 & ~x=0
Join, 75, 14
As Required:
78 ~[x=0 & t=0]
4 Conclusion, 74
79 x^t e n
Detach, 73, 78
Apply axiom
80 ALL(b):[x^t e n & b e n => [~x^t=0 & ~b=0 => ~x^t*b=0]]
U Spec, 7, 79
81 x^t e n & x e n => [~x^t=0 & ~x=0 => ~x^t*x=0]
U Spec, 80
82 x^t e n & x e n
Join, 79, 13
83 ~x^t=0 & ~x=0 => ~x^t*x=0
Detach, 81, 82
84 ~x^t=0 & ~x=0
Join, 47, 14
85 ~x^t*x=0
Detach, 83, 84
86 ~x^(t+1)=0
Substitute, 69,
85
87 t+1 e n & ~x^(t+1)=0
Join, 59, 86
88 t+1 e p
Detach, 55, 87
As Required:
89 ALL(b):[b e p => b+1 e p]
4 Conclusion, 40
Joining results...
90 0 e p & ALL(b):[b e p => b+1 e p]
Join, 39, 89
As Required:
91 ALL(b):[b e n => b e p]
Detach, 29, 90
Prove: ALL(b):[b e n => ~x^b=0]
Suppose...
92 y e n
Premise
93 y e n => y e p
U Spec, 91
94 y e p
Detach, 93, 92
Apply definition of p
95 y e p <=> y e n & ~x^y=0
U Spec, 18
96 [y e p => y e n & ~x^y=0] & [y e n & ~x^y=0 => y e p]
Iff-And, 95
97 y e p => y e n & ~x^y=0
Split, 96
98 y e n & ~x^y=0 => y e p
Split, 96
99 y e n & ~x^y=0
Detach, 97, 94
100 y e n
Split, 99
101 ~x^y=0
Split, 99
As Required:
102 ALL(b):[b e n => ~x^b=0]
4 Conclusion, 92
As Required:
103 ~x=0 => ALL(b):[b e n => ~x^b=0]
4 Conclusion, 14
As Required:
104 ALL(a):[a e n => [~a=0 => ALL(b):[b e n => ~a^b=0]]]
4 Conclusion, 13
Prove: ALL(a):ALL(b):[a e n & b e n => [~a=0
=> ~a^b=0]]
Suppose...
105 x e n & y e n
Premise
106 x e n
Split, 105
107 y e n
Split, 105
108 x e n => [~x=0 => ALL(b):[b e n => ~x^b=0]]
U Spec, 104
109 ~x=0 => ALL(b):[b e n => ~x^b=0]
Detach, 108, 106
Prove: ~x=0 => ~x^y=0
Suppose...
110 ~x=0
Premise
111 ALL(b):[b e n => ~x^b=0]
Detach, 109, 110
112 y e n => ~x^y=0
U Spec, 111
113 ~x^y=0
Detach, 112, 107
As Required:
114 ~x=0 => ~x^y=0
4 Conclusion, 110
As Required:
115 ALL(a):ALL(b):[a e n & b e n => [~a=0 => ~a^b=0]]
4 Conclusion, 105