let x, a, b, c be Real; :: thesis: for n being Element of NAT st a <> 0 & n is odd & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) holds
x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))
let n be Element of NAT ; :: thesis: ( a <> 0 & n is odd & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) implies x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) )
assume that
A1: a <> 0 and
A2: n is odd and
A3: ( delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 ) ; :: thesis: ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) )
( x |^ n = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x |^ n = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by A1, A3, POLYEQ_1:5;
hence ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) ) by A2, POWER:4; :: thesis: verum