let m be Nat; for f being FinSequence of NAT st m <> 0 holds
(Product (f mod m)) mod m = (Product f) mod m
defpred S1[ Nat] means for f being FinSequence of NAT st m <> 0 & len f = $1 holds
(Product (f mod m)) mod m = (Product f) mod m;
let f be FinSequence of NAT ; ( m <> 0 implies (Product (f mod m)) mod m = (Product f) mod m )
assume A1:
m <> 0
; (Product (f mod m)) mod m = (Product f) mod m
A2:
len f is Element of NAT
;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
let f be
FinSequence of
NAT ;
( m <> 0 & len f = n + 1 implies (Product (f mod m)) mod m = (Product f) mod m )
assume that A5:
m <> 0
and A6:
len f = n + 1
;
(Product (f mod m)) mod m = (Product f) mod m
reconsider fn =
f | n as
FinSequence of
NAT ;
A7:
len fn = n
by A6, FINSEQ_1:59, NAT_1:11;
A8:
len (f mod m) = n + 1
by A6, Def1;
then A9:
len ((f mod m) | n) = n
by FINSEQ_1:59, NAT_1:11;
A10:
n <= len f
by A6, NAT_1:11;
A11:
for
i being
Nat st 1
<= i &
i <= len ((f mod m) | n) holds
((f mod m) | n) . i = (fn mod m) . i
proof
let i be
Nat;
( 1 <= i & i <= len ((f mod m) | n) implies ((f mod m) | n) . i = (fn mod m) . i )
assume that A12:
1
<= i
and A13:
i <= len ((f mod m) | n)
;
((f mod m) | n) . i = (fn mod m) . i
A14:
(f | n) . i = (f | (Seg n)) . i
by FINSEQ_1:def 15;
A15:
i in Seg n
by A9, A12, A13, FINSEQ_1:1;
then A16:
((f mod m) | (Seg n)) . i = (f mod m) . i
by FUNCT_1:49;
i <= len f
by A10, A9, A13, XXREAL_0:2;
then A17:
i in dom f
by A12, FINSEQ_3:25;
i in dom fn
by A7, A9, A12, A13, FINSEQ_3:25;
then (fn mod m) . i =
(fn . i) mod m
by Def1
.=
(f . i) mod m
by A15, A14, FUNCT_1:49
.=
(f mod m) . i
by A17, Def1
;
hence
((f mod m) | n) . i = (fn mod m) . i
by A16, FINSEQ_1:def 15;
verum
end;
0 + 1
<= n + 1
by NAT_1:13;
then
n + 1
in dom f
by A6, FINSEQ_3:25;
then A18:
(f mod m) . (n + 1) = (f . (n + 1)) mod m
by Def1;
len ((f mod m) | n) = len (fn mod m)
by A7, A9, Def1;
then
(f mod m) | n = fn mod m
by A11, FINSEQ_1:14;
then
f mod m = (fn mod m) ^ <*((f . (n + 1)) mod m)*>
by A8, A18, RFINSEQ:7;
then A19:
(Product (f mod m)) mod m =
((Product (fn mod m)) * ((f . (n + 1)) mod m)) mod m
by RVSUM_1:96
.=
(((Product (fn mod m)) mod m) * (((f . (n + 1)) mod m) mod m)) mod m
by Th9
.=
(((Product fn) mod m) * (((f . (n + 1)) mod m) mod m)) mod m
by A4, A5, A7
.=
(((Product fn) mod m) * ((f . (n + 1)) mod m)) mod m
by Th5
;
(Product f) mod m =
(Product (fn ^ <*(f . (n + 1))*>)) mod m
by A6, RFINSEQ:7
.=
((Product fn) * (f . (n + 1))) mod m
by RVSUM_1:96
;
hence
(Product (f mod m)) mod m = (Product f) mod m
by A19, Th9;
verum
end;
A20:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A20, A3);
hence
(Product (f mod m)) mod m = (Product f) mod m
by A1, A2; verum