let m be Element of NAT ; for a being Integer
for X being finite Subset of INT st a,m are_coprime & X is_CRS_of m holds
a ** X is_CRS_of m
let a be Integer; for X being finite Subset of INT st a,m are_coprime & X is_CRS_of m holds
a ** X is_CRS_of m
let X be finite Subset of INT; ( a,m are_coprime & X is_CRS_of m implies a ** X is_CRS_of m )
assume that
A1:
a,m are_coprime
and
A2:
X is_CRS_of m
; a ** X is_CRS_of m
A3:
card X = m
by A2, Th49;
A4:
a ** X c= INT
by Lm2;
per cases
( a = 0 or a <> 0 )
;
suppose A11:
a <> 0
;
a ** X is_CRS_of mA12:
for
x,
y being
Integer st
x in a ** X &
y in a ** X &
x <> y holds
not
[x,y] in Cong m
proof
let x,
y be
Integer;
( x in a ** X & y in a ** X & x <> y implies not [x,y] in Cong m )
assume that A13:
x in a ** X
and A14:
y in a ** X
and A15:
x <> y
;
not [x,y] in Cong m
consider y1 being
Integer such that A16:
y1 in X
and A17:
y = a * y1
by A14, Lm3;
consider x1 being
Integer such that A18:
x1 in X
and A19:
x = a * x1
by A13, Lm3;
not
[x1,y1] in Cong m
by A2, A15, A18, A19, A16, A17, Th49;
then A20:
not
x1,
y1 are_congruent_mod m
by Def1;
assume
[x,y] in Cong m
;
contradiction
then
a * x1,
a * y1 are_congruent_mod m
by A19, A17, Def1;
hence
contradiction
by A1, A20, Th9;
verum
end;
card (a ** X) = m
by A3, A11, Th5;
hence
a ** X is_CRS_of m
by A4, A12, Th52;
verum end; end;