set t2 = ((- (b ^2)) + ((c * a) * 4)) / 4;
let z be Complex; :: thesis: ( not Polynom (a,b,c,z) = 0 or z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) )
set x = Re z;
set y = Im z;
A4: z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
assume Polynom (a,b,c,z) = 0 ; :: thesis: ( z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) )
then (((a + (0 * <i>)) * ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) + (b * z)) + c = 0 by A4;
then (((((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 = 0 by COMPLEX1:82;
then ((((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 = 0 by A3, COMPLEX1:12;
then ((((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 = 0 by COMPLEX1:12;
then ((((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 = 0 by A3, COMPLEX1:12;
then ((((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 = 0 by COMPLEX1:12;
then ((((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 = 0 by A3, COMPLEX1:12;
then ((((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 = 0 by COMPLEX1:12;
then ((((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 = 0 by A3, COMPLEX1:12;
then ((((a * (((Re z) ^2) - ((Im z) ^2))) - (0 * ((2 * (Re z)) * (Im z)))) + ((((((Re z) ^2) - ((Im z) ^2)) * 0) + (a * ((2 * (Re z)) * (Im z)))) * <i>)) + ((b + (0 * <i>)) * ((Re z) + ((Im z) * <i>)))) + c = 0 by COMPLEX1:13;
then A5: (((a * (((Re z) ^2) - ((Im z) ^2))) + (b * (Re z))) + c) + (((a * ((2 * (Re z)) * (Im z))) + (b * (Im z))) * <i>) = 0 ;
then ((a * (2 * (Re z))) * (Im z)) + (b * (Im z)) = 0 by COMPLEX1:4, COMPLEX1:12;
then A6: ((a * 2) * (Re z)) * (Im z) = (- b) * (Im z) ;
set t = ((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2);
set t1 = (((Re z) * a) + (b / 2)) ^2 ;
0 - (delta (a,b,c)) > 0 by A2;
then A7: 0 + 0 < ((((Re z) * a) + (b / 2)) ^2) + (((- (b ^2)) + ((c * a) * 4)) / 4) by XREAL_1:8, XREAL_1:63;
((- (a * ((Im z) ^2))) + (((b * (Re z)) + (a * ((Re z) ^2))) + c)) + (a * ((Im z) ^2)) = 0 + (a * ((Im z) ^2)) by A5, COMPLEX1:4, COMPLEX1:12;
then (((a * ((Re z) ^2)) * a) + ((b * (Re z)) * a)) + (c * a) = (a * ((Im z) ^2)) * a by XCMPLX_1:9;
then Im z <> 0 by A7;
then a * (2 * (Re z)) = - b by A6, XCMPLX_1:5;
then 2 * (Re z) = (- b) / a by A1, XCMPLX_1:89;
then Re z = (1 / a) * ((- b) / 2) ;
then A8: Re z = (- b) / (2 * a) by XCMPLX_1:103;
then ((a * (((b / (2 * a)) ^2) - ((Im z) ^2))) + (b * (- (b / (2 * a))))) + c = 0 by A5, COMPLEX1:4, COMPLEX1:12;
then ((b / (2 * a)) ^2) - ((Im z) ^2) = ((- ((b * (- (b / (2 * a)))) + c)) / a) - 0 by A1, 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 A9: ((Im z) ^2) * ((2 * a) ^2) = ((b ^2) + ((c * (a ")) * ((2 * a) ^2))) - (((b ^2) * (((2 * a) ") * (a "))) * ((2 * a) ^2)) by A1, 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)) ;
(((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 A1, 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 A1, XCMPLX_1:87;
then A10: (((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) / 2 = b ^2 by A1, XCMPLX_1:87;
set t = (c * (a ")) * ((2 * a) ^2);
(c * (a ")) * ((2 * a) ^2) = (((c / a) * a) * 2) * (2 * a) ;
then (c * (a ")) * ((2 * a) ^2) = (c * 2) * (2 * a) by A1, XCMPLX_1:87;
then ((Im z) * (2 * a)) ^2 = (sqrt (- (delta (a,b,c)))) ^2 by A2, A9, A10, SQUARE_1:def 2;
then (((Im z) * (2 * a)) + (sqrt (- (delta (a,b,c))))) * (((Im z) * (2 * a)) - (sqrt (- (delta (a,b,c))))) = 0 ;
then ( ((Im z) * (2 * a)) + (sqrt (- (delta (a,b,c)))) = 0 or ((Im z) * (2 * a)) - (sqrt (- (delta (a,b,c)))) = 0 ) ;
then ( Im z = (- (sqrt (- (delta (a,b,c))))) / (2 * a) or ((Im z) * (2 * a)) / (2 * a) = (sqrt (- (delta (a,b,c)))) / (2 * a) ) by A1, XCMPLX_1:89;
then ( ( Re z = - (b / (2 * a)) & Im z = (sqrt (- (delta (a,b,c)))) / (2 * a) ) or ( Re z = - (b / (2 * a)) & Im z = - ((sqrt (- (delta (a,b,c)))) / (2 * a)) ) ) by A1, A8, XCMPLX_1:89;
hence ( z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) ) by COMPLEX1:13; :: thesis: verum