THEOREM
*******
Powers of a non-zero base are themselves 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 software available at http://www.dcproof.com
AXIOMS / DEFINITIONS USED
*************************
Define: ^ (partial function on n, infix version of pow function)
1 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => a^b e n]
Axiom
2 ALL(a):[a e n & ~a=0 => a^0=1]
Axiom
3 0^1=0
Axiom
4 ALL(a):ALL(b):[a e n & b e n & ~[a=0 & b=0] => a^(b+1)=a^b*a]
Axiom
n is a set (the set of natural numbers)
5 Set(n)
Axiom
6 0 e n
Axiom
Define: +
7 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
Define: 1
8 1 e n
Axiom
9 ~1=0
Axiom
Zero-product rule
10 ALL(a):ALL(b):[a e n & b e n => [a*b=0 => a=0 | b=0]]
Axiom
The principle of mathematical induction (starting at 0)
11 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
PROOF
*****
Prove: ALL(a):[a e n & ~a=0 => ALL(b):[b e n => ~a^b=0]]
Suppose...
12 x e n & ~x=0
Premise
13 x e n
Split, 12
14 ~x=0
Split, 12
15 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ~x^b=0]]
Subset, 5
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 Principle of Mathematic Induction
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, 11
Prove: ALL(b):[b e p => b e n]
Suppose...
20 t e p
Premise
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: 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
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: 0 e p
33 0 e n & ~x^0=0 => 0 e p
Split, 31
34 x e n & ~x=0 => x^0=1
U Spec, 2
35 x^0=1
Detach, 34, 12
36 ~x^0=0
Substitute, 35, 9
37 0 e n & ~x^0=0
Join, 6, 36
As Required:
38 0 e p
Detach, 33, 37
Prove: ALL(b):[b e p => b+1 e p]
Suppose...
39 t e p
Premise
40 t e p <=> t e n & ~x^t=0
U Spec, 18
41 [t e p => t e n & ~x^t=0] & [t e n & ~x^t=0 => t e p]
Iff-And, 40
42 t e p => t e n & ~x^t=0
Split, 41
43 t e n & ~x^t=0 => t e p
Split, 41
44 t e n & ~x^t=0
Detach, 42, 39
45 t e n
Split, 44
46 ~x^t=0
Split, 44
47 t+1 e p <=> t+1 e n & ~x^(t+1)=0
U Spec, 18
48 [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, 47
49 t+1 e p => t+1 e n & ~x^(t+1)=0
Split, 48
Sufficient: t+1 e p
50 t+1 e n & ~x^(t+1)=0 => t+1 e p
Split, 48
51 ALL(b):[t e n & b e n => t+b e n]
U Spec, 7
52 t e n & 1 e n => t+1 e n
U Spec, 51
53 t e n & 1 e n
Join, 45, 8
54 t+1 e n
Detach, 52, 53
55 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^(b+1)=x^b*x]
U Spec, 4
56 x e n & t e n & ~[x=0 & t=0] => x^(t+1)=x^t*x
U Spec, 55
Prove: ~[x=0 & t=0]
Suppose to the contrary...
57 x=0 & t=0
Premise
58 x=0
Split, 57
59 t=0
Split, 57
60 x=0 & ~x=0
Join, 58, 14
As Required:
61 ~[x=0 & t=0]
4 Conclusion, 57
62 x e n & t e n
Join, 13, 45
63 x e n & t e n & ~[x=0 & t=0]
Join, 62, 61
64 x^(t+1)=x^t*x
Detach, 56, 63
65 ALL(b):[x^t e n & b e n => [x^t*b=0 => x^t=0 | b=0]]
U Spec, 10
66 x^t e n & x e n => [x^t*x=0 => x^t=0 | x=0]
U Spec, 65
67 ALL(b):[x e n & b e n & ~[x=0 & b=0] => x^b e n]
U Spec, 1
68 x e n & t e n & ~[x=0 & t=0] => x^t e n
U Spec, 67
69 x^t e n
Detach, 68, 63
70 x^t e n & x e n
Join, 69, 13
71 x^t*x=0 => x^t=0 | x=0
Detach, 66, 70
72 ~[x^t=0 | x=0] => ~x^t*x=0
Contra, 71
73 ~~[~x^t=0 & ~x=0] => ~x^t*x=0
DeMorgan, 72
74 ~x^t=0 & ~x=0 => ~x^t*x=0
Rem DNeg, 73
75 ~x^t=0 & ~x=0
Join, 46, 14
76 ~x^t*x=0
Detach, 74, 75
77 ~x^(t+1)=0
Substitute, 64, 76
78 t+1 e n & ~x^(t+1)=0
Join, 54, 77
79 t+1 e p
Detach, 50, 78
As Required:
80 ALL(b):[b e p => b+1 e p]
4 Conclusion, 39
81 0 e p & ALL(b):[b e p => b+1 e p]
Join, 38, 80
As Required:
82 ALL(b):[b e n => b e p]
Detach, 29, 81
Prove: ALL(b):[b e n => ~x^b=0]
Suppose...
83 t e n
Premise
84 t e n => t e p
U Spec, 82
85 t e p
Detach, 84, 83
86 t e p <=> t e n & ~x^t=0
U Spec, 18
87 [t e p => t e n & ~x^t=0] & [t e n & ~x^t=0 => t e p]
Iff-And, 86
88 t e p => t e n & ~x^t=0
Split, 87
89 t e n & ~x^t=0 => t e p
Split, 87
90 t e n & ~x^t=0
Detach, 88, 85
91 t e n
Split, 90
92 ~x^t=0
Split, 90
As Required:
93 ALL(b):[b e n => ~x^b=0]
4 Conclusion, 83
As Required:
94 ALL(a):[a e n & ~a=0 => ALL(b):[b e n => ~a^b=0]]
4 Conclusion, 12
Prove: ALL(a):ALL(b):[a e n & b e n & ~a=0 => ~a^b=0]
Suppose...
95 x e n & y e n & ~x=0
Premise
96 x e n
Split, 95
97 y e n
Split, 95
98 ~x=0
Split, 95
99 x e n & ~x=0 => ALL(b):[b e n => ~x^b=0]
U Spec, 94
100 x e n & ~x=0
Join, 96, 98
101 ALL(b):[b e n => ~x^b=0]
Detach, 99, 100
102 y e n => ~x^y=0
U Spec, 101
103 ~x^y=0
Detach, 102, 97
As Required:
104 ALL(a):ALL(b):[a e n & b e n & ~a=0 => ~a^b=0]
4 Conclusion, 95