let s be FinSequence of NAT ; :: thesis: for n being Nat st n > 1 & len s = n - 1 & ( for i being Nat st i in dom s holds
s . i = i |^ n ) & n is odd holds
n divides Sum s
let n be Nat; :: thesis: ( n > 1 & len s = n - 1 & ( for i being Nat st i in dom s holds
s . i = i |^ n ) & n is odd implies n divides Sum s )
assume that
n: ( n > 1 & len s = n - 1 ) and
s: for i being Nat st i in dom s holds
s . i = i |^ n ; :: thesis: ( not n is odd or n divides Sum s )
rng s c= REAL ;
then reconsider s0 = s as FinSequence of REAL by FINSEQ_1:def 4;
reconsider ser = Sum s as Nat by TARSKI:1;
d: dom s = dom (Rev s) by FINSEQ_5:57;
d2: dom (s + (Rev s)) = (dom s) /\ (dom (Rev s)) by VALUED_1:def 1
.= dom s by d ;
then Seg (len (s + (Rev s))) = dom s by FINSEQ_1:def 3
.= Seg (len s) by FINSEQ_1:def 3 ;
then l1: len s0 = len (s0 + (Rev s0)) by FINSEQ_1:6;
Seg (len s) = dom (Rev s) by d, FINSEQ_1:def 3;
then l2: len s0 = len (Rev s0) by FINSEQ_1:def 3;
for k being Nat st k in dom s0 holds
(s0 + (Rev s0)) . k = (s0 . k) + ((Rev s0) . k) by d2, VALUED_1:def 1;
then ss: Sum (s0 + (Rev s0)) = (Sum s0) + (Sum (Rev s0)) by l1, l2, ENTROPY1:7
.= (Sum s) + (Sum s) by POLYNOM3:3
.= 2 * (Sum s) ;
rng (s + (Rev s)) c= NAT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in rng (s + (Rev s)) or o in NAT )
assume o in rng (s + (Rev s)) ; :: thesis: o in NAT
then consider a being object such that
a: ( a in dom (s + (Rev s)) & o = (s + (Rev s)) . a ) by FUNCT_1:def 3;
reconsider a = a as Nat by a;
o = (s . a) + ((Rev s) . a) by a, VALUED_1:def 1;
hence o in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then reconsider sr = s + (Rev s) as FinSequence of NAT by FINSEQ_1:def 4;
thus ( n is odd implies n divides Sum s ) :: thesis: verum

proof

assume no: n is odd ; :: thesis: n divides Sum s
2 |^ 1 = 2 by NEWTON:5;
then 2c: 2,n are_coprime by NAT_5:3, no;

now :: thesis: for k being Nat st k in dom sr holds
n divides sr . k

let k be Nat; :: thesis: ( k in dom sr implies n divides sr . k )
assume k: k in dom sr ; :: thesis: n divides sr . k
then serek: sr . k = (s . k) + ((Rev s) . k) by VALUED_1:def 1
.= (k |^ n) + ((Rev s) . k) by d2, k, s
.= (k |^ n) + (s . (((len s) - k) + 1)) by FINSEQ_5:58, k, d2
.= (k |^ n) + (s . (n - k)) by n ;
k in Seg (len s) by k, d2, FINSEQ_1:def 3;
then kk: ( 1 <= k & k <= n - 1 ) by FINSEQ_1:1, n;
then nk: n - k <= n - 1 by XREAL_1:10;
k + (1 - k) <= (n - 1) + (1 - k) by kk, XREAL_1:6;
then jk: 1 <= n - k ;
then reconsider nik = n - k as Nat ;
nik in Seg (len s) by n, jk, nk;
then n - k in dom s by FINSEQ_1:def 3;
then sr . k = (k |^ n) + ((n - k) |^ n) by serek, s;
hence n divides sr . k by no, lemmandiv; :: thesis: verum

end;

then n divides Sum sr by NEWTON04:80;
then n divides 2 * (Sum s) by ss;
then n divides ser by 2c, EULER_1:13;
hence n divides Sum s ; :: thesis: verum

end;