let b, c be Real; :: thesis: for z being Complex st b <> 0 & ( for z being Complex holds Polynom (0,b,c,z) = 0 ) holds
z = - (c / b)
let z be Complex; :: thesis: ( b <> 0 & ( for z being Complex holds Polynom (0,b,c,z) = 0 ) implies z = - (c / b) )
A1: 0 = 0 + (0 * <i>) ;
assume A2: b <> 0 ; :: thesis: ( ex z being Complex st not Polynom (0,b,c,z) = 0 or z = - (c / b) )
assume A3: for z being Complex holds Polynom (0,b,c,z) = 0 ; :: thesis: z = - (c / b)
now :: thesis: for z1 being Complex holds z1 = - (c / b)
let z1 be Complex; :: thesis: z1 = - (c / b)
Polynom (0,b,c,z1) = 0 by A3;
then (b * ((Re z1) + ((Im z1) * <i>))) + c = 0 by COMPLEX1:13;
then A4: (((b * (Re z1)) - 0) + c) + (((b * (Im z1)) + 0) * <i>) = 0 + (0 * <i>) ;
then ((b * (Re z1)) - 0) + c = Re 0 by COMPLEX1:12;
then ((b * (Re z1)) - 0) + c = 0 by A1, COMPLEX1:12;
then A5: Re z1 = (- c) / b by A2, XCMPLX_1:89;
b * (Im z1) = Im 0 by A4, COMPLEX1:12;
then Im z1 = 0 by A1, A2, COMPLEX1:12;
then z1 = (- (c / b)) + (0 * <i>) by A5, COMPLEX1:13;
hence z1 = - (c / b) ; :: thesis: verum
end;
hence z = - (c / b) ; :: thesis: verum