let a, b, c, x be real number ; :: thesis: ( a <> 0 & delta a,b,c >= 0 & Polynom a,b,c,0 ,x = 0 & not x = 0 & not x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) implies x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) )
assume A1: ( a <> 0 & delta a,b,c >= 0 ) ; :: thesis: ( not Polynom a,b,c,0 ,x = 0 or x = 0 or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) )
assume A2: Polynom a,b,c,0 ,x = 0 ; :: thesis: ( x = 0 or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) )
x |^ 3 = x |^ (2 + 1) ;
then x |^ 3 = (x |^ (1 + 1)) * x by NEWTON:11;
then A3: x |^ 3 = ((x |^ 1) * x) * x by NEWTON:11;
x |^ 1 = x to_power 1 by POWER:46;
then x |^ 3 = (x ^2 ) * x by A3, POWER:30;
then (((a * (x ^2 )) + (b * x)) + c) * x = 0 by A2;
then ( x = 0 or Polynom a,b,c,x = 0 ) by XCMPLX_1:6;
hence ( x = 0 or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) ) by A1, Th5; :: thesis: verum