let m be Element of NAT ; 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; 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; ( X is_CRS_of m implies a ++ X is_CRS_of m )
assume A1:
X is_CRS_of m
; 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;
( 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
;
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
;
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;
verum
end;
a ++ X is Subset of INT
by Lm1;
hence
a ++ X is_CRS_of m
by A2, A3, Th52; verum