let a, b, c, x be Real; ( 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:6;
then A2:
x |^ 3 = ((x |^ 1) * x) * x
by NEWTON:6;
A3:
x |^ 3 = (x ^2) * x
by A2;
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