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