:: POLYEQ_1 semantic presentation

begin


definition
let a, b, x be complex number ;
func Polynom (a,b,x) ->  set  equals :: POLYEQ_1:def 1
(a * x) + b;
coherence
 (a * x) + b is set ;
end;

:: deftheorem  defines Polynom POLYEQ_1:def_1_:_
 for a, b, x being complex number holds Polynom (a,b,x) = (a * x) + b;

registration
let a, b, x be complex number ;
cluster Polynom (a,b,x) ->  complex ;
coherence
 Polynom (a,b,x) is complex ;
end;

registration
let a, b, x be real number ;
cluster Polynom (a,b,x) ->  real ;
coherence
 Polynom (a,b,x) is real ;
end;

definition
let a, b, x be Real;
:: original: Polynom
redefine func Polynom (a,b,x) ->  Real;
coherence
 Polynom (a,b,x) is Real by XREAL_0:def_1;
end;

theorem :: POLYEQ_1:1
for a, b, x being complex number st a <> 0 & Polynom (a,b,x) = 0 holds
x = - (b / a)
proof
let a, b, x be complex number ; ::_thesis: ( a <> 0 & Polynom (a,b,x) = 0 implies x = - (b / a) )
assume that
A1: a <> 0 and
A2: Polynom (a,b,x) = 0 ; ::_thesis: x = - (b / a)
(a ") * (- b) = (a ") * (a * x) by A2
.= ((a ") * a) * x ;
then  1 * x = (a ") * (- b) by A1, XCMPLX_0:def_7;
then  x = - ((a ") * b) ;
hence  x = - (b / a) by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: POLYEQ_1:2
for x being complex number holds Polynom (0,0,x) = 0 ;

theorem :: POLYEQ_1:3
for b being complex number st b <> 0 holds
for x being complex number holds not Polynom (0,b,x) = 0 ;

definition
let a, b, c, x be complex number ;
func Polynom (a,b,c,x) ->  set  equals :: POLYEQ_1:def 2
((a * (x ^2)) + (b * x)) + c;
coherence
 ((a * (x ^2)) + (b * x)) + c is set ;
end;

:: deftheorem  defines Polynom POLYEQ_1:def_2_:_
 for a, b, c, x being complex number holds Polynom (a,b,c,x) = ((a * (x ^2)) + (b * x)) + c;

registration
let a, b, c, x be real number ;
cluster Polynom (a,b,c,x) ->  real ;
coherence
 Polynom (a,b,c,x) is real ;
end;

registration
let a, b, c, x be complex number ;
cluster Polynom (a,b,c,x) ->  complex ;
coherence
 Polynom (a,b,c,x) is complex ;
end;

definition
let a, b, c, x be Real;
:: original: Polynom
redefine func Polynom (a,b,c,x) ->  Real;
coherence
 Polynom (a,b,c,x) is Real by XREAL_0:def_1;
end;

theorem Th4: :: POLYEQ_1:4
for a, b, c, a9, b9, c9 being complex number st ( for x being real number holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) holds
( a = a9 & b = b9 & c = c9 )
proof
let a, b, c, a9, b9, c9 be complex number ; ::_thesis: ( ( for x being real number holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) implies ( a = a9 & b = b9 & c = c9 ) )
assume A1: for x being real number holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ; ::_thesis: ( a = a9 & b = b9 & c = c9 )
then A2: Polynom (a,b,c,(- 1)) = Polynom (a9,b9,c9,(- 1)) ;
 ( Polynom (a,b,c,0) = Polynom (a9,b9,c9,0) & Polynom (a,b,c,1) = Polynom (a9,b9,c9,1) ) by A1;
hence  ( a = a9 & b = b9 & c = c9 ) by A2; ::_thesis: verum
end;

theorem Th5: :: POLYEQ_1:5
for a, b, c being real number st a <> 0 & delta (a,b,c) >= 0 holds
for x being real number holds
( not Polynom (a,b,c,x) = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
proof
let a, b, c be real number ; ::_thesis: ( a <> 0 & delta (a,b,c) >= 0 implies for x being real number holds
( not Polynom (a,b,c,x) = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) )
assume that
A1: a <> 0 and
A2: delta (a,b,c) >= 0 ; ::_thesis: for x being real number holds
( not Polynom (a,b,c,x) = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
now__::_thesis:_for_y_being_real_number_holds_
(_not_Polynom_(a,b,c,y)_=_0_or_y_=_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_or_y_=_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_)
set e = a * c;
let y be real number ; ::_thesis: ( not Polynom (a,b,c,y) = 0 or y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
set t = ((a ^2) * (y ^2)) + ((a * b) * y);
assume  Polynom (a,b,c,y) = 0 ; ::_thesis: ( y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) )
then  a * (((a * (y ^2)) + (b * y)) + c) = a * 0 ;
then  ((a * (a * (y ^2))) + (a * (b * y))) + (a * c) = 0 ;
then A3: ((((a ^2) * (y ^2)) + ((a * b) * y)) + ((b ^2) / 4)) - ((b ^2) * (4 ")) = - ((4 * (a * c)) * (4 ")) ;
A4: delta (a,b,c) = (b ^2) - ((4 * a) * c) by QUIN_1:def_1;
A5: now__::_thesis:_(_((a_*_y)_+_(b_/_2))_-_(sqrt_(((b_^2)_-_(4_*_(a_*_c)))_/_4))_=_0_implies_y_=_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_)
assume  ((a * y) + (b / 2)) - (sqrt (((b ^2) - (4 * (a * c))) / 4)) = 0 ; ::_thesis: y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a)
then  (a * y) + (b / 2) = (sqrt ((b ^2) - (4 * (a * c)))) / 2 by A2, A4, SQUARE_1:20, SQUARE_1:30;
then a * y = - ((b * (2 ")) - ((sqrt ((b ^2) - (4 * (a * c)))) * (2 ")))
.= ((- b) * (2 ")) + ((sqrt (delta (a,b,c))) * (2 ")) by A4 ;
then y = (((- b) * (2 ")) + ((sqrt (delta (a,b,c))) * (2 "))) / a by A1, XCMPLX_1:89
.= (((- b) * (2 ")) + ((sqrt (delta (a,b,c))) * (2 "))) * (a ") by XCMPLX_0:def_9
.= ((- b) + (sqrt (delta (a,b,c)))) * ((2 ") * (a "))
.= ((- b) + (sqrt (delta (a,b,c)))) * ((2 * a) ") by XCMPLX_1:204 ;
hence  y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) by XCMPLX_0:def_9; ::_thesis: verum
end;
A6: now__::_thesis:_(_((a_*_y)_+_(b_/_2))_+_(sqrt_(((b_^2)_-_(4_*_(a_*_c)))_/_4))_=_0_implies_y_=_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_)
assume  ((a * y) + (b / 2)) + (sqrt (((b ^2) - (4 * (a * c))) / 4)) = 0 ; ::_thesis: y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)
then  (a * y) + (b / 2) = - (sqrt (((b ^2) - (4 * (a * c))) / 4)) ;
then  (a * y) + (b / 2) = - ((sqrt ((b ^2) - (4 * (a * c)))) / 2) by A2, A4, SQUARE_1:20, SQUARE_1:30;
then a * y = - ((b * (2 ")) + ((sqrt ((b ^2) - (4 * (a * c)))) * (2 ")))
.= ((- b) * (2 ")) - ((sqrt (delta (a,b,c))) * (2 ")) by A4 ;
then y = (((- b) * (2 ")) - ((sqrt (delta (a,b,c))) * (2 "))) / a by A1, XCMPLX_1:89
.= (((- b) * (2 ")) - ((sqrt (delta (a,b,c))) * (2 "))) * (a ") by XCMPLX_0:def_9
.= ((- b) - (sqrt (delta (a,b,c)))) * ((2 ") * (a "))
.= ((- b) - (sqrt (delta (a,b,c)))) * ((2 * a) ") by XCMPLX_1:204 ;
hence  y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) by XCMPLX_0:def_9; ::_thesis: verum
end;
 ((b ^2) - (4 * (a * c))) / 4 >= 0 / 4 by A2, A4, XREAL_1:72;
then  ((a * y) + (b / 2)) ^2 = (sqrt (((b ^2) - (4 * (a * c))) / 4)) ^2 by A3, SQUARE_1:def_2;
then  (((a * y) + (b / 2)) - (sqrt (((b ^2) - (4 * (a * c))) / 4))) * (((a * y) + (b / 2)) + (sqrt (((b ^2) - (4 * (a * c))) / 4))) = 0 ;
hence  ( y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by A5, A6, XCMPLX_1:6; ::_thesis: verum
end;
hence  for x being real number holds
( not Polynom (a,b,c,x) = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) ; ::_thesis: verum
end;

theorem :: POLYEQ_1:6
for a, b, c, x being complex number st a <> 0 & delta (a,b,c) = 0 & Polynom (a,b,c,x) = 0 holds
x = - (b / (2 * a))
proof
let a, b, c, x be complex number ; ::_thesis: ( a <> 0 & delta (a,b,c) = 0 & Polynom (a,b,c,x) = 0 implies x = - (b / (2 * a)) )
assume that
A1: a <> 0 and
A2: delta (a,b,c) = 0 ; ::_thesis: ( not Polynom (a,b,c,x) = 0 or x = - (b / (2 * a)) )
set y = x;
set t = ((a ^2) * (x ^2)) + ((a * b) * x);
A3: (b ^2) - ((4 * a) * c) = delta (a,b,c) by QUIN_1:def_1;
assume  Polynom (a,b,c,x) = 0 ; ::_thesis: x = - (b / (2 * a))
then  a * (((a * (x ^2)) + (b * x)) + c) = 0 ;
then  (((a ^2) * (x ^2)) + ((a * b) * x)) + (a * c) = 0 ;
then  (((a * x) ^2) + (2 * (((a * x) * b) * (2 ")))) + ((b / 2) ^2) = 0 by A2, A3;
then  ((a * x) + (b / 2)) ^2 = 0 ;
then  (a * x) + (b / 2) = 0 by XCMPLX_1:6;
then x = (- (b * (2 "))) / a by A1, XCMPLX_1:89
.= ((- 1) * (b * (2 "))) * (a ") by XCMPLX_0:def_9
.= - ((b * ((2 ") * (a "))) * 1)
.= - (b * ((2 * a) ")) by XCMPLX_1:204 ;
hence  x = - (b / (2 * a)) by XCMPLX_0:def_9; ::_thesis: verum
end;

theorem :: POLYEQ_1:7
for a, b, c being real number st delta (a,b,c) < 0 holds
for x being real number holds not Polynom (a,b,c,x) = 0
proof
let a, b, c be real number ; ::_thesis: ( delta (a,b,c) < 0 implies for x being real number holds not Polynom (a,b,c,x) = 0 )
set e = a * c;
assume  delta (a,b,c) < 0 ; ::_thesis: for x being real number holds not Polynom (a,b,c,x) = 0
then  (b ^2) - ((4 * a) * c) < 0 by QUIN_1:def_1;
then A1: ((b ^2) - (4 * (a * c))) * (4 ") < 0 by XREAL_1:132;
given y being real number  such that A2: Polynom (a,b,c,y) = 0 ; ::_thesis: contradiction
set t = ((a ^2) * (y ^2)) + ((a * b) * y);
 a * (((a * (y ^2)) + (b * y)) + c) = a * 0 by A2;
then  ((((a ^2) * (y ^2)) + ((a * b) * y)) + ((b ^2) / 4)) - (((b ^2) * (4 ")) - ((4 * (a * c)) * (4 "))) = 0 ;
then A3: ((a * y) + (b / 2)) ^2 = ((b ^2) - (4 * (a * c))) * (4 ") ;
then  (a * y) + (b / 2) > 0 by A1, XREAL_1:133;
hence  contradiction by A3, A1, XREAL_1:133; ::_thesis: verum
end;

theorem :: POLYEQ_1:8
for x being real number
for b, c being complex number st b <> 0 & ( for x being real number holds Polynom (0,b,c,x) = 0 ) holds
x = - (c / b)
proof
let x be real number ; ::_thesis: for b, c being complex number st b <> 0 & ( for x being real number holds Polynom (0,b,c,x) = 0 ) holds
x = - (c / b)
let b, c be complex number ; ::_thesis: ( b <> 0 & ( for x being real number holds Polynom (0,b,c,x) = 0 ) implies x = - (c / b) )
assume A1: b <> 0 ; ::_thesis: ( ex x being real number st not Polynom (0,b,c,x) = 0 or x = - (c / b) )
set y = x;
assume  for x being real number holds Polynom (0,b,c,x) = 0 ; ::_thesis: x = - (c / b)
then  Polynom (0,b,c,x) = 0 ;
then x = (- c) / b by A1, XCMPLX_1:89
.= ((- 1) * c) * (b ") by XCMPLX_0:def_9
.= (- 1) * (c * (b "))
.= (- 1) * (c / b) by XCMPLX_0:def_9 ;
hence  x = - (c / b) ; ::_thesis: verum
end;

theorem :: POLYEQ_1:9
for x being complex number holds Polynom (0,0,0,x) = 0 ;

theorem :: POLYEQ_1:10
for c being complex number st c <> 0 holds
for x being complex number holds not Polynom (0,0,c,x) = 0 ;

definition
let a, x, x1, x2 be complex number ;
func Quard (a,x1,x2,x) ->  set  equals :: POLYEQ_1:def 3
a * ((x - x1) * (x - x2));
coherence
 a * ((x - x1) * (x - x2)) is set ;
end;

:: deftheorem  defines Quard POLYEQ_1:def_3_:_
 for a, x, x1, x2 being complex number holds Quard (a,x1,x2,x) = a * ((x - x1) * (x - x2));

registration
let a, x, x1, x2 be real number ;
cluster Quard (a,x1,x2,x) ->  real ;
coherence
 Quard (a,x1,x2,x) is real ;
end;

definition
let a, x, x1, x2 be Real;
:: original: Quard
redefine func Quard (a,x1,x2,x) ->  Real;
coherence
 Quard (a,x1,x2,x) is Real by XREAL_0:def_1;
end;

theorem :: POLYEQ_1:11
for x1, x2 being real number
for a, b, c being complex number st a <> 0 & ( for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) holds
( b / a = - (x1 + x2) & c / a = x1 * x2 )
proof
let x1, x2 be real number ; ::_thesis: for a, b, c being complex number st a <> 0 & ( for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) holds
( b / a = - (x1 + x2) & c / a = x1 * x2 )
let a, b, c be complex number ; ::_thesis: ( a <> 0 & ( for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) implies ( b / a = - (x1 + x2) & c / a = x1 * x2 ) )
assume A1: a <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a,b,c,x) = Quard (a,x1,x2,x) or ( b / a = - (x1 + x2) & c / a = x1 * x2 ) )
assume A2: for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ; ::_thesis: ( b / a = - (x1 + x2) & c / a = x1 * x2 )
now__::_thesis:_for_z_being_real_number_holds_Polynom_(1,(-_(x1_+_x2)),(x1_*_x2),z)_=_Polynom_(1,(b_/_a),(c_/_a),z)
let z be real number ; ::_thesis: Polynom (1,(- (x1 + x2)),(x1 * x2),z) = Polynom (1,(b / a),(c / a),z)
set h = z - x1;
set t = z - x2;
set e = ((z - x1) * (z - x2)) - (z ^2);
 Polynom (a,b,c,z) = Quard (a,x1,x2,z) by A2;
then  a * (((z - x1) * (z - x2)) - (z ^2)) = (b * z) + c ;
then ((z - x1) * (z - x2)) - (z ^2) = ((b * z) + c) / a by A1, XCMPLX_1:89
.= (a ") * ((b * z) + c) by XCMPLX_0:def_9
.= ((a ") * (b * z)) + ((a ") * c) ;
then  (((z * z) - (z * x2)) - (x1 * z)) + (x1 * x2) = ((z ^2) + (((a ") * b) * z)) + ((a ") * c) ;
then ((z ^2) - ((x1 + x2) * z)) + (x1 * x2) = ((z ^2) + ((b / a) * z)) + ((a ") * c) by XCMPLX_0:def_9
.= ((z ^2) + ((b / a) * z)) + (c / a) by XCMPLX_0:def_9 ;
hence  Polynom (1,(- (x1 + x2)),(x1 * x2),z) = Polynom (1,(b / a),(c / a),z) ; ::_thesis: verum
end;
hence  ( b / a = - (x1 + x2) & c / a = x1 * x2 ) by Th4; ::_thesis: verum
end;

begin

definition
let a, b, c, d, x be complex number ;
func Polynom (a,b,c,d,x) ->  set  equals :: POLYEQ_1:def 4
(((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d;
coherence
 (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d is set ;
end;

:: deftheorem  defines Polynom POLYEQ_1:def_4_:_
 for a, b, c, d, x being complex number holds Polynom (a,b,c,d,x) = (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d;

registration
let a, b, c, d, x be complex number ;
cluster Polynom (a,b,c,d,x) ->  complex ;
coherence
 Polynom (a,b,c,d,x) is complex ;
end;

registration
let a, b, c, d, x be real number ;
cluster Polynom (a,b,c,d,x) ->  real ;
coherence
 Polynom (a,b,c,d,x) is real ;
end;

definition
let a, b, c, d, x be Real;
:: original: Polynom
redefine func Polynom (a,b,c,d,x) ->  Real;
coherence
 Polynom (a,b,c,d,x) is Real by XREAL_0:def_1;
end;

 3 = (2 * 1) + 1
;

then Lm1:  3 is odd
by ABIAN:1;

theorem Th12: :: POLYEQ_1:12
for a, b, c, d, a9, b9, c9, d9 being real number st ( for x being real number holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ) holds
( a = a9 & b = b9 & c = c9 & d = d9 )
proof
let a, b, c, d, a9, b9, c9, d9 be real number ; ::_thesis: ( ( for x being real number holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ) implies ( a = a9 & b = b9 & c = c9 & d = d9 ) )
(- 1) |^ 3 = - (1 |^ (2 + 1)) by Lm1, POWER:2
.= - ((1 |^ 2) * 1) by NEWTON:6 ;
then A1: ( 0 |^ 3 = 0 & (- 1) |^ 3 = - 1 ) by NEWTON:10, NEWTON:11;
A2: 2 |^ 1 = 2 to_power 1 by POWER:41
.= 2 by POWER:25 ;
A3: 2 |^ 3 = 2 |^ (2 + 1)
.= (2 |^ (1 + 1)) * 2 by NEWTON:6
.= ((2 |^ 1) * 2) * 2 by NEWTON:6
.= (2 |^ 1) * (2 * 2) ;
assume A4: for x being real number holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ; ::_thesis: ( a = a9 & b = b9 & c = c9 & d = d9 )
then A5: Polynom (a,b,c,d,2) = Polynom (a9,b9,c9,d9,2) ;
 Polynom (a,b,c,d,1) = Polynom (a9,b9,c9,d9,1) by A4;
then  (((a * 1) + (b * 1)) + (c * 1)) + d = Polynom (a9,b9,c9,d9,1) by NEWTON:10;
then A6: ((a + b) + c) + d = (((a9 * 1) + (b9 * 1)) + (c9 * 1)) + d9 by NEWTON:10
.= ((a9 + b9) + c9) + d9 ;
 ( Polynom (a,b,c,d,0) = Polynom (a9,b9,c9,d9,0) & Polynom (a,b,c,d,(- 1)) = Polynom (a9,b9,c9,d9,(- 1)) ) by A4;
hence  ( a = a9 & b = b9 & c = c9 & d = d9 ) by A6, A1, A5, A3, A2; ::_thesis: verum
end;

definition
let a, x, x1, x2, x3 be real number ;
func Tri (a,x1,x2,x3,x) ->  set  equals :: POLYEQ_1:def 5
a * (((x - x1) * (x - x2)) * (x - x3));
coherence
 a * (((x - x1) * (x - x2)) * (x - x3)) is set ;
end;

:: deftheorem  defines Tri POLYEQ_1:def_5_:_
 for a, x, x1, x2, x3 being real number holds Tri (a,x1,x2,x3,x) = a * (((x - x1) * (x - x2)) * (x - x3));

registration
let a, x, x1, x2, x3 be real number ;
cluster Tri (a,x1,x2,x3,x) ->  real ;
coherence
 Tri (a,x1,x2,x3,x) is real ;
end;

definition
let a, x, x1, x2, x3 be Real;
:: original: Tri
redefine func Tri (a,x1,x2,x3,x) ->  Real;
coherence
 Tri (a,x1,x2,x3,x) is Real by XREAL_0:def_1;
end;

theorem :: POLYEQ_1:13
for a, b, c, d, x1, x2, x3 being real number st a <> 0 & ( for x being real number holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ) holds
( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) )
proof
let a, b, c, d, x1, x2, x3 be real number ; ::_thesis: ( a <> 0 & ( for x being real number holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ) implies ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) )
assume A1: a <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) or ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) )
set t3 = d / a;
set t2 = c / a;
set t1 = b / a;
set d9 = - ((x1 * x2) * x3);
set c9 = ((x1 * x2) + (x2 * x3)) + (x1 * x3);
set b9 = - ((x1 + x2) + x3);
assume A2: for x being real number holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ; ::_thesis: ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) )
now__::_thesis:_for_x_being_real_number_holds_Polynom_(1,(b_/_a),(c_/_a),(d_/_a),x)_=_Polynom_(1,(-_((x1_+_x2)_+_x3)),(((x1_*_x2)_+_(x2_*_x3))_+_(x1_*_x3)),(-_((x1_*_x2)_*_x3)),x)
let x be real number ; ::_thesis: Polynom (1,(b / a),(c / a),(d / a),x) = Polynom (1,(- ((x1 + x2) + x3)),(((x1 * x2) + (x2 * x3)) + (x1 * x3)),(- ((x1 * x2) * x3)),x)
set t = (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d;
set r8 = ((x - x1) * (x - x2)) * (x - x3);
A3: x |^ 1 = x to_power 1 by POWER:41;
x |^ 3 = x |^ (2 + 1)
.= (x |^ (1 + 1)) * x by NEWTON:6
.= ((x |^ 1) * x) * x by NEWTON:6 ;
then A4: x |^ 3 = (x * x) * x by A3, POWER:25;
 Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) by A2;
then A5: ((((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d) / a = ((x - x1) * (x - x2)) * (x - x3) by A1, XCMPLX_1:89;
(a ") * ((((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d) = ((((a ") * a) * (x |^ 3)) + (((a ") * b) * (x ^2))) + ((a ") * ((c * x) + d))
.= ((1 * (x |^ 3)) + (((a ") * b) * (x ^2))) + ((((a ") * c) * x) + ((a ") * d)) by A1, XCMPLX_0:def_7
.= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + ((((a ") * c) * x) + ((a ") * d)) by XCMPLX_0:def_9
.= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + (((c / a) * x) + ((a ") * d)) by XCMPLX_0:def_9
.= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + (((c / a) * x) + (d / a)) by XCMPLX_0:def_9
.= Polynom (1,(b / a),(c / a),(d / a),x) ;
hence  Polynom (1,(b / a),(c / a),(d / a),x) = Polynom (1,(- ((x1 + x2) + x3)),(((x1 * x2) + (x2 * x3)) + (x1 * x3)),(- ((x1 * x2) * x3)),x) by A5, A4, XCMPLX_0:def_9; ::_thesis: verum
end;
hence  ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) by Th12; ::_thesis: verum
end;

theorem Th14: :: POLYEQ_1:14
for y, h being real number holds (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3)
proof
let y, h be real number ; ::_thesis: (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3)
 (y + h) |^ 3 = (y + h) |^ (2 + 1) ;
then A1: (y + h) |^ 3 = ((y + h) |^ (1 + 1)) * (y + h) by NEWTON:6
.= (((y + h) |^ 1) * (y + h)) * (y + h) by NEWTON:6
.= ((y + h) |^ 1) * ((y + h) ^2)
.= ((y + h) to_power 1) * (((y ^2) + ((2 * y) * h)) + (h ^2)) by POWER:41
.= (y + h) * (((y ^2) + ((2 * y) * h)) + (h ^2)) by POWER:25
.= ((y * (y ^2)) + (((3 * h) * (y ^2)) + (((2 + 1) * (h ^2)) * y))) + (h * (h ^2)) ;
y |^ 3 = y |^ (2 + 1)
.= (y |^ (1 + 1)) * y by NEWTON:6
.= ((y |^ 1) * y) * y by NEWTON:6
.= (y |^ 1) * (y ^2) ;
then A2: y |^ 3 = (y to_power 1) * (y ^2) by POWER:41;
h |^ 3 = h |^ (2 + 1)
.= (h |^ (1 + 1)) * h by NEWTON:6
.= ((h |^ 1) * h) * h by NEWTON:6
.= (h |^ 1) * (h ^2)
.= (h to_power 1) * (h ^2) by POWER:41
.= h * (h ^2) by POWER:25 ;
hence  (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3) by A1, A2, POWER:25; ::_thesis: verum
end;

theorem Th15: :: POLYEQ_1:15
for a, b, c, d, x being real number st a <> 0 & Polynom (a,b,c,d,x) = 0 holds
for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0
proof
let a, b, c, d, x be real number ; ::_thesis: ( a <> 0 & Polynom (a,b,c,d,x) = 0 implies for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 )
assume A1: a <> 0 ; ::_thesis: ( not Polynom (a,b,c,d,x) = 0 or for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 )
assume A2: Polynom (a,b,c,d,x) = 0 ; ::_thesis: for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0
let a1, a2, a3, h, y be real number ; ::_thesis: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a implies ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 )
assume that
A3: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) ) and
A4: ( a1 = b / a & a2 = c / a & a3 = d / a ) ; ::_thesis: ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0
0 = (a ") * (((a * (x |^ 3)) + (b * (x ^2))) + ((c * x) + d)) by A2
.= ((((a ") * a) * (x |^ 3)) + ((a ") * (b * (x ^2)))) + ((a ") * ((c * x) + d))
.= ((1 * (x |^ 3)) + ((a ") * (b * (x ^2)))) + ((a ") * ((c * x) + d)) by A1, XCMPLX_0:def_7
.= (((x |^ 3) + (((a ") * b) * (x ^2))) + (((a ") * c) * x)) + ((a ") * d)
.= (((x |^ 3) + ((b / a) * (x ^2))) + (((a ") * c) * x)) + ((a ") * d) by XCMPLX_0:def_9
.= (((x |^ 3) + ((b / a) * (x ^2))) + ((c / a) * x)) + ((a ") * d) by XCMPLX_0:def_9
.= (((x |^ 3) + (a1 * (x ^2))) + (a2 * x)) + a3 by A4, XCMPLX_0:def_9 ;
then  0 = (((((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3)) + (((a1 * (y ^2)) + ((2 * (a1 * h)) * y)) + (a1 * (h ^2)))) + (a2 * (y + h))) + a3 by A3, Th14
.= (((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (((2 * (a1 * h)) * y) + (a1 * (y ^2)))) + ((a2 * y) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3))) ;
hence  ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 ; ::_thesis: verum
end;

theorem :: POLYEQ_1:16
for a, b, c, d, x being real number st a <> 0 & Polynom (a,b,c,d,x) = 0 holds
for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
(((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0
proof
let a, b, c, d, x be real number ; ::_thesis: ( a <> 0 & Polynom (a,b,c,d,x) = 0 implies for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
(((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 )
assume A1: a <> 0 ; ::_thesis: ( not Polynom (a,b,c,d,x) = 0 or for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
(((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 )
then A2: 3 * a <> 0 ;
assume A3: Polynom (a,b,c,d,x) = 0 ; ::_thesis: for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds
(((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0
let a1, a2, a3, h, y be real number ; ::_thesis: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a implies (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 )
assume that
A4: y = x + (b / (3 * a)) and
A5: h = - (b / (3 * a)) and
A6: a1 = b / a and
A7: a2 = c / a and
A8: a3 = d / a ; ::_thesis: (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0
set p0 = (3 * h) + a1;
A9: (3 * h) + a1 = (- (3 * (b / (3 * a)))) + a1 by A5
.= (- (3 * (((3 * a) ") * b))) + a1 by XCMPLX_0:def_9
.= (- (3 * (((3 ") * (a ")) * b))) + a1 by XCMPLX_1:204
.= (- (((3 * (3 ")) * (a ")) * b)) + a1
.= (- (b / a)) + a1 by XCMPLX_0:def_9 ;
set q2 = ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3);
A10: ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3) = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))
proof
set t = 3 * a;
set a6 = b / (3 * a);
A11: b / a = (3 * b) / (3 * a) by XCMPLX_1:91;
A12: (b / (3 * a)) |^ 3 = (b / (3 * a)) |^ (2 + 1)
.= ((b / (3 * a)) |^ (1 + 1)) * (b / (3 * a)) by NEWTON:6
.= (((b / (3 * a)) |^ 1) * (b / (3 * a))) * (b / (3 * a)) by NEWTON:6
.= ((b / (3 * a)) |^ 1) * ((b / (3 * a)) ^2)
.= ((b / (3 * a)) to_power 1) * ((b / (3 * a)) ^2) by POWER:41 ;
((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3) = (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((c / a) * (b / (3 * a)))) + (d / a)) by A5, A6, A7, A8
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((b * c) / ((3 * a) * a))) + (d / a)) by XCMPLX_1:76
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((b * c) / (3 * (a ^2)))) + (1 * (d / a)))
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((b * c) / (3 * (a ^2)))) + (((3 * a) / (3 * a)) * (d / a))) by A2, XCMPLX_1:60
.= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + (((3 * a) / (3 * a)) * (d / a))) - ((b * c) / (3 * (a ^2)))
.= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + (((3 * a) * d) / ((3 * a) * a))) - ((b * c) / (3 * (a ^2))) by XCMPLX_1:76
.= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + (((3 * a) * d) * ((3 * (a ^2)) "))) - ((b * c) / (3 * (a ^2))) by XCMPLX_0:def_9
.= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + (((3 * a) * d) * ((3 * (a ^2)) "))) - ((b * c) * ((3 * (a ^2)) ")) by XCMPLX_0:def_9
.= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((((3 * a) * d) - (b * c)) * ((3 * (a ^2)) "))
.= (((- (b / (3 * a))) |^ (2 + 1)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_0:def_9
.= ((((- (b / (3 * a))) |^ (1 + 1)) * (- (b / (3 * a)))) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by NEWTON:6
.= (((((- (b / (3 * a))) |^ 1) * (- (b / (3 * a)))) * (- (b / (3 * a)))) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by NEWTON:6
.= ((((- (b / (3 * a))) |^ 1) * ((- (b / (3 * a))) ^2)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))
.= ((((- (b / (3 * a))) to_power 1) * ((- (b / (3 * a))) ^2)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by POWER:41
.= (((- (b / (3 * a))) * ((b / (3 * a)) ^2)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by POWER:25
.= (((- (b / (3 * a))) * ((b ^2) / ((3 * a) ^2))) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_1:76
.= (((- (b / (3 * a))) * ((b ^2) / ((3 * a) ^2))) + ((b / a) * ((b ^2) / ((3 * a) ^2)))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_1:76
.= (((b / a) - (b / (3 * a))) * ((b ^2) / ((3 * a) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))
.= ((((3 * b) * ((3 * a) ")) - ((1 * b) / (3 * a))) * ((b ^2) / ((3 * a) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by A11, XCMPLX_0:def_9
.= ((((3 * b) * ((3 * a) ")) - ((1 * b) * ((3 * a) "))) * ((b ^2) / ((3 * a) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_0:def_9
.= (2 * ((b * ((3 * a) ")) * ((b ^2) / ((3 * a) ^2)))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))
.= (2 * ((b / (3 * a)) * ((b ^2) / ((3 * a) ^2)))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_0:def_9
.= (2 * ((b / (3 * a)) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_1:76 ;
hence  ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3) = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by A12, POWER:25; ::_thesis: verum
end;
set p2 = ((3 * (h ^2)) + (2 * (a1 * h))) + a2;
A13: ((3 * (h ^2)) + (2 * (a1 * h))) + a2 = (((3 * a) * c) - (b ^2)) / (3 * (a ^2))
proof
set t = ((3 * a) ") * b;
A14: (3 * a) / (3 * a) = 1 by A2, XCMPLX_1:60;
((3 * (h ^2)) + (2 * (a1 * h))) + a2 = ((3 * ((b / (3 * a)) ^2)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by A5
.= ((3 * ((((3 * a) ") * b) ^2)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def_9
.= ((((3 * ((3 * a) ")) * b) * (((3 * a) ") * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2
.= ((((3 * ((3 ") * (a "))) * b) * (((3 * a) ") * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_1:204
.= (((b / a) * (((3 * a) ") * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def_9
.= (((b / a) * (b / (3 * a))) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def_9
.= (((b * b) / (a * (3 * a))) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_1:76
.= (((b ^2) / (3 * (a ^2))) - (2 * ((b / a) * (b / (3 * a))))) + (c / a) by A6, A7
.= (((b ^2) / (3 * (a ^2))) - (2 * ((b * b) / (a * (3 * a))))) + (c / a) by XCMPLX_1:76
.= (- ((b ^2) / (3 * (a ^2)))) + (((3 * a) / (3 * a)) * (c / a)) by A14
.= (- ((b ^2) / (3 * (a ^2)))) + (((3 * a) * c) / ((3 * a) * a)) by XCMPLX_1:76
.= (((3 * a) * c) / (3 * (a ^2))) - ((b ^2) / (3 * (a ^2)))
.= (((3 * a) * c) * ((3 * (a ^2)) ")) - ((b ^2) / (3 * (a ^2))) by XCMPLX_0:def_9
.= (((3 * a) * c) * ((3 * (a ^2)) ")) - ((b ^2) * ((3 * (a ^2)) ")) by XCMPLX_0:def_9
.= (((3 * a) * c) - (b ^2)) * ((3 * (a ^2)) ") ;
hence  ((3 * (h ^2)) + (2 * (a1 * h))) + a2 = (((3 * a) * c) - (b ^2)) / (3 * (a ^2)) by XCMPLX_0:def_9; ::_thesis: verum
end;
 ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 by A1, A3, A4, A5, A6, A7, A8, Th15;
hence  (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 by A6, A9, A13, A10; ::_thesis: verum
end;

theorem :: POLYEQ_1:17
for y, a, c, b, d being real number st (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 holds
for p, q being real number st p = (((3 * a) * c) - (b ^2)) / (3 * (a ^2)) & q = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) holds
Polynom (1,0,p,q,y) = 0 ;

theorem Th18: :: POLYEQ_1:18
for p, q, y being real number st Polynom (1,0,p,q,y) = 0 holds
for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 holds
( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 )
proof
let p, q, y be real number ; ::_thesis: ( Polynom (1,0,p,q,y) = 0 implies for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 holds
( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) )
assume A1: Polynom (1,0,p,q,y) = 0 ; ::_thesis: for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 holds
( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 )
let u, v be real number ; ::_thesis: ( y = u + v & ((3 * v) * u) + p = 0 implies ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) )
assume that
A2: y = u + v and
A3: ((3 * v) * u) + p = 0 ; ::_thesis: ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 )
(u + v) |^ 3 = ((u |^ 3) + (((3 * v) * (u ^2)) + ((3 * (v ^2)) * u))) + (v |^ 3) by Th14
.= ((u |^ 3) + (((3 * v) * u) * (u + v))) + (v |^ 3) ;
then  0 = (((u |^ 3) + (v |^ 3)) + ((((3 * v) * u) + p) * (u + v))) + q by A1, A2;
hence  (u |^ 3) + (v |^ 3) = - q by A3; ::_thesis: (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3
 3 * (v * u) = - p by A3;
hence  (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 by NEWTON:7; ::_thesis: verum
end;

theorem Th19: :: POLYEQ_1:19
for p, q, y being real number st Polynom (1,0,p,q,y) = 0 holds
for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) holds
y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))))
proof
let p, q, y be real number ; ::_thesis: ( Polynom (1,0,p,q,y) = 0 implies for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) holds
y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
set e1 = 1;
assume A1: Polynom (1,0,p,q,y) = 0 ; ::_thesis: for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) holds
y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))))
set e3 = (- (p / 3)) |^ 3;
set e2 = q;
let u, v be real number ; ::_thesis: ( y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) implies y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
assume that
A2: y = u + v and
A3: ((3 * v) * u) + p = 0 ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
set z2 = v |^ 3;
set z1 = u |^ 3;
A4: now__::_thesis:_for_z_being_real_number_holds_(z_-_(u_|^_3))_*_(z_-_(v_|^_3))_=_((z_^2)_+_(q_*_z))_+_((-_(p_/_3))_|^_3)
let z be real number ; ::_thesis: (z - (u |^ 3)) * (z - (v |^ 3)) = ((z ^2) + (q * z)) + ((- (p / 3)) |^ 3)
thus (z - (u |^ 3)) * (z - (v |^ 3)) = ((z ^2) - (((u |^ 3) + (v |^ 3)) * z)) + ((u |^ 3) * (v |^ 3))
.= ((z ^2) - ((- q) * z)) + ((u |^ 3) * (v |^ 3)) by A1, A2, A3, Th18
.= ((z ^2) + (q * z)) + ((- (p / 3)) |^ 3) by A1, A2, A3, Th18 ; ::_thesis: verum
end;
A5: (u |^ 3) + (v |^ 3) = - q by A1, A2, A3, Th18;
then  q ^2 = ((u |^ 3) + (v |^ 3)) ^2 by SQUARE_1:3;
then A6: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) = (- (- ((((u |^ 3) ^2) + ((2 * (u |^ 3)) * (v |^ 3))) + ((v |^ 3) ^2)))) - (4 * ((u |^ 3) * (v |^ 3))) by A1, A2, A3, Th18
.= ((u |^ 3) - (v |^ 3)) ^2 ;
then A7: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) >= 0 by XREAL_1:63;
then A8: delta (1,q,((- (p / 3)) |^ 3)) >= 0 by QUIN_1:def_1;
 ((u |^ 3) - (u |^ 3)) * ((u |^ 3) - (v |^ 3)) = 0 * ((u |^ 3) - (v |^ 3)) ;
then A9: Polynom (1,q,((- (p / 3)) |^ 3),(u |^ 3)) = 0 by A4;
 ((v |^ 3) - (u |^ 3)) * ((v |^ 3) - (v |^ 3)) = ((v |^ 3) - (u |^ 3)) * 0 ;
then A10: Polynom (1,q,((- (p / 3)) |^ 3),(v |^ 3)) = 0 by A4;
A11: (v |^ 3) * (u |^ 3) = (- (p / 3)) |^ 3 by A1, A2, A3, Th18;
now__::_thesis:_(_(_u_|^_3_=_((-_q)_+_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_or_(_u_|^_3_=_((-_q)_-_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_u_|^_3_=_(-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_-_((-_(p_/_3))_|^_3)))_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_)
percases ( u |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or u |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A9, A8, Th5;
caseA12: u |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
A13: (p / 3) |^ 3 = (p / 3) |^ (2 + 1)
.= ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6
.= (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6
.= ((p / 3) |^ 1) * ((p / 3) ^2)
.= ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41
.= (p / 3) * ((p / 3) ^2) by POWER:25 ;
A14: (q ^2) - (4 * ((- (p / 3)) |^ 3)) >= 0 by A6, XREAL_1:63;
A15: (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1)
.= ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6
.= (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6
.= ((- (p / 3)) |^ 1) * ((- (p / 3)) ^2) ;
then A16: (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41
.= (- (p / 3)) * ((p / 3) ^2) by POWER:25
.= - ((p / 3) * ((p / 3) ^2)) ;
A17: u |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A12, QUIN_1:def_1
.= ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62
.= ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A14, SQUARE_1:30
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
A18: now__::_thesis:_(_(_u_>_0_&_u_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_u_=_0_&_u_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_u_<_0_&_u_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_)
percases ( u > 0 or u = 0 or u < 0 ) by XXREAL_0:1;
caseA19: u > 0 ; ::_thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A20: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A17, A16, A13, PREPOWER:6;
then  u = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A17, A16, A13, A19, PREPOWER:def_2;
hence  u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A20, POWER:def_1; ::_thesis: verum
end;
caseA21: u = 0 ; ::_thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A22: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A17, A16, A13, NEWTON:11;
then  3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) = 0 by PREPOWER:def_2;
hence  u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A21, A22, POWER:def_1; ::_thesis: verum
end;
case u < 0 ; ::_thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A23: - u > 0 by XREAL_1:58;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A24: 3 -root (- 1) = - 1 by Lm1, POWER:8;
(- u) |^ 3 = (- u) |^ (2 + 1)
.= ((- u) |^ (1 + 1)) * (- u) by NEWTON:6
.= (((- u) |^ 1) * (- u)) * (- u) by NEWTON:6
.= ((- u) |^ 1) * ((- u) ^2) ;
then  (- u) |^ 3 = ((- u) to_power 1) * ((- u) ^2) by POWER:41;
then A25: (- u) |^ 3 = (- u) * (u ^2) by POWER:25
.= - (u * (u ^2)) ;
u |^ 3 = u |^ (2 + 1)
.= (u |^ (1 + 1)) * u by NEWTON:6
.= ((u |^ 1) * u) * u by NEWTON:6
.= (u |^ 1) * (u * u) ;
then A26: u |^ 3 = (u to_power 1) * (u ^2) by POWER:41;
then A27: (- u) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A17, A16, A13, A25, POWER:25;
A28: (- u) |^ 3 = - (u |^ 3) by A25, A26, POWER:25;
then A29: - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A17, A16, A13, A23, PREPOWER:6;
 - (u |^ 3) > 0 by A23, A28, PREPOWER:6;
then  - u = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A17, A16, A13, A23, A27, PREPOWER:def_2;
then  - u = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A29, POWER:def_1;
then  - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence  u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A24; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_(_v_|^_3_=_((-_q)_+_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_or_(_v_|^_3_=_((-_q)_-_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_)
percases ( v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A8, A10, Th5;
case v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
then  v |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by QUIN_1:def_1;
then  v |^ 3 = ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62;
then A30: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:30
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
A31: (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by A15, POWER:41
.= (- (p / 3)) * ((p / 3) ^2) by POWER:25 ;
now__::_thesis:_(_(_v_>_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_=_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_<_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_)
percases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;
caseA32: v > 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A33: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A13, A30, A31, PREPOWER:6;
then  v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A13, A30, A31, A32, PREPOWER:def_2;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A33, POWER:def_1; ::_thesis: verum
end;
caseA34: v = 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then  (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A13, A30, A31, NEWTON:11;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A34, POWER:5; ::_thesis: verum
end;
case v < 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A35: - v > 0 by XREAL_1:58;
then A36: (- v) |^ 3 > 0 by PREPOWER:6;
 (- v) |^ 3 = (- v) |^ (2 + 1) ;
then  (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6;
then  (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6;
then  (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then  (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41;
then  (- v) |^ 3 = (- v) * ((- v) ^2) by POWER:25;
then A37: (- v) |^ 3 = - (v * (v ^2)) ;
 v |^ 3 = v |^ (2 + 1) ;
then  v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6;
then  v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6;
then  v |^ 3 = (v |^ 1) * (v * v) ;
then A38: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41;
then  (- v) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A13, A30, A31, A37, POWER:25;
then A39: - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A35, A36, PREPOWER:def_2;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A40: 3 -root (- 1) = - 1 by Lm1, POWER:8;
 - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A13, A30, A31, A36, A37, A38, POWER:25;
then  - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A39, POWER:def_1;
then  - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A40; ::_thesis: verum
end;
end;
end;
hence  ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A18; ::_thesis: verum
end;
case v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
then  v |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by QUIN_1:def_1;
then  v |^ 3 = ((- q) / 2) - ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / 2) ;
then A41: v |^ 3 = (- (q / 2)) - (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:20, SQUARE_1:30
.= (- (q / 2)) - (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
now__::_thesis:_(_(_v_>_0_&_v_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_=_0_&_v_=_3_-Root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_&_v_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_<_0_&_v_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_)
percases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;
caseA42: v > 0 ; ::_thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then  (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A16, A13, A41, PREPOWER:6;
then A43: v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A16, A13, A41, A42, PREPOWER:def_2;
 (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A16, A13, A41, A42, PREPOWER:6;
hence  v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A43, POWER:def_1; ::_thesis: verum
end;
caseA44: v = 0 ; ::_thesis: ( v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) & v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) )
then A45: (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A16, A13, A41, NEWTON:11;
hence  v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A44, PREPOWER:def_2; ::_thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
hence  v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A45, POWER:def_1; ::_thesis: verum
end;
case v < 0 ; ::_thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A46: - v > 0 by XREAL_1:58;
set r = (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A47: 3 -root (- 1) = - 1 by Lm1, POWER:8;
 v |^ 3 = v |^ (2 + 1) ;
then  v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6;
then A48: v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6;
 (- v) |^ 3 = (- v) |^ (2 + 1) ;
then  (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6;
then  (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6;
then  (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then A49: (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41
.= (- v) * (v ^2) by POWER:25
.= - (v * (v ^2)) ;
A50: v to_power 1 = v by POWER:25;
then  (- v) |^ 3 = - (v |^ 3) by A49, A48, POWER:41;
then A51: - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A16, A13, A41, A46, PREPOWER:6;
 (- v) |^ 3 = - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A16, A13, A41, A49, A48, A50, POWER:41;
then  - v = 3 -Root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A46, A51, PREPOWER:def_2;
then  - v = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A51, POWER:def_1;
then  - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence  v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A47; ::_thesis: verum
end;
end;
end;
hence  ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A18; ::_thesis: verum
end;
end;
end;
hence  ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; ::_thesis: verum
end;
caseA52: u |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( u |^ 3 = (- (q / 2)) - (sqrt (((q ^2) / 4) - ((- (p / 3)) |^ 3))) & ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) )
 (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) ;
then  (- (p / 3)) |^ 3 = ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6;
then  (- (p / 3)) |^ 3 = (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6;
then  (- (p / 3)) |^ 3 = ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ;
then  (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41;
then  (- (p / 3)) |^ 3 = (- (p / 3)) * ((- (p / 3)) ^2) by POWER:25;
then A53: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ;
 u |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A52, QUIN_1:def_1;
then A54: u |^ 3 = ((- q) * (2 ")) - ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / 2)
.= (- (q / 2)) - (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:20, SQUARE_1:30
.= (- (q / 2)) - (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
hence  u |^ 3 = (- (q / 2)) - (sqrt (((q ^2) / 4) - ((- (p / 3)) |^ 3))) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
 (p / 3) |^ 3 = (p / 3) |^ (2 + 1) ;
then  (p / 3) |^ 3 = ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6;
then  (p / 3) |^ 3 = (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6;
then  (p / 3) |^ 3 = ((p / 3) |^ 1) * ((p / 3) * (p / 3)) ;
then  (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41;
then A55: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A53, POWER:25;
A56: now__::_thesis:_(_(_u_>_0_&_u_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_u_=_0_&_u_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_u_<_0_&_u_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_)
percases ( u > 0 or u = 0 or u < 0 ) by XXREAL_0:1;
caseA57: u > 0 ; ::_thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then  (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A54, A55, PREPOWER:6;
then A58: u = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A54, A55, A57, PREPOWER:def_2;
 (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A54, A55, A57, PREPOWER:6;
hence  u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A58, POWER:def_1; ::_thesis: verum
end;
caseA59: u = 0 ; ::_thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then  (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A54, A55, NEWTON:11;
hence  u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A59, POWER:5; ::_thesis: verum
end;
case u < 0 ; ::_thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A60: - u > 0 by XREAL_1:58;
then A61: (- u) |^ 3 > 0 by PREPOWER:6;
 (- u) |^ 3 = (- u) |^ (2 + 1) ;
then  (- u) |^ 3 = ((- u) |^ (1 + 1)) * (- u) by NEWTON:6;
then  (- u) |^ 3 = (((- u) |^ 1) * (- u)) * (- u) by NEWTON:6;
then  (- u) |^ 3 = ((- u) |^ 1) * ((- u) * (- u)) ;
then  (- u) |^ 3 = ((- u) to_power 1) * ((- u) ^2) by POWER:41;
then  (- u) |^ 3 = (- u) * ((- u) ^2) by POWER:25;
then A62: (- u) |^ 3 = - (u * (u ^2)) ;
 u |^ 3 = u |^ (2 + 1) ;
then  u |^ 3 = (u |^ (1 + 1)) * u by NEWTON:6;
then  u |^ 3 = ((u |^ 1) * u) * u by NEWTON:6;
then  u |^ 3 = (u |^ 1) * (u * u) ;
then A63: u |^ 3 = (u to_power 1) * (u ^2) by POWER:41;
then  - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A54, A55, A61, A62, POWER:25;
then A64: 3 -Root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) = 3 -root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by POWER:def_1;
set r = (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
 (- u) |^ 3 = - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A54, A55, A62, A63, POWER:25;
then  - u = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A60, A61, A64, PREPOWER:def_2;
then A65: - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
 3 -root (- 1) = - 1 by Lm1, POWER:8;
hence  u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A65; ::_thesis: verum
end;
end;
end;
now__::_thesis:_(_(_v_|^_3_=_((-_q)_+_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_or_(_v_|^_3_=_((-_q)_-_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)
percases ( v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A8, A10, Th5;
caseA66: v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) )
 (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) ;
then  (- (p / 3)) |^ 3 = ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6;
then  (- (p / 3)) |^ 3 = (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6;
then  (- (p / 3)) |^ 3 = ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ;
then  (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41;
then  (- (p / 3)) |^ 3 = (- (p / 3)) * ((- (p / 3)) ^2) by POWER:25;
then A67: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ;
 (p / 3) |^ 3 = (p / 3) |^ (2 + 1) ;
then  (p / 3) |^ 3 = ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6;
then  (p / 3) |^ 3 = (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6;
then  (p / 3) |^ 3 = ((p / 3) |^ 1) * ((p / 3) * (p / 3)) ;
then  (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41;
then A68: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A67, POWER:25;
 v |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A66, QUIN_1:def_1;
then  v |^ 3 = ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62;
then A69: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:30
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
now__::_thesis:_(_(_v_>_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_=_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_<_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_)
percases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;
caseA70: v > 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A71: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A69, A68, PREPOWER:6;
then  v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A69, A68, A70, PREPOWER:def_2;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A71, POWER:def_1; ::_thesis: verum
end;
caseA72: v = 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then  (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A69, A68, NEWTON:11;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A72, POWER:5; ::_thesis: verum
end;
case v < 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A73: - v > 0 by XREAL_1:58;
then A74: (- v) |^ 3 > 0 by PREPOWER:6;
 (- v) |^ 3 = (- v) |^ (2 + 1) ;
then  (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6;
then  (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6;
then  (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ;
then  (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41;
then  (- v) |^ 3 = (- v) * ((- v) ^2) by POWER:25;
then A75: (- v) |^ 3 = - (v * (v ^2)) ;
 v |^ 3 = v |^ (2 + 1) ;
then  v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6;
then  v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6;
then  v |^ 3 = (v |^ 1) * (v * v) ;
then A76: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41;
then A77: - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A69, A68, A74, A75, POWER:25;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
A78: 3 -root (- 1) = - 1 by Lm1, POWER:8;
 v |^ 3 = v * (v ^2) by A76, POWER:25;
then  - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A69, A68, A73, A74, A75, PREPOWER:def_2;
then  - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A77, POWER:def_1;
then  - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A78; ::_thesis: verum
end;
end;
end;
hence  ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A56; ::_thesis: verum
end;
caseA79: v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))))
 q ^2 = ((u |^ 3) + (v |^ 3)) ^2 by A5, SQUARE_1:3;
then A80: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) = ((u |^ 3) - (v |^ 3)) ^2 by A11;
(- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1)
.= ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6
.= (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6
.= ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ;
then (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41
.= (- (p / 3)) * ((p / 3) ^2) by POWER:25 ;
then A81: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ;
(p / 3) |^ 3 = (p / 3) |^ (2 + 1)
.= ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6
.= (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6
.= ((p / 3) |^ 1) * ((p / 3) ^2) ;
then  (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41;
then A82: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A81, POWER:25;
 v |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A79, QUIN_1:def_1;
then A83: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A52, A79, A80, SQUARE_1:17
.= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ;
now__::_thesis:_(_(_v_>_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_=_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_<_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_)
percases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1;
caseA84: v > 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A85: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A83, A82, PREPOWER:6;
then  v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A83, A82, A84, PREPOWER:def_2;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A85, POWER:def_1; ::_thesis: verum
end;
caseA86: v = 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then  v |^ 3 = 0 by NEWTON:11;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A83, A82, A86, POWER:5; ::_thesis: verum
end;
case v < 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))
then A87: - v > 0 by XREAL_1:58;
then A88: (- v) |^ 3 > 0 by PREPOWER:6;
set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)));
v |^ 3 = v |^ (2 + 1)
.= (v |^ (1 + 1)) * v by NEWTON:6
.= ((v |^ 1) * v) * v by NEWTON:6
.= (v |^ 1) * (v ^2) ;
then A89: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41;
(- v) |^ 3 = (- v) |^ (2 + 1)
.= ((- v) |^ (1 + 1)) * (- v) by NEWTON:6
.= (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6
.= ((- v) |^ 1) * ((- v) ^2)
.= ((- v) to_power 1) * ((- v) ^2) by POWER:41
.= (- v) * (v ^2) by POWER:25 ;
then A90: (- v) |^ 3 = - (v * (v ^2)) ;
then A91: - (v |^ 3) > 0 by A88, A89, POWER:25;
A92: 3 -root (- 1) = - 1 by Lm1, POWER:8;
 (- v) |^ 3 = - (v |^ 3) by A90, A89, POWER:25;
then  - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A83, A82, A87, A88, PREPOWER:def_2;
then  - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A83, A82, A91, POWER:def_1;
then  - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11;
hence  v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A92; ::_thesis: verum
end;
end;
end;
hence  y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A2, A56; ::_thesis: verum
end;
end;
end;
hence  ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; ::_thesis: verum
end;
end;
end;
hence  ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; ::_thesis: verum
end;

theorem :: POLYEQ_1:20
for b, c, d, x being real number st b <> 0 & delta (b,c,d) > 0 & Polynom (0,b,c,d,x) = 0 & not x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) holds
x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b)
proof
let b, c, d, x be real number ; ::_thesis: ( b <> 0 & delta (b,c,d) > 0 & Polynom (0,b,c,d,x) = 0 & not x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) implies x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) )
assume A1: ( b <> 0 & delta (b,c,d) > 0 ) ; ::_thesis: ( not Polynom (0,b,c,d,x) = 0 or x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) )
assume  Polynom (0,b,c,d,x) = 0 ; ::_thesis: ( x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) )
then  Polynom (b,c,d,x) = 0 ;
hence  ( x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) ) by A1, Th5; ::_thesis: verum
end;

theorem :: POLYEQ_1:21
for a, p, c, q, d, x being real number st a <> 0 & p = c / a & q = d / a & Polynom (a,0,c,d,x) = 0 holds
for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds
x = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3)))))
proof
let a, p, c, q, d, x be real number ; ::_thesis: ( a <> 0 & p = c / a & q = d / a & Polynom (a,0,c,d,x) = 0 implies for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds
x = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) )
assume that
A1: a <> 0 and
A2: p = c / a and
A3: q = d / a ; ::_thesis: ( not Polynom (a,0,c,d,x) = 0 or for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds
x = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) )
A4: ( p / 3 = c / (3 * a) & - (q / 2) = - (d / (2 * a)) ) by A2, A3, XCMPLX_1:78;
assume  Polynom (a,0,c,d,x) = 0 ; ::_thesis: for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds
x = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3)))))
then  (a ") * (((a * (x |^ 3)) + (c * x)) + d) = 0 ;
then  (((a ") * a) * (x |^ 3)) + ((a ") * ((c * x) + d)) = 0 ;
then  (1 * (x |^ 3)) + ((a ") * ((c * x) + d)) = 0 by A1, XCMPLX_0:def_7;
then  (x |^ 3) + ((((a ") * c) * x) + ((a ") * d)) = 0 ;
then  (x |^ 3) + (((c / a) * x) + ((a ") * d)) = 0 by XCMPLX_0:def_9;
then  (x |^ 3) + (((c / a) * x) + (d / a)) = 0 by XCMPLX_0:def_9;
then A5: Polynom (1,0,p,q,x) = 0 by A2, A3;
 (q ^2) / 4 = ((d ^2) / (a ^2)) / 4 by A3, XCMPLX_1:76;
then A6: (q ^2) / 4 = (d ^2) / (4 * (a ^2)) by XCMPLX_1:78;
let u, v be real number ; ::_thesis: ( x = u + v & ((3 * v) * u) + p = 0 & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) implies x = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) )
assume  ( x = u + v & ((3 * v) * u) + p = 0 ) ; ::_thesis: ( x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) or x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) or x = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) )
hence  ( x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) or x = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) or x = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) ) by A5, A4, A6, Th19; ::_thesis: verum
end;

theorem :: POLYEQ_1:22
for a, b, c, x being real number st 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) holds
x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)
proof
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) )
 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;
 x |^ 1 = x to_power 1 by POWER:41;
then A3: x |^ 3 = (x ^2) * x by A2, POWER:25;
assume  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) )
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; ::_thesis: verum
end;

theorem :: POLYEQ_1:23
for a, c, x being real number st a <> 0 & c / a < 0 & Polynom (a,0,c,0,x) = 0 & not x = 0 & not x = sqrt (- (c / a)) holds
x = - (sqrt (- (c / a)))
proof
let a, c, x be real number ; ::_thesis: ( a <> 0 & c / a < 0 & Polynom (a,0,c,0,x) = 0 & not x = 0 & not x = sqrt (- (c / a)) implies x = - (sqrt (- (c / a))) )
assume that
A1: a <> 0 and
A2: c / a < 0 ; ::_thesis: ( not Polynom (a,0,c,0,x) = 0 or x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
 x |^ 3 = x |^ (2 + 1) ;
then  x |^ 3 = (x |^ (1 + 1)) * x by NEWTON:6;
then A3: x |^ 3 = ((x |^ 1) * x) * x by NEWTON:6;
 x |^ 1 = x to_power 1 by POWER:41;
then A4: x |^ 3 = (x ^2) * x by A3, POWER:25;
assume  Polynom (a,0,c,0,x) = 0 ; ::_thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
then  ((a * (x ^2)) + c) * x = 0 by A4;
then A5: ( x = 0 or (a * (x ^2)) + c = 0 ) by XCMPLX_1:6;
now__::_thesis:_(_(_x_>_0_&_(_x_=_0_or_x_=_sqrt_(-_(c_/_a))_or_x_=_-_(sqrt_(-_(c_/_a)))_)_)_or_(_x_<_0_&_(_x_=_0_or_x_=_sqrt_(-_(c_/_a))_or_x_=_-_(sqrt_(-_(c_/_a)))_)_)_or_(_x_=_0_&_(_x_=_0_or_x_=_sqrt_(-_(c_/_a))_or_x_=_-_(sqrt_(-_(c_/_a)))_)_)_)
percases ( x > 0 or x < 0 or x = 0 ) by XXREAL_0:1;
caseA6: x > 0 ; ::_thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
 x |^ 2 = x |^ (1 + 1) ;
then  x |^ 2 = (x |^ 1) * x by NEWTON:6;
then  x |^ 2 = (x to_power 1) * x by POWER:41;
then A7: x |^ 2 = x * x by POWER:25;
A8: - (c / a) > 0 by A2, XREAL_1:58;
 x ^2 = (- c) / a by A1, A5, A6, XCMPLX_1:89;
then  x ^2 = (- c) * (a ") by XCMPLX_0:def_9;
then  x ^2 = - (c * (a ")) ;
then  x ^2 = - (c / a) by XCMPLX_0:def_9;
then  x = 2 -Root (- (c / a)) by A6, A8, A7, PREPOWER:def_2;
hence  ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) by A8, PREPOWER:32; ::_thesis: verum
end;
caseA9: x < 0 ; ::_thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
 (- x) |^ 2 = (- x) |^ (1 + 1) ;
then  (- x) |^ 2 = ((- x) |^ 1) * (- x) by NEWTON:6;
then  (- x) |^ 2 = ((- x) to_power 1) * (- x) by POWER:41;
then A10: (- x) |^ 2 = (- x) * (- x) by POWER:25;
 x ^2 = (- c) / a by A1, A5, A9, XCMPLX_1:89;
then  x ^2 = (- c) * (a ") by XCMPLX_0:def_9;
then  x ^2 = - (c * (a ")) ;
then A11: (- x) ^2 = - (c / a) by XCMPLX_0:def_9;
A12: - (c / a) > 0 by A2, XREAL_1:58;
 - x > 0 by A9, XREAL_1:58;
then  - x = 2 -Root (- (c / a)) by A11, A12, A10, PREPOWER:def_2;
then  - x = sqrt (- (c / a)) by A12, PREPOWER:32;
hence  ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; ::_thesis: verum
end;
case x = 0 ; ::_thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) )
hence  ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; ::_thesis: verum
end;
end;
end;
hence  ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; ::_thesis: verum
end;