:: by Liang Xiquan

::

:: Received May 18, 2000

:: Copyright (c) 2000-2019 Association of Mizar Users

:: deftheorem defines Polynom POLYEQ_1:def 1 :

for a, b, x being Complex holds Polynom (a,b,x) = (a * x) + b;

for a, b, x being Complex holds Polynom (a,b,x) = (a * x) + b;

registration
end;

registration
end;

theorem :: POLYEQ_1:3

:: deftheorem defines Polynom POLYEQ_1:def 2 :

for a, b, c, x being Complex holds Polynom (a,b,c,x) = ((a * (x ^2)) + (b * x)) + c;

for a, b, c, x being Complex holds Polynom (a,b,c,x) = ((a * (x ^2)) + (b * x)) + c;

registration
end;

theorem Th4: :: POLYEQ_1:4

for a, b, c, a9, b9, c9 being Complex st ( for x being Real holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) holds

( a = a9 & b = b9 & c = c9 )

( a = a9 & b = b9 & c = c9 )

proof end;

theorem Th5: :: POLYEQ_1:5

for a, b, c being Real st a <> 0 & delta (a,b,c) >= 0 holds

for x being Real 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) )

for x being Real 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 st a <> 0 & delta (a,b,c) = 0 & Polynom (a,b,c,x) = 0 holds

x = - (b / (2 * a))

x = - (b / (2 * a))

proof end;

theorem :: POLYEQ_1:8

for x being Real

for b, c being Complex st b <> 0 & ( for x being Real holds Polynom (0,b,c,x) = 0 ) holds

x = - (c / b)

for b, c being Complex st b <> 0 & ( for x being Real holds Polynom (0,b,c,x) = 0 ) holds

x = - (c / b)

proof end;

theorem :: POLYEQ_1:10

:: deftheorem defines Quard POLYEQ_1:def 3 :

for a, x, x1, x2 being Complex holds Quard (a,x1,x2,x) = a * ((x - x1) * (x - x2));

for a, x, x1, x2 being Complex holds Quard (a,x1,x2,x) = a * ((x - x1) * (x - x2));

registration
end;

theorem :: POLYEQ_1:11

for x1, x2 being Real

for a, b, c being Complex st a <> 0 & ( for x being Real holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) holds

( b / a = - (x1 + x2) & c / a = x1 * x2 )

for a, b, c being Complex st a <> 0 & ( for x being Real holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) holds

( b / a = - (x1 + x2) & c / a = x1 * x2 )

proof end;

definition

let a, b, c, d, x be Complex;

(((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d is number ;

end;
func Polynom (a,b,c,d,x) -> number equals :: POLYEQ_1:def 4

(((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d;

coherence (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d;

(((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d is number ;

:: deftheorem defines Polynom POLYEQ_1:def 4 :

for a, b, c, d, x being Complex holds Polynom (a,b,c,d,x) = (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d;

for a, b, c, d, x being Complex holds Polynom (a,b,c,d,x) = (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d;

3 = (2 * 1) + 1

;

then Lm1: 3 is odd

by ABIAN:1;

theorem Th12: :: POLYEQ_1:12

for a, a9, b, b9, c, c9, d, d9 being Real st ( for x being Real holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ) holds

( a = a9 & b = b9 & c = c9 & d = d9 )

( a = a9 & b = b9 & c = c9 & d = d9 )

proof end;

definition
end;

:: deftheorem defines Tri POLYEQ_1:def 5 :

for a, x, x1, x2, x3 being Complex holds Tri (a,x1,x2,x3,x) = a * (((x - x1) * (x - x2)) * (x - x3));

for a, x, x1, x2, x3 being Complex holds Tri (a,x1,x2,x3,x) = a * (((x - x1) * (x - x2)) * (x - x3));

theorem :: POLYEQ_1:13

for a, b, c, d, x1, x2, x3 being Real st a <> 0 & ( for x being Real 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) )

( 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 h, y being Real 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 st a <> 0 & Polynom (a,b,c,d,x) = 0 holds

for a1, a2, a3, h, y being Real 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

for a1, a2, a3, h, y being Real 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 st a <> 0 & Polynom (a,b,c,d,x) = 0 holds

for a1, a2, a3, h, y being Real 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

for a1, a2, a3, h, y being Real 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 a, b, c, d, y being Real 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 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 ;

for p, q being Real 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 st Polynom (1,0,p,q,y) = 0 holds

for u, v being Real st y = u + v & ((3 * v) * u) + p = 0 holds

( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 )

for u, v being Real 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 st Polynom (1,0,p,q,y) = 0 holds

for u, v being Real 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)))))

for u, v being Real 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 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)

x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b)

proof end;

theorem :: POLYEQ_1:21

for a, c, d, p, q, x being Real st a <> 0 & p = c / a & q = d / a & Polynom (a,0,c,d,x) = 0 holds

for u, v being Real 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)))))

for u, v being Real 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 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)

x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)

proof end;

theorem :: POLYEQ_1:23

for a, c, x being Real 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)))

x = - (sqrt (- (c / a)))

proof end;