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 / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * <i>) holds
z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * <i>)
let z be Complex; :: thesis: ( b <> 0 & delta (b,c,d) < 0 & Polynom (0,b,c,d,z) = 0 & not z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * <i>) implies z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * <i>) )
assume that
A1: ( b <> 0 & delta (b,c,d) < 0 ) and
A2: Polynom (0,b,c,d,z) = 0 ; :: thesis: ( z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * <i>) or z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * <i>) )
Polynom (b,c,d,z) = 0 by A2;
hence ( z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * <i>) or z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * <i>) ) by A1, Th2; :: thesis: verum