let x, y be Integer; :: thesis: for fp being FinSequence of NAT st ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds

(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds

fp . b > 0 ) holds

for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds

x,y are_congruent_mod Product fp

let fp be FinSequence of NAT ; :: thesis: ( ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds

(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds

fp . b > 0 ) implies for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds

x,y are_congruent_mod Product fp )

assume that

A1: for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds

(fp . b) gcd (fp . c) = 1 and

A2: for b being Element of NAT st b in dom fp holds

fp . b > 0 ; :: thesis: for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds

x,y are_congruent_mod Product fp

let fp1 be FinSequence of NAT ; :: thesis: ( ( for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) implies x,y are_congruent_mod Product fp )

assume A3: for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ; :: thesis: x,y are_congruent_mod Product fp

(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds

fp . b > 0 ) holds

for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds

x,y are_congruent_mod Product fp

let fp be FinSequence of NAT ; :: thesis: ( ( for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds

(fp . b) gcd (fp . c) = 1 ) & ( for b being Element of NAT st b in dom fp holds

fp . b > 0 ) implies for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds

x,y are_congruent_mod Product fp )

assume that

A1: for b, c being Element of NAT st b in dom fp & c in dom fp & b <> c holds

(fp . b) gcd (fp . c) = 1 and

A2: for b being Element of NAT st b in dom fp holds

fp . b > 0 ; :: thesis: for fp1 being FinSequence of NAT st ( for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) holds

x,y are_congruent_mod Product fp

let fp1 be FinSequence of NAT ; :: thesis: ( ( for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ) implies x,y are_congruent_mod Product fp )

assume A3: for b being Element of NAT st b in dom fp holds

( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) ; :: thesis: x,y are_congruent_mod Product fp

per cases
( x >= y or x < y )
;

end;

suppose
x >= y
; :: thesis: x,y are_congruent_mod Product fp

then
x - y in NAT
by INT_1:3, XREAL_1:48;

then reconsider k = x - y as Nat ;

for b being Element of NAT st b in dom fp holds

fp . b divides k

hence x,y are_congruent_mod Product fp ; :: thesis: verum

end;then reconsider k = x - y as Nat ;

for b being Element of NAT st b in dom fp holds

fp . b divides k

proof

then
Product fp divides k
by A1, Th38;
let b be Element of NAT ; :: thesis: ( b in dom fp implies fp . b divides k )

assume A4: b in dom fp ; :: thesis: fp . b divides k

A5: fp . b > 0 by A2, A4;

(y - (fp1 . b)) mod (fp . b) = 0 by A3, A4;

then A6: fp . b divides y - (fp1 . b) by A5, INT_1:62;

(x - (fp1 . b)) mod (fp . b) = 0 by A3, A4;

then fp . b divides x - (fp1 . b) by A5, INT_1:62;

then fp . b divides (x - (fp1 . b)) - (y - (fp1 . b)) by A6, Lm4;

then consider i being Integer such that

A7: x - y = (fp . b) * i ;

i >= 0

then reconsider i = i as Nat ;

thus fp . b divides k by A7; :: thesis: verum

end;assume A4: b in dom fp ; :: thesis: fp . b divides k

A5: fp . b > 0 by A2, A4;

(y - (fp1 . b)) mod (fp . b) = 0 by A3, A4;

then A6: fp . b divides y - (fp1 . b) by A5, INT_1:62;

(x - (fp1 . b)) mod (fp . b) = 0 by A3, A4;

then fp . b divides x - (fp1 . b) by A5, INT_1:62;

then fp . b divides (x - (fp1 . b)) - (y - (fp1 . b)) by A6, Lm4;

then consider i being Integer such that

A7: x - y = (fp . b) * i ;

i >= 0

proof

then
i in NAT
by INT_1:3;
assume
i < 0
; :: thesis: contradiction

then k < 0 by A2, A4, A7, XREAL_1:132;

hence contradiction ; :: thesis: verum

end;then k < 0 by A2, A4, A7, XREAL_1:132;

hence contradiction ; :: thesis: verum

then reconsider i = i as Nat ;

thus fp . b divides k by A7; :: thesis: verum

hence x,y are_congruent_mod Product fp ; :: thesis: verum

suppose
x < y
; :: thesis: x,y are_congruent_mod Product fp

then
y - x > 0
by XREAL_1:50;

then y - x in NAT by INT_1:3;

then reconsider k = y - x as Nat ;

for b being Element of NAT st b in dom fp holds

fp . b divides k

then y,x are_congruent_mod Product fp ;

hence x,y are_congruent_mod Product fp by INT_1:14; :: thesis: verum

end;then y - x in NAT by INT_1:3;

then reconsider k = y - x as Nat ;

for b being Element of NAT st b in dom fp holds

fp . b divides k

proof

then
Product fp divides k
by A1, Th38;
let b be Element of NAT ; :: thesis: ( b in dom fp implies fp . b divides k )

assume A8: b in dom fp ; :: thesis: fp . b divides k

A9: fp . b > 0 by A2, A8;

(y - (fp1 . b)) mod (fp . b) = 0 by A3, A8;

then A10: fp . b divides y - (fp1 . b) by A9, INT_1:62;

(x - (fp1 . b)) mod (fp . b) = 0 by A3, A8;

then fp . b divides x - (fp1 . b) by A9, INT_1:62;

then fp . b divides (y - (fp1 . b)) - (x - (fp1 . b)) by A10, Lm4;

then consider i being Integer such that

A11: y - x = (fp . b) * i ;

k = (fp . b) * i by A11;

then i >= 0 by A2, A8, XREAL_1:132;

then i in NAT by INT_1:3;

then reconsider i = i as Nat ;

thus fp . b divides k by A11; :: thesis: verum

end;assume A8: b in dom fp ; :: thesis: fp . b divides k

A9: fp . b > 0 by A2, A8;

(y - (fp1 . b)) mod (fp . b) = 0 by A3, A8;

then A10: fp . b divides y - (fp1 . b) by A9, INT_1:62;

(x - (fp1 . b)) mod (fp . b) = 0 by A3, A8;

then fp . b divides x - (fp1 . b) by A9, INT_1:62;

then fp . b divides (y - (fp1 . b)) - (x - (fp1 . b)) by A10, Lm4;

then consider i being Integer such that

A11: y - x = (fp . b) * i ;

k = (fp . b) * i by A11;

then i >= 0 by A2, A8, XREAL_1:132;

then i in NAT by INT_1:3;

then reconsider i = i as Nat ;

thus fp . b divides k by A11; :: thesis: verum

then y,x are_congruent_mod Product fp ;

hence x,y are_congruent_mod Product fp by INT_1:14; :: thesis: verum