Closure of PROD operator
Prove: ALL(f):[ALL(a):[a 
n => f(a) n]
=> ALL(a):ALL(b):[a n & b n & a<=b => PROD(i,a,b):f(i) n]]
Peano's Axioms
1 Set(n)
& 1 n
& ALL(a):[a n => next(a) n]
& ALL(a):[a n => ~next(a)=1]
& ALL(a):ALL(b):[a n & b n & next(a)=next(b) => a=b]
& ALL(a):[Set(a) & 1 a & ALL(b):[b n & b a => next(b) a]
=> ALL(b):[b n => b a]]
Premise
2 Set(n)
Split, 1
3 1 n
Split, 1
4 ALL(a):[a n => next(a) n]
Split, 1
5 ALL(a):[a n => ~next(a)=1]
Split, 1
6 ALL(a):ALL(b):[a n & b n & next(a)=next(b) => a=b]
Split, 1
7 ALL(a):[Set(a) & 1 a & ALL(b):[b n & b a => next(b) a]
=> ALL(b):[b n => b a]]
Split, 1
Define: +
8 ALL(a):ALL(b):[a n & b n => a+b n]
& ALL(a):[a n => a+1=next(a)]
& ALL(a):ALL(b):[a n & b n => a+next(b)=next(a+b)]
Definition
9 ALL(a):ALL(b):[a n & b n => a+b n]
Split, 8
10 ALL(a):[a n => a+1=next(a)]
Split, 8
11 ALL(a):ALL(b):[a n & b n => a+next(b)=next(a+b)]
Split, 8
Define: *
12 ALL(a):ALL(b):[a n & b n => a*b n]
& ALL(a):[a n => a*1=a]
& ALL(a):ALL(b):[a n & b n => a*(b+1)=a*b+a]
Definition
13 ALL(a):ALL(b):[a n & b n => a*b n]
Split, 12
14 ALL(a):[a n => a*1=a]
Split, 12
15 ALL(a):ALL(b):[a n & b n => a*(b+1)=a*b+a]
Split, 12
16 ALL(f):[ALL(a):[a n => f(a) n]
=> ALL(a):[a n => SUM(i,a,a):f(i)=f(a)]
& ALL(a):ALL(b):[a n & b n => SUM(i,a,b+1):f(i)=SUM(i,a,b):f(i)+f(b+1)]]
Definition
Define: <
17 ALL(a):ALL(b):[a n & b n => [a<b <=> EXIST(c):[c n & a+c=b]]]
Definition
Define: <=
18 ALL(a):ALL(b):[a n & b n => [a<=b <=> a<b | a=b]]
Definition
Previous result: + is associative
19 ALL(a):ALL(b):ALL(c):[a n & b n & c n => a+b+c=a+(b+c)]
Premise
Define: f
20 ALL(a):[a n => f(a) n]
Premise
21 ALL(f):[ALL(a):[a n => f(a) n]
=> ALL(a):[a n => PROD(i,a,a):f(i)=f(a)]
& ALL(a):ALL(b):[a n & b n => PROD(i,a,b+1):f(i)=PROD(i,a,b):f(i)*f(b+1)]]
Definition
22 ALL(a):[a n => f(a) n]
=> ALL(a):[a n => PROD(i,a,a):f(i)=f(a)]
& ALL(a):ALL(b):[a n & b n => PROD(i,a,b+1):f(i)=PROD(i,a,b):f(i)*f(b+1)]
U Spec, 21
From the definition of PROD...
23 ALL(a):[a n => PROD(i,a,a):f(i)=f(a)]
& ALL(a):ALL(b):[a n & b n => PROD(i,a,b+1):f(i)=PROD(i,a,b):f(i)*f(b+1)]
Detach, 22, 20
24 ALL(a):[a n => PROD(i,a,a):f(i)=f(a)]
Split, 23
25 ALL(a):ALL(b):[a n & b n => PROD(i,a,b+1):f(i)=PROD(i,a,b):f(i)*f(b+1)]
Split, 23
Prove: x n => ALL(k):[k n => PROD(i,x,x+k):f(i) n]
Suppose...
26 x n
Premise
Sufficient: For ALL(k):[k n => PROD(i,x,x+k):f(i) n]
27 PROD(i,x,x+1):f(i) n
& ALL(k):[k n & PROD(i,x,x+k):f(i) n => PROD(i,x,x+(k+1)):f(i) n]
=> ALL(k):[k n => PROD(i,x,x+k):f(i) n]
Induction
Prove: PROD(i,x,x+1):f(i) n (Induction, Part 1)
Applying the definition of PROD...
28 x n => PROD(i,x,x):f(i)=f(x)
U Spec, 24
29 PROD(i,x,x):f(i)=f(x)
Detach, 28, 26
30 x n => f(x) n
U Spec, 20
31 f(x) n
Detach, 30, 26
32 PROD(i,x,x):f(i) n
Substitute, 29, 31
33 ALL(b):[x n & b n => PROD(i,x,b+1):f(i)=PROD(i,x,b):f(i)*f(b+1)]
U Spec, 25
34 x n & x n => PROD(i,x,x+1):f(i)=PROD(i,x,x):f(i)*f(x+1)
U Spec, 33
35 x n & x n
Join, 26, 26
36 PROD(i,x,x+1):f(i)=PROD(i,x,x):f(i)*f(x+1)
Detach, 34, 35
37 ALL(b):[x n & b n => x+b n]
U Spec, 9
38 x n & 1 n => x+1 n
U Spec, 37
39 x n & 1 n
Join, 26, 3
40 x+1 n
Detach, 38, 39
41 x+1 n => f(x+1) n
U Spec, 20
42 f(x+1) n
Detach, 41, 40
Applying the definition of *...
43 ALL(b):[PROD(i,x,x):f(i) n & b n => PROD(i,x,x):f(i)*b n]
U Spec, 13
44 PROD(i,x,x):f(i) n & f(x+1) n => PROD(i,x,x):f(i)*f(x+1) n
U Spec, 43
45 PROD(i,x,x):f(i) n & f(x+1) n
Join, 32, 42
46 PROD(i,x,x):f(i)*f(x+1) n
Detach, 44, 45
As Required: (Induction, Part 1)
47 PROD(i,x,x+1):f(i) n
Substitute, 36, 46
Prove: y n & PROD(i,x,x+y):f(i) n
=> PROD(i,x,x+(y+1)):f(i) n
(Induction, Part 2)
Suppose...
48 y n & PROD(i,x,x+y):f(i) n
Premise
49 y n
Split, 48
50 PROD(i,x,x+y):f(i) n
Split, 48
Applying the definition of PROD...
51 ALL(b):[x n & b n => PROD(i,x,b+1):f(i)=PROD(i,x,b):f(i)*f(b+1)]
U Spec, 25
52 x n & x+y n => PROD(i,x,x+y+1):f(i)=PROD(i,x,x+y):f(i)*f(x+y+1)
U Spec, 51
53 ALL(b):[x n & b n => x+b n]
U Spec, 9
54 x n & y n => x+y n
U Spec, 53
55 x n & y n
Join, 26, 49
56 x+y n
Detach, 54, 55
57 x n & y n
Join, 26, 49
58 x+y n
Detach, 54, 57
59 x n & x+y n
Join, 26, 58
60 PROD(i,x,x+y+1):f(i)=PROD(i,x,x+y):f(i)*f(x+y+1)
Detach, 52, 59
61 x+y+1 n => f(x+y+1) n
U Spec, 20
Applying the definition of +
62 ALL(b):[x+y n & b n => x+y+b n]
U Spec, 9
63 x+y n & 1 n => x+y+1 n
U Spec, 62
64 x+y n & 1 n
Join, 58, 3
65 x+y+1 n
Detach, 63, 64
66 f(x+y+1) n
Detach, 61, 65
Applying the definition of *
67 ALL(b):[PROD(i,x,x+y):f(i) n & b n => PROD(i,x,x+y):f(i)*b n]
U Spec, 13
68 PROD(i,x,x+y):f(i) n & f(x+y+1) n => PROD(i,x,x+y):f(i)*f(x+y+1) n
U Spec, 67
69 PROD(i,x,x+y):f(i) n & f(x+y+1) n
Join, 50, 66
70 PROD(i,x,x+y):f(i)*f(x+y+1) n
Detach, 68, 69
71 PROD(i,x,x+y+1):f(i) n
Substitute, 60, 70
Applying associativity of +...
72 ALL(b):ALL(c):[x n & b n & c n => x+b+c=x+(b+c)]
U Spec, 19
73 ALL(c):[x n & y n & c n => x+y+c=x+(y+c)]
U Spec, 72
74 x n & y n & 1 n => x+y+1=x+(y+1)
U Spec, 73
75 x n & y n & 1 n
Join, 57, 3
76 x+y+1=x+(y+1)
Detach, 74, 75
77 PROD(i,x,x+(y+1)):f(i) n
Substitute, 76, 71
As Required:
78 y n & PROD(i,x,x+y):f(i) n
=> PROD(i,x,x+(y+1)):f(i) n
Conclusion, 48
As Required: (Induction, Part 2)
79 ALL(k):[k n & PROD(i,x,x+k):f(i) n
=> PROD(i,x,x+(k+1)):f(i) n]
U Gen, 78
80 PROD(i,x,x+1):f(i) n
& ALL(k):[k n & PROD(i,x,x+k):f(i) n
=> PROD(i,x,x+(k+1)):f(i) n]
Join, 47, 79
81 ALL(k):[k n => PROD(i,x,x+k):f(i) n]
Detach, 27, 80
As Required:
82 x n => ALL(k):[k n => PROD(i,x,x+k):f(i) n]
Conclusion, 26
Generalizing...
83 ALL(j):[j n => ALL(k):[k n => PROD(i,j,j+k):f(i) n]]
U Gen, 82
Prove: x n & y n & x<y => PROD(i,x,y):f(i) n
Suppose...
84 x n & y n & x<y
Premise
85 x n
Split, 84
86 y n
Split, 84
87 x<y
Split, 84
Applying the definition of <
88 ALL(b):[x n & b n => [x<b <=> EXIST(c):[c n & x+c=b]]]
U Spec, 17
89 x n & y n => [x<y <=> EXIST(c):[c n & x+c=y]]
U Spec, 88
90 x n & y n
Join, 85, 86
91 x<y <=> EXIST(c):[c n & x+c=y]
Detach, 89, 90
92 [x<y => EXIST(c):[c n & x+c=y]]
& [EXIST(c):[c n & x+c=y] => x<y]
Iff-And, 91
93 x<y => EXIST(c):[c n & x+c=y]
Split, 92
94 EXIST(c):[c n & x+c=y] => x<y
Split, 92
95 EXIST(c):[c n & x+c=y]
Detach, 93, 87
Define: z
96 z n & x+z=y
E Spec, 95
97 z n
Split, 96
98 x+z=y
Split, 96
99 x n => ALL(k):[k n => PROD(i,x,x+k):f(i) n]
U Spec, 83
100 ALL(k):[k n => PROD(i,x,x+k):f(i) n]
Detach, 99, 85
101 z n => PROD(i,x,x+z):f(i) n
U Spec, 100
102 PROD(i,x,x+z):f(i) n
Detach, 101, 97
103 PROD(i,x,y):f(i) n
Substitute, 98, 102
As Required:
104 x n & y n & x<y => PROD(i,x,y):f(i) n
Conclusion, 84
Generalizing...
105 ALL(b):[x n & b n & x<b => PROD(i,x,b):f(i) n]
U Gen, 104
As Required:
106 ALL(a):ALL(b):[a n & b n & a<b => PROD(i,a,b):f(i) n]
U Gen, 105
Prove: x n & y n & x<=y => PROD(i,x,y):f(i) n
Suppose...
107 x n & y n & x<=y
Premise
108 x n
Split, 107
109 y n
Split, 107
110 x<=y
Split, 107
Applying the definition of <=...
111 ALL(b):[x n & b n => [x<=b <=> x<b | x=b]]
U Spec, 18
112 x n & y n => [x<=y <=> x<y | x=y]
U Spec, 111
113 x n & y n
Join, 108, 109
114 x<=y <=> x<y | x=y
Detach, 112, 113
115 [x<=y => x<y | x=y] & [x<y | x=y => x<=y]
Iff-And, 114
116 x<=y => x<y | x=y
Split, 115
117 x<y | x=y => x<=y
Split, 115
Cases
118 x<y | x=y
Detach, 116, 110
Case 1
Suppose...
119 x<y
Premise
Applying previous result...
120 ALL(b):[x n & b n & x<b => PROD(i,x,b):f(i) n]
U Spec, 106
121 x n & y n & x<y => PROD(i,x,y):f(i) n
U Spec, 120
122 x n & y n
Join, 108, 109
123 x n & y n & x<y
Join, 122, 119
124 PROD(i,x,y):f(i) n
Detach, 121, 123
Case 1
125 x<y => PROD(i,x,y):f(i) n
Conclusion, 119
Case 2
Suppose...
126 x=y
Premise
Applying definition of PROD...
127 x n => PROD(i,x,x):f(i)=f(x)
U Spec, 24
128 PROD(i,x,x):f(i)=f(x)
Detach, 127, 108
129 PROD(i,x,y):f(i)=f(x)
Substitute, 126, 128
130 x n => f(x) n
U Spec, 20
131 f(x) n
Detach, 130, 108
132 PROD(i,x,x):f(i) n
Substitute, 128, 131
133 PROD(i,x,y):f(i) n
Substitute, 126, 132
Case 2
134 x=y => PROD(i,x,y):f(i) n
Conclusion, 126
135 [x<y => PROD(i,x,y):f(i) n]
& [x=y => PROD(i,x,y):f(i) n]
Join, 125, 134
136 PROD(i,x,y):f(i) n
Cases, 118, 135
As Required:
137 x n & y n & x<=y => PROD(i,x,y):f(i) n
Conclusion, 107
Generalizing...
138 ALL(b):[x n & b n & x<=b => PROD(i,x,b):f(i) n]
U Gen, 137
139 ALL(a):ALL(b):[a n & b n & a<=b => PROD(i,a,b):f(i) n]
U Gen, 138
As Required:
140 ALL(a):[a n => f(a) n]
=> ALL(a):ALL(b):[a n & b n & a<=b => PROD(i,a,b):f(i) n]
Conclusion, 20
As Required:
141 ALL(f):[ALL(a):[a n => f(a) n]
=> ALL(a):ALL(b):[a n & b n & a<=b => PROD(i,a,b):f(i) n]]
U Gen, 140