let n, k be Nat; :: thesis: ( n is odd implies n divides (k |^ n) + ((n - k) |^ n) )
assume no: n is odd ; :: thesis: n divides (k |^ n) + ((n - k) |^ n)
then reconsider p = n as positive Nat ;
kk: (k |^ p) + ((p + (- k)) |^ p) = (k |^ p) + (Sum ((p,(- k)) In_Power p)) by NEWTON:30
.= (k |^ p) + (((p |^ p) + ((- k) |^ p)) + (Sum ((((p,(- k)) In_Power p) | p) /^ 1))) by lemman02
.= (k |^ p) + (((p |^ p) + (- (k |^ p))) + (Sum ((((p,(- k)) In_Power p) | p) /^ 1))) by no, POWER:2
.= (p |^ p) + (Sum ((((p,(- k)) In_Power p) | p) /^ 1)) ;
pp: p divides p |^ p by NAT_3:3;
reconsider S = Sum ((((p,(- k)) In_Power p) | p) /^ 1) as Integer ;
reconsider f = (((p,(- k)) In_Power p) | p) /^ 1 as INT -valued FinSequence ;

now :: thesis: for o being Nat st o in dom f holds
n divides f . o

let o be Nat; :: thesis: ( o in dom f implies n divides f . o )
assume o: o in dom f ; :: thesis: n divides f . o
then f <> {} ;
then 1 <= len (((p,(- k)) In_Power p) | p) by RFINSEQ:def 1;
then rf: ( len f = (len (((p,(- k)) In_Power p) | p)) - 1 & ( for l being Nat st l in dom f holds
f . l = (((p,(- k)) In_Power p) | p) . (l + 1) ) ) by RFINSEQ:def 1;
elen: ( len ((p,(- k)) In_Power p) = n + 1 & ( for i, l, m being Nat st i in dom ((p,(- k)) In_Power p) & m = i - 1 & l = n - m holds
((p,(- k)) In_Power p) . i = ((n choose m) * (p |^ l)) * ((- k) |^ m) ) ) by NEWTON:def 4;
x: 0 + 1 <= o + 1 by XREAL_1:6;
pz: p + 0 <= n + 1 by XREAL_1:6;
len (((p,(- k)) In_Power p) | p) = p by elen, pz, FINSEQ_1:17;
then lp: len f = p - 1 by rf;
o in Seg (len f) by o, FINSEQ_1:def 3;
then o <= p - 1 by lp, FINSEQ_1:1;
then op: o + 1 <= (p - 1) + 1 by XREAL_1:6;
then el: o + 1 in Seg p by x;
set i = o + 1;
o + 1 < p + 1 by NAT_1:13, op;
then o + 1 in Seg (len ((p,(- k)) In_Power p)) by x, elen;
then i: o + 1 in dom ((p,(- k)) In_Power p) by FINSEQ_1:def 3;
reconsider m = (o + 1) - 1 as Nat ;
po: p - o >= (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; :: thesis: verum

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) ; :: thesis: verum