let i, j be Integer; :: thesis: for p being Prime holds
( not p divides i * j or p divides i or p divides j )
let p be Prime; :: thesis: ( not p divides i * j or p divides i or p divides j )
assume A1: p divides i * j ; :: thesis: ( p divides i or p divides j )

per cases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( i < 0 & j < 0 ) ) ;

suppose ( i >= 0 & j >= 0 ) ; :: thesis: ( p divides i or p divides j )

then reconsider i = i, j = j as Element of NAT by INT_1:3;
p divides i * j by A1;
hence ( p divides i or p divides j ) by NEWTON:80; :: thesis: verum

end;

suppose ( i >= 0 & j < 0 ) ; :: thesis: ( p divides i or p divides j )

then reconsider i = i, j9 = - j as Element of NAT by INT_1:3;
p divides - (i * j) by A1, INT_2:10;
then p divides i * j9 ;
then ( p divides i or p divides j9 ) by NEWTON:80;
hence ( p divides i or p divides j ) by INT_2:10; :: thesis: verum

end;

suppose ( i < 0 & j >= 0 ) ; :: thesis: ( p divides i or p divides j )

then reconsider i9 = - i, j = j as Element of NAT by INT_1:3;
p divides - (i * j) by A1, INT_2:10;
then p divides i9 * j ;
then ( p divides i9 or p divides j ) by NEWTON:80;
hence ( p divides i or p divides j ) by INT_2:10; :: thesis: verum

end;

suppose ( i < 0 & j < 0 ) ; :: thesis: ( p divides i or p divides j )

then reconsider i9 = - i, j9 = - j as Element of NAT by INT_1:3;
p divides i9 * j9 by A1;
then ( p divides i9 or p divides j9 ) by NEWTON:80;
hence ( p divides i or p divides j ) by INT_2:10; :: thesis: verum

end;

end;