let a, b, n, m 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
A4: ( a < b or a = b ) by A2, XXREAL_0:1;
defpred S₁[ Nat] means ( a < $1 implies ( (divSeq (m,n)) . $1 = 0 & (modSeq (m,n)) . $1 = 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 A7: a < k + 1 ; :: thesis: ( (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 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, NAT_1:13; :: thesis: verum

end;

suppose A9: 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, 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 ;
:: thesis: (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 ; :: 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 ;
A12: k = k1 + 1 ;

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

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

end;

suppose A14: 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 Def2
.= 0 by A6, A14 ; :: 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 Def1
.= 0 by A6, A14 ; :: thesis: verum

end;

end;

end;

end;

end;

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