let a, b, c be Real; for z being Complex st a <> 0 & delta (a,b,c) < 0 & Polynom (a,b,c,z) = 0 & not z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) holds
z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>)
let z be Complex; ( a <> 0 & delta (a,b,c) < 0 & Polynom (a,b,c,z) = 0 & not z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * <i>) implies z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * <i>) )
assume that
A1:
a <> 0
and
A2:
delta (a,b,c) < 0
; ( not Polynom (a,b,c,z) = 0 or 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>) )
A3:
a = a + (0 * <i>)
;
now for z being Complex holds
( not Polynom (a,b,c,z) = 0 or 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>) )set t2 =
((- (b ^2)) + ((c * a) * 4)) / 4;
let z be
Complex;
( not Polynom (a,b,c,z) = 0 or 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>) )set x =
Re z;
set y =
Im z;
A4:
z = (Re z) + ((Im z) * <i>)
by COMPLEX1:13;
assume
Polynom (
a,
b,
c,
z)
= 0
;
( 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>) )then
(((a + (0 * <i>)) * ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) + (b * z)) + c = 0
by A4;
then
(((((Re a) * (Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c = 0
by COMPLEX1:82;
then
((((a * (Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c = 0
by A3, COMPLEX1:12;
then
((((a * (((Re z) ^2) - ((Im z) ^2))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c = 0
by COMPLEX1:12;
then
((((a * (((Re z) ^2) - ((Im z) ^2))) - (0 * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>)))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c = 0
by A3, COMPLEX1:12;
then
((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + ((((Re a) * ((2 * (Re z)) * (Im z))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c = 0
by COMPLEX1:12;
then
((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + (((a * ((2 * (Re z)) * (Im z))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * <i>))) * (Im a))) * <i>)) + (b * z)) + c = 0
by A3, COMPLEX1:12;
then
((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + (((a * ((2 * (Re z)) * (Im z))) + ((((Re z) ^2) - ((Im z) ^2)) * (Im a))) * <i>)) + (b * z)) + c = 0
by COMPLEX1:12;
then
((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + (((a * ((2 * (Re z)) * (Im z))) + ((((Re z) ^2) - ((Im z) ^2)) * 0)) * <i>)) + (b * z)) + c = 0
by A3, COMPLEX1:12;
then
((((a * (((Re z) ^2) - ((Im z) ^2))) - (0 * ((2 * (Re z)) * (Im z)))) + ((((((Re z) ^2) - ((Im z) ^2)) * 0) + (a * ((2 * (Re z)) * (Im z)))) * <i>)) + ((b + (0 * <i>)) * ((Re z) + ((Im z) * <i>)))) + c = 0
by COMPLEX1:13;
then A5:
(((a * (((Re z) ^2) - ((Im z) ^2))) + (b * (Re z))) + c) + (((a * ((2 * (Re z)) * (Im z))) + (b * (Im z))) * <i>) = 0
;
then
((a * (2 * (Re z))) * (Im z)) + (b * (Im z)) = 0
by COMPLEX1:4, COMPLEX1:12;
then A6:
((a * 2) * (Re z)) * (Im z) = (- b) * (Im z)
;
set t =
((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2);
set t1 =
(((Re z) * a) + (b / 2)) ^2 ;
0 - (delta (a,b,c)) > 0
by A2;
then A7:
0 + 0 < ((((Re z) * a) + (b / 2)) ^2) + (((- (b ^2)) + ((c * a) * 4)) / 4)
by XREAL_1:8, XREAL_1:63;
((- (a * ((Im z) ^2))) + (((b * (Re z)) + (a * ((Re z) ^2))) + c)) + (a * ((Im z) ^2)) = 0 + (a * ((Im z) ^2))
by A5, COMPLEX1:4, COMPLEX1:12;
then
(((a * ((Re z) ^2)) * a) + ((b * (Re z)) * a)) + (c * a) = (a * ((Im z) ^2)) * a
by XCMPLX_1:9;
then
Im z <> 0
by A7;
then
a * (2 * (Re z)) = - b
by A6, XCMPLX_1:5;
then
2
* (Re z) = (- b) / a
by A1, XCMPLX_1:89;
then
Re z = (1 / a) * ((- b) / 2)
;
then A8:
Re z = (- b) / (2 * a)
by XCMPLX_1:103;
then
((a * (((b / (2 * a)) ^2) - ((Im z) ^2))) + (b * (- (b / (2 * a))))) + c = 0
by A5, COMPLEX1:4, COMPLEX1:12;
then
((b / (2 * a)) ^2) - ((Im z) ^2) = ((- ((b * (- (b / (2 * a)))) + c)) / a) - 0
by A1, XCMPLX_1:89;
then
((b / (2 * a)) ^2) - ((- ((b * (- (b / (2 * a)))) + c)) / a) = ((Im z) ^2) - 0
;
then
(Im z) ^2 = (((b / (2 * a)) ^2) + (c * (a "))) - (((b ^2) / (2 * a)) * (a "))
;
then ((Im z) ^2) * ((2 * a) ^2) =
((((b ^2) / ((2 * a) ^2)) + (c * (a "))) - (((b ^2) / (2 * a)) * (a "))) * ((2 * a) ^2)
by XCMPLX_1:76
.=
((((b ^2) / ((2 * a) ^2)) * ((2 * a) ^2)) + ((c * (a ")) * ((2 * a) ^2))) - ((((b ^2) * ((2 * a) ")) * (a ")) * ((2 * a) ^2))
;
then A9:
((Im z) ^2) * ((2 * a) ^2) =
((b ^2) + ((c * (a ")) * ((2 * a) ^2))) - (((b ^2) * (((2 * a) ") * (a "))) * ((2 * a) ^2))
by A1, XCMPLX_1:87
.=
((b ^2) + ((c * (a ")) * ((2 * a) ^2))) - (((b ^2) * (((2 * a) * a) ")) * ((2 * a) ^2))
by XCMPLX_1:204
.=
((b ^2) + ((c * (a ")) * ((2 * a) ^2))) - (((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2))
;
(((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ") = ((b ^2) * ((2 * (a * a)) ")) * (((2 * a) ^2) * (1 / ((2 * a) ^2)))
;
then
(((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ") = ((b ^2) * ((2 * (a * a)) ")) * 1
by A1, XCMPLX_1:106;
then
((((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ")) * (2 ") = ((b ^2) * ((2 * (a ^2)) ")) * (2 ")
;
then
((((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ")) * (2 ") = (b ^2) * (((2 * (a ^2)) ") * (2 "))
;
then
((((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (((2 * a) ^2) ")) * (2 ") = (b ^2) * ((2 * ((a ^2) * 2)) ")
by XCMPLX_1:204;
then
(((((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (2 ")) / ((2 * a) ^2)) * ((2 * a) ^2) = ((b ^2) / ((2 * a) ^2)) * ((2 * a) ^2)
;
then
(((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) * (2 ") = ((b ^2) / ((2 * a) ^2)) * ((2 * a) ^2)
by A1, XCMPLX_1:87;
then A10:
(((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) / 2
= b ^2
by A1, XCMPLX_1:87;
set t =
(c * (a ")) * ((2 * a) ^2);
(c * (a ")) * ((2 * a) ^2) = (((c / a) * a) * 2) * (2 * a)
;
then
(c * (a ")) * ((2 * a) ^2) = (c * 2) * (2 * a)
by A1, XCMPLX_1:87;
then
((Im z) * (2 * a)) ^2 = (sqrt (- (delta (a,b,c)))) ^2
by A2, A9, A10, SQUARE_1:def 2;
then
(((Im z) * (2 * a)) + (sqrt (- (delta (a,b,c))))) * (((Im z) * (2 * a)) - (sqrt (- (delta (a,b,c))))) = 0
;
then
(
((Im z) * (2 * a)) + (sqrt (- (delta (a,b,c)))) = 0 or
((Im z) * (2 * a)) - (sqrt (- (delta (a,b,c)))) = 0 )
;
then
(
Im z = (- (sqrt (- (delta (a,b,c))))) / (2 * a) or
((Im z) * (2 * a)) / (2 * a) = (sqrt (- (delta (a,b,c)))) / (2 * a) )
by A1, XCMPLX_1:89;
then
( (
Re z = - (b / (2 * a)) &
Im z = (sqrt (- (delta (a,b,c)))) / (2 * a) ) or (
Re z = - (b / (2 * a)) &
Im z = - ((sqrt (- (delta (a,b,c)))) / (2 * a)) ) )
by A1, A8, XCMPLX_1:89;
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>) )
by COMPLEX1:13;
verum end;
hence
( not Polynom (a,b,c,z) = 0 or 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>) )
; verum