let m be Nat; ( 0 < m implies for n being Nat ex k, t being Nat st
( n = (m * k) + t & t < m ) )
defpred S1[ Nat] means ex k, t being Nat st
( $1 = (m * k) + t & t < m );
assume A1:
0 < m
; for n being Nat ex k, t being Nat st
( n = (m * k) + t & t < m )
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
given k1,
t1 being
Nat such that A3:
n = (m * k1) + t1
and A4:
t1 < m
;
S1[n + 1]
A5:
(
t1 + 1
< m implies ex
k,
t being
Nat st
(
n + 1
= (m * k) + t &
t < m ) )
proof
assume A6:
t1 + 1
< m
;
ex k, t being Nat st
( n + 1 = (m * k) + t & t < m )
take k =
k1;
ex t being Nat st
( n + 1 = (m * k) + t & t < m )
take t =
t1 + 1;
( n + 1 = (m * k) + t & t < m )
thus
n + 1
= (m * k) + t
by A3;
t < m
thus
t < m
by A6;
verum
end;
A7:
(
t1 + 1
= m implies ex
k,
t being
Nat st
(
n + 1
= (m * k) + t &
t < m ) )
proof
assume A8:
t1 + 1
= m
;
ex k, t being Nat st
( n + 1 = (m * k) + t & t < m )
take k =
k1 + 1;
ex t being Nat st
( n + 1 = (m * k) + t & t < m )
take t =
0 ;
( n + 1 = (m * k) + t & t < m )
thus
n + 1
= (m * k) + t
by A3, A8;
t < m
thus
t < m
by A1;
verum
end;
t1 + 1
<= m
by A4, Th13;
hence
S1[
n + 1]
by A5, A7, XXREAL_0:1;
verum
end;
0 = (m * 0) + 0
;
then A9:
S1[ 0 ]
by A1;
thus
for n being Nat holds S1[n]
from NAT_1:sch 2(A9, A2); verum