let a, b, n, m be Nat; ( a <> 0 & a <= b & (divSeq (m,n)) . a = 0 implies (divSeq (m,n)) . b = 0 )
set fd = divSeq (m,n);
set fm = modSeq (m,n);
assume that
A1:
a <> 0
and
A2:
a <= b
and
A3:
(divSeq (m,n)) . a = 0
; (divSeq (m,n)) . b = 0
A4:
( a < b or a = b )
by A2, XXREAL_0:1;
defpred S1[ Nat] means ( a < $1 implies ( (divSeq (m,n)) . $1 = 0 & (modSeq (m,n)) . $1 = 0 ) );
A5:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A6:
S1[
k]
;
S1[k + 1]
assume A7:
a < k + 1
;
( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 )
then A8:
a <= k
by NAT_1:13;
per cases
( k = 0 or k = 1 or k > 1 )
by NAT_1:25;
suppose A9:
k = 1
;
( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 )then
(divSeq (m,n)) . (0 + 1) = 0
by A1, A3, A8, NAT_1:25;
then A10:
(modSeq (m,n)) . 0 = 0
by Th16;
A11:
2
= 2
+ 0
;
hence (divSeq (m,n)) . (k + 1) =
((modSeq (m,n)) . 0) div ((modSeq (m,n)) . (0 + 1))
by A9, Def2
.=
0
by A10
;
(modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) =
((modSeq (m,n)) . 0) mod ((modSeq (m,n)) . (0 + 1))
by A9, A11, Def1
.=
0
by A10
;
verum end; suppose
k > 1
;
( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 )then reconsider k1 =
k - 1 as
Nat ;
A12:
k = k1 + 1
;
per cases
( a = k or a < k )
by A8, XXREAL_0:1;
suppose
a = k
;
( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 )then A13:
(modSeq (m,n)) . k1 = 0
by A3, A12, Th16;
thus (divSeq (m,n)) . (k + 1) =
(divSeq (m,n)) . (k1 + 2)
.=
((modSeq (m,n)) . k1) div ((modSeq (m,n)) . (k1 + 1))
by Def2
.=
0
by A13
;
(modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) =
(modSeq (m,n)) . (k1 + 2)
.=
((modSeq (m,n)) . k1) mod ((modSeq (m,n)) . (k1 + 1))
by Def1
.=
0
by A13
;
verum end; suppose A14:
a < k
;
( (divSeq (m,n)) . (k + 1) = 0 & (modSeq (m,n)) . (k + 1) = 0 )thus (divSeq (m,n)) . (k + 1) =
(divSeq (m,n)) . (k1 + 2)
.=
((modSeq (m,n)) . k1) div ((modSeq (m,n)) . (k1 + 1))
by Def2
.=
0
by A6, A14
;
(modSeq (m,n)) . (k + 1) = 0 thus (modSeq (m,n)) . (k + 1) =
(modSeq (m,n)) . (k1 + 2)
.=
((modSeq (m,n)) . k1) mod ((modSeq (m,n)) . (k1 + 1))
by Def1
.=
0
by A6, A14
;
verum end; end;
end;
A15:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A15, A5);
hence
(divSeq (m,n)) . b = 0
by A3, A4; verum