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:16;
p divides i * j by A1;
hence ( p divides i or p divides j ) by NEWTON:98; :: thesis: verum

end;

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

then ( i >= 0 & - j > 0 ) by XREAL_1:60;
then reconsider i = i, j' = - j as Element of NAT by INT_1:16;
p divides - (i * j) by A1, INT_2:14;
then p divides i * j' ;
then ( p divides i or p divides j' ) by NEWTON:98;
hence ( p divides i or p divides j ) by INT_2:14; :: thesis: verum

end;

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

then ( - i > 0 & j >= 0 ) by XREAL_1:60;
then reconsider i' = - i, j = j as Element of NAT by INT_1:16;
p divides - (i * j) by A1, INT_2:14;
then p divides i' * j ;
then ( p divides i' or p divides j ) by NEWTON:98;
hence ( p divides i or p divides j ) by INT_2:14; :: thesis: verum

end;

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

then ( - i > 0 & - j > 0 ) by XREAL_1:60;
then reconsider i' = - i, j' = - j as Element of NAT by INT_1:16;
p divides i' * j' by A1;
then ( p divides i' or p divides j' ) by NEWTON:98;
hence ( p divides i or p divides j ) by INT_2:14; :: thesis: verum

end;

end;