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

now :: thesis: ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) )

per cases ( x |^ n = 0 or x |^ n = - (b / a) ) by A1, A4, Th5;

suppose x |^ n = 0 ; :: thesis: ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) )

hence ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) ) by PREPOWER:5; :: thesis: verum

end;

suppose x |^ n = - (b / a) ; :: thesis: ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) )

hence ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) ) by A3, A5, Th4; :: thesis: verum

end;

end;

end;

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