let m be CR_Sequence; :: thesis: for c being CR_coefficients of m
for i, j being Nat st i in dom c & j in dom c & i <> j holds
c . i, 0 are_congruent_mod m . j
let c be CR_coefficients of m; :: thesis: for i, j being Nat st i in dom c & j in dom c & i <> j holds
c . i, 0 are_congruent_mod m . j
let i, j be Nat; :: thesis: ( i in dom c & j in dom c & i <> j implies c . i, 0 are_congruent_mod m . j )
assume that
A1: i in dom c and
A2: j in dom c and
A3: i <> j ; :: thesis: c . i, 0 are_congruent_mod m . j
consider s, mm being Integer such that
A4: mm = (Product m) / (m . i) and
s * mm,1 are_congruent_mod m . i and
A5: c . i = s * ((Product m) / (m . i)) by A1, Def4;
len m = len c by Def4;
then dom m = Seg (len c) by FINSEQ_1:def 3
.= dom c by FINSEQ_1:def 3 ;
then consider z being Integer such that
A6: z * (m . j) = mm by A2, A3, A4, Lm6;
A7: m . j, 0 are_congruent_mod m . j by INT_1:12;
A8: s,s are_congruent_mod m . j by INT_1:11;
z,z are_congruent_mod m . j by INT_1:11;
then z * (m . j),z * 0 are_congruent_mod m . j by A7, INT_1:18;
then s * mm,s * 0 are_congruent_mod m . j by A6, A8, INT_1:18;
hence c . i, 0 are_congruent_mod m . j by A4, A5; :: thesis: verum