let m be Element of NAT ; :: thesis: for a being Integer
for X being finite Subset of INT st X is_CRS_of m holds
a ++ X is_CRS_of m
let a be Integer; :: thesis: for X being finite Subset of INT st X is_CRS_of m holds
a ++ X is_CRS_of m
let X be finite Subset of INT; :: thesis: ( X is_CRS_of m implies a ++ X is_CRS_of m )
assume A1: X is_CRS_of m ; :: thesis: a ++ X is_CRS_of m
then card X = m by Th49;
then A2: card (a ++ X) = m by Th2;
A3: for i, j being Integer st i in a ++ X & j in a ++ X & i <> j holds
not [i,j] in Cong m

proof

let i, j be Integer; :: thesis: ( i in a ++ X & j in a ++ X & i <> j implies not [i,j] in Cong m )
assume that
A4: i in a ++ X and
A5: j in a ++ X and
A6: i <> j ; :: thesis: not [i,j] in Cong m
consider u being Complex such that
A7: i = a + u and
A8: u in X by A4, MEMBER_1:143;
consider w being Complex such that
A9: j = a + w and
A10: w in X by A5, MEMBER_1:143;
reconsider u9 = u, w9 = w as Integer by A8, A10;
assume [i,j] in Cong m ; :: thesis: contradiction
then i,j are_congruent_mod m by Def1;
then m divides (a + u9) - (a + w9) by A7, A9;
then m divides u9 - w9 ;
then A11: u9,w9 are_congruent_mod m ;
not [u9,w9] in Cong m by A1, A6, A8, A7, A10, A9, Th49;
hence contradiction by A11, Def1; :: thesis: verum

end;

a ++ X is Subset of INT by Lm1;
hence a ++ X is_CRS_of m by A2, A3, Th52; :: thesis: verum