= o+1-o by op,XREAL_1:9; then reconsider l=n-m as Nat; fo: f.o = (((p,-k) In_Power p)|p).(o+1) by o,rf .= ((p,-k) In_Power p).(o+1) by el,FUNCT_1:49 .= (n choose m) * p|^l * (-k)|^m by elen,i .= p|^l * ((n choose m) * (-k)|^m); p divides p|^l by po,NAT_3:3; hence n divides f.o by fo,INT_2:2; end; then n divides Sum f by NEWTON04:80; then n divides k|^n + (n+(-k))|^n by kk,pp,WSIERP_1:4; hence n divides k|^n + (n-k)|^n; end; begin :: Problem 10 theorem for s being FinSequence of NAT, n being Nat st n>1 & len s=n-1 & for i being Nat st i in dom s holds s.i=i|^n holds n is odd implies n divides Sum s proof let s be FinSequence of NAT, n be Nat such that n: n>1 & len s=n-1 and s: for i being Nat st i in dom s holds s.i=i|^n; 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; assume o in rng (s+Rev s); 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 as Nat by a; o=s.a+(Rev s).a by a,VALUED_1:def 1; hence o in NAT by ORDINAL1:def 12; 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 proof assume no: n is odd; 2|^1=2 by NEWTON:5; then 2c: 2,n are_coprime by NAT_5:3,no; now let k be Nat; assume k: k in dom sr; 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; 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; end; end;