:: Quadratic Inequalities :: by Jan Popio\l ek :: :: Received July 19, 1991 :: Copyright (c) 1991-2018 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, BOOLE; equalities SQUARE_1; theorems SQUARE_1, XCMPLX_1, XREAL_1, XXREAL_0; begin reserve x, a, b, c for Real; definition let a,b,c be Complex; func delta(a,b,c) -> number equals b^2 - 4 * a * c; coherence; end; registration let a,b,c be Complex; cluster delta(a,b,c) -> complex; coherence; end; registration let a,b,c be Real; cluster delta(a,b,c) -> real; coherence; end; theorem Th1: 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) proof let a, b, c, x be Complex; 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 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; 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 holds a^2 = b^2 implies a = b or a = - b proof let a, b be Complex; 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 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; 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;