let b, c, d be Real; :: thesis: for z being Element of COMPLEX st b <> 0 & delta b,c,d >= 0 & Polynom 0 ,b,c,d,z = 0 & not z = ((- c) + (sqrt (delta b,c,d))) / (2 * b) & not z = ((- c) - (sqrt (delta b,c,d))) / (2 * b) holds
z = - (c / (2 * b))
let z be Element of COMPLEX ; :: thesis: ( b <> 0 & delta b,c,d >= 0 & Polynom 0 ,b,c,d,z = 0 & not z = ((- c) + (sqrt (delta b,c,d))) / (2 * b) & not z = ((- c) - (sqrt (delta b,c,d))) / (2 * b) implies z = - (c / (2 * b)) )
assume that
A1: ( b <> 0 & delta b,c,d >= 0 ) and
A2: Polynom 0 ,b,c,d,z = 0 ; :: thesis: ( z = ((- c) + (sqrt (delta b,c,d))) / (2 * b) or z = ((- c) - (sqrt (delta b,c,d))) / (2 * b) or z = - (c / (2 * b)) )
Polynom b,c,d,z = 0 by A2;
hence ( z = ((- c) + (sqrt (delta b,c,d))) / (2 * b) or z = ((- c) - (sqrt (delta b,c,d))) / (2 * b) or z = - (c / (2 * b)) ) by A1, Th4; :: thesis: verum