let x, y, a, p, q be Real; for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is even & n >= 1 & p / a > 0 & a <> 0 & not ( x = n -root (p / a) & y = q * (n -root (a / p)) ) 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 & n is even & n >= 1 & p / a > 0 & a <> 0 & not ( x = n -root (p / a) & y = q * (n -root (a / p)) ) 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 even & n >= 1 )
and
A4:
p / a > 0
and
A5:
a <> 0
; ( ( x = n -root (p / a) & y = q * (n -root (a / p)) ) or ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) )
A6:
x |^ n = p / a
by A1, A5, XCMPLX_1:89;
(p / a) " > 0
by A4;
then
1 / (p / a) > 0
by XCMPLX_1:215;
then A7:
(1 * a) / p > 0
by XCMPLX_1:77;
A8:
p <> 0
by A4;