let a, b, c be Real; :: thesis: for z being Complex st a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,z) = 0 & not z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) holds
z = - (b / (2 * a))
let z be Complex; :: thesis: ( a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,z) = 0 & not z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) implies z = - (b / (2 * a)) )
A1: a = a + (0 * <i>) ;
set y = Im z;
A2: z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
set x = Re z;
assume that
A3: a <> 0 and
A4: delta (a,b,c) >= 0 ; :: thesis: ( not Polynom (a,b,c,z) = 0 or z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) )
assume Polynom (a,b,c,z) = 0 ; :: thesis: ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) )
then (((a + (0 * <i>)) * ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * <i>))) + (b * z)) + c = 0 by A2;
then 0 = (((((Re a) * (Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c by COMPLEX1:82
.= ((((a * (Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c by A1, COMPLEX1:12
.= ((((a * (((Re z) ^2) - ((Im z) ^2))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c by COMPLEX1:12
.= ((((a * (((Re z) ^2) - ((Im z) ^2))) - (0 * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c by A1, COMPLEX1:12
.= ((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + ((((Re a) * ((2 * (Re z)) * (Im z))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c by COMPLEX1:12
.= ((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + (((a * ((2 * (Re z)) * (Im z))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c by A1, COMPLEX1:12
.= ((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + (((a * ((2 * (Re z)) * (Im z))) + ((((Re z) ^2) - ((Im z) ^2)) * (Im a))) * <i>)) + (b * z)) + c by COMPLEX1:12
.= ((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + (((a * ((2 * (Re z)) * (Im z))) + ((((Re z) ^2) - ((Im z) ^2)) * 0)) * <i>)) + (b * z)) + c by A1, COMPLEX1:12 ;
then A5: ((((a * (((Re z) ^2) - ((Im z) ^2))) - (0 * ((2 * (Re z)) * (Im z)))) + ((0 + (a * ((2 * (Re z)) * (Im z)))) * <i>)) + ((b + (0 * <i>)) * ((Re z) + ((Im z) * <i>)))) + c = 0 by COMPLEX1:13;
then A6: (((a * (((Re z) ^2) - ((Im z) ^2))) + (b * (Re z))) + c) + (((a * ((2 * (Re z)) * (Im z))) + (b * (Im z))) * <i>) = 0 ;
then A7: (((2 * a) * (Re z)) + b) * (Im z) = 0 by COMPLEX1:4, COMPLEX1:12;
per cases ( Im z = 0 or ((2 * a) * (Re z)) + b = 0 ) by A7;
suppose A8: Im z = 0 ; :: thesis: ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) )
then Polynom (a,b,c,(Re z)) = 0 by A5;
then ( ( Re z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & Im z = 0 ) or ( Re z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & Im z = 0 ) ) by A3, A4, A8, POLYEQ_1:5;
then ( z = (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) + (0 * <i>) or z = (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) + (0 * <i>) ) by COMPLEX1:13;
hence ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) ) ; :: thesis: verum
end;
suppose ((2 * a) * (Re z)) + b = 0 ; :: thesis: ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) )
then A9: Re z = (- b) / (2 * a) by A3, XCMPLX_1:89;
then ((a * (((b / (2 * a)) ^2) - ((Im z) ^2))) + (b * (- (b / (2 * a))))) + c = 0 by A6, COMPLEX1:4, COMPLEX1:12;
then ((b / (2 * a)) ^2) - ((Im z) ^2) = ((- ((b * (- (b / (2 * a)))) + c)) / a) - 0 by A3, XCMPLX_1:89;
then ((b / (2 * a)) ^2) - ((- ((b * (- (b / (2 * a)))) + c)) / a) = ((Im z) ^2) - 0 ;
then (Im z) ^2 = (((b / (2 * a)) ^2) + (c * (a "))) - (((b ^2) / (2 * a)) * (a ")) ;
then ((Im z) ^2) * ((2 * a) ^2) = ((((b ^2) / ((2 * a) ^2)) + (c * (a "))) - (((b ^2) / (2 * a)) * (a "))) * ((2 * a) ^2) by XCMPLX_1:76
.= ((((b ^2) / ((2 * a) ^2)) * ((2 * a) ^2)) + ((c * (a ")) * ((2 * a) ^2))) - ((((b ^2) * ((2 * a) ")) * (a ")) * ((2 * a) ^2)) ;
then A10: ((Im z) ^2) * ((2 * a) ^2) = ((b ^2) + ((c * (a ")) * ((2 * a) ^2))) - (((b ^2) * (((2 * a) ") * (a "))) * ((2 * a) ^2)) by A3, XCMPLX_1:87
.= ((b ^2) + ((c * (a ")) * ((2 * a) ^2))) - (((b ^2) * (((2 * a) * a) ")) * ((2 * a) ^2)) by XCMPLX_1:204
.= ((b ^2) + ((c * (a ")) * ((2 * a) ^2))) - (((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) ;
set t = ((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2);
(((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ") = ((b ^2) * ((2 * (a * a)) ")) * (((2 * a) ^2) * (1 / ((2 * a) ^2))) ;
then (((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ") = ((b ^2) * ((2 * (a * a)) ")) * 1 by A3, XCMPLX_1:106;
then ((((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ")) * (2 ") = ((b ^2) * ((2 * (a ^2)) ")) * (2 ") ;
then ((((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ")) * (2 ") = (b ^2) * (((2 * (a ^2)) ") * (2 ")) ;
then ((((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ")) * (2 ") = (b ^2) * ((2 * ((a ^2) * 2)) ") by XCMPLX_1:204;
then (((((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (2 ")) / ((2 * a) ^2)) * ((2 * a) ^2) = ((b ^2) / ((2 * a) ^2)) * ((2 * a) ^2) ;
then (((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (2 ") = ((b ^2) / ((2 * a) ^2)) * ((2 * a) ^2) by A3, XCMPLX_1:87;
then A11: (((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) / 2 = b ^2 by A3, XCMPLX_1:87;
set t = (c * (a ")) * ((2 * a) ^2);
(c * (a ")) * ((2 * a) ^2) = (((c / a) * a) * 2) * (2 * a) ;
then A12: (c * (a ")) * ((2 * a) ^2) = (c * 2) * (2 * a) by A3, XCMPLX_1:87;
- (delta (a,b,c)) <= 0 by A4;
then ((Im z) * (2 * a)) ^2 = 0 by A10, A11, A12, XREAL_1:63;
then Im z = 0 by A3;
then z = (- (b / (2 * a))) + (0 * <i>) by A9, COMPLEX1:13;
hence ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) ) ; :: thesis: verum
end;
end;