let a, b, c, x be real number ; ( 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 )
; ( 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) )
x |^ 3 = x |^ (2 + 1)
;
then
x |^ 3 = (x |^ (1 + 1)) * x
by NEWTON:11;
then A2:
x |^ 3 = ((x |^ 1) * x) * x
by NEWTON:11;
x |^ 1 = x to_power 1
by POWER:46;
then A3:
x |^ 3 = (x ^2 ) * x
by A2, POWER:30;
assume
Polynom a,b,c,0 ,x = 0
; ( x = 0 or x = ((- b) + (sqrt (delta a,b,c))) / (2 * a) or x = ((- b) - (sqrt (delta a,b,c))) / (2 * a) )
then
(((a * (x ^2 )) + (b * x)) + c) * x = 0
by A3;
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; verum