THEOREM
*******
ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [a=0 => [~b=0
& ~c=0 => a^b*a^c=a^(b+c)]]
<-- 0 base
& [~a=0 => a^b*a^c=a^(b+c)]] <-- non-zero base
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
+ Associative
7 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => a+b+c=a+(b+c)]
Axiom
8 ALL(a):ALL(b):[a e n & b e n => [~a=0 & ~b=0 => ~a+b=0]]
Axiom
Properties of *
***************
Closed on n
9 ALL(a):ALL(b):[a e n & b e n => a*b e n]
Axiom
Multiplying by 0
10 ALL(a):[a e n => a*0=0]
Axiom
Multiplying by 1
11 ALL(a):[a e n => a*1=a]
Axiom
* Associative
12 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n =>
a*b*c=a*(b*c)]
Axiom
* Commutative
13 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Define: ^ on n
**************
14 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => a^b e n]]
Axiom
15 0^1=0
Axiom
16 ALL(a):[a e n => [~a=0 => a^0=1]]
Axiom
17 ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => a^(b+1)=a^b*a]]
Axiom
Principle of Mathematical
Induction
***********************************
18 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
PREVIOUS RESULTS (links to
proofs)
****************
Product of Powers Rule for
non-zero bases Proof
19 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [~a=0 => a^(b+c)=a^b*a^c]]
Axiom
Product of Powers Rule for zero
bases Proof
20 ALL(a):ALL(b):[a e n & b e n => [~a=0 & ~b=0 => 0^a*0^b=0^(a+b)]]
Axiom
Suppose...
21 x e n & y e n & z e n
Premise
22 x e n
Split, 21
23 y e n
Split, 21
24 z e n
Split, 21
Prove: x=0 => [~y=0 & ~z=0 => x^y*x^z=x^(y+z)]
Suppose...
25 x=0
Premise
Prove: ~y=0 & ~z=0 => x^y*x^z=x^(y+z)
Suppose...
26 ~y=0 & ~z=0
Premise
27 ALL(b):[y e n & b e n => [~y=0 & ~b=0 => 0^y*0^b=0^(y+b)]]
U Spec, 20
28 y e n & z e n => [~y=0 & ~z=0 => 0^y*0^z=0^(y+z)]
U Spec, 27
29 y e n & z e n
Join, 23, 24
30 ~y=0 & ~z=0 => 0^y*0^z=0^(y+z)
Detach, 28, 29
31 0^y*0^z=0^(y+z)
Detach, 30, 26
32 x^y*x^z=x^(y+z)
Substitute, 25, 31
As Required:
33 ~y=0 & ~z=0 => x^y*x^z=x^(y+z)
4 Conclusion, 26
As Required:
34 x=0 => [~y=0 & ~z=0 => x^y*x^z=x^(y+z)]
4 Conclusion, 25
35 ALL(b):ALL(c):[x e n & b e n & c e n => [~x=0 => x^(b+c)=x^b*x^c]]
U Spec, 19
36 ALL(c):[x e n & y e n & c e n => [~x=0 => x^(y+c)=x^y*x^c]]
U Spec, 35
37 x e n & y e n & z e n => [~x=0 => x^(y+z)=x^y*x^z]
U Spec, 36
38 ~x=0 => x^(y+z)=x^y*x^z
Detach, 37, 21
39 ~x=0 => x^y*x^z=x^(y+z)
Sym, 38
40 [x=0 => [~y=0 & ~z=0 => x^y*x^z=x^(y+z)]]
&
[~x=0 => x^y*x^z=x^(y+z)]
Join, 34, 39
As Required:
41 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=>
[a=0 => [~b=0 & ~c=0 => a^b*a^c=a^(b+c)]]
&
[~a=0 => a^b*a^c=a^(b+c)]]
4 Conclusion, 21