let x, y, a, p, q be Real; :: thesis: for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is odd & p * a <> 0 holds
( x = n -root (p / a) & y = q * (n -root (a / p)) )
let n be Element of NAT ; :: thesis: ( a * (x |^ n) = p & x * y = q & n is odd & p * a <> 0 implies ( x = n -root (p / a) & y = q * (n -root (a / p)) ) )
assume that
A1: a * (x |^ n) = p and
A2: x * y = q and
A3: n is odd and
A4: p * a <> 0 ; :: thesis: ( x = n -root (p / a) & y = q * (n -root (a / p)) )
consider m being Nat such that
A5: n = (2 * m) + 1 by A3, ABIAN:9;
A6: a <> 0 by A4;
then A7: x |^ n = p / a by A1, XCMPLX_1:89;
then x = n -root (p / a) by A3, POWER:4;
then y * ((n -root (p / a)) * (n -root (a / p))) = q * (n -root (a / p)) by A2;
then y * (n -root ((p / a) * (a / p))) = q * (n -root (a / p)) by A3, POWER:11;
then y * (n -root ((p / a) * (a * (p ")))) = q * (n -root (a / p)) by XCMPLX_0:def 9;
then y * (n -root (((p / a) * a) * (p "))) = q * (n -root (a / p)) ;
then y * (n -root (p * (p "))) = q * (n -root (a / p)) by A6, XCMPLX_1:87;
then A8: y * (n -root (p / p)) = q * (n -root (a / p)) by XCMPLX_0:def 9;
A9: (2 * m) + 1 >= 0 + 1 by XREAL_1:7;
p <> 0 by A4;
then y * (n -root 1) = q * (n -root (a / p)) by A8, XCMPLX_1:60;
then y * 1 = q * (n -root (a / p)) by A5, A9, POWER:6;
hence ( x = n -root (p / a) & y = q * (n -root (a / p)) ) by A3, A7, POWER:4; :: thesis: verum