Sum of Constant Terms
Prove: ALL(m):ALL(f):[m 
n & ALL(a):[a n => f(a)=m]
=> ALL(k):[k n => SUM(i,1,k):f(i)=k*m]]
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
Previous result: * is commutative
16 ALL(a):ALL(b):[a n & b n => a*b=b*a]
Premise
Define: f
f is constant function.
17 x n & ALL(a):[a n => f(a)=x]
Premise
18 x n
Split, 17
19 ALL(a):[a n => f(a)=x]
Split, 17
Prove: y n => f(y) n
Suppose...
20 y n
Premise
21 y n => f(y)=x
U Spec, 19
22 f(y)=x
Detach, 21, 20
23 f(y) n
Substitute, 22, 18
As Required:
24 y n => f(y) n
Conclusion, 20
Generalizing...
25 ALL(a):[a n => f(a) n]
U Gen, 24
Define: SUM
26 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
27 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, 26
28 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, 27, 25
From the definitions of SUM and f...
29 ALL(a):[a n => SUM(i,a,a):f(i)=f(a)]
Split, 28
30 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, 28
Prove: y n => SUM(i,y,y):f(i)=x
Suppose...
31 y n
Premise
32 y n => SUM(i,y,y):f(i)=f(y)
U Spec, 29
33 SUM(i,y,y):f(i)=f(y)
Detach, 32, 31
34 y n => f(y)=x
U Spec, 19
35 f(y)=x
Detach, 34, 31
36 SUM(i,y,y):f(i)=x
Substitute, 35, 33
As Required:
37 y n => SUM(i,y,y):f(i)=x
Conclusion, 31
From the definiton of SUM and f...
38 ALL(a):[a n => SUM(i,a,a):f(i)=x]
U Gen, 37
Prove: y n & z n => SUM(i,y,z+1):f(i)=SUM(i,y,z):f(i)+x
Suppose...
39 y n & z n
Premise
40 y n
Split, 39
41 z n
Split, 39
Applying the definitions of SUM and f...
42 ALL(b):[y n & b n => SUM(i,y,b+1):f(i)=SUM(i,y,b):f(i)+f(b+1)]
U Spec, 30
43 y n & z n => SUM(i,y,z+1):f(i)=SUM(i,y,z):f(i)+f(z+1)
U Spec, 42
44 SUM(i,y,z+1):f(i)=SUM(i,y,z):f(i)+f(z+1)
Detach, 43, 39
45 z+1 n => f(z+1)=x
U Spec, 19
46 ALL(b):[z n & b n => z+b n]
U Spec, 9
47 z n & 1 n => z+1 n
U Spec, 46
48 z n & 1 n
Join, 41, 3
49 z+1 n
Detach, 47, 48
50 f(z+1)=x
Detach, 45, 49
51 SUM(i,y,z+1):f(i)=SUM(i,y,z):f(i)+x
Substitute, 50, 44
As Required:
52 y n & z n => SUM(i,y,z+1):f(i)=SUM(i,y,z):f(i)+x
Conclusion, 39
Generalizing...
53 ALL(b):[y n & b n => SUM(i,y,b+1):f(i)=SUM(i,y,b):f(i)+x]
U Gen, 52
From the definitions of SUM and f...
54 ALL(a):ALL(b):[a n & b n => SUM(i,a,b+1):f(i)=SUM(i,a,b):f(i)+x]
U Gen, 53
Sufficient: For ALL(k):[k n => SUM(i,1,k):f(i)=k*x]
55 SUM(i,1,1):f(i)=1*x
& ALL(k):[k n & SUM(i,1,k):f(i)=k*x => SUM(i,1,k+1):f(i)=(k+1)*x]
=> ALL(k):[k n => SUM(i,1,k):f(i)=k*x]
Induction
Prove: SUM(i,1,1):f(i)=1*x (Induction, Part1)
Applying the defintions of SUM and f...
56 1 n => SUM(i,1,1):f(i)=x
U Spec, 38
57 SUM(i,1,1):f(i)=x
Detach, 56, 3
58 x n => x*1=x
U Spec, 14
59 x*1=x
Detach, 58, 18
Applying commutativity of *...
60 ALL(b):[x n & b n => x*b=b*x]
U Spec, 16
61 x n & 1 n => x*1=1*x
U Spec, 60
62 x n & 1 n
Join, 18, 3
63 x*1=1*x
Detach, 61, 62
64 1*x=x
Substitute, 63, 59
As Required: (Induction, Part 1)
65 SUM(i,1,1):f(i)=1*x
Substitute, 64, 57
Prove: y n & SUM(i,1,y):f(i)=y*x => SUM(i,1,y+1):f(i)=(y+1)*x
Suppose...
66 y n & SUM(i,1,y):f(i)=y*x
Premise
67 y n
Split, 66
68 SUM(i,1,y):f(i)=y*x
Split, 66
Applying the definitions of SUM and f...
69 ALL(b):[1 n & b n => SUM(i,1,b+1):f(i)=SUM(i,1,b):f(i)+x]
U Spec, 54
70 1 n & y n => SUM(i,1,y+1):f(i)=SUM(i,1,y):f(i)+x
U Spec, 69
71 1 n & y n
Join, 3, 67
72 SUM(i,1,y+1):f(i)=SUM(i,1,y):f(i)+x
Detach, 70, 71
73 SUM(i,1,y+1):f(i)=y*x+x
Substitute, 68, 72
Applying distributive rule...
74 ALL(b):[x n & b n => x*(b+1)=x*b+x]
U Spec, 15
75 x n & y n => x*(y+1)=x*y+x
U Spec, 74
76 x n & y n
Join, 18, 67
77 x*(y+1)=x*y+x
Detach, 75, 76
Applying commutativity of *...
78 ALL(b):[x n & b n => x*b=b*x]
U Spec, 16
79 x n & y n => x*y=y*x
U Spec, 78
80 x*y=y*x
Detach, 79, 76
81 x*(y+1)=y*x+x
Substitute, 80, 77
82 x n & y+1 n => x*(y+1)=(y+1)*x
U Spec, 78
83 ALL(b):[y n & b n => y+b n]
U Spec, 9
84 y n & 1 n => y+1 n
U Spec, 83
85 y n & 1 n
Join, 67, 3
86 y+1 n
Detach, 84, 85
87 x n & y+1 n
Join, 18, 86
88 x*(y+1)=(y+1)*x
Detach, 82, 87
89 (y+1)*x=y*x+x
Substitute, 88, 81
90 SUM(i,1,y+1):f(i)=(y+1)*x
Substitute, 89, 73
91 y n & SUM(i,1,y):f(i)=y*x
=> SUM(i,1,y+1):f(i)=(y+1)*x
Conclusion, 66
92 ALL(k):[k n & SUM(i,1,k):f(i)=k*x
=> SUM(i,1,k+1):f(i)=(k+1)*x]
U Gen, 91
93 SUM(i,1,1):f(i)=1*x
& ALL(k):[k n & SUM(i,1,k):f(i)=k*x
=> SUM(i,1,k+1):f(i)=(k+1)*x]
Join, 65, 92
94 ALL(k):[k n => SUM(i,1,k):f(i)=k*x]
Detach, 55, 93
As Required:
95 x n & ALL(a):[a n => f(a)=x]
=> ALL(k):[k n => SUM(i,1,k):f(i)=k*x]
Conclusion, 17
Generalizing...
96 ALL(f):[x n & ALL(a):[a n => f(a)=x]
=> ALL(k):[k n => SUM(i,1,k):f(i)=k*x]]
U Gen, 95
As Required:
97 ALL(m):ALL(f):[m n & ALL(a):[a n => f(a)=m]
=> ALL(k):[k n => SUM(i,1,k):f(i)=k*m]]
U Gen, 96