:: POLYEQ_2 semantic presentation

begin

 4 = 2 * 2
;

then  2 divides 4
by INT_1:def_3;

then Lm1:  4 is even
by ABIAN:def_1;

 3 = (2 * 1) + 1
;

then Lm2:  3 is odd
by ABIAN:1;

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

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

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

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

theorem :: POLYEQ_2:1
for a, c, e, x being real number st a <> 0 & e <> 0 & (c ^2) - ((4 * a) * e) > 0 & Polynom (a,0,c,0,e,x) = 0 holds
( 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))) ) )
proof
let a, c, e, x be real number ; ::_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;
percases ( x > 0 or x < 0 ) by A5, XXREAL_0:1;
supposeA6: 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  ( abs x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or abs 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;
supposeA8: 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  ( abs x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or abs 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;
end;

theorem Th2: :: POLYEQ_2:2
for a, b, c, x, y being real number st a <> 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 holds
( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 )
proof
let a, b, c, x, y be real number ; ::_thesis: ( a <> 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 implies ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) )
assume that
A1: a <> 0 and
A2: y = x + (1 / x) ; ::_thesis: ( not Polynom (a,b,c,b,a,x) = 0 or ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) )
assume A3: Polynom (a,b,c,b,a,x) = 0 ; ::_thesis: ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 )
A4: x <> 0
proof
assume  x = 0 ; ::_thesis: contradiction
then  ((a * (0 to_power 4)) + (b * (0 |^ 3))) + a = 0 by A3;
then  ((a * 0) + (b * (0 |^ 3))) + a = 0 by POWER:def_2;
then  ((a * 0) + (b * 0)) + a = 0 by NEWTON:11;
hence  contradiction by A1; ::_thesis: verum
end;
then A5: x ^2 > 0 by SQUARE_1:12;
A6: x |^ 4 = x to_power (2 + 2) by POWER:41;
A7: now__::_thesis:_(_(_x_>_0_&_a_*_((x_^2)_+_(1_/_(x_^2)))_=_(-_(b_*_(x_+_(1_/_x))))_-_c_&_((x_^2)_-_(x_*_y))_+_1_=_0_)_or_(_x_<_0_&_a_*_((x_^2)_+_(1_/_(x_^2)))_=_(-_(b_*_(x_+_(1_/_x))))_-_c_&_((x_^2)_-_(x_*_y))_+_1_=_0_)_)
percases ( x > 0 or x < 0 ) by A4, XXREAL_0:1;
caseA8: x > 0 ; ::_thesis: ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 )
set n = - ((b * x) + a);
set m = (a * (x ^2)) + ((b * x) + c);
x |^ 3 = x to_power (2 + 1) by POWER:41
.= (x to_power 2) * (x to_power 1) by A8, POWER:27 ;
then A9: x |^ 3 = (x to_power 2) * x by POWER:25
.= (x ^2) * x by POWER:46 ;
x |^ 4 = (x to_power 2) * (x to_power 2) by A6, A8, POWER:27
.= (x ^2) * (x to_power 2) by POWER:46
.= (x ^2) * (x ^2) by POWER:46 ;
then  ((a * (x ^2)) + ((b * x) + c)) * (x ^2) = (- ((b * x) + a)) * 1 by A3, A9;
then  ((a * (x ^2)) + ((b * x) + c)) / 1 = (- ((b * x) + a)) / (x ^2) by A5, XCMPLX_1:94;
then (a * (x ^2)) + ((b * x) + c) = (- ((b * x) + a)) * (1 / (x ^2)) by XCMPLX_1:99
.= (- ((b * x) + a)) * ((x ^2) ") by XCMPLX_1:215
.= (- (b * (x * ((x ^2) ")))) - (a * ((x ^2) ")) ;
then  a * ((x ^2) + ((x ^2) ")) = (- (b * ((x * ((x ^2) ")) + x))) - c ;
then A10: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((x * ((x ^2) ")) + x))) - c by XCMPLX_1:215
.= (- (b * ((x * (1 / (x ^2))) + x))) - c by XCMPLX_1:215 ;
 1 / (x * x) = (1 / x) * (1 / x) by XCMPLX_1:102;
then  a * ((x ^2) + (1 / (x ^2))) = (- (b * (((x * (1 / x)) * (1 / x)) + x))) - c by A10;
then A11: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((1 * (1 / x)) + x))) - c by A8, XCMPLX_1:106;
 x * y = (x * x) + (x * (1 / x)) by A2;
then  (x * y) + 0 = (x ^2) + 1 by A4, XCMPLX_1:106;
hence  ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) by A11; ::_thesis: verum
end;
caseA12: x < 0 ; ::_thesis: ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 )
set n = - ((b * x) + a);
set m = (a * (x ^2)) + ((b * x) + c);
((- x) |^ 3) + (x |^ 3) = - ((x |^ 3) + (- (x |^ 3))) by Lm2, POWER:2
.= (x |^ 3) - (x |^ 3) ;
then A13: x |^ 3 = - ((- x) |^ 3) ;
A14: 0 < - x by A12, XREAL_1:58;
 (- x) |^ 4 = x |^ 4 by Lm1, POWER:1;
then A15: x |^ 4 = (- x) to_power (2 + 2) by POWER:41
.= ((- x) to_power 2) * ((- x) to_power 2) by A14, POWER:27
.= ((- x) ^2) * ((- x) to_power 2) by POWER:46
.= (x ^2) * ((- x) ^2) by POWER:46 ;
(- x) |^ 3 = (- x) to_power (2 + 1) by POWER:41
.= ((- x) to_power 2) * ((- x) to_power 1) by A14, POWER:27 ;
then A16: (- x) |^ 3 = ((- x) to_power 2) * (- x) by POWER:25;
(- x) to_power 2 = (- x) ^2 by POWER:46
.= x ^2 ;
then  ((a * (x ^2)) + ((b * x) + c)) * (x ^2) = (- ((b * x) + a)) * 1 by A3, A15, A16, A13;
then  ((a * (x ^2)) + ((b * x) + c)) / 1 = (- ((b * x) + a)) / (x ^2) by A5, XCMPLX_1:94;
then (a * (x ^2)) + ((b * x) + c) = (- ((b * x) + a)) * (1 / (x ^2)) by XCMPLX_1:99
.= (- ((b * x) + a)) * ((x ^2) ") by XCMPLX_1:215
.= (- (b * (x * ((x ^2) ")))) - (a * ((x ^2) ")) ;
then  a * ((x ^2) + ((x ^2) ")) = (- (b * ((x * ((x ^2) ")) + x))) - c ;
then a * ((x ^2) + (1 / (x ^2))) = (- (b * ((x * ((x ^2) ")) + x))) - c by XCMPLX_1:215
.= (- (b * ((x * (1 / (x ^2))) + x))) - c by XCMPLX_1:215 ;
then a * ((x ^2) + (1 / (x ^2))) = (- (b * ((x * ((1 / x) * (1 / x))) + x))) - c by XCMPLX_1:102
.= (- (b * (((x * (1 / x)) * (1 / x)) + x))) - c ;
then A17: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((1 * (1 / x)) + x))) - c by A12, XCMPLX_1:106;
x * y = (x * x) + (x * (1 / x)) by A2
.= (x * x) + 1 by A12, XCMPLX_1:106 ;
hence  ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) by A17; ::_thesis: verum
end;
end;
end;
y ^2 = ((x ^2) + (2 * (x * (1 / x)))) + ((1 / x) ^2) by A2
.= ((x ^2) + (2 * 1)) + ((1 / x) ^2) by A4, XCMPLX_1:106
.= ((x ^2) + 2) + ((1 ^2) / (x ^2)) by XCMPLX_1:76
.= (x ^2) - ((- 2) - (1 / (x ^2))) ;
then  (a * (y ^2)) - (2 * a) = (- (b * y)) - c by A2, A7;
hence  ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) by A4; ::_thesis: verum
end;

theorem :: POLYEQ_2:3
for a, b, c, x, y being real number st a <> 0 & ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) > 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 holds
for y1, y2 being real number st y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) holds
( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) )
proof
let a, b, c, x, y be real number ; ::_thesis: ( a <> 0 & ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) > 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 implies for y1, y2 being real number st y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) holds
( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) )
assume that
A1: a <> 0 and
A2: ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) > 0 and
A3: y = x + (1 / x) and
A4: Polynom (a,b,c,b,a,x) = 0 ; ::_thesis: for y1, y2 being real number st y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) holds
( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) )
A5: x <> 0 by A1, A3, A4, Th2;
set f = c - (2 * a);
 (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 by A1, A3, A4, Th2;
then  ((a * (y ^2)) + (b * y)) + (c - (2 * a)) = 0 ;
then A6: Polynom (a,b,(c - (2 * a)),y) = 0 by POLYEQ_1:def_2;
let y1, y2 be real number ; ::_thesis: ( y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) implies ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) )
assume A7: ( y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) ) ; ::_thesis: ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) )
 x * y = (x ^2) + (x * (1 / x)) by A3;
then  (x * y) + 0 = (x ^2) + 1 by A5, XCMPLX_1:106;
then  ((1 * (x ^2)) + ((- y) * x)) + 1 = 0 ;
then A8: Polynom (1,(- y),1,x) = 0 by POLYEQ_1:def_2;
delta (1,(- y),1) = ((- y) ^2) - ((4 * 1) * 1) by QUIN_1:def_1
.= (((x ^2) + (2 * (x * (1 / x)))) + ((1 / x) ^2)) - 4 by A3
.= (((x ^2) + (2 * 1)) + ((1 / x) ^2)) - 4 by A5, XCMPLX_1:106
.= (x ^2) + ((- (2 * 1)) + ((1 / x) ^2))
.= (x ^2) + ((- (2 * (x * (1 / x)))) + ((1 / x) ^2)) by A5, XCMPLX_1:106
.= (x - (1 / x)) ^2 ;
then A9: ( x = ((- (- y)) + (sqrt (delta (1,(- y),1)))) / (2 * 1) or x = ((- (- y)) - (sqrt (delta (1,(- y),1)))) / (2 * 1) ) by A8, POLYEQ_1:5, XREAL_1:63;
A10: (b ^2) - ((4 * a) * (c - (2 * a))) = ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) ;
then  delta (a,b,(c - (2 * a))) > 0 by A2, QUIN_1:def_1;
then  ( y = ((- b) + (sqrt (delta (a,b,(c - (2 * a)))))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,(c - (2 * a)))))) / (2 * a) ) by A1, A6, POLYEQ_1:5;
then  ( y = y1 or y = y2 ) by A7, A10, QUIN_1:def_1;
hence  ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) by A1, A3, A4, A9, Th2; ::_thesis: verum
end;

theorem Th4: :: POLYEQ_2:4
for x being real number holds
( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 )
proof
let x be real number ; ::_thesis: ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 )
percases ( x = 0 or x > 0 or x < 0 ) by XXREAL_0:1;
suppose x = 0 ; ::_thesis: ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 )
hence  ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) by NEWTON:11; ::_thesis: verum
end;
supposeA1: x > 0 ; ::_thesis: ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 )
(x |^ 3) * x = (x |^ 3) * (x to_power 1) by POWER:25
.= (x to_power 3) * (x to_power 1) ;
then A2: (x |^ 3) * x = x to_power (3 + 1) by A1, POWER:27;
 x ^2 = x to_power 2 by POWER:46;
then (x ^2) * x = (x to_power 2) * (x to_power 1) by POWER:25
.= x to_power (2 + 1) by A1, POWER:27
.= x |^ 3 by POWER:41 ;
hence  ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) by A2, POWER:41; ::_thesis: verum
end;
suppose x < 0 ; ::_thesis: ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 )
then A3: - x > 0 by XREAL_1:58;
((- x) |^ 3) + (x |^ 3) = - ((x |^ 3) + (- (x |^ 3))) by Lm2, POWER:2
.= (x |^ 3) - (x |^ 3) ;
then A4: (x |^ 3) + (((- x) |^ 3) - ((- x) |^ 3)) = 0 - ((- x) |^ 3) ;
A5: (- x) to_power 2 = (- x) ^2 by POWER:46
.= x ^2 ;
(- x) |^ 3 = (- x) to_power (2 + 1) by POWER:41
.= ((- x) to_power 2) * ((- x) to_power 1) by A3, POWER:27 ;
then A6: (- x) |^ 3 = ((- x) to_power 2) * (- x) by POWER:25;
 (- x) |^ 4 = x |^ 4 by Lm1, POWER:1;
then x |^ 4 = (- x) to_power (3 + 1) by POWER:41
.= ((- x) to_power 3) * ((- x) to_power 1) by A3, POWER:27
.= ((- x) |^ 3) * ((- x) to_power 1) ;
then x |^ 4 = ((- x) |^ 3) * (- x) by POWER:25
.= (x ^2) * (x * x) by A6, A5 ;
hence  ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) by A6, A5, A4; ::_thesis: verum
end;
end;
end;

theorem Th5: :: POLYEQ_2:5
for x, y being real number st x + y <> 0 holds
(x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y)
proof
let x, y be real number ; ::_thesis: ( x + y <> 0 implies (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) )
assume A1: x + y <> 0 ; ::_thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y)
percases ( x + y > 0 or x + y < 0 ) by A1, XXREAL_0:1;
supposeA2: x + y > 0 ; ::_thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y)
(x + y) |^ 4 = (x + y) to_power (3 + 1) by POWER:41
.= ((x + y) to_power 3) * ((x + y) to_power 1) by A2, POWER:27
.= ((x + y) to_power 3) * (x + y) by POWER:25 ;
then (x + y) |^ 4 = ((x + y) |^ 3) * (x + y)
.= (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * (x + y) by POLYEQ_1:14 ;
hence  (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) ; ::_thesis: verum
end;
suppose x + y < 0 ; ::_thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y)
then A3: - (x + y) > 0 by XREAL_1:58;
 (- (x + y)) |^ 4 = (x + y) |^ 4 by Lm1, POWER:1;
then (x + y) |^ 4 = (- (x + y)) to_power (3 + 1) by POWER:41
.= ((- (x + y)) to_power 3) * ((- (x + y)) to_power 1) by A3, POWER:27
.= ((- (x + y)) |^ 3) * ((- (x + y)) to_power 1) ;
then  (x + y) |^ 4 = ((- (x + y)) |^ 3) * (- (x + y)) by POWER:25;
then (x + y) |^ 4 = (- ((x + y) |^ 3)) * (- (x + y)) by Lm2, POWER:2
.= ((x + y) |^ 3) * (x + y)
.= (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * (x + y) by POLYEQ_1:14 ;
hence  (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) ; ::_thesis: verum
end;
end;
end;

theorem :: POLYEQ_2:6
for x, y being real number st x + y <> 0 holds
(x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4)
proof
let x, y be real number ; ::_thesis: ( x + y <> 0 implies (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4) )
set g = (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x;
set h = (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y;
set p = y |^ 3;
set q = x |^ 3;
set u = x |^ 4;
set v = y |^ 4;
A1: (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x = (((x |^ 3) * x) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * x)) + ((y |^ 3) * x) ;
A2: y |^ 3 = (y ^2) * y by Th4;
assume  x + y <> 0 ; ::_thesis: (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4)
then A3: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) by Th5;
(((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y = (((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + ((y |^ 3) * y)
.= (((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4) by Th4 ;
then (x + y) |^ 4 = (((x |^ 4) + (((3 * y) * ((x ^2) * x)) - ((- ((3 * (y ^2)) * x)) * x))) + ((y |^ 3) * x)) + ((((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4)) by A3, A1, Th4
.= (((x |^ 4) + (((3 * y) * (x |^ 3)) - (- ((3 * (y ^2)) * (x ^2))))) + ((y |^ 3) * x)) + ((((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4)) by Th4
.= (((x |^ 4) + ((3 * y) * (x |^ 3))) + (((3 * (y ^2)) * (x ^2)) + ((y |^ 3) * x))) + ((((x |^ 3) * y) + (((3 * (y ^2)) * (x ^2)) + (((3 * (y ^2)) * x) * y))) + (y |^ 4)) ;
hence  (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4) by A2; ::_thesis: verum
end;

theorem Th7: :: POLYEQ_2:7
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds
( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 )
proof
set x = - 1;
let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be real number ; ::_thesis: ( ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) implies ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) )
A1: ( 0 |^ 3 = 0 & 0 |^ 4 = 0 ) by NEWTON:11;
assume A2: for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ; ::_thesis: ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 )
then A3: Polynom (a1,a2,a3,a4,a5,(- 1)) = Polynom (b1,b2,b3,b4,b5,(- 1)) ;
A4: ( 1 |^ 3 = 1 & 1 |^ 4 = 1 ) by NEWTON:10;
A5: ( (- 1) |^ 3 = ((- 1) ^2) * (- 1) & ((- 1) |^ 3) * (- 1) = (- 1) |^ 4 ) by Th4;
 ( Polynom (a1,a2,a3,a4,a5,0) = Polynom (b1,b2,b3,b4,b5,0) & Polynom (a1,a2,a3,a4,a5,1) = Polynom (b1,b2,b3,b4,b5,1) ) by A2;
hence  ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) by A1, A4, A3, A5; ::_thesis: verum
end;

theorem Th8: :: POLYEQ_2:8
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds
( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 )
proof
let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be real number ; ::_thesis: ( ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) implies ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) )
assume  for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ; ::_thesis: ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 )
then  ( ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) by Th7;
hence  ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) ; ::_thesis: verum
end;

theorem Th9: :: POLYEQ_2:9
for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds
( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 )
proof
A1: (- 2) |^ 3 = ((- 2) ^2) * (- 2) by Th4
.= - (4 * 2) ;
A2: (- 2) |^ 4 = 16 by Lm1, POWER:1, POWER:62;
let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be real number ; ::_thesis: ( ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) implies ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) )
assume A3: for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ; ::_thesis: ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 )
then A4: Polynom (a1,a2,a3,a4,a5,(- 2)) = Polynom (b1,b2,b3,b4,b5,(- 2)) ;
A5: ( a5 = b5 & Polynom (a1,a2,a3,a4,a5,2) = Polynom (b1,b2,b3,b4,b5,2) ) by A3, Th7;
 ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) by A3, Th8;
hence  ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) by A5, A4, A2, A1, POWER:61, POWER:62; ::_thesis: verum
end;

definition
let a1, x1, x2, x3, x4, x be real number ;
func Four0 (a1,x1,x2,x3,x4,x) ->  set  equals :: POLYEQ_2:def 2
a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4));
correctness
coherence
a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) is set ;
;
end;

:: deftheorem  defines Four0 POLYEQ_2:def_2_:_
 for a1, x1, x2, x3, x4, x being real number holds Four0 (a1,x1,x2,x3,x4,x) = a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4));

registration
let a1, x1, x2, x3, x4, x be real number ;
cluster Four0 (a1,x1,x2,x3,x4,x) ->  real ;
coherence
 Four0 (a1,x1,x2,x3,x4,x) is real ;
end;

theorem Th10: :: POLYEQ_2:10
for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) holds
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4)
proof
let a1, a2, a3, a4, a5, x, x1, x2, x3, x4 be real number ; ::_thesis: ( a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) implies (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) )
assume A1: a1 <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) or (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) )
set z = (((x - x1) * (x - x2)) * (x - x3)) * (x - x4);
set w = ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5;
assume  for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ; ::_thesis: (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4)
then  Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ;
then  (((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) * a1) - (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) = (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) - (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) by A1, XCMPLX_1:87;
then  (((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) - ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4))) * a1 = 0 ;
then  ((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) + (- ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4))) = 0 - 0 by A1, XCMPLX_1:6;
hence  (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) ; ::_thesis: verum
end;

theorem Th11: :: POLYEQ_2:11
for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) holds
(((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)
proof
let a1, a2, a3, a4, a5, x, x1, x2, x3, x4 be real number ; ::_thesis: ( a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) implies (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) )
assume A1: a1 <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) or (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) )
set w = ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5;
assume  for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ; ::_thesis: (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4)
then  (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) by A1, Th10;
then  (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - ((((x1 + x2) + x3) + x4) * ((x ^2) * x))) + (((((x1 * x3) + (x2 * x3)) + (x1 * x2)) + (((x2 * x4) + (x1 * x4)) + (x3 * x4))) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + (- (- ((x1 * x3) * x4)))) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) ;
then  (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * ((x ^2) * x))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) by Th4;
hence  (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) by Th4; ::_thesis: verum
end;

theorem :: POLYEQ_2:12
for a1, a2, a3, a4, a5, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) holds
( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 )
proof
set b1 = 1;
let a1, a2, a3, a4, a5, x1, x2, x3, x4 be real number ; ::_thesis: ( a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) implies ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) )
assume A1: a1 <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) or ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) )
set b5 = ((x1 * x2) * x3) * x4;
set b4 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4));
set b3 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4);
set b2 = - (((x1 + x2) + x3) + x4);
assume A2: for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ; ::_thesis: ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 )
now__::_thesis:_for_x_being_real_number_holds_Polynom_(1,(a2_/_a1),(a3_/_a1),(a4_/_a1),(a5_/_a1),x)_=_Polynom_(1,(-_(((x1_+_x2)_+_x3)_+_x4)),(((((x1_*_x2)_+_(x1_*_x3))_+_(x1_*_x4))_+_((x2_*_x3)_+_(x2_*_x4)))_+_(x3_*_x4)),(-_(((((x1_*_x2)_*_x3)_+_((x1_*_x2)_*_x4))_+_((x1_*_x3)_*_x4))_+_((x2_*_x3)_*_x4))),(((x1_*_x2)_*_x3)_*_x4),x)
let x be real number ; ::_thesis: Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x) = Polynom (1,(- (((x1 + x2) + x3) + x4)),(((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)),(- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))),(((x1 * x2) * x3) * x4),x)
set t = ((((1 * (x |^ 4)) + ((- (((x1 + x2) + x3) + x4)) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) + ((- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))) * x)) + (((x1 * x2) * x3) * x4);
 (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) by A1, A2, Th11;
then ((((1 * (x |^ 4)) + ((- (((x1 + x2) + x3) + x4)) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) + ((- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))) * x)) + (((x1 * x2) * x3) * x4) = (a1 ") * ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + ((a3 * (x ^2)) + (a4 * x))) + a5) by XCMPLX_0:def_9
.= ((((a1 ") * a1) * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5))
.= (((a1 / a1) * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5)) by XCMPLX_0:def_9
.= ((1 * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5)) by A1, XCMPLX_1:60
.= ((x |^ 4) + (((a1 ") * a2) * (x |^ 3))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5))
.= ((x |^ 4) + ((a2 / a1) * (x |^ 3))) + (((((a1 ") * a3) * (x ^2)) + ((a1 ") * (a4 * x))) + ((a1 ") * a5)) by XCMPLX_0:def_9
.= ((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + (((a1 ") * a4) * x)) + ((a1 ") * a5)) by XCMPLX_0:def_9
.= ((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + ((a4 / a1) * x)) + ((a1 ") * a5)) by XCMPLX_0:def_9
.= ((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + ((a4 / a1) * x)) + (a5 / a1)) by XCMPLX_0:def_9
.= Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x) ;
hence  Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x) = Polynom (1,(- (((x1 + x2) + x3) + x4)),(((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)),(- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))),(((x1 * x2) * x3) * x4),x) ; ::_thesis: verum
end;
hence  ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) by Th9; ::_thesis: verum
end;

theorem :: POLYEQ_2:13
for a, k, y being real number st a <> 0 & ( for x being real number holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ) holds
(((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0
proof
let a, k, y be real number ; ::_thesis: ( a <> 0 & ( for x being real number holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ) implies (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0 )
assume that
A1: a <> 0 and
A2: for x being real number holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ; ::_thesis: (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0
((a * y) |^ 4) + (a |^ 4) = ((k * a) * (a * y)) * (((a * y) ^2) + (a ^2)) by A2
.= (k * ((a ^2) * y)) * (((a ^2) * (y ^2)) + ((a ^2) * 1)) ;
then ((a * y) |^ 4) + (a |^ 4) = k * ((((a ^2) * (a ^2)) * y) * ((y ^2) + 1))
.= k * (((a |^ 4) * y) * ((y ^2) + 1)) by Th4
.= ((a |^ 4) * (k * y)) * ((y ^2) + 1) ;
then  ((a |^ 4) * (y |^ 4)) + ((a |^ 4) * 1) = (a |^ 4) * ((k * y) * ((y ^2) + 1)) by NEWTON:7;
then  ((a |^ 4) ") * ((a |^ 4) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1)))) = 0 ;
then  (((a |^ 4) ") * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0 ;
then A3: ((1 / (a |^ 4)) * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0 by XCMPLX_1:215;
 a |^ 4 <> 0 by A1, PREPOWER:5;
then  1 * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0 by A3, XCMPLX_1:106;
then  (((y |^ 4) - (k * ((y ^2) * y))) - (k * y)) + 1 = 0 ;
hence  (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0 by Th4; ::_thesis: verum
end;