:: Quadratic Inequalities
::  by Jan Popio\l ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XREAL_0, ORDINAL1, XCMPLX_0, FUNCT_3, SQUARE_1, ARYTM_1,
      RELAT_1, REAL_1, CARD_1, ARYTM_3, XXREAL_0;
 notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, XXREAL_0;
 constructors SQUARE_1, MEMBERED;
 registrations XCMPLX_0, XREAL_0, SQUARE_1, MEMBERED;
 requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
 definitions SQUARE_1;
 theorems XREAL_0, SQUARE_1, XCMPLX_1, XREAL_1, XXREAL_0;

begin

reserve x, a, b, c for real number;

definition
  let a,b,c be complex number;
  func delta(a,b,c) equals
  b^2 - 4 * a * c;
  coherence;
end;

registration
  let a,b,c be complex number;
  cluster delta(a,b,c) -> complex;
  coherence;
end;

registration
  let a,b,c;
  cluster delta(a,b,c) -> real;
  coherence;
end;

definition
  let a,b,c be Real;
  redefine func delta(a,b,c) -> Real;
  coherence by XREAL_0:def 1;
end;

theorem Th1:
  for a, b, c, x being complex number holds a <> 0 implies a * x^2
  + b * x + c = a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a)
proof
  let a, b, c, x be complex number;
  assume
A1: a <> 0;
  then
A2: 4 * a <> 0;
  a * x^2 + b * x + c = a * x^2 + (b * x) * 1 + c
    .= a * x^2 + (b * x) * (a * (1/a)) + c by A1,XCMPLX_1:106
    .= a * (x^2 + ((b * x) * (1/a))) + c
    .= a * (x^2 + ((b * x)/a)) + c by XCMPLX_1:99
    .= a * (x^2 + x * (b/a)) + c by XCMPLX_1:74
    .= a * (x^2 + x * ((2 * b)/(2 * a))) + c by XCMPLX_1:91
    .= a * (x^2 + x * (2 * (b/(2 * a)))) + c by XCMPLX_1:74
    .= (a * (x^2 + 2 * x * (b/(2 * a))) + b^2/(4 * a)) + (c - b^2/(4 * a))
    .= (a * (x^2 + 2 * x * (b/(2 * a))) + a * (b^2/(4 * a) * (1/a))) + (c -
  b^2/(4 * a)) by A1,XCMPLX_1:109
    .= (a * (x^2 + 2 * x * (b/(2 * a))) + a * ((b^2 * 1)/((4 * a) * a))) + (
  c - b^2/(4 * a)) by XCMPLX_1:76
    .= (a * (x^2 + 2 * x * (b/(2 * a))) + a * (b^2/(2 * a)^2)) + (c - b^2/(4
  * a))
    .= (a * (x^2 + 2 * x * (b/(2 * a))) + a * (b/(2 * a))^2) + (c - b^2/(4 *
  a)) by XCMPLX_1:76
    .= a * (x + b/(2 * a))^2 - (b^2/(4 * a) - c)
    .= a * (x + b/(2 * a))^2 - (b^2/(4 * a) - ((4 * a * c)/(4 * a))) by A2,
XCMPLX_1:89
    .= a * (x + b/(2 * a))^2 - (b^2 - (4 * a * c))/(4 * a) by XCMPLX_1:120;
  hence thesis;
end;

theorem
  a > 0 & delta(a,b,c) <= 0 implies a * x^2 + b * x + c >= 0
proof
  assume that
A1: a > 0 and
A2: delta(a,b,c) <= 0;
  - delta(a,b,c) >= -0 & 4 * a > 0 by A1,A2,XREAL_1:25,129;
  then (- delta(a,b,c))/(4 * a) >= 0 by XREAL_1:136;
  then - delta(a,b,c)/(4 * a) >= 0 by XCMPLX_1:187;
  then
A3: a * (x + b/(2 * a))^2 + - delta(a,b,c)/(4 * a) >= a * (x + b/(2 * a) )^2
  + 0 by XREAL_1:7;
  (x +b/(2 * a))^2 >= 0 by XREAL_1:63;
  then a * (x +b/(2 * a))^2 >= 0 by A1,XREAL_1:127;
  then a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) >= 0 by A3,XXREAL_0:2;
  hence thesis by A1,Th1;
end;

theorem
  a > 0 & delta(a,b,c) < 0 implies a * x^2 + b * x + c > 0
proof
  assume that
A1: a > 0 and
A2: delta(a,b,c) < 0;
  - delta(a,b,c) > -0 & 4 * a > 0 by A1,A2,XREAL_1:26,129;
  then (- delta(a,b,c))/(4 * a) > 0 by XREAL_1:139;
  then - delta(a,b,c)/(4 * a) > 0 by XCMPLX_1:187;
  then
A3: a * (x + b/(2 * a))^2 + - delta(a,b,c)/(4 * a) > a * (x + b/(2 * a)) ^2
  by XREAL_1:29;
  (x +b/(2 * a))^2 >= 0 by XREAL_1:63;
  then a * (x +b/(2 * a))^2 >= 0 by A1,XREAL_1:127;
  then a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) > 0 by A3,XXREAL_0:2;
  hence thesis by A1,Th1;
end;

theorem
  a < 0 & delta(a,b,c) <= 0 implies a * x^2 + b * x + c <= 0
proof
  assume that
A1: a < 0 and
A2: delta(a,b,c) <= 0;
  - delta(a,b,c) >= -0 & 4 * a < 0 by A1,A2,XREAL_1:25,132;
  then (- delta(a,b,c))/(4 * a) <= 0 by XREAL_1:137;
  then - delta(a,b,c)/(4 * a) <= 0 by XCMPLX_1:187;
  then
A3: a * (x + b/(2 * a))^2 + - delta(a,b,c)/(4 * a) <= a * (x + b/(2 * a) )^2
  + 0 by XREAL_1:7;
  a * (x +b/(2 * a))^2 <= 0 by A1,XREAL_1:63,131;
  then a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) <= 0 by A3,XXREAL_0:2;
  hence thesis by A1,Th1;
end;

theorem
  a < 0 & delta(a,b,c) < 0 implies a * x^2 + b * x + c < 0
proof
  assume that
A1: a < 0 and
A2: delta(a,b,c) < 0;
  - delta(a,b,c) > 0 & 4 * a < 0 by A1,A2,XREAL_1:58,132;
  then (- delta(a,b,c))/(4 * a) < 0 by XREAL_1:142;
  then - delta(a,b,c)/(4 * a) < 0 by XCMPLX_1:187;
  then
A3: a * (x + b/(2 * a))^2 + - delta(a,b,c)/(4 * a) < a * (x + b/(2 * a)) ^2
  + 0 by XREAL_1:6;
  a * (x +b/(2 * a))^2 <= 0 by A1,XREAL_1:63,131;
  then a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) < 0 by A3,XXREAL_0:2;
  hence thesis by A1,Th1;
end;

theorem Th6:
  a > 0 & a * x^2 + b * x + c >= 0 implies (2 * a * x + b)^2 -
  delta(a,b,c) >= 0
proof
  assume that
A1: a > 0 and
A2: a * x^2 + b * x + c >= 0;
A3: 4 * a <> 0 by A1;
  4 * a > 0 & a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) >= 0 by A1,A2,Th1,
XREAL_1:129;
  then (4 * a) * (a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a)) >= 0 by
XREAL_1:127;
  then
A4: ((2 * a) * x + (2 * a) * (b/(2 * a)))^2 - (4 * a) * (delta(a,b,c)/(4 * a
  )) >= 0;
  2 * a <> 0 by A1;
  then (2 * a * x + b)^2 - (4 * a) * (delta(a,b,c)/(4 * a)) >= 0 by A4,
XCMPLX_1:87;
  hence thesis by A3,XCMPLX_1:87;
end;

theorem Th7:
  a > 0 & a * x^2 + b * x + c > 0 implies (2 * a * x + b)^2 - delta (a,b,c) > 0
proof
  assume that
A1: a > 0 and
A2: a * x^2 + b * x + c > 0;
A3: 4 * a <> 0 by A1;
  4 * a > 0 & a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) > 0 by A1,A2,Th1,
XREAL_1:129;
  then (4 * a) * (a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a)) > 0 by
XREAL_1:129;
  then
A4: ((2 * a) * x + (2 * a) * (b/(2 * a)))^2 - (4 * a) * (delta(a,b,c)/(4 * a
  )) > 0;
  2 * a <> 0 by A1;
  then (2 * a * x + b)^2 - (4 * a) * (delta(a,b,c)/(4 * a)) > 0 by A4,
XCMPLX_1:87;
  hence thesis by A3,XCMPLX_1:87;
end;

theorem Th8:
  a < 0 & a * x^2 + b * x + c <= 0 implies (2 * a * x + b)^2 -
  delta(a,b,c) >= 0
proof
  assume that
A1: a < 0 and
A2: a * x^2 + b * x + c <= 0;
A3: 4 * a <> 0 by A1;
  4 * a < 0 & a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) <= 0 by A1,A2,Th1,
XREAL_1:132;
  then (4 * a) * (a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a)) >= 0 by
XREAL_1:128;
  then
A4: ((2 * a) * x + (2 * a) * (b/(2 * a)))^2 - (4 * a) * (delta(a,b,c)/(4 * a
  )) >= 0;
  2 * a <> 0 by A1;
  then (2 * a * x + b)^2 - (4 * a) * (delta(a,b,c)/(4 * a)) >= 0 by A4,
XCMPLX_1:87;
  hence thesis by A3,XCMPLX_1:87;
end;

theorem Th9:
  a < 0 & a * x^2 + b * x + c < 0 implies (2 * a * x + b)^2 - delta (a,b,c) > 0
proof
  assume that
A1: a < 0 and
A2: a * x^2 + b * x + c < 0;
A3: 4 * a <> 0 by A1;
  4 * a < 0 & a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) < 0 by A1,A2,Th1,
XREAL_1:132;
  then (4 * a) * (a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a)) > 0 by
XREAL_1:130;
  then
A4: ((2 * a) * x + (2 * a) * (b/(2 * a)))^2 - (4 * a) * (delta(a,b,c)/(4 * a
  )) > 0;
  2 * a <> 0 by A1;
  then (2 * a * x + b)^2 - (4 * a) * (delta(a,b,c)/(4 * a)) > 0 by A4,
XCMPLX_1:87;
  hence thesis by A3,XCMPLX_1:87;
end;

theorem
  ( for x holds a * x^2 + b * x + c >= 0 ) & a > 0 implies delta(a,b,c) <= 0
proof
  assume that
A1: for x holds a * x^2 + b * x + c >= 0 and
A2: a > 0;
  a * (- b/(2 * a))^2 + b * (- b/(2 * a)) + c >= 0 by A1;
  then (2 * a * (- b/(2 * a)) + b)^2 - delta(a,b,c) >= 0 by A2,Th6;
  then
A3: (- (2 * a) * (b/(2 * a)) + b)^2 - delta(a,b,c) >= 0;
  2 * a <> 0 by A2;
  then (- b + b)^2 - delta(a,b,c) >= 0 by A3,XCMPLX_1:87;
  then - delta(a,b,c) >= -0;
  hence thesis by XREAL_1:24;
end;

theorem
  ( for x holds a * x^2 + b * x + c <= 0 ) & a < 0 implies delta(a,b,c) <= 0
proof
  assume that
A1: for x holds a * x^2 + b * x + c <= 0 and
A2: a < 0;
  a * (- b/(2 * a))^2 + b * (- b/(2 * a)) + c <= 0 by A1;
  then (2 * a * (- b/(2 * a)) + b)^2 - delta(a,b,c) >= 0 by A2,Th8;
  then
A3: (- (2 * a) * (b/(2 * a)) + b)^2 - delta(a,b,c) >= 0;
  2 * a <> 0 by A2;
  then (- b + b)^2 - delta(a,b,c) >= 0 by A3,XCMPLX_1:87;
  then - delta(a,b,c) >= -0;
  hence thesis by XREAL_1:24;
end;

theorem
  ( for x holds a * x^2 + b * x + c > 0 ) & a > 0 implies delta(a,b,c) < 0
proof
  assume that
A1: for x holds a * x^2 + b * x + c > 0 and
A2: a > 0;
  a * (- b/(2 * a))^2 + b * (- b/(2 * a)) + c > 0 by A1;
  then (2 * a * (- b/(2 * a)) + b)^2 - delta(a,b,c) > 0 by A2,Th7;
  then
A3: (- (2 * a) * (b/(2 * a)) + b)^2 - delta(a,b,c) > 0;
  2 * a <> 0 by A2;
  then (- b + b)^2 - delta(a,b,c) > 0 by A3,XCMPLX_1:87;
  then - delta(a,b,c) > 0;
  hence thesis by XREAL_1:58;
end;

theorem
  ( for x holds a * x^2 + b * x + c < 0 ) & a < 0 implies delta(a,b,c) < 0
proof
  assume that
A1: for x holds a * x^2 + b * x + c < 0 and
A2: a < 0;
  a * (- b/(2 * a))^2 + b * (- b/(2 * a)) + c < 0 by A1;
  then (2 * a * (- b/(2 * a)) + b)^2 - delta(a,b,c) > 0 by A2,Th9;
  then
A3: (- (2 * a) * (b/(2 * a)) + b)^2 - delta(a,b,c) > 0;
  2 * a <> 0 by A2;
  then (- b + b)^2 - delta(a,b,c) > 0 by A3,XCMPLX_1:87;
  then - delta(a,b,c) > -0;
  hence thesis by XREAL_1:24;
end;

theorem Th14:
  for a, b, c, x being complex number holds a <> 0 & a * x^2 + b *
  x + c = 0 implies (2 * a * x + b)^2 - delta(a,b,c) = 0
proof
  let a, b, c, x be complex number;
  assume that
A1: a <> 0 and
A2: a * x^2 + b * x + c = 0;
A3: 4 * a <> 0 by A1;
  a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) = 0 by A1,A2,Th1;
  then
A4: ((2 * a) * x + (2 * a) * (b/(2 * a)))^2 - (4 * a) * (delta(a,b,c)/(4 * a
  )) = 0;
  2 * a <> 0 by A1;
  then (2 * a * x + b)^2 - (4 * a) * (delta(a,b,c)/(4 * a)) = 0 by A4,
XCMPLX_1:87;
  hence thesis by A3,XCMPLX_1:87;
end;

Lm1: for a, b being complex number holds a^2 = b^2 implies a = b or a = - b
proof
  let a, b be complex number;
  assume a^2 = b^2;
  then (a + b) * (a - b) = 0;
  then a + b = 0 or a - b = 0 by XCMPLX_1:6;
  hence thesis;
end;

theorem
  a <> 0 & delta(a,b,c) >= 0 & a * x^2 + b * x + c = 0 implies x = (- b
  - sqrt delta(a,b,c))/(2 * a) or x = (- b + sqrt delta(a,b,c))/(2 * a)
proof
  assume that
A1: a <> 0 and
A2: delta(a,b,c) >= 0 and
A3: a * x^2 + b * x + c = 0;
  (2 * a * x + b)^2 - delta(a,b,c) = 0 by A1,A3,Th14;
  then (2 * a * x + b)^2 = (sqrt delta(a,b,c))^2 by A2,SQUARE_1:def 2;
  then
A4: 2 * a * x + b = sqrt delta(a,b,c) or 2 * a * x + b = - sqrt delta(a, b,c
  ) by Lm1;
  2 * a <> 0 by A1;
  hence thesis by A4,XCMPLX_1:89;
end;

theorem Th16:
  a <> 0 & delta(a,b,c) >= 0 implies 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
  assume that
A1: a <> 0 and
A2: delta(a,b,c) >= 0;
  a * x^2 + b * x + c = a * (x + b/(2 * a))^2 - 1 * (delta(a,b,c)/(4 * a))
  by A1,Th1
    .= a * (x + b/(2 * a))^2 - (a * (1/a)) * (delta(a,b,c)/(4 * a)) by A1,
XCMPLX_1:106
    .= a * ((x + b/(2 * a))^2 - (1/a) * (delta(a,b,c)/(4 * a)))
    .= a * ((x + b/(2 * a))^2 - (delta(a,b,c) * 1)/((4 * a) * a)) by
XCMPLX_1:76
    .= a * ((x + b/(2 * a))^2 - (sqrt delta(a,b,c))^2/(2 * a)^2) by A2,
SQUARE_1:def 2
    .= a * ((x + b/(2 * a))^2 - (sqrt delta(a,b,c)/(2 * a))^2) by XCMPLX_1:76
    .= a * (x - (- b/(2 * a) + sqrt delta(a,b,c)/(2 * a))) * (x - (- b/(2 *
  a) - sqrt delta(a,b,c)/(2 * a)))
    .= a * (x - ((- b)/(2 * a) + sqrt delta(a,b,c)/(2 * a))) * (x - (- b/(2
  * a) - sqrt delta(a,b,c)/(2 * a))) by XCMPLX_1:187
    .= a * (x - ((- b)/(2 * a) + sqrt delta(a,b,c)/(2 * a))) * (x - ((- b)/(
  2 * a) - sqrt delta(a,b,c)/(2 * a))) by XCMPLX_1:187
    .= a * (x - (- b + sqrt delta(a,b,c))/(2 * a)) * (x - ((- b)/(2 * a) -
  sqrt delta(a,b,c)/(2 * a))) by XCMPLX_1:62
    .= a * (x - (- b + sqrt delta(a,b,c))/(2 * a)) * (x - (- b - sqrt delta(
  a,b,c))/(2 * a)) by XCMPLX_1:120;
  hence thesis;
end;

theorem Th17:
  a < 0 & delta(a,b,c) > 0 implies (- b + sqrt delta(a,b,c))/(2 *
  a) < (- b - sqrt delta(a,b,c))/(2 * a)
proof
  assume that
A1: a < 0 and
A2: delta(a,b,c) > 0;
  sqrt delta(a,b,c) > 0 by A2,SQUARE_1:25;
  then 2 * sqrt delta(a,b,c) > 0 by XREAL_1:129;
  then sqrt delta(a,b,c) + sqrt delta(a,b,c) > 0;
  then sqrt delta(a,b,c) > - sqrt delta(a,b,c) by XREAL_1:59;
  then
A3: - b + sqrt delta(a,b,c) > - b + - sqrt delta(a,b,c) by XREAL_1:6;
  2 * a < 0 by A1,XREAL_1:132;
  hence thesis by A3,XREAL_1:75;
end;

theorem
  a < 0 & delta(a,b,c) > 0 implies ( 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
  assume that
A1: a < 0 and
A2: delta(a,b,c) > 0;
  thus a * x^2 + b * x + c > 0 implies (- b + sqrt delta(a,b,c))/(2 * a) < x &
  x < (- b - sqrt delta(a,b,c))/(2 * a)
  proof
    assume a * x^2 + b * x + c > 0;
    then
    a * (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a
    ,b,c))/(2 * a)) > 0 by A1,A2,Th16;
    then
    a * ((x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(
    a,b,c))/(2 * a))) > 0;
    then
    (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,b,c
    ))/(2 * a)) < 0/a by A1,XREAL_1:84;
    then
    x - (- b - sqrt delta(a,b,c))/(2 * a) > 0 & x - (- b + sqrt delta(a,b,
c))/(2 * a) < 0 or x - (- b - sqrt delta(a,b,c))/(2 * a) < 0 & x - (- b + sqrt
    delta(a,b,c))/(2 * a) > 0 by XREAL_1:133;
    then
    x > (- b - sqrt delta(a,b,c))/(2 * a) & x < (- b + sqrt delta(a,b,c))/
(2 * a) & (- b + sqrt delta(a,b,c))/(2 * a) < (- b - sqrt delta(a,b,c))/(2 * a)
or x < (- b - sqrt delta(a,b,c))/(2 * a) & x > (- b + sqrt delta(a,b,c))/(2 * a
    ) by A1,A2,Th17,XREAL_1:47,48;
    hence thesis by XXREAL_0:2;
  end;
  assume (- b + sqrt delta(a,b,c))/(2 * a) < x & x < (- b - sqrt delta(a,b,c
  ))/(2 * a );
  then
  x - (- b + sqrt delta(a,b,c))/(2 * a) > 0 & x - (- b - sqrt delta(a,b,c
  ))/(2 * a) < 0 by XREAL_1:49,50;
  then
  (x - (- b + sqrt delta(a,b,c))/(2 * a)) * (x - (- b - sqrt delta(a,b,c)
  )/(2 * a)) < 0 by XREAL_1:132;
  then
  a * ((x - (- b + sqrt delta(a,b,c))/(2 * a)) * (x - (- b - sqrt delta(a
  ,b,c))/(2 * a))) > 0 by A1,XREAL_1:130;
  then
  a * (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,
  b,c))/(2 * a)) > 0;
  hence thesis by A1,A2,Th16;
end;

theorem
  a < 0 & delta(a,b,c) > 0 implies ( a * x^2 + b * x + c < 0 iff x < (-
  b + sqrt delta(a,b,c))/(2 * a) or x > (- b - sqrt delta(a,b,c))/(2 * a) )
proof
  assume that
A1: a < 0 and
A2: delta(a,b,c) > 0;
  thus a * x^2 + b * x + c < 0 implies x < (- b + sqrt delta(a,b,c))/(2 * a)
  or x > (- b - sqrt delta(a,b,c))/(2 * a)
  proof
    assume a * x^2 + b * x + c < 0;
    then
    a * (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a
    ,b,c))/(2 * a)) < 0 by A1,A2,Th16;
    then
    a * ((x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(
    a,b,c))/(2 * a))) < 0;
    then
    (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,b,c
    ))/(2 * a)) > 0/a by A1,XREAL_1:82;
    then
    x - (- b - sqrt delta(a,b,c))/(2 * a) > 0 & x - (- b + sqrt delta(a,b,
c))/(2 * a) > 0 or x - (- b - sqrt delta(a,b,c))/(2 * a) < 0 & x - (- b + sqrt
    delta(a,b,c))/(2 * a) < 0 by XREAL_1:134;
    hence thesis by XREAL_1:47,48;
  end;
  assume x < (- b + sqrt delta(a,b,c))/(2 * a) or x > (- b - sqrt delta(a,b,
  c))/(2 * a);
  then
A3: x - (- b + sqrt delta(a,b,c))/(2 * a) < 0 or x - (- b - sqrt delta(a,b,
  c))/(2 * a) > 0 by XREAL_1:49,50;
  (- b + sqrt delta(a,b,c))/(2 * a) < (- b - sqrt delta(a,b,c))/(2 * a)
  by A1,A2,Th17;
  then
  x - (- b + sqrt delta(a,b,c))/(2 * a) > x - (- b - sqrt delta(a,b,c))/(
  2 * a) by XREAL_1:10;
  then
  x - (- b + sqrt delta(a,b,c))/(2 * a) < 0 & x - (- b - sqrt delta(a,b,c
  ))/(2 * a) < 0 or x - (- b - sqrt delta(a,b,c))/(2 * a) > 0 & x - (- b + sqrt
  delta(a,b,c))/(2 * a) > 0 by A3,XXREAL_0:2;
  then
  (x - (- b + sqrt delta(a,b,c))/(2 * a)) * (x - (- b - sqrt delta(a,b,c)
  )/(2 * a)) > 0 by XREAL_1:129,130;
  then
  a * ((x - (- b + sqrt delta(a,b,c))/(2 * a)) * (x - (- b - sqrt delta(a
  ,b,c))/(2 * a))) < 0 by A1,XREAL_1:132;
  then
  a * (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,
  b,c))/(2 * a)) < 0;
  hence thesis by A1,A2,Th16;
end;

theorem
  for a, b, c, x being complex number holds a <> 0 & delta(a,b,c) = 0 &
  a * x^2 + b * x + c = 0 implies x = - b/(2 * a)
proof
  let a, b, c, x be complex number;
  assume that
A1: a <> 0 and
A2: delta(a,b,c) = 0 & a * x^2 + b * x + c = 0;
  (2 * a * x + b)^2 - 0 = 0 by A1,A2,Th14;
  then
A3: 2 * a * x + b = 0 by XCMPLX_1:6;
  2 * a <> 0 by A1;
  then x = (- b)/(2 * a) by A3,XCMPLX_1:89;
  hence thesis by XCMPLX_1:187;
end;

theorem Th21:
  a > 0 & (2 * a * x + b)^2 - delta(a,b,c) > 0 implies a * x^2 + b * x + c > 0
proof
  assume that
A1: a > 0 and
A2: (2 * a * x + b)^2 - delta(a,b,c) > 0;
  4 * a <> 0 by A1;
  then
A3: (2 * a * x + b)^2 - (4 * a) * (delta(a,b,c)/(4 * a)) > 0 by A2,XCMPLX_1:87;
  2 * a <> 0 by A1;
  then
  (2 * a * x + (2 * a) * (b/(2 * a)))^2 - (4 * a) * (delta(a,b,c)/(4 * a))
  > 0 by A3,XCMPLX_1:87;
  then
A4: (4 * a) * (a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a)) > 0;
  4 * a > 0 by A1,XREAL_1:129;
  then a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) > 0/(4 * a) by A4,
XREAL_1:83;
  hence thesis by A1,Th1;
end;

theorem
  a > 0 & delta(a,b,c) = 0 implies ( a * x^2 + b * x + c > 0 iff x <> -
  b/(2 * a) )
proof
  assume that
A1: a > 0 and
A2: delta(a,b,c) = 0;
A3: 2 * a <> 0 by A1;
  thus a * x^2 + b * x + c > 0 implies x <> - b/(2 * a)
  proof
    assume a * x^2 + b * x + c > 0;
    then (2 * a * x + b)^2 - 0 > 0 by A1,A2,Th7;
    then 2 * a * x <> - b;
    then x <> (- b)/(2 * a) by A3,XCMPLX_1:87;
    hence thesis by XCMPLX_1:187;
  end;
  assume x <> - b/(2 * a);
  then x <> (- b)/(2 * a) by XCMPLX_1:187;
  then 2 * a * x + b <> 0 by A3,XCMPLX_1:89;
  then (2 * a * x + b)^2 - delta(a,b,c) > 0 by A2,SQUARE_1:12;
  hence thesis by A1,Th21;
end;

theorem Th23:
  a < 0 & (2 * a * x + b)^2 - delta(a,b,c) > 0 implies a * x^2 + b * x + c < 0
proof
  assume that
A1: a < 0 and
A2: (2 * a * x + b)^2 - delta(a,b,c) > 0;
  4 * a <> 0 by A1;
  then
A3: (2 * a * x + b)^2 - (4 * a) * (delta(a,b,c)/(4 * a)) > 0 by A2,XCMPLX_1:87;
  2 * a <> 0 by A1;
  then
  (2 * a * x + (2 * a) * (b/(2 * a)))^2 - (4 * a) * (delta(a,b,c)/(4 * a))
  > 0 by A3,XCMPLX_1:87;
  then
A4: (4 * a) * (a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a)) > 0;
  4 * a < 0 by A1,XREAL_1:132;
  then a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a) < 0/(4 * a) by A4,
XREAL_1:84;
  hence thesis by A1,Th1;
end;

theorem
  a < 0 & delta(a,b,c) = 0 implies ( a * x^2 + b * x + c < 0 iff x <> -
  b/(2 * a) )
proof
  assume that
A1: a < 0 and
A2: delta(a,b,c) = 0;
A3: 2 * a <> 0 by A1;
  thus a * x^2 + b * x + c < 0 implies x <> - b/(2 * a)
  proof
    assume a * x^2 + b * x + c < 0;
    then (2 * a * x + b)^2 - 0 > 0 by A1,A2,Th9;
    then 2 * a * x <> - b;
    then x <> (- b)/(2 * a) by A3,XCMPLX_1:87;
    hence thesis by XCMPLX_1:187;
  end;
  assume x <> - b/(2 * a);
  then x <> (- b)/(2 * a) by XCMPLX_1:187;
  then 2 * a * x + b <> 0 by A3,XCMPLX_1:89;
  then (2 * a * x + b)^2 - delta(a,b,c) > 0 by A2,SQUARE_1:12;
  hence thesis by A1,Th23;
end;

theorem Th25:
  a > 0 & delta(a,b,c) > 0 implies (- b + sqrt delta(a,b,c))/(2 *
  a) > (- b - sqrt delta(a,b,c))/(2 * a)
proof
  assume that
A1: a > 0 and
A2: delta(a,b,c) > 0;
  sqrt delta(a,b,c) > 0 by A2,SQUARE_1:25;
  then 2 * sqrt delta(a,b,c) > 0 by XREAL_1:129;
  then sqrt delta(a,b,c) + sqrt delta(a,b,c) > 0;
  then sqrt delta(a,b,c) > - sqrt delta(a,b,c) by XREAL_1:59;
  then
A3: - b + sqrt delta(a,b,c) > - b + - sqrt delta(a,b,c) by XREAL_1:6;
  2 * a > 0 by A1,XREAL_1:129;
  hence thesis by A3,XREAL_1:74;
end;

theorem
  a > 0 & delta(a,b,c) > 0 implies ( 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
  assume that
A1: a > 0 and
A2: delta(a,b,c) > 0;
  thus a * x^2 + b * x + c < 0 implies (- b - sqrt delta(a,b,c))/(2 * a) < x &
  x < (- b + sqrt delta(a,b,c))/(2 * a)
  proof
    assume a * x^2 + b * x + c < 0;
    then
    a * (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a
    ,b,c))/(2 * a)) < 0 by A1,A2,Th16;
    then
    a * ((x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(
    a,b,c))/(2 * a))) < 0;
    then
    (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,b,c
    ))/(2 * a)) < 0/a by A1,XREAL_1:81;
    then
    x - (- b - sqrt delta(a,b,c))/(2 * a) > 0 & x - (- b + sqrt delta(a,b,
c))/(2 * a) < 0 or x - (- b - sqrt delta(a,b,c))/(2 * a) < 0 & x - (- b + sqrt
    delta(a,b,c))/(2 * a) > 0 by XREAL_1:133;
    then
    x > (- b - sqrt delta(a,b,c))/(2 * a) & x < (- b + sqrt delta(a,b,c))/
(2 * a) or (- b + sqrt delta(a,b,c))/(2 * a) > (- b - sqrt delta(a,b,c))/(2 * a
) & x < (- b - sqrt delta(a,b,c))/(2 * a) & x > (- b + sqrt delta(a,b,c))/(2 *
    a) by A1,A2,Th25,XREAL_1:47,48;
    hence thesis by XXREAL_0:2;
  end;
  assume (- b - sqrt delta(a,b,c))/(2 * a) < x & x < (- b + sqrt delta(a,b,c
  ))/(2 * a );
  then
  x - (- b - sqrt delta(a,b,c))/(2 * a) > 0 & x - (- b + sqrt delta(a,b,c
  ))/(2 * a) < 0 by XREAL_1:49,50;
  then
  (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,b,c)
  )/(2 * a)) < 0 by XREAL_1:132;
  then
  a * ((x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a
  ,b,c))/(2 * a))) < 0 by A1,XREAL_1:132;
  then
  a * (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,
  b,c))/(2 * a)) < 0;
  hence thesis by A1,A2,Th16;
end;

theorem
  a > 0 & delta(a,b,c) > 0 implies ( a * x^2 + b * x + c > 0 iff x < (-
  b - sqrt delta(a,b,c))/(2 * a) or x > (- b + sqrt delta(a,b,c))/(2 * a) )
proof
  assume that
A1: a > 0 and
A2: delta(a,b,c) > 0;
  thus a * x^2 + b * x + c > 0 implies x < (- b - sqrt delta(a,b,c))/(2 * a)
  or x > (- b + sqrt delta(a,b,c))/(2 * a)
  proof
    assume a * x^2 + b * x + c > 0;
    then
    a * (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a
    ,b,c))/(2 * a)) > 0 by A1,A2,Th16;
    then
    a * ((x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(
    a,b,c))/(2 * a))) > 0;
    then
    (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,b,c
    ))/(2 * a)) > 0/a by A1,XREAL_1:83;
    then
    x - (- b - sqrt delta(a,b,c))/(2 * a) > 0 & x - (- b + sqrt delta(a,b,
c))/(2 * a) > 0 or x - (- b - sqrt delta(a,b,c))/(2 * a) < 0 & x - (- b + sqrt
    delta(a,b,c))/(2 * a) < 0 by XREAL_1:134;
    hence thesis by XREAL_1:47,48;
  end;
  assume x < (- b - sqrt delta(a,b,c))/(2 * a) or x > (- b + sqrt delta(a,b,
  c))/(2 * a);
  then
A3: x - (- b - sqrt delta(a,b,c))/(2 * a) < 0 or x - (- b + sqrt delta(a,b,
  c))/(2 * a) > 0 by XREAL_1:49,50;
  (- b + sqrt delta(a,b,c))/(2 * a) > (- b - sqrt delta(a,b,c))/(2 * a)
  by A1,A2,Th25;
  then
  x - (- b + sqrt delta(a,b,c))/(2 * a) < x - (- b - sqrt delta(a,b,c))/(
  2 * a) by XREAL_1:10;
  then
  x - (- b - sqrt delta(a,b,c))/(2 * a) < 0 & x - (- b + sqrt delta(a,b,c
  ))/(2 * a) < 0 or x - (- b - sqrt delta(a,b,c))/(2 * a) > 0 & x - (- b + sqrt
  delta(a,b,c))/(2 * a) > 0 by A3,XXREAL_0:2;
  then
  (x - (- b + sqrt delta(a,b,c))/(2 * a)) * (x - (- b - sqrt delta(a,b,c)
  )/(2 * a)) > 0 by XREAL_1:129,130;
  then
  a * ((x - (- b + sqrt delta(a,b,c))/(2 * a)) * (x - (- b - sqrt delta(a
  ,b,c))/(2 * a))) > 0 by A1,XREAL_1:129;
  then
  a * (x - (- b - sqrt delta(a,b,c))/(2 * a)) * (x - (- b + sqrt delta(a,
  b,c))/(2 * a)) > 0;
  hence thesis by A1,A2,Th16;
end;