let a be Nat; :: thesis: for n being prime Nat holds n * a divides ((a + 1) |^ n) - ((a |^ n) + 1)
let n be prime Nat; :: thesis: n * a divides ((a + 1) |^ n) - ((a |^ n) + 1)
L1: ( a > 0 implies (n * a) * 1 divides ((a + 1) |^ n) - ((a |^ n) + (1 |^ n)) ) by Th55;
( a = 0 implies n * a divides ((a + 1) |^ n) - ((a |^ n) + 1) ) ;
hence n * a divides ((a + 1) |^ n) - ((a |^ n) + 1) by L1; :: thesis: verum