let a, b, x be Real; ( a <> 0 & ((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 )) >= 0 & Polynom a,b,b,a,x = 0 & not x = - 1 & not x = ((a - b) + (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) implies x = ((a - b) - (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) )
assume that
A1:
( a <> 0 & ((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 )) >= 0 )
and
A2:
Polynom a,b,b,a,x = 0
; ( x = - 1 or x = ((a - b) + (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) )
(((a * (x |^ 3)) + (b * (x ^2 ))) + (b * x)) + a = 0
by A2, POLYEQ_1:def 4;
then
(((x |^ 3) + 1) * a) + ((((x ^2 ) + x) + 0 ) * b) = 0
;
then
(((x |^ 3) + (1 to_power 3)) * a) + (((x + 1) * x) * b) = 0
by POWER:31;
then
(((x + 1) * (((x ^2 ) - (x * 1)) + (1 ^2 ))) * a) + (((x + 1) * x) * b) = 0
by Th11;
then A3:
(((((x ^2 ) * a) - (x * a)) + (x * b)) + a) * (x + 1) = 0
;
now per cases
( x + 1 = 0 or ((a * (x ^2 )) - ((a - b) * x)) + a = 0 )
by A3, XCMPLX_1:6;
case A4:
((a * (x ^2 )) - ((a - b) * x)) + a = 0
;
( x = - 1 or x = ((a - b) + (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) )A5:
delta a,
((- a) + b),
a =
(((- a) + b) ^2 ) - ((4 * a) * a)
by QUIN_1:def 1
.=
((b ^2 ) - ((2 * a) * b)) + ((- (4 - 1)) * (a ^2 ))
;
((a * (x ^2 )) + (((- a) + b) * x)) + a = 0
by A4;
then
Polynom a,
((- a) + b),
a,
x = 0
by POLYEQ_1:def 2;
then
(
x = ((- ((- a) + b)) + (sqrt (delta a,((- a) + b),a))) / (2 * a) or
x = ((- ((- a) + b)) - (sqrt (delta a,((- a) + b),a))) / (2 * a) )
by A1, A5, POLYEQ_1:5;
hence
(
x = - 1 or
x = ((a - b) + (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) or
x = ((a - b) - (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) )
by A5;
verum end;
hence
( x = - 1 or x = ((a - b) + (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 ))))) / (2 * a) )
; verum