let a, k be Nat; :: thesis: for p being odd Prime st p |^ (k + 1) divides (a |^ (p |^ k)) + 1 holds
p |^ (k + 2) divides (a |^ (p |^ (k + 1))) + 1
let p be odd Prime; :: thesis: ( p |^ (k + 1) divides (a |^ (p |^ k)) + 1 implies p |^ (k + 2) divides (a |^ (p |^ (k + 1))) + 1 )
assume A1: p |^ (k + 1) divides (a |^ (p |^ k)) + 1 ; :: thesis: p |^ (k + 2) divides (a |^ (p |^ (k + 1))) + 1
set b = a |^ (p |^ k);
a |^ (p |^ k), - 1 are_congruent_mod p |^ (k + 1) by A1;
then A2: a |^ (p |^ k), - 1 are_congruent_mod p by Th6;
A3: for L being Nat holds (a |^ (p |^ k)) |^ (2 * L),1 are_congruent_mod p

proof

let L be Nat; :: thesis: (a |^ (p |^ k)) |^ (2 * L),1 are_congruent_mod p
(a |^ (p |^ k)) |^ (2 * L),(- 1) |^ (2 * L) are_congruent_mod p by A2, GR_CY_3:34;
hence (a |^ (p |^ k)) |^ (2 * L),1 are_congruent_mod p ; :: thesis: verum

end;

A4: for L being Nat holds (a |^ (p |^ k)) |^ ((2 * L) + 1), - 1 are_congruent_mod p

proof

let L be Nat; :: thesis: (a |^ (p |^ k)) |^ ((2 * L) + 1), - 1 are_congruent_mod p
(a |^ (p |^ k)) |^ ((2 * L) + 1),(- 1) |^ ((2 * L) + 1) are_congruent_mod p by A2, GR_CY_3:34;
hence (a |^ (p |^ k)) |^ ((2 * L) + 1), - 1 are_congruent_mod p ; :: thesis: verum

end;

p |^ (k + 1) = p * (p |^ k) by NEWTON:6;
then A5: a |^ (p |^ (k + 1)) = (a |^ (p |^ k)) |^ p by NEWTON:9;
reconsider F = OddEvenPowers ((a |^ (p |^ k)),p) as INT -valued FinSequence ;
reconsider M = F mod p as INT -valued FinSequence ;
A6: for x being Nat st 1 <= x & x <= len F holds
M . x = 1

proof

let x be Nat; :: thesis: ( 1 <= x & x <= len F implies M . x = 1 )
assume A7: ( 1 <= x & x <= len F ) ; :: thesis: M . x = 1
x in dom F by A7, FINSEQ_3:25;
then A8: M . x = (F . x) mod p by EULER_2:def 1;
A9: len F = p by Def3;
then reconsider m = p - x as Element of NAT by A7, INT_1:5;
A10: 1 mod p = 1 ;

per cases ( x is odd or x is even ) ;

suppose A11: x is odd ; :: thesis: M . x = 1

then A12: m is even ;
F . x = (a |^ (p |^ k)) |^ m by A7, A9, A11, Def3;
hence M . x = 1 by A3, A8, A10, A12, NAT_D:64; :: thesis: verum

end;

suppose A13: x is even ; :: thesis: M . x = 1

then ex L being Nat st m = (2 * L) + 1 by ABIAN:9;
then A14: (- 1) * ((a |^ (p |^ k)) |^ m),(- 1) * (- 1) are_congruent_mod p by A4, INT_4:11;
F . x = - ((a |^ (p |^ k)) |^ m) by A7, A9, A13, Def3;
hence M . x = 1 by A8, A10, A14, NAT_D:64; :: thesis: verum

end;

end;

end;

set P = p |-> 1;
A15: len F = p by Def3;
dom M = dom F by EULER_2:def 1;
then A16: len M = len F by FINSEQ_3:29;
then A17: dom M = Seg p by A15, FINSEQ_1:def 3;
for k being Nat st k in dom (p |-> 1) holds
M . k = (p |-> 1) . k

proof

let k be Nat; :: thesis: ( k in dom (p |-> 1) implies M . k = (p |-> 1) . k )
assume A18: k in dom (p |-> 1) ; :: thesis: M . k = (p |-> 1) . k
( 1 <= k & k <= p ) by A15, A16, A17, A18, FINSEQ_3:25;
hence M . k = 1 by A6, A15
.= (p |-> 1) . k by A18, FINSEQ_2:57 ;
:: thesis: verum

end;

then M = p |-> 1 by A17, FINSEQ_1:13;
then Sum M = p * 1 by RVSUM_1:80;
then A19: Sum M, 0 are_congruent_mod p ;
A20: ex z being Nat st p = (2 * z) + 1 by ABIAN:9;
Sum F, Sum M are_congruent_mod p by Th10;
then Sum F, 0 are_congruent_mod p by A19, INT_1:15;
then A21: p * (p |^ (k + 1)) divides ((a |^ (p |^ k)) + 1) * (Sum F) by A1, NEWTON02:2;
p |^ ((k + 1) + 1) = p * (p |^ (k + 1)) by NEWTON:6;
hence p |^ (k + 2) divides (a |^ (p |^ (k + 1))) + 1 by A5, A20, A21, Th21; :: thesis: verum