let s be XFinSequence of NAT ; :: thesis:
let n be Nat; :: thesis:
assume that
n: ( n > 1 & len s = n - 1 ) and
s: for i being Nat st i in dom s holds
s . i = (i + 1) |^ n ; :: thesis:
reconsider n1 = n - 1 as Nat by n;
d: dom s = dom (Rev s) by AFINSQ_2:5;
d2: dom (s + (Rev s)) = (dom s) /\ (dom (Rev s)) by VALUED_1:def 1
.= dom s by d ;
reconsider ss = s as n1 -element complex-valued XFinSequence by n, CARD_1:def 7;
reconsider rs = Rev s as n1 -element complex-valued XFinSequence by n, CARD_1:def 7, d;
ss: Sum (ss + rs) = (Sum s) + (Sum (Rev s)) by RVSUM_4:49
.= (Sum s) + (Sum s) by AFINSQ_2:69
.= 2 * (Sum s) ;
rng (s + (Rev s)) c= NAT

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in rng (s + (Rev s)) ; :: thesis:
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:

end;

then reconsider sr = s + (Rev s) as XFinSequence of NAT by RELAT_1:def 19;
thus ( n is odd implies n divides Sum s ) :: thesis:

proof

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

now :: thesis:

let k be Nat; :: thesis:
assume k: k in dom sr ; :: thesis:
then serek: sr . k = (s . k) + ((Rev s) . k) by VALUED_1:def 1
.= ((k + 1) |^ n) + ((Rev s) . k) by d2, k, s
.= ((k + 1) |^ n) + (s . ((len s) - (k + 1))) by k, d, d2, AFINSQ_2:def 1
.= ((k + 1) |^ n) + (s . ((n - k) - 2)) by n ;
k < n - 1 by n, AFINSQ_1:66, k, d2;
then k + 2 < (n - 1) + 2 by XREAL_1:6;
then k + 2 < n + 1 ;
then k + 2 <= n by NAT_1:13;
then reconsider nik = n - (k + 2) as Nat by NAT_1:21;
1 < k + 2 by XREAL_1:40;
then nik < n - 1 by XREAL_1:10;
then nik in dom s by n, AFINSQ_1:66;
then sr . k = ((k + 1) |^ n) + ((nik + 1) |^ n) by serek, s
.= ((k + 1) |^ n) + ((n - (k + 1)) |^ n) ;
hence n divides sr . k by no, lemmandiv; :: thesis:

end;

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

end;

thus ( n divides Sum s implies n is odd ) :: thesis:

proof

assume that
nd: n divides Sum s and
e: n is even ; :: thesis:
reconsider ne = n as even Nat by e;
consider n2 being Nat such that
n2: n = 2 * n2 by ABIAN:def 2, e;
set h = 2 |-count n;
2 divides n by n2, INT_1:def 3;
then 2 |-count n <> 0 by n, NAT_3:27;
then hen: 2 |-count n > 0 ;
then reconsider hj = (2 |-count n) - 1 as Nat by NAT_1:20;
dwah: 2 |^ (2 |-count n) divides n by n, NAT_3:def 7;
then 2n: 2 |^ (2 |-count n) <= n by n, INT_2:27;
2 |^ (2 |-count n) >= 2 |-count n by NAT_3:2;
then 2 |-count n <= n by 2n, XXREAL_0:2;
then hn2: 2 |^ (2 |-count n) divides 2 |^ n by NEWTON:89;
deffunc H₁( Nat) -> Element of omega = (s . $1) mod (2 |^ (2 |-count n));
consider sm being XFinSequence of NAT such that
sm: ( len sm = len s & ( for j being Nat st j in len s holds
sm . j = H₁(j) ) ) from AFINSQ_2:sch 1();
ss: (Sum s) mod (2 |^ (2 |-count n)) = (Sum sm) mod (2 |^ (2 |-count n)) by sm, NUMERAL2:17;
set B1 = OddNAT ;
set B2 = EvenNAT ;

now :: thesis:

let o be object ; :: thesis:
assume o: o in dom (SubXFinS (sm,OddNAT)) ; :: thesis:
then reconsider k = o as Nat ;
reconsider ds = dom sm as finite natural-membered set ;
reconsider BB = OddNAT /\ ds as finite natural-membered set ;
kid: k in dom (Sgm0 BB) by o, NUMERAL2:6;
SX: (SubXFinS (sm,OddNAT)) . o = sm . ((Sgm0 BB) . k) by o, FUNCT_1:12
.= sm . ((2 * k) + 1) by kid, NUMERAL2:13 ;
thus (SubXFinS (sm,OddNAT)) . o = 0 :: thesis:

proof

per cases ) + 1 in dom s or not (2 * k) + 1 in dom s ) ;

suppose dk: (2 * k) + 1 in dom s ; :: thesis:

then sf: (SubXFinS (sm,OddNAT)) . o = (s . ((2 * k) + 1)) mod (2 |^ (2 |-count n)) by SX, sm
.= ((((2 * k) + 1) + 1) |^ n) mod (2 |^ (2 |-count n)) by s, dk
.= ((2 * (k + 1)) |^ n) mod (2 |^ (2 |-count n))
.= ((2 |^ n) * ((k + 1) |^ n)) mod (2 |^ (2 |-count n)) by NEWTON:7 ;
2 |^ (2 |-count n) divides (2 |^ n) * ((k + 1) |^ n) by hn2, INT_2:2;
hence (SubXFinS (sm,OddNAT)) . o = 0 by sf, PEPIN:6; :: thesis:

end;

suppose not (2 * k) + 1 in dom s ; :: thesis:

then not (2 * k) + 1 in dom sm by sm;
hence (SubXFinS (sm,OddNAT)) . o = 0 by SX, FUNCT_1:def 2; :: thesis:

end;

then SubXFinS (sm,OddNAT) = (dom (SubXFinS (sm,OddNAT))) --> 0 by FUNCOP_1:11;
then sz: Sum (SubXFinS (sm,OddNAT)) = (len (SubXFinS (sm,OddNAT))) * 0 by AFINSQ_2:58;
ll: len sm = ne - 1 by n, sm;
then reconsider Slm = Segm (len sm) as odd Nat ;
card (Slm /\ EvenNAT) = (Slm div 2) + 1 by lemmacardeven
.= ((Slm - 1) / 2) + 1 by NAT_6:5
.= n2 by n2, ll ;
then dn2: len (SubXFinS (sm,EvenNAT)) = n2 by AFINSQ_2:36;

now :: thesis:

let o be object ; :: thesis:
assume o: o in dom (SubXFinS (sm,EvenNAT)) ; :: thesis:
then reconsider k = o as Nat ;
reconsider ds = dom sm as finite natural-membered set ;
reconsider BB = EvenNAT /\ ds as finite natural-membered set ;
kid: k in dom (Sgm0 BB) by o, NUMERAL2:6;
reconsider dk = 2 * k as even Nat ;
reconsider dkj = dk + 1 as odd Nat ;
k < len (SubXFinS (sm,EvenNAT)) by o, AFINSQ_1:86;
then k < n2 by dn2;
then 2 * k < 2 * n2 by XREAL_1:68;
then dk < (len s) + 1 by n, n2;
then dk <= len s by NAT_1:13;
then ( dk < len s or dk = ne - 1 ) by n, XXREAL_0:1;
then dks: dk in dom s by AFINSQ_1:86;
SX: (SubXFinS (sm,EvenNAT)) . o = sm . ((Sgm0 BB) . k) by o, FUNCT_1:12
.= sm . (2 * k) by kid, NUMERAL2:12
.= (s . dk) mod (2 |^ (2 |-count n)) by sm, dks
.= (dkj |^ n) mod (2 |^ (2 |-count n)) by s, dks ;
reconsider d = 2 as Prime by INT_2:28;
hen1: 2 |-count n >= 1 by hen, NAT_1:14;
then eu: Euler (2 |^ (2 |-count n)) = (d |^ (2 |-count n)) - (d |^ ((2 |-count n) -' 1)) by INT_8:8
.= (d |^ (hj + 1)) - (d |^ hj) by XREAL_1:233, hen1
.= ((d |^ hj) * d) - (d |^ hj) by NEWTON:6
.= d |^ hj ;
2 |^ (2 |-count n) >= 1 + 1 by hen1, PREPOWER:12;
then ddh: 2 |^ (2 |-count n) > 1 by NAT_1:13;
hj <= (2 |-count n) - 0 by XREAL_1:10;
then 2 |^ hj divides 2 |^ (2 |-count n) by PEPIN:31;
then 2 |^ hj divides n by dwah, INT_2:9;
then consider a being Nat such that
a: n = (2 |^ hj) * a by NAT_D:def 3;
dkj,2 |^ 1 are_coprime by NAT_5:3;
then dkj,2 are_coprime by NEWTON:5;
then dkj,2 |^ (2 |-count n) are_coprime by EULER_2:17;
then (dkj |^ (Euler (2 |^ (2 |-count n)))) mod (2 |^ (2 |-count n)) = 1 by ddh, EULER_2:18;
then (dkj |^ (d |^ hj)) mod (2 |^ (2 |-count n)) = 1 by eu;
then ((dkj |^ (d |^ hj)) |^ a) mod (2 |^ (2 |-count n)) = 1 by ddh, PEPIN:35;
then (dkj |^ ((d |^ hj) * a)) mod (2 |^ (2 |-count n)) = 1 by NEWTON:9;
hence (SubXFinS (sm,EvenNAT)) . o = 1 by SX, a; :: thesis:

end;

then SubXFinS (sm,EvenNAT) = (dom (SubXFinS (sm,EvenNAT))) --> 1 by FUNCOP_1:11;
then sn: Sum (SubXFinS (sm,EvenNAT)) = n2 * 1 by dn2, AFINSQ_2:58;
OddNAT misses EvenNAT by NUMERAL2:7;
then Sum (SubXFinS (sm,(OddNAT \/ EvenNAT))) = 0 + (Sum (SubXFinS (sm,EvenNAT))) by NUMERAL2:10, sz;
then Sum sm = Sum (SubXFinS (sm,EvenNAT)) by NUMERAL2:8, NUMERAL2:11;
then (Sum s) mod (2 |^ (2 |-count n)) = n2 mod (2 |^ (2 |-count n)) by sn, ss;
then fs: n2, Sum s are_congruent_mod 2 |^ (2 |-count n) by NAT_D:64;
2 |^ (2 |-count n) divides n by n, NAT_3:def 7;
then 2 |^ (2 |-count n) divides (Sum s) - 0 by INT_2:9, nd;
then Sum s, 0 are_congruent_mod 2 |^ (2 |-count n) by INT_1:def 4;
then n2, 0 are_congruent_mod 2 |^ (2 |-count n) by fs, INT_1:15;
then 2 |^ (2 |-count n) divides n2 - 0 by INT_1:def 4;
then 2 * (2 |^ (2 |-count n)) divides n by INT_6:8, n2;
then 2 |^ ((2 |-count n) + 1) divides n by NEWTON:6;
hence contradiction by n, NAT_3:def 7; :: thesis:

end;