let b, c, d be Real; :: thesis: for z being 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 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, Th1; :: thesis: verum