let a be Nat; :: thesis: for n being prime Nat holds
( n divides (a |^ n) + 1 iff n divides a + 1 )
let n be prime Nat; :: thesis: ( n divides (a |^ n) + 1 iff n divides a + 1 )
( n divides (a |^ n) + (1 |^ n) iff n divides a + 1 ) by Th60;
hence ( n divides (a |^ n) + 1 iff n divides a + 1 ) ; :: thesis: verum