THEOREM
*******
Here we construct, i.e. prove the existence of an multiplication function (*) on the set of natural numbers n using Peano's Axioms, the previously construct add function (+), the Subset, Cartesian Product, Power Set and Function axioms (DC Proof).
Prove: EXIST(mult):[ALL(a):ALL(b):[a e n & b e n => mult(a,b) e n]
& ALL(a):[a e n => mult(a,1)=a]
& ALL(a):ALL(b):[a e n & b e n => mult(a,b+1)=mult(a,b)+a]]
In subsequent proofs, we will use the more standard infix '*' notation.
This proof was written and verified with the aid of the author's DC Proof 2.0 software available free at http://www.dcproof.com
OUTLINE OF PROOF
****************
We begin by constructing the set all ordered triples of natural numbers (n3), as well as its power set (pn3) using the Cartesian Product and Power Set axioms (lines 1-25).
Using the Subset axiom (DC Proof), we then (lines 26-29) construct the subset add of n3 (mult) such that:
ALL(a):ALL(b):ALL(c):[(a,b,c) e mult
<=> (a,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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]]
We then (lines 30-733) establish the functionality and other required properties of mult.
PEANO'S AXIOMS
**************
1 Set(n)
Axiom
2 1 e n
Axiom
3 ALL(a):[a e n => s(a) e n]
Axiom
4 ALL(a):ALL(b):[a e n & b e n => [s(a)=s(b) => a=b]]
Axiom
5 ALL(a):[a e n => ~s(a)=1]
Axiom
6 ALL(a):[Set(a) & ALL(b):[b e a => b e n]
=> [1 e a & ALL(b):[b e a => s(b) e a]
=> ALL(b):[b e n => b e a]]]
Axiom
FROM PREVIOUS RESULTS
*********************
7 ALL(a):ALL(b):[a e n & b e n => a+b e n]
Axiom
8 ALL(a):[a e n => a+1=s(a)]
Axiom
9 ALL(a):ALL(b):[a e n & b e n => a+(b+1)=a+b+1]
Axiom
PROOF
*****
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(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, 10
12
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, 11
13
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, 12
14 Set(n) & Set(n)
Join, 1, 1
15 Set(n) & Set(n) & Set(n)
Join, 14, 1
16 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, 13, 15
17 Set''(n3) & ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
E Spec, 16
Define: n3
**********
The set of ordered triples of natural numbers
18 Set''(n3)
Split, 17
19 ALL(c1):ALL(c2):ALL(c3):[(c1,c2,c3) e n3 <=> c1 e n & c2 e n & c3 e n]
Split, 17
Apply Power Set axiom
20 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
21 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, 20
22 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, 21, 18
23 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, 22
Define: pn3
***********
The power set of n3
24 Set(pn3)
Split, 23
25 ALL(c):[c e pn3 <=> Set''(c) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e c => (d1,d2,d3) e n3]]
Split, 23
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
& ALL(e):[e e n => (e,1,e) 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, 18
27 Set''(mult) & ALL(a):ALL(b):ALL(c):[(a,b,c) e mult
<=> (a,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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: mult
************
28 Set''(mult)
Split, 27
29 ALL(a):ALL(b):ALL(c):[(a,b,c) e mult
<=> (a,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
30 x e n
Premise
31 ALL(b):ALL(c):[(x,b,c) e mult
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
32 ALL(c):[(x,1,c) e mult
<=> (x,1,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,c) e d]]
U Spec, 31
33 (x,1,x) e mult
<=> (x,1,x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,x) e d]
U Spec, 32
34 [(x,1,x) e mult => (x,1,x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,x) e d]]
& [(x,1,x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,x) e d] => (x,1,x) e mult]
Iff-And, 33
35 (x,1,x) e mult => (x,1,x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,x) e d]
Split, 34
Sufficient: For (x,1,x) e mult
36 (x,1,x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,x) e d] => (x,1,x) e mult
Split, 34
37 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 19
38 ALL(c3):[(x,1,c3) e n3 <=> x e n & 1 e n & c3 e n]
U Spec, 37
39 (x,1,x) e n3 <=> x e n & 1 e n & x e n
U Spec, 38
40 [(x,1,x) e n3 => x e n & 1 e n & x e n]
& [x e n & 1 e n & x e n => (x,1,x) e n3]
Iff-And, 39
41 (x,1,x) e n3 => x e n & 1 e n & x e n
Split, 40
42 x e n & 1 e n & x e n => (x,1,x) e n3
Split, 40
43 x e n & 1 e n
Join, 30, 2
44 x e n & 1 e n & x e n
Join, 43, 30
As Required:
45 (x,1,x) e n3
Detach, 42, 44
46 d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
Premise
47 d e pn3
Split, 46
48 ALL(e):[e e n => (e,1,e) e d]
Split, 46
49 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
Split, 46
50 x e n => (x,1,x) e d
U Spec, 48
51 (x,1,x) e d
Detach, 50, 30
52 ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,x) e d]
4 Conclusion, 46
53 (x,1,x) e n3
& ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,x) e d]
Join, 45, 52
54 (x,1,x) e mult
Detach, 36, 53
Some properties of mult:
As Required:
55 ALL(a):[a e n => (a,1,a) e mult]
4 Conclusion, 30
56 (x,y,z) e mult
Premise
57 ALL(b):ALL(c):[(x,b,c) e mult
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
58 ALL(c):[(x,y,c) e mult
<=> (x,y,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 57
59 (x,y,z) e mult
<=> (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 58
60 [(x,y,z) e mult => (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
& ALL(e):[e e n => (e,1,e) 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 mult]
Iff-And, 59
61 (x,y,z) e mult => (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 60
62 (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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 mult
Split, 60
63 (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 61, 56
64 (x,y,z) e n3
Split, 63
65 ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 63
66 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 19
67 ALL(c3):[(x,y,c3) e n3 <=> x e n & y e n & c3 e n]
U Spec, 66
68 (x,y,z) e n3 <=> x e n & y e n & z e n
U Spec, 67
69 [(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, 68
70 (x,y,z) e n3 => x e n & y e n & z e n
Split, 69
71 x e n & y e n & z e n => (x,y,z) e n3
Split, 69
72 x e n & y e n & z e n
Detach, 70, 64
73 (x,y,z) e n3 & [x e n & y e n & z e n]
Join, 64, 72
As Required:
74 ALL(a):ALL(b):ALL(c):[(a,b,c) e mult
=> (a,b,c) e n3 & [a e n & b e n & c e n]]
4 Conclusion, 56
75 (x,y,z) e mult
Premise
76 ALL(b):ALL(c):[(x,b,c) e mult
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 74
77 ALL(c):[(x,y,c) e mult
=> (x,y,c) e n3 & [x e n & y e n & c e n]]
U Spec, 76
78 (x,y,z) e mult
=> (x,y,z) e n3 & [x e n & y e n & z e n]
U Spec, 77
79 (x,y,z) e n3 & [x e n & y e n & z e n]
Detach, 78, 75
80 (x,y,z) e n3
Split, 79
81 x e n & y e n & z e n
Split, 79
82 x e n
Split, 81
83 y e n
Split, 81
84 z e n
Split, 81
85 ALL(b):ALL(c):[(x,b,c) e mult
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
86 ALL(c):[(x,y+1,c) e mult
<=> (x,y+1,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 85
87 (x,y+1,z+x) e mult
<=> (x,y+1,z+x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 86
88 [(x,y+1,z+x) e mult => (x,y+1,z+x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
& ALL(e):[e e n => (e,1,e) 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 mult]
Iff-And, 87
89 (x,y+1,z+x) e mult => (x,y+1,z+x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 88
Sufficient: For (x,y+1,z+x) e mult
90 (x,y+1,z+x) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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 mult
Split, 88
91 ALL(c2):ALL(c3):[(x,c2,c3) e n3 <=> x e n & c2 e n & c3 e n]
U Spec, 19
92 ALL(c3):[(x,y+1,c3) e n3 <=> x e n & y+1 e n & c3 e n]
U Spec, 91
93 (x,y+1,z+x) e n3 <=> x e n & y+1 e n & z+x e n
U Spec, 92
94 [(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, 93
95 (x,y+1,z+x) e n3 => x e n & y+1 e n & z+x e n
Split, 94
96 x e n & y+1 e n & z+x e n => (x,y+1,z+x) e n3
Split, 94
97 ALL(b):[y e n & b e n => y+b e n]
U Spec, 7
98 y e n & 1 e n => y+1 e n
U Spec, 97
99 y e n & 1 e n
Join, 83, 2
100 y+1 e n
Detach, 98, 99
101 ALL(b):[z e n & b e n => z+b e n]
U Spec, 7
102 z e n & x e n => z+x e n
U Spec, 101
103 z e n & x e n
Join, 84, 82
104 z+x e n
Detach, 102, 103
105 x e n & y+1 e n
Join, 82, 100
106 x e n & y+1 e n & z+x e n
Join, 105, 104
107 (x,y+1,z+x) e n3
Detach, 96, 106
108 d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
Premise
109 d e pn3
Split, 108
110 ALL(e):[e e n => (e,1,e) e d]
Split, 108
111 ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
Split, 108
112 ALL(f):ALL(g):[(x,f,g) e d => (x,f+1,g+x) e d]
U Spec, 111
113 ALL(g):[(x,y,g) e d => (x,y+1,g+x) e d]
U Spec, 112
114 (x,y,z) e d => (x,y+1,z+x) e d
U Spec, 113
115 ALL(b):ALL(c):[(x,b,c) e mult
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
116 ALL(c):[(x,y,c) e mult
<=> (x,y,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 115
117 (x,y,z) e mult
<=> (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 116
118 [(x,y,z) e mult => (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
& ALL(e):[e e n => (e,1,e) 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 mult]
Iff-And, 117
119 (x,y,z) e mult => (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 118
120 (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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 mult
Split, 118
121 (x,y,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 119, 75
122 (x,y,z) e n3
Split, 121
123 ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 121
124 d e pn3
& ALL(e):[e e n => (e,1,e) 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, 123
125 (x,y,z) e d
Detach, 124, 108
126 (x,y+1,z+x) e d
Detach, 114, 125
127 ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 108
128 (x,y+1,z+x) e n3
& ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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, 107, 127
129 (x,y+1,z+x) e mult
Detach, 90, 128
As Required:
130 ALL(a):ALL(b):ALL(c):[(a,b,c) e mult => (a,b+1,c+a) e mult]
4 Conclusion, 75
131 x e n & z e n
Premise
132 x e n
Split, 131
133 z e n
Split, 131
Suppose to the contrary...
134 ~[(x,1,z) e mult => z=x]
Premise
135 ~~[(x,1,z) e mult & ~z=x]
Imply-And, 134
136 (x,1,z) e mult & ~z=x
Rem DNeg, 135
137 (x,1,z) e mult
Split, 136
138 ~z=x
Split, 136
139 ALL(b):ALL(c):[(x,b,c) e mult
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
140 ALL(c):[(x,1,c) e mult
<=> (x,1,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,c) e d]]
U Spec, 139
141 (x,1,z) e mult
<=> (x,1,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d]
U Spec, 140
142 [(x,1,z) e mult => (x,1,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d]]
& [(x,1,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d] => (x,1,z) e mult]
Iff-And, 141
143 (x,1,z) e mult => (x,1,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d]
Split, 142
144 (x,1,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d] => (x,1,z) e mult
Split, 142
145 ~[(x,1,z) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d]] => ~(x,1,z) e mult
Contra, 143
146 ~~[~(x,1,z) e n3 | ~ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d]] => ~(x,1,z) e mult
DeMorgan, 145
147 ~(x,1,z) e n3 | ~ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d] => ~(x,1,z) e mult
Rem DNeg, 146
148 ~(x,1,z) e n3 | ~~EXIST(d):~[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d] => ~(x,1,z) e mult
Quant, 147
149 ~(x,1,z) e n3 | EXIST(d):~[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,1,z) e d] => ~(x,1,z) e mult
Rem DNeg, 148
150 ~(x,1,z) e n3 | EXIST(d):~~[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g)
e d =>
(e,f+1,g+e)
e d] & ~(x,1,z)
e d]
=> ~(x,1,z)
e mult
Imply-And, 149
Sufficient: ~(x,1,z) e mult
151 ~(x,1,z) e n3 | EXIST(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g)
e d =>
(e,f+1,g+e)
e d] & ~(x,1,z)
e d]
=> ~(x,1,z)
e mult
Rem DNeg, 150
152 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e mult & ~[a=x & b=1 & c=z]]]
Subset, 28
153 Set''(q) & ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e mult & ~[a=x & b=1 & c=z]]
E Spec, 152
Define: q
*********
154 Set''(q)
Split, 153
155 ALL(a):ALL(b):ALL(c):[(a,b,c) e q
<=> (a,b,c) e mult & ~[a=x & b=1 & c=z]]
Split, 153
156 q e pn3 <=> Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
U Spec, 25
157 [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, 156
158 q e pn3 => Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Split, 157
159 Set''(q) & ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3] => q e pn3
Split, 157
160 (t,u,v) e q
Premise
161 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e mult & ~[t=x & b=1 & c=z]]
U Spec, 155
162 ALL(c):[(t,u,c) e q
<=> (t,u,c) e mult & ~[t=x & u=1 & c=z]]
U Spec, 161
163 (t,u,v) e q
<=> (t,u,v) e mult & ~[t=x & u=1 & v=z]
U Spec, 162
164 [(t,u,v) e q => (t,u,v) e mult & ~[t=x & u=1 & v=z]]
& [(t,u,v) e mult & ~[t=x & u=1 & v=z] => (t,u,v) e q]
Iff-And, 163
165 (t,u,v) e q => (t,u,v) e mult & ~[t=x & u=1 & v=z]
Split, 164
166 (t,u,v) e mult & ~[t=x & u=1 & v=z] => (t,u,v) e q
Split, 164
167 (t,u,v) e mult & ~[t=x & u=1 & v=z]
Detach, 165, 160
168 (t,u,v) e mult
Split, 167
169 ~[t=x & u=1 & v=z]
Split, 167
170 ALL(b):ALL(c):[(t,b,c) e mult
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 74
171 ALL(c):[(t,u,c) e mult
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 170
172 (t,u,v) e mult
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 171
173 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 172, 168
174 (t,u,v) e n3
Split, 173
175 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
4 Conclusion, 160
176 Set''(q)
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q => (d1,d2,d3) e n3]
Join, 154, 175
As Required:
177 q e pn3
Detach, 159, 176
178 t e n
Premise
179 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e mult & ~[t=x & b=1 & c=z]]
U Spec, 155
180 ALL(c):[(t,1,c) e q
<=> (t,1,c) e mult & ~[t=x & 1=1 & c=z]]
U Spec, 179
181 (t,1,t) e q
<=> (t,1,t) e mult & ~[t=x & 1=1 & t=z]
U Spec, 180
182 [(t,1,t) e q => (t,1,t) e mult & ~[t=x & 1=1 & t=z]]
& [(t,1,t) e mult & ~[t=x & 1=1 & t=z] => (t,1,t) e q]
Iff-And, 181
183 (t,1,t) e q => (t,1,t) e mult & ~[t=x & 1=1 & t=z]
Split, 182
184 (t,1,t) e mult & ~[t=x & 1=1 & t=z] => (t,1,t) e q
Split, 182
185 t e n => (t,1,t) e mult
U Spec, 55
186 (t,1,t) e mult
Detach, 185, 178
187 t=x & 1=1 & t=z
Premise
188 t=x
Split, 187
189 1=1
Split, 187
190 t=z
Split, 187
191 x=z
Substitute, 188, 190
192 z=x
Sym, 191
193 z=x & ~z=x
Join, 192, 138
194 ~[t=x & 1=1 & t=z]
4 Conclusion, 187
195 (t,1,t) e mult & ~[t=x & 1=1 & t=z]
Join, 186, 194
196 (t,1,t) e q
Detach, 184, 195
As Required:
197 ALL(e):[e e n => (e,1,e) e q]
4 Conclusion, 178
198 (t,u,v) e q
Premise
199 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e mult & ~[t=x & b=1 & c=z]]
U Spec, 155
200 ALL(c):[(t,u+1,c) e q
<=> (t,u+1,c) e mult & ~[t=x & u+1=1 & c=z]]
U Spec, 199
201 (t,u+1,v+t) e q
<=> (t,u+1,v+t) e mult & ~[t=x & u+1=1 & v+t=z]
U Spec, 200
202 [(t,u+1,v+t) e q => (t,u+1,v+t) e mult & ~[t=x & u+1=1 & v+t=z]]
& [(t,u+1,v+t) e mult & ~[t=x & u+1=1 & v+t=z] => (t,u+1,v+t) e q]
Iff-And, 201
203 (t,u+1,v+t) e q => (t,u+1,v+t) e mult & ~[t=x & u+1=1 & v+t=z]
Split, 202
204 (t,u+1,v+t) e mult & ~[t=x & u+1=1 & v+t=z] => (t,u+1,v+t) e q
Split, 202
205 ALL(b):ALL(c):[(t,b,c) e mult => (t,b+1,c+t) e mult]
U Spec, 130
206 ALL(c):[(t,u,c) e mult => (t,u+1,c+t) e mult]
U Spec, 205
207 (t,u,v) e mult => (t,u+1,v+t) e mult
U Spec, 206
208 ALL(b):ALL(c):[(t,b,c) e q
<=> (t,b,c) e mult & ~[t=x & b=1 & c=z]]
U Spec, 155
209 ALL(c):[(t,u,c) e q
<=> (t,u,c) e mult & ~[t=x & u=1 & c=z]]
U Spec, 208
210 (t,u,v) e q
<=> (t,u,v) e mult & ~[t=x & u=1 & v=z]
U Spec, 209
211 [(t,u,v) e q => (t,u,v) e mult & ~[t=x & u=1 & v=z]]
& [(t,u,v) e mult & ~[t=x & u=1 & v=z] => (t,u,v) e q]
Iff-And, 210
212 (t,u,v) e q => (t,u,v) e mult & ~[t=x & u=1 & v=z]
Split, 211
213 (t,u,v) e mult & ~[t=x & u=1 & v=z] => (t,u,v) e q
Split, 211
214 (t,u,v) e mult & ~[t=x & u=1 & v=z]
Detach, 212, 198
215 (t,u,v) e mult
Split, 214
216 ~[t=x & u=1 & v=z]
Split, 214
217 (t,u+1,v+t) e mult
Detach, 207, 215
218 t=x & u+1=1 & v+t=z
Premise
219 t=x
Split, 218
220 u+1=1
Split, 218
221 v+t=z
Split, 218
222 u e n => ~s(u)=1
U Spec, 5
223 ALL(b):ALL(c):[(t,b,c) e mult
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 74
224 ALL(c):[(t,u,c) e mult
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 223
225 (t,u,v) e mult
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 224
226 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 225, 215
227 (t,u,v) e n3
Split, 226
228 t e n & u e n & v e n
Split, 226
229 t e n
Split, 228
230 u e n
Split, 228
231 v e n
Split, 228
232 ~s(u)=1
Detach, 222, 230
233 u e n => u+1=s(u)
U Spec, 8
234 u+1=s(u)
Detach, 233, 230
235 ~u+1=1
Substitute, 234, 232
236 u+1=1 & ~u+1=1
Join, 220, 235
237 ~[t=x & u+1=1 & v+t=z]
4 Conclusion, 218
238 (t,u+1,v+t) e mult & ~[t=x & u+1=1 & v+t=z]
Join, 217, 237
239 (t,u+1,v+t) e q
Detach, 204, 238
As Required:
240 ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g+e) e q]
4 Conclusion, 198
241 ALL(b):ALL(c):[(x,b,c) e q
<=> (x,b,c) e mult & ~[x=x & b=1 & c=z]]
U Spec, 155
242 ALL(c):[(x,1,c) e q
<=> (x,1,c) e mult & ~[x=x & 1=1 & c=z]]
U Spec, 241
243 (x,1,z) e q
<=> (x,1,z) e mult & ~[x=x & 1=1 & z=z]
U Spec, 242
244 [(x,1,z) e q => (x,1,z) e mult & ~[x=x & 1=1 & z=z]]
& [(x,1,z) e mult & ~[x=x & 1=1 & z=z] => (x,1,z) e q]
Iff-And, 243
245 (x,1,z) e q => (x,1,z) e mult & ~[x=x & 1=1 & z=z]
Split, 244
246 (x,1,z) e mult & ~[x=x & 1=1 & z=z] => (x,1,z) e q
Split, 244
247 ~[(x,1,z) e mult & ~[x=x & 1=1 & z=z]] => ~(x,1,z) e q
Contra, 245
248 ~~[~(x,1,z) e mult | ~~[x=x & 1=1 & z=z]] => ~(x,1,z) e q
DeMorgan, 247
249 ~(x,1,z) e mult | ~~[x=x & 1=1 & z=z] => ~(x,1,z) e q
Rem DNeg, 248
250 ~(x,1,z) e mult | x=x & 1=1 & z=z => ~(x,1,z) e q
Rem DNeg, 249
251 x=x
Reflex
252 1=1
Reflex
253 z=z
Reflex
254 x=x & 1=1
Join, 251, 252
255 x=x & 1=1 & z=z
Join, 254, 253
256 ~(x,1,z) e mult | x=x & 1=1 & z=z
Arb Or, 255
As Required:
257 ~(x,1,z) e q
Detach, 250, 256
258 q e pn3 & ALL(e):[e e n => (e,1,e) e q]
Join, 177, 197
259 q e pn3 & ALL(e):[e e n => (e,1,e) e q]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g+e) e q]
Join, 258, 240
260 q e pn3 & ALL(e):[e e n => (e,1,e) e q]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q => (e,f+1,g+e) e q]
& ~(x,1,z) e q
Join, 259, 257
261 EXIST(d):[d e pn3 & ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
& ~(x,1,z) e d]
E Gen, 260
262 ~(x,1,z) e n3 | EXIST(d):[d e pn3 & ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
& ~(x,1,z) e d]
Arb Or, 261
263 ~(x,1,z) e mult
Detach, 151, 262
264 (x,1,z) e mult & ~(x,1,z) e mult
Join, 137, 263
265 ~~[(x,1,z) e mult => z=x]
4 Conclusion, 134
266 (x,1,z) e mult => z=x
Rem DNeg, 265
As Required:
267 ALL(a):ALL(c):[a e n & c e n => [(a,1,c) e mult => c=a]]
4 Conclusion, 131
268 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
269 ALL(a1):ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e mult => 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 mult]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e mult & (c1,c2,d2) e mult => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=mult(c1,c2) <=> (c1,c2,d) e mult]]
U Spec, 268
270 ALL(a2):ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e mult => 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 mult]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e mult & (c1,c2,d2) e mult => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=mult(c1,c2) <=> (c1,c2,d) e mult]]
U Spec, 269
271 ALL(b):[ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e mult => 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 mult]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e mult & (c1,c2,d2) e mult => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=mult(c1,c2) <=> (c1,c2,d) e mult]]
U Spec, 270
Sufficient: For functionality of mult
272 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e mult => 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 mult]]
& ALL(c1):ALL(c2):ALL(d1):ALL(d2):[(c1,c2,d1) e mult & (c1,c2,d2) e mult => d1=d2]
=> ALL(c1):ALL(c2):ALL(d):[d=mult(c1,c2) <=> (c1,c2,d) e mult]
U Spec, 271
273 (x,y,z) e mult
Premise
274 ALL(b):ALL(c):[(x,b,c) e mult
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 74
275 ALL(c):[(x,y,c) e mult
=> (x,y,c) e n3 & [x e n & y e n & c e n]]
U Spec, 274
276 (x,y,z) e mult
=> (x,y,z) e n3 & [x e n & y e n & z e n]
U Spec, 275
277 (x,y,z) e n3 & [x e n & y e n & z e n]
Detach, 276, 273
278 (x,y,z) e n3
Split, 277
279 x e n & y e n & z e n
Split, 277
Functionality of mult: Part 1
280 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e mult => c1 e n & c2 e n & d e n]
4 Conclusion, 273
281 x e n
Premise
282 EXIST(sub):[Set(sub) & ALL(b):[b e sub <=> b e n & EXIST(c):[c e n & (x,b,c) e mult]]]
Subset, 1
283 Set(p) & ALL(b):[b e p <=> b e n & EXIST(c):[c e n & (x,b,c) e mult]]
E Spec, 282
Define: p
*********
284 Set(p)
Split, 283
285 ALL(b):[b e p <=> b e n & EXIST(c):[c e n & (x,b,c) e mult]]
Split, 283
286 Set(p) & ALL(b):[b e p => b e n]
=> [1 e p & ALL(b):[b e p => s(b) e p]
=> ALL(b):[b e n => b e p]]
U Spec, 6
287 t e p
Premise
288 t e p <=> t e n & EXIST(c):[c e n & (x,t,c) e mult]
U Spec, 285
289 [t e p => t e n & EXIST(c):[c e n & (x,t,c) e mult]]
& [t e n & EXIST(c):[c e n & (x,t,c) e mult] => t e p]
Iff-And, 288
290 t e p => t e n & EXIST(c):[c e n & (x,t,c) e mult]
Split, 289
291 t e n & EXIST(c):[c e n & (x,t,c) e mult] => t e p
Split, 289
292 t e n & EXIST(c):[c e n & (x,t,c) e mult]
Detach, 290, 287
293 t e n
Split, 292
As Required:
294 ALL(b):[b e p => b e n]
4 Conclusion, 287
295 Set(p) & ALL(b):[b e p => b e n]
Join, 284, 294
Sufficient: ALL(b):[b e n => b e p]
296 1 e p & ALL(b):[b e p => s(b) e p]
=> ALL(b):[b e n => b e p]
Detach, 286, 295
297 1 e p <=> 1 e n & EXIST(c):[c e n & (x,1,c) e mult]
U Spec, 285
298 [1 e p => 1 e n & EXIST(c):[c e n & (x,1,c) e mult]]
& [1 e n & EXIST(c):[c e n & (x,1,c) e mult] => 1 e p]
Iff-And, 297
299 1 e p => 1 e n & EXIST(c):[c e n & (x,1,c) e mult]
Split, 298
Sufficient: 1 e p
300 1 e n & EXIST(c):[c e n & (x,1,c) e mult] => 1 e p
Split, 298
301 x e n => (x,1,x) e mult
U Spec, 55
302 (x,1,x) e mult
Detach, 301, 281
303 x e n & (x,1,x) e mult
Join, 281, 302
304 EXIST(c):[c e n & (x,1,c) e mult]
E Gen, 303
305 1 e n & EXIST(c):[c e n & (x,1,c) e mult]
Join, 2, 304
As Required:
306 1 e p
Detach, 300, 305
Suppose...
307 y e p
Premise
308 s(y) e p <=> s(y) e n & EXIST(c):[c e n & (x,s(y),c) e mult]
U Spec, 285
309 [s(y) e p => s(y) e n & EXIST(c):[c e n & (x,s(y),c) e mult]]
& [s(y) e n & EXIST(c):[c e n & (x,s(y),c) e mult] => s(y) e p]
Iff-And, 308
310 s(y) e p => s(y) e n & EXIST(c):[c e n & (x,s(y),c) e mult]
Split, 309
Sufficient: For s(y) e p
311 s(y) e n & EXIST(c):[c e n & (x,s(y),c) e mult] => s(y) e p
Split, 309
312 y e p <=> y e n & EXIST(c):[c e n & (x,y,c) e mult]
U Spec, 285
313 [y e p => y e n & EXIST(c):[c e n & (x,y,c) e mult]]
& [y e n & EXIST(c):[c e n & (x,y,c) e mult] => y e p]
Iff-And, 312
314 y e p => y e n & EXIST(c):[c e n & (x,y,c) e mult]
Split, 313
315 y e n & EXIST(c):[c e n & (x,y,c) e mult] => y e p
Split, 313
316 y e n & EXIST(c):[c e n & (x,y,c) e mult]
Detach, 314, 307
317 y e n
Split, 316
318 EXIST(c):[c e n & (x,y,c) e mult]
Split, 316
319 z e n & (x,y,z) e mult
E Spec, 318
320 z e n
Split, 319
321 y e n => s(y) e n
U Spec, 3
322 s(y) e n
Detach, 321, 317
323 (x,y,z) e mult
Split, 319
324 ALL(b):ALL(c):[(x,b,c) e mult => (x,b+1,c+x) e mult]
U Spec, 130
325 ALL(c):[(x,y,c) e mult => (x,y+1,c+x) e mult]
U Spec, 324
326 (x,y,z) e mult => (x,y+1,z+x) e mult
U Spec, 325
327 (x,y+1,z+x) e mult
Detach, 326, 323
328 y e n => y+1=s(y)
U Spec, 8
329 y+1=s(y)
Detach, 328, 317
330 (x,s(y),z+x) e mult
Substitute, 329, 327
331 ALL(b):[z e n & b e n => z+b e n]
U Spec, 7
332 z e n & x e n => z+x e n
U Spec, 331
333 z e n & x e n
Join, 320, 281
334 z+x e n
Detach, 332, 333
335 z+x e n & (x,s(y),z+x) e mult
Join, 334, 330
336 EXIST(c):[c e n & (x,s(y),c) e mult]
E Gen, 335
337 s(y) e n & EXIST(c):[c e n & (x,s(y),c) e mult]
Join, 322, 336
338 s(y) e p
Detach, 311, 337
As Required:
339 ALL(b):[b e p => s(b) e p]
4 Conclusion, 307
340 1 e p & ALL(b):[b e p => s(b) e p]
Join, 306, 339
341 ALL(b):[b e n => b e p]
Detach, 296, 340
342 y e n
Premise
343 y e n => y e p
U Spec, 341
344 y e p
Detach, 343, 342
345 y e p <=> y e n & EXIST(c):[c e n & (x,y,c) e mult]
U Spec, 285
346 [y e p => y e n & EXIST(c):[c e n & (x,y,c) e mult]]
& [y e n & EXIST(c):[c e n & (x,y,c) e mult] => y e p]
Iff-And, 345
347 y e p => y e n & EXIST(c):[c e n & (x,y,c) e mult]
Split, 346
348 y e n & EXIST(c):[c e n & (x,y,c) e mult] => y e p
Split, 346
349 y e n & EXIST(c):[c e n & (x,y,c) e mult]
Detach, 347, 344
350 y e n
Split, 349
351 EXIST(c):[c e n & (x,y,c) e mult]
Split, 349
352 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e mult]]
4 Conclusion, 342
As Required:
353 ALL(a):[a e n
=> ALL(b):[b e n => EXIST(c):[c e n & (a,b,c) e mult]]]
4 Conclusion, 281
354 x e n & y e n
Premise
355 x e n
Split, 354
356 y e n
Split, 354
357 x e n
=> ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e mult]]
U Spec, 353
358 ALL(b):[b e n => EXIST(c):[c e n & (x,b,c) e mult]]
Detach, 357, 355
359 y e n => EXIST(c):[c e n & (x,y,c) e mult]
U Spec, 358
360 EXIST(c):[c e n & (x,y,c) e mult]
Detach, 359, 356
Functionality of mult: Part 2
361 ALL(a):ALL(b):[a e n & b e n => EXIST(c):[c e n & (a,b,c) e mult]]
4 Conclusion, 354
362 x e n
Premise
363
EXIST(sub):[Set(sub)
& ALL(b):[b e
sub <=> b
e n
& ALL(c1):ALL(c2):[(x,b,c1)
e mult
& (x,b,c2)
e mult
=> c1=c2]]]
Subset, 1
364
Set(p')
& ALL(b):[b e
p'
<=> b e
n
& ALL(c1):ALL(c2):[(x,b,c1)
e mult
& (x,b,c2)
e mult
=> c1=c2]]
E Spec, 363
Define: p'
365 Set(p')
Split, 364
366 ALL(b):[b e p' <=> b e n & ALL(c1):ALL(c2):[(x,b,c1) e mult & (x,b,c2) e mult => c1=c2]]
Split, 364
367 Set(p') & ALL(b):[b e p' => b e n]
=> [1 e p' & ALL(b):[b e p' => s(b) e p']
=> ALL(b):[b e n => b e p']]
U Spec, 6
368 t e p'
Premise
369 t e p' <=> t e n & ALL(c1):ALL(c2):[(x,t,c1) e mult & (x,t,c2) e mult => c1=c2]
U Spec, 366
370 [t e p' => t e n & ALL(c1):ALL(c2):[(x,t,c1) e mult & (x,t,c2) e mult => c1=c2]]
& [t e n & ALL(c1):ALL(c2):[(x,t,c1) e mult & (x,t,c2) e mult => c1=c2] => t e p']
Iff-And, 369
371 t e p' => t e n & ALL(c1):ALL(c2):[(x,t,c1) e mult & (x,t,c2) e mult => c1=c2]
Split, 370
372 t e n & ALL(c1):ALL(c2):[(x,t,c1) e mult & (x,t,c2) e mult => c1=c2] => t e p'
Split, 370
373 t e n & ALL(c1):ALL(c2):[(x,t,c1) e mult & (x,t,c2) e mult => c1=c2]
Detach, 371, 368
374 t e n
Split, 373
375 ALL(b):[b e p' => b e n]
4 Conclusion, 368
376 Set(p') & ALL(b):[b e p' => b e n]
Join, 365, 375
Sufficient: For ALL(b):[b e n => b e p']
377 1 e p' & ALL(b):[b e p' => s(b) e p']
=> ALL(b):[b e n => b e p']
Detach, 367, 376
378 1 e p' <=> 1 e n & ALL(c1):ALL(c2):[(x,1,c1) e mult & (x,1,c2) e mult => c1=c2]
U Spec, 366
379 [1 e p' => 1 e n & ALL(c1):ALL(c2):[(x,1,c1) e mult & (x,1,c2) e mult => c1=c2]]
& [1 e n & ALL(c1):ALL(c2):[(x,1,c1) e mult & (x,1,c2) e mult => c1=c2] => 1 e p']
Iff-And, 378
380 1 e p' => 1 e n & ALL(c1):ALL(c2):[(x,1,c1) e mult & (x,1,c2) e mult => c1=c2]
Split, 379
Sufficient: For 1 e p'
381 1 e n & ALL(c1):ALL(c2):[(x,1,c1) e mult & (x,1,c2) e mult => c1=c2] => 1 e p'
Split, 379
382 (x,1,z1) e mult & (x,1,z2) e mult
Premise
383 (x,1,z1) e mult
Split, 382
384 (x,1,z2) e mult
Split, 382
385 ALL(c):[x e n & c e n => [(x,1,c) e mult => c=x]]
U Spec, 267
386 x e n & z1 e n => [(x,1,z1) e mult => z1=x]
U Spec, 385
387 x e n & z2 e n => [(x,1,z2) e mult => z2=x]
U Spec, 385
388 ALL(b):ALL(c):[(x,b,c) e mult
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 74
389 ALL(c):[(x,1,c) e mult
=> (x,1,c) e n3 & [x e n & 1 e n & c e n]]
U Spec, 388
390 (x,1,z1) e mult
=> (x,1,z1) e n3 & [x e n & 1 e n & z1 e n]
U Spec, 389
391 (x,1,z1) e n3 & [x e n & 1 e n & z1 e n]
Detach, 390, 383
392 (x,1,z1) e n3
Split, 391
393 x e n & 1 e n & z1 e n
Split, 391
394 x e n
Split, 393
395 1 e n
Split, 393
396 z1 e n
Split, 393
397 (x,1,z2) e mult
=> (x,1,z2) e n3 & [x e n & 1 e n & z2 e n]
U Spec, 389
398 (x,1,z2) e n3 & [x e n & 1 e n & z2 e n]
Detach, 397, 384
399 (x,1,z2) e n3
Split, 398
400 x e n & 1 e n & z2 e n
Split, 398
401 x e n
Split, 400
402 1 e n
Split, 400
403 z2 e n
Split, 400
404 x e n & z1 e n
Join, 362, 396
405 (x,1,z1) e mult => z1=x
Detach, 386, 404
406 z1=x
Detach, 405, 383
407 x e n & z2 e n
Join, 362, 403
408 (x,1,z2) e mult => z2=x
Detach, 387, 407
409 z2=x
Detach, 408, 384
410 z1=z2
Substitute, 409, 406
411 ALL(c1):ALL(c2):[(x,1,c1) e mult & (x,1,c2) e mult => c1=c2]
4 Conclusion, 382
412 1 e n
& ALL(c1):ALL(c2):[(x,1,c1) e mult & (x,1,c2) e mult => c1=c2]
Join, 2, 411
As Required:
413 1 e p'
Detach, 381, 412
414 y e p'
Premise
415 y e p' <=> y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
U Spec, 366
416 [y e p' => y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]]
& [y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2] => y e p']
Iff-And, 415
417 y e p' => y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
Split, 416
418 y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2] => y e p'
Split, 416
419 y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
Detach, 417, 414
420 y e n
Split, 419
Product of x and y is unique
421 ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
Split, 419
422
s(y)
e p'
<=> s(y)
e n
& ALL(c1):ALL(c2):[(x,s(y),c1)
e mult
& (x,s(y),c2)
e mult
=> c1=c2]
U Spec, 366
423
[s(y)
e p'
=> s(y)
e n
& ALL(c1):ALL(c2):[(x,s(y),c1)
e mult
& (x,s(y),c2)
e mult
=> c1=c2]]
& [s(y)
e n
& ALL(c1):ALL(c2):[(x,s(y),c1)
e mult
& (x,s(y),c2)
e mult
=> c1=c2]
=> s(y)
e p']
Iff-And, 422
424
s(y)
e p'
=> s(y)
e n
& ALL(c1):ALL(c2):[(x,s(y),c1)
e mult
& (x,s(y),c2)
e mult
=> c1=c2]
Split, 423
Sufficient: For s(y) e p'
425
s(y)
e n
& ALL(c1):ALL(c2):[(x,s(y),c1)
e mult
& (x,s(y),c2)
e mult
=> c1=c2]
=> s(y)
e p'
Split, 423
426 y e n => s(y) e n
U Spec, 3
As Required:
427 s(y) e n
Detach, 426, 420
428 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e mult]]
U Spec, 361
429 x e n & y e n => EXIST(c):[c e n & (x,y,c) e mult]
U Spec, 428
430 x e n & y e n
Join, 362, 420
431 EXIST(c):[c e n & (x,y,c) e mult]
Detach, 429, 430
432 z e n & (x,y,z) e mult
E Spec, 431
Define: z
433 z e n
Split, 432
434 (x,y,z) e mult
Split, 432
435 z' e n
Premise
436 ALL(c2):[(x,y,z) e mult & (x,y,c2) e mult => z=c2]
U Spec, 421
437 (x,y,z) e mult & (x,y,z') e mult => z=z'
U Spec, 436
438 (x,y,z') e mult
Premise
439 (x,y,z) e mult & (x,y,z') e mult
Join, 434, 438
440 z=z'
Detach, 437, 439
441 (x,y,z') e mult => z=z'
4 Conclusion, 438
As Required:
442 ALL(c):[c e n => [(x,y,c) e mult => z=c]]
4 Conclusion, 435
Suppose...
443 z' e n
Premise
Suppose to the contrary...
444 ~[(x,s(y),z') e mult => z'=z+x]
Premise
445 ~~[(x,s(y),z') e mult & ~z'=z+x]
Imply-And, 444
446 (x,s(y),z') e mult & ~z'=z+x
Rem DNeg, 445
447 (x,s(y),z') e mult
Split, 446
448 ~z'=z+x
Split, 446
449 ALL(b):ALL(c):[(x,b,c) e mult
<=> (x,b,c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) 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
450 ALL(c):[(x,s(y),c) e mult
<=> (x,s(y),c) e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),c) e d]]
U Spec, 449
451 (x,s(y),z') e mult
<=> (x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d]
U Spec, 450
452 [(x,s(y),z') e mult => (x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d]]
& [(x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d] => (x,s(y),z') e mult]
Iff-And, 451
453 (x,s(y),z') e mult => (x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d]
Split, 452
454 (x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d] => (x,s(y),z') e mult
Split, 452
455 ~[(x,s(y),z') e n3 & ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d]] => ~(x,s(y),z') e mult
Contra, 453
456 ~~[~(x,s(y),z') e n3 | ~ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d]] => ~(x,s(y),z') e mult
DeMorgan, 455
457 ~(x,s(y),z') e n3 | ~ALL(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d] => ~(x,s(y),z') e mult
Rem DNeg, 456
458 ~(x,s(y),z') e n3 | ~~EXIST(d):~[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d] => ~(x,s(y),z') e mult
Quant, 457
459 ~(x,s(y),z') e n3 | EXIST(d):~[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
=> (x,s(y),z') e d] => ~(x,s(y),z') e mult
Rem DNeg, 458
460 ~(x,s(y),z') e n3 | EXIST(d):~~[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g)
e d => (e,f+1,g+e)
e d] & ~(x,s(y),z')
e d]
=> ~(x,s(y),z')
e mult
Imply-And, 459
Sufficient: For ~(x,s(y),z') e mult to obtain contradiction
461 ~(x,s(y),z') e n3 | EXIST(d):[d e pn3
& ALL(e):[e e n => (e,1,e) e d]
&
ALL(e):ALL(f):ALL(g):[(e,f,g)
e d => (e,f+1,g+e)
e d] & ~(x,s(y),z')
e d]
=> ~(x,s(y),z')
e mult
Rem DNeg, 460
462 EXIST(sub):[Set''(sub) & ALL(a):ALL(b):ALL(c):[(a,b,c) e sub
<=> (a,b,c) e mult & ~[a=x & b=s(y) & c=z']]]
Subset, 28
463 Set''(q') & ALL(a):ALL(b):ALL(c):[(a,b,c) e q'
<=> (a,b,c) e mult & ~[a=x & b=s(y) & c=z']]
E Spec, 462
Define: q'
464 Set''(q')
Split, 463
465 ALL(a):ALL(b):ALL(c):[(a,b,c) e q'
<=> (a,b,c) e mult & ~[a=x & b=s(y) & c=z']]
Split, 463
466
q'
e pn3
<=> Set''(q')
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3)
e q'
=> (d1,d2,d3) e
n3]
U Spec, 25
467
[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, 466
468
q'
e pn3
=> Set''(q')
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3)
e q'
=> (d1,d2,d3) e
n3]
Split, 467
469
Set''(q')
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3)
e q'
=> (d1,d2,d3) e
n3]
=> q'
e pn3
Split, 467
470 (t,u,v) e q'
Premise
471 ALL(b):ALL(c):[(t,b,c) e q'
<=> (t,b,c) e mult & ~[t=x & b=s(y) & c=z']]
U Spec, 465
472 ALL(c):[(t,u,c) e q'
<=> (t,u,c) e mult & ~[t=x & u=s(y) & c=z']]
U Spec, 471
473 (t,u,v) e q'
<=> (t,u,v) e mult & ~[t=x & u=s(y) & v=z']
U Spec, 472
474 [(t,u,v) e q' => (t,u,v) e mult & ~[t=x & u=s(y) & v=z']]
& [(t,u,v) e mult & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q']
Iff-And, 473
475 (t,u,v) e q' => (t,u,v) e mult & ~[t=x & u=s(y) & v=z']
Split, 474
476 (t,u,v) e mult & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q'
Split, 474
477 (t,u,v) e mult & ~[t=x & u=s(y) & v=z']
Detach, 475, 470
478 (t,u,v) e mult
Split, 477
479 ~[t=x & u=s(y) & v=z']
Split, 477
480 ALL(b):ALL(c):[(t,b,c) e mult
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 74
481 ALL(c):[(t,u,c) e mult
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 480
482 (t,u,v) e mult
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 481
483 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 482, 478
484 (t,u,v) e n3
Split, 483
485 ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q' => (d1,d2,d3) e n3]
4 Conclusion, 470
486 Set''(q')
& ALL(d1):ALL(d2):ALL(d3):[(d1,d2,d3) e q' => (d1,d2,d3) e n3]
Join, 464, 485
As Required:
487 q' e pn3
Detach, 469, 486
488 t e n
Premise
489 ALL(b):ALL(c):[(t,b,c) e q'
<=> (t,b,c) e mult & ~[t=x & b=s(y) & c=z']]
U Spec, 465
490 ALL(c):[(t,1,c) e q'
<=> (t,1,c) e mult & ~[t=x & 1=s(y) & c=z']]
U Spec, 489
491 (t,1,t) e q'
<=> (t,1,t) e mult & ~[t=x & 1=s(y) & t=z']
U Spec, 490
492 [(t,1,t) e q' => (t,1,t) e mult & ~[t=x & 1=s(y) & t=z']]
& [(t,1,t) e mult & ~[t=x & 1=s(y) & t=z'] => (t,1,t) e q']
Iff-And, 491
493 (t,1,t) e q' => (t,1,t) e mult & ~[t=x & 1=s(y) & t=z']
Split, 492
494 (t,1,t) e mult & ~[t=x & 1=s(y) & t=z'] => (t,1,t) e q'
Split, 492
495 t e n => (t,1,t) e mult
U Spec, 55
496 (t,1,t) e mult
Detach, 495, 488
497 t=x & 1=s(y) & t=z'
Premise
498 t=x
Split, 497
499 1=s(y)
Split, 497
500 t=z'
Split, 497
501 y e n => ~s(y)=1
U Spec, 5
502 ~s(y)=1
Detach, 501, 420
503 s(y)=1
Sym, 499
504 s(y)=1 & ~s(y)=1
Join, 503, 502
505 ~[t=x & 1=s(y) & t=z']
4 Conclusion, 497
506 (t,1,t) e mult & ~[t=x & 1=s(y) & t=z']
Join, 496, 505
507 (t,1,t) e q'
Detach, 494, 506
As Required:
508 ALL(e):[e e n => (e,1,e) e q']
4 Conclusion, 488
509 (t,u,v) e q'
Premise
510 ALL(b):ALL(c):[(t,b,c) e q'
<=> (t,b,c) e mult & ~[t=x & b=s(y) & c=z']]
U Spec, 465
511 ALL(c):[(t,u,c) e q'
<=> (t,u,c) e mult & ~[t=x & u=s(y) & c=z']]
U Spec, 510
512 (t,u,v) e q'
<=> (t,u,v) e mult & ~[t=x & u=s(y) & v=z']
U Spec, 511
513 [(t,u,v) e q' => (t,u,v) e mult & ~[t=x & u=s(y) & v=z']]
& [(t,u,v) e mult & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q']
Iff-And, 512
514 (t,u,v) e q' => (t,u,v) e mult & ~[t=x & u=s(y) & v=z']
Split, 513
515 (t,u,v) e mult & ~[t=x & u=s(y) & v=z'] => (t,u,v) e q'
Split, 513
516 (t,u,v) e mult & ~[t=x & u=s(y) & v=z']
Detach, 514, 509
517 (t,u,v) e mult
Split, 516
518 ~[t=x & u=s(y) & v=z']
Split, 516
519 ALL(b):ALL(c):[(t,b,c) e mult
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 74
520 ALL(c):[(t,u,c) e mult
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 519
521 (t,u,v) e mult
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 520
522 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 521, 517
523 (t,u,v) e n3
Split, 522
524 t e n & u e n & v e n
Split, 522
525 t e n
Split, 524
526 u e n
Split, 524
527 v e n
Split, 524
528 ALL(b):ALL(c):[(t,b,c) e q'
<=> (t,b,c) e mult & ~[t=x & b=s(y) & c=z']]
U Spec, 465
529 ALL(c):[(t,s(u),c) e q'
<=> (t,s(u),c) e mult & ~[t=x & s(u)=s(y) & c=z']]
U Spec, 528
530 (t,s(u),v+t) e q'
<=> (t,s(u),v+t) e mult & ~[t=x & s(u)=s(y) & v+t=z']
U Spec, 529
531
[(t,s(u),v+t)
e q'
=> (t,s(u),v+t)
e mult
& ~[t=x
& s(u)=s(y)
& v+t=z']]
& [(t,s(u),v+t)
e mult
& ~[t=x
& s(u)=s(y)
& v+t=z']
=> (t,s(u),v+t)
e q']
Iff-And, 530
532 (t,s(u),v+t) e q' => (t,s(u),v+t) e mult & ~[t=x & s(u)=s(y) & v+t=z']
Split, 531
Sufficient: (t,s(u),v+t) e q'
533 (t,s(u),v+t) e mult & ~[t=x & s(u)=s(y) & v+t=z'] => (t,s(u),v+t) e q'
Split, 531
534 ALL(b):ALL(c):[(t,b,c) e mult => (t,b+1,c+t) e mult]
U Spec, 130
535 ALL(c):[(t,u,c) e mult => (t,u+1,c+t) e mult]
U Spec, 534
536 (t,u,v) e mult => (t,u+1,v+t) e mult
U Spec, 535
537 (t,u+1,v+t) e mult
Detach, 536, 517
538 u e n => u+1=s(u)
U Spec, 8
539 u+1=s(u)
Detach, 538, 526
540 (t,s(u),v+t) e mult
Substitute, 539, 537
See line 539
541 t=x & s(u)=s(y) & v+t=z'
Premise
542 t=x
Split, 541
543 s(u)=s(y)
Split, 541
544 v+t=z'
Split, 541
545 ALL(b):[u e n & b e n => [s(u)=s(b) => u=b]]
U Spec, 4
546 u e n & y e n => [s(u)=s(y) => u=y]
U Spec, 545
547 ALL(b):ALL(c):[(t,b,c) e mult
=> (t,b,c) e n3 & [t e n & b e n & c e n]]
U Spec, 74
548 ALL(c):[(t,u,c) e mult
=> (t,u,c) e n3 & [t e n & u e n & c e n]]
U Spec, 547
549 (t,u,v) e mult
=> (t,u,v) e n3 & [t e n & u e n & v e n]
U Spec, 548
550 (t,u,v) e n3 & [t e n & u e n & v e n]
Detach, 549, 517
551 (t,u,v) e n3
Split, 550
552 t e n & u e n & v e n
Split, 550
553 t e n
Split, 552
554 u e n
Split, 552
555 v e n
Split, 552
556 u e n & y e n
Join, 554, 420
557 s(u)=s(y) => u=y
Detach, 546, 556
558 u=y
Detach, 557, 543
559 (x,u,v) e mult
Substitute, 542, 517
560 (x,y,v) e mult
Substitute, 558, 559
561 v e n => [(x,y,v) e mult => z=v]
U Spec, 442
562 (x,y,v) e mult => z=v
Detach, 561, 555
563 z=v
Detach, 562, 560
564 z+t=z'
Substitute, 563, 544
565 z+x=z'
Substitute, 542, 564
566 z'=z+x
Sym, 565
567 z'=z+x & ~z'=z+x
Join, 566, 448
568 ~[t=x & s(u)=s(y) & v+t=z']
4 Conclusion, 541
569 (t,s(u),v+t) e mult & ~[t=x & s(u)=s(y) & v+t=z']
Join, 540, 568
570 (t,s(u),v+t) e q'
Detach, 533, 569
571 (t,u+1,v+t) e q'
Substitute, 539, 570
572 ALL(e):ALL(f):ALL(g):[(e,f,g) e q' => (e,f+1,g+e) e q']
4 Conclusion, 509
573 ALL(b):ALL(c):[(x,b,c) e q'
<=> (x,b,c) e mult & ~[x=x & b=s(y) & c=z']]
U Spec, 465
574 ALL(c):[(x,s(y),c) e q'
<=> (x,s(y),c) e mult & ~[x=x & s(y)=s(y) & c=z']]
U Spec, 573
575 (x,s(y),z') e q'
<=> (x,s(y),z') e mult & ~[x=x & s(y)=s(y) & z'=z']
U Spec, 574
576 [(x,s(y),z') e q' => (x,s(y),z') e mult & ~[x=x & s(y)=s(y) & z'=z']]
& [(x,s(y),z') e mult & ~[x=x & s(y)=s(y) & z'=z'] => (x,s(y),z') e q']
Iff-And, 575
577 (x,s(y),z') e q' => (x,s(y),z') e mult & ~[x=x & s(y)=s(y) & z'=z']
Split, 576
578 (x,s(y),z') e mult & ~[x=x & s(y)=s(y) & z'=z'] => (x,s(y),z') e q'
Split, 576
579 ~[(x,s(y),z') e mult & ~[x=x & s(y)=s(y) & z'=z']] => ~(x,s(y),z') e q'
Contra, 577
580 ~~[~(x,s(y),z') e mult | ~~[x=x & s(y)=s(y) & z'=z']] => ~(x,s(y),z') e q'
DeMorgan, 579
581 ~(x,s(y),z') e mult | ~~[x=x & s(y)=s(y) & z'=z'] => ~(x,s(y),z') e q'
Rem DNeg, 580
582 ~(x,s(y),z') e mult | x=x & s(y)=s(y) & z'=z' => ~(x,s(y),z') e q'
Rem DNeg, 581
583 x=x
Reflex
584 s(y)=s(y)
Reflex
585 z'=z'
Reflex
586 x=x & s(y)=s(y)
Join, 583, 584
587 x=x & s(y)=s(y) & z'=z'
Join, 586, 585
588 ~(x,s(y),z') e mult | x=x & s(y)=s(y) & z'=z'
Arb Or, 587
As Required:
589 ~(x,s(y),z') e q'
Detach, 582, 588
590 q' e pn3 & ALL(e):[e e n => (e,1,e) e q']
Join, 487, 508
591 q' e pn3 & ALL(e):[e e n => (e,1,e) e q']
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q' => (e,f+1,g+e) e q']
Join, 590, 572
592 q' e pn3 & ALL(e):[e e n => (e,1,e) e q']
& ALL(e):ALL(f):ALL(g):[(e,f,g) e q' => (e,f+1,g+e) e q']
& ~(x,s(y),z') e q'
Join, 591, 589
593 EXIST(d):[d e pn3 & ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
& ~(x,s(y),z') e d]
E Gen, 592
594 ~(x,s(y),z') e n3 | EXIST(d):[d e pn3 & ALL(e):[e e n => (e,1,e) e d]
& ALL(e):ALL(f):ALL(g):[(e,f,g) e d => (e,f+1,g+e) e d]
& ~(x,s(y),z') e d]
Arb Or, 593
595 ~(x,s(y),z') e mult
Detach, 461, 594
596 (x,s(y),z') e mult & ~(x,s(y),z') e mult
Join, 447, 595
597 ~~[(x,s(y),z') e mult => z'=z+x]
4 Conclusion, 444
598 (x,s(y),z') e mult => z'=z+x
Rem DNeg, 597
599 ALL(d):[d e n => [(x,s(y),d) e mult => d=z+x]]
4 Conclusion, 443
600 (x,s(y),z1) e mult & (x,s(y),z2) e mult
Premise
601 (x,s(y),z1) e mult
Split, 600
602 (x,s(y),z2) e mult
Split, 600
603 ALL(b):ALL(c):[(x,b,c) e mult
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 74
604 ALL(c):[(x,s(y),c) e mult
=> (x,s(y),c) e n3 & [x e n & s(y) e n & c e n]]
U Spec, 603
605 (x,s(y),z1) e mult
=> (x,s(y),z1) e n3 & [x e n & s(y) e n & z1 e n]
U Spec, 604
606 (x,s(y),z1) e n3 & [x e n & s(y) e n & z1 e n]
Detach, 605, 601
607 (x,s(y),z1) e n3
Split, 606
608 x e n & s(y) e n & z1 e n
Split, 606
609 x e n
Split, 608
610 s(y) e n
Split, 608
611 z1 e n
Split, 608
612 (x,s(y),z2) e mult
=> (x,s(y),z2) e n3 & [x e n & s(y) e n & z2 e n]
U Spec, 604
613 (x,s(y),z2) e n3 & [x e n & s(y) e n & z2 e n]
Detach, 612, 602
614 (x,s(y),z2) e n3
Split, 613
615 x e n & s(y) e n & z2 e n
Split, 613
616 x e n
Split, 615
617 s(y) e n
Split, 615
618 z2 e n
Split, 615
619 z1 e n => [(x,s(y),z1) e mult => z1=z+x]
U Spec, 599
620 (x,s(y),z1) e mult => z1=z+x
Detach, 619, 611
621 z1=z+x
Detach, 620, 601
622 z2 e n => [(x,s(y),z2) e mult => z2=z+x]
U Spec, 599
623 (x,s(y),z2) e mult => z2=z+x
Detach, 622, 618
624 z2=z+x
Detach, 623, 602
625 z1=z2
Substitute, 624, 621
626 ALL(c1):ALL(c2):[(x,s(y),c1) e mult & (x,s(y),c2) e mult => c1=c2]
4 Conclusion, 600
627 s(y) e n
& ALL(c1):ALL(c2):[(x,s(y),c1) e mult & (x,s(y),c2) e mult => c1=c2]
Join, 427, 626
628 s(y) e p'
Detach, 425, 627
As Required:
629 ALL(b):[b e p' => s(b) e p']
4 Conclusion, 414
630 1 e p' & ALL(b):[b e p' => s(b) e p']
Join, 413, 629
As Required:
631 ALL(b):[b e n => b e p']
Detach, 377, 630
632 y e n
Premise
633 y e n => y e p'
U Spec, 631
634 y e p'
Detach, 633, 632
635 y e p' <=> y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
U Spec, 366
636 [y e p' => y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]]
& [y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2] => y e p']
Iff-And, 635
637 y e p' => y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
Split, 636
638 y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2] => y e p'
Split, 636
639 y e n & ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
Detach, 637, 634
640 y e n
Split, 639
641 ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
Split, 639
642 ALL(b):[b e n
=> ALL(c1):ALL(c2):[(x,b,c1) e mult & (x,b,c2) e mult => c1=c2]]
4 Conclusion, 632
643 ALL(a):[a e n
=> ALL(b):[b e n
=> ALL(c1):ALL(c2):[(a,b,c1) e mult & (a,b,c2) e mult => c1=c2]]]
4 Conclusion, 362
644 (x,y,z1) e mult & (x,y,z2) e mult
Premise
645 (x,y,z1) e mult
Split, 644
646 (x,y,z2) e mult
Split, 644
647 ALL(b):ALL(c):[(x,b,c) e mult
=> (x,b,c) e n3 & [x e n & b e n & c e n]]
U Spec, 74
648 ALL(c):[(x,y,c) e mult
=> (x,y,c) e n3 & [x e n & y e n & c e n]]
U Spec, 647
649 (x,y,z1) e mult
=> (x,y,z1) e n3 & [x e n & y e n & z1 e n]
U Spec, 648
650 (x,y,z1) e n3 & [x e n & y e n & z1 e n]
Detach, 649, 645
651 (x,y,z1) e n3
Split, 650
652 x e n & y e n & z1 e n
Split, 650
653 x e n
Split, 652
654 y e n
Split, 652
655 z1 e n
Split, 652
656 (x,y,z2) e mult
=> (x,y,z2) e n3 & [x e n & y e n & z2 e n]
U Spec, 648
657 (x,y,z2) e n3 & [x e n & y e n & z2 e n]
Detach, 656, 646
658 (x,y,z2) e n3
Split, 657
659 x e n & y e n & z2 e n
Split, 657
660 x e n
Split, 659
661 y e n
Split, 659
662 z2 e n
Split, 659
663 x e n
=> ALL(b):[b e n
=> ALL(c1):ALL(c2):[(x,b,c1) e mult & (x,b,c2) e mult => c1=c2]]
U Spec, 643
664 ALL(b):[b e n
=> ALL(c1):ALL(c2):[(x,b,c1) e mult & (x,b,c2) e mult => c1=c2]]
Detach, 663, 653
665 y e n
=> ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
U Spec, 664
666 ALL(c1):ALL(c2):[(x,y,c1) e mult & (x,y,c2) e mult => c1=c2]
Detach, 665, 654
667 ALL(c2):[(x,y,z1) e mult & (x,y,c2) e mult => z1=c2]
U Spec, 666
668 (x,y,z1) e mult & (x,y,z2) e mult => z1=z2
U Spec, 667
669 z1=z2
Detach, 668, 644
Functionality of mult: Part 3
670 ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e mult & (a,b,c2) e mult => c1=c2]
4 Conclusion, 644
671 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e mult => 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 mult]]
Join, 280, 361
672 ALL(c1):ALL(c2):ALL(d):[(c1,c2,d) e mult => 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 mult]]
& ALL(a):ALL(b):ALL(c1):ALL(c2):[(a,b,c1) e mult & (a,b,c2) e mult => c1=c2]
Join, 671, 670
mult is a function
As Required:
673 ALL(c1):ALL(c2):ALL(d):[d=mult(c1,c2) <=> (c1,c2,d) e mult]
Detach, 272, 672
674 x e n & y e n
Premise
675 x e n
Split, 674
676 y e n
Split, 674
677 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e mult]]
U Spec, 361
678 x e n & y e n => EXIST(c):[c e n & (x,y,c) e mult]
U Spec, 677
679 EXIST(c):[c e n & (x,y,c) e mult]
Detach, 678, 674
680 z e n & (x,y,z) e mult
E Spec, 679
681 z e n
Split, 680
682 (x,y,z) e mult
Split, 680
683 ALL(c2):ALL(d):[d=mult(x,c2) <=> (x,c2,d) e mult]
U Spec, 673
684 ALL(d):[d=mult(x,y) <=> (x,y,d) e mult]
U Spec, 683
685 z=mult(x,y) <=> (x,y,z) e mult
U Spec, 684
686 [z=mult(x,y) => (x,y,z) e mult]
& [(x,y,z) e mult => z=mult(x,y)]
Iff-And, 685
687 z=mult(x,y) => (x,y,z) e mult
Split, 686
688 (x,y,z) e mult => z=mult(x,y)
Split, 686
689 z=mult(x,y)
Detach, 688, 682
690 mult(x,y) e n
Substitute, 689, 681
691 ALL(a):ALL(b):[a e n & b e n => mult(a,b) e n]
4 Conclusion, 674
692 x e n
Premise
693 x e n => (x,1,x) e mult
U Spec, 55
694 (x,1,x) e mult
Detach, 693, 692
695 ALL(c2):ALL(d):[d=mult(x,c2) <=> (x,c2,d) e mult]
U Spec, 673
696 ALL(d):[d=mult(x,1) <=> (x,1,d) e mult]
U Spec, 695
697 x=mult(x,1) <=> (x,1,x) e mult
U Spec, 696
698 [x=mult(x,1) => (x,1,x) e mult]
& [(x,1,x) e mult => x=mult(x,1)]
Iff-And, 697
699 x=mult(x,1) => (x,1,x) e mult
Split, 698
700 (x,1,x) e mult => x=mult(x,1)
Split, 698
701 x=mult(x,1)
Detach, 700, 694
702 mult(x,1)=x
Sym, 701
As Required:
703 ALL(a):[a e n => mult(a,1)=a]
4 Conclusion, 692
704 x e n & y e n
Premise
705 x e n
Split, 704
706 y e n
Split, 704
707 ALL(b):[x e n & b e n => EXIST(c):[c e n & (x,b,c) e mult]]
U Spec, 361
708 x e n & y e n => EXIST(c):[c e n & (x,y,c) e mult]
U Spec, 707
709 EXIST(c):[c e n & (x,y,c) e mult]
Detach, 708, 704
710 z e n & (x,y,z) e mult
E Spec, 709
711 z e n
Split, 710
712 (x,y,z) e mult
Split, 710
713 ALL(c2):ALL(d):[d=mult(x,c2) <=> (x,c2,d) e mult]
U Spec, 673
714 ALL(d):[d=mult(x,y) <=> (x,y,d) e mult]
U Spec, 713
715 z=mult(x,y) <=> (x,y,z) e mult
U Spec, 714
716 [z=mult(x,y) => (x,y,z) e mult]
& [(x,y,z) e mult => z=mult(x,y)]
Iff-And, 715
717 z=mult(x,y) => (x,y,z) e mult
Split, 716
718 (x,y,z) e mult => z=mult(x,y)
Split, 716
719 z=mult(x,y)
Detach, 718, 712
720 ALL(b):ALL(c):[(x,b,c) e mult => (x,b+1,c+x) e mult]
U Spec, 130
721 ALL(c):[(x,y,c) e mult => (x,y+1,c+x) e mult]
U Spec, 720
722 (x,y,z) e mult => (x,y+1,z+x) e mult
U Spec, 721
723 (x,y+1,z+x) e mult
Detach, 722, 712
724 ALL(c2):ALL(d):[d=mult(x,c2) <=> (x,c2,d) e mult]
U Spec, 673
725 ALL(d):[d=mult(x,y+1) <=> (x,y+1,d) e mult]
U Spec, 724
726 z+x=mult(x,y+1) <=> (x,y+1,z+x) e mult
U Spec, 725
727 [z+x=mult(x,y+1) => (x,y+1,z+x) e mult]
& [(x,y+1,z+x) e mult => z+x=mult(x,y+1)]
Iff-And, 726
728 z+x=mult(x,y+1) => (x,y+1,z+x) e mult
Split, 727
729 (x,y+1,z+x) e mult => z+x=mult(x,y+1)
Split, 727
730 z+x=mult(x,y+1)
Detach, 729, 723
731 mult(x,y)+x=mult(x,y+1)
Substitute, 719, 730
732 mult(x,y+1)=mult(x,y)+x
Sym, 731
As Required:
733 ALL(a):ALL(b):[a e n & b e n => mult(a,b+1)=mult(a,b)+a]
4 Conclusion, 704
734 ALL(a):ALL(b):[a e n & b e n => mult(a,b) e n]
& ALL(a):[a e n => mult(a,1)=a]
Join, 691, 703
735 ALL(a):ALL(b):[a e n & b e n => mult(a,b) e n]
& ALL(a):[a e n => mult(a,1)=a]
& ALL(a):ALL(b):[a e n & b e n => mult(a,b+1)=mult(a,b)+a]
Join, 734, 733
As Required:
736 EXIST(mult):[ALL(a):ALL(b):[a e n & b e n => mult(a,b) e n]
& ALL(a):[a e n => mult(a,1)=a]
& ALL(a):ALL(b):[a e n & b e n => mult(a,b+1)=mult(a,b)+a]]
E Gen, 735