let a be non zero square Nat; :: thesis: for p being prime Nat st p divides a holds
not a + p is square
let p be prime Nat; :: thesis: ( p divides a implies not a + p is square )
assume B0: p divides a ; :: thesis: not a + p is square
then consider k being Nat such that
B1: a = p * k by NAT_D:def 3;
B3: not p is trivial ;
p ^2 divides a by B0, LmSQ;
then p * p divides p * k by B1, SQUARE_1:def 1;
then p divides k by INT_4:7;
then consider n being Nat such that
B4: k = p * n by NAT_D:def 3;
not p divides 1 * (k + 1) by B3, INT_2:13, B4, NEWTON02:77;
then not p * p divides p * (k + 1) by INT_4:7;
then not p ^2 divides p * (k + 1) by SQUARE_1:def 1;
hence not a + p is square by B1, LmSQ, INT_1:def 3; :: thesis: verum