let m be Integer; for f, fr being FinSequence of INT st len f = len fr & ( for d being Nat st d in dom f holds
f . d, - (fr . d) are_congruent_mod m ) holds
Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m
defpred S1[ Nat] means for f, fr being FinSequence of INT st len f = $1 & len f = len fr & ( for d being Nat st d in dom f holds
f . d, - (fr . d) are_congruent_mod m ) holds
Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m;
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
S1[
n + 1]
proof
let f,
fr be
FinSequence of
INT ;
( len f = n + 1 & len f = len fr & ( for d being Nat st d in dom f holds
f . d, - (fr . d) are_congruent_mod m ) implies Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m )
assume that A3:
len f = n + 1
and A4:
len f = len fr
and A5:
for
d being
Nat st
d in dom f holds
f . d,
- (fr . d) are_congruent_mod m
;
Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m
consider fr1 being
FinSequence of
INT ,
b being
Element of
INT such that A6:
fr = fr1 ^ <*b*>
by A3, A4, FINSEQ_2:19;
f <> {}
by A3;
then A7:
n + 1
in dom f
by A3, FINSEQ_5:6;
consider f1 being
FinSequence of
INT ,
a being
Element of
INT such that A8:
f = f1 ^ <*a*>
by A3, FINSEQ_2:19;
A9:
n + 1
= (len fr1) + 1
by A3, A4, A6, FINSEQ_2:16;
then A10:
fr . (n + 1) = b
by A6, FINSEQ_1:42;
A11:
n + 1
= (len f1) + 1
by A3, A8, FINSEQ_2:16;
then A12:
dom f1 = dom fr1
by A9, FINSEQ_3:29;
for
d being
Nat st
d in dom f1 holds
f1 . d,
- (fr1 . d) are_congruent_mod m
proof
let d be
Nat;
( d in dom f1 implies f1 . d, - (fr1 . d) are_congruent_mod m )
assume A13:
d in dom f1
;
f1 . d, - (fr1 . d) are_congruent_mod m
then A14:
f . d = f1 . d
by A8, FINSEQ_1:def 7;
fr . d = fr1 . d
by A6, A12, A13, FINSEQ_1:def 7;
hence
f1 . d,
- (fr1 . d) are_congruent_mod m
by A5, A8, A13, A14, FINSEQ_2:15;
verum
end;
then A15:
Product f1,
((- 1) |^ (len f1)) * (Product fr1) are_congruent_mod m
by A2, A11, A9;
f . (n + 1) = a
by A8, A11, FINSEQ_1:42;
then
a,
- b are_congruent_mod m
by A5, A7, A10;
then
(Product f1) * a,
(((- 1) |^ (len f1)) * (Product fr1)) * (- b) are_congruent_mod m
by A15, INT_1:18;
then
Product f,
(((- 1) |^ (len f1)) * (- 1)) * ((Product fr1) * b) are_congruent_mod m
by A8, RVSUM_1:96;
then
Product f,
((- 1) |^ ((len f1) + 1)) * ((Product fr1) * b) are_congruent_mod m
by NEWTON:6;
hence
Product f,
((- 1) |^ (len f)) * (Product fr) are_congruent_mod m
by A3, A6, A11, RVSUM_1:96;
verum
end;
hence
S1[
n + 1]
;
verum
end;
A16:
S1[ 0 ]
proof
let f,
fr be
FinSequence of
INT ;
( len f = 0 & len f = len fr & ( for d being Nat st d in dom f holds
f . d, - (fr . d) are_congruent_mod m ) implies Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m )
assume that A17:
len f = 0
and A18:
len f = len fr
;
( ex d being Nat st
( d in dom f & not f . d, - (fr . d) are_congruent_mod m ) or Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m )
A19:
f = <*> INT
by A17;
A20:
(- 1) |^ (len f) = 1
by A17, NEWTON:4;
fr = <*> INT
by A17, A18;
hence
( ex
d being
Nat st
(
d in dom f & not
f . d,
- (fr . d) are_congruent_mod m ) or
Product f,
((- 1) |^ (len f)) * (Product fr) are_congruent_mod m )
by A19, A20, INT_1:11;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A16, A1);
hence
for f, fr being FinSequence of INT st len f = len fr & ( for d being Nat st d in dom f holds
f . d, - (fr . d) are_congruent_mod m ) holds
Product f,((- 1) |^ (len f)) * (Product fr) are_congruent_mod m
; verum