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]
U Spec, 385
387 (t,0,1) e n3 <=> t e n & 0 e n & 1 e n
U Spec, 386
388 [(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, 387
389 (t,0,1) e n3 => t e n & 0 e n & 1 e n
Split, 388
390 t e n & 0 e n & 1 e n => (t,0,1) e n3
Split, 388
391 t e n & 0 e n
Join, 377, 4
392 t e n & 0 e n & 1 e n
Join, 391, 5
393 (t,0,1) e n3
Detach, 390, 392
394 t=x & 0=0 & 1=z
Premise
395 t=x
Split, 394
396 0=0
Split, 394
397 1=z
Split, 394
398 z=1
Sym, 397
399 z=1 & ~z=1
Join, 398, 317
400 ~[t=x & 0=0 & 1=z]
4 Conclusion, 394
401 (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]
Join, 393, 400
402 (t,0,1) e q
Detach, 384, 401
403 ~t=0 => (t,0,1) e q
4 Conclusion, 378
As Required:
404 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
4 Conclusion, 377
Suppose...
405 (t,u,v) e q
Premise
406 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]
U Spec, 343
407 ALL(c):[(t,u,c) e q
<=> (t,u,c) e n3 & ~[t=x & u=0 & c=z]]
U Spec, 406
408 (t,u,v) e q
<=> (t,u,v) e n3 & ~[t=x & u=0 & v=z]
U Spec, 407
409 [(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, 408
410 (t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]
Split, 409
411 (t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q
Split, 409
412 (t,u,v) e n3 & ~[t=x & u=0 & v=z]
Detach, 410, 405
413 (t,u,v) e n3
Split, 412
414 ~[t=x & u=0 & v=z]
Split, 412
415 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 25
416 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 415
417 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 416
418 [(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, 417
419 (t,u,v) e n3 => t e n & u e n & v e n
Split, 418
420 t e n & u e n & v e n => (t,u,v) e n3
Split, 418
421 t e n & u e n & v e n
Detach, 419, 413
422 t e n
Split, 421
423 u e n
Split, 421
424 v e n
Split, 421
425 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]
U Spec, 343
426 ALL(c):[(t,u+1,c) e q
<=> (t,u+1,c) e n3 & ~[t=x & u+1=0 & c=z]]
U Spec, 425
427 (t,u+1,v*t) e q
<=> (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]
U Spec, 426
428 [(t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]]
& [(t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q]
Iff-And, 427
429 (t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]
Split, 428
Sufficient: (t,u+1,v*t) e q
430 (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q
Split, 428
431 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 25
432 ALL(c3):[(t,u+1,c3) e n3 <=> t e n & u+1 e n & c3 e n]
U Spec, 431
433 (t,u+1,v*t) e n3 <=> t e n & u+1 e n & v*t e n
U Spec, 432
434 [(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, 433
435 (t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n
Split, 434
436 t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3
Split, 434
437 ALL(b):[u e n & b e n => u+b e n]
U Spec, 2
438 u e n & 1 e n => u+1 e n
U Spec, 437
439 u e n & 1 e n
Join, 423, 5
440 u+1 e n
Detach, 438, 439
441 ALL(b):[v e n & b e n => v*b e n]
U Spec, 3
442 v e n & t e n => v*t e n
U Spec, 441
443 v e n & t e n
Join, 424, 422
444 v*t e n
Detach, 442, 443
445 t e n & u+1 e n
Join, 422, 440
446 t e n & u+1 e n & v*t e n
Join, 445, 444
447 (t,u+1,v*t) e n3
Detach, 436, 446
448 t=x & u+1=0 & v*t=z
Premise
449 t=x
Split, 448
450 u+1=0
Split, 448
451 v*t=z
Split, 448
452 u e n => ~u+1=0
U Spec, 15
453 ~u+1=0
Detach, 452, 423
454 u+1=0 & ~u+1=0
Join, 450, 453
455 ~[t=x & u+1=0 & v*t=z]
4 Conclusion, 448
456 (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]
Join, 447, 455
457 (t,u+1,v*t) e q
Detach, 430, 456
As Required:
458 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
4 Conclusion, 405
459 ALL(b):ALL(c):[(0,b,c) e q
<=> (0,b,c) e n3 & ~[0=x & b=0 & c=z]]
U Spec, 343
460 ALL(c):[(0,0,c) e q
<=> (0,0,c) e n3 & ~[0=x & 0=0 & c=z]]
U Spec, 459
461 (0,0,x0) e q
<=> (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]
U Spec, 460
462 [(0,0,x0) e q => (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]]
& [(0,0,x0) e n3 & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q]
Iff-And, 461
463 (0,0,x0) e q => (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]
Split, 462
464 (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q
Split, 462
465 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 25
466 ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]
U Spec, 465
467 (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n
U Spec, 466
468 [(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, 467
469 (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n
Split, 468
470 0 e n & 0 e n & x0 e n => (0,0,x0) e n3
Split, 468
471 0 e n & 0 e n
Join, 4, 4
472 0 e n & 0 e n & x0 e n
Join, 471, 32
473 (0,0,x0) e n3
Detach, 470, 472
474 0=x & 0=0 & x0=z
Premise
475 0=x
Split, 474
476 0=0
Split, 474
477 x0=z
Split, 474
478 x=0
Sym, 475
479 x=0 & ~x=0
Join, 478, 313
480 ~[0=x & 0=0 & x0=z]
4 Conclusion, 474
481 (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]
Join, 473, 480
As Required:
482 (0,0,x0) e q
Detach, 464, 481
483 q e pn3 & (0,0,x0) e q
Join, 359, 482
484 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Join, 483, 404
485 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, 484, 458
486 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,0,z) e q
Join, 485, 376
487 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]
E Gen, 486
488 ~(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]
Arb Or, 487
489 ~(x,0,z) e pow
Detach, 339, 488
490 (x,0,z) e pow & ~(x,0,z) e pow
Join, 316, 489
As Required:
491 ~[(x,0,z) e pow & ~z=1]
4 Conclusion, 315
492 ~~[(x,0,z) e pow => ~~z=1]
Imply-And, 491
493 (x,0,z) e pow => ~~z=1
Rem DNeg, 492
494 (x,0,z) e pow => z=1
Rem DNeg, 493
As Required:
495 ALL(b):[b e n => [(x,0,b) e pow => b=1]]
4 Conclusion, 314
As Required:
496 ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]
4 Conclusion, 313
As Required:
497 ALL(a):[a e n
=> [~a=0 => ALL(b):[b e n => [(a,0,b) e pow => b=1]]]]
4 Conclusion, 312
Prove: pow is a function
Apply Function Axiom
498 ALL(f):ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e f => c1 e a1 & c2 e a2 & d e b]
& ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e f]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e f & (c1,c2,d2) e f => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=f(c1,c2) <=> (c1,c2,d) e f]]
Function
499 ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e a1 & c2 e a2 & d e b]
& ALL(c1):ALL(c2):[c1 e a1 & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e pow]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]]
U Spec, 498
500 ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e a2 & d e b]
& ALL(c1):ALL(c2):[c1 e n & c2 e a2 => EXIST(d):[d e b & (c1,c2,d) e pow]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]]
U Spec, 499
501 ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e b]
& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e b & (c1,c2,d) e pow]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]]
U Spec, 500
Sufficient: For functionality of pow
502 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]
& ALL(c1):ALL(c2):[c1 e n & c2 e n => EXIST(d):[d e n & (c1,c2,d) e pow]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]
U Spec, 501
Prove: ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]
Suppose...
503 (x,y,z) e pow
Premise
504 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
505 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, 504
506 (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, 505
507 [(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, 506
508 (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, 507
509 (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, 507
510 (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, 508, 503
511 (x,y,z) e n3
Split, 510
512 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, 510
513 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 25
514 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 513
515 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 514
516 [(x,y,z) e n3 => x e n & y e n & z e n]
& [x e n & y e n & z e n => (x,y,z) e n3]
Iff-And, 515
517 (x,y,z) e n3 => x e n & y e n & z e n
Split, 516
518 x e n & y e n & z e n => (x,y,z) e n3
Split, 516
519 x e n & y e n & z e n
Detach, 517, 511
Functionality of pow, Part 1
520 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]
4 Conclusion, 503
Prove: ALL(a):[a e n
=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e pow]]]
Suppose...
521 x e n
Premise
522 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]]
Subset, 1
523 Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]
E Spec, 522
Define: p1
**********
524 Set(p1)
Split, 523
525 ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]
Split, 523
Apply Principle of Mathematical Induction
526 Set(p1) & ALL(b):[b e p1 => b e n]
=> [0 e p1 & ALL(b):[b e p1 => b+1 e p1]
=> ALL(b):[b e n => b e p1]]
U Spec, 13
Prove: ALL(b):[b e p1 => b e n]
Suppose...
527 y e p1
Premise
528 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 525
529 [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]]
& [y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1]
Iff-And, 528
530 y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]
Split, 529
531 y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1
Split, 529
532 y e n & EXIST(c):[c e n & (x,y,c) e pow]
Detach, 530, 527
533 y e n
Split, 532
As Required:
534 ALL(b):[b e p1 => b e n]
4 Conclusion, 527
535 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 524, 534
Sufficient: ALL(b):[b e n => b e p1]
536 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
=> ALL(b):[b e n => b e p1]
Detach, 526, 535
537 0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e pow]
U Spec, 525
538 [0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e pow]]
& [0 e n & EXIST(c):[c e n & (x,0,c) e pow] => 0 e p1]
Iff-And, 537
539 0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e pow]
Split, 538
540 0 e n & EXIST(c):[c e n & (x,0,c) e pow] => 0 e p1
Split, 538
2 Cases:
541 x=0 | ~x=0
Or Not
Case one
Prove: x=0 => 0 e p1
Suppose...
542 x=0
Premise
543 (x,0,x0) e pow
Substitute, 542, 57
544 x0 e n & (x,0,x0) e pow
Join, 32, 543
545 EXIST(c):[c e n & (x,0,c) e pow]
E Gen, 544
546 0 e n & EXIST(c):[c e n & (x,0,c) e pow]
Join, 4, 545
547 0 e p1
Detach, 540, 546
As Required:
548 x=0 => 0 e p1
4 Conclusion, 542
Case 2
Prove: ~x=0 => 0 e p1
Suppose...
549 ~x=0
Premise
550 x e n => [~x=0 => (x,0,1) e pow]
U Spec, 87
551 ~x=0 => (x,0,1) e pow
Detach, 550, 521
552 (x,0,1) e pow
Detach, 551, 549
553 1 e n & (x,0,1) e pow
Join, 5, 552
554 EXIST(c):[c e n & (x,0,c) e pow]
E Gen, 553
555 0 e n & EXIST(c):[c e n & (x,0,c) e pow]
Join, 4, 554
556 0 e p1
Detach, 540, 555
As Required:
557 ~x=0 => 0 e p1
4 Conclusion, 549
558 [x=0 => 0 e p1] & [~x=0 => 0 e p1]
Join, 548, 557
As Required:
559 0 e p1
Cases, 541, 558
Prove: ALL(b):[b e p1 => b+1 e p1]
Suppose...
560 y e p1
Premise
561 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 525
562 [y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]]
& [y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1]
Iff-And, 561
563 y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]
Split, 562
564 y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1
Split, 562
565 y e n & EXIST(c):[c e n & (x,y,c) e pow]
Detach, 563, 560
566 y e n
Split, 565
567 EXIST(c):[c e n & (x,y,c) e pow]
Split, 565
568 z e n & (x,y,z) e pow
E Spec, 567
569 z e n
Split, 568
570 (x,y,z) e pow
Split, 568
571 y+1 e p1 <=> y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]
U Spec, 525
572 [y+1 e p1 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]]
& [y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow] => y+1 e p1]
Iff-And, 571
573 y+1 e p1 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]
Split, 572
Sufficient: y+1 e p1
574 y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow] => y+1 e p1
Split, 572
575 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
576 y e n & 1 e n => y+1 e n
U Spec, 575
577 y e n & 1 e n
Join, 566, 5
578 y+1 e n
Detach, 576, 577
579 ALL(b):ALL(c):[x e n & b e n & c e n
=> [(x,b,c) e pow => (x,b+1,c*x) e pow]]
U Spec, 140
580 ALL(c):[x e n & y e n & c e n
=> [(x,y,c) e pow => (x,y+1,c*x) e pow]]
U Spec, 579
581 x e n & y e n & z e n
=> [(x,y,z) e pow => (x,y+1,z*x) e pow]
U Spec, 580
582 x e n & y e n
Join, 521, 566
583 x e n & y e n & z e n
Join, 582, 569
584 (x,y,z) e pow => (x,y+1,z*x) e pow
Detach, 581, 583
585 (x,y+1,z*x) e pow
Detach, 584, 570
586 ALL(b):[z e n & b e n => z*b e n]
U Spec, 3
587 z e n & x e n => z*x e n
U Spec, 586
588 z e n & x e n
Join, 569, 521
589 z*x e n
Detach, 587, 588
590 z*x e n & (x,y+1,z*x) e pow
Join, 589, 585
591 EXIST(c):[c e n & (x,y+1,c) e pow]
E Gen, 590
592 y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]
Join, 578, 591
593 y+1 e p1
Detach, 574, 592
As Required:
594 ALL(b):[b e p1 => b+1 e p1]
4 Conclusion, 560
595 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
Join, 559, 594
596 ALL(b):[b e n => b e p1]
Detach, 536, 595
Prove: ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]
Suppose...
597 t e n
Premise
598 t e n => t e p1
U Spec, 596
599 t e p1
Detach, 598, 597
600 t e p1 <=> t e n & EXIST(c):[c e n & (x,t,c) e pow]
U Spec, 525
601 [t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e pow]]
& [t e n & EXIST(c):[c e n & (x,t,c) e pow] => t e p1]
Iff-And, 600
602 t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e pow]
Split, 601
603 t e n & EXIST(c):[c e n & (x,t,c) e pow] => t e p1
Split, 601
604 t e n & EXIST(c):[c e n & (x,t,c) e pow]
Detach, 602, 599
605 t e n
Split, 604
606 EXIST(c):[c e n & (x,t,c) e pow]
Split, 604
As Required:
607 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]
4 Conclusion, 597
As Required:
608 ALL(a):[a e n
=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e pow]]]
4 Conclusion, 521
Prove: ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]
Suppose...
609 x e n & y e n
Premise
610 x e n
Split, 609
611 y e n
Split, 609
612 x e n
=> ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]
U Spec, 608
613 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]
Detach, 612, 610
614 y e n => EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 613
615 EXIST(c):[c e n & (x,y,c) e pow]
Detach, 614, 611
Functionality of pow, Part 2
616 ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]
4 Conclusion, 609
Prove: ALL(a):[a e n
=> ALL(b):[b e n
=> ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]]]]
Suppose...
617 x e n
Premise
618 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]]
Subset, 1
619 Set(p2) & ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]
E Spec, 618
Define: p2
**********
620 Set(p2)
Split, 619
621 ALL(b):[b e p2 <=> b e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]
Split, 619
Apply Principle of Mathematical Induction
622 Set(p2) & ALL(b):[b e p2 => b e n]
=> [0 e p2 & ALL(b):[b e p2 => b+1 e p2]
=> ALL(b):[b e n => b e p2]]
U Spec, 13
Prove: ALL(b):[b e p2 => b e n]
Suppose...
623 y e p2
Premise
624 y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
U Spec, 621
625 [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]]
& [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2]
Iff-And, 624
626 y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Split, 625
627 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2
Split, 625
628 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Detach, 626, 623
629 y e n
Split, 628
As Required:
630 ALL(b):[b e p2 => b e n]
4 Conclusion, 623
631 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 620, 630
Sufficient: ALL(b):[b e n => b e p2]
632 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
=> ALL(b):[b e n => b e p2]
Detach, 622, 631
633 0 e p2 <=> 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]
U Spec, 621
634 [0 e p2 => 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]]
& [0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]] => 0 e p2]
Iff-And, 633
635 0 e p2 => 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]
Split, 634
Sufficient: 0 e p2
636 0 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]] => 0 e p2
Split, 634
Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]
Suppose...
637 z1 e n & z2 e n
Premise
638 z1 e n
Split, 637
639 z2 e n
Split, 637
Prove: (x,0,z1) e pow & (x,0,z2) e pow => z1=z2
Suppose...
640 (x,0,z1) e pow & (x,0,z2) e pow
Premise
641 (x,0,z1) e pow
Split, 640
642 (x,0,z2) e pow
Split, 640
2 cases:
643 x=0 | ~x=0
Or Not
Case one
Prove: x=0 => z1=z2
Suppose...
644 x=0
Premise
645 z1 e n => [(0,0,z1) e pow => z1=x0]
U Spec, 311
646 (0,0,z1) e pow => z1=x0
Detach, 645, 638
647 (x,0,z1) e pow => z1=x0
Substitute, 644, 646
648 z1=x0
Detach, 647, 641
649 z2 e n => [(0,0,z2) e pow => z2=x0]
U Spec, 311
650 (0,0,z2) e pow => z2=x0
Detach, 649, 639
651 (x,0,z2) e pow => z2=x0
Substitute, 644, 650
652 z2=x0
Detach, 651, 642
653 z1=z2
Substitute, 652, 648
As Required:
654 x=0 => z1=z2
4 Conclusion, 644
Case two
Prove: ~x=0 => z1=z2
Suppose...
655 ~x=0
Premise
656 x e n
=> [~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]]
U Spec, 497
657 ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]
Detach, 656, 617
658 ALL(b):[b e n => [(x,0,b) e pow => b=1]]
Detach, 657, 655
659 z1 e n => [(x,0,z1) e pow => z1=1]
U Spec, 658
660 (x,0,z1) e pow => z1=1
Detach, 659, 638
661 z1=1
Detach, 660, 641
662 z2 e n => [(x,0,z2) e pow => z2=1]
U Spec, 658
663 (x,0,z2) e pow => z2=1
Detach, 662, 639
664 z2=1
Detach, 663, 642
665 z1=z2
Substitute, 664, 661
As Required:
666 ~x=0 => z1=z2
4 Conclusion, 655
667 [x=0 => z1=z2] & [~x=0 => z1=z2]
Join, 654, 666
668 z1=z2
Cases, 643, 667
As Required:
669 (x,0,z1) e pow & (x,0,z2) e pow => z1=z2
4 Conclusion, 640
As Required:
670 ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]
4 Conclusion, 637
671 0 e n
& ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]
Join, 4, 670
As Required:
672 0 e p2
Detach, 636, 671
Prove: ALL(b):[b e p2 => b+1 e p2]
Suppose...
673 y e p2
Premise
674 y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
U Spec, 621
675 [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]]
& [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2]
Iff-And, 674
676 y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Split, 675
677 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2
Split, 675
678 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Detach, 676, 673
679 y e n
Split, 678
680 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Split, 678
681 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]
U Spec, 616
682 x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 681
683 x e n & y e n
Join, 617, 679
684 EXIST(c):[c e n & (x,y,c) e pow]
Detach, 682, 683
685 z e n & (x,y,z) e pow
E Spec, 684
686 z e n
Split, 685
687 (x,y,z) e pow
Split, 685
688 ALL(c2):[z e n & c2 e n => [(x,y,z) e pow & (x,y,c2) e pow => z=c2]]
U Spec, 680
Prove: ALL(c):[c e n => [(x,y,c) e pow => z=c]]
Suppose...
689 z' e n
Premise
690 z e n & z' e n => [(x,y,z) e pow & (x,y,z') e pow => z=z']
U Spec, 688
691 z e n & z' e n
Join, 686, 689
692 (x,y,z) e pow & (x,y,z') e pow => z=z'
Detach, 690, 691
693 (x,y,z') e pow
Premise
694 (x,y,z) e pow & (x,y,z') e pow
Join, 687, 693
695 z=z'
Detach, 692, 694
696 (x,y,z') e pow => z=z'
4 Conclusion, 693
As Required:
697 ALL(c):[c e n => [(x,y,c) e pow => z=c]]
4 Conclusion, 689
Prove: ALL(d):[d e n => [(x,y+1,d) e pow => d=z*x]]
Suppose...
698 z' e n
Premise
Prove: ~[(x,y+1,z') e pow & ~z'=z*x]
Suppose to the contrary...
699 (x,y+1,z') e pow & ~z'=z*x
Premise
700 (x,y+1,z') e pow
Split, 699
701 ~z'=z*x
Split, 699
702 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
703 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, 702
704 (x,y+1,z') e pow
<=> (x,y+1,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+1,z') e d]
U Spec, 703
705 [(x,y+1,z') e pow => (x,y+1,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+1,z') e d]]
& [(x,y+1,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+1,z') e d] => (x,y+1,z') e pow]
Iff-And, 704
706 (x,y+1,z') e pow => (x,y+1,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+1,z') e d]
Split, 705
707 (x,y+1,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+1,z') e d] => (x,y+1,z') e pow
Split, 705
708 ~[(x,y+1,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+1,z') e d]] => ~(x,y+1,z') e pow
Contra, 706
709 ~~[~(x,y+1,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+1,z') e d]] => ~(x,y+1,z') e pow
DeMorgan, 708
710 ~(x,y+1,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+1,z') e d] => ~(x,y+1,z') e pow
Rem DNeg, 709
711 ~(x,y+1,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+1,z') e d] => ~(x,y+1,z') e pow
Imply-And, 710
712 ~(x,y+1,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,y+1,z') e d] => ~(x,y+1,z') e pow
Quant, 711
713 ~(x,y+1,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,y+1,z') e d] => ~(x,y+1,z') e pow
Rem DNeg, 712
Sufficient: ~(x,y+1,z') e pow (to obtain a contradiction)
714 ~(x,y+1,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,y+1,z') e d] => ~(x,y+1,z') e pow
Rem DNeg, 713
715 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]]
Subset, 35
716 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]
E Spec, 715
Define: q
*********
717 Set''(q)
Split, 716
718 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]
Split, 716
719 q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
U Spec, 31
720 [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, 719
721 q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Split, 720
Sufficient: q e pn3
722 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 720
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]
Suppose...
723 (t,u,v) e q
Premise
724 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 718
725 ALL(c):[(t,u,c) e q
<=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]
U Spec, 724
726 (t,u,v) e q
<=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
U Spec, 725
727 [(t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']]
& [(t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]
Iff-And, 726
728 (t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Split, 727
729 (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q
Split, 727
730 (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Detach, 728, 723
731 (t,u,v) e pow
Split, 730
732 ~[t=x & u=y+1 & v=z']
Split, 730
733 ALL(b):ALL(c):[(t,b,c) e pow
<=> (t,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]
=> (t,b,c) e d]]
U Spec, 36
734 ALL(c):[(t,u,c) e pow
<=> (t,u,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]
=> (t,u,c) e d]]
U Spec, 733
735 (t,u,v) e pow
<=> (t,u,v) 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]
=> (t,u,v) e d]
U Spec, 734
736 [(t,u,v) e pow => (t,u,v) 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]
=> (t,u,v) e d]]
& [(t,u,v) 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]
=> (t,u,v) e d] => (t,u,v) e pow]
Iff-And, 735
737 (t,u,v) e pow => (t,u,v) 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]
=> (t,u,v) e d]
Split, 736
738 (t,u,v) 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]
=> (t,u,v) e d] => (t,u,v) e pow
Split, 736
739 (t,u,v) 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]
=> (t,u,v) e d]
Detach, 737, 731
740 (t,u,v) e n3
Split, 739
As Required:
741 ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]
4 Conclusion, 723
742 Set''(q)
& ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]
Join, 717, 741
As Required:
743 q e pn3
Detach, 722, 742
744 ALL(b):ALL(c):[(0,b,c) e q
<=> (0,b,c) e pow & ~[0=x & b=y+1 & c=z']]
U Spec, 718
745 ALL(c):[(0,0,c) e q
<=> (0,0,c) e pow & ~[0=x & 0=y+1 & c=z']]
U Spec, 744
746 (0,0,x0) e q
<=> (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']
U Spec, 745
747 [(0,0,x0) e q => (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']]
& [(0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q]
Iff-And, 746
748 (0,0,x0) e q => (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']
Split, 747
749 (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q
Split, 747
Prove: ~[0=x & 0=y+1 & x0=z']
Suppose to the contrary...
750 0=x & 0=y+1 & x0=z'
Premise
751 0=x
Split, 750
752 0=y+1
Split, 750
753 x0=z'
Split, 750
754 y e n => ~y+1=0
U Spec, 15
755 ~y+1=0
Detach, 754, 679
756 y+1=0
Sym, 752
757 y+1=0 & ~y+1=0
Join, 756, 755
As Required:
758 ~[0=x & 0=y+1 & x0=z']
4 Conclusion, 750
759 (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']
Join, 57, 758
As Required:
760 (0,0,x0) e q
Detach, 749, 759
761 ALL(b):ALL(c):[(x,b,c) e q
<=> (x,b,c) e pow & ~[x=x & b=y+1 & c=z']]
U Spec, 718
762 ALL(c):[(x,y+1,c) e q
<=> (x,y+1,c) e pow & ~[x=x & y+1=y+1 & c=z']]
U Spec, 761
763 (x,y+1,z') e q
<=> (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']
U Spec, 762
764 [(x,y+1,z') e q => (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']]
& [(x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q]
Iff-And, 763
765 (x,y+1,z') e q => (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']
Split, 764
766 (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q
Split, 764
767 ~[(x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q
Contra, 765
768 ~~[~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q
DeMorgan, 767
769 ~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z'] => ~(x,y+1,z') e q
Rem DNeg, 768
770 ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z' => ~(x,y+1,z') e q
Rem DNeg, 769
771 x=x
Reflex
772 y+1=y+1
Reflex
773 z'=z'
Reflex
774 x=x & y+1=y+1
Join, 771, 772
775 x=x & y+1=y+1 & z'=z'
Join, 774, 773
776 ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z'
Arb Or, 775
As Required:
777 ~(x,y+1,z') e q
Detach, 770, 776
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Suppose...
778 (t,u,v) e q
Premise
779 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 718
780 ALL(c):[(t,u,c) e q
<=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]
U Spec, 779
781 (t,u,v) e q
<=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
U Spec, 780
782 [(t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']]
& [(t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q]
Iff-And, 781
783 (t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Split, 782
784 (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q
Split, 782
785 (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Detach, 783, 778
786 (t,u,v) e pow
Split, 785
787 ~[t=x & u=y+1 & v=z']
Split, 785
788 ALL(b):ALL(c):[(t,b,c) e pow
<=> (t,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]
=> (t,b,c) e d]]
U Spec, 36
789 ALL(c):[(t,u,c) e pow
<=> (t,u,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]
=> (t,u,c) e d]]
U Spec, 788
790 (t,u,v) e pow
<=> (t,u,v) 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]
=> (t,u,v) e d]
U Spec, 789
791 [(t,u,v) e pow => (t,u,v) 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]
=> (t,u,v) e d]]
& [(t,u,v) 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]
=> (t,u,v) e d] => (t,u,v) e pow]
Iff-And, 790
792 (t,u,v) e pow => (t,u,v) 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]
=> (t,u,v) e d]
Split, 791
793 (t,u,v) 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]
=> (t,u,v) e d] => (t,u,v) e pow
Split, 791
794 (t,u,v) 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]
=> (t,u,v) e d]
Detach, 792, 786
795 (t,u,v) e n3
Split, 794
796 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 25
797 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 796
798 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 797
799 [(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, 798
800 (t,u,v) e n3 => t e n & u e n & v e n
Split, 799
801 t e n & u e n & v e n => (t,u,v) e n3
Split, 799
802 t e n & u e n & v e n
Detach, 800, 795
803 t e n
Split, 802
804 u e n
Split, 802
805 v e n
Split, 802
806 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]
=> (t,u,v) e d]
Split, 794
807 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 718
808 ALL(c):[(t,u+1,c) e q
<=> (t,u+1,c) e pow & ~[t=x & u+1=y+1 & c=z']]
U Spec, 807
809 (t,u+1,v*t) e q
<=> (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']
U Spec, 808
810 [(t,u+1,v*t) e q => (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']]
& [(t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q]
Iff-And, 809
811 (t,u+1,v*t) e q => (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']
Split, 810
812 (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q
Split, 810
813 ALL(b):ALL(c):[t e n & b e n & c e n
=> [(t,b,c) e pow => (t,b+1,c*t) e pow]]
U Spec, 140
814 ALL(c):[t e n & u e n & c e n
=> [(t,u,c) e pow => (t,u+1,c*t) e pow]]
U Spec, 813
815 t e n & u e n & v e n
=> [(t,u,v) e pow => (t,u+1,v*t) e pow]
U Spec, 814
816 (t,u,v) e pow => (t,u+1,v*t) e pow
Detach, 815, 802
817 (t,u+1,v*t) e pow
Detach, 816, 786
Prove: ~[t=x & u+1=y+1 & v*t=z']
Suppose to the contrary...
818 t=x & u+1=y+1 & v*t=z'
Premise
819 t=x
Split, 818
820 u+1=y+1
Split, 818
821 v*t=z'
Split, 818
822 v*x=z'
Substitute, 819, 821
823 ALL(b):ALL(c):[u e n & b e n & c e n => [u+b=c+b => u=c]]
U Spec, 14
824 ALL(c):[u e n & 1 e n & c e n => [u+1=c+1 => u=c]]
U Spec, 823
825 u e n & 1 e n & y e n => [u+1=y+1 => u=y]
U Spec, 824
826 u e n & 1 e n
Join, 804, 5
827 u e n & 1 e n & y e n
Join, 826, 679
828 u+1=y+1 => u=y
Detach, 825, 827
829 u=y
Detach, 828, 820
830 (x,u,v) e pow
Substitute, 819, 786
831 (x,y,v) e pow
Substitute, 829, 830
832 v e n => [(x,y,v) e pow => z=v]
U Spec, 697
833 (x,y,v) e pow => z=v
Detach, 832, 805
834 z=v
Detach, 833, 831
835 z*x=z'
Substitute, 834, 822
836 z'=z*x
Sym, 835
837 z'=z*x & ~z'=z*x
Join, 836, 701
As Required:
838 ~[t=x & u+1=y+1 & v*t=z']
4 Conclusion, 818
839 (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']
Join, 817, 838
840 (t,u+1,v*t) e q
Detach, 812, 839
As Required:
841 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
4 Conclusion, 778
842 t e n
Premise
843 ~t=0
Premise
844 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 718
845 ALL(c):[(t,0,c) e q
<=> (t,0,c) e pow & ~[t=x & 0=y+1 & c=z']]
U Spec, 844
846 (t,0,1) e q
<=> (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']
U Spec, 845
847 [(t,0,1) e q => (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']]
& [(t,0,1) e pow & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q]
Iff-And, 846
848 (t,0,1) e q => (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']
Split, 847
Sufficient: (t,0,1) e q
849 (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q
Split, 847
850 t e n => [~t=0 => (t,0,1) e pow]
U Spec, 87
851 ~t=0 => (t,0,1) e pow
Detach, 850, 842
852 (t,0,1) e pow
Detach, 851, 843
853 t=x & 0=y+1 & 1=z'
Premise
854 t=x
Split, 853
855 0=y+1
Split, 853
856 1=z'
Split, 853
857 y e n => ~y+1=0
U Spec, 15
858 ~y+1=0
Detach, 857, 679
859 y+1=0
Sym, 855
860 y+1=0 & ~y+1=0
Join, 859, 858
861 ~[t=x & 0=y+1 & 1=z']
4 Conclusion, 853
862 (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']
Join, 852, 861
863 (t,0,1) e q
Detach, 849, 862
864 ~t=0 => (t,0,1) e q
4 Conclusion, 843
As Required:
865 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
4 Conclusion, 842
866 q e pn3 & (0,0,x0) e q
Join, 743, 760
867 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Join, 866, 865
868 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, 867, 841
869 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+1,z') e q
Join, 868, 777
870 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,y+1,z') e d]
E Gen, 869
871 ~(x,y+1,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,y+1,z') e d]
Arb Or, 870
872 ~(x,y+1,z') e pow
Detach, 714, 871
873 (x,y+1,z') e pow & ~(x,y+1,z') e pow
Join, 700, 872
As Required:
874 ~[(x,y+1,z') e pow & ~z'=z*x]
4 Conclusion, 699
875 ~~[(x,y+1,z') e pow => ~~z'=z*x]
Imply-And, 874
876 (x,y+1,z') e pow => ~~z'=z*x
Rem DNeg, 875
877 (x,y+1,z') e pow => z'=z*x
Rem DNeg, 876
As Required:
878 ALL(d):[d e n => [(x,y+1,d) e pow => d=z*x]]
4 Conclusion, 698
879 y+1 e p2 <=> y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]
U Spec, 621
880 [y+1 e p2 => y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]]
& [y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]] => y+1 e p2]
Iff-And, 879
881 y+1 e p2 => y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]
Split, 880
Sufficient: y+1 e p2
882 y+1 e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]] => y+1 e p2
Split, 880
883 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
884 y e n & 1 e n => y+1 e n
U Spec, 883
885 y e n & 1 e n
Join, 679, 5
886 y+1 e n
Detach, 884, 885
Prove: ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]
Suppose...
887 z1 e n & z2 e n
Premise
888 z1 e n
Split, 887
889 z2 e n
Split, 887
Prove: (x,y+1,z1) e pow & (x,y+1,z2) e pow => z1=z2
Suppose...
890 (x,y+1,z1) e pow & (x,y+1,z2) e pow
Premise
891 (x,y+1,z1) e pow
Split, 890
892 (x,y+1,z2) e pow
Split, 890
893 z1 e n => [(x,y+1,z1) e pow => z1=z*x]
U Spec, 878
894 (x,y+1,z1) e pow => z1=z*x
Detach, 893, 888
895 z1=z*x
Detach, 894, 891
896 z2 e n => [(x,y+1,z2) e pow => z2=z*x]
U Spec, 878
897 (x,y+1,z2) e pow => z2=z*x
Detach, 896, 889
898 z2=z*x
Detach, 897, 892
899 z1=z2
Substitute, 898, 895
As Required:
900 (x,y+1,z1) e pow & (x,y+1,z2) e pow => z1=z2
4 Conclusion, 890
As Required:
901 ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]
4 Conclusion, 887
902 y+1 e n
& ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,y+1,c1) e pow & (x,y+1,c2) e pow => c1=c2]]
Join, 886, 901
903 y+1 e p2
Detach, 882, 902
As Required:
904 ALL(b):[b e p2 => b+1 e p2]
4 Conclusion, 673
905 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
Join, 672, 904
As Required:
906 ALL(b):[b e n => b e p2]
Detach, 632, 905
Prove: ALL(b):[b e n
=> ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]
Suppose...
907 y e n
Premise
908 y e n => y e p2
U Spec, 906
909 y e p2
Detach, 908, 907
910 y e p2 <=> y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
U Spec, 621
911 [y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]]
& [y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2]
Iff-And, 910
912 y e p2 => y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Split, 911
913 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]] => y e p2
Split, 911
914 y e n & ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Detach, 912, 909
915 y e n
Split, 914
916 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Split, 914
As Required:
917 ALL(b):[b e n
=> ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]
4 Conclusion, 907
As Required:
918 ALL(a):[a e n
=> ALL(b):[b e n
=> ALL(c1):ALL(c2):[c1 e n & c2 e n => [(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]]]]
4 Conclusion, 617
Prove: ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]
Suppose...
919 (x,y,z1) e pow & (x,y,z2) e pow
Premise
920 (x,y,z1) e pow
Split, 919
921 (x,y,z2) e pow
Split, 919
922 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
923 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, 922
924 (x,y,z1) e pow
<=> (x,y,z1) 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,z1) e d]
U Spec, 923
925 [(x,y,z1) e pow => (x,y,z1) 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,z1) e d]]
& [(x,y,z1) 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,z1) e d] => (x,y,z1) e pow]
Iff-And, 924
926 (x,y,z1) e pow => (x,y,z1) 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,z1) e d]
Split, 925
927 (x,y,z1) 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,z1) e d] => (x,y,z1) e pow
Split, 925
928 (x,y,z1) 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,z1) e d]
Detach, 926, 920
929 (x,y,z1) e n3
Split, 928
930 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,z1) e d]
Split, 928
931 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 25
932 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 931
933 (x,y,z1) e n3 <=> x e n & y e n & z1 e n
U Spec, 932
934 [(x,y,z1) e n3 => x e n & y e n & z1 e n]
& [x e n & y e n & z1 e n => (x,y,z1) e n3]
Iff-And, 933
935 (x,y,z1) e n3 => x e n & y e n & z1 e n
Split, 934
936 x e n & y e n & z1 e n => (x,y,z1) e n3
Split, 934
937 x e n & y e n & z1 e n
Detach, 935, 929
938 x e n
Split, 937
939 y e n
Split, 937
940 z1 e n
Split, 937
941 (x,y,z2) e pow
<=> (x,y,z2) 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,z2) e d]
U Spec, 923
942 [(x,y,z2) e pow => (x,y,z2) 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,z2) e d]]
& [(x,y,z2) 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,z2) e d] => (x,y,z2) e pow]
Iff-And, 941
943 (x,y,z2) e pow => (x,y,z2) 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,z2) e d]
Split, 942
944 (x,y,z2) 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,z2) e d] => (x,y,z2) e pow
Split, 942
945 (x,y,z2) 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,z2) e d]
Detach, 943, 921
946 (x,y,z2) e n3
Split, 945
947 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,z2) e d]
Split, 945
948 (x,y,z2) e n3 <=> x e n & y e n & z2 e n
U Spec, 932
949 [(x,y,z2) e n3 => x e n & y e n & z2 e n]
& [x e n & y e n & z2 e n => (x,y,z2) e n3]
Iff-And, 948
950 (x,y,z2) e n3 => x e n & y e n & z2 e n
Split, 949
951 x e n & y e n & z2 e n => (x,y,z2) e n3
Split, 949
952 x e n & y e n & z2 e n
Detach, 950, 946
953 x e n
Split, 952
954 y e n
Split, 952
955 z2 e n
Split, 952
956 x e n
=> ALL(b):[b e n
=> ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]
U Spec, 918
957 ALL(b):[b e n
=> ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,b,c1) e pow & (x,b,c2) e pow => c1=c2]]]
Detach, 956, 938
958 y e n
=> ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
U Spec, 957
959 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Detach, 958, 939
960 ALL(c2):[z1 e n & c2 e n => [(x,y,z1) e pow & (x,y,c2) e pow => z1=c2]]
U Spec, 959
961 z1 e n & z2 e n => [(x,y,z1) e pow & (x,y,z2) e pow => z1=z2]
U Spec, 960
962 z1 e n & z2 e n
Join, 940, 955
963 (x,y,z1) e pow & (x,y,z2) e pow => z1=z2
Detach, 961, 962
964 z1=z2
Detach, 963, 919
Functionality of pow, Part 3
965 ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]
4 Conclusion, 919
966 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]
& ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]
Join, 520, 616
967 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]
& ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]
& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]
Join, 966, 965
pow is a function!
******************
968 ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]
Detach, 502, 967
Prove: ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
Suppose...
969 x e n & y e n
Premise
970 x e n
Split, 969
971 y e n
Split, 969
972 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]
U Spec, 616
973 x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 972
974 EXIST(c):[c e n & (x,y,c) e pow]
Detach, 973, 969
975 z e n & (x,y,z) e pow
E Spec, 974
976 z e n
Split, 975
977 (x,y,z) e pow
Split, 975
978 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 968
979 ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]
U Spec, 978
980 z=pow(x,y) <=> (x,y,z) e pow
U Spec, 979
981 [z=pow(x,y) => (x,y,z) e pow]
& [(x,y,z) e pow => z=pow(x,y)]
Iff-And, 980
982 z=pow(x,y) => (x,y,z) e pow
Split, 981
983 (x,y,z) e pow => z=pow(x,y)
Split, 981
984 z=pow(x,y)
Detach, 983, 977
985 pow(x,y) e n
Substitute, 984, 976
As Required:
986 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
4 Conclusion, 969
Prove: pow(0,0)=x0
987 ALL(c2):ALL(d):[d=pow(0,c2) <=> (0,c2,d) e pow]
U Spec, 968
988 ALL(d):[d=pow(0,0) <=> (0,0,d) e pow]
U Spec, 987
989 x0=pow(0,0) <=> (0,0,x0) e pow
U Spec, 988
990 [x0=pow(0,0) => (0,0,x0) e pow]
& [(0,0,x0) e pow => x0=pow(0,0)]
Iff-And, 989
991 x0=pow(0,0) => (0,0,x0) e pow
Split, 990
992 (0,0,x0) e pow => x0=pow(0,0)
Split, 990
993 x0=pow(0,0)
Detach, 992, 57
As Required:
994 pow(0,0)=x0
Sym, 993
Prove: ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
Suppose...
995 x e n
Premise
996 x e n => [~x=0 => (x,0,1) e pow]
U Spec, 87
997 ~x=0 => (x,0,1) e pow
Detach, 996, 995
Prove: ~x=0 => pow(x,0)=1
Suppose...
998 ~x=0
Premise
999 (x,0,1) e pow
Detach, 997, 998
1000 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 968
1001 ALL(d):[d=pow(x,0) <=> (x,0,d) e pow]
U Spec, 1000
1002 1=pow(x,0) <=> (x,0,1) e pow
U Spec, 1001
1003 [1=pow(x,0) => (x,0,1) e pow]
& [(x,0,1) e pow => 1=pow(x,0)]
Iff-And, 1002
1004 1=pow(x,0) => (x,0,1) e pow
Split, 1003
1005 (x,0,1) e pow => 1=pow(x,0)
Split, 1003
1006 1=pow(x,0)
Detach, 1005, 999
1007 pow(x,0)=1
Sym, 1006
As Required:
1008 ~x=0 => pow(x,0)=1
4 Conclusion, 998
As Required:
1009 ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
4 Conclusion, 995
Prove: ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
Suppose...
1010 x e n & y e n
Premise
1011 x e n
Split, 1010
1012 y e n
Split, 1010
1013 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]
U Spec, 616
1014 x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 1013
1015 EXIST(c):[c e n & (x,y,c) e pow]
Detach, 1014, 1010
1016 z1 e n & (x,y,z1) e pow
E Spec, 1015
1017 z1 e n
Split, 1016
1018 (x,y,z1) e pow
Split, 1016
1019 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 968
1020 ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]
U Spec, 1019
1021 z1=pow(x,y) <=> (x,y,z1) e pow
U Spec, 1020
1022 [z1=pow(x,y) => (x,y,z1) e pow]
& [(x,y,z1) e pow => z1=pow(x,y)]
Iff-And, 1021
1023 z1=pow(x,y) => (x,y,z1) e pow
Split, 1022
1024 (x,y,z1) e pow => z1=pow(x,y)
Split, 1022
1025 z1=pow(x,y)
Detach, 1024, 1018
1026 ALL(b):ALL(c):[x e n & b e n & c e n
=> [(x,b,c) e pow => (x,b+1,c*x) e pow]]
U Spec, 140
1027 ALL(c):[x e n & y e n & c e n
=> [(x,y,c) e pow => (x,y+1,c*x) e pow]]
U Spec, 1026
1028 x e n & y e n & z1 e n
=> [(x,y,z1) e pow => (x,y+1,z1*x) e pow]
U Spec, 1027
1029 x e n & y e n & z1 e n
Join, 1010, 1017
1030 (x,y,z1) e pow => (x,y+1,z1*x) e pow
Detach, 1028, 1029
1031 (x,y+1,z1*x) e pow
Detach, 1030, 1018
1032 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 968
1033 ALL(d):[d=pow(x,y+1) <=> (x,y+1,d) e pow]
U Spec, 1032
1034 z1*x=pow(x,y+1) <=> (x,y+1,z1*x) e pow
U Spec, 1033
1035 [z1*x=pow(x,y+1) => (x,y+1,z1*x) e pow]
& [(x,y+1,z1*x) e pow => z1*x=pow(x,y+1)]
Iff-And, 1034
1036 z1*x=pow(x,y+1) => (x,y+1,z1*x) e pow
Split, 1035
1037 (x,y+1,z1*x) e pow => z1*x=pow(x,y+1)
Split, 1035
1038 z1*x=pow(x,y+1)
Detach, 1037, 1031
1039 pow(x,y+1)=z1*x
Sym, 1038
1040 pow(x,y+1)=pow(x,y)*x
Substitute, 1025, 1039
As Required:
1041 ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
4 Conclusion, 1010
Prove: ALL(a):[aen => pow(a,2)=a*a]
Suppose...
1042 x e n
Premise
Two cases:
1043 x=0 | ~x=0
Or Not
1044 ALL(b):[0 e n & b e n => pow(0,b+1)=pow(0,b)*0]
U Spec, 1041
1045 0 e n & 0 e n => pow(0,0+1)=pow(0,0)*0
U Spec, 1044
1046 0 e n & 0 e n
Join, 4, 4
1047 pow(0,0+1)=pow(0,0)*0
Detach, 1045, 1046
1048 1 e n => 1+0=1
U Spec, 8
1049 1+0=1
Detach, 1048, 5
1050 ALL(b):[0 e n & b e n => 0+b=b+0]
U Spec, 11
1051 0 e n & 1 e n => 0+1=1+0
U Spec, 1050
1052 0 e n & 1 e n
Join, 4, 5
1053 0+1=1+0
Detach, 1051, 1052
1054 0+1=1
Substitute, 1053, 1049
1055 pow(0,1)=pow(0,0)*0
Substitute, 1054, 1047
1056 pow(0,1)=x0*0
Substitute, 994, 1055
1057 x0 e n => x0*0=0
U Spec, 9
1058 x0*0=0
Detach, 1057, 32
Case One
Prove: x=0 => pow(x,2)=x*x
Suppose...
1059 x=0
Premise
1060 pow(0,1)=0
Substitute, 1058, 1056
1061 ALL(b):[0 e n & b e n => pow(0,b+1)=pow(0,b)*0]
U Spec, 1041
1062 0 e n & 1 e n => pow(0,1+1)=pow(0,1)*0
U Spec, 1061
1063 0 e n & 1 e n
Join, 4, 5
1064 pow(0,1+1)=pow(0,1)*0
Detach, 1062, 1063
1065 pow(0,2)=pow(0,1)*0
Substitute, 7, 1064
1066 pow(0,2)=0*0
Substitute, 1060, 1065
1067 pow(x,2)=x*x
Substitute, 1059, 1066
As Required:
1068 x=0 => pow(x,2)=x*x
4 Conclusion, 1059
Case Two
Prove: ~x=0 => pow(x,2)=x*x
Suppose...
1069 ~x=0
Premise
1070 x e n => [~x=0 => pow(x,0)=1]
U Spec, 1009
1071 ~x=0 => pow(x,0)=1
Detach, 1070, 1042
1072 pow(x,0)=1
Detach, 1071, 1069
1073 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 1041
1074 x e n & 0 e n => pow(x,0+1)=pow(x,0)*x
U Spec, 1073
1075 x e n & 0 e n
Join, 1042, 4
1076 pow(x,0+1)=pow(x,0)*x
Detach, 1074, 1075
1077 1 e n => 1+0=1
U Spec, 8
1078 1+0=1
Detach, 1077, 5
1079 ALL(b):[0 e n & b e n => 0+b=b+0]
U Spec, 11
1080 0 e n & 1 e n => 0+1=1+0
U Spec, 1079
1081 0 e n & 1 e n
Join, 4, 5
1082 0+1=1+0
Detach, 1080, 1081
1083 0+1=1
Substitute, 1082, 1078
1084 pow(x,1)=pow(x,0)*x
Substitute, 1083, 1076
1085 pow(x,1)=1*x
Substitute, 1072, 1084
1086 x e n => x*1=x
U Spec, 10
1087 x*1=x
Detach, 1086, 1042
1088 ALL(b):[1 e n & b e n => 1*b=b*1]
U Spec, 12
1089 1 e n & x e n => 1*x=x*1
U Spec, 1088
1090 1 e n & x e n
Join, 5, 1042
1091 1*x=x*1
Detach, 1089, 1090
1092 1*x=x
Substitute, 1091, 1087
1093 pow(x,1)=x
Substitute, 1092, 1085
1094 ALL(b):[x e n & b e n => pow(x,b+1)=pow(x,b)*x]
U Spec, 1041
1095 x e n & 1 e n => pow(x,1+1)=pow(x,1)*x
U Spec, 1094
1096 x e n & 1 e n
Join, 1042, 5
1097 pow(x,1+1)=pow(x,1)*x
Detach, 1095, 1096
1098 pow(x,2)=pow(x,1)*x
Substitute, 7, 1097
1099 pow(x,2)=x*x
Substitute, 1093, 1098
As Required:
1100 ~x=0 => pow(x,2)=x*x
4 Conclusion, 1069
1101 [x=0 => pow(x,2)=x*x] & [~x=0 => pow(x,2)=x*x]
Join, 1068, 1100
1102 pow(x,2)=x*x
Cases, 1043, 1101
As Required:
1103 ALL(a):[a e n => pow(a,2)=a*a]
4 Conclusion, 1042
1104 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=x0
Join, 986, 994
1105 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]
Join, 1104, 1103
1106 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]
Join, 1105, 1041
As Required:
1107 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]]]
4 Conclusion, 32