THEOREM
*******
ALL(a):ALL(b):[a
e n & b e n => [~a=0
& ~b=0 => 0^a * 0^b = 0^(a+b)]]
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
7 ALL(a):ALL(b):[a e n & b e n => [~a=0 & ~b=0 => ~a+b=0]]
Axiom
Principle of Mathematical
Induction
***********************************
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
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
* Commutative
12 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
Define: ^ on n
**************
13 ALL(a):ALL(b):[a e n & b e n => [~[a=0 & b=0] => a^b e n]]
Axiom
14 0^1=0
Axiom
15 ALL(a):[a e n => [~a=0 => a^0=1]]
Axiom
16 ALL(a):ALL(b):[a e n & b e n
=>
[~[a=0 & b=0] => a^(b+1)=a^b*a]]
Axiom
Previous Result
***************
Zero Exponents
17 ALL(a):[a e n => [~a=0 => 0^a=0]] Proof
Axiom
Suppose...
18 x e n & y e n
Premise
19 x e n
Split, 18
20 y e n
Split, 18
Prove: ~x=0 & ~y=0 => 0^x*0^y=0^(x+y)
Suppose...
21 ~x=0 & ~y=0
Premise
22 ~x=0
Split, 21
23 ~y=0
Split, 21
Apply definition of ^ on n
24 x e n => [~x=0 => 0^x=0]
U Spec, 17
25 ~x=0 => 0^x=0
Detach, 24, 19
26 0^x=0
Detach, 25, 22
Apply definition of ^ on n
27 y e n => [~y=0 => 0^y=0]
U Spec, 17
28 ~y=0 => 0^y=0
Detach, 27, 20
29 0^y=0
Detach, 28, 23
30 0^x e n
Substitute, 26, 2
31 0^y e n
Substitute, 29, 2
32 0 e n => 0*0=0
U Spec, 10
33 0*0=0
Detach, 32, 2
34 0^x*0=0
Substitute, 26,
33
35 0^x*0^y=0
Substitute, 29,
34
36 ALL(b):[x e n & b e n => x+b e n]
U Spec, 4
37 x e n & y e n => x+y e n
U Spec, 36
38 x+y e n
Detach, 37, 18
Apply definition of ^ on n
39 x+y e n => [~x+y=0 => 0^(x+y)=0]
U Spec, 17, 38
40 ALL(b):[x e n & b e n => [~x=0 & ~b=0 => ~x+b=0]]
U Spec, 7
41 x e n & y e n => [~x=0 & ~y=0 => ~x+y=0]
U Spec, 40
42 ~x=0 & ~y=0 => ~x+y=0
Detach, 41, 18
43 ~x+y=0
Detach, 42, 21
44 x+y e n => [~x+y=0 => 0^(x+y)=0]
U Spec, 17, 38
45 ~x+y=0 => 0^(x+y)=0
Detach, 44, 38
46 0^(x+y)=0
Detach, 45, 43
47 0^x*0^y=0^(x+y)
Substitute, 46,
35
As Required:
48 ~x=0 & ~y=0 => 0^x*0^y=0^(x+y)
4 Conclusion, 21
As Required:
49 ALL(a):ALL(b):[a e n & b e n => [~a=0 & ~b=0 => 0^a*0^b=0^(a+b)]]
4 Conclusion, 18