let x, y be Integer; :: thesis: for fp being FinSequence of NAT st len fp >= 2 & ( 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 len fp1 = len fp & ( 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: ( len fp >= 2 & ( 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 len fp1 = len fp & ( 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 A1: ( len fp >= 2 & ( 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 ) ) ; :: thesis: for fp1 being FinSequence of NAT st len fp1 = len fp & ( 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: ( len fp1 = len fp & ( 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 A2: ( len fp1 = len fp & ( 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 ) ;

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

then x - y in NAT by INT_1:16, XREAL_1:50;
then reconsider k = x - y as Nat ;
A3: for b being Element of NAT st b in dom fp holds
fp . b divides k

proof

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: ( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) by A2, A4;
fp . b > 0 by A1, A4;
then ( fp . b divides x - (fp1 . b) & fp . b divides y - (fp1 . b) ) by A5, INT_1:89;
then fp . b divides (x - (fp1 . b)) - (y - (fp1 . b)) by Lm4;
then consider i being Integer such that
A6: x - y = (fp . b) * i by INT_1:def 9;
i >= 0

proof

assume A7: i < 0 ; :: thesis: contradiction
fp . b > 0 by A1, A4;
then k < 0 by A6, A7, XREAL_1:134;
hence contradiction ; :: thesis: verum

end;

then i in NAT by INT_1:16;
then reconsider i = i as Nat ;
( k is Nat & fp . b is Nat & i is Nat ) ;
hence fp . b divides k by A6, NAT_D:def 3; :: thesis: verum

end;

Product fp divides k by A1, A3, Th38;
then consider l being Nat such that
A8: k = (Product fp) * l by NAT_D:def 3;
Product fp divides x - y by A8, INT_1:def 9;
hence x,y are_congruent_mod Product fp by INT_2:19; :: thesis: verum

end;

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

then y - x > 0 by XREAL_1:52;
then y - x in NAT by INT_1:16;
then reconsider k = y - x as Nat ;
A9: for b being Element of NAT st b in dom fp holds
fp . b divides k

proof

let b be Element of NAT ; :: thesis: ( b in dom fp implies fp . b divides k )
assume A10: b in dom fp ; :: thesis: fp . b divides k
A11: ( (x - (fp1 . b)) mod (fp . b) = 0 & (y - (fp1 . b)) mod (fp . b) = 0 ) by A2, A10;
fp . b > 0 by A1, A10;
then ( fp . b divides x - (fp1 . b) & fp . b divides y - (fp1 . b) ) by A11, INT_1:89;
then fp . b divides (y - (fp1 . b)) - (x - (fp1 . b)) by Lm4;
then consider i being Integer such that
A12: y - x = (fp . b) * i by INT_1:def 9;
A13: k = (fp . b) * i by A12;
i >= 0 by A13, A1, A10, XREAL_1:134;
then i in NAT by INT_1:16;
then reconsider i = i as Nat ;
( k is Nat & fp . b is Nat & i is Nat ) ;
hence fp . b divides k by A12, NAT_D:def 3; :: thesis: verum

end;

Product fp divides k by A1, A9, Th38;
then consider l being Nat such that
A15: k = (Product fp) * l by NAT_D:def 3;
Product fp divides y - x by A15, INT_1:def 9;
then y,x are_congruent_mod Product fp by INT_2:19;
hence x,y are_congruent_mod Product fp by INT_1:35; :: thesis: verum

end;

end;