let a, b, n, m be Nat; :: thesis: ( a <= b & (modSeq (m,n)) . a = 0 implies (modSeq (m,n)) . b = 0 )
set fm = modSeq (m,n);
assume that
A1: a <= b and
A2: (modSeq (m,n)) . a = 0 ; :: thesis: (modSeq (m,n)) . b = 0
A3: ( a < b or a = b ) by A1, XXREAL_0:1;
defpred S₁[ Nat] means ( a < $1 implies (modSeq (m,n)) . $1 = 0 );
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
assume A6: a < k + 1 ; :: thesis: (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:25;

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

then A9: a = 0 by A6, NAT_1:13;
thus (modSeq (m,n)) . (k + 1) = n mod ((modSeq (m,n)) . 0) by A8, Th13
.= 0 by A2, A9 ; :: thesis: verum

end;

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

then A11: ( a = 0 or a = 1 ) by A7, NAT_1:25;
2 = 2 + 0 ;
hence (modSeq (m,n)) . (k + 1) = ((modSeq (m,n)) . 0) mod ((modSeq (m,n)) . (0 + 1)) by A10, Def1
.= 0 by A2, A11 ;
:: thesis: verum

end;

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

then reconsider k1 = k - 1 as Nat ;

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

suppose A12: a = k ; :: 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 A2, A12 ; :: thesis: verum

end;

suppose A13: a < k ; :: 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 A5, A13 ; :: thesis: verum

end;

end;

end;

end;

end;

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