let k be Nat; :: thesis: for p being prime Nat st p divides (p + (k + 1)) * (p - (k + 1)) holds
k + 1 >= p
let p be prime Nat; :: thesis: ( p divides (p + (k + 1)) * (p - (k + 1)) implies k + 1 >= p )
p divides p * p ;
then A1: p divides p |^ 2 by NEWTON:81;
A2: p |^ 2 = ((p |^ 2) - ((k + 1) |^ 2)) + ((k + 1) |^ 2) ;
assume p divides (p + (k + 1)) * (p - (k + 1)) ; :: thesis: k + 1 >= p
then p divides (p |^ 2) - ((k + 1) |^ 2) by NEWTON01:1;
then p divides (k + 1) |^ 2 by A1, A2, INT_2:1;
hence k + 1 >= p by NAT_D:7, NAT_3:5; :: thesis: verum