let u be INT -valued FinSequence; for m being CR_Sequence st len m = len u holds
for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
let m be CR_Sequence; ( len m = len u implies for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m )
assume A1:
len u = len m
; for c1, c2 being CR_coefficients of m holds Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
let c1, c2 be CR_coefficients of m; Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
set s1 = (Sum (u (#) c1)) mod (Product m);
set s2 = (Sum (u (#) c2)) mod (Product m);
A2:
(Sum (u (#) c1)) mod (Product m) < Product m
by NAT_D:62;
A3:
for i being Nat st i in dom m holds
(Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i
proof
let i be
Nat;
( i in dom m implies (Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i )
((Sum (u (#) c1)) mod (Product m)) mod (Product m) = (Sum (u (#) c1)) mod (Product m)
by NAT_D:65;
then A4:
(Sum (u (#) c1)) mod (Product m),
Sum (u (#) c1) are_congruent_mod Product m
by NAT_D:64;
assume A5:
i in dom m
;
(Sum (u (#) c1)) mod (Product m),u . i are_congruent_mod m . i
then
m . i in rng m
by FUNCT_1:3;
then A6:
m . i > 0
by PARTFUN3:def 1;
ex
z being
Integer st
z * (m . i) = Product m
by A5, Th10;
then
(Sum (u (#) c1)) mod (Product m),
Sum (u (#) c1) are_congruent_mod m . i
by A4, INT_1:20;
then A7:
((Sum (u (#) c1)) mod (Product m)) mod (m . i) = (Sum (u (#) c1)) mod (m . i)
by NAT_D:64;
Sum (u (#) c1),
u . i are_congruent_mod m . i
by A1, A5, Th29;
then
(Sum (u (#) c1)) mod (m . i) = (u . i) mod (m . i)
by NAT_D:64;
hence
(Sum (u (#) c1)) mod (Product m),
u . i are_congruent_mod m . i
by A6, A7, NAT_D:64;
verum
end;
A8:
0 <= (Sum (u (#) c2)) mod (Product m)
by NAT_D:62;
A9:
for i being Nat st i in dom m holds
(Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i
proof
let i be
Nat;
( i in dom m implies (Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i )
((Sum (u (#) c2)) mod (Product m)) mod (Product m) = (Sum (u (#) c2)) mod (Product m)
by NAT_D:65;
then A10:
(Sum (u (#) c2)) mod (Product m),
Sum (u (#) c2) are_congruent_mod Product m
by NAT_D:64;
assume A11:
i in dom m
;
(Sum (u (#) c2)) mod (Product m),u . i are_congruent_mod m . i
then
m . i in rng m
by FUNCT_1:3;
then A12:
m . i > 0
by PARTFUN3:def 1;
ex
z being
Integer st
z * (m . i) = Product m
by A11, Th10;
then
(Sum (u (#) c2)) mod (Product m),
Sum (u (#) c2) are_congruent_mod m . i
by A10, INT_1:20;
then A13:
((Sum (u (#) c2)) mod (Product m)) mod (m . i) = (Sum (u (#) c2)) mod (m . i)
by NAT_D:64;
Sum (u (#) c2),
u . i are_congruent_mod m . i
by A1, A11, Th29;
then
(Sum (u (#) c2)) mod (m . i) = (u . i) mod (m . i)
by NAT_D:64;
hence
(Sum (u (#) c2)) mod (Product m),
u . i are_congruent_mod m . i
by A12, A13, NAT_D:64;
verum
end;
A14:
(Sum (u (#) c2)) mod (Product m) < Product m
by NAT_D:62;
0 <= (Sum (u (#) c1)) mod (Product m)
by NAT_D:62;
then
(Sum (u (#) c1)) mod (Product m) = (Sum (u (#) c2)) mod (Product m)
by A3, A9, A2, A8, A14, Lm9;
hence
Sum (u (#) c1), Sum (u (#) c2) are_congruent_mod Product m
by NAT_D:64; verum