let a, b, c be Real; for z being Element of 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 Element of 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 set t2 =
((- (b ^2 )) + ((c * a) * 4)) / 4;
let z be
Element of
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:29;
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:def 10;
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:28;
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:28;
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:28;
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:28;
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:28;
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:28;
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:28;
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:29;
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:12, COMPLEX1:28;
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:10, XREAL_1:65;
((- (a * ((Im z) ^2 ))) + (((b * (Re z)) + (a * ((Re z) ^2 ))) + c)) + (a * ((Im z) ^2 )) = 0 + (a * ((Im z) ^2 ))
by A5, COMPLEX1:12, COMPLEX1:28;
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:90;
then
Re z = (1 / a) * ((- b) / 2)
;
then A8:
Re z = (- b) / (2 * a)
by XCMPLX_1:104;
then
((a * (((b / (2 * a)) ^2 ) - ((Im z) ^2 ))) + (b * (- (b / (2 * a))))) + c = 0
by A5, COMPLEX1:12, COMPLEX1:28;
then
((b / (2 * a)) ^2 ) - ((Im z) ^2 ) = ((- ((b * (- (b / (2 * a)))) + c)) / a) - 0
by A1, XCMPLX_1:90;
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:77
.=
((((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:88
.=
((b ^2 ) + ((c * (a " )) * ((2 * a) ^2 ))) - (((b ^2 ) * (((2 * a) * a) " )) * ((2 * a) ^2 ))
by XCMPLX_1:205
.=
((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:107;
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:205;
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:88;
then A10:
(((b ^2 ) * ((2 * (a * a)) " )) * ((2 * a) ^2 )) / 2
= b ^2
by A1, XCMPLX_1:88;
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:88;
then
((Im z) * (2 * a)) ^2 = (sqrt (- (delta a,b,c))) ^2
by A2, A9, A10, SQUARE_1:def 4;
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:90;
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:90;
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:29;
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