let n be Nat; :: thesis: for i, j, z being Integer st n is odd & i,j are_coprime & i * j = z |^ n holds
ex k being Integer st i = k |^ n
let i, j, z be Integer; :: thesis: ( n is odd & i,j are_coprime & i * j = z |^ n implies ex k being Integer st i = k |^ n )
assume A1: n is odd ; :: thesis: ( not i,j are_coprime or not i * j = z |^ n or ex k being Integer st i = k |^ n )
assume i,j are_coprime ; :: thesis: ( not i * j = z |^ n or ex k being Integer st i = k |^ n )
then A2: |.i.|,|.j.| are_coprime by INT_2:34;
assume A3: i * j = z |^ n ; :: thesis: ex k being Integer st i = k |^ n
A4: |.i.| * |.j.| = |.(i * j).| by COMPLEX1:65;
|.(z |^ n).| = |.z.| |^ n by TAYLOR_2:1;
then consider k being Nat such that
A5: k |^ n = |.i.| by A2, A3, A4, NEWTON02:30;

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

suppose A6: i >= 0 ; :: thesis: ex k being Integer st i = k |^ n

take k ; :: thesis: i = k |^ n
thus k |^ n = i by A5, A6, ABSVALUE:def 1; :: thesis: verum

end;

suppose i <= 0 ; :: thesis: ex k being Integer st i = k |^ n

then A7: |.i.| = - i by ABSVALUE:30;
take - k ; :: thesis: i = (- k) |^ n
thus (- k) |^ n = - (k |^ n) by A1, POWER:2
.= i by A5, A7 ; :: thesis: verum

end;

end;