THEOREM
*******
Given the set of natural numbers n and a binary function * that is closed on set s, there exists a binary function pow
such that, for all x e s, we have:
pow(x,1) = x
pow(x,2) = x*x
pow(x,3) = x*x*x
and so on.
This formal proof was written and machine-verified with the aid of the author's DC Proof 2.0 available at http://www.dcproof.com
REQUIRED PROPERTIES OF N
************************
1 Set(n)
Axiom
2 1 e n
Axiom
Required properties of + on n
3 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
4 ALL(a):[a e n => ~a+1=1]
Axiom
5 ALL(a):ALL(b):ALL(c):[a e n & b e n & c e n => [a+b=c+b => a=c]]
Axiom
Induction property
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n] => [1 e a & ALL(b):[b e a => b+1 e a] => ALL(b):[b e n => b e a]]]
Axiom
Prove: ALL(s):[Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
=> EXIST(pow):[ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]]]
Let * be a binary function that is closed on set s
7 Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
Premise
8 Set(s)
Split, 7
9 ALL(a):ALL(b):[a e s & b e s => a*b e s]
Split, 7
Construct Cartesian product of s, n and s
Apply Cartesian Product axiom
10 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
11 ALL(a2):ALL(a3):[Set(s) & Set(a2) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e s & c2 e a2 & c3 e a3]]]
U Spec, 10
12 ALL(a3):[Set(s) & Set(n) & Set(a3) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e s & c2 e n & c3 e a3]]]
U Spec, 11
13 Set(s) & Set(n) & Set(s) => EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e s & c2 e n & c3 e s]]
U Spec, 12
14 Set(s) & Set(n)
Join, 8, 1
15 Set(s) & Set(n) & Set(s)
Join, 14, 8
16 EXIST(b):[Set''(b) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e b <=> c1 e s & c2 e n & c3 e s]]
Detach, 13, 15
17 Set''(sns) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e sns <=> c1 e s & c2 e n & c3 e s]
E Spec, 16
Define: sns
The Cartesian product of s, n and s
18 Set''(sns)
Split, 17
19 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e sns <=> c1 e s & c2 e n & c3 e s]
Split, 17
Construct the set pow
Apply Subset Axiom
20 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (a,b,c) e d]]]
Subset, 18
21 Set''(pow) & ALL(a):ALL(b):ALL(c):[(a,b,c) e pow
<=> (a,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (a,b,c) e d]]
E Spec, 20
Define: pow
22 Set''(pow)
Split, 21
23 ALL(a):ALL(b):ALL(c):[(a,b,c) e pow
<=> (a,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (a,b,c) e d]]
Split, 21
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e pow => a e s & b e n & c e s]
Suppose...
24 (x,y,z) e pow
Premise
Apply definition of pow
25 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,b,c) e d]]
U Spec, 23
26 ALL(c):[(x,y,c) e pow
<=> (x,y,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,c) e d]]
U Spec, 25
27 (x,y,z) e pow
<=> (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]
U Spec, 26
28 [(x,y,z) e pow => (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]]
& [(x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d] => (x,y,z) e pow]
Iff-And, 27
29 (x,y,z) e pow => (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]
Split, 28
30 (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d] => (x,y,z) e pow
Split, 28
31 (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]
Detach, 29, 24
32 (x,y,z) e sns
Split, 31
33 ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]
Split, 31
Apply definition of sns
34 ALL(c2):ALL(c3):[(x,c2,c3) e sns <=> x e s & c2 e n & c3 e s]
U Spec, 19
35 ALL(c3):[(x,y,c3) e sns <=> x e s & y e n & c3 e s]
U Spec, 34
36 (x,y,z) e sns <=> x e s & y e n & z e s
U Spec, 35
37 [(x,y,z) e sns => x e s & y e n & z e s]
& [x e s & y e n & z e s => (x,y,z) e sns]
Iff-And, 36
38 (x,y,z) e sns => x e s & y e n & z e s
Split, 37
39 x e s & y e n & z e s => (x,y,z) e sns
Split, 37
40 x e s & y e n & z e s
Detach, 38, 32
As Required:
41 ALL(a):ALL(b):ALL(c):[(a,b,c) e pow => a e s & b e n & c e s]
4 Conclusion, 24
Define: ALL(a):[a e s => (a,1,a) e pow]
Suppose...
42 x e s
Premise
Apply definition of pow
43 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,b,c) e d]]
U Spec, 23
44 ALL(c):[(x,1,c) e pow
<=> (x,1,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,c) e d]]
U Spec, 43
45 (x,1,x) e pow
<=> (x,1,x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,x) e d]
U Spec, 44
46 [(x,1,x) e pow => (x,1,x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,x) e d]]
& [(x,1,x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,x) e d] => (x,1,x) e pow]
Iff-And, 45
47 (x,1,x) e pow => (x,1,x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,x) e d]
Split, 46
Sufficient: For (x,1,x) e pow
48 (x,1,x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,x) e d] => (x,1,x) e pow
Split, 46
Prove: (x,1,x) e sns
Apply definition of sns
49 ALL(c2):ALL(c3):[(x,c2,c3) e sns <=> x e s & c2 e n & c3 e s]
U Spec, 19
50 ALL(c3):[(x,1,c3) e sns <=> x e s & 1 e n & c3 e s]
U Spec, 49
51 (x,1,x) e sns <=> x e s & 1 e n & x e s
U Spec, 50
52 [(x,1,x) e sns => x e s & 1 e n & x e s]
& [x e s & 1 e n & x e s => (x,1,x) e sns]
Iff-And, 51
53 (x,1,x) e sns => x e s & 1 e n & x e s
Split, 52
54 x e s & 1 e n & x e s => (x,1,x) e sns
Split, 52
55 x e s & 1 e n
Join, 42, 2
56 x e s & 1 e n & x e s
Join, 55, 42
As Required:
57 (x,1,x) e sns
Detach, 54, 56
Prove: ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,x) e d]
Suppose...
58 Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
Premise
59 Set''(d)
Split, 58
60 ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
Split, 58
61 ALL(i):[i e s => (i,1,i) e d]
Split, 58
62 ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
Split, 58
63 x e s => (x,1,x) e d
U Spec, 61
64 (x,1,x) e d
Detach, 63, 42
As Required:
65 ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,x) e d]
4 Conclusion, 58
Joining results...
66 (x,1,x) e sns
& ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,x) e d]
Join, 57, 65
67 (x,1,x) e pow
Detach, 48, 66
As Required:
68 ALL(a):[a e s => (a,1,a) e pow]
4 Conclusion, 42
Prove: ALL(a):ALL(b):ALL(c):[(a,b,c) e pow => (a,b+1,c*a) e pow]
Suppose...
69 (x,y,z) e pow
Premise
Apply definition of pow
70 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,b,c) e d]]
U Spec, 23
71 ALL(c):[(x,y,c) e pow
<=> (x,y,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,c) e d]]
U Spec, 70
72 (x,y,z) e pow
<=> (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]
U Spec, 71
73 [(x,y,z) e pow => (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]]
& [(x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d] => (x,y,z) e pow]
Iff-And, 72
74 (x,y,z) e pow => (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]
Split, 73
75 (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d] => (x,y,z) e pow
Split, 73
76 (x,y,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]
Detach, 74, 69
77 (x,y,z) e sns
Split, 76
78 ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d]
Split, 76
Prove: x e s & y e n & z e s
Apply definition of sns
79 ALL(b):ALL(c):[(x,b,c) e pow => x e s & b e n & c e s]
U Spec, 41
80 ALL(c):[(x,y,c) e pow => x e s & y e n & c e s]
U Spec, 79
81 (x,y,z) e pow => x e s & y e n & z e s
U Spec, 80
As Required:
82 x e s & y e n & z e s
Detach, 81, 69
83 x e s
Split, 82
84 y e n
Split, 82
85 z e s
Split, 82
Prove: (x,y+1,z*x) e pow
Apply definition of pow
86 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,b,c) e d]]
U Spec, 23
87 ALL(c):[(x,y+1,c) e pow
<=> (x,y+1,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,c) e d]]
U Spec, 86
88 (x,y+1,z*x) e pow
<=> (x,y+1,z*x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z*x) e d]
U Spec, 87
89 [(x,y+1,z*x) e pow => (x,y+1,z*x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z*x) e d]]
& [(x,y+1,z*x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z*x) e d] => (x,y+1,z*x) e pow]
Iff-And, 88
90 (x,y+1,z*x) e pow => (x,y+1,z*x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z*x) e d]
Split, 89
Sufficient: For (x,y+1,z*x) e pow
91 (x,y+1,z*x) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z*x) e d] => (x,y+1,z*x) e pow
Split, 89
Prove: (x,y+1,z*x) e sns
Apply definition of sns
92 ALL(c2):ALL(c3):[(x,c2,c3) e sns <=> x e s & c2 e n & c3 e s]
U Spec, 19
93 ALL(c3):[(x,y+1,c3) e sns <=> x e s & y+1 e n & c3 e s]
U Spec, 92
94 (x,y+1,z*x) e sns <=> x e s & y+1 e n & z*x e s
U Spec, 93
95 [(x,y+1,z*x) e sns => x e s & y+1 e n & z*x e s]
& [x e s & y+1 e n & z*x e s => (x,y+1,z*x) e sns]
Iff-And, 94
96 (x,y+1,z*x) e sns => x e s & y+1 e n & z*x e s
Split, 95
Sufficient: For (x,y+1,z*x) e sns
97 x e s & y+1 e n & z*x e s => (x,y+1,z*x) e sns
Split, 95
Prove: y+1 e n
Apply definition of +
98 ALL(b):[y e n & b e n => y+b e n]
U Spec, 3
99 y e n & 1 e n => y+1 e n
U Spec, 98
100 y e n & 1 e n
Join, 84, 2
As Required:
101 y+1 e n
Detach, 99, 100
Prove: z*x e s
Apply definition of *
102 ALL(b):[z e s & b e s => z*b e s]
U Spec, 9
103 z e s & x e s => z*x e s
U Spec, 102
104 z e s & x e s
Join, 85, 83
As Required:
105 z*x e s
Detach, 103, 104
106 x e s & y+1 e n
Join, 83, 101
107 x e s & y+1 e n & z*x e s
Join, 106, 105
As Required:
108 (x,y+1,z*x) e sns
Detach, 97, 107
Prove: ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z*x) e d]
Suppose...
109 Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
Premise
110 Set''(d)
Split, 109
111 ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
Split, 109
112 ALL(i):[i e s => (i,1,i) e d]
Split, 109
113 ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
Split, 109
114 ALL(j):ALL(k):[(x,j,k) e d => (x,j+1,k*x) e d]
U Spec, 113
115 ALL(k):[(x,y,k) e d => (x,y+1,k*x) e d]
U Spec, 114
116 (x,y,z) e d => (x,y+1,z*x) e d
U Spec, 115
117 Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y,z) e d
U Spec, 78
118 (x,y,z) e d
Detach, 117, 109
119 (x,y+1,z*x) e d
Detach, 116, 118
As Required:
120 ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z*x) e d]
4 Conclusion, 109
121 (x,y+1,z*x) e sns
& ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z*x) e d]
Join, 108, 120
As Required:
122 (x,y+1,z*x) e pow
Detach, 91, 121
As Required:
123 ALL(a):ALL(b):ALL(c):[(a,b,c) e pow => (a,b+1,c*a) e pow]
4 Conclusion, 69
Prove: ~EXIST(a):EXIST(c):[(a,1,c) e pow & ~c=a]
Suppose to the contrary...
124 (x,1,z) e pow & ~z=x
Premise
125 (x,1,z) e pow
Split, 124
126 ~z=x
Split, 124
Apply definition of pow
127 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,b,c) e d]]
U Spec, 23
128 ALL(c):[(x,1,c) e pow
<=> (x,1,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,c) e d]]
U Spec, 127
129 (x,1,z) e pow
<=> (x,1,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d]
U Spec, 128
130 [(x,1,z) e pow => (x,1,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d]]
& [(x,1,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d] => (x,1,z) e pow]
Iff-And, 129
131 (x,1,z) e pow => (x,1,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d]
Split, 130
132 (x,1,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d] => (x,1,z) e pow
Split, 130
133 ~[(x,1,z) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d]] => ~(x,1,z) e pow
Contra, 131
134 ~~[~(x,1,z) e sns | ~ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d]] => ~(x,1,z) e pow
DeMorgan, 133
135 ~(x,1,z) e sns | ~ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d] => ~(x,1,z) e pow
Rem DNeg, 134
136 ~(x,1,z) e sns | ~~EXIST(d):~[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d] => ~(x,1,z) e pow
Quant, 135
137 ~(x,1,z) e sns | EXIST(d):~[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,1,z) e d] => ~(x,1,z) e pow
Rem DNeg, 136
138 ~(x,1,z) e sns | EXIST(d):~~[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d] & ~(x,1,z) e d] => ~(x,1,z) e pow
Imply-And, 137
Sufficient: For ~(x,1,z) e pow (to obtain a contradiction)
Let d = q1 as defined below
139 ~(x,1,z) e sns | EXIST(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d] & ~(x,1,z) e d] => ~(x,1,z) e pow
Rem DNeg, 138
Construct q1
Apply Subset Axiom
140 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e pow & ~[a=x & b=1 & c=z]]]
Subset, 22
141 Set''(q1) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q1
<=> (a,b,c) e pow & ~[a=x & b=1 & c=z]]
E Spec, 140
Define: q1
142 Set''(q1)
Split, 141
143 ALL(a):ALL(b):ALL(c):[(a,b,c) e q1
<=> (a,b,c) e pow & ~[a=x & b=1 & c=z]]
Split, 141
Prove: ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]
Suppose...
144 (t,u,v) e q1
Premise
Apply definition of q1
145 ALL(b):ALL(c):[(t,b,c) e q1
<=> (t,b,c) e pow & ~[t=x & b=1 & c=z]]
U Spec, 143
146 ALL(c):[(t,u,c) e q1
<=> (t,u,c) e pow & ~[t=x & u=1 & c=z]]
U Spec, 145
147 (t,u,v) e q1
<=> (t,u,v) e pow & ~[t=x & u=1 & v=z]
U Spec, 146
148 [(t,u,v) e q1 => (t,u,v) e pow & ~[t=x & u=1 & v=z]]
& [(t,u,v) e pow & ~[t=x & u=1 & v=z] => (t,u,v) e q1]
Iff-And, 147
149 (t,u,v) e q1 => (t,u,v) e pow & ~[t=x & u=1 & v=z]
Split, 148
150 (t,u,v) e pow & ~[t=x & u=1 & v=z] => (t,u,v) e q1
Split, 148
151 (t,u,v) e pow & ~[t=x & u=1 & v=z]
Detach, 149, 144
152 (t,u,v) e pow
Split, 151
153 ~[t=x & u=1 & v=z]
Split, 151
Apply definition of pow
154 ALL(b):ALL(c):[(t,b,c) e pow => t e s & b e n & c e s]
U Spec, 41
155 ALL(c):[(t,u,c) e pow => t e s & u e n & c e s]
U Spec, 154
156 (t,u,v) e pow => t e s & u e n & v e s
U Spec, 155
157 t e s & u e n & v e s
Detach, 156, 152
As Required:
158 ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]
4 Conclusion, 144
Prove: ALL(i):[i e s => (i,1,i) e q1]
Suppose...
159 t e s
Premise
Apply definition of q1
160 ALL(b):ALL(c):[(t,b,c) e q1
<=> (t,b,c) e pow & ~[t=x & b=1 & c=z]]
U Spec, 143
161 ALL(c):[(t,1,c) e q1
<=> (t,1,c) e pow & ~[t=x & 1=1 & c=z]]
U Spec, 160
162 (t,1,t) e q1
<=> (t,1,t) e pow & ~[t=x & 1=1 & t=z]
U Spec, 161
163 [(t,1,t) e q1 => (t,1,t) e pow & ~[t=x & 1=1 & t=z]]
& [(t,1,t) e pow & ~[t=x & 1=1 & t=z] => (t,1,t) e q1]
Iff-And, 162
164 (t,1,t) e q1 => (t,1,t) e pow & ~[t=x & 1=1 & t=z]
Split, 163
Sufficient: For (t,1,t) e q1
165 (t,1,t) e pow & ~[t=x & 1=1 & t=z] => (t,1,t) e q1
Split, 163
Apply previous result
166 t e s => (t,1,t) e pow
U Spec, 68
167 (t,1,t) e pow
Detach, 166, 159
Prove: ~[t=x & 1=1 & t=z]
Suppose to the contrary...
168 t=x & 1=1 & t=z
Premise
169 t=x
Split, 168
170 1=1
Split, 168
171 t=z
Split, 168
172 z=x
Substitute, 171, 169
Join results to obtain a contradiction
173 z=x & ~z=x
Join, 172, 126
As Required:
174 ~[t=x & 1=1 & t=z]
4 Conclusion, 168
175 (t,1,t) e pow & ~[t=x & 1=1 & t=z]
Join, 167, 174
176 (t,1,t) e q1
Detach, 165, 175
As Required:
177 ALL(i):[i e s => (i,1,i) e q1]
4 Conclusion, 159
Prove: ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => (i,j+1,k*i) e q1]
Suppose...
178 (t,u,v) e q1
Premise
Apply definition of q1
179 ALL(b):ALL(c):[(t,b,c) e q1
<=> (t,b,c) e pow & ~[t=x & b=1 & c=z]]
U Spec, 143
180 ALL(c):[(t,u,c) e q1
<=> (t,u,c) e pow & ~[t=x & u=1 & c=z]]
U Spec, 179
181 (t,u,v) e q1
<=> (t,u,v) e pow & ~[t=x & u=1 & v=z]
U Spec, 180
182 [(t,u,v) e q1 => (t,u,v) e pow & ~[t=x & u=1 & v=z]]
& [(t,u,v) e pow & ~[t=x & u=1 & v=z] => (t,u,v) e q1]
Iff-And, 181
183 (t,u,v) e q1 => (t,u,v) e pow & ~[t=x & u=1 & v=z]
Split, 182
184 (t,u,v) e pow & ~[t=x & u=1 & v=z] => (t,u,v) e q1
Split, 182
185 (t,u,v) e pow & ~[t=x & u=1 & v=z]
Detach, 183, 178
186 (t,u,v) e pow
Split, 185
187 ~[t=x & u=1 & v=z]
Split, 185
Apply definition of q1
188 ALL(b):ALL(c):[(t,b,c) e q1
<=> (t,b,c) e pow & ~[t=x & b=1 & c=z]]
U Spec, 143
189 ALL(c):[(t,u+1,c) e q1
<=> (t,u+1,c) e pow & ~[t=x & u+1=1 & c=z]]
U Spec, 188
190 (t,u+1,v*t) e q1
<=> (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z]
U Spec, 189
191 [(t,u+1,v*t) e q1 => (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z]]
& [(t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z] => (t,u+1,v*t) e q1]
Iff-And, 190
192 (t,u+1,v*t) e q1 => (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z]
Split, 191
Sufficient: For (t,u+1,v*t) e q1
193 (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z] => (t,u+1,v*t) e q1
Split, 191
Apply previous result
194 ALL(b):ALL(c):[(t,b,c) e pow => (t,b+1,c*t) e pow]
U Spec, 123
195 ALL(c):[(t,u,c) e pow => (t,u+1,c*t) e pow]
U Spec, 194
196 (t,u,v) e pow => (t,u+1,v*t) e pow
U Spec, 195
197 (t,u+1,v*t) e pow
Detach, 196, 186
Prove: ~[t=x & u+1=1 & v*t=z]
Suppose to the contrary...
198 t=x & u+1=1 & v*t=z
Premise
199 t=x
Split, 198
200 u+1=1
Split, 198
201 v*t=z
Split, 198
Apply property of +
202 u e n => ~u+1=1
U Spec, 4
Apply previous result
203 ALL(b):ALL(c):[(t,b,c) e pow => t e s & b e n & c e s]
U Spec, 41
204 ALL(c):[(t,u,c) e pow => t e s & u e n & c e s]
U Spec, 203
205 (t,u,v) e pow => t e s & u e n & v e s
U Spec, 204
206 t e s & u e n & v e s
Detach, 205, 186
207 t e s
Split, 206
208 u e n
Split, 206
209 v e s
Split, 206
210 ~u+1=1
Detach, 202, 208
Join results to obtain contradiction
211 u+1=1 & ~u+1=1
Join, 200, 210
As Required:
212 ~[t=x & u+1=1 & v*t=z]
4 Conclusion, 198
213 (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z]
Join, 197, 212
214 (t,u+1,v*t) e pow & ~[t=x & u+1=1 & v*t=z]
Join, 197, 212
215 (t,u+1,v*t) e q1
Detach, 193, 214
As Required:
216 ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => (i,j+1,k*i) e q1]
4 Conclusion, 178
Prove: ~(x,1,z) e q1
Apply definition of q1
217 ALL(b):ALL(c):[(x,b,c) e q1
<=> (x,b,c) e pow & ~[x=x & b=1 & c=z]]
U Spec, 143
218 ALL(c):[(x,1,c) e q1
<=> (x,1,c) e pow & ~[x=x & 1=1 & c=z]]
U Spec, 217
219 (x,1,z) e q1
<=> (x,1,z) e pow & ~[x=x & 1=1 & z=z]
U Spec, 218
220 [(x,1,z) e q1 => (x,1,z) e pow & ~[x=x & 1=1 & z=z]]
& [(x,1,z) e pow & ~[x=x & 1=1 & z=z] => (x,1,z) e q1]
Iff-And, 219
221 (x,1,z) e q1 => (x,1,z) e pow & ~[x=x & 1=1 & z=z]
Split, 220
222 (x,1,z) e pow & ~[x=x & 1=1 & z=z] => (x,1,z) e q1
Split, 220
223 ~[(x,1,z) e pow & ~[x=x & 1=1 & z=z]] => ~(x,1,z) e q1
Contra, 221
224 ~~[~(x,1,z) e pow | ~~[x=x & 1=1 & z=z]] => ~(x,1,z) e q1
DeMorgan, 223
225 ~(x,1,z) e pow | ~~[x=x & 1=1 & z=z] => ~(x,1,z) e q1
Rem DNeg, 224
226 ~(x,1,z) e pow | x=x & 1=1 & z=z => ~(x,1,z) e q1
Rem DNeg, 225
227 x=x
Reflex
228 1=1
Reflex
229 z=z
Reflex
230 x=x & 1=1
Join, 227, 228
231 x=x & 1=1 & z=z
Join, 230, 229
232 ~(x,1,z) e pow | x=x & 1=1 & z=z
Arb Or, 231
As Required:
233 ~(x,1,z) e q1
Detach, 226, 232
Join results
234 Set''(q1)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]
Join, 142, 158
235 Set''(q1)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e q1]
Join, 234, 177
236 Set''(q1)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e q1]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => (i,j+1,k*i) e q1]
Join, 235, 216
237 Set''(q1)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e q1]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q1 => (i,j+1,k*i) e q1]
& ~(x,1,z) e q1
Join, 236, 233
Generalizing...
238 EXIST(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
& ~(x,1,z) e d]
E Gen, 237
239 ~(x,1,z) e sns | EXIST(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
& ~(x,1,z) e d]
Arb Or, 238
240 ~(x,1,z) e pow
Detach, 139, 239
Join to obtain contradiction
241 (x,1,z) e pow & ~(x,1,z) e pow
Join, 125, 240
As Required:
242 ~EXIST(a):EXIST(c):[(a,1,c) e pow & ~c=a]
4 Conclusion, 124
Prove: ALL(a):ALL(c):[(a,1,c) e pow => c=a]
Change quantifiers, etc.
243 ~~ALL(a):~EXIST(c):[(a,1,c) e pow & ~c=a]
Quant, 242
244 ALL(a):~EXIST(c):[(a,1,c) e pow & ~c=a]
Rem DNeg, 243
245 ALL(a):~~ALL(c):~[(a,1,c) e pow & ~c=a]
Quant, 244
246 ALL(a):ALL(c):~[(a,1,c) e pow & ~c=a]
Rem DNeg, 245
247 ALL(a):ALL(c):~~[(a,1,c) e pow => ~~c=a]
Imply-And, 246
248 ALL(a):ALL(c):[(a,1,c) e pow => ~~c=a]
Rem DNeg, 247
As Required:
249 ALL(a):ALL(c):[(a,1,c) e pow => c=a]
Rem DNeg, 248
Prove: pow is a function
Apply Function Axiom
250 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
251 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, 250
252 ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e s & c2 e a2 & d e b]
& ALL(c1):ALL(c2):[c1 e s & 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, 251
253 ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e s & c2 e n & d e b]
& ALL(c1):ALL(c2):[c1 e s & 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, 252
Sufficient: For functionality of pow
254 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e s & c2 e n & d e s]
& ALL(c1):ALL(c2):[c1 e s & c2 e n => EXIST(d):[d e s & (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, 253
Prove: ALL(a):[a e s => ALL(b):[b e n => EXIST(c):[c e s & (a,b,c) e pow]]]
Suppose...
255 x e s
Premise
Prove by Induction: ALL(b):[b e n => EXIST(c):[c e s & (x,b,c) e pow]]
First, apply Subset Axiom to get a subset p1 of n
256 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e s & (x,b,c) e pow]]]
Subset, 1
257 Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e s & (x,b,c) e pow]]
E Spec, 256
Define: p1
258 Set(p1)
Split, 257
259 ALL(b):[b e p1 <=> b e n & EXIST(c):[c e s & (x,b,c) e pow]]
Split, 257
Apply principle of induction
260 Set(p1) & ALL(b):[b e p1 => b e n] => [1 e p1 & ALL(b):[b e p1 => b+1 e p1] => ALL(b):[b e n => b e p1]]
U Spec, 6
Prove: p1 is a subset of n
Suppose...
261 t e p1
Premise
Apply definition of p1
262 t e p1 <=> t e n & EXIST(c):[c e s & (x,t,c) e pow]
U Spec, 259
263 [t e p1 => t e n & EXIST(c):[c e s & (x,t,c) e pow]]
& [t e n & EXIST(c):[c e s & (x,t,c) e pow] => t e p1]
Iff-And, 262
264 t e p1 => t e n & EXIST(c):[c e s & (x,t,c) e pow]
Split, 263
265 t e n & EXIST(c):[c e s & (x,t,c) e pow] => t e p1
Split, 263
266 t e n & EXIST(c):[c e s & (x,t,c) e pow]
Detach, 264, 261
267 t e n
Split, 266
As Required:
268 ALL(b):[b e p1 => b e n]
4 Conclusion, 261
Joining results...
269 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 258, 268
Sufficient: For ALL(b):[b e n => b e p1]
270 1 e p1 & ALL(b):[b e p1 => b+1 e p1] => ALL(b):[b e n => b e p1]
Detach, 260, 269
Base case
*********
Prove: 1 e p1
Apply definition of p1
271 1 e p1 <=> 1 e n & EXIST(c):[c e s & (x,1,c) e pow]
U Spec, 259
272 [1 e p1 => 1 e n & EXIST(c):[c e s & (x,1,c) e pow]]
& [1 e n & EXIST(c):[c e s & (x,1,c) e pow] => 1 e p1]
Iff-And, 271
273 1 e p1 => 1 e n & EXIST(c):[c e s & (x,1,c) e pow]
Split, 272
Sufficient: For 1 e p1
274 1 e n & EXIST(c):[c e s & (x,1,c) e pow] => 1 e p1
Split, 272
Apply previous result
275 x e s => (x,1,x) e pow
U Spec, 68
276 (x,1,x) e pow
Detach, 275, 255
277 x e s & (x,1,x) e pow
Join, 255, 276
278 EXIST(c):[c e s & (x,1,c) e pow]
E Gen, 277
279 1 e n & EXIST(c):[c e s & (x,1,c) e pow]
Join, 2, 278
As Required:
280 1 e p1
Detach, 274, 279
Inductive Step
**************
Prove: ALL(b):[b e p1 => b+1 e p1]
Suppose...
281 y e p1
Premise
Apply definition of p1
282 y e p1 <=> y e n & EXIST(c):[c e s & (x,y,c) e pow]
U Spec, 259
283 [y e p1 => y e n & EXIST(c):[c e s & (x,y,c) e pow]]
& [y e n & EXIST(c):[c e s & (x,y,c) e pow] => y e p1]
Iff-And, 282
284 y e p1 => y e n & EXIST(c):[c e s & (x,y,c) e pow]
Split, 283
285 y e n & EXIST(c):[c e s & (x,y,c) e pow] => y e p1
Split, 283
286 y e n & EXIST(c):[c e s & (x,y,c) e pow]
Detach, 284, 281
287 y e n
Split, 286
288 EXIST(c):[c e s & (x,y,c) e pow]
Split, 286
289 z e s & (x,y,z) e pow
E Spec, 288
Define: z
290 z e s
Split, 289
291 (x,y,z) e pow
Split, 289
Apply definition of p1
292 y+1 e p1 <=> y+1 e n & EXIST(c):[c e s & (x,y+1,c) e pow]
U Spec, 259
293 [y+1 e p1 => y+1 e n & EXIST(c):[c e s & (x,y+1,c) e pow]]
& [y+1 e n & EXIST(c):[c e s & (x,y+1,c) e pow] => y+1 e p1]
Iff-And, 292
294 y+1 e p1 => y+1 e n & EXIST(c):[c e s & (x,y+1,c) e pow]
Split, 293
Sufficient: For y+1 e p1
Let c = z*x
295 y+1 e n & EXIST(c):[c e s & (x,y+1,c) e pow] => y+1 e p1
Split, 293
Prove: y+1 e n
Apply definition of + on n
296 ALL(b):[y e n & b e n => y+b e n]
U Spec, 3
297 y e n & 1 e n => y+1 e n
U Spec, 296
298 y e n & 1 e n
Join, 287, 2
As Required:
299 y+1 e n
Detach, 297, 298
Prove: (x,y+1,z*x) e pow
Apply previous result
300 ALL(b):ALL(c):[(x,b,c) e pow => (x,b+1,c*x) e pow]
U Spec, 123
301 ALL(c):[(x,y,c) e pow => (x,y+1,c*x) e pow]
U Spec, 300
302 (x,y,z) e pow => (x,y+1,z*x) e pow
U Spec, 301
As Required:
303 (x,y+1,z*x) e pow
Detach, 302, 291
Prove: z*x e s
Apply definition of * on s
304 ALL(b):[z e s & b e s => z*b e s]
U Spec, 9
305 z e s & x e s => z*x e s
U Spec, 304
306 z e s & x e s
Join, 290, 255
As Required:
307 z*x e s
Detach, 305, 306
Joining results...
308 z*x e s & (x,y+1,z*x) e pow
Join, 307, 303
Generalizing...
309 EXIST(c):[c e s & (x,y+1,c) e pow]
E Gen, 308
310 y+1 e n & EXIST(c):[c e s & (x,y+1,c) e pow]
Join, 299, 309
As Required:
311 y+1 e p1
Detach, 295, 310
As Required:
312 ALL(b):[b e p1 => b+1 e p1]
4 Conclusion, 281
Joining results...
313 1 e p1 & ALL(b):[b e p1 => b+1 e p1]
Join, 280, 312
As Required:
314 ALL(b):[b e n => b e p1]
Detach, 270, 313
Prove: ALL(b):[b e n => EXIST(c):[c e s & (x,b,c) e pow]]
Suppose...
315 y e n
Premise
Apply previous result
316 y e n => y e p1
U Spec, 314
317 y e p1
Detach, 316, 315
Apply definition of p1
318 y e p1 <=> y e n & EXIST(c):[c e s & (x,y,c) e pow]
U Spec, 259
319 [y e p1 => y e n & EXIST(c):[c e s & (x,y,c) e pow]]
& [y e n & EXIST(c):[c e s & (x,y,c) e pow] => y e p1]
Iff-And, 318
320 y e p1 => y e n & EXIST(c):[c e s & (x,y,c) e pow]
Split, 319
321 y e n & EXIST(c):[c e s & (x,y,c) e pow] => y e p1
Split, 319
322 y e n & EXIST(c):[c e s & (x,y,c) e pow]
Detach, 320, 317
323 y e n
Split, 322
324 EXIST(c):[c e s & (x,y,c) e pow]
Split, 322
As Required:
325 ALL(b):[b e n => EXIST(c):[c e s & (x,b,c) e pow]]
4 Conclusion, 315
As Required:
326 ALL(a):[a e s
=> ALL(b):[b e n => EXIST(c):[c e s & (a,b,c) e pow]]]
4 Conclusion, 255
Prove: ALL(a):ALL(b):[a e s & b e n => EXIST(c):[c e s & (a,b,c) e pow]]
Suppose...
327 x e s & y e n
Premise
328 x e s
Split, 327
329 y e n
Split, 327
Apply previous result
330 x e s
=> ALL(b):[b e n => EXIST(c):[c e s & (x,b,c) e pow]]
U Spec, 326
331 ALL(b):[b e n => EXIST(c):[c e s & (x,b,c) e pow]]
Detach, 330, 328
332 y e n => EXIST(c):[c e s & (x,y,c) e pow]
U Spec, 331
333 EXIST(c):[c e s & (x,y,c) e pow]
Detach, 332, 329
Functionality, Part 2
334 ALL(a):ALL(b):[a e s & b e n => EXIST(c):[c e s & (a,b,c) e pow]]
4 Conclusion, 327
Prove: ALL(a):[a e s => ALL(b):[b e n
=> ALL(d1):ALL(d2):[(a,b,d1) e pow & (a,b,d2) e pow => d1=d2]]]
Suppose...
335 x e s
Premise
Prove by Induction:
ALL(b):[b e n => ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,bd2) e pow => d1=d2]]
Construct subset p2 of n
Apply Subset Axiom
336 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]]
Subset, 1
337 Set(p2) & ALL(b):[b e p2 <=> b e n & ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]
E Spec, 336
Define: p2
338 Set(p2)
Split, 337
339 ALL(b):[b e p2 <=> b e n & ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]
Split, 337
Apply Induction Principle
340 Set(p2) & ALL(b):[b e p2 => b e n] => [1 e p2 & ALL(b):[b e p2 => b+1 e p2] => ALL(b):[b e n => b e p2]]
U Spec, 6
Prove: p2 is a subset of n
Suppose...
341 t e p2
Premise
Apply definition of p2
342 t e p2 <=> t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2]
U Spec, 339
343 [t e p2 => t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2]]
& [t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2] => t e p2]
Iff-And, 342
344 t e p2 => t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2]
Split, 343
345 t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2] => t e p2
Split, 343
346 t e n & ALL(d1):ALL(d2):[(x,t,d1) e pow & (x,t,d2) e pow => d1=d2]
Detach, 344, 341
347 t e n
Split, 346
As Required:
348 ALL(b):[b e p2 => b e n]
4 Conclusion, 341
Joining results...
349 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 338, 348
Sufficient: For ALL(b):[b e n => b e p2]
350 1 e p2 & ALL(b):[b e p2 => b+1 e p2] => ALL(b):[b e n => b e p2]
Detach, 340, 349
Base Case
*********
Prove: 1 e p2
Apply definition of p2
351 1 e p2 <=> 1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]
U Spec, 339
352 [1 e p2 => 1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]]
& [1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2] => 1 e p2]
Iff-And, 351
353 1 e p2 => 1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]
Split, 352
Sufficient: For 1 e p2
354 1 e n & ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2] => 1 e p2
Split, 352
Prove: ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]
Suppose...
355 (x,1,z1) e pow & (x,1,z2) e pow
Premise
356 (x,1,z1) e pow
Split, 355
357 (x,1,z2) e pow
Split, 355
Apply previous result
358 ALL(c):[(x,1,c) e pow => c=x]
U Spec, 249
359 (x,1,z1) e pow => z1=x
U Spec, 358
360 z1=x
Detach, 359, 356
Apply previous result
361 ALL(c):[(x,1,c) e pow => c=x]
U Spec, 249
362 (x,1,z2) e pow => z2=x
U Spec, 361
363 z2=x
Detach, 362, 357
364 z1=z2
Substitute, 363, 360
As Required:
365 ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]
4 Conclusion, 355
Joining results...
366 1 e n
& ALL(d1):ALL(d2):[(x,1,d1) e pow & (x,1,d2) e pow => d1=d2]
Join, 2, 365
As Required:
367 1 e p2
Detach, 354, 366
Inductive Step
**************
Prove: ALL(b):[b e p2 => b+1 e p2]
Suppose...
368 y e p2
Premise
Apply definition of p2
369 y e p2 <=> y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
U Spec, 339
370 [y e p2 => y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]]
& [y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2] => y e p2]
Iff-And, 369
371 y e p2 => y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
Split, 370
372 y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2] => y e p2
Split, 370
373 y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
Detach, 371, 368
374 y e n
Split, 373
375 ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
Split, 373
Apply definition of p2
376 y+1 e p2 <=> y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]
U Spec, 339
377 [y+1 e p2 => y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]]
& [y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2] => y+1 e p2]
Iff-And, 376
378 y+1 e p2 => y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]
Split, 377
Sufficient: For y+1 e p2
379 y+1 e n & ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2] => y+1 e p2
Split, 377
Prove: y+1 e n
Apply definition of + on n
380 ALL(b):[y e n & b e n => y+b e n]
U Spec, 3
381 y e n & 1 e n => y+1 e n
U Spec, 380
382 y e n & 1 e n
Join, 374, 2
As Required:
383 y+1 e n
Detach, 381, 382
Apply previous result
384 ALL(b):[x e s & b e n => EXIST(c):[c e s & (x,b,c) e pow]]
U Spec, 334
385 x e s & y e n => EXIST(c):[c e s & (x,y,c) e pow]
U Spec, 384
386 x e s & y e n
Join, 335, 374
387 EXIST(c):[c e s & (x,y,c) e pow]
Detach, 385, 386
388 z e s & (x,y,z) e pow
E Spec, 387
Define: z
389 z e s
Split, 388
390 (x,y,z) e pow
Split, 388
Apply previous result
391 ALL(d2):[(x,y,z) e pow & (x,y,d2) e pow => z=d2]
U Spec, 375
Prove: ALL(c):[c e s => [(x,y,c) e pow => c=z]]
Suppose...
392 z' e s
Premise
Apply previous result
393 (x,y,z) e pow & (x,y,z') e pow => z=z'
U Spec, 391
Prove: (x,y,z') e pow => z'=z
Suppose...
394 (x,y,z') e pow
Premise
395 (x,y,z) e pow & (x,y,z') e pow
Join, 390, 394
396 z=z'
Detach, 393, 395
397 z'=z
Sym, 396
As Required:
398 (x,y,z') e pow => z'=z
4 Conclusion, 394
As Required:
399 ALL(c):[c e s => [(x,y,c) e pow => c=z]]
4 Conclusion, 392
Prove: ~EXIST(c):[(x,y+1,c) e pow & ~c=z*x]
Suppose to the contrary...
400 (x,y+1,z') e pow & ~z'=z*x
Premise
401 (x,y+1,z') e pow
Split, 400
402 ~z'=z*x
Split, 400
Apply definition of pow
403 ALL(b):ALL(c):[(x,b,c) e pow
<=> (x,b,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,b,c) e d]]
U Spec, 23
404 ALL(c):[(x,y+1,c) e pow
<=> (x,y+1,c) e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,c) e d]]
U Spec, 403
405 (x,y+1,z') e pow
<=> (x,y+1,z') e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d]
U Spec, 404
406 [(x,y+1,z') e pow => (x,y+1,z') e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d]]
& [(x,y+1,z') e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d] => (x,y+1,z') e pow]
Iff-And, 405
407 (x,y+1,z') e pow => (x,y+1,z') e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d]
Split, 406
408 (x,y+1,z') e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d] => (x,y+1,z') e pow
Split, 406
409 ~[(x,y+1,z') e sns & ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d]] => ~(x,y+1,z') e pow
Contra, 407
410 ~~[~(x,y+1,z') e sns | ~ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d]] => ~(x,y+1,z') e pow
DeMorgan, 409
411 ~(x,y+1,z') e sns | ~ALL(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d] => ~(x,y+1,z') e pow
Rem DNeg, 410
412 ~(x,y+1,z') e sns | ~~EXIST(d):~[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d] => ~(x,y+1,z') e pow
Quant, 411
413 ~(x,y+1,z') e sns | EXIST(d):~[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
=> (x,y+1,z') e d] => ~(x,y+1,z') e pow
Rem DNeg, 412
414 ~(x,y+1,z') e sns | EXIST(d):~~[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e pow
Imply-And, 413
Sufficient: For ~(x,y+1,z') e pow (to obtain contradiction)
Use d = q2 as defined below
415 ~(x,y+1,z') e sns | EXIST(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d] & ~(x,y+1,z') e d] => ~(x,y+1,z') e pow
Rem DNeg, 414
Construct q2
Apply Subset Axiom
416 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, 22
417 Set''(q2) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q2
<=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]
E Spec, 416
Define: q2
418 Set''(q2)
Split, 417
419 ALL(a):ALL(b):ALL(c):[(a,b,c) e q2
<=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]
Split, 417
Prove: ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => i e s & j e n & k e s]
Suppose...
420 (t,u,v) e q2
Premise
Apply definition of q2
421 ALL(b):ALL(c):[(t,b,c) e q2
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 419
422 ALL(c):[(t,u,c) e q2
<=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]
U Spec, 421
423 (t,u,v) e q2
<=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
U Spec, 422
424 [(t,u,v) e q2 => (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 q2]
Iff-And, 423
425 (t,u,v) e q2 => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Split, 424
426 (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q2
Split, 424
427 (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Detach, 425, 420
428 (t,u,v) e pow
Split, 427
429 ~[t=x & u=y+1 & v=z']
Split, 427
Apply previous result
430 ALL(b):ALL(c):[(t,b,c) e pow => t e s & b e n & c e s]
U Spec, 41
431 ALL(c):[(t,u,c) e pow => t e s & u e n & c e s]
U Spec, 430
432 (t,u,v) e pow => t e s & u e n & v e s
U Spec, 431
433 t e s & u e n & v e s
Detach, 432, 428
As Required:
434 ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => i e s & j e n & k e s]
4 Conclusion, 420
Prove: ALL(i):[i e s => (i,1,i) e q2]
Suppose...
435 t e s
Premise
Apply definition of p2
436 ALL(b):ALL(c):[(t,b,c) e q2
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 419
437 ALL(c):[(t,1,c) e q2
<=> (t,1,c) e pow & ~[t=x & 1=y+1 & c=z']]
U Spec, 436
438 (t,1,t) e q2
<=> (t,1,t) e pow & ~[t=x & 1=y+1 & t=z']
U Spec, 437
439 [(t,1,t) e q2 => (t,1,t) e pow & ~[t=x & 1=y+1 & t=z']]
& [(t,1,t) e pow & ~[t=x & 1=y+1 & t=z'] => (t,1,t) e q2]
Iff-And, 438
440 (t,1,t) e q2 => (t,1,t) e pow & ~[t=x & 1=y+1 & t=z']
Split, 439
Sufficient: For (t,1,t) e q2
441 (t,1,t) e pow & ~[t=x & 1=y+1 & t=z'] => (t,1,t) e q2
Split, 439
Apply previous result
442 t e s => (t,1,t) e pow
U Spec, 68
443 (t,1,t) e pow
Detach, 442, 435
Prove: ~[t=x & 1=y+1 & t=z']
Suppose to the contrary...
444 t=x & 1=y+1 & t=z'
Premise
445 t=x
Split, 444
446 1=y+1
Split, 444
447 t=z'
Split, 444
Apply property of + on n
448 y e n => ~y+1=1
U Spec, 4
449 ~y+1=1
Detach, 448, 374
450 y+1=1
Sym, 446
Joining results to obtain contradiction
451 y+1=1 & ~y+1=1
Join, 450, 449
As Required:
452 ~[t=x & 1=y+1 & t=z']
4 Conclusion, 444
Joining results...
453 (t,1,t) e pow & ~[t=x & 1=y+1 & t=z']
Join, 443, 452
As Required:
454 (t,1,t) e q2
Detach, 441, 453
As Required:
455 ALL(i):[i e s => (i,1,i) e q2]
4 Conclusion, 435
Prove: ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => (i,j+1,k*i) e q2]
Suppose...
456 (t,u,v) e q2
Premise
Apply definition of q2
457 ALL(b):ALL(c):[(t,b,c) e q2
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 419
458 ALL(c):[(t,u,c) e q2
<=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]
U Spec, 457
459 (t,u,v) e q2
<=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
U Spec, 458
460 [(t,u,v) e q2 => (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 q2]
Iff-And, 459
461 (t,u,v) e q2 => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Split, 460
462 (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q2
Split, 460
463 (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Detach, 461, 456
464 (t,u,v) e pow
Split, 463
465 ~[t=x & u=y+1 & v=z']
Split, 463
Apply definition of q2
466 ALL(b):ALL(c):[(t,b,c) e q2
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 419
467 ALL(c):[(t,u+1,c) e q2
<=> (t,u+1,c) e pow & ~[t=x & u+1=y+1 & c=z']]
U Spec, 466
468 (t,u+1,v*t) e q2
<=> (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']
U Spec, 467
469 [(t,u+1,v*t) e q2 => (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 q2]
Iff-And, 468
470 (t,u+1,v*t) e q2 => (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']
Split, 469
471 (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q2
Split, 469
Apply definition of pow
472 ALL(b):ALL(c):[(t,b,c) e pow => (t,b+1,c*t) e pow]
U Spec, 123
473 ALL(c):[(t,u,c) e pow => (t,u+1,c*t) e pow]
U Spec, 472
474 (t,u,v) e pow => (t,u+1,v*t) e pow
U Spec, 473
475 (t,u+1,v*t) e pow
Detach, 474, 464
Prove: ~[t=x & u+1=y+1 & v*t=z']
Suppose to the contrary...
476 t=x & u+1=y+1 & v*t=z'
Premise
477 t=x
Split, 476
478 u+1=y+1
Split, 476
479 v*t=z'
Split, 476
Apply property of + on n
480 ALL(b):ALL(c):[u e n & b e n & c e n => [u+b=c+b => u=c]]
U Spec, 5
481 ALL(c):[u e n & 1 e n & c e n => [u+1=c+1 => u=c]]
U Spec, 480
482 u e n & 1 e n & y e n => [u+1=y+1 => u=y]
U Spec, 481
Apply definition of pow
483 ALL(b):ALL(c):[(t,b,c) e pow => t e s & b e n & c e s]
U Spec, 41
484 ALL(c):[(t,u,c) e pow => t e s & u e n & c e s]
U Spec, 483
485 (t,u,v) e pow => t e s & u e n & v e s
U Spec, 484
486 t e s & u e n & v e s
Detach, 485, 464
487 t e s
Split, 486
488 u e n
Split, 486
489 v e s
Split, 486
490 u e n & 1 e n
Join, 488, 2
491 u e n & 1 e n & y e n
Join, 490, 374
492 u+1=y+1 => u=y
Detach, 482, 491
493 u=y
Detach, 492, 478
494 (x,u,v) e pow
Substitute, 477, 464
495 (x,y,v) e pow
Substitute, 493, 494
Apply previous result
496 v e s => [(x,y,v) e pow => v=z]
U Spec, 399
497 (x,y,v) e pow => v=z
Detach, 496, 489
498 v=z
Detach, 497, 495
499 v*x=z'
Substitute, 477, 479
500 z*x=z'
Substitute, 498, 499
501 z'=z*x
Sym, 500
Joining to obtain contradiction...
502 z'=z*x & ~z'=z*x
Join, 501, 402
As Required:
503 ~[t=x & u+1=y+1 & v*t=z']
4 Conclusion, 476
Joining results...
504 (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']
Join, 475, 503
As Required:
505 (t,u+1,v*t) e q2
Detach, 471, 504
As Required:
506 ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => (i,j+1,k*i) e q2]
4 Conclusion, 456
Apply definition of q2
507 ALL(b):ALL(c):[(x,b,c) e q2
<=> (x,b,c) e pow & ~[x=x & b=y+1 & c=z']]
U Spec, 419
508 ALL(c):[(x,y+1,c) e q2
<=> (x,y+1,c) e pow & ~[x=x & y+1=y+1 & c=z']]
U Spec, 507
509 (x,y+1,z') e q2
<=> (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']
U Spec, 508
510 [(x,y+1,z') e q2 => (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 q2]
Iff-And, 509
511 (x,y+1,z') e q2 => (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']
Split, 510
512 (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q2
Split, 510
513 ~[(x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q2
Contra, 511
514 ~~[~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q2
DeMorgan, 513
515 ~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z'] => ~(x,y+1,z') e q2
Rem DNeg, 514
Sufficient: For ~(x,y+1,z') e q2
516 ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z' => ~(x,y+1,z') e q2
Rem DNeg, 515
517 x=x
Reflex
518 y+1=y+1
Reflex
519 z'=z'
Reflex
520 x=x & y+1=y+1
Join, 517, 518
521 x=x & y+1=y+1 & z'=z'
Join, 520, 519
522 ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z'
Arb Or, 521
As Required:
523 ~(x,y+1,z') e q2
Detach, 516, 522
Joining results...
524 Set''(q2)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => i e s & j e n & k e s]
Join, 418, 434
525 Set''(q2)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e q2]
Join, 524, 455
526 Set''(q2)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e q2]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => (i,j+1,k*i) e q2]
Join, 525, 506
527 Set''(q2)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e q2]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e q2 => (i,j+1,k*i) e q2]
& ~(x,y+1,z') e q2
Join, 526, 523
Generalizing...
528 EXIST(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
& ~(x,y+1,z') e d]
E Gen, 527
529 ~(x,y+1,z') e sns | EXIST(d):[Set''(d)
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => i e s & j e n & k e s]
& ALL(i):[i e s => (i,1,i) e d]
& ALL(i):ALL(j):ALL(k):[(i,j,k) e d => (i,j+1,k*i) e d]
& ~(x,y+1,z') e d]
Arb Or, 528
530 ~(x,y+1,z') e pow
Detach, 415, 529
Joining to obtain a contradiction...
531 (x,y+1,z') e pow & ~(x,y+1,z') e pow
Join, 401, 530
As Required:
532 ~EXIST(c):[(x,y+1,c) e pow & ~c=z*x]
4 Conclusion, 400
533 ~~ALL(c):~[(x,y+1,c) e pow & ~c=z*x]
Quant, 532
534 ALL(c):~[(x,y+1,c) e pow & ~c=z*x]
Rem DNeg, 533
535 ALL(c):~~[(x,y+1,c) e pow => ~~c=z*x]
Imply-And, 534
536 ALL(c):[(x,y+1,c) e pow => ~~c=z*x]
Rem DNeg, 535
As Required:
537 ALL(c):[(x,y+1,c) e pow => c=z*x]
Rem DNeg, 536
Prove: ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]
Suppose...
538 (x,y+1,z1) e pow & (x,y+1,z2) e pow
Premise
539 (x,y+1,z1) e pow
Split, 538
540 (x,y+1,z2) e pow
Split, 538
Apply previous result
541 (x,y+1,z1) e pow => z1=z*x
U Spec, 537
542 z1=z*x
Detach, 541, 539
Apply previous result
543 (x,y+1,z2) e pow => z2=z*x
U Spec, 537
544 z2=z*x
Detach, 543, 540
545 z1=z2
Substitute, 544, 542
As Required:
546 ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]
4 Conclusion, 538
Joining results...
547 y+1 e n
& ALL(d1):ALL(d2):[(x,y+1,d1) e pow & (x,y+1,d2) e pow => d1=d2]
Join, 383, 546
548 y+1 e p2
Detach, 379, 547
As Required:
549 ALL(b):[b e p2 => b+1 e p2]
4 Conclusion, 368
Joining results...
550 1 e p2 & ALL(b):[b e p2 => b+1 e p2]
Join, 367, 549
As Required:
551 ALL(b):[b e n => b e p2]
Detach, 350, 550
Prove: ALL(b):[b e n
=> ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]
Suppose...
552 y e n
Premise
Apply previous result
553 y e n => y e p2
U Spec, 551
554 y e p2
Detach, 553, 552
Apply definition of p2
555 y e p2 <=> y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
U Spec, 339
556 [y e p2 => y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]]
& [y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2] => y e p2]
Iff-And, 555
557 y e p2 => y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
Split, 556
558 y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2] => y e p2
Split, 556
559 y e n & ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
Detach, 557, 554
560 y e n
Split, 559
561 ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
Split, 559
As Required:
562 ALL(b):[b e n
=> ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]
4 Conclusion, 552
As Required:
563 ALL(a):[a e s
=> ALL(b):[b e n
=> ALL(d1):ALL(d2):[(a,b,d1) e pow & (a,b,d2) e pow => d1=d2]]]
4 Conclusion, 335
Prove: ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]
Suppose...
564 (x,y,z1) e pow & (x,y,z2) e pow
Premise
565 (x,y,z1) e pow
Split, 564
566 (x,y,z2) e pow
Split, 564
Apply previous result
567 ALL(b):ALL(c):[(x,b,c) e pow => x e s & b e n & c e s]
U Spec, 41
568 ALL(c):[(x,y,c) e pow => x e s & y e n & c e s]
U Spec, 567
569 (x,y,z1) e pow => x e s & y e n & z1 e s
U Spec, 568
570 x e s & y e n & z1 e s
Detach, 569, 565
571 x e s
Split, 570
572 y e n
Split, 570
573 z1 e s
Split, 570
Apply previous result
574 x e s
=> ALL(b):[b e n
=> ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]
U Spec, 563
575 ALL(b):[b e n
=> ALL(d1):ALL(d2):[(x,b,d1) e pow & (x,b,d2) e pow => d1=d2]]
Detach, 574, 571
576 y e n
=> ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
U Spec, 575
577 ALL(d1):ALL(d2):[(x,y,d1) e pow & (x,y,d2) e pow => d1=d2]
Detach, 576, 572
578 ALL(d2):[(x,y,z1) e pow & (x,y,d2) e pow => z1=d2]
U Spec, 577
579 (x,y,z1) e pow & (x,y,z2) e pow => z1=z2
U Spec, 578
580 z1=z2
Detach, 579, 564
Functionality, Part 3
581 ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]
4 Conclusion, 564
Joining results...
582 ALL(a):ALL(b):ALL(c):[(a,b,c) e pow => a e s & b e n & c e s]
& ALL(a):ALL(b):[a e s & b e n => EXIST(c):[c e s & (a,b,c) e pow]]
Join, 41, 334
583 ALL(a):ALL(b):ALL(c):[(a,b,c) e pow => a e s & b e n & c e s]
& ALL(a):ALL(b):[a e s & b e n => EXIST(c):[c e s & (a,b,c) e pow]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e pow & (c1,c2,d2) e pow => d1=d2]
Join, 582, 581
pow is a function
584 ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]
Detach, 254, 583
Prove: ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
Suppose...
585 x e s & y e n
Premise
586 x e s
Split, 585
587 y e n
Split, 585
Apply previous result
588 ALL(b):[x e s & b e n => EXIST(c):[c e s & (x,b,c) e pow]]
U Spec, 334
589 x e s & y e n => EXIST(c):[c e s & (x,y,c) e pow]
U Spec, 588
590 EXIST(c):[c e s & (x,y,c) e pow]
Detach, 589, 585
591 z e s & (x,y,z) e pow
E Spec, 590
592 z e s
Split, 591
593 (x,y,z) e pow
Split, 591
Apply functionality of pow
594 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 584
595 ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]
U Spec, 594
596 z=pow(x,y) <=> (x,y,z) e pow
U Spec, 595
597 [z=pow(x,y) => (x,y,z) e pow]
& [(x,y,z) e pow => z=pow(x,y)]
Iff-And, 596
598 z=pow(x,y) => (x,y,z) e pow
Split, 597
599 (x,y,z) e pow => z=pow(x,y)
Split, 597
600 z=pow(x,y)
Detach, 599, 593
601 pow(x,y) e s
Substitute, 600, 592
As Required:
602 ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
4 Conclusion, 585
Prove: ALL(a):[a e s => pow(a,1)=a]
Suppose...
603 x e s
Premise
Apply previous result
604 x e s => (x,1,x) e pow
U Spec, 68
605 (x,1,x) e pow
Detach, 604, 603
Apply functionality of pow
606 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 584
607 ALL(d):[d=pow(x,1) <=> (x,1,d) e pow]
U Spec, 606
608 x=pow(x,1) <=> (x,1,x) e pow
U Spec, 607
609 [x=pow(x,1) => (x,1,x) e pow]
& [(x,1,x) e pow => x=pow(x,1)]
Iff-And, 608
610 x=pow(x,1) => (x,1,x) e pow
Split, 609
611 (x,1,x) e pow => x=pow(x,1)
Split, 609
612 x=pow(x,1)
Detach, 611, 605
613 pow(x,1)=x
Sym, 612
As Required:
614 ALL(a):[a e s => pow(a,1)=a]
4 Conclusion, 603
Prove: ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
Suppose...
615 x e s & y e n
Premise
616 x e s
Split, 615
617 y e n
Split, 615
Apply previous result
618 ALL(b):[x e s & b e n => EXIST(c):[c e s & (x,b,c) e pow]]
U Spec, 334
619 x e s & y e n => EXIST(c):[c e s & (x,y,c) e pow]
U Spec, 618
620 EXIST(c):[c e s & (x,y,c) e pow]
Detach, 619, 615
621 z e s & (x,y,z) e pow
E Spec, 620
622 z e s
Split, 621
623 (x,y,z) e pow
Split, 621
Apply previous result
624 ALL(b):ALL(c):[(x,b,c) e pow => (x,b+1,c*x) e pow]
U Spec, 123
625 ALL(c):[(x,y,c) e pow => (x,y+1,c*x) e pow]
U Spec, 624
626 (x,y,z) e pow => (x,y+1,z*x) e pow
U Spec, 625
627 (x,y+1,z*x) e pow
Detach, 626, 623
Apply functionality of pow
628 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 584
629 ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]
U Spec, 628
630 z=pow(x,y) <=> (x,y,z) e pow
U Spec, 629
631 [z=pow(x,y) => (x,y,z) e pow]
& [(x,y,z) e pow => z=pow(x,y)]
Iff-And, 630
632 z=pow(x,y) => (x,y,z) e pow
Split, 631
633 (x,y,z) e pow => z=pow(x,y)
Split, 631
634 z=pow(x,y)
Detach, 633, 623
635 ALL(d):[d=pow(x,y+1) <=> (x,y+1,d) e pow]
U Spec, 628
636 z*x=pow(x,y+1) <=> (x,y+1,z*x) e pow
U Spec, 635
637 [z*x=pow(x,y+1) => (x,y+1,z*x) e pow]
& [(x,y+1,z*x) e pow => z*x=pow(x,y+1)]
Iff-And, 636
638 z*x=pow(x,y+1) => (x,y+1,z*x) e pow
Split, 637
639 (x,y+1,z*x) e pow => z*x=pow(x,y+1)
Split, 637
640 z*x=pow(x,y+1)
Detach, 639, 627
641 pow(x,y)*x=pow(x,y+1)
Substitute, 634, 640
642 pow(x,y+1)=pow(x,y)*x
Sym, 641
As Required:
643 ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
4 Conclusion, 615
644 ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
Join, 602, 614
645 ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]
Join, 644, 643
As Required:
646 ALL(s):[Set(s)
& ALL(a):ALL(b):[a e s & b e s => a*b e s]
=> EXIST(pow):[ALL(a):ALL(b):[a e s & b e n => pow(a,b) e s]
& ALL(a):[a e s => pow(a,1)=a]
& ALL(a):ALL(b):[a e s & b e n => pow(a,b+1)=pow(a,b)*a]]]
4 Conclusion, 7