let u, v be Integer; for m being CR_Sequence st 0 <= u * v & u * v < Product m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v
let m be CR_Sequence; ( 0 <= u * v & u * v < Product m implies to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v )
assume that
A1:
0 <= u * v
and
A2:
u * v < Product m
; to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v
set z = to_int (((mod (u,m)) (#) (mod (v,m))),m);
A3:
for i being Nat st i in dom m holds
u * v,(mod ((u * v),m)) . i are_congruent_mod m . i
by Th32;
A4:
len (mod ((u * v),m)) = len m
by Def3;
A5:
for i being Nat st i in dom m holds
to_int (((mod (u,m)) (#) (mod (v,m))),m),(mod ((u * v),m)) . i are_congruent_mod m . i
proof
let i be
Nat;
( i in dom m implies to_int (((mod (u,m)) (#) (mod (v,m))),m),(mod ((u * v),m)) . i are_congruent_mod m . i )
assume A6:
i in dom m
;
to_int (((mod (u,m)) (#) (mod (v,m))),m),(mod ((u * v),m)) . i are_congruent_mod m . i
then
to_int (
((mod (u,m)) (#) (mod (v,m))),
m),
u * v are_congruent_mod m . i
by Th37;
then A7:
(to_int (((mod (u,m)) (#) (mod (v,m))),m)) mod (m . i) = (u * v) mod (m . i)
by NAT_D:64;
dom (mod ((u * v),m)) =
Seg (len m)
by A4, FINSEQ_1:def 3
.=
dom m
by FINSEQ_1:def 3
;
then A8:
(mod ((u * v),m)) . i = (u * v) mod (m . i)
by A6, Def3;
m . i in rng m
by A6, FUNCT_1:3;
then A9:
m . i > 0
by PARTFUN3:def 1;
then
m . i is
Element of
NAT
by INT_1:3;
then
(u * v) mod (m . i) = ((u * v) mod (m . i)) mod (m . i)
by NAT_D:65;
hence
to_int (
((mod (u,m)) (#) (mod (v,m))),
m),
(mod ((u * v),m)) . i are_congruent_mod m . i
by A8, A7, A9, NAT_D:64;
verum
end;
A10:
len (mod (u,m)) = len m
by Def3;
len (mod (v,m)) = len m
by Def3;
then A11:
len ((mod (u,m)) (#) (mod (v,m))) = len m
by A10, Lm4;
then A12:
to_int (((mod (u,m)) (#) (mod (v,m))),m) < Product m
by Th31;
0 <= to_int (((mod (u,m)) (#) (mod (v,m))),m)
by A11, Th31;
hence
to_int (((mod (u,m)) (#) (mod (v,m))),m) = u * v
by A1, A2, A3, A12, A5, Lm9; verum