:: Quadratic Inequalities
:: by Jan Popio\l ek
::
:: Received July 19, 1991
:: Copyright (c) 1991-2026 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;
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;