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 / (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 Element of 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, Th5; :: thesis: verum