let a, b, m, n be Nat; :: thesis: ( 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 ; :: thesis: (divSeq m,n) . b = 0
defpred S₁[ Nat] means ( a < $1 implies ( (divSeq m,n) . $1 = 0 & (modSeq m,n) . $1 = 0 ) );
A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
assume a < k + 1 ; :: thesis: ( (divSeq m,n) . (k + 1) = 0 & (modSeq m,n) . (k + 1) = 0 )
then A7: a <= k by NAT_1:13;

per cases ( k = 0 or k = 1 or k > 1 ) by NAT_1:26;

suppose k = 0 ; :: thesis: ( (divSeq m,n) . (k + 1) = 0 & (modSeq m,n) . (k + 1) = 0 )

hence ( (divSeq m,n) . (k + 1) = 0 & (modSeq m,n) . (k + 1) = 0 ) by A1, A7; :: thesis: verum

end;

suppose A8: k = 1 ; :: thesis: ( (divSeq m,n) . (k + 1) = 0 & (modSeq m,n) . (k + 1) = 0 )

then (divSeq m,n) . (0 + 1) = 0 by A1, A3, A7, NAT_1:26;
then A9: (modSeq m,n) . 0 = 0 by Th16;
A10: 2 = 2 + 0 ;
hence (divSeq m,n) . (k + 1) = ((modSeq m,n) . 0 ) div ((modSeq m,n) . (0 + 1)) by A8, Def3
.= 0 by A9 ;
:: thesis: (modSeq m,n) . (k + 1) = 0
thus (modSeq m,n) . (k + 1) = ((modSeq m,n) . 0 ) mod ((modSeq m,n) . (0 + 1)) by A8, A10, Def2
.= 0 by A9 ; :: thesis: verum

end;

suppose k > 1 ; :: thesis: ( (divSeq m,n) . (k + 1) = 0 & (modSeq m,n) . (k + 1) = 0 )

then reconsider k1 = k - 1 as Nat by Lm1;
A11: k = k1 + 1 ;

per cases ( a = k or a < k ) by A7, XXREAL_0:1;

suppose a = k ; :: thesis: ( (divSeq m,n) . (k + 1) = 0 & (modSeq m,n) . (k + 1) = 0 )

then A12: (modSeq m,n) . k1 = 0 by A3, A11, Th16;
thus (divSeq m,n) . (k + 1) = (divSeq m,n) . (k1 + 2)
.= ((modSeq m,n) . k1) div ((modSeq m,n) . (k1 + 1)) by Def3
.= 0 by A12 ; :: thesis: (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 Def2
.= 0 by A12 ; :: thesis: verum

end;

suppose A13: a < k ; :: thesis: ( (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 Def3
.= 0 by A6, A13 ; :: thesis: (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 Def2
.= 0 by A6, A13 ; :: thesis: verum

end;

end;

end;

end;

end;

A14: for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A5);
( a < b or a = b ) by A2, XXREAL_0:1;
hence (divSeq m,n) . b = 0 by A3, A14; :: thesis: verum