let a, k be Nat; :: thesis: for n being prime Nat holds n divides (a |^ (n + k)) - (a |^ (k + 1))
let n be prime Nat; :: thesis: n divides (a |^ (n + k)) - (a |^ (k + 1))
(a |^ (n + k)) - (a |^ (k + 1)) = ((a |^ n) * (a |^ k)) - (a |^ (k + 1)) by NEWTON:8
.= ((a |^ n) * (a |^ k)) - ((a |^ k) * a) by NEWTON:6
.= (a |^ k) * ((a |^ n) - a) ;
hence n divides (a |^ (n + k)) - (a |^ (k + 1)) by Th58, INT_2:2; :: thesis: verum