THEOREM
*******
There are infinitely many binary functions pow on N that satisfy:
pow(x,2) = x*x
pow(x,y+1) = pow(x,y) * x
Here, we formally prove:
ALL(x0):[x0 e n
=> EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=x0
& ALL(a):[a e n => pow(a,2)=a*a]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]]]
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
*************************
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 2 e n
Axiom
7 2=1+1
Axiom
Adding 0
8 ALL(a):[a e n => a+0=a]
Axiom
Multiplying by 0
9 ALL(a):[a e n => a*0=0]
Axiom
Multiplying by 1
10 ALL(a):[a e n => a*1=a]
Axiom
+ is commutative
11 ALL(a):ALL(b):[a e n & b e n => a+b=b+a]
Axiom
* is commutative
12 ALL(a):ALL(b):[a e n & b e n => a*b=b*a]
Axiom
The principle of mathematical induction (starting at 0)
13 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
Right cancelability of +
14 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=c+b => a=c]]
Axiom
0 has no predecessor
15 ALL(a):[a e n => ~a+1=0]
Axiom
PROOF
*****
Construct the set of ordered triples of n
Apply Cartesian Product Axiom
16 ALL(a1):ALL(a2):ALL(a3):[Set(a1) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e a1 & c2 e a2 & c3 e a3]]]
Cart Prod
17 ALL(a2):ALL(a3):[Set(n) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e a2 & c3 e a3]]]
U Spec, 16
18 ALL(a3):[Set(n) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e a3]]]
U Spec, 17
19 Set(n) & Set(n) & Set(n) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
U Spec, 18
20 Set(n) & Set(n)
Join, 1, 1
21 Set(n) & Set(n) & Set(n)
Join, 20, 1
22 EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e n & c2 e n & c3 e n]]
Detach, 19, 21
23 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 22
Define: n3 (the set of ordered triples of n)
**********
24 Set''(n3)
Split, 23
25 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 23
Construct the powerset of n3
Apply the Power Set Axiom
26 ALL(a):[Set''(a) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e a]]]]
Power Set
27 Set''(n3) => EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]]
U Spec, 26
28 EXIST(b):[Set(b)
& ALL(c):[c e b <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]]
Detach, 27, 24
29 Set(pn3)
& ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]
E Spec, 28
Define: pn3 (the power set of n3)
***********
30 Set(pn3)
Split, 29
31 ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]
Split, 29
Prove: ALL(x0):[x0 e n
=> EXIST(pow):[ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=x0
& ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
& ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]]]
Suppose...
32 x0 e n
Premise
Construct the set pow, a subset of n3
Apply the Subset Axiom
33 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (a,b,c) e d]]]
Subset, 24
34 Set''(pow) & ALL(a):ALL(b):ALL(c):[(a,b,c) e pow
<=> (a,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (a,b,c) e d]]
E Spec, 33
Define: pow
***********
35 Set''(pow)
Split, 34
36 ALL(a):ALL(b):ALL(c):[(a,b,c) e pow
<=> (a,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (a,b,c) e d]]
Split, 34
Establish some useful properties of pow
Prove: (0,0,x0) e pow
Apply definition of pow
37 ALL(b):ALL(c):[(0,b,c) e pow
<=> (0,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,b,c) e d]]
U Spec, 36
38 ALL(c):[(0,0,c) e pow
<=> (0,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,c) e d]]
U Spec, 37
39 (0,0,x0) e pow
<=> (0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,x0) e d]
U Spec, 38
40 [(0,0,x0) e pow => (0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,x0) e d]]
& [(0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,x0) e d] => (0,0,x0) e pow]
Iff-And, 39
41 (0,0,x0) e pow => (0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,x0) e d]
Split, 40
Sufficient: (0,0,x0) e pow
42 (0,0,x0) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,x0) e d] => (0,0,x0) e pow
Split, 40
Prove: (0,0,x0) e n3
43 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 25
44 ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]
U Spec, 43
45 (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n
U Spec, 44
46 [(0,0,x0) e n3 => 0 e n & 0 e n & x0 e n]
& [0 e n & 0 e n & x0 e n => (0,0,x0) e n3]
Iff-And, 45
47 (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n
Split, 46
48 0 e n & 0 e n & x0 e n => (0,0,x0) e n3
Split, 46
49 0 e n & 0 e n
Join, 4, 4
50 0 e n & 0 e n & x0 e n
Join, 49, 32
As Required:
51 (0,0,x0) e n3
Detach, 48, 50
Prove: ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
Suppose...
52 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Premise
53 q e pn3
Split, 52
54 (0,0,x0) e q
Split, 52
As Required:
55 ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,x0) e d]
4 Conclusion, 52
56 (0,0,x0) e n3
& ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,x0) e d]
Join, 51, 55
As Required:
57 (0,0,x0) e pow
Detach, 42, 56
Prove: ALL(a):[a e n => [~a=0 => (a,0,1) e pow]]
Suppose...
58 x e n
Premise
Prove: ~x=0 => (x,0,1) e pow
Suppose...
59 ~x=0
Premise
Apply definition of pow
60 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,b,c) e d]]
U Spec, 36
61 ALL(c):[(x,0,c) e pow
<=> (x,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,c) e d]]
U Spec, 60
62 (x,0,1) e pow
<=> (x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,1) e d]
U Spec, 61
63 [(x,0,1) e pow => (x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,1) e d]]
& [(x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,1) e d] => (x,0,1) e pow]
Iff-And, 62
64 (x,0,1) e pow => (x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,1) e d]
Split, 63
Sufficient: (x,0,1) e pow
65 (x,0,1) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,1) e d] => (x,0,1) e pow
Split, 63
Prove: (x,0,1) e n3
Apply definition of n3
66 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 25
67 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]
U Spec, 66
68 (x,0,1) e n3 <=> x e n & 0 e n & 1 e n
U Spec, 67
69 [(x,0,1) e n3 => x e n & 0 e n & 1 e n]
& [x e n & 0 e n & 1 e n => (x,0,1) e n3]
Iff-And, 68
70 (x,0,1) e n3 => x e n & 0 e n & 1 e n
Split, 69
71 x e n & 0 e n & 1 e n => (x,0,1) e n3
Split, 69
72 x e n & 0 e n
Join, 58, 4
73 x e n & 0 e n & 1 e n
Join, 72, 5
74 (x,0,1) e n3
Detach, 71, 73
75 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Premise
76 q e pn3
Split, 75
77 (0,0,x0) e q
Split, 75
78 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Split, 75
79 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Split, 75
80 x e n => [~x=0 => (x,0,1) e q]
U Spec, 78
81 ~x=0 => (x,0,1) e q
Detach, 80, 58
82 (x,0,1) e q
Detach, 81, 59
83 ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,1) e d]
4 Conclusion, 75
84 (x,0,1) e n3
& ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,1) e d]
Join, 74, 83
85 (x,0,1) e pow
Detach, 65, 84
As Required:
86 ~x=0 => (x,0,1) e pow
4 Conclusion, 59
As Required:
87 ALL(a):[a e n => [~a=0 => (a,0,1) e pow]]
4 Conclusion, 58
Prove: ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [(a,b,c) e pow => (a,b+1,c*a) e pow]]
Suppose...
88 x e n & y e n & z e n
Premise
89 x e n
Split, 88
90 y e n
Split, 88
91 z e n
Split, 88
Prove: (x,y,z) e pow => (x,y+1,z*x) e pow
Suppose...
92 (x,y,z) e pow
Premise
Apply definition of pow
93 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,b,c) e d]]
U Spec, 36
94 ALL(c):[(x,y,c) e pow
<=> (x,y,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y,c) e d]]
U Spec, 93
95 (x,y,z) e pow
<=> (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y,z) e d]
U Spec, 94
96 [(x,y,z) e pow => (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y,z) e d]]
& [(x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y,z) e d] => (x,y,z) e pow]
Iff-And, 95
97 (x,y,z) e pow => (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y,z) e d]
Split, 96
98 (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y,z) e d] => (x,y,z) e pow
Split, 96
99 (x,y,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y,z) e d]
Detach, 97, 92
100 (x,y,z) e n3
Split, 99
101 ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y,z) e d]
Split, 99
Apply definition of pow
102 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,b,c) e d]]
U Spec, 36
103 ALL(c):[(x,y+1,c) e pow
<=> (x,y+1,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,c) e d]]
U Spec, 102
104 (x,y+1,z*x) e pow
<=> (x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,z*x) e d]
U Spec, 103
105 [(x,y+1,z*x) e pow => (x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,z*x) e d]]
& [(x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,z*x) e d] => (x,y+1,z*x) e pow]
Iff-And, 104
106 (x,y+1,z*x) e pow => (x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,z*x) e d]
Split, 105
Sufficient: (x,y+1,z*x) e pow
107 (x,y+1,z*x) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,z*x) e d] => (x,y+1,z*x) e pow
Split, 105
Prove: (x,y+1,z*x) e n3
Apply definition of n3
108 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 25
109 ALL(c3):[(x,y+1,c3) e n3 <=> x e n & y+1 e n & c3 e n]
U Spec, 108
110 (x,y+1,z*x) e n3 <=> x e n & y+1 e n & z*x e n
U Spec, 109
111 [(x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n]
& [x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3]
Iff-And, 110
112 (x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n
Split, 111
113 x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3
Split, 111
114 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
115 y e n & 1 e n => y+1 e n
U Spec, 114
116 y e n & 1 e n
Join, 90, 5
117 y+1 e n
Detach, 115, 116
118 ALL(b):[z e n & b e n => z*b e n]
U Spec, 3
119 z e n & x e n => z*x e n
U Spec, 118
120 z e n & x e n
Join, 91, 89
121 z*x e n
Detach, 119, 120
122 x e n & y+1 e n
Join, 89, 117
123 x e n & y+1 e n & z*x e n
Join, 122, 121
124 (x,y+1,z*x) e n3
Detach, 113, 123
Prove: ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,z*x) e d]
Suppose...
125 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Premise
126 q e pn3
Split, 125
127 (0,0,x0) e q
Split, 125
128 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Split, 125
Apply definition of q
129 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Split, 125
130 ALL(f):ALL(g):[(x,f,g) e q => (x,f+1,g*x) e q]
U Spec, 129
131 ALL(g):[(x,y,g) e q => (x,y+1,g*x) e q]
U Spec, 130
132 (x,y,z) e q => (x,y+1,z*x) e q
U Spec, 131
133 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
=> (x,y,z) e q
U Spec, 101
134 (x,y,z) e q
Detach, 133, 125
135 (x,y+1,z*x) e q
Detach, 132, 134
As Required:
136 ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,z*x) e d]
4 Conclusion, 125
137 (x,y+1,z*x) e n3
& ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,y+1,z*x) e d]
Join, 124, 136
138 (x,y+1,z*x) e pow
Detach, 107, 137
As Required:
139 (x,y,z) e pow => (x,y+1,z*x) e pow
4 Conclusion, 92
As Required:
140 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n
=> [(a,b,c) e pow => (a,b+1,c*a) e pow]]
4 Conclusion, 88
Prove: ALL(a):[a e n => [(0,0,a) e pow => a=x0]]
Suppose...
141 z e n
Premise
Prove: ~[(0,0,z) e pow & ~z=x0]
Suppose to contrary...
142 (0,0,z) e pow & ~z=x0
Premise
143 (0,0,z) e pow
Split, 142
144 ~z=x0
Split, 142
Apply definition of pow
145 ALL(b):ALL(c):[(0,b,c) e pow
<=> (0,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,b,c) e d]]
U Spec, 36
146 ALL(c):[(0,0,c) e pow
<=> (0,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,c) e d]]
U Spec, 145
147 (0,0,z) e pow
<=> (0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,z) e d]
U Spec, 146
148 [(0,0,z) e pow => (0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,z) e d]]
& [(0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,z) e d] => (0,0,z) e pow]
Iff-And, 147
149 (0,0,z) e pow => (0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,z) e d]
Split, 148
150 (0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,z) e d] => (0,0,z) e pow
Split, 148
151 ~[(0,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,z) e d]] => ~(0,0,z) e pow
Contra, 149
152 ~~[~(0,0,z) e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,z) e d]] => ~(0,0,z) e pow
DeMorgan, 151
153 ~(0,0,z) e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (0,0,z) e d] => ~(0,0,z) e pow
Rem DNeg, 152
154 ~(0,0,z) e n3 | ~ALL(d):~[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e pow
Imply-And, 153
155 ~(0,0,z) e n3 | ~~EXIST(d):~~[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e pow
Quant, 154
156 ~(0,0,z) e n3 | EXIST(d):~~[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e pow
Rem DNeg, 155
Sufficient: ~(0,0,z) e pow (to obtain contradiction)
157 ~(0,0,z) e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(0,0,z) e d] => ~(0,0,z) e pow
Rem DNeg, 156
158 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e n3 & ~[a=0 & b=0 & c=z]]]
Subset, 24
159 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e n3 & ~[a=0 & b=0 & c=z]]
E Spec, 158
Define: q
160 Set''(q)
Split, 159
161 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e n3 & ~[a=0 & b=0 & c=z]]
Split, 159
162 q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
U Spec, 31
163 [q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]]
& [Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]
Iff-And, 162
164 q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Split, 163
165 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 163
Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Suppose...
166 (t,u,v) e q
Premise
Apply definition of q
167 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]
U Spec, 161
168 ALL(c):[(t,u,c) e q
<=> (t,u,c) e n3 & ~[t=0 & u=0 & c=z]]
U Spec, 167
169 (t,u,v) e q
<=> (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
U Spec, 168
170 [(t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]]
& [(t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q]
Iff-And, 169
171 (t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
Split, 170
172 (t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q
Split, 170
173 (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
Detach, 171, 166
174 (t,u,v) e n3
Split, 173
As Required:
175 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
4 Conclusion, 166
176 Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Join, 160, 175
As Required:
177 q e pn3
Detach, 165, 176
Prove: (0,0,x0) e q
Apply definition of q
178 ALL(b):ALL(c):[(0,b,c) e q
<=> (0,b,c) e n3 & ~[0=0 & b=0 & c=z]]
U Spec, 161
179 ALL(c):[(0,0,c) e q
<=> (0,0,c) e n3 & ~[0=0 & 0=0 & c=z]]
U Spec, 178
180 (0,0,x0) e q
<=> (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]
U Spec, 179
181 [(0,0,x0) e q => (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]]
& [(0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q]
Iff-And, 180
182 (0,0,x0) e q => (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]
Split, 181
183 (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q
Split, 181
184 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 25
185 ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]
U Spec, 184
186 (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n
U Spec, 185
187 [(0,0,x0) e n3 => 0 e n & 0 e n & x0 e n]
& [0 e n & 0 e n & x0 e n => (0,0,x0) e n3]
Iff-And, 186
188 (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n
Split, 187
189 0 e n & 0 e n & x0 e n => (0,0,x0) e n3
Split, 187
190 0 e n & 0 e n
Join, 4, 4
191 0 e n & 0 e n & x0 e n
Join, 190, 32
192 (0,0,x0) e n3
Detach, 189, 191
Prove: ~[0=0 & 0=0 & x0=z]
Suppose to the contrary...
193 0=0 & 0=0 & x0=z
Premise
194 0=0
Split, 193
195 0=0
Split, 193
196 x0=z
Split, 193
197 ~x0=z
Sym, 144
198 x0=z & ~x0=z
Join, 196, 197
As Required:
199 ~[0=0 & 0=0 & x0=z]
4 Conclusion, 193
200 (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]
Join, 192, 199
As Required:
201 (0,0,x0) e q
Detach, 183, 200
Prove: ~(0,0,z) e q
Apply definition of q
202 ALL(b):ALL(c):[(0,b,c) e q
<=> (0,b,c) e n3 & ~[0=0 & b=0 & c=z]]
U Spec, 161
203 ALL(c):[(0,0,c) e q
<=> (0,0,c) e n3 & ~[0=0 & 0=0 & c=z]]
U Spec, 202
204 (0,0,z) e q
<=> (0,0,z) e n3 & ~[0=0 & 0=0 & z=z]
U Spec, 203
205 [(0,0,z) e q => (0,0,z) e n3 & ~[0=0 & 0=0 & z=z]]
& [(0,0,z) e n3 & ~[0=0 & 0=0 & z=z] => (0,0,z) e q]
Iff-And, 204
206 (0,0,z) e q => (0,0,z) e n3 & ~[0=0 & 0=0 & z=z]
Split, 205
207 (0,0,z) e n3 & ~[0=0 & 0=0 & z=z] => (0,0,z) e q
Split, 205
208 ~[(0,0,z) e n3 & ~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q
Contra, 206
209 ~~[~(0,0,z) e n3 | ~~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q
DeMorgan, 208
210 ~(0,0,z) e n3 | ~~[0=0 & 0=0 & z=z] => ~(0,0,z) e q
Rem DNeg, 209
211 ~(0,0,z) e n3 | 0=0 & 0=0 & z=z => ~(0,0,z) e q
Rem DNeg, 210
212 0=0
Reflex
213 z=z
Reflex
214 0=0 & 0=0
Join, 212, 212
215 0=0 & 0=0 & z=z
Join, 214, 213
216 ~(0,0,z) e n3 | 0=0 & 0=0 & z=z
Arb Or, 215
As Required:
217 ~(0,0,z) e q
Detach, 211, 216
218 t e n
Premise
Prove: ~t=0 => (t,0,1) e q
Suppose...
219 ~t=0
Premise
Apply definition of q
220 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]
U Spec, 161
221 ALL(c):[(t,0,c) e q
<=> (t,0,c) e n3 & ~[t=0 & 0=0 & c=z]]
U Spec, 220
222 (t,0,1) e q
<=> (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]
U Spec, 221
223 [(t,0,1) e q => (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]]
& [(t,0,1) e n3 & ~[t=0 & 0=0 & 1=z] => (t,0,1) e q]
Iff-And, 222
224 (t,0,1) e q => (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]
Split, 223
Sufficient: (t,0,1) e q
225 (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z] => (t,0,1) e q
Split, 223
226 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 25
227 ALL(c3):[(t,0,c3) e n3 <=> t e n & 0 e n & c3 e n]
U Spec, 226
228 (t,0,1) e n3 <=> t e n & 0 e n & 1 e n
U Spec, 227
229 [(t,0,1) e n3 => t e n & 0 e n & 1 e n]
& [t e n & 0 e n & 1 e n => (t,0,1) e n3]
Iff-And, 228
230 (t,0,1) e n3 => t e n & 0 e n & 1 e n
Split, 229
231 t e n & 0 e n & 1 e n => (t,0,1) e n3
Split, 229
232 t e n & 0 e n
Join, 218, 4
233 t e n & 0 e n & 1 e n
Join, 232, 5
234 (t,0,1) e n3
Detach, 231, 233
Prove: ~[t=0 & 0=0 & 1=z]
Suppose to the contrary...
235 t=0 & 0=0 & 1=z
Premise
236 t=0
Split, 235
237 0=0
Split, 235
238 1=z
Split, 235
239 t=0 & ~t=0
Join, 236, 219
As Required:
240 ~[t=0 & 0=0 & 1=z]
4 Conclusion, 235
241 (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]
Join, 234, 240
242 (t,0,1) e q
Detach, 225, 241
As Required:
243 ~t=0 => (t,0,1) e q
4 Conclusion, 219
As Required:
244 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
4 Conclusion, 218
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Suppose...
245 (t,u,v) e q
Premise
246 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]
U Spec, 161
247 ALL(c):[(t,u,c) e q
<=> (t,u,c) e n3 & ~[t=0 & u=0 & c=z]]
U Spec, 246
248 (t,u,v) e q
<=> (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
U Spec, 247
249 [(t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]]
& [(t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q]
Iff-And, 248
250 (t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
Split, 249
251 (t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q
Split, 249
252 (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
Detach, 250, 245
253 (t,u,v) e n3
Split, 252
254 ~[t=0 & u=0 & v=z]
Split, 252
255 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 25
256 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 255
257 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 256
258 [(t,u,v) e n3 => t e n & u e n & v e n]
& [t e n & u e n & v e n => (t,u,v) e n3]
Iff-And, 257
259 (t,u,v) e n3 => t e n & u e n & v e n
Split, 258
260 t e n & u e n & v e n => (t,u,v) e n3
Split, 258
261 t e n & u e n & v e n
Detach, 259, 253
262 t e n
Split, 261
263 u e n
Split, 261
264 v e n
Split, 261
265 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]
U Spec, 161
266 ALL(c):[(t,u+1,c) e q
<=> (t,u+1,c) e n3 & ~[t=0 & u+1=0 & c=z]]
U Spec, 265
267 (t,u+1,v*t) e q
<=> (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]
U Spec, 266
268 [(t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]]
& [(t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q]
Iff-And, 267
269 (t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]
Split, 268
270 (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q
Split, 268
271 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 25
272 ALL(c3):[(t,u+1,c3) e n3 <=> t e n & u+1 e n & c3 e n]
U Spec, 271
273 (t,u+1,v*t) e n3 <=> t e n & u+1 e n & v*t e n
U Spec, 272
274 [(t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n]
& [t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3]
Iff-And, 273
275 (t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n
Split, 274
276 t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3
Split, 274
277 ALL(b):[u e n & b e n => u+b e n]
U Spec, 2
278 u e n & 1 e n => u+1 e n
U Spec, 277
279 u e n & 1 e n
Join, 263, 5
280 u+1 e n
Detach, 278, 279
281 ALL(b):[v e n & b e n => v*b e n]
U Spec, 3
282 v e n & t e n => v*t e n
U Spec, 281
283 v e n & t e n
Join, 264, 262
284 v*t e n
Detach, 282, 283
285 t e n & u+1 e n
Join, 262, 280
286 t e n & u+1 e n & v*t e n
Join, 285, 284
287 (t,u+1,v*t) e n3
Detach, 276, 286
288 t=0 & u+1=0 & v*t=z
Premise
289 t=0
Split, 288
290 u+1=0
Split, 288
291 v*t=z
Split, 288
292 u e n => ~u+1=0
U Spec, 15
293 ~u+1=0
Detach, 292, 263
294 u+1=0 & ~u+1=0
Join, 290, 293
295 ~[t=0 & u+1=0 & v*t=z]
4 Conclusion, 288
296 (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]
Join, 287, 295
297 (t,u+1,v*t) e q
Detach, 270, 296
As Required:
298 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
4 Conclusion, 245
299 q e pn3 & (0,0,x0) e q
Join, 177, 201
300 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Join, 299, 244
301 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Join, 300, 298
302 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
& ~(0,0,z) e q
Join, 301, 217
303 EXIST(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
& ~(0,0,z) e d]
E Gen, 302
304 ~(0,0,z) e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
& ~(0,0,z) e d]
Arb Or, 303
305 ~(0,0,z) e pow
Detach, 157, 304
306 (0,0,z) e pow & ~(0,0,z) e pow
Join, 143, 305
As Required:
307 ~[(0,0,z) e pow & ~z=x0]
4 Conclusion, 142
308 ~~[(0,0,z) e pow => ~~z=x0]
Imply-And, 307
309 (0,0,z) e pow => ~~z=x0
Rem DNeg, 308
310 (0,0,z) e pow => z=x0
Rem DNeg, 309
As Required:
311 ALL(a):[a e n => [(0,0,a) e pow => a=x0]]
4 Conclusion, 141
Prove: ALL(a):[a e n
=> [~a=0 => ALL(b):[b e n => [(a,0,b) e pow => b=1]]]]
Suppose...
312 x e n
Premise
Prove: ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]
Suppose...
313 ~x=0
Premise
Prove: ALL(b):[b e n => [(x,0,b) e pow => b=1]]
Suppose...
314 z e n
Premise
Prove: ~[(x,0,z) e pow & ~z=1]
Suppose to the contrary...
315 (x,0,z) e pow & ~z=1
Premise
316 (x,0,z) e pow
Split, 315
317 ~z=1
Split, 315
318 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,b,c) e d]]
U Spec, 36
319 ALL(c):[(x,0,c) e pow
<=> (x,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,c) e d]]
U Spec, 318
320 (x,0,z) e pow
<=> (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]
U Spec, 319
321 [(x,0,z) e pow => (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]]
& [(x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d] => (x,0,z) e pow]
Iff-And, 320
322 (x,0,z) e pow => (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]
Split, 321
323 (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d] => (x,0,z) e pow
Split, 321
324 (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]
Detach, 322, 316
325 (x,0,z) e n3
Split, 324
326 ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]
Split, 324
327 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,b,c) e d]]
U Spec, 36
328 ALL(c):[(x,0,c) e pow
<=> (x,0,c) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,c) e d]]
U Spec, 327
329 (x,0,z) e pow
<=> (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]
U Spec, 328
330 [(x,0,z) e pow => (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]]
& [(x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d] => (x,0,z) e pow]
Iff-And, 329
331 (x,0,z) e pow => (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]
Split, 330
332 (x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d] => (x,0,z) e pow
Split, 330
333 ~[(x,0,z) e n3 & ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]] => ~(x,0,z) e pow
Contra, 331
334 ~~[~(x,0,z) e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d]] => ~(x,0,z) e pow
DeMorgan, 333
335 ~(x,0,z) e n3 | ~ALL(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d]
=> (x,0,z) e d] => ~(x,0,z) e pow
Rem DNeg, 334
336 ~(x,0,z) e n3 | ~ALL(d):~[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e pow
Imply-And, 335
337 ~(x,0,z) e n3 | ~~EXIST(d):~~[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e pow
Quant, 336
338 ~(x,0,z) e n3 | EXIST(d):~~[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e pow
Rem DNeg, 337
Sufficient: ~(x,0,z) e pow (to obtain contradiction)
339 ~(x,0,z) e n3 | EXIST(d):[d e pn3 & (0,0,x0) e d
& ALL(e):[e e n => [~e=0 => (e,0,1) e d]]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g*e) e d] & ~(x,0,z) e d] => ~(x,0,z) e pow
Rem DNeg, 338
340 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e n3 & ~[a=x & b=0 & c=z]]]
Subset, 24
341 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e n3 & ~[a=x & b=0 & c=z]]
E Spec, 340
Define: q
*********
342 Set''(q)
Split, 341
343 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e n3 & ~[a=x & b=0 & c=z]]
Split, 341
344 q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
U Spec, 31
345 [q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]]
& [Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3]
Iff-And, 344
346 q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Split, 345
347 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 345
348 (t,u,v) e q
Premise
349 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]
U Spec, 343
350 ALL(c):[(t,u,c) e q
<=> (t,u,c) e n3 & ~[t=x & u=0 & c=z]]
U Spec, 349
351 (t,u,v) e q
<=> (t,u,v) e n3 & ~[t=x & u=0 & v=z]
U Spec, 350
352 [(t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]]
& [(t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q]
Iff-And, 351
353 (t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]
Split, 352
354 (t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q
Split, 352
355 (t,u,v) e n3 & ~[t=x & u=0 & v=z]
Detach, 353, 348
356 (t,u,v) e n3
Split, 355
357 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
4 Conclusion, 348
358 Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Join, 342, 357
359 q e pn3
Detach, 347, 358
360 ALL(b):ALL(c):[(x,b,c) e q
<=> (x,b,c) e n3 & ~[x=x & b=0 & c=z]]
U Spec, 343
361 ALL(c):[(x,0,c) e q
<=> (x,0,c) e n3 & ~[x=x & 0=0 & c=z]]
U Spec, 360
362 (x,0,z) e q
<=> (x,0,z) e n3 & ~[x=x & 0=0 & z=z]
U Spec, 361
363 [(x,0,z) e q => (x,0,z) e n3 & ~[x=x & 0=0 & z=z]]
& [(x,0,z) e n3 & ~[x=x & 0=0 & z=z] => (x,0,z) e q]
Iff-And, 362
364 (x,0,z) e q => (x,0,z) e n3 & ~[x=x & 0=0 & z=z]
Split, 363
365 (x,0,z) e n3 & ~[x=x & 0=0 & z=z] => (x,0,z) e q
Split, 363
366 ~[(x,0,z) e n3 & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e q
Contra, 364
367 ~~[~(x,0,z) e n3 | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e q
DeMorgan, 366
368 ~(x,0,z) e n3 | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e q
Rem DNeg, 367
369 ~(x,0,z) e n3 | x=x & 0=0 & z=z => ~(x,0,z) e q
Rem DNeg, 368
370 x=x
Reflex
371 0=0
Reflex
372 z=z
Reflex
373 x=x & 0=0
Join, 370, 371
374 x=x & 0=0 & z=z
Join, 373, 372
375 ~(x,0,z) e n3 | x=x & 0=0 & z=z
Arb Or, 374
As Required:
376 ~(x,0,z) e q
Detach, 369, 375
377 t e n
Premise
378 ~t=0
Premise
379 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]
U Spec, 343
380 ALL(c):[(t,0,c) e q
<=> (t,0,c) e n3 & ~[t=x & 0=0 & c=z]]
U Spec, 379
381 (t,0,1) e q
<=> (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]
U Spec, 380
382 [(t,0,1) e q => (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]]
& [(t,0,1) e n3 & ~[t=x & 0=0 & 1=z] => (t,0,1) e q]
Iff-And, 381
383 (t,0,1) e q => (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]
Split, 382
Sufficient: (t,0,1) e q
384 (t,0,1) e n3 & ~[t=x & 0=0 & 1=z] => (t,0,1) e q
Split, 382
385 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 25
386 ALL(c3):[(t,0,c3) e n3 <=> t e n & 0 e n & c3 e n