let a, n, m be Nat; ( (divSeq (m,n)) . (a + 1) = 0 implies (modSeq (m,n)) . a = 0 )
set fd = divSeq (m,n);
set fm = modSeq (m,n);
defpred S1[ Nat] means ( (divSeq (m,n)) . ($1 + 1) = 0 implies (modSeq (m,n)) . $1 = 0 );
A1:
for b being Nat st S1[b] holds
S1[b + 1]
proof
let b be
Nat;
( S1[b] implies S1[b + 1] )
assume
S1[
b]
;
S1[b + 1]
set x =
(modSeq (m,n)) . (b + 1);
assume
(divSeq (m,n)) . ((b + 1) + 1) = 0
;
(modSeq (m,n)) . (b + 1) = 0
then
(divSeq (m,n)) . (b + (1 + 1)) = 0
;
then A2:
((modSeq (m,n)) . b) div ((modSeq (m,n)) . (b + 1)) = 0
by Def2;
assume A3:
(modSeq (m,n)) . (b + 1) <> 0
;
contradiction
then
(modSeq (m,n)) . b = (((modSeq (m,n)) . (b + 1)) * (((modSeq (m,n)) . b) div ((modSeq (m,n)) . (b + 1)))) + (((modSeq (m,n)) . b) mod ((modSeq (m,n)) . (b + 1)))
by NAT_D:2;
then A4:
(modSeq (m,n)) . b < (modSeq (m,n)) . (b + 1)
by A2, A3, NAT_D:1;
A5:
b + 0 < b + 1
by XREAL_1:6;
then
(modSeq (m,n)) . b <> 0
by A3, Th14;
hence
contradiction
by A4, A5, Th15;
verum
end;
A6:
S1[ 0 ]
proof
set x =
m mod n;
assume
(divSeq (m,n)) . (0 + 1) = 0
;
(modSeq (m,n)) . 0 = 0
then A7:
n div ((modSeq (m,n)) . 0) = 0
by Th12;
assume A8:
(modSeq (m,n)) . 0 <> 0
;
contradiction
then
m mod n <> 0
by Def1;
then A9:
n <> 0
;
A10:
(modSeq (m,n)) . 0 = m mod n
by Def1;
then
n = ((m mod n) * (n div (m mod n))) + (n mod (m mod n))
by A8, NAT_D:2;
then
n < m mod n
by A7, A10, A8, NAT_D:1;
hence
contradiction
by A9, NAT_D:1;
verum
end;
for b being Nat holds S1[b]
from NAT_1:sch 2(A6, A1);
hence
( (divSeq (m,n)) . (a + 1) = 0 implies (modSeq (m,n)) . a = 0 )
; verum