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

hence a ++ X is_CRS_of m by A2, A3, Th52; :: thesis: verum

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

a ++ X is Subset of INT
by Lm1;
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;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

hence a ++ X is_CRS_of m by A2, A3, Th52; :: thesis: verum