let m be Element of NAT ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: a ** X is_CRS_of m

A3: card X = m by A2, Th49;

A4: a ** X c= INT by Lm2;

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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 )
;

end;

suppose A5:
a = 0
; :: thesis: a ** X is_CRS_of m

then a gcd m =
|.m.|
by WSIERP_1:8

.= m by ABSVALUE:def 1 ;

then A6: m = 1 by A1, INT_2:def 3;

then ex x being object st X = {x} by A3, CARD_2:42;

then A7: a ** X = {0} by A5, Th4;

A8: for x, y being Integer st x in a ** X & y in a ** X & x <> y holds

not [x,y] in Cong m

hence a ** X is_CRS_of m by A4, A8, Th52; :: thesis: verum

end;.= m by ABSVALUE:def 1 ;

then A6: m = 1 by A1, INT_2:def 3;

then ex x being object st X = {x} by A3, CARD_2:42;

then A7: a ** X = {0} by A5, Th4;

A8: for x, y being Integer st x in a ** X & y in a ** X & x <> y holds

not [x,y] in Cong m

proof

card (a ** X) = m
by A6, A7, CARD_2:42;
let x, y be Integer; :: thesis: ( x in a ** X & y in a ** X & x <> y implies not [x,y] in Cong m )

assume that

A9: x in a ** X and

A10: ( y in a ** X & x <> y ) ; :: thesis: not [x,y] in Cong m

assume [x,y] in Cong m ; :: thesis: contradiction

x = 0 by A7, A9, TARSKI:def 1;

hence contradiction by A7, A10, TARSKI:def 1; :: thesis: verum

end;assume that

A9: x in a ** X and

A10: ( y in a ** X & x <> y ) ; :: thesis: not [x,y] in Cong m

assume [x,y] in Cong m ; :: thesis: contradiction

x = 0 by A7, A9, TARSKI:def 1;

hence contradiction by A7, A10, TARSKI:def 1; :: thesis: verum

hence a ** X is_CRS_of m by A4, A8, Th52; :: thesis: verum

suppose A11:
a <> 0
; :: thesis: a ** X is_CRS_of m

A12:
for x, y being Integer st x in a ** X & y in a ** X & x <> y holds

not [x,y] in Cong m

hence a ** X is_CRS_of m by A4, A12, Th52; :: thesis: verum

end;not [x,y] in Cong m

proof

card (a ** X) = m
by A3, A11, Th5;
let x, y be Integer; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: contradiction

then a * x1,a * y1 are_congruent_mod m by A19, A17, Def1;

hence contradiction by A1, A20, Th9; :: thesis: verum

end;assume that

A13: x in a ** X and

A14: y in a ** X and

A15: x <> y ; :: thesis: 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 ; :: thesis: contradiction

then a * x1,a * y1 are_congruent_mod m by A19, A17, Def1;

hence contradiction by A1, A20, Th9; :: thesis: verum

hence a ** X is_CRS_of m by A4, A12, Th52; :: thesis: verum