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