let x, a, b, c be Real; for n being Element of NAT st a <> 0 & b / a < 0 & c / a > 0 & n is even & n >= 1 & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) & not x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) & 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 ; ( a <> 0 & b / a < 0 & c / a > 0 & n is even & n >= 1 & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) & not x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) & 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:
( b / a < 0 & c / a > 0 & n is even & n >= 1 )
and
A3:
delta (a,b,c) >= 0
and
A4:
Polynom (a,b,c,(x |^ n)) = 0
; ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) )
now ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) )per cases
( x |^ n = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x |^ n = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
by A1, A3, A4, POLYEQ_1:5;
suppose
x |^ n = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a)
;
( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) )then
(
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, A3, Th1, Th4;
hence
(
x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or
x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or
x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or
x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) )
;
verum end; suppose
x |^ n = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)
;
( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) )then
(
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, A3, Th1, Th4;
hence
(
x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or
x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or
x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or
x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) )
;
verum end; end; end;
hence
( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) )
; verum