let a, b, m be Integer; ( m <> 0 & a gcd m divides b implies ex fp being FinSequence of INT st
( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds
((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds
not fp . c1,fp . c2 are_congruent_mod m ) ) )
assume that
A1:
m <> 0
and
A2:
a gcd m divides b
; ex fp being FinSequence of INT st
( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds
((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds
not fp . c1,fp . c2 are_congruent_mod m ) )
set l = a gcd m;
reconsider l = a gcd m as Element of NAT by ORDINAL1:def 12;
consider a1, m1 being Integer such that
A3:
a = l * a1
and
A4:
m = l * m1
and
A5:
a1,m1 are_coprime
by A1, INT_2:23;
consider b1 being Integer such that
A6:
b = l * b1
by A2;
consider x1 being Integer such that
A7:
((a1 * x1) - b1) mod m1 = 0
by A5, Th15;
deffunc H1( Nat) -> set = x1 + (($1 - 1) * m1);
consider fp being FinSequence such that
A8:
( len fp = l & ( for c being Nat st c in dom fp holds
fp . c = H1(c) ) )
from FINSEQ_1:sch 2();
for c being Nat st c in dom fp holds
fp . c in INT
then reconsider fp = fp as FinSequence of INT by FINSEQ_2:12;
A9:
m1 <> 0
by A1, A4;
A10:
for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds
not fp . c1,fp . c2 are_congruent_mod m
proof
let c1,
c2 be
Element of
NAT ;
( c1 in dom fp & c2 in dom fp & c1 <> c2 implies not fp . c1,fp . c2 are_congruent_mod m )
assume that A11:
c1 in dom fp
and A12:
c2 in dom fp
and A13:
c1 <> c2
;
not fp . c1,fp . c2 are_congruent_mod m
assume A14:
fp . c1,
fp . c2 are_congruent_mod m
;
contradiction
(
fp . c1 = x1 + ((c1 - 1) * m1) &
fp . c2 = x1 + ((c2 - 1) * m1) )
by A8, A11, A12;
then
m divides (((c1 - 1) * m1) + x1) - (((c2 - 1) * m1) + x1)
by A14;
then consider w being
Integer such that A15:
(c1 - c2) * m1 = (l * m1) * w
by A4;
(c1 - c2) * m1 = (l * w) * m1
by A15;
then
c1 - c2 = l * w
by A9, XCMPLX_1:5;
then A16:
l divides c1 - c2
;
A17:
c2 in Seg l
by A8, A12, FINSEQ_1:def 3;
then A18:
c2 >= 1
by FINSEQ_1:1;
A19:
c1 in Seg l
by A8, A11, FINSEQ_1:def 3;
then
c1 <= l
by FINSEQ_1:1;
then
c1 - c2 <= l - 1
by A18, XREAL_1:13;
then A20:
c1 - c2 < l
by XREAL_1:147;
A21:
c2 <= l
by A17, FINSEQ_1:1;
c1 >= 1
by A19, FINSEQ_1:1;
then
c1 - c2 >= 1
- l
by A21, XREAL_1:13;
then
c1 - c2 > - l
by XREAL_1:145;
then A22:
|.(c1 - c2).| < l
by A20, SEQ_2:1;
c1 - c2 <> 0
by A13;
then
|.l.| <= |.(c1 - c2).|
by A16, Th6;
hence
contradiction
by A22, ABSVALUE:def 1;
verum
end;
take
fp
; ( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds
((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds
not fp . c1,fp . c2 are_congruent_mod m ) )
((a1 * x1) - b1) mod m1 = 0 mod m1
by A7, Th12;
then
(a1 * x1) - b1, 0 are_congruent_mod m1
by A9, NAT_D:64;
then
((a1 * x1) - b1) * l,0 * l are_congruent_mod m1 * l
by Th10;
then A23:
((a * x1) - b) mod m = 0 mod m
by A3, A4, A6, NAT_D:64;
for c being Element of NAT st c in dom fp holds
((a * (fp . c)) - b) mod m = 0
hence
( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds
((a * (fp . c)) - b) mod m = 0 ) & ( for c1, c2 being Element of NAT st c1 in dom fp & c2 in dom fp & c1 <> c2 holds
not fp . c1,fp . c2 are_congruent_mod m ) )
by A8, A10; verum