let a, c, e, x be real number ; :: thesis: ( a <> 0 & e <> 0 & (c ^2 ) - ((4 * a) * e) > 0 & Polynom a,0 ,c,0 ,e,x = 0 implies ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) ) )
assume that
A1: a <> 0 and
A2: e <> 0 and
A3: (c ^2 ) - ((4 * a) * e) > 0 ; :: thesis: ( not Polynom a,0 ,c,0 ,e,x = 0 or ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) ) )
set y = x ^2 ;
assume A4: Polynom a,0 ,c,0 ,e,x = 0 ; :: thesis: ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) )

A5: now

assume x = 0 ; :: thesis: contradiction
then ((a * 0 ) + (0 * (0 |^ 3))) + e = 0 by A4, NEWTON:16;
hence contradiction by A2; :: thesis: verum

end;

per cases ( x > 0 or x < 0 ) by A5, XXREAL_0:1;

suppose A6: x > 0 ; :: thesis: ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) )

x |^ 4 = x to_power (2 + 2) by POWER:46
.= (x to_power 2) * (x to_power 2) by A6, POWER:32
.= (x ^2 ) * (x to_power 2) by POWER:53
.= (x ^2 ) * (x ^2 ) by POWER:53 ;
then ((a * ((x ^2 ) ^2 )) + (c * (x ^2 ))) + e = 0 by A4;
then A7: Polynom a,c,e,(x ^2 ) = 0 by POLYEQ_1:def 2;
delta a,c,e >= 0 by A3, QUIN_1:def 1;
then ( x ^2 = ((- c) + (sqrt (delta a,c,e))) / (2 * a) or x ^2 = ((- c) - (sqrt (delta a,c,e))) / (2 * a) ) by A1, A7, POLYEQ_1:5;
then ( abs x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or abs x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) ) by COMPLEX1:158;
hence ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) ) by A6, ABSVALUE:def 1; :: thesis: verum

end;

suppose A8: x < 0 ; :: thesis: ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) )

then A9: 0 < - x by XREAL_1:60;
(- x) |^ 4 = x |^ 4 by Lm1, POWER:1;
then x |^ 4 = (- x) to_power (2 + 2) by POWER:46
.= ((- x) to_power 2) * ((- x) to_power 2) by A9, POWER:32
.= ((- x) ^2 ) * ((- x) to_power 2) by POWER:53
.= (x ^2 ) * (x ^2 ) by POWER:53 ;
then ((a * ((x ^2 ) ^2 )) + (c * (x ^2 ))) + e = 0 by A4;
then A10: Polynom a,c,e,(x ^2 ) = 0 by POLYEQ_1:def 2;
(c ^2 ) - ((4 * a) * e) = delta a,c,e by QUIN_1:def 1;
then ( x ^2 = ((- c) + (sqrt (delta a,c,e))) / (2 * a) or x ^2 = ((- c) - (sqrt (delta a,c,e))) / (2 * a) ) by A1, A3, A10, POLYEQ_1:5;
then ( abs x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or abs x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) ) by COMPLEX1:158;
then ( (- 1) * (- x) = (- 1) * (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or (- 1) * (- x) = (- 1) * (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) by A8, ABSVALUE:def 1;
hence ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta a,c,e))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta a,c,e))) / (2 * a))) ) ) by A5; :: thesis: verum

end;

end;