let s be FinSequence of NAT ; 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; ( 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
; ( 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
then reconsider sr = s + (Rev s) as FinSequence of NAT by FINSEQ_1:def 4;
thus
( n is odd implies n divides Sum s )
verumproof
assume no:
n is
odd
;
n divides Sum s
2
|^ 1
= 2
by NEWTON:5;
then 2c:
2,
n are_coprime
by NAT_5:3, no;
now for k being Nat st k in dom sr holds
n divides sr . klet k be
Nat;
( k in dom sr implies n divides sr . k )assume k:
k in dom sr
;
n divides sr . kthen 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;
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
;
verum
end;