let u, v be Integer; for m being CR_Sequence
for i being Nat st i in dom m holds
to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
let m be CR_Sequence; for i being Nat st i in dom m holds
to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
let i be Nat; ( i in dom m implies to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i )
set z = to_int (((mod (u,m)) - (mod (v,m))),m);
set c = the CR_coefficients of m;
A1:
len (mod (u,m)) = len m
by Def3;
len (mod (v,m)) = len m
by Def3;
then A2:
len ((mod (u,m)) - (mod (v,m))) = len m
by A1, Lm3;
then
to_int (((mod (u,m)) - (mod (v,m))),m) = (Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m)
by Def5;
then
(to_int (((mod (u,m)) - (mod (v,m))),m)) mod (Product m) = (Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m)) mod (Product m)
by NAT_D:65;
then A3:
to_int (((mod (u,m)) - (mod (v,m))),m), Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod Product m
by NAT_D:64;
assume A4:
i in dom m
; to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
then
ex y being Integer st y * (m . i) = Product m
by Th10;
then A5:
to_int (((mod (u,m)) - (mod (v,m))),m), Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m) are_congruent_mod m . i
by A3, INT_1:20;
Sum (((mod (u,m)) - (mod (v,m))) (#) the CR_coefficients of m),((mod (u,m)) - (mod (v,m))) . i are_congruent_mod m . i
by A4, A2, Th29;
then A6:
to_int (((mod (u,m)) - (mod (v,m))),m),((mod (u,m)) - (mod (v,m))) . i are_congruent_mod m . i
by A5, INT_1:15;
((mod (u,m)) - (mod (v,m))) . i,u - v are_congruent_mod m . i
by A4, Lm10;
hence
to_int (((mod (u,m)) - (mod (v,m))),m),u - v are_congruent_mod m . i
by A6, INT_1:15; verum