:: Solving Roots of Polynomial Equation of Degree 4 with Real Coefficients
:: by Xiquan Liang
::
:: Received February 3, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

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;

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 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;

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;

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 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 end;

theorem Th2: :: POLYEQ_2:2

for a, b, c, x, y being Real 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 end;

theorem :: POLYEQ_2:3

for a, b, c, x, y being Real 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 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 end;

theorem Th4: :: POLYEQ_2:4

for x being Real holds
( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 )

proof end;

theorem Th5: :: POLYEQ_2:5

for x, y being Real 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 end;

theorem :: POLYEQ_2:6

for x, y being Real 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 end;

theorem Th7: :: POLYEQ_2:7

for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being Real st ( for x being Real 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 end;

theorem Th8: :: POLYEQ_2:8

for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being Real st ( for x being Real 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 end;

theorem Th9: :: POLYEQ_2:9

for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being Real st ( for x being Real 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 end;

definition

let a1, x1, x2, x3, x4, x be Real;

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 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;

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 st a1 <> 0 & ( for x being Real 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 end;

theorem Th11: :: POLYEQ_2:11

for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being Real st a1 <> 0 & ( for x being Real 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 end;

theorem :: POLYEQ_2:12

for a1, a2, a3, a4, a5, x1, x2, x3, x4 being Real st a1 <> 0 & ( for x being Real 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 end;

theorem :: POLYEQ_2:13

for a, k, y being Real st a <> 0 & ( for x being Real holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ) holds
(((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0

proof end;