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