quin_1.miz



    begin

    reserve x,a,b,c for Real;

    definition

      let a,b,c be Complex;

      :: QUIN_1:def1

      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 :: QUIN_1:1

    

     Th1: for a,b,c,x be 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 :: QUIN_1:2

    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, 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 thesis by A1, Th1;

    end;

    theorem :: QUIN_1:3

    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, 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 thesis by A1, Th1;

    end;

    theorem :: QUIN_1:4

    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, 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 thesis by A1, Th1;

    end;

    theorem :: QUIN_1:5

    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, 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 thesis by A1, Th1;

    end;

    theorem :: QUIN_1:6

    

     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 :: QUIN_1:7

    

     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 :: QUIN_1:8

    

     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 :: QUIN_1:9

    

     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 :: QUIN_1:10

    (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 :: QUIN_1:11

    (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 :: QUIN_1:12

    (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 :: QUIN_1:13

    (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 :: QUIN_1:14

    

     Th14: for a,b,c,x be 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 be 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 :: 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))

    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 :: QUIN_1:16

    

     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 :: QUIN_1:17

    

     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 :: 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)))

    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, XREAL_1: 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, 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 thesis by A1, A2, Th16;

    end;

    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)))

    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, XREAL_1: 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, 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 thesis by A1, A2, Th16;

    end;

    theorem :: QUIN_1:20

    for a,b,c,x be 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 :: QUIN_1:21

    

     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 :: QUIN_1:22

    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 :: QUIN_1:23

    

     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 :: QUIN_1:24

    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 :: QUIN_1:25

    

     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 :: 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)))

    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, XREAL_1: 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, 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 thesis by A1, A2, Th16;

    end;

    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)))

    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, XREAL_1: 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, 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 thesis by A1, A2, Th16;

    end;