let a, x, p, y, q be Real; :: thesis: for n being Element of NAT st a * (x |^ n) = p & x * y = q & ex m being Element of NAT st
( n = 2 * m & m >= 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 ; :: thesis: ( a * (x |^ n) = p & x * y = q & ex m being Element of NAT st
( n = 2 * m & m >= 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 A1:
( a * (x |^ n) = p & x * y = q & ex m being Element of NAT st
( n = 2 * m & m >= 1 ) & p / a > 0 & a <> 0 )
; :: thesis: ( ( x = n -root (p / a) & y = q * (n -root (a / p)) ) or ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) )
then consider m being Element of NAT such that
A2:
( n = 2 * m & m >= 1 )
;
A3:
n >= 1
by A2, XREAL_1:163;
A4:
p <> 0
by A1;
(p / a) " > 0
by A1, XREAL_1:124;
then
1 / (p / a) > 0
by XCMPLX_1:217;
then A5:
(1 * a) / p > 0
by XCMPLX_1:78;
A6:
x |^ n = p / a
by A1, XCMPLX_1:90;