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