:: Solving Roots of Polynomial Equations of Degree 2 and 3 with Real Coefficients
:: by Liang Xiquan
::
:: Received May 18, 2000
:: Copyright (c) 2000-2012 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, 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 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;

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