let a, n be Nat; :: thesis: for p being prime Nat st p divides a holds

p divides a |^ (n + 1)

let p be prime Nat; :: thesis: ( p divides a implies p divides a |^ (n + 1) )

assume p divides a ; :: thesis: p divides a |^ (n + 1)

then p divides a * (a |^ n) by INT_2:2;

hence p divides a |^ (n + 1) by NEWTON:6; :: thesis: verum

p divides a |^ (n + 1)

let p be prime Nat; :: thesis: ( p divides a implies p divides a |^ (n + 1) )

assume p divides a ; :: thesis: p divides a |^ (n + 1)

then p divides a * (a |^ n) by INT_2:2;

hence p divides a |^ (n + 1) by NEWTON:6; :: thesis: verum