environ
vocabularies NATURAL;
notations NATURAL,INDUCT;
constructors NATURAL,INDUCT;
registrations NATURAL;
requirements NATURAL;
theorems INDUCT;
schemes INDUCT;
definitions INDUCT;
begin
reserve i,j,k,l,m,n for natural number;
L1:
0 + n = n
proof
defpred P[natural number] means 0 + $1 = $1;
z: P[0] by INDUCT:3;
k: for k st P[k] holds P[succ k]
proof
let k;
assume P[k];
then k: 0 + k = k;
:: 0 + succ k = succ (0+k) by INDUCT:4 .= succ k by k;
0 + succ k = succ k by k,INDUCT:4;
hence P[succ k];
end;
for n holds P[n] from INDUCT:sch 1(z,k);
hence thesis;
end;
L2:
succ(n) + m = succ (n+m)
proof
defpred P[natural number] means succ n + $1 = succ (n+$1);
succ n + 0 = succ n by INDUCT:3 .= succ (n+0) by INDUCT:3;
then z: P[0];
k: for k st P[k] holds P[succ k]
proof
let k;
assume P[k];
then s: succ n + k = succ (n+k);
succ n + succ k = succ(succ n+ k) by INDUCT:4 .= succ(succ(n+k)) by s
.= succ(n+succ k) by INDUCT:4;
hence P[succ k];
end;
for m holds P[m] from INDUCT:sch 1(z,k);
hence thesis;
end;
theorem T1:
n+m=m+n
proof
defpred P[natural number] means n+$1 = $1+n;
n+0=n by INDUCT:3 .= 0+n by L1;
then a: P[0];
b: P[k] implies P[succ k]
proof
assume P[k];
then i: n+k=k+n;
n+succ k = succ (n+k) by INDUCT:4 .= succ(k+n) by i .= succ k + n by L2;
hence P[succ k];
end;
for k holds P[k] from INDUCT:sch 1(a,b);
hence thesis;
end;
theorem T2:
(k+n)+m=k+(n+m)
proof
defpred P[natural number] means k + n + $1 = k + (n+$1);
k+n+0= k+n by INDUCT:3
.= k+(n+0) by INDUCT:3;
then a: P[0];
b: for m holds P[m] implies P[succ m]
proof
let m;
assume P[m];
then k: k + n + m = k + (n+m);
k + n + succ m = succ (k+n+m) by INDUCT:4
.= succ (k+(n+m)) by k
.= k + succ (n+m) by INDUCT:4
.= k + (n+succ m) by INDUCT:4;
hence P[succ m];
end;
for k holds P[k] from INDUCT:sch 1(a,b);
hence thesis;
end;
L3: 0*n=0
proof
defpred P[natural number] means 0*$1 = 0;
z: P[0] by INDUCT:5;
k: for k st P[k] holds P[succ k]
proof
let k;
assume k: P[k];
0*succ k = 0*k + 0 by INDUCT:6 .= 0+0 by k .= 0 by INDUCT:3;
hence P[succ k];
end;
for k holds P[k] from INDUCT:sch 1(z,k);
hence thesis;
end;
L4: succ(n)*m=n*m+m
proof
defpred P[natural number] means succ(n)*$1=n*$1+$1;
succ(n)*0 = 0 by INDUCT:5
.= 0 + 0 by INDUCT:3
.= n*0 + 0 by INDUCT:5;
then z: P[0];
k: for k st P[k] holds P[succ k]
proof
let k;
assume k: P[k];
succ(n)*succ(k)= succ(n)*k+succ(n) by INDUCT:6
.= n*k+k+succ(n) by k
.= n*k + (k + succ n) by T2
.= n*k + succ (k+n) by INDUCT: 4
.= n*k + succ (n+k) by T1
.= n*k + (n + succ k) by INDUCT: 4
.= n*k + n + succ k by T2
.= n * succ k + succ k by INDUCT: 6;
hence P[succ k];
end;
for k holds P[k] from INDUCT:sch 1(z,k);
hence thesis;
end;
theorem T3:
n*m = m*n
proof
defpred P[natural number] means m*$1 = $1*m;
z:P[0]
proof
thus m*0 = 0 by INDUCT: 5
.= 0*m by L3;
end;
k:for n st P[n] holds P[succ n]
proof
let n;
assume a1:P[n];
thus m*succ n =m*n + m by INDUCT: 6
.= n*m + m by a1
.= succ n * m by L4;
end;
for n holds P[n] from INDUCT:sch 1(z,k);
hence thesis;
end;
theorem T4:
(k+n)*m = (k*m) + (n*m)
proof
defpred P[natural number] means (k+n)*$1 = (k*$1) + (n*$1);
z:P[0]
proof
thus (k+n)*0 = 0 by INDUCT: 5
.= 0 + 0 by INDUCT: 3
.= k*0 + 0 by INDUCT: 5
.= k*0 + (n*0) by INDUCT: 5;
end;
m:for m st P[m] holds P[succ m]
proof
let m;
assume a1: P[m];
thus (k+n)*succ m = (k+n)*m + (k+n) by INDUCT: 6
.= (k*m + (n*m)) + (k+n) by a1
.= ((k*m + (n*m)) + k) + n by T2
.= ((n*m + (k*m)) + k) + n by T1
.= (n*m + (k*m + k)) + n by T2
.= (n*m + (k*succ m)) + n by INDUCT: 6
.= (k*succ m + (n*m)) + n by T1
.= k*succ m + (n*m + n) by T2
.= k*succ m + (n*succ m) by INDUCT: 6;
end;
for m holds P[m] from INDUCT:sch 1(z,m);
hence thesis;
end;
theorem T5:
(k*n)*m = k*(n*m)
proof
defpred P[natural number] means (k*$1)*m = k*($1*m);
(k*0)*m = 0*m by INDUCT:5 .= 0 by L3 .= k*0 by INDUCT:5 .= k*(0*m) by L3;
then
z: P[0];
k: for i st P[i] holds P[succ i]
proof
let i;
assume P[i];
then i: (k*i)*m = k*(i*m);
(k*succ (i))*m = (k*i + k)*m by INDUCT:6
.= (k*i)*m + (k*m) by T4
.= k*(i*m)+(k*m) by i
.= (i*m)*k + (k*m) by T3
.= (i*m)*k + (m*k) by T3
.= (i*m+m)*k by T4
.= k*(i*m+m) by T3
.= k*(succ(i)*m) by L4;
hence P[succ i];
end;
for j holds P[j] from INDUCT:sch 1(z,k);
hence thesis;
end;
2+2=(succ succ 0) + (succ succ 0)
.= succ 1 + succ 1
.= succ (1+ succ 1) by L2
.= succ (succ (1+1)) by INDUCT:4
.= succ (succ 1+1) by L2
.= succ (2+1)
.= succ (2+succ 0)
.= succ (succ (2+0)) by INDUCT:4
.= succ (succ 2) by INDUCT:3
.= succ 3
.= 4;