THEOREM 1
*********
There exists infinitely many exponent-like functions on the natural numbers. Here we show that, for every
natural number x0, there exists a function pow such that:
pow(0,0) = x0 (0^0 = x0)
pow(a,0) = 1 for ~a=0 (a^1 = 1)
pow(a,b+1) = pow(a,b) * a (a^(b+1) = a^b * a)
Formally, we 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]]]
By Dan Christensen
October 2013
(This proof was written with the aid of the author's DC Proof software available at http://www.dcproof.com )
OUTLINE
*******
Lines 1-8 The basic principles of arithematic assumed here
Lines 9-18 Constructing the set n3 of ordered triples of natural number using the Cartesian Product Axiom
Lines 19-24 Constructing the set pn3, the power set of n3, using the Power Set Axiom
Lines 25-29 Constructing a subset pow of n3 using the Subset Axiom
Line3 30-490 Establishing some useful properties of the pow set
Lines 491-960 Proving that pow is a function
Lines 961-1038 Establishing the required properties of the pow function
BASIC PRINCIPLES OF ARITHMETIC 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
The principle of mathematical induction (starting at 0)
6 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 +
7 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
8 ALL(a):[a e n => ~a+1=0]
Axiom
PROOF
*****
Construct the set of ordered triples of n
Apply Cartesian Product Axiom
9 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
10 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, 9
11 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, 10
12 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, 11
13 Set(n) & Set(n)
Join, 1, 1
14 Set(n) & Set(n) & Set(n)
Join, 13, 1
15 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, 12, 14
16 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 15
Define: n3 (the set of ordered triples of n)
**********
17 Set''(n3)
Split, 16
18 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 16
Construct the powerset of n3
Apply the Power Set Axiom
19 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
20 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, 19
21 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, 20, 17
22 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, 21
Define: pn3 (the power set of n3)
***********
23 Set(pn3)
Split, 22
24 ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]
Split, 22
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...
25 x0 e n
Premise
Construct the set pow, a subset of n3
Apply the Subset Axiom
26 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, 17
27 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, 26
Define: pow
***********
28 Set''(pow)
Split, 27
29 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, 27
Establish some useful properties of pow
Prove: (0,0,x0) e pow
Apply definition of pow
30 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, 29
31 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, 30
32 (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, 31
33 [(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, 32
34 (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, 33
Sufficient: (0,0,x0) e pow
35 (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, 33
Prove: (0,0,x0) e n3
36 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 18
37 ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]
U Spec, 36
38 (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n
U Spec, 37
39 [(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, 38
40 (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n
Split, 39
41 0 e n & 0 e n & x0 e n => (0,0,x0) e n3
Split, 39
42 0 e n & 0 e n
Join, 4, 4
43 0 e n & 0 e n & x0 e n
Join, 42, 25
44 (0,0,x0) e n3
Detach, 41, 43
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...
45 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
46 q e pn3
Split, 45
47 (0,0,x0) e q
Split, 45
48 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, 45
49 (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, 44, 48
As Required:
50 (0,0,x0) e pow
Detach, 35, 49
Prove: ALL(a):[a e n => [~a=0 => (a,0,1) e pow]]
Suppose...
51 x e n
Premise
Prove: ~x=0 => (x,0,1) e pow
Suppose...
52 ~x=0
Premise
Apply definition of pow
53 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, 29
54 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, 53
55 (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, 54
56 [(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, 55
57 (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, 56
Sufficient: (x,0,1) e pow
58 (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, 56
Prove: (x,0,1) e n3
Apply definition of n3
59 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 18
60 ALL(c3):[(x,0,c3) e n3 <=> x e n & 0 e n & c3 e n]
U Spec, 59
61 (x,0,1) e n3 <=> x e n & 0 e n & 1 e n
U Spec, 60
62 [(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, 61
63 (x,0,1) e n3 => x e n & 0 e n & 1 e n
Split, 62
64 x e n & 0 e n & 1 e n => (x,0,1) e n3
Split, 62
65 x e n & 0 e n
Join, 51, 4
66 x e n & 0 e n & 1 e n
Join, 65, 5
67 (x,0,1) e n3
Detach, 64, 66
68 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
69 q e pn3
Split, 68
70 (0,0,x0) e q
Split, 68
71 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Split, 68
72 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Split, 68
73 x e n => [~x=0 => (x,0,1) e q]
U Spec, 71
74 ~x=0 => (x,0,1) e q
Detach, 73, 51
75 (x,0,1) e q
Detach, 74, 52
76 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, 68
77 (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, 67, 76
78 (x,0,1) e pow
Detach, 58, 77
As Required:
79 ~x=0 => (x,0,1) e pow
4 Conclusion, 52
As Required:
80 ALL(a):[a e n => [~a=0 => (a,0,1) e pow]]
4 Conclusion, 51
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...
81 x e n & y e n & z e n
Premise
82 x e n
Split, 81
83 y e n
Split, 81
84 z e n
Split, 81
Prove: (x,y,z) e pow => (x,y+1,z*x) e pow
Suppose...
85 (x,y,z) e pow
Premise
Apply definition of pow
86 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, 29
87 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, 86
88 (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, 87
89 [(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, 88
90 (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, 89
91 (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, 89
92 (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, 90, 85
93 (x,y,z) e n3
Split, 92
94 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, 92
Apply definition of pow
95 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, 29
96 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, 95
97 (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, 96
98 [(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, 97
99 (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, 98
Sufficient: (x,y+1,z*x) e pow
100 (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, 98
Prove: (x,y+1,z*x) e n3
Apply definition of n3
101 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 18
102 ALL(c3):[(x,y+1,c3) e n3 <=> x e n & y+1 e n & c3 e n]
U Spec, 101
103 (x,y+1,z*x) e n3 <=> x e n & y+1 e n & z*x e n
U Spec, 102
104 [(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, 103
105 (x,y+1,z*x) e n3 => x e n & y+1 e n & z*x e n
Split, 104
106 x e n & y+1 e n & z*x e n => (x,y+1,z*x) e n3
Split, 104
107 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
108 y e n & 1 e n => y+1 e n
U Spec, 107
109 y e n & 1 e n
Join, 83, 5
110 y+1 e n
Detach, 108, 109
111 ALL(b):[z e n & b e n => z*b e n]
U Spec, 3
112 z e n & x e n => z*x e n
U Spec, 111
113 z e n & x e n
Join, 84, 82
114 z*x e n
Detach, 112, 113
115 x e n & y+1 e n
Join, 82, 110
116 x e n & y+1 e n & z*x e n
Join, 115, 114
117 (x,y+1,z*x) e n3
Detach, 106, 116
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...
118 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
119 q e pn3
Split, 118
120 (0,0,x0) e q
Split, 118
121 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Split, 118
Apply definition of q
122 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Split, 118
123 ALL(f):ALL(g):[(x,f,g) e q => (x,f+1,g*x) e q]
U Spec, 122
124 ALL(g):[(x,y,g) e q => (x,y+1,g*x) e q]
U Spec, 123
125 (x,y,z) e q => (x,y+1,z*x) e q
U Spec, 124
126 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, 94
127 (x,y,z) e q
Detach, 126, 118
128 (x,y+1,z*x) e q
Detach, 125, 127
As Required:
129 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, 118
130 (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, 117, 129
131 (x,y+1,z*x) e pow
Detach, 100, 130
As Required:
132 (x,y,z) e pow => (x,y+1,z*x) e pow
4 Conclusion, 85
As Required:
133 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, 81
Prove: ALL(a):[a e n => [(0,0,a) e pow => a=x0]]
Suppose...
134 z e n
Premise
Prove: ~[(0,0,z) e pow & ~z=x0]
Suppose to contrary...
135 (0,0,z) e pow & ~z=x0
Premise
136 (0,0,z) e pow
Split, 135
137 ~z=x0
Split, 135
Apply definition of pow
138 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, 29
139 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, 138
140 (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, 139
141 [(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, 140
142 (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, 141
143 (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, 141
144 ~[(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, 142
145 ~~[~(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, 144
146 ~(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, 145
147 ~(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, 146
148 ~(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, 147
149 ~(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, 148
Sufficient: ~(0,0,z) e pow (to obtain contradiction)
150 ~(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, 149
151 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, 17
152 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, 151
Define: q
153 Set''(q)
Split, 152
154 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e n3 & ~[a=0 & b=0 & c=z]]
Split, 152
155 q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
U Spec, 24
156 [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, 155
157 q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Split, 156
158 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 156
Prove: ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Suppose...
159 (t,u,v) e q
Premise
Apply definition of q
160 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]
U Spec, 154
161 ALL(c):[(t,u,c) e q
<=> (t,u,c) e n3 & ~[t=0 & u=0 & c=z]]
U Spec, 160
162 (t,u,v) e q
<=> (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
U Spec, 161
163 [(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, 162
164 (t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
Split, 163
165 (t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q
Split, 163
166 (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
Detach, 164, 159
167 (t,u,v) e n3
Split, 166
As Required:
168 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
4 Conclusion, 159
169 Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Join, 153, 168
As Required:
170 q e pn3
Detach, 158, 169
Prove: (0,0,x0) e q
Apply definition of q
171 ALL(b):ALL(c):[(0,b,c) e q
<=> (0,b,c) e n3 & ~[0=0 & b=0 & c=z]]
U Spec, 154
172 ALL(c):[(0,0,c) e q
<=> (0,0,c) e n3 & ~[0=0 & 0=0 & c=z]]
U Spec, 171
173 (0,0,x0) e q
<=> (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]
U Spec, 172
174 [(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, 173
175 (0,0,x0) e q => (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]
Split, 174
176 (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z] => (0,0,x0) e q
Split, 174
177 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 18
178 ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]
U Spec, 177
179 (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n
U Spec, 178
180 [(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, 179
181 (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n
Split, 180
182 0 e n & 0 e n & x0 e n => (0,0,x0) e n3
Split, 180
183 0 e n & 0 e n
Join, 4, 4
184 0 e n & 0 e n & x0 e n
Join, 183, 25
185 (0,0,x0) e n3
Detach, 182, 184
Prove: ~[0=0 & 0=0 & x0=z]
Suppose to the contrary...
186 0=0 & 0=0 & x0=z
Premise
187 0=0
Split, 186
188 0=0
Split, 186
189 x0=z
Split, 186
190 ~x0=z
Sym, 137
191 x0=z & ~x0=z
Join, 189, 190
As Required:
192 ~[0=0 & 0=0 & x0=z]
4 Conclusion, 186
193 (0,0,x0) e n3 & ~[0=0 & 0=0 & x0=z]
Join, 185, 192
As Required:
194 (0,0,x0) e q
Detach, 176, 193
Prove: ~(0,0,z) e q
Apply definition of q
195 ALL(b):ALL(c):[(0,b,c) e q
<=> (0,b,c) e n3 & ~[0=0 & b=0 & c=z]]
U Spec, 154
196 ALL(c):[(0,0,c) e q
<=> (0,0,c) e n3 & ~[0=0 & 0=0 & c=z]]
U Spec, 195
197 (0,0,z) e q
<=> (0,0,z) e n3 & ~[0=0 & 0=0 & z=z]
U Spec, 196
198 [(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, 197
199 (0,0,z) e q => (0,0,z) e n3 & ~[0=0 & 0=0 & z=z]
Split, 198
200 (0,0,z) e n3 & ~[0=0 & 0=0 & z=z] => (0,0,z) e q
Split, 198
201 ~[(0,0,z) e n3 & ~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q
Contra, 199
202 ~~[~(0,0,z) e n3 | ~~[0=0 & 0=0 & z=z]] => ~(0,0,z) e q
DeMorgan, 201
203 ~(0,0,z) e n3 | ~~[0=0 & 0=0 & z=z] => ~(0,0,z) e q
Rem DNeg, 202
204 ~(0,0,z) e n3 | 0=0 & 0=0 & z=z => ~(0,0,z) e q
Rem DNeg, 203
205 0=0
Reflex
206 z=z
Reflex
207 0=0 & 0=0
Join, 205, 205
208 0=0 & 0=0 & z=z
Join, 207, 206
209 ~(0,0,z) e n3 | 0=0 & 0=0 & z=z
Arb Or, 208
As Required:
210 ~(0,0,z) e q
Detach, 204, 209
211 t e n
Premise
Prove: ~t=0 => (t,0,1) e q
Suppose...
212 ~t=0
Premise
Apply definition of q
213 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]
U Spec, 154
214 ALL(c):[(t,0,c) e q
<=> (t,0,c) e n3 & ~[t=0 & 0=0 & c=z]]
U Spec, 213
215 (t,0,1) e q
<=> (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]
U Spec, 214
216 [(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, 215
217 (t,0,1) e q => (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]
Split, 216
Sufficient: (t,0,1) e q
218 (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z] => (t,0,1) e q
Split, 216
219 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 18
220 ALL(c3):[(t,0,c3) e n3 <=> t e n & 0 e n & c3 e n]
U Spec, 219
221 (t,0,1) e n3 <=> t e n & 0 e n & 1 e n
U Spec, 220
222 [(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, 221
223 (t,0,1) e n3 => t e n & 0 e n & 1 e n
Split, 222
224 t e n & 0 e n & 1 e n => (t,0,1) e n3
Split, 222
225 t e n & 0 e n
Join, 211, 4
226 t e n & 0 e n & 1 e n
Join, 225, 5
227 (t,0,1) e n3
Detach, 224, 226
Prove: ~[t=0 & 0=0 & 1=z]
Suppose to the contrary...
228 t=0 & 0=0 & 1=z
Premise
229 t=0
Split, 228
230 0=0
Split, 228
231 1=z
Split, 228
232 t=0 & ~t=0
Join, 229, 212
As Required:
233 ~[t=0 & 0=0 & 1=z]
4 Conclusion, 228
234 (t,0,1) e n3 & ~[t=0 & 0=0 & 1=z]
Join, 227, 233
235 (t,0,1) e q
Detach, 218, 234
As Required:
236 ~t=0 => (t,0,1) e q
4 Conclusion, 212
As Required:
237 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
4 Conclusion, 211
Prove: ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
Suppose...
238 (t,u,v) e q
Premise
239 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]
U Spec, 154
240 ALL(c):[(t,u,c) e q
<=> (t,u,c) e n3 & ~[t=0 & u=0 & c=z]]
U Spec, 239
241 (t,u,v) e q
<=> (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
U Spec, 240
242 [(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, 241
243 (t,u,v) e q => (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
Split, 242
244 (t,u,v) e n3 & ~[t=0 & u=0 & v=z] => (t,u,v) e q
Split, 242
245 (t,u,v) e n3 & ~[t=0 & u=0 & v=z]
Detach, 243, 238
246 (t,u,v) e n3
Split, 245
247 ~[t=0 & u=0 & v=z]
Split, 245
248 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 18
249 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 248
250 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 249
251 [(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, 250
252 (t,u,v) e n3 => t e n & u e n & v e n
Split, 251
253 t e n & u e n & v e n => (t,u,v) e n3
Split, 251
254 t e n & u e n & v e n
Detach, 252, 246
255 t e n
Split, 254
256 u e n
Split, 254
257 v e n
Split, 254
258 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=0 & b=0 & c=z]]
U Spec, 154
259 ALL(c):[(t,u+1,c) e q
<=> (t,u+1,c) e n3 & ~[t=0 & u+1=0 & c=z]]
U Spec, 258
260 (t,u+1,v*t) e q
<=> (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]
U Spec, 259
261 [(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, 260
262 (t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]
Split, 261
263 (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z] => (t,u+1,v*t) e q
Split, 261
264 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 18
265 ALL(c3):[(t,u+1,c3) e n3 <=> t e n & u+1 e n & c3 e n]
U Spec, 264
266 (t,u+1,v*t) e n3 <=> t e n & u+1 e n & v*t e n
U Spec, 265
267 [(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, 266
268 (t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n
Split, 267
269 t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3
Split, 267
270 ALL(b):[u e n & b e n => u+b e n]
U Spec, 2
271 u e n & 1 e n => u+1 e n
U Spec, 270
272 u e n & 1 e n
Join, 256, 5
273 u+1 e n
Detach, 271, 272
274 ALL(b):[v e n & b e n => v*b e n]
U Spec, 3
275 v e n & t e n => v*t e n
U Spec, 274
276 v e n & t e n
Join, 257, 255
277 v*t e n
Detach, 275, 276
278 t e n & u+1 e n
Join, 255, 273
279 t e n & u+1 e n & v*t e n
Join, 278, 277
280 (t,u+1,v*t) e n3
Detach, 269, 279
281 t=0 & u+1=0 & v*t=z
Premise
282 t=0
Split, 281
283 u+1=0
Split, 281
284 v*t=z
Split, 281
285 u e n => ~u+1=0
U Spec, 8
286 ~u+1=0
Detach, 285, 256
287 u+1=0 & ~u+1=0
Join, 283, 286
288 ~[t=0 & u+1=0 & v*t=z]
4 Conclusion, 281
289 (t,u+1,v*t) e n3 & ~[t=0 & u+1=0 & v*t=z]
Join, 280, 288
290 (t,u+1,v*t) e q
Detach, 263, 289
As Required:
291 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
4 Conclusion, 238
292 q e pn3 & (0,0,x0) e q
Join, 170, 194
293 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Join, 292, 237
294 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, 293, 291
295 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, 294, 210
296 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, 295
297 ~(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, 296
298 ~(0,0,z) e pow
Detach, 150, 297
299 (0,0,z) e pow & ~(0,0,z) e pow
Join, 136, 298
As Required:
300 ~[(0,0,z) e pow & ~z=x0]
4 Conclusion, 135
301 ~~[(0,0,z) e pow => ~~z=x0]
Imply-And, 300
302 (0,0,z) e pow => ~~z=x0
Rem DNeg, 301
303 (0,0,z) e pow => z=x0
Rem DNeg, 302
As Required:
304 ALL(a):[a e n => [(0,0,a) e pow => a=x0]]
4 Conclusion, 134
Prove: ALL(a):[a e n
=> [~a=0 => ALL(b):[b e n => [(a,0,b) e pow => b=1]]]]
Suppose...
305 x e n
Premise
Prove: ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]
Suppose...
306 ~x=0
Premise
Prove: ALL(b):[b e n => [(x,0,b) e pow => b=1]]
Suppose...
307 z e n
Premise
Prove: ~[(x,0,z) e pow & ~z=1]
Suppose to the contrary...
308 (x,0,z) e pow & ~z=1
Premise
309 (x,0,z) e pow
Split, 308
310 ~z=1
Split, 308
311 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, 29
312 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, 311
313 (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, 312
314 [(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, 313
315 (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, 314
316 (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, 314
317 (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, 315, 309
318 (x,0,z) e n3
Split, 317
319 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, 317
320 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, 29
321 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, 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]
U Spec, 321
323 [(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, 322
324 (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, 323
325 (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, 323
326 ~[(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, 324
327 ~~[~(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, 326
328 ~(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, 327
329 ~(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, 328
330 ~(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, 329
331 ~(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, 330
Sufficient: ~(x,0,z) e pow (to obtain contradiction)
332 ~(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, 331
333 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, 17
334 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, 333
Define: q
*********
335 Set''(q)
Split, 334
336 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e n3 & ~[a=x & b=0 & c=z]]
Split, 334
337 q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
U Spec, 24
338 [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, 337
339 q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Split, 338
340 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 338
341 (t,u,v) e q
Premise
342 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]
U Spec, 336
343 ALL(c):[(t,u,c) e q
<=> (t,u,c) e n3 & ~[t=x & u=0 & c=z]]
U Spec, 342
344 (t,u,v) e q
<=> (t,u,v) e n3 & ~[t=x & u=0 & v=z]
U Spec, 343
345 [(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, 344
346 (t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]
Split, 345
347 (t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q
Split, 345
348 (t,u,v) e n3 & ~[t=x & u=0 & v=z]
Detach, 346, 341
349 (t,u,v) e n3
Split, 348
350 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
4 Conclusion, 341
351 Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Join, 335, 350
352 q e pn3
Detach, 340, 351
353 ALL(b):ALL(c):[(x,b,c) e q
<=> (x,b,c) e n3 & ~[x=x & b=0 & c=z]]
U Spec, 336
354 ALL(c):[(x,0,c) e q
<=> (x,0,c) e n3 & ~[x=x & 0=0 & c=z]]
U Spec, 353
355 (x,0,z) e q
<=> (x,0,z) e n3 & ~[x=x & 0=0 & z=z]
U Spec, 354
356 [(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, 355
357 (x,0,z) e q => (x,0,z) e n3 & ~[x=x & 0=0 & z=z]
Split, 356
358 (x,0,z) e n3 & ~[x=x & 0=0 & z=z] => (x,0,z) e q
Split, 356
359 ~[(x,0,z) e n3 & ~[x=x & 0=0 & z=z]] => ~(x,0,z) e q
Contra, 357
360 ~~[~(x,0,z) e n3 | ~~[x=x & 0=0 & z=z]] => ~(x,0,z) e q
DeMorgan, 359
361 ~(x,0,z) e n3 | ~~[x=x & 0=0 & z=z] => ~(x,0,z) e q
Rem DNeg, 360
362 ~(x,0,z) e n3 | x=x & 0=0 & z=z => ~(x,0,z) e q
Rem DNeg, 361
363 x=x
Reflex
364 0=0
Reflex
365 z=z
Reflex
366 x=x & 0=0
Join, 363, 364
367 x=x & 0=0 & z=z
Join, 366, 365
368 ~(x,0,z) e n3 | x=x & 0=0 & z=z
Arb Or, 367
As Required:
369 ~(x,0,z) e q
Detach, 362, 368
370 t e n
Premise
371 ~t=0
Premise
372 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]
U Spec, 336
373 ALL(c):[(t,0,c) e q
<=> (t,0,c) e n3 & ~[t=x & 0=0 & c=z]]
U Spec, 372
374 (t,0,1) e q
<=> (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]
U Spec, 373
375 [(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, 374
376 (t,0,1) e q => (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]
Split, 375
Sufficient: (t,0,1) e q
377 (t,0,1) e n3 & ~[t=x & 0=0 & 1=z] => (t,0,1) e q
Split, 375
378 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 18
379 ALL(c3):[(t,0,c3) e n3 <=> t e n & 0 e n & c3 e n]
U Spec, 378
380 (t,0,1) e n3 <=> t e n & 0 e n & 1 e n
U Spec, 379
381 [(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, 380
382 (t,0,1) e n3 => t e n & 0 e n & 1 e n
Split, 381
383 t e n & 0 e n & 1 e n => (t,0,1) e n3
Split, 381
384 t e n & 0 e n
Join, 370, 4
385 t e n & 0 e n & 1 e n
Join, 384, 5
386 (t,0,1) e n3
Detach, 383, 385
387 t=x & 0=0 & 1=z
Premise
388 t=x
Split, 387
389 0=0
Split, 387
390 1=z
Split, 387
391 z=1
Sym, 390
392 z=1 & ~z=1
Join, 391, 310
393 ~[t=x & 0=0 & 1=z]
4 Conclusion, 387
394 (t,0,1) e n3 & ~[t=x & 0=0 & 1=z]
Join, 386, 393
395 (t,0,1) e q
Detach, 377, 394
396 ~t=0 => (t,0,1) e q
4 Conclusion, 371
As Required:
397 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
4 Conclusion, 370
Suppose...
398 (t,u,v) e q
Premise
399 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]
U Spec, 336
400 ALL(c):[(t,u,c) e q
<=> (t,u,c) e n3 & ~[t=x & u=0 & c=z]]
U Spec, 399
401 (t,u,v) e q
<=> (t,u,v) e n3 & ~[t=x & u=0 & v=z]
U Spec, 400
402 [(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, 401
403 (t,u,v) e q => (t,u,v) e n3 & ~[t=x & u=0 & v=z]
Split, 402
404 (t,u,v) e n3 & ~[t=x & u=0 & v=z] => (t,u,v) e q
Split, 402
405 (t,u,v) e n3 & ~[t=x & u=0 & v=z]
Detach, 403, 398
406 (t,u,v) e n3
Split, 405
407 ~[t=x & u=0 & v=z]
Split, 405
408 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 18
409 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 408
410 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 409
411 [(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, 410
412 (t,u,v) e n3 => t e n & u e n & v e n
Split, 411
413 t e n & u e n & v e n => (t,u,v) e n3
Split, 411
414 t e n & u e n & v e n
Detach, 412, 406
415 t e n
Split, 414
416 u e n
Split, 414
417 v e n
Split, 414
418 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e n3 & ~[t=x & b=0 & c=z]]
U Spec, 336
419 ALL(c):[(t,u+1,c) e q
<=> (t,u+1,c) e n3 & ~[t=x & u+1=0 & c=z]]
U Spec, 418
420 (t,u+1,v*t) e q
<=> (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]
U Spec, 419
421 [(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, 420
422 (t,u+1,v*t) e q => (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]
Split, 421
Sufficient: (t,u+1,v*t) e q
423 (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z] => (t,u+1,v*t) e q
Split, 421
424 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 18
425 ALL(c3):[(t,u+1,c3) e n3 <=> t e n & u+1 e n & c3 e n]
U Spec, 424
426 (t,u+1,v*t) e n3 <=> t e n & u+1 e n & v*t e n
U Spec, 425
427 [(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, 426
428 (t,u+1,v*t) e n3 => t e n & u+1 e n & v*t e n
Split, 427
429 t e n & u+1 e n & v*t e n => (t,u+1,v*t) e n3
Split, 427
430 ALL(b):[u e n & b e n => u+b e n]
U Spec, 2
431 u e n & 1 e n => u+1 e n
U Spec, 430
432 u e n & 1 e n
Join, 416, 5
433 u+1 e n
Detach, 431, 432
434 ALL(b):[v e n & b e n => v*b e n]
U Spec, 3
435 v e n & t e n => v*t e n
U Spec, 434
436 v e n & t e n
Join, 417, 415
437 v*t e n
Detach, 435, 436
438 t e n & u+1 e n
Join, 415, 433
439 t e n & u+1 e n & v*t e n
Join, 438, 437
440 (t,u+1,v*t) e n3
Detach, 429, 439
441 t=x & u+1=0 & v*t=z
Premise
442 t=x
Split, 441
443 u+1=0
Split, 441
444 v*t=z
Split, 441
445 u e n => ~u+1=0
U Spec, 8
446 ~u+1=0
Detach, 445, 416
447 u+1=0 & ~u+1=0
Join, 443, 446
448 ~[t=x & u+1=0 & v*t=z]
4 Conclusion, 441
449 (t,u+1,v*t) e n3 & ~[t=x & u+1=0 & v*t=z]
Join, 440, 448
450 (t,u+1,v*t) e q
Detach, 423, 449
As Required:
451 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
4 Conclusion, 398
452 ALL(b):ALL(c):[(0,b,c) e q
<=> (0,b,c) e n3 & ~[0=x & b=0 & c=z]]
U Spec, 336
453 ALL(c):[(0,0,c) e q
<=> (0,0,c) e n3 & ~[0=x & 0=0 & c=z]]
U Spec, 452
454 (0,0,x0) e q
<=> (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]
U Spec, 453
455 [(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, 454
456 (0,0,x0) e q => (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]
Split, 455
457 (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z] => (0,0,x0) e q
Split, 455
458 ALL(c2):ALL(c3):[(0,c2,c3) e n3 <=> 0 e n & c2 e n & c3 e n]
U Spec, 18
459 ALL(c3):[(0,0,c3) e n3 <=> 0 e n & 0 e n & c3 e n]
U Spec, 458
460 (0,0,x0) e n3 <=> 0 e n & 0 e n & x0 e n
U Spec, 459
461 [(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, 460
462 (0,0,x0) e n3 => 0 e n & 0 e n & x0 e n
Split, 461
463 0 e n & 0 e n & x0 e n => (0,0,x0) e n3
Split, 461
464 0 e n & 0 e n
Join, 4, 4
465 0 e n & 0 e n & x0 e n
Join, 464, 25
466 (0,0,x0) e n3
Detach, 463, 465
467 0=x & 0=0 & x0=z
Premise
468 0=x
Split, 467
469 0=0
Split, 467
470 x0=z
Split, 467
471 x=0
Sym, 468
472 x=0 & ~x=0
Join, 471, 306
473 ~[0=x & 0=0 & x0=z]
4 Conclusion, 467
474 (0,0,x0) e n3 & ~[0=x & 0=0 & x0=z]
Join, 466, 473
As Required:
475 (0,0,x0) e q
Detach, 457, 474
476 q e pn3 & (0,0,x0) e q
Join, 352, 475
477 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Join, 476, 397
478 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, 477, 451
479 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, 478, 369
480 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, 479
481 ~(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, 480
482 ~(x,0,z) e pow
Detach, 332, 481
483 (x,0,z) e pow & ~(x,0,z) e pow
Join, 309, 482
As Required:
484 ~[(x,0,z) e pow & ~z=1]
4 Conclusion, 308
485 ~~[(x,0,z) e pow => ~~z=1]
Imply-And, 484
486 (x,0,z) e pow => ~~z=1
Rem DNeg, 485
487 (x,0,z) e pow => z=1
Rem DNeg, 486
As Required:
488 ALL(b):[b e n => [(x,0,b) e pow => b=1]]
4 Conclusion, 307
As Required:
489 ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]
4 Conclusion, 306
As Required:
490 ALL(a):[a e n
=> [~a=0 => ALL(b):[b e n => [(a,0,b) e pow => b=1]]]]
4 Conclusion, 305
Prove: pow is a function
Apply Function Axiom
491 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
492 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, 491
493 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, 492
494 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, 493
Sufficient: For functionality of pow
495 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, 494
Prove: ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]
Suppose...
496 (x,y,z) e pow
Premise
497 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, 29
498 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, 497
499 (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, 498
500 [(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, 499
501 (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, 500
502 (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, 500
503 (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, 501, 496
504 (x,y,z) e n3
Split, 503
505 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, 503
506 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 18
507 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 506
508 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 507
509 [(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, 508
510 (x,y,z) e n3 => x e n & y e n & z e n
Split, 509
511 x e n & y e n & z e n => (x,y,z) e n3
Split, 509
512 x e n & y e n & z e n
Detach, 510, 504
Functionality of pow, Part 1
513 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e pow => c1 e n & c2 e n & d e n]
4 Conclusion, 496
Prove: ALL(a):[a e n
=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e pow]]]
Suppose...
514 x e n
Premise
515 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]]
Subset, 1
516 Set(p1) & ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]
E Spec, 515
Define: p1
**********
517 Set(p1)
Split, 516
518 ALL(b):[b e p1 <=> b e n & EXIST(c):[c e n & (x,b,c) e pow]]
Split, 516
519 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, 6
Prove: ALL(b):[b e p1 => b e n]
Suppose...
520 y e p1
Premise
521 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 518
522 [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, 521
523 y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]
Split, 522
524 y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1
Split, 522
525 y e n & EXIST(c):[c e n & (x,y,c) e pow]
Detach, 523, 520
526 y e n
Split, 525
As Required:
527 ALL(b):[b e p1 => b e n]
4 Conclusion, 520
528 Set(p1) & ALL(b):[b e p1 => b e n]
Join, 517, 527
Sufficient: ALL(b):[b e n => b e p1]
529 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
=> ALL(b):[b e n => b e p1]
Detach, 519, 528
530 0 e p1 <=> 0 e n & EXIST(c):[c e n & (x,0,c) e pow]
U Spec, 518
531 [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, 530
532 0 e p1 => 0 e n & EXIST(c):[c e n & (x,0,c) e pow]
Split, 531
533 0 e n & EXIST(c):[c e n & (x,0,c) e pow] => 0 e p1
Split, 531
2 Cases:
534 x=0 | ~x=0
Or Not
Prove: x=0 => 0 e p1
Suppose...
535 x=0
Premise
536 (x,0,x0) e pow
Substitute, 535, 50
537 x0 e n & (x,0,x0) e pow
Join, 25, 536
538 EXIST(c):[c e n & (x,0,c) e pow]
E Gen, 537
539 0 e n & EXIST(c):[c e n & (x,0,c) e pow]
Join, 4, 538
540 0 e p1
Detach, 533, 539
As Required:
541 x=0 => 0 e p1
4 Conclusion, 535
Prove: ~x=0 => 0 e p1
Suppose...
542 ~x=0
Premise
543 x e n => [~x=0 => (x,0,1) e pow]
U Spec, 80
544 ~x=0 => (x,0,1) e pow
Detach, 543, 514
545 (x,0,1) e pow
Detach, 544, 542
546 1 e n & (x,0,1) e pow
Join, 5, 545
547 EXIST(c):[c e n & (x,0,c) e pow]
E Gen, 546
548 0 e n & EXIST(c):[c e n & (x,0,c) e pow]
Join, 4, 547
549 0 e p1
Detach, 533, 548
As Required:
550 ~x=0 => 0 e p1
4 Conclusion, 542
551 [x=0 => 0 e p1] & [~x=0 => 0 e p1]
Join, 541, 550
As Required:
552 0 e p1
Cases, 534, 551
Prove: ALL(b):[b e p1 => b+1 e p1]
Suppose...
553 y e p1
Premise
554 y e p1 <=> y e n & EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 518
555 [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, 554
556 y e p1 => y e n & EXIST(c):[c e n & (x,y,c) e pow]
Split, 555
557 y e n & EXIST(c):[c e n & (x,y,c) e pow] => y e p1
Split, 555
558 y e n & EXIST(c):[c e n & (x,y,c) e pow]
Detach, 556, 553
559 y e n
Split, 558
560 EXIST(c):[c e n & (x,y,c) e pow]
Split, 558
561 z e n & (x,y,z) e pow
E Spec, 560
562 z e n
Split, 561
563 (x,y,z) e pow
Split, 561
564 y+1 e p1 <=> y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]
U Spec, 518
565 [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, 564
566 y+1 e p1 => y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]
Split, 565
Sufficient: y+1 e p1
567 y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow] => y+1 e p1
Split, 565
568 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
569 y e n & 1 e n => y+1 e n
U Spec, 568
570 y e n & 1 e n
Join, 559, 5
571 y+1 e n
Detach, 569, 570
572 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, 133
573 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, 572
574 x e n & y e n & z e n
=> [(x,y,z) e pow => (x,y+1,z*x) e pow]
U Spec, 573
575 x e n & y e n
Join, 514, 559
576 x e n & y e n & z e n
Join, 575, 562
577 (x,y,z) e pow => (x,y+1,z*x) e pow
Detach, 574, 576
578 (x,y+1,z*x) e pow
Detach, 577, 563
579 ALL(b):[z e n & b e n => z*b e n]
U Spec, 3
580 z e n & x e n => z*x e n
U Spec, 579
581 z e n & x e n
Join, 562, 514
582 z*x e n
Detach, 580, 581
583 z*x e n & (x,y+1,z*x) e pow
Join, 582, 578
584 EXIST(c):[c e n & (x,y+1,c) e pow]
E Gen, 583
585 y+1 e n & EXIST(c):[c e n & (x,y+1,c) e pow]
Join, 571, 584
586 y+1 e p1
Detach, 567, 585
As Required:
587 ALL(b):[b e p1 => b+1 e p1]
4 Conclusion, 553
588 0 e p1 & ALL(b):[b e p1 => b+1 e p1]
Join, 552, 587
589 ALL(b):[b e n => b e p1]
Detach, 529, 588
Prove: ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]
Suppose...
590 t e n
Premise
591 t e n => t e p1
U Spec, 589
592 t e p1
Detach, 591, 590
593 t e p1 <=> t e n & EXIST(c):[c e n & (x,t,c) e pow]
U Spec, 518
594 [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, 593
595 t e p1 => t e n & EXIST(c):[c e n & (x,t,c) e pow]
Split, 594
596 t e n & EXIST(c):[c e n & (x,t,c) e pow] => t e p1
Split, 594
597 t e n & EXIST(c):[c e n & (x,t,c) e pow]
Detach, 595, 592
598 t e n
Split, 597
599 EXIST(c):[c e n & (x,t,c) e pow]
Split, 597
As Required:
600 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]
4 Conclusion, 590
As Required:
601 ALL(a):[a e n
=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e pow]]]
4 Conclusion, 514
Prove: ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]
Suppose...
602 x e n & y e n
Premise
603 x e n
Split, 602
604 y e n
Split, 602
605 x e n
=> ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]
U Spec, 601
606 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e pow]]
Detach, 605, 603
607 y e n => EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 606
608 EXIST(c):[c e n & (x,y,c) e pow]
Detach, 607, 604
Functionality of pow, Part 2
609 ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e pow]]
4 Conclusion, 602
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...
610 x e n
Premise
611 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
612 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, 611
Define: p2
**********
613 Set(p2)
Split, 612
614 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, 612
615 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, 6
616 y e p2
Premise
617 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, 614
618 [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, 617
619 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, 618
620 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, 618
621 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, 619, 616
622 y e n
Split, 621
623 ALL(b):[b e p2 => b e n]
4 Conclusion, 616
624 Set(p2) & ALL(b):[b e p2 => b e n]
Join, 613, 623
Sufficient: ALL(b):[b e n => b e p2]
625 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
=> ALL(b):[b e n => b e p2]
Detach, 615, 624
626 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, 614
627 [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, 626
628 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, 627
Sufficient: 0 e p2
629 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, 627
630 z1 e n & z2 e n
Premise
631 z1 e n
Split, 630
632 z2 e n
Split, 630
633 (x,0,z1) e pow & (x,0,z2) e pow
Premise
634 (x,0,z1) e pow
Split, 633
635 (x,0,z2) e pow
Split, 633
2 cases:
636 x=0 | ~x=0
Or Not
637 x=0
Premise
638 z1 e n => [(0,0,z1) e pow => z1=x0]
U Spec, 304
639 (0,0,z1) e pow => z1=x0
Detach, 638, 631
640 (x,0,z1) e pow => z1=x0
Substitute, 637, 639
641 z1=x0
Detach, 640, 634
642 z2 e n => [(0,0,z2) e pow => z2=x0]
U Spec, 304
643 (0,0,z2) e pow => z2=x0
Detach, 642, 632
644 (x,0,z2) e pow => z2=x0
Substitute, 637, 643
645 z2=x0
Detach, 644, 635
646 z1=z2
Substitute, 645, 641
647 x=0 => z1=z2
4 Conclusion, 637
648 ~x=0
Premise
649 x e n
=> [~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]]
U Spec, 490
650 ~x=0 => ALL(b):[b e n => [(x,0,b) e pow => b=1]]
Detach, 649, 610
651 ALL(b):[b e n => [(x,0,b) e pow => b=1]]
Detach, 650, 648
652 z1 e n => [(x,0,z1) e pow => z1=1]
U Spec, 651
653 (x,0,z1) e pow => z1=1
Detach, 652, 631
654 z1=1
Detach, 653, 634
655 z2 e n => [(x,0,z2) e pow => z2=1]
U Spec, 651
656 (x,0,z2) e pow => z2=1
Detach, 655, 632
657 z2=1
Detach, 656, 635
658 z1=z2
Substitute, 657, 654
659 ~x=0 => z1=z2
4 Conclusion, 648
660 [x=0 => z1=z2] & [~x=0 => z1=z2]
Join, 647, 659
661 z1=z2
Cases, 636, 660
662 (x,0,z1) e pow & (x,0,z2) e pow => z1=z2
4 Conclusion, 633
663 ALL(c1):ALL(c2):[c1 e n & c2 e n
=> [(x,0,c1) e pow & (x,0,c2) e pow => c1=c2]]
4 Conclusion, 630
664 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, 663
As Required:
665 0 e p2
Detach, 629, 664
Suppose...
666 y e p2
Premise
667 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, 614
668 [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, 667
669 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, 668
670 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, 668
671 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, 669, 666
672 y e n
Split, 671
673 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Split, 671
674 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]
U Spec, 609
675 x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 674
676 x e n & y e n
Join, 610, 672
677 EXIST(c):[c e n & (x,y,c) e pow]
Detach, 675, 676
678 z e n & (x,y,z) e pow
E Spec, 677
679 z e n
Split, 678
680 (x,y,z) e pow
Split, 678
681 ALL(c2):[z e n & c2 e n => [(x,y,z) e pow & (x,y,c2) e pow => z=c2]]
U Spec, 673
682 z' e n
Premise
683 z e n & z' e n => [(x,y,z) e pow & (x,y,z') e pow => z=z']
U Spec, 681
684 z e n & z' e n
Join, 679, 682
685 (x,y,z) e pow & (x,y,z') e pow => z=z'
Detach, 683, 684
686 (x,y,z') e pow
Premise
687 (x,y,z) e pow & (x,y,z') e pow
Join, 680, 686
688 z=z'
Detach, 685, 687
689 (x,y,z') e pow => z=z'
4 Conclusion, 686
z is unique
690 ALL(c):[c e n => [(x,y,c) e pow => z=c]]
4 Conclusion, 682
Prove: ALL(a):[aen => [(x,y+1,a) => a=z*x]]
Suppose...
691 z' e n
Premise
Suppose to the contrary...
692 (x,y+1,z') e pow & ~z'=z*x
Premise
693 (x,y+1,z') e pow
Split, 692
694 ~z'=z*x
Split, 692
695 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, 29
696 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, 695
697 (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, 696
698 [(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, 697
699 (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, 698
700 (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, 698
701 ~[(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, 699
702 ~~[~(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, 701
703 ~(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, 702
704 ~(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, 703
705 ~(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, 704
706 ~(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, 705
Sufficient: ~(x,y+1,z') e pow (to obtain a contradiction)
707 ~(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, 706
708 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, 28
709 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, 708
Define: q
*********
710 Set''(q)
Split, 709
711 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e pow & ~[a=x & b=y+1 & c=z']]
Split, 709
712 q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
U Spec, 24
713 [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, 712
714 q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Split, 713
Sufficient: q e pn3
715 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 713
Suppose...
716 (t,u,v) e q
Premise
717 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 711
718 ALL(c):[(t,u,c) e q
<=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]
U Spec, 717
719 (t,u,v) e q
<=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
U Spec, 718
720 [(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, 719
721 (t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Split, 720
722 (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q
Split, 720
723 (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Detach, 721, 716
724 (t,u,v) e pow
Split, 723
725 ~[t=x & u=y+1 & v=z']
Split, 723
726 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, 29
727 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, 726
728 (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, 727
729 [(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, 728
730 (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, 729
731 (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, 729
732 (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, 730, 724
733 (t,u,v) e n3
Split, 732
734 ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]
4 Conclusion, 716
735 Set''(q)
& ALL(a):ALL(b):ALL(c):[(a,b,c) e q => (a,b,c) e n3]
Join, 710, 734
As Required:
736 q e pn3
Detach, 715, 735
737 ALL(b):ALL(c):[(0,b,c) e q
<=> (0,b,c) e pow & ~[0=x & b=y+1 & c=z']]
U Spec, 711
738 ALL(c):[(0,0,c) e q
<=> (0,0,c) e pow & ~[0=x & 0=y+1 & c=z']]
U Spec, 737
739 (0,0,x0) e q
<=> (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']
U Spec, 738
740 [(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, 739
741 (0,0,x0) e q => (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']
Split, 740
742 (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z'] => (0,0,x0) e q
Split, 740
743 0=x & 0=y+1 & x0=z'
Premise
744 0=x
Split, 743
745 0=y+1
Split, 743
746 x0=z'
Split, 743
747 y e n => ~y+1=0
U Spec, 8
748 ~y+1=0
Detach, 747, 672
749 y+1=0
Sym, 745
750 y+1=0 & ~y+1=0
Join, 749, 748
751 ~[0=x & 0=y+1 & x0=z']
4 Conclusion, 743
752 (0,0,x0) e pow & ~[0=x & 0=y+1 & x0=z']
Join, 50, 751
As Required:
753 (0,0,x0) e q
Detach, 742, 752
754 ALL(b):ALL(c):[(x,b,c) e q
<=> (x,b,c) e pow & ~[x=x & b=y+1 & c=z']]
U Spec, 711
755 ALL(c):[(x,y+1,c) e q
<=> (x,y+1,c) e pow & ~[x=x & y+1=y+1 & c=z']]
U Spec, 754
756 (x,y+1,z') e q
<=> (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']
U Spec, 755
757 [(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, 756
758 (x,y+1,z') e q => (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']
Split, 757
759 (x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z'] => (x,y+1,z') e q
Split, 757
760 ~[(x,y+1,z') e pow & ~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q
Contra, 758
761 ~~[~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z']] => ~(x,y+1,z') e q
DeMorgan, 760
762 ~(x,y+1,z') e pow | ~~[x=x & y+1=y+1 & z'=z'] => ~(x,y+1,z') e q
Rem DNeg, 761
763 ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z' => ~(x,y+1,z') e q
Rem DNeg, 762
764 x=x
Reflex
765 y+1=y+1
Reflex
766 z'=z'
Reflex
767 x=x & y+1=y+1
Join, 764, 765
768 x=x & y+1=y+1 & z'=z'
Join, 767, 766
769 ~(x,y+1,z') e pow | x=x & y+1=y+1 & z'=z'
Arb Or, 768
As Required:
770 ~(x,y+1,z') e q
Detach, 763, 769
Suppose...
771 (t,u,v) e q
Premise
772 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 711
773 ALL(c):[(t,u,c) e q
<=> (t,u,c) e pow & ~[t=x & u=y+1 & c=z']]
U Spec, 772
774 (t,u,v) e q
<=> (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
U Spec, 773
775 [(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, 774
776 (t,u,v) e q => (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Split, 775
777 (t,u,v) e pow & ~[t=x & u=y+1 & v=z'] => (t,u,v) e q
Split, 775
778 (t,u,v) e pow & ~[t=x & u=y+1 & v=z']
Detach, 776, 771
779 (t,u,v) e pow
Split, 778
780 ~[t=x & u=y+1 & v=z']
Split, 778
781 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, 29
782 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, 781
783 (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, 782
784 [(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, 783
785 (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, 784
786 (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, 784
787 (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, 785, 779
788 (t,u,v) e n3
Split, 787
789 ALL(c2):ALL(c3):[(t,c2,c3) e n3 <=> t e n & c2 e n & c3 e n]
U Spec, 18
790 ALL(c3):[(t,u,c3) e n3 <=> t e n & u e n & c3 e n]
U Spec, 789
791 (t,u,v) e n3 <=> t e n & u e n & v e n
U Spec, 790
792 [(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, 791
793 (t,u,v) e n3 => t e n & u e n & v e n
Split, 792
794 t e n & u e n & v e n => (t,u,v) e n3
Split, 792
795 t e n & u e n & v e n
Detach, 793, 788
796 t e n
Split, 795
797 u e n
Split, 795
798 v e n
Split, 795
799 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, 787
800 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 711
801 ALL(c):[(t,u+1,c) e q
<=> (t,u+1,c) e pow & ~[t=x & u+1=y+1 & c=z']]
U Spec, 800
802 (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, 801
803 [(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, 802
804 (t,u+1,v*t) e q => (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']
Split, 803
805 (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z'] => (t,u+1,v*t) e q
Split, 803
806 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, 133
807 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, 806
808 t e n & u e n & v e n
=> [(t,u,v) e pow => (t,u+1,v*t) e pow]
U Spec, 807
809 (t,u,v) e pow => (t,u+1,v*t) e pow
Detach, 808, 795
810 (t,u+1,v*t) e pow
Detach, 809, 779
Suppose to the contrary...
811 t=x & u+1=y+1 & v*t=z'
Premise
812 t=x
Split, 811
813 u+1=y+1
Split, 811
814 v*t=z'
Split, 811
815 v*x=z'
Substitute, 812, 814
816 ALL(b):ALL(c):[u e n & b e n & c e n => [u+b=c+b => u=c]]
U Spec, 7
817 ALL(c):[u e n & 1 e n & c e n => [u+1=c+1 => u=c]]
U Spec, 816
818 u e n & 1 e n & y e n => [u+1=y+1 => u=y]
U Spec, 817
819 u e n & 1 e n
Join, 797, 5
820 u e n & 1 e n & y e n
Join, 819, 672
821 u+1=y+1 => u=y
Detach, 818, 820
822 u=y
Detach, 821, 813
823 (x,u,v) e pow
Substitute, 812, 779
824 (x,y,v) e pow
Substitute, 822, 823
825 v e n => [(x,y,v) e pow => z=v]
U Spec, 690
826 (x,y,v) e pow => z=v
Detach, 825, 798
827 z=v
Detach, 826, 824
828 z*x=z'
Substitute, 827, 815
829 z'=z*x
Sym, 828
830 z'=z*x & ~z'=z*x
Join, 829, 694
831 ~[t=x & u+1=y+1 & v*t=z']
4 Conclusion, 811
832 (t,u+1,v*t) e pow & ~[t=x & u+1=y+1 & v*t=z']
Join, 810, 831
833 (t,u+1,v*t) e q
Detach, 805, 832
As Required:
834 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g*e) e q]
4 Conclusion, 771
835 t e n
Premise
836 ~t=0
Premise
837 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e pow & ~[t=x & b=y+1 & c=z']]
U Spec, 711
838 ALL(c):[(t,0,c) e q
<=> (t,0,c) e pow & ~[t=x & 0=y+1 & c=z']]
U Spec, 837
839 (t,0,1) e q
<=> (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']
U Spec, 838
840 [(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, 839
841 (t,0,1) e q => (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']
Split, 840
Sufficient: (t,0,1) e q
842 (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z'] => (t,0,1) e q
Split, 840
843 t e n => [~t=0 => (t,0,1) e pow]
U Spec, 80
844 ~t=0 => (t,0,1) e pow
Detach, 843, 835
845 (t,0,1) e pow
Detach, 844, 836
846 t=x & 0=y+1 & 1=z'
Premise
847 t=x
Split, 846
848 0=y+1
Split, 846
849 1=z'
Split, 846
850 y e n => ~y+1=0
U Spec, 8
851 ~y+1=0
Detach, 850, 672
852 y+1=0
Sym, 848
853 y+1=0 & ~y+1=0
Join, 852, 851
854 ~[t=x & 0=y+1 & 1=z']
4 Conclusion, 846
855 (t,0,1) e pow & ~[t=x & 0=y+1 & 1=z']
Join, 845, 854
856 (t,0,1) e q
Detach, 842, 855
857 ~t=0 => (t,0,1) e q
4 Conclusion, 836
As Required:
858 ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
4 Conclusion, 835
859 q e pn3 & (0,0,x0) e q
Join, 736, 753
860 q e pn3 & (0,0,x0) e q
& ALL(e):[e e n => [~e=0 => (e,0,1) e q]]
Join, 859, 858
861 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, 860, 834
862 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, 861, 770
863 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, 862
864 ~(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, 863
865 ~(x,y+1,z') e pow
Detach, 707, 864
866 (x,y+1,z') e pow & ~(x,y+1,z') e pow
Join, 693, 865
867 ~[(x,y+1,z') e pow & ~z'=z*x]
4 Conclusion, 692
868 ~~[(x,y+1,z') e pow => ~~z'=z*x]
Imply-And, 867
869 (x,y+1,z') e pow => ~~z'=z*x
Rem DNeg, 868
870 (x,y+1,z') e pow => z'=z*x
Rem DNeg, 869
As Required:
871 ALL(d):[d e n => [(x,y+1,d) e pow => d=z*x]]
4 Conclusion, 691
872 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, 614
873 [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, 872
874 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, 873
Sufficient: y+1 e p2
875 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, 873
876 ALL(b):[y e n & b e n => y+b e n]
U Spec, 2
877 y e n & 1 e n => y+1 e n
U Spec, 876
878 y e n & 1 e n
Join, 672, 5
879 y+1 e n
Detach, 877, 878
880 z1 e n & z2 e n
Premise
881 z1 e n
Split, 880
882 z2 e n
Split, 880
883 (x,y+1,z1) e pow & (x,y+1,z2) e pow
Premise
884 (x,y+1,z1) e pow
Split, 883
885 (x,y+1,z2) e pow
Split, 883
886 z1 e n => [(x,y+1,z1) e pow => z1=z*x]
U Spec, 871
887 (x,y+1,z1) e pow => z1=z*x
Detach, 886, 881
888 z1=z*x
Detach, 887, 884
889 z2 e n => [(x,y+1,z2) e pow => z2=z*x]
U Spec, 871
890 (x,y+1,z2) e pow => z2=z*x
Detach, 889, 882
891 z2=z*x
Detach, 890, 885
892 z1=z2
Substitute, 891, 888
893 (x,y+1,z1) e pow & (x,y+1,z2) e pow => z1=z2
4 Conclusion, 883
As Required:
894 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, 880
895 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, 879, 894
896 y+1 e p2
Detach, 875, 895
897 ALL(b):[b e p2 => b+1 e p2]
4 Conclusion, 666
898 0 e p2 & ALL(b):[b e p2 => b+1 e p2]
Join, 665, 897
As Required:
899 ALL(b):[b e n => b e p2]
Detach, 625, 898
900 y e n
Premise
901 y e n => y e p2
U Spec, 899
902 y e p2
Detach, 901, 900
903 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, 614
904 [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, 903
905 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, 904
906 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, 904
907 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, 905, 902
908 y e n
Split, 907
909 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Split, 907
910 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, 900
As Required:
911 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, 610
Prove: ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]
Suppose...
912 (x,y,z1) e pow & (x,y,z2) e pow
Premise
913 (x,y,z1) e pow
Split, 912
914 (x,y,z2) e pow
Split, 912
915 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, 29
916 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, 915
917 (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, 916
918 [(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, 917
919 (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, 918
920 (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, 918
921 (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, 919, 913
922 (x,y,z1) e n3
Split, 921
923 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, 921
924 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 18
925 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 924
926 (x,y,z1) e n3 <=> x e n & y e n & z1 e n
U Spec, 925
927 [(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, 926
928 (x,y,z1) e n3 => x e n & y e n & z1 e n
Split, 927
929 x e n & y e n & z1 e n => (x,y,z1) e n3
Split, 927
930 x e n & y e n & z1 e n
Detach, 928, 922
931 x e n
Split, 930
932 y e n
Split, 930
933 z1 e n
Split, 930
934 (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, 916
935 [(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, 934
936 (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, 935
937 (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, 935
938 (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, 936, 914
939 (x,y,z2) e n3
Split, 938
940 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, 938
941 (x,y,z2) e n3 <=> x e n & y e n & z2 e n
U Spec, 925
942 [(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, 941
943 (x,y,z2) e n3 => x e n & y e n & z2 e n
Split, 942
944 x e n & y e n & z2 e n => (x,y,z2) e n3
Split, 942
945 x e n & y e n & z2 e n
Detach, 943, 939
946 x e n
Split, 945
947 y e n
Split, 945
948 z2 e n
Split, 945
949 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, 911
950 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, 949, 931
951 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, 950
952 ALL(c1):ALL(c2):[c1 e n & c2 e n => [(x,y,c1) e pow & (x,y,c2) e pow => c1=c2]]
Detach, 951, 932
953 ALL(c2):[z1 e n & c2 e n => [(x,y,z1) e pow & (x,y,c2) e pow => z1=c2]]
U Spec, 952
954 z1 e n & z2 e n => [(x,y,z1) e pow & (x,y,z2) e pow => z1=z2]
U Spec, 953
955 z1 e n & z2 e n
Join, 933, 948
956 (x,y,z1) e pow & (x,y,z2) e pow => z1=z2
Detach, 954, 955
957 z1=z2
Detach, 956, 912
Functionality of pow, Part 3
958 ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e pow & (a,b,c2) e pow => c1=c2]
4 Conclusion, 912
959 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, 513, 609
960 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, 959, 958
pow is a function!
******************
961 ALL(c1):ALL(c2):ALL(d):[d=pow(c1,c2) <=> (c1,c2,d) e pow]
Detach, 495, 960
Prove: ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
Suppose...
962 x e n & y e n
Premise
963 x e n
Split, 962
964 y e n
Split, 962
965 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]
U Spec, 609
966 x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 965
967 EXIST(c):[c e n & (x,y,c) e pow]
Detach, 966, 962
968 z e n & (x,y,z) e pow
E Spec, 967
969 z e n
Split, 968
970 (x,y,z) e pow
Split, 968
971 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 961
972 ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]
U Spec, 971
973 z=pow(x,y) <=> (x,y,z) e pow
U Spec, 972
974 [z=pow(x,y) => (x,y,z) e pow]
& [(x,y,z) e pow => z=pow(x,y)]
Iff-And, 973
975 z=pow(x,y) => (x,y,z) e pow
Split, 974
976 (x,y,z) e pow => z=pow(x,y)
Split, 974
977 z=pow(x,y)
Detach, 976, 970
978 pow(x,y) e n
Substitute, 977, 969
As Required:
979 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
4 Conclusion, 962
Prove: pow(0,0)=x0
980 ALL(c2):ALL(d):[d=pow(0,c2) <=> (0,c2,d) e pow]
U Spec, 961
981 ALL(d):[d=pow(0,0) <=> (0,0,d) e pow]
U Spec, 980
982 x0=pow(0,0) <=> (0,0,x0) e pow
U Spec, 981
983 [x0=pow(0,0) => (0,0,x0) e pow]
& [(0,0,x0) e pow => x0=pow(0,0)]
Iff-And, 982
984 x0=pow(0,0) => (0,0,x0) e pow
Split, 983
985 (0,0,x0) e pow => x0=pow(0,0)
Split, 983
986 x0=pow(0,0)
Detach, 985, 50
As Required:
987 pow(0,0)=x0
Sym, 986
Prove: ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
Suppose...
988 x e n
Premise
989 x e n => [~x=0 => (x,0,1) e pow]
U Spec, 80
990 ~x=0 => (x,0,1) e pow
Detach, 989, 988
Prove: ~x=0 => pow(x,0)=1
Suppose...
991 ~x=0
Premise
992 (x,0,1) e pow
Detach, 990, 991
993 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 961
994 ALL(d):[d=pow(x,0) <=> (x,0,d) e pow]
U Spec, 993
995 1=pow(x,0) <=> (x,0,1) e pow
U Spec, 994
996 [1=pow(x,0) => (x,0,1) e pow]
& [(x,0,1) e pow => 1=pow(x,0)]
Iff-And, 995
997 1=pow(x,0) => (x,0,1) e pow
Split, 996
998 (x,0,1) e pow => 1=pow(x,0)
Split, 996
999 1=pow(x,0)
Detach, 998, 992
1000 pow(x,0)=1
Sym, 999
As Required:
1001 ~x=0 => pow(x,0)=1
4 Conclusion, 991
As Required:
1002 ALL(a):[a e n => [~a=0 => pow(a,0)=1]]
4 Conclusion, 988
Prove: ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
Suppose...
1003 x e n & y e n
Premise
1004 x e n
Split, 1003
1005 y e n
Split, 1003
1006 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e pow]]
U Spec, 609
1007 x e n & y e n => EXIST(c):[c e n & (x,y,c) e pow]
U Spec, 1006
1008 EXIST(c):[c e n & (x,y,c) e pow]
Detach, 1007, 1003
1009 z1 e n & (x,y,z1) e pow
E Spec, 1008
1010 z1 e n
Split, 1009
1011 (x,y,z1) e pow
Split, 1009
1012 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 961
1013 ALL(d):[d=pow(x,y) <=> (x,y,d) e pow]
U Spec, 1012
1014 z1=pow(x,y) <=> (x,y,z1) e pow
U Spec, 1013
1015 [z1=pow(x,y) => (x,y,z1) e pow]
& [(x,y,z1) e pow => z1=pow(x,y)]
Iff-And, 1014
1016 z1=pow(x,y) => (x,y,z1) e pow
Split, 1015
1017 (x,y,z1) e pow => z1=pow(x,y)
Split, 1015
1018 z1=pow(x,y)
Detach, 1017, 1011
1019 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, 133
1020 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, 1019
1021 x e n & y e n & z1 e n
=> [(x,y,z1) e pow => (x,y+1,z1*x) e pow]
U Spec, 1020
1022 x e n & y e n & z1 e n
Join, 1003, 1010
1023 (x,y,z1) e pow => (x,y+1,z1*x) e pow
Detach, 1021, 1022
1024 (x,y+1,z1*x) e pow
Detach, 1023, 1011
1025 ALL(c2):ALL(d):[d=pow(x,c2) <=> (x,c2,d) e pow]
U Spec, 961
1026 ALL(d):[d=pow(x,y+1) <=> (x,y+1,d) e pow]
U Spec, 1025
1027 z1*x=pow(x,y+1) <=> (x,y+1,z1*x) e pow
U Spec, 1026
1028 [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, 1027
1029 z1*x=pow(x,y+1) => (x,y+1,z1*x) e pow
Split, 1028
1030 (x,y+1,z1*x) e pow => z1*x=pow(x,y+1)
Split, 1028
1031 z1*x=pow(x,y+1)
Detach, 1030, 1024
1032 pow(x,y+1)=z1*x
Sym, 1031
1033 pow(x,y+1)=pow(x,y)*x
Substitute, 1018, 1032
As Required:
1034 ALL(a):ALL(b):[a e n & b e n => pow(a,b+1)=pow(a,b)*a]
4 Conclusion, 1003
1035 ALL(a):ALL(b):[a e n & b e n => pow(a,b) e n]
& pow(0,0)=x0
Join, 979, 987
1036 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]]
Join, 1035, 1002
1037 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]
Join, 1036, 1034
As Required:
1038 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]]]
4 Conclusion, 25