let a, c be Real; :: thesis: for z being 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 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 that
A1: ( a <> 0 & (4 * a) * c <= 0 ) and
A2: 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 )
((a * (z ^2)) + c) * z = 0 by A2;
then ( Polynom (a,0,c,z) = 0 or z = 0 ) ;
then ( 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, Th1;
hence ( z = (sqrt (- ((4 * a) * c))) / (2 * a) or z = (- (sqrt (- ((4 * a) * c)))) / (2 * a) or z = 0 ) ; :: thesis: verum