let a, b, m be Integer; :: thesis: ( 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 ; :: thesis: 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 H_{1}( 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 = H_{1}(c) ) )
from FINSEQ_1:sch 2();

for c being Nat st c in dom fp holds

fp . c in INT

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

((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

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

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

consider fp being FinSequence such that

A8: ( len fp = l & ( for c being Nat st c in dom fp holds

fp . c = H

for c being Nat st c in dom fp holds

fp . c in INT

proof

then reconsider fp = fp as FinSequence of INT by FINSEQ_2:12;
let c be Nat; :: thesis: ( c in dom fp implies fp . c in INT )

assume c in dom fp ; :: thesis: fp . c in INT

then fp . c = x1 + ((c - 1) * m1) by A8;

hence fp . c in INT by INT_1:def 2; :: thesis: verum

end;assume c in dom fp ; :: thesis: fp . c in INT

then fp . c = x1 + ((c - 1) * m1) by A8;

hence fp . c in INT by INT_1:def 2; :: thesis: verum

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

take
fp
; :: thesis: ( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds
let c1, c2 be Element of NAT ; :: thesis: ( 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 ; :: thesis: not fp . c1,fp . c2 are_congruent_mod m

assume A14: fp . c1,fp . c2 are_congruent_mod m ; :: thesis: 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; :: thesis: verum

end;assume that

A11: c1 in dom fp and

A12: c2 in dom fp and

A13: c1 <> c2 ; :: thesis: not fp . c1,fp . c2 are_congruent_mod m

assume A14: fp . c1,fp . c2 are_congruent_mod m ; :: thesis: 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; :: thesis: verum

((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

proof

hence
( len fp = a gcd m & ( for c being Element of NAT st c in dom fp holds
let c be Element of NAT ; :: thesis: ( c in dom fp implies ((a * (fp . c)) - b) mod m = 0 )

assume c in dom fp ; :: thesis: ((a * (fp . c)) - b) mod m = 0

hence ((a * (fp . c)) - b) mod m = ((a * (x1 + ((c - 1) * m1))) - b) mod m by A8

.= (((a * x1) - b) + ((a1 * (c - 1)) * m)) mod m by A3, A4

.= ((a * x1) - b) mod m by NAT_D:61

.= 0 by A23, Th12 ;

:: thesis: verum

end;assume c in dom fp ; :: thesis: ((a * (fp . c)) - b) mod m = 0

hence ((a * (fp . c)) - b) mod m = ((a * (x1 + ((c - 1) * m1))) - b) mod m by A8

.= (((a * x1) - b) + ((a1 * (c - 1)) * m)) mod m by A3, A4

.= ((a * x1) - b) mod m by NAT_D:61

.= 0 by A23, Th12 ;

:: thesis: verum

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