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 )

( 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 ) )
;

end;

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;p divides i * j by A1;

hence ( p divides i or p divides j ) by NEWTON:80; :: thesis: verum

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;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

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;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