let x, a be Real; :: thesis: for n being Element of NAT st a > 0 & n is even & n >= 1 & x |^ n = a & not x = n -root a holds
x = - (n -root a)
let n be Element of NAT ; :: thesis: ( a > 0 & n is even & n >= 1 & x |^ n = a & not x = n -root a implies x = - (n -root a) )
assume that
A1: a > 0 and
A2: n is even and
A3: n >= 1 ; :: thesis: ( not x |^ n = a or x = n -root a or x = - (n -root a) )
assume A4: x |^ n = a ; :: thesis: ( x = n -root a or x = - (n -root a) )
then A5: x <> 0 by A1, A3, NEWTON:11;

now :: thesis: ( ( x > 0 & ( x = n -root a or x = - (n -root a) ) ) or ( x < 0 & ( x = n -root a or x = - (n -root a) ) ) )

per cases ( x > 0 or x < 0 ) by A5;

case x > 0 ; :: thesis: ( x = n -root a or x = - (n -root a) )

hence ( x = n -root a or x = - (n -root a) ) by A4, A3, POWER:4; :: thesis: verum

end;

case x < 0 ; :: thesis: ( x = n -root a or x = - (n -root a) )

then A6: - x > 0 by XREAL_1:58;
n -root a = n -root ((- x) |^ n) by A2, A4, POWER:1;
then (- 1) * (n -root a) = (- 1) * (- x) by A3, A6, POWER:4;
hence ( x = n -root a or x = - (n -root a) ) ; :: thesis: verum

end;

end;

end;

hence ( x = n -root a or x = - (n -root a) ) ; :: thesis: verum