let a, c, e, x be Real; :: 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 :: thesis: not x = 0
assume x = 0 ; :: thesis: contradiction
then ((a * 0) + (0 * (0 |^ 3))) + e = 0 by A4, NEWTON:11;
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:41
.= (x to_power 2) * (x to_power 2) by A6, POWER:27
.= (x ^2) * (x to_power 2) by POWER:46
.= (x ^2) * (x ^2) by POWER:46 ;
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 ( |.x.| = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or |.x.| = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) ) by COMPLEX1:72;
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:58;
(- x) |^ 4 = x |^ 4 by Lm1, POWER:1;
then x |^ 4 = (- x) to_power (2 + 2) by POWER:41
.= ((- x) to_power 2) * ((- x) to_power 2) by A9, POWER:27
.= ((- x) ^2) * ((- x) to_power 2) by POWER:46
.= (x ^2) * (x ^2) by POWER:46 ;
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 ( |.x.| = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or |.x.| = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) ) by COMPLEX1:72;
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;