:: QUIN_1 semantic presentation begin definition let a, b, c be complex number ; func delta (a,b,c) -> set equals :: QUIN_1:def 1 (b ^2) - ((4 * a) * c); coherence (b ^2) - ((4 * a) * c) is set ; end; :: deftheorem defines delta QUIN_1:def_1_:_ for a, b, c being complex number holds delta (a,b,c) = (b ^2) - ((4 * a) * c); registration let a, b, c be complex number ; cluster delta (a,b,c) -> complex ; coherence delta (a,b,c) is complex ; end; registration let a, b, c be real number ; cluster delta (a,b,c) -> real ; coherence delta (a,b,c) is real ; end; definition let a, b, c be Real; :: original: delta redefine func delta (a,b,c) -> Real; coherence delta (a,b,c) is Real by XREAL_0:def_1; end; theorem Th1: :: QUIN_1:1 for a, b, c, x being complex number st a <> 0 holds ((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 ; ::_thesis: ( a <> 0 implies ((a * (x ^2)) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) ) assume A1: a <> 0 ; ::_thesis: ((a * (x ^2)) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) 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 ((a * (x ^2)) + (b * x)) + c = (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) ; ::_thesis: verum end; theorem :: QUIN_1:2 for a, b, c, x being real number st a > 0 & delta (a,b,c) <= 0 holds ((a * (x ^2)) + (b * x)) + c >= 0 proof let a, b, c, x be real number ; ::_thesis: ( a > 0 & delta (a,b,c) <= 0 implies ((a * (x ^2)) + (b * x)) + c >= 0 ) assume that A1: a > 0 and A2: delta (a,b,c) <= 0 ; ::_thesis: ((a * (x ^2)) + (b * x)) + c >= 0 ( - (delta (a,b,c)) >= - 0 & 4 * a > 0 ) by A1, A2, XREAL_1:25, XREAL_1: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 ((a * (x ^2)) + (b * x)) + c >= 0 by A1, Th1; ::_thesis: verum end; theorem :: QUIN_1:3 for a, b, c, x being real number st a > 0 & delta (a,b,c) < 0 holds ((a * (x ^2)) + (b * x)) + c > 0 proof let a, b, c, x be real number ; ::_thesis: ( a > 0 & delta (a,b,c) < 0 implies ((a * (x ^2)) + (b * x)) + c > 0 ) assume that A1: a > 0 and A2: delta (a,b,c) < 0 ; ::_thesis: ((a * (x ^2)) + (b * x)) + c > 0 ( - (delta (a,b,c)) > - 0 & 4 * a > 0 ) by A1, A2, XREAL_1:26, XREAL_1: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 ((a * (x ^2)) + (b * x)) + c > 0 by A1, Th1; ::_thesis: verum end; theorem :: QUIN_1:4 for a, b, c, x being real number st a < 0 & delta (a,b,c) <= 0 holds ((a * (x ^2)) + (b * x)) + c <= 0 proof let a, b, c, x be real number ; ::_thesis: ( a < 0 & delta (a,b,c) <= 0 implies ((a * (x ^2)) + (b * x)) + c <= 0 ) assume that A1: a < 0 and A2: delta (a,b,c) <= 0 ; ::_thesis: ((a * (x ^2)) + (b * x)) + c <= 0 ( - (delta (a,b,c)) >= - 0 & 4 * a < 0 ) by A1, A2, XREAL_1:25, XREAL_1: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, XREAL_1:131; then (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) <= 0 by A3, XXREAL_0:2; hence ((a * (x ^2)) + (b * x)) + c <= 0 by A1, Th1; ::_thesis: verum end; theorem :: QUIN_1:5 for a, b, c, x being real number st a < 0 & delta (a,b,c) < 0 holds ((a * (x ^2)) + (b * x)) + c < 0 proof let a, b, c, x be real number ; ::_thesis: ( a < 0 & delta (a,b,c) < 0 implies ((a * (x ^2)) + (b * x)) + c < 0 ) assume that A1: a < 0 and A2: delta (a,b,c) < 0 ; ::_thesis: ((a * (x ^2)) + (b * x)) + c < 0 ( - (delta (a,b,c)) > 0 & 4 * a < 0 ) by A1, A2, XREAL_1:58, XREAL_1: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, XREAL_1:131; then (a * ((x + (b / (2 * a))) ^2)) - ((delta (a,b,c)) / (4 * a)) < 0 by A3, XXREAL_0:2; hence ((a * (x ^2)) + (b * x)) + c < 0 by A1, Th1; ::_thesis: verum end; theorem Th6: :: QUIN_1:6 for a, x, b, c being real number st a > 0 & ((a * (x ^2)) + (b * x)) + c >= 0 holds ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0 proof let a, x, b, c be real number ; ::_thesis: ( a > 0 & ((a * (x ^2)) + (b * x)) + c >= 0 implies ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0 ) assume that A1: a > 0 and A2: ((a * (x ^2)) + (b * x)) + c >= 0 ; ::_thesis: ((((2 * a) * x) + b) ^2) - (delta (a,b,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 ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0 by A3, XCMPLX_1:87; ::_thesis: verum end; theorem Th7: :: QUIN_1:7 for a, x, b, c being real number st a > 0 & ((a * (x ^2)) + (b * x)) + c > 0 holds ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 proof let a, x, b, c be real number ; ::_thesis: ( a > 0 & ((a * (x ^2)) + (b * x)) + c > 0 implies ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 ) assume that A1: a > 0 and A2: ((a * (x ^2)) + (b * x)) + c > 0 ; ::_thesis: ((((2 * a) * x) + b) ^2) - (delta (a,b,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 ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 by A3, XCMPLX_1:87; ::_thesis: verum end; theorem Th8: :: QUIN_1:8 for a, x, b, c being real number st a < 0 & ((a * (x ^2)) + (b * x)) + c <= 0 holds ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0 proof let a, x, b, c be real number ; ::_thesis: ( a < 0 & ((a * (x ^2)) + (b * x)) + c <= 0 implies ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0 ) assume that A1: a < 0 and A2: ((a * (x ^2)) + (b * x)) + c <= 0 ; ::_thesis: ((((2 * a) * x) + b) ^2) - (delta (a,b,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 ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) >= 0 by A3, XCMPLX_1:87; ::_thesis: verum end; theorem Th9: :: QUIN_1:9 for a, x, b, c being real number st a < 0 & ((a * (x ^2)) + (b * x)) + c < 0 holds ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 proof let a, x, b, c be real number ; ::_thesis: ( a < 0 & ((a * (x ^2)) + (b * x)) + c < 0 implies ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 ) assume that A1: a < 0 and A2: ((a * (x ^2)) + (b * x)) + c < 0 ; ::_thesis: ((((2 * a) * x) + b) ^2) - (delta (a,b,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 ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 by A3, XCMPLX_1:87; ::_thesis: verum end; theorem :: QUIN_1:10 for a, b, c being real number st ( for x being real number holds ((a * (x ^2)) + (b * x)) + c >= 0 ) & a > 0 holds delta (a,b,c) <= 0 proof let a, b, c be real number ; ::_thesis: ( ( for x being real number holds ((a * (x ^2)) + (b * x)) + c >= 0 ) & a > 0 implies delta (a,b,c) <= 0 ) assume that A1: for x being real number holds ((a * (x ^2)) + (b * x)) + c >= 0 and A2: a > 0 ; ::_thesis: delta (a,b,c) <= 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 delta (a,b,c) <= 0 by XREAL_1:24; ::_thesis: verum end; theorem :: QUIN_1:11 for a, b, c being real number st ( for x being real number holds ((a * (x ^2)) + (b * x)) + c <= 0 ) & a < 0 holds delta (a,b,c) <= 0 proof let a, b, c be real number ; ::_thesis: ( ( for x being real number holds ((a * (x ^2)) + (b * x)) + c <= 0 ) & a < 0 implies delta (a,b,c) <= 0 ) assume that A1: for x being real number holds ((a * (x ^2)) + (b * x)) + c <= 0 and A2: a < 0 ; ::_thesis: delta (a,b,c) <= 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 delta (a,b,c) <= 0 by XREAL_1:24; ::_thesis: verum end; theorem :: QUIN_1:12 for a, b, c being real number st ( for x being real number holds ((a * (x ^2)) + (b * x)) + c > 0 ) & a > 0 holds delta (a,b,c) < 0 proof let a, b, c be real number ; ::_thesis: ( ( for x being real number holds ((a * (x ^2)) + (b * x)) + c > 0 ) & a > 0 implies delta (a,b,c) < 0 ) assume that A1: for x being real number holds ((a * (x ^2)) + (b * x)) + c > 0 and A2: a > 0 ; ::_thesis: delta (a,b,c) < 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 delta (a,b,c) < 0 by XREAL_1:58; ::_thesis: verum end; theorem :: QUIN_1:13 for a, b, c being real number st ( for x being real number holds ((a * (x ^2)) + (b * x)) + c < 0 ) & a < 0 holds delta (a,b,c) < 0 proof let a, b, c be real number ; ::_thesis: ( ( for x being real number holds ((a * (x ^2)) + (b * x)) + c < 0 ) & a < 0 implies delta (a,b,c) < 0 ) assume that A1: for x being real number holds ((a * (x ^2)) + (b * x)) + c < 0 and A2: a < 0 ; ::_thesis: delta (a,b,c) < 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 delta (a,b,c) < 0 by XREAL_1:24; ::_thesis: verum end; theorem Th14: :: QUIN_1:14 for a, b, c, x being complex number st a <> 0 & ((a * (x ^2)) + (b * x)) + c = 0 holds ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) = 0 proof let a, b, c, x be complex number ; ::_thesis: ( a <> 0 & ((a * (x ^2)) + (b * x)) + c = 0 implies ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) = 0 ) assume that A1: a <> 0 and A2: ((a * (x ^2)) + (b * x)) + c = 0 ; ::_thesis: ((((2 * a) * x) + b) ^2) - (delta (a,b,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 ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) = 0 by A3, XCMPLX_1:87; ::_thesis: verum end; Lm1: for a, b being complex number holds ( not a ^2 = b ^2 or a = b or a = - b ) proof let a, b be complex number ; ::_thesis: ( not a ^2 = b ^2 or a = b or a = - b ) assume a ^2 = b ^2 ; ::_thesis: ( a = b or a = - b ) then (a + b) * (a - b) = 0 ; then ( a + b = 0 or a - b = 0 ) by XCMPLX_1:6; hence ( a = b or a = - b ) ; ::_thesis: verum end; theorem :: QUIN_1:15 for a, b, c, x being real number 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) proof let a, b, c, x be real number ; ::_thesis: ( a <> 0 & delta (a,b,c) >= 0 & ((a * (x ^2)) + (b * x)) + c = 0 & not x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) implies x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) assume that A1: a <> 0 and A2: delta (a,b,c) >= 0 and A3: ((a * (x ^2)) + (b * x)) + c = 0 ; ::_thesis: ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ((((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 ( x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) by A4, XCMPLX_1:89; ::_thesis: verum end; theorem Th16: :: QUIN_1:16 for a, b, c, x being real number 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))) proof let a, b, c, x be real number ; ::_thesis: ( 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))) ) assume that A1: a <> 0 and A2: delta (a,b,c) >= 0 ; ::_thesis: ((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 / (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 ((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))) ; ::_thesis: verum end; theorem Th17: :: QUIN_1:17 for a, b, c being real number 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) proof let a, b, c be real number ; ::_thesis: ( a < 0 & delta (a,b,c) > 0 implies ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) assume that A1: a < 0 and A2: delta (a,b,c) > 0 ; ::_thesis: ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) 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 ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) by A3, XREAL_1:75; ::_thesis: verum end; theorem :: QUIN_1:18 for a, b, c, x being real number 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) ) ) proof let a, b, c, x be real number ; ::_thesis: ( 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) ) ) ) assume that A1: a < 0 and A2: delta (a,b,c) > 0 ; ::_thesis: ( ((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) ) ) 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) ) ) ::_thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) implies ((a * (x ^2)) + (b * x)) + c > 0 ) proof assume ((a * (x ^2)) + (b * x)) + c > 0 ; ::_thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) 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, XREAL_1:48; hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by XXREAL_0:2; ::_thesis: verum end; assume ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) ; ::_thesis: ((a * (x ^2)) + (b * x)) + c > 0 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, XREAL_1: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 ((a * (x ^2)) + (b * x)) + c > 0 by A1, A2, Th16; ::_thesis: verum end; theorem :: QUIN_1:19 for a, b, c, x being real number 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 ) proof let a, b, c, x be real number ; ::_thesis: ( a < 0 & delta (a,b,c) > 0 implies ( ( 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 ) ) assume that A1: a < 0 and A2: delta (a,b,c) > 0 ; ::_thesis: ( ( 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 ) thus ( not ((a * (x ^2)) + (b * x)) + c < 0 or x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) ::_thesis: ( ( x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) implies ((a * (x ^2)) + (b * x)) + c < 0 ) proof assume ((a * (x ^2)) + (b * x)) + c < 0 ; ::_thesis: ( x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) 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 ( x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by XREAL_1:47, XREAL_1:48; ::_thesis: verum end; assume ( x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) ; ::_thesis: ((a * (x ^2)) + (b * x)) + c < 0 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, XREAL_1: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, XREAL_1: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 ((a * (x ^2)) + (b * x)) + c < 0 by A1, A2, Th16; ::_thesis: verum end; theorem :: QUIN_1:20 for a, b, c, x being complex number st a <> 0 & delta (a,b,c) = 0 & ((a * (x ^2)) + (b * x)) + c = 0 holds x = - (b / (2 * a)) proof let a, b, c, x be complex number ; ::_thesis: ( a <> 0 & delta (a,b,c) = 0 & ((a * (x ^2)) + (b * x)) + c = 0 implies x = - (b / (2 * a)) ) assume that A1: a <> 0 and A2: ( delta (a,b,c) = 0 & ((a * (x ^2)) + (b * x)) + c = 0 ) ; ::_thesis: x = - (b / (2 * a)) ((((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 x = - (b / (2 * a)) by XCMPLX_1:187; ::_thesis: verum end; theorem Th21: :: QUIN_1:21 for a, x, b, c being real number st a > 0 & ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 holds ((a * (x ^2)) + (b * x)) + c > 0 proof let a, x, b, c be real number ; ::_thesis: ( a > 0 & ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 implies ((a * (x ^2)) + (b * x)) + c > 0 ) assume that A1: a > 0 and A2: ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 ; ::_thesis: ((a * (x ^2)) + (b * x)) + 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 ((a * (x ^2)) + (b * x)) + c > 0 by A1, Th1; ::_thesis: verum end; theorem :: QUIN_1:22 for a, b, c, x being real number st a > 0 & delta (a,b,c) = 0 holds ( ((a * (x ^2)) + (b * x)) + c > 0 iff x <> - (b / (2 * a)) ) proof let a, b, c, x be real number ; ::_thesis: ( a > 0 & delta (a,b,c) = 0 implies ( ((a * (x ^2)) + (b * x)) + c > 0 iff x <> - (b / (2 * a)) ) ) assume that A1: a > 0 and A2: delta (a,b,c) = 0 ; ::_thesis: ( ((a * (x ^2)) + (b * x)) + c > 0 iff x <> - (b / (2 * a)) ) A3: 2 * a <> 0 by A1; thus ( ((a * (x ^2)) + (b * x)) + c > 0 implies x <> - (b / (2 * a)) ) ::_thesis: ( x <> - (b / (2 * a)) implies ((a * (x ^2)) + (b * x)) + c > 0 ) proof assume ((a * (x ^2)) + (b * x)) + c > 0 ; ::_thesis: x <> - (b / (2 * a)) 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 x <> - (b / (2 * a)) by XCMPLX_1:187; ::_thesis: verum end; assume x <> - (b / (2 * a)) ; ::_thesis: ((a * (x ^2)) + (b * x)) + c > 0 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 ((a * (x ^2)) + (b * x)) + c > 0 by A1, Th21; ::_thesis: verum end; theorem Th23: :: QUIN_1:23 for a, x, b, c being real number st a < 0 & ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 holds ((a * (x ^2)) + (b * x)) + c < 0 proof let a, x, b, c be real number ; ::_thesis: ( a < 0 & ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 implies ((a * (x ^2)) + (b * x)) + c < 0 ) assume that A1: a < 0 and A2: ((((2 * a) * x) + b) ^2) - (delta (a,b,c)) > 0 ; ::_thesis: ((a * (x ^2)) + (b * x)) + 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 ((a * (x ^2)) + (b * x)) + c < 0 by A1, Th1; ::_thesis: verum end; theorem :: QUIN_1:24 for a, b, c, x being real number st a < 0 & delta (a,b,c) = 0 holds ( ((a * (x ^2)) + (b * x)) + c < 0 iff x <> - (b / (2 * a)) ) proof let a, b, c, x be real number ; ::_thesis: ( a < 0 & delta (a,b,c) = 0 implies ( ((a * (x ^2)) + (b * x)) + c < 0 iff x <> - (b / (2 * a)) ) ) assume that A1: a < 0 and A2: delta (a,b,c) = 0 ; ::_thesis: ( ((a * (x ^2)) + (b * x)) + c < 0 iff x <> - (b / (2 * a)) ) A3: 2 * a <> 0 by A1; thus ( ((a * (x ^2)) + (b * x)) + c < 0 implies x <> - (b / (2 * a)) ) ::_thesis: ( x <> - (b / (2 * a)) implies ((a * (x ^2)) + (b * x)) + c < 0 ) proof assume ((a * (x ^2)) + (b * x)) + c < 0 ; ::_thesis: x <> - (b / (2 * a)) 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 x <> - (b / (2 * a)) by XCMPLX_1:187; ::_thesis: verum end; assume x <> - (b / (2 * a)) ; ::_thesis: ((a * (x ^2)) + (b * x)) + c < 0 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 ((a * (x ^2)) + (b * x)) + c < 0 by A1, Th23; ::_thesis: verum end; theorem Th25: :: QUIN_1:25 for a, b, c being real number 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) proof let a, b, c be real number ; ::_thesis: ( a > 0 & delta (a,b,c) > 0 implies ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) assume that A1: a > 0 and A2: delta (a,b,c) > 0 ; ::_thesis: ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) 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 ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) by A3, XREAL_1:74; ::_thesis: verum end; theorem :: QUIN_1:26 for a, b, c, x being real number 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) ) ) proof let a, b, c, x be real number ; ::_thesis: ( 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) ) ) ) assume that A1: a > 0 and A2: delta (a,b,c) > 0 ; ::_thesis: ( ((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) ) ) 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) ) ) ::_thesis: ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) implies ((a * (x ^2)) + (b * x)) + c < 0 ) proof assume ((a * (x ^2)) + (b * x)) + c < 0 ; ::_thesis: ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) 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, XREAL_1:48; hence ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) by XXREAL_0:2; ::_thesis: verum end; assume ( ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < x & x < ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ; ::_thesis: ((a * (x ^2)) + (b * x)) + c < 0 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, XREAL_1: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 ((a * (x ^2)) + (b * x)) + c < 0 by A1, A2, Th16; ::_thesis: verum end; theorem :: QUIN_1:27 for a, b, c, x being real number 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 ) proof let a, b, c, x be real number ; ::_thesis: ( a > 0 & delta (a,b,c) > 0 implies ( ( 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 ) ) assume that A1: a > 0 and A2: delta (a,b,c) > 0 ; ::_thesis: ( ( 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 ) thus ( not ((a * (x ^2)) + (b * x)) + c > 0 or x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ::_thesis: ( ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) implies ((a * (x ^2)) + (b * x)) + c > 0 ) proof assume ((a * (x ^2)) + (b * x)) + c > 0 ; ::_thesis: ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) 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 ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) by XREAL_1:47, XREAL_1:48; ::_thesis: verum end; assume ( x < ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or x > ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ) ; ::_thesis: ((a * (x ^2)) + (b * x)) + c > 0 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, XREAL_1: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, XREAL_1: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 ((a * (x ^2)) + (b * x)) + c > 0 by A1, A2, Th16; ::_thesis: verum end;