let m be Nat; for X being finite set st X is_RRS_of m holds
( card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) )
let X be finite set ; ( X is_RRS_of m implies ( card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) ) )
assume
X is_RRS_of m
; ( card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) )
then consider fp being FinSequence of INT such that
A1:
( len fp = len (Sgm (RelPrimes m)) & ( for d being Element of NAT st d in dom fp holds
fp . d in Class ((Cong m),((Sgm (RelPrimes m)) . d)) ) & X = rng fp )
;
A2:
dom fp = dom (Sgm (RelPrimes m))
by A1, FINSEQ_3:29;
for a, b being object st a in dom fp & b in dom fp & fp . a = fp . b holds
a = b
proof
let a,
b be
object ;
( a in dom fp & b in dom fp & fp . a = fp . b implies a = b )
assume A3:
(
a in dom fp &
b in dom fp &
fp . a = fp . b )
;
a = b
reconsider a =
a,
b =
b as
Element of
NAT by A3;
reconsider l =
fp . a,
ll =
fp . b as
Element of
INT by A3, FINSEQ_2:11;
(
l in Class (
(Cong m),
((Sgm (RelPrimes m)) . a)) &
ll in Class (
(Cong m),
((Sgm (RelPrimes m)) . b)) )
by A1, A3;
then
(
[((Sgm (RelPrimes m)) . a),l] in Cong m &
[((Sgm (RelPrimes m)) . b),ll] in Cong m )
by EQREL_1:18;
then A4:
(
(Sgm (RelPrimes m)) . a,
l are_congruent_mod m &
(Sgm (RelPrimes m)) . b,
ll are_congruent_mod m )
by INT_4:def 1;
then
l,
(Sgm (RelPrimes m)) . b are_congruent_mod m
by A3, INT_1:14;
hence
a = b
by Th23, A3, A2, A4, INT_1:15;
verum
end;
then A5:
fp is one-to-one
by FUNCT_1:def 4;
A6:
RelPrimes m c= Seg m
by Th1;
A7: card X =
len (Sgm (RelPrimes m))
by A1, FINSEQ_4:62, A5
.=
Euler m
by A6, FINSEQ_3:39
;
A8:
for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m
proof
let x,
y be
Integer;
( x in X & y in X & x <> y implies not x,y are_congruent_mod m )
assume A9:
(
x in X &
y in X &
x <> y )
;
not x,y are_congruent_mod m
then consider d being
Nat such that A10:
(
d in dom fp &
fp . d = x )
by A1, FINSEQ_2:10;
consider e being
Nat such that A11:
(
e in dom fp &
fp . e = y )
by A1, A9, FINSEQ_2:10;
A12:
(
d in dom (Sgm (RelPrimes m)) &
e in dom (Sgm (RelPrimes m)) )
by A10, A11, A1, FINSEQ_3:29;
reconsider d =
d,
e =
e as
Element of
NAT by A10, A11;
(
fp . d in Class (
(Cong m),
((Sgm (RelPrimes m)) . d)) &
fp . e in Class (
(Cong m),
((Sgm (RelPrimes m)) . e)) )
by A10, A11, A1;
then
(
[((Sgm (RelPrimes m)) . d),(fp . d)] in Cong m &
[((Sgm (RelPrimes m)) . e),(fp . e)] in Cong m )
by EQREL_1:18;
then A13:
(
(Sgm (RelPrimes m)) . d,
fp . d are_congruent_mod m &
(Sgm (RelPrimes m)) . e,
fp . e are_congruent_mod m )
by INT_4:def 1;
now not fp . d,fp . e are_congruent_mod massume
fp . d,
fp . e are_congruent_mod m
;
contradictionthen
(Sgm (RelPrimes m)) . d,
fp . e are_congruent_mod m
by A13, INT_1:15;
then
fp . e,
(Sgm (RelPrimes m)) . d are_congruent_mod m
by INT_1:14;
hence
contradiction
by A12, A10, A11, A9, Th23, A13, INT_1:15;
verum end;
hence
not
x,
y are_congruent_mod m
by A10, A11;
verum
end;
for x being Integer st x in X holds
x,m are_coprime
proof
let x be
Integer;
( x in X implies x,m are_coprime )
assume
x in X
;
x,m are_coprime
then consider d being
Nat such that A14:
(
d in dom fp &
fp . d = x )
by A1, FINSEQ_2:10;
reconsider d =
d as
Element of
NAT by A14;
fp . d in Class (
(Cong m),
((Sgm (RelPrimes m)) . d))
by A1, A14;
then
[((Sgm (RelPrimes m)) . d),(fp . d)] in Cong m
by EQREL_1:18;
then
(Sgm (RelPrimes m)) . d,
fp . d are_congruent_mod m
by INT_4:def 1;
then A15:
((Sgm (RelPrimes m)) . d) gcd m = (fp . d) gcd m
by WSIERP_1:43;
RelPrimes m c= Seg m
by Th1;
then
rng (Sgm (RelPrimes m)) = RelPrimes m
by FINSEQ_1:def 13;
then
(Sgm (RelPrimes m)) . d in RelPrimes m
by A2, A14, FUNCT_1:def 3;
then consider k being
Element of
NAT such that A16:
(
(Sgm (RelPrimes m)) . d = k &
m,
k are_coprime &
k >= 1 &
k <= m )
;
(fp . d) gcd m = 1
by A15, A16, INT_2:def 3;
hence
x,
m are_coprime
by A14, INT_2:def 3;
verum
end;
hence
( card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) )
by A7, A8; verum