:: Solving Roots of Polynomial Equations of Degree 2 and 3 withReal Coefficients
:: by Liang Xiquan
::
:: Received May 18, 2000
:: Copyright (c) 2000 Association of Mizar Users

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 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, a', b', c' being complex number st ( for x being real number holds Polynom a,b,c,x = Polynom a',b',c',x ) holds
( a = a' & b = b' & c = c' )

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

theorem Th12: :: POLYEQ_1:12

for a, b, c, d, a', b', c', d' being real number st ( for x being real number holds Polynom a,b,c,d,x = Polynom a',b',c',d',x ) holds
( a = a' & b = b' & c = c' & d = d' )

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