let n be Nat; :: thesis: for i, j being Integer
for p being Prime st i,j are_coprime & p |^ n divides i * j & not p |^ n divides i holds
p |^ n divides j
let i, j be Integer; :: thesis: for p being Prime st i,j are_coprime & p |^ n divides i * j & not p |^ n divides i holds
p |^ n divides j
let p be Prime; :: thesis: ( i,j are_coprime & p |^ n divides i * j & not p |^ n divides i implies p |^ n divides j )
assume i,j are_coprime ; :: thesis: ( not p |^ n divides i * j or p |^ n divides i or p |^ n divides j )
then A1: |.i.|,|.j.| are_coprime by INT_2:34;
assume p |^ n divides i * j ; :: thesis: ( p |^ n divides i or p |^ n divides j )
then p |^ n divides |.(i * j).| by Th4;
then p |^ n divides |.i.| * |.j.| by COMPLEX1:65;
then ( p |^ n divides |.i.| or p |^ n divides |.j.| ) by A1, NUMBER08:107;
hence ( p |^ n divides i or p |^ n divides j ) by Th4; :: thesis: verum