:: Quadratic Inequalities :: by Jan Popio\l ek :: :: Received July 19, 1991 :: Copyright (c) 1991-2021 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, XCMPLX_0, FUNCT_3, SQUARE_1, ARYTM_1, RELAT_1, REAL_1, CARD_1, ARYTM_3, XXREAL_0, ORDINAL1; notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, SQUARE_1, XXREAL_0; constructors SQUARE_1, MEMBERED, XXREAL_0; registrations XCMPLX_0, XREAL_0, SQUARE_1, MEMBERED; requirements REAL, NUMERALS, SUBSET, ARITHM; begin reserve x, a, b, c for Real; definition let a,b,c be Complex; func delta(a,b,c) -> number equals :: QUIN_1:def 1 b^2 - 4 * a * c; end; registration let a,b,c be Complex; cluster delta(a,b,c) -> complex; end; registration let a,b,c be Real; cluster delta(a,b,c) -> real; end; theorem :: QUIN_1:1 for a, b, c, x being Complex holds a <> 0 implies a * x^2 + b * x + c = a * (x + b/(2 * a))^2 - delta(a,b,c)/(4 * a); theorem :: QUIN_1:2 a > 0 & delta(a,b,c) <= 0 implies a * x^2 + b * x + c >= 0; theorem :: QUIN_1:3 a > 0 & delta(a,b,c) < 0 implies a * x^2 + b * x + c > 0; theorem :: QUIN_1:4 a < 0 & delta(a,b,c) <= 0 implies a * x^2 + b * x + c <= 0; theorem :: QUIN_1:5 a < 0 & delta(a,b,c) < 0 implies a * x^2 + b * x + c < 0; theorem :: QUIN_1:6 a > 0 & a * x^2 + b * x + c >= 0 implies (2 * a * x + b)^2 - delta(a,b,c) >= 0; theorem :: QUIN_1:7 a > 0 & a * x^2 + b * x + c > 0 implies (2 * a * x + b)^2 - delta (a,b,c) > 0 ; theorem :: QUIN_1:8 a < 0 & a * x^2 + b * x + c <= 0 implies (2 * a * x + b)^2 - delta(a,b,c) >= 0; theorem :: QUIN_1:9 a < 0 & a * x^2 + b * x + c < 0 implies (2 * a * x + b)^2 - delta (a,b,c) > 0 ; theorem :: QUIN_1:10 ( for x holds a * x^2 + b * x + c >= 0 ) & a > 0 implies delta(a,b,c) <= 0; theorem :: QUIN_1:11 ( for x holds a * x^2 + b * x + c <= 0 ) & a < 0 implies delta(a,b,c) <= 0; theorem :: QUIN_1:12 ( for x holds a * x^2 + b * x + c > 0 ) & a > 0 implies delta(a,b,c) < 0; theorem :: QUIN_1:13 ( for x holds a * x^2 + b * x + c < 0 ) & a < 0 implies delta(a,b,c) < 0; theorem :: QUIN_1:14 for a, b, c, x being Complex holds a <> 0 & a * x^2 + b * x + c = 0 implies (2 * a * x + b)^2 - delta(a,b,c) = 0; theorem :: QUIN_1:15 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); theorem :: QUIN_1:16 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)); theorem :: QUIN_1:17 a < 0 & delta(a,b,c) > 0 implies (- b + sqrt delta(a,b,c))/(2 * a) < (- b - sqrt delta(a,b,c))/(2 * a); theorem :: QUIN_1:18 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) ); theorem :: QUIN_1:19 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) ); theorem :: QUIN_1:20 for a, b, c, x being Complex holds a <> 0 & delta(a,b,c) = 0 & a * x^2 + b * x + c = 0 implies x = - b/(2 * a); theorem :: QUIN_1:21 a > 0 & (2 * a * x + b)^2 - delta(a,b,c) > 0 implies a * x^2 + b * x + c > 0; theorem :: QUIN_1:22 a > 0 & delta(a,b,c) = 0 implies ( a * x^2 + b * x + c > 0 iff x <> - b/(2 * a) ); theorem :: QUIN_1:23 a < 0 & (2 * a * x + b)^2 - delta(a,b,c) > 0 implies a * x^2 + b * x + c < 0; theorem :: QUIN_1:24 a < 0 & delta(a,b,c) = 0 implies ( a * x^2 + b * x + c < 0 iff x <> - b/(2 * a) ); theorem :: QUIN_1:25 a > 0 & delta(a,b,c) > 0 implies (- b + sqrt delta(a,b,c))/(2 * a) > (- b - sqrt delta(a,b,c))/(2 * a); theorem :: QUIN_1:26 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) ); theorem :: QUIN_1:27 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) );