let a, x, p, y, q be Real; for n being Element of NAT st a * (x |^ n) = p & x * y = q & not n is even & p * a <> 0 holds
( x = n -root (p / a) & y = q * (n -root (a / p)) )
let n be Element of NAT ; ( a * (x |^ n) = p & x * y = q & not n is even & 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:
not n is even
and
A4:
p * a <> 0
; ( x = n -root (p / a) & y = q * (n -root (a / p)) )
consider m being Element of 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:90;
then
x = n -root (p / a)
by A3, POWER:5;
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:12;
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:88;
then A8:
y * (n -root (p / p)) = q * (n -root (a / p))
by XCMPLX_0:def 9;
2 * m >= 0
by NAT_1:2;
then A9:
(2 * m) + 1 >= 0 + 1
by XREAL_1:9;
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:7;
hence
( x = n -root (p / a) & y = q * (n -root (a / p)) )
by A3, A7, POWER:5; verum