:: by Jan Popio\l ek

::

:: Received July 19, 1991

:: Copyright (c) 1991-2017 Association of Mizar Users

:: deftheorem defines delta QUIN_1:def 1 :

for a, b, c being Complex holds delta (a,b,c) = (b ^2) - ((4 * a) * c);

for a, b, c being Complex holds delta (a,b,c) = (b ^2) - ((4 * a) * c);

registration
end;

registration
end;

theorem Th1: :: QUIN_1:1

for a, b, c, x being Complex st a <> 0 holds

((a * (x ^2)) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a))

((a * (x ^2)) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a))

proof end;

theorem Th6: :: QUIN_1:6

for x, a, b, c being Real st a > 0 & ((a * (x ^2)) + (b * x)) + c >= 0 holds

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0

proof end;

theorem Th7: :: QUIN_1:7

for x, a, b, c being Real st a > 0 & ((a * (x ^2)) + (b * x)) + c > 0 holds

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0

proof end;

theorem Th8: :: QUIN_1:8

for x, a, b, c being Real st a < 0 & ((a * (x ^2)) + (b * x)) + c <= 0 holds

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0

proof end;

theorem Th9: :: QUIN_1:9

for x, a, b, c being Real st a < 0 & ((a * (x ^2)) + (b * x)) + c < 0 holds

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0

proof end;

theorem :: QUIN_1:10

for a, b, c being Real st ( for x being Real holds ((a * (x ^2)) + (b * x)) + c >= 0 ) & a > 0 holds

delta (a,b,c) <= 0

delta (a,b,c) <= 0

proof end;

theorem :: QUIN_1:11

for a, b, c being Real st ( for x being Real holds ((a * (x ^2)) + (b * x)) + c <= 0 ) & a < 0 holds

delta (a,b,c) <= 0

delta (a,b,c) <= 0

proof end;

theorem :: QUIN_1:12

for a, b, c being Real st ( for x being Real holds ((a * (x ^2)) + (b * x)) + c > 0 ) & a > 0 holds

delta (a,b,c) < 0

delta (a,b,c) < 0

proof end;

theorem :: QUIN_1:13

for a, b, c being Real st ( for x being Real holds ((a * (x ^2)) + (b * x)) + c < 0 ) & a < 0 holds

delta (a,b,c) < 0

delta (a,b,c) < 0

proof end;

theorem Th14: :: QUIN_1:14

for a, b, c, x being Complex st a <> 0 & ((a * (x ^2)) + (b * x)) + c = 0 holds

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) = 0

((((2 * a) * x) + b) ^2) - (delta (a,b,c)) = 0

proof end;

Lm1: for a, b being Complex holds

( not a ^2 = b ^2 or a = b or a = - b )

proof end;

theorem :: QUIN_1:15

for x, a, b, c being Real st a <> 0 & delta (a,b,c) >= 0 & ((a * (x ^2)) + (b * x)) + c = 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 Th16: :: QUIN_1:16

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

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

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

proof end;

theorem Th17: :: QUIN_1:17

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

((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)

((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)

proof end;

theorem :: QUIN_1:18

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

( ((a * (x ^2)) + (b * x)) + c > 0 iff ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) )

( ((a * (x ^2)) + (b * x)) + c > 0 iff ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) )

proof end;

theorem :: QUIN_1:19

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

( ( x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) iff ((a * (x ^2)) + (b * x)) + c < 0 )

( ( x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) iff ((a * (x ^2)) + (b * x)) + c < 0 )

proof end;

theorem :: QUIN_1:20

for a, b, c, x being Complex st a <> 0 & delta (a,b,c) = 0 & ((a * (x ^2)) + (b * x)) + c = 0 holds

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

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

proof end;

theorem Th21: :: QUIN_1:21

for x, a, b, c being Real st a > 0 & ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 holds

((a * (x ^2)) + (b * x)) + c > 0

((a * (x ^2)) + (b * x)) + c > 0

proof end;

theorem :: QUIN_1:22

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

( ((a * (x ^2)) + (b * x)) + c > 0 iff x <> - (b / (2 * a)) )

( ((a * (x ^2)) + (b * x)) + c > 0 iff x <> - (b / (2 * a)) )

proof end;

theorem Th23: :: QUIN_1:23

for x, a, b, c being Real st a < 0 & ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 holds

((a * (x ^2)) + (b * x)) + c < 0

((a * (x ^2)) + (b * x)) + c < 0

proof end;

theorem :: QUIN_1:24

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

( ((a * (x ^2)) + (b * x)) + c < 0 iff x <> - (b / (2 * a)) )

( ((a * (x ^2)) + (b * x)) + c < 0 iff x <> - (b / (2 * a)) )

proof end;

theorem Th25: :: QUIN_1:25

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

((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)

((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a)

proof end;

theorem :: QUIN_1:26

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

( ((a * (x ^2)) + (b * x)) + c < 0 iff ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) )

( ((a * (x ^2)) + (b * x)) + c < 0 iff ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) )

proof end;

theorem :: QUIN_1:27

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

( ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) iff ((a * (x ^2)) + (b * x)) + c > 0 )

( ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) iff ((a * (x ^2)) + (b * x)) + c > 0 )

proof end;