:: POLYEQ_3 semantic presentation begin definition let z be Element of COMPLEX ; :: original: ^2 redefine funcz ^2 -> Element of COMPLEX equals :: POLYEQ_3:def 1 (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ); compatibility for b1 being Element of COMPLEX holds ( b1 = z ^2 iff b1 = (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ) ) proof z = (Re z) + ((Im z) * ) by COMPLEX1:13; hence for b1 being Element of COMPLEX holds ( b1 = z ^2 iff b1 = (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ) ) ; ::_thesis: verum end; correctness coherence z ^2 is Element of COMPLEX ; by XCMPLX_0:def_2; end; :: deftheorem defines ^2 POLYEQ_3:def_1_:_ for z being Element of COMPLEX holds z ^2 = (((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ); definition let a, b, c be Real; let z be Element of COMPLEX ; :: original: Polynom redefine func Polynom (a,b,c,z) -> Element of COMPLEX ; coherence Polynom (a,b,c,z) is Element of COMPLEX by XCMPLX_0:def_2; end; theorem Th1: :: POLYEQ_3:1 for a, b, c being Real for z being Element of COMPLEX st a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,z) = 0 & not z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) holds z = - (b / (2 * a)) proof 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,z) = 0 & not z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) holds z = - (b / (2 * a)) let z be Element of COMPLEX ; ::_thesis: ( a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,z) = 0 & not z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) implies z = - (b / (2 * a)) ) A1: a = a + (0 * ) ; set y = Im z; A2: z = (Re z) + ((Im z) * ) by COMPLEX1:13; set x = Re z; assume that A3: a <> 0 and A4: delta (a,b,c) >= 0 ; ::_thesis: ( not Polynom (a,b,c,z) = 0 or z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) ) assume Polynom (a,b,c,z) = 0 ; ::_thesis: ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) ) then (((a + (0 * )) * ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))) + (b * z)) + c = 0 by A2; then 0 = (((((Re a) * (Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) * (Im a))) * )) + (b * z)) + c by COMPLEX1:def_6 .= ((((a * (Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) * (Im a))) * )) + (b * z)) + c by A1, COMPLEX1:12 .= ((((a * (((Re z) ^2) - ((Im z) ^2))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) * (Im a))) * )) + (b * z)) + c by COMPLEX1:12 .= ((((a * (((Re z) ^2) - ((Im z) ^2))) - (0 * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) * (Im a))) * )) + (b * z)) + c by A1, COMPLEX1:12 .= ((((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)) * ))) * (Im a))) * )) + (b * z)) + c by COMPLEX1:12 .= ((((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)) * ))) * (Im a))) * )) + (b * z)) + c by A1, COMPLEX1:12 .= ((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + (((a * ((2 * (Re z)) * (Im z))) + ((((Re z) ^2) - ((Im z) ^2)) * (Im a))) * )) + (b * z)) + c by COMPLEX1:12 .= ((((a * (((Re z) ^2) - ((Im z) ^2))) - 0) + (((a * ((2 * (Re z)) * (Im z))) + ((((Re z) ^2) - ((Im z) ^2)) * 0)) * )) + (b * z)) + c by A1, COMPLEX1:12 ; then A5: ((((a * (((Re z) ^2) - ((Im z) ^2))) - (0 * ((2 * (Re z)) * (Im z)))) + ((0 + (a * ((2 * (Re z)) * (Im z)))) * )) + ((b + (0 * )) * ((Re z) + ((Im z) * )))) + c = 0 by COMPLEX1:13; then A6: (((a * (((Re z) ^2) - ((Im z) ^2))) + (b * (Re z))) + c) + (((a * ((2 * (Re z)) * (Im z))) + (b * (Im z))) * ) = 0 ; then A7: (((2 * a) * (Re z)) + b) * (Im z) = 0 by COMPLEX1:4, COMPLEX1:12; percases ( Im z = 0 or ((2 * a) * (Re z)) + b = 0 ) by A7; supposeA8: Im z = 0 ; ::_thesis: ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) ) then Polynom (a,b,c,(Re z)) = 0 by A5; then ( ( Re z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & Im z = 0 ) or ( Re z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & Im z = 0 ) ) by A3, A4, A8, POLYEQ_1:5; then ( z = (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) + (0 * ) or z = (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) + (0 * ) ) by COMPLEX1:13; hence ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) ) ; ::_thesis: verum end; suppose ((2 * a) * (Re z)) + b = 0 ; ::_thesis: ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) ) then A9: Re z = (- b) / (2 * a) by A3, XCMPLX_1:89; then ((a * (((b / (2 * a)) ^2) - ((Im z) ^2))) + (b * (- (b / (2 * a))))) + c = 0 by A6, COMPLEX1:4, COMPLEX1:12; then ((b / (2 * a)) ^2) - ((Im z) ^2) = ((- ((b * (- (b / (2 * a)))) + c)) / a) - 0 by A3, 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 A10: ((Im z) ^2) * ((2 * a) ^2) = ((b ^2) + ((c * (a ")) * ((2 * a) ^2))) - (((b ^2) * (((2 * a) ") * (a "))) * ((2 * a) ^2)) by A3, 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)) ; set t = ((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 A3, 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 A3, XCMPLX_1:87; then A11: (((b ^2) * ((2 * (a * a)) ")) * ((2 * a) ^2)) / 2 = b ^2 by A3, XCMPLX_1:87; set t = (c * (a ")) * ((2 * a) ^2); (c * (a ")) * ((2 * a) ^2) = (((c / a) * a) * 2) * (2 * a) ; then A12: (c * (a ")) * ((2 * a) ^2) = (c * 2) * (2 * a) by A3, XCMPLX_1:87; - (delta (a,b,c)) <= 0 by A4; then ((Im z) * (2 * a)) ^2 = 0 by A10, A11, A12, XREAL_1:63; then Im z = 0 by A3; then z = (- (b / (2 * a))) + (0 * ) by A9, COMPLEX1:13; hence ( z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) ) ; ::_thesis: verum end; end; end; theorem Th2: :: POLYEQ_3:2 for a, b, c being 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)) * ) holds z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) proof 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,z) = 0 & not z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * ) holds z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) let z be Element of COMPLEX ; ::_thesis: ( 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)) * ) implies z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) ) assume that A1: a <> 0 and A2: delta (a,b,c) < 0 ; ::_thesis: ( not Polynom (a,b,c,z) = 0 or z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * ) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) ) A3: a = a + (0 * ) ; now__::_thesis:_for_z_being_Element_of_COMPLEX_holds_ (_not_Polynom_(a,b,c,z)_=_0_or_z_=_(-_(b_/_(2_*_a)))_+_(((sqrt_(-_(delta_(a,b,c))))_/_(2_*_a))_*_)_or_z_=_(-_(b_/_(2_*_a)))_+_((-_((sqrt_(-_(delta_(a,b,c))))_/_(2_*_a)))_*_)_) set t2 = ((- (b ^2)) + ((c * a) * 4)) / 4; let z be Element of COMPLEX ; ::_thesis: ( not Polynom (a,b,c,z) = 0 or z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * ) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) ) set x = Re z; set y = Im z; A4: z = (Re z) + ((Im z) * ) by COMPLEX1:13; assume Polynom (a,b,c,z) = 0 ; ::_thesis: ( z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * ) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) ) then (((a + (0 * )) * ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) + (b * z)) + c = 0 by A4; then (((((Re a) * (Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) * (Im a))) * )) + (b * z)) + c = 0 by COMPLEX1:def_6; then ((((a * (Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) - ((Im a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) * (Im a))) * )) + (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)) * ))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) * (Im a))) * )) + (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)) * ))))) + ((((Re a) * (Im ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((Re ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ))) * (Im a))) * )) + (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)) * ))) * (Im a))) * )) + (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)) * ))) * (Im a))) * )) + (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))) * )) + (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)) * )) + (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)))) * )) + ((b + (0 * )) * ((Re z) + ((Im z) * )))) + 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))) * ) = 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)) * ) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) ) by COMPLEX1:13; ::_thesis: verum end; hence ( not Polynom (a,b,c,z) = 0 or z = (- (b / (2 * a))) + (((sqrt (- (delta (a,b,c)))) / (2 * a)) * ) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) ) ; ::_thesis: verum end; theorem :: POLYEQ_3:3 for b, c being Real for z being Element of COMPLEX st b <> 0 & ( for z being Element of COMPLEX holds Polynom (0,b,c,z) = 0 ) holds z = - (c / b) proof let b, c be Real; ::_thesis: for z being Element of COMPLEX st b <> 0 & ( for z being Element of COMPLEX holds Polynom (0,b,c,z) = 0 ) holds z = - (c / b) let z be Element of COMPLEX ; ::_thesis: ( b <> 0 & ( for z being Element of COMPLEX holds Polynom (0,b,c,z) = 0 ) implies z = - (c / b) ) A1: 0 = 0 + (0 * ) ; assume A2: b <> 0 ; ::_thesis: ( ex z being Element of COMPLEX st not Polynom (0,b,c,z) = 0 or z = - (c / b) ) assume A3: for z being Element of COMPLEX holds Polynom (0,b,c,z) = 0 ; ::_thesis: z = - (c / b) now__::_thesis:_for_z1_being_Element_of_COMPLEX_holds_z1_=_-_(c_/_b) let z1 be Element of COMPLEX ; ::_thesis: z1 = - (c / b) Polynom (0,b,c,z1) = 0 by A3; then (b * ((Re z1) + ((Im z1) * ))) + c = 0 by COMPLEX1:13; then A4: (((b * (Re z1)) - 0) + c) + (((b * (Im z1)) + 0) * ) = 0 + (0 * ) ; then ((b * (Re z1)) - 0) + c = Re 0 by COMPLEX1:12; then ((b * (Re z1)) - 0) + c = 0 by A1, COMPLEX1:12; then A5: Re z1 = (- c) / b by A2, XCMPLX_1:89; b * (Im z1) = Im 0 by A4, COMPLEX1:12; then Im z1 = 0 by A1, A2, COMPLEX1:12; then z1 = (- (c / b)) + (0 * ) by A5, COMPLEX1:13; hence z1 = - (c / b) ; ::_thesis: verum end; hence z = - (c / b) ; ::_thesis: verum end; theorem :: POLYEQ_3:4 for a, b, c being Real for z, z1, z2 being complex number st a <> 0 & ( for z being complex number holds Polynom (a,b,c,z) = Quard (a,z1,z2,z) ) holds ( b / a = - (z1 + z2) & c / a = z1 * z2 ) proof let a, b, c be Real; ::_thesis: for z, z1, z2 being complex number st a <> 0 & ( for z being complex number holds Polynom (a,b,c,z) = Quard (a,z1,z2,z) ) holds ( b / a = - (z1 + z2) & c / a = z1 * z2 ) let z, z1, z2 be complex number ; ::_thesis: ( a <> 0 & ( for z being complex number holds Polynom (a,b,c,z) = Quard (a,z1,z2,z) ) implies ( b / a = - (z1 + z2) & c / a = z1 * z2 ) ) assume A1: a <> 0 ; ::_thesis: ( ex z being complex number st not Polynom (a,b,c,z) = Quard (a,z1,z2,z) or ( b / a = - (z1 + z2) & c / a = z1 * z2 ) ) assume A2: for z being complex number holds Polynom (a,b,c,z) = Quard (a,z1,z2,z) ; ::_thesis: ( b / a = - (z1 + z2) & c / a = z1 * z2 ) then A3: Polynom (a,b,c,0) = Quard (a,z1,z2,0) ; Quard (a,z1,z2,1) = Polynom (a,b,c,1) by A2 .= (a + b) + c ; then (a + b) + c = (a + (a * (- (z1 + z2)))) + c by A3; hence ( b / a = - (z1 + z2) & c / a = z1 * z2 ) by A1, A3, XCMPLX_1:203; ::_thesis: verum end; definition let z be complex number ; funcz ^3 -> Element of COMPLEX equals :: POLYEQ_3:def 2 (z ^2) * z; correctness coherence (z ^2) * z is Element of COMPLEX ; ; end; :: deftheorem defines ^3 POLYEQ_3:def_2_:_ for z being complex number holds z ^3 = (z ^2) * z; Lm1: for z being complex number holds z |^ 2 = z * z proof let z be complex number ; ::_thesis: z |^ 2 = z * z z |^ (1 + 1) = (z |^ 1) * z by NEWTON:6 .= z * z by NEWTON:5 ; hence z |^ 2 = z * z ; ::_thesis: verum end; definition let a, b, c, d, z be complex number ; redefine func Polynom (a,b,c,d,z) equals :: POLYEQ_3:def 3 (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d; compatibility for b1 being set holds ( b1 = Polynom (a,b,c,d,z) iff b1 = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d ) proof let x be set ; ::_thesis: ( x = Polynom (a,b,c,d,z) iff x = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d ) Polynom (a,b,c,d,z) = (((a * (z |^ (2 + 1))) + (b * (z ^2))) + (c * z)) + d .= (((a * ((z |^ 2) * z)) + (b * (z ^2))) + (c * z)) + d by NEWTON:6 ; hence ( x = Polynom (a,b,c,d,z) iff x = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d ) by Lm1; ::_thesis: verum end; end; :: deftheorem defines Polynom POLYEQ_3:def_3_:_ for a, b, c, d, z being complex number holds Polynom (a,b,c,d,z) = (((a * (z ^3)) + (b * (z ^2))) + (c * z)) + d; theorem Th5: :: POLYEQ_3:5 for z being Element of COMPLEX holds ( Re (z ^3) = ((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)) & Im (z ^3) = (- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)) ) proof let z be Element of COMPLEX ; ::_thesis: ( Re (z ^3) = ((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)) & Im (z ^3) = (- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)) ) set x = Re z; set y = Im z; (Re z) + ((Im z) * ) = z by COMPLEX1:13; then z ^3 = (((Re ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))) * (Re ((Re z) + ((Im z) * )))) - ((Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))) * (Im ((Re z) + ((Im z) * ))))) + ((((Re ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))) * (Im ((Re z) + ((Im z) * )))) + ((Re ((Re z) + ((Im z) * ))) * (Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))))) * ) by COMPLEX1:def_6 .= (((((Re z) ^2) - ((Im z) ^2)) * (Re ((Re z) + ((Im z) * )))) - ((Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))) * (Im ((Re z) + ((Im z) * ))))) + ((((Re ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))) * (Im ((Re z) + ((Im z) * )))) + ((Re ((Re z) + ((Im z) * ))) * (Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))))) * ) by COMPLEX1:12 .= (((((Re z) ^2) - ((Im z) ^2)) * (Re ((Re z) + ((Im z) * )))) - ((2 * ((Re z) * (Im z))) * (Im ((Re z) + ((Im z) * ))))) + ((((Re ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))) * (Im ((Re z) + ((Im z) * )))) + ((Re ((Re z) + ((Im z) * ))) * (Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))))) * ) by COMPLEX1:12 .= (((((Re z) ^2) - ((Im z) ^2)) * (Re ((Re z) + ((Im z) * )))) - ((2 * ((Re z) * (Im z))) * (Im ((Re z) + ((Im z) * ))))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im ((Re z) + ((Im z) * )))) + ((Re ((Re z) + ((Im z) * ))) * (Im ((((Re z) ^2) - ((Im z) ^2)) + ((2 * ((Re z) * (Im z))) * ))))) * ) by COMPLEX1:12 .= (((((Re z) ^2) - ((Im z) ^2)) * (Re ((Re z) + ((Im z) * )))) - ((2 * ((Re z) * (Im z))) * (Im ((Re z) + ((Im z) * ))))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im ((Re z) + ((Im z) * )))) + ((Re ((Re z) + ((Im z) * ))) * (2 * ((Re z) * (Im z))))) * ) by COMPLEX1:12 .= (((((Re z) ^2) - ((Im z) ^2)) * (Re z)) - ((2 * ((Re z) * (Im z))) * (Im ((Re z) + ((Im z) * ))))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im ((Re z) + ((Im z) * )))) + ((Re ((Re z) + ((Im z) * ))) * (2 * ((Re z) * (Im z))))) * ) by COMPLEX1:12 .= (((((Re z) ^2) - ((Im z) ^2)) * (Re z)) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im ((Re z) + ((Im z) * )))) + ((Re ((Re z) + ((Im z) * ))) * (2 * ((Re z) * (Im z))))) * ) by COMPLEX1:12 .= (((((Re z) ^2) - ((Im z) ^2)) * (Re z)) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) - ((Im z) ^2)) * (Im z)) + ((Re ((Re z) + ((Im z) * ))) * (2 * ((Re z) * (Im z))))) * ) by COMPLEX1:12 .= ((((((Re z) ^2) * (Re z)) - (((Im z) ^2) * (Re z))) + (0 * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + (((((((Re z) ^2) - ((Im z) ^2)) + 0) * (Im z)) + ((Re z) * (2 * ((Re z) * (Im z))))) * ) by COMPLEX1:12 .= ((((((Re z) |^ 1) * (Re z)) * (Re z)) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - (((Im z) ^2) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * ) by NEWTON:5 .= (((((Re z) |^ (1 + 1)) * (Re z)) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - (((Im z) ^2) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * ) by NEWTON:6 .= ((((Re z) |^ (2 + 1)) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - (((Im z) ^2) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * ) by NEWTON:6 .= ((((Re z) |^ 3) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - ((((Im z) |^ 1) * (Im z)) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * ) by NEWTON:5 .= ((((Re z) |^ 3) - (((Im z) ^2) * (Re z))) - ((2 * ((Re z) * (Im z))) * (Im z))) + ((((((Re z) ^2) * (Im z)) - (((Im z) |^ (1 + 1)) * (Im z))) + ((Re z) * (2 * ((Re z) * (Im z))))) * ) by NEWTON:6 .= ((((Re z) |^ 3) - (((Im z) ^2) * (Re z))) - (2 * ((Re z) * ((Im z) * (Im z))))) + ((((((Re z) ^2) * (Im z)) - ((Im z) |^ (2 + 1))) + ((Re z) * (2 * ((Re z) * (Im z))))) * ) by NEWTON:6 .= (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ) ; hence ( Re (z ^3) = ((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)) & Im (z ^3) = (- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)) ) by COMPLEX1:12; ::_thesis: verum end; theorem :: POLYEQ_3:6 for a, b, c, d, a9, b9, c9, d9 being Real st ( for z being complex number holds Polynom (a,b,c,d,z) = Polynom (a9,b9,c9,d9,z) ) holds ( a = a9 & b = b9 & c = c9 & d = d9 ) proof let a, b, c, d, a9, b9, c9, d9 be Real; ::_thesis: ( ( for z being complex number holds Polynom (a,b,c,d,z) = Polynom (a9,b9,c9,d9,z) ) implies ( a = a9 & b = b9 & c = c9 & d = d9 ) ) assume A1: for z being complex number holds Polynom (a,b,c,d,z) = Polynom (a9,b9,c9,d9,z) ; ::_thesis: ( a = a9 & b = b9 & c = c9 & d = d9 ) then A2: Polynom (a,b,c,d,0) = Polynom (a9,b9,c9,d9,0) ; A3: ( Polynom (a,b,c,d,1) = Polynom (a9,b9,c9,d9,1) & Polynom (a,b,c,d,(- 1)) = Polynom (a9,b9,c9,d9,(- 1)) ) by A1; A4: Polynom (a,b,c,d,2) = Polynom (a9,b9,c9,d9,2) by A1; hence a = a9 by A2, A3; ::_thesis: ( b = b9 & c = c9 & d = d9 ) thus b = b9 by A2, A3; ::_thesis: ( c = c9 & d = d9 ) thus c = c9 by A2, A3, A4; ::_thesis: d = d9 thus d = d9 by A2; ::_thesis: verum end; theorem :: POLYEQ_3:7 for b, c, d being Real for z being Element of COMPLEX st b <> 0 & delta (b,c,d) >= 0 & Polynom (0,b,c,d,z) = 0 & not z = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) & not z = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) holds z = - (c / (2 * b)) proof let b, c, d be Real; ::_thesis: for z being Element of COMPLEX st b <> 0 & delta (b,c,d) >= 0 & Polynom (0,b,c,d,z) = 0 & not z = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) & not z = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) holds z = - (c / (2 * b)) let z be Element of COMPLEX ; ::_thesis: ( b <> 0 & delta (b,c,d) >= 0 & Polynom (0,b,c,d,z) = 0 & not z = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) & not z = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) implies z = - (c / (2 * b)) ) assume that A1: ( b <> 0 & delta (b,c,d) >= 0 ) and A2: Polynom (0,b,c,d,z) = 0 ; ::_thesis: ( z = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or z = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) or z = - (c / (2 * b)) ) Polynom (b,c,d,z) = 0 by A2; hence ( z = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or z = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) or z = - (c / (2 * b)) ) by A1, Th1; ::_thesis: verum end; theorem :: POLYEQ_3:8 for b, c, d being Real for z being Element of COMPLEX st b <> 0 & delta (b,c,d) < 0 & Polynom (0,b,c,d,z) = 0 & not z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * ) holds z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * ) proof let b, c, d be Real; ::_thesis: for z being Element of COMPLEX st b <> 0 & delta (b,c,d) < 0 & Polynom (0,b,c,d,z) = 0 & not z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * ) holds z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * ) let z be Element of COMPLEX ; ::_thesis: ( b <> 0 & delta (b,c,d) < 0 & Polynom (0,b,c,d,z) = 0 & not z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * ) implies z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * ) ) assume that A1: ( b <> 0 & delta (b,c,d) < 0 ) and A2: Polynom (0,b,c,d,z) = 0 ; ::_thesis: ( z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * ) or z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * ) ) Polynom (b,c,d,z) = 0 by A2; hence ( z = (- (c / (2 * b))) + (((sqrt (- (delta (b,c,d)))) / (2 * b)) * ) or z = (- (c / (2 * b))) + ((- ((sqrt (- (delta (b,c,d)))) / (2 * b))) * ) ) by A1, Th2; ::_thesis: verum end; theorem :: POLYEQ_3:9 for a, c being Real 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 proof 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 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 end; theorem :: POLYEQ_3:10 for a, b, c being Real for z being Element of COMPLEX st a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,0,z) = 0 & not z = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & not z = - (b / (2 * a)) holds z = 0 proof 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) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & not z = - (b / (2 * a)) 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) + (sqrt (delta (a,b,c)))) / (2 * a) & not z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) & not z = - (b / (2 * a)) 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) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) 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) + (sqrt (delta (a,b,c)))) / (2 * a) or z = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) or z = - (b / (2 * a)) or z = 0 ) by A1, Th1; ::_thesis: verum end; theorem :: POLYEQ_3:11 for a, b, c being Real 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)) * ) & not z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) holds z = 0 proof 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)) * ) & not z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) 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)) * ) & not z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) 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)) * ) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) 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)) * ) or z = (- (b / (2 * a))) + ((- ((sqrt (- (delta (a,b,c)))) / (2 * a))) * ) or z = 0 ) by A1, Th2; ::_thesis: verum end; theorem Th12: :: POLYEQ_3:12 for y, a being Real holds ( not y ^2 = a or y = sqrt a or y = - (sqrt a) ) proof let y, a be Real; ::_thesis: ( not y ^2 = a or y = sqrt a or y = - (sqrt a) ) assume A1: y ^2 = a ; ::_thesis: ( y = sqrt a or y = - (sqrt a) ) then A2: a >= 0 by XREAL_1:63; Polynom (1,0,(- a),y) = 0 by A1; then ( y = ((- 0) + (sqrt (delta (1,0,(- a))))) / (2 * 1) or y = ((- 0) - (sqrt (delta (1,0,(- a))))) / (2 * 1) ) by A2, POLYEQ_1:5; then ( y = (sqrt (4 * a)) / 2 or y = (0 - (sqrt (4 * a))) / 2 ) ; then ( y = ((sqrt a) * 2) / 2 or y = (- (2 * (sqrt a))) / 2 ) by A2, SQUARE_1:20, SQUARE_1:29; hence ( y = sqrt a or y = - (sqrt a) ) ; ::_thesis: verum end; theorem :: POLYEQ_3:13 for a, c, d being Real for z being Element of COMPLEX st a <> 0 & Im z = 0 & Polynom (a,0,c,d,z) = 0 holds for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) proof let a, c, d be Real; ::_thesis: for z being Element of COMPLEX st a <> 0 & Im z = 0 & Polynom (a,0,c,d,z) = 0 holds for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) let z be Element of COMPLEX ; ::_thesis: ( a <> 0 & Im z = 0 & Polynom (a,0,c,d,z) = 0 implies for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) ) assume A1: a <> 0 ; ::_thesis: ( not Im z = 0 or not Polynom (a,0,c,d,z) = 0 or for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) ) set y = Im z; set x = Re z; assume that A2: Im z = 0 and A3: Polynom (a,0,c,d,z) = 0 ; ::_thesis: for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) holds z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) A4: a = a + (0 * ) ; 0 = (((a * ((Re (z ^3)) + ((Im (z ^3)) * ))) + (0 * (z ^2))) + (c * z)) + d by A3, COMPLEX1:13 .= (((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + ((Im (z ^3)) * ))) + (0 * (z ^2))) + (c * z)) + d by Th5 .= ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) + (c * z)) + d by Th5 .= (((a + (0 * )) * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:13 .= (((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:def_6 .= (((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= (((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= (((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= (((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by A4, COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - (0 * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by A4, COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by A4, COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * 0)) * )) + (c * ((Re z) + ((Im z) * )))) + d by A4, COMPLEX1:12 .= (((a * (((Re z) |^ 3) - 0)) + (c * (Re z))) + d) + ((a * (- 0)) * ) by A2, NEWTON:11 .= ((a * ((Re z) |^ 3)) + (c * (Re z))) + d ; then (a ") * (((a * ((Re z) |^ 3)) + (c * (Re z))) + d) = (a ") * 0 ; then ((((Re z) |^ 3) * (a / a)) + (((a ") * c) * (Re z))) + ((a ") * d) = 0 ; then A5: Polynom (1,0,(c / a),(d / a),(Re z)) = 0 by A1, XCMPLX_1:88; A6: ((d / a) ^2) / 4 = (1 / 4) * ((d ^2) / (a ^2)) by XCMPLX_1:76 .= (d ^2) / ((a ^2) * 4) by XCMPLX_1:103 ; let u, v be Real; ::_thesis: ( Re z = u + v & ((3 * v) * u) + (c / a) = 0 & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) & not z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) implies z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) ) assume A7: ( Re z = u + v & ((3 * v) * u) + (c / a) = 0 ) ; ::_thesis: ( z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) or z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) or z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) ) A8: - ((d / a) / 2) = - ((1 / 2) * (d / a)) .= - (d / (a * 2)) by XCMPLX_1:103 ; A9: (c / a) / 3 = (1 / 3) * (c / a) .= c / (a * 3) by XCMPLX_1:103 ; z = (Re z) + ((Im z) * ) by COMPLEX1:13 .= Re z by A2 ; hence ( z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) or z = (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) + (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) or z = (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) + (3 -root ((- (d / (2 * a))) - (sqrt (((d ^2) / (4 * (a ^2))) + ((c / (3 * a)) |^ 3))))) ) by A7, A5, A8, A6, A9, POLYEQ_1:19; ::_thesis: verum end; theorem :: POLYEQ_3:14 for a, c, d being Real for z being Element of COMPLEX st a <> 0 & Im z <> 0 & Polynom (a,0,c,d,z) = 0 holds for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) holds z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) proof let a, c, d be Real; ::_thesis: for z being Element of COMPLEX st a <> 0 & Im z <> 0 & Polynom (a,0,c,d,z) = 0 holds for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) holds z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) let z be Element of COMPLEX ; ::_thesis: ( a <> 0 & Im z <> 0 & Polynom (a,0,c,d,z) = 0 implies for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) holds z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) ) assume A1: a <> 0 ; ::_thesis: ( not Im z <> 0 or not Polynom (a,0,c,d,z) = 0 or for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) holds z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) ) set y = Im z; set x = Re z; assume that A2: Im z <> 0 and A3: Polynom (a,0,c,d,z) = 0 ; ::_thesis: for u, v being Real st Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) holds z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) A4: a = a + (0 * ) ; A5: 0 = (((a * ((Re (z ^3)) + ((Im (z ^3)) * ))) + (0 * (z ^2))) + (c * z)) + d by A3, COMPLEX1:13 .= ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + ((Im (z ^3)) * ))) + (c * z)) + d by Th5 .= ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) + (c * z)) + d by Th5 .= (((a + (0 * )) * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:13 .= (((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:def_6 .= (((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= (((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= (((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= (((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - ((Im a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by A4, COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - (0 * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))))) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by A4, COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * (Im a))) * )) + (c * ((Re z) + ((Im z) * )))) + d by A4, COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) * 0)) * )) + (c * ((Re z) + ((Im z) * )))) + d by A4, COMPLEX1:12 .= (((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) + (c * (Re z))) + d) + ((((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + (c * (Im z))) + 0) * ) ; then (a * ((- ((Im z) |^ (2 + 1))) + ((3 * ((Re z) ^2)) * (Im z)))) + (c * (Im z)) = 0 by COMPLEX1:4, COMPLEX1:12; then (a * ((- (((Im z) |^ 2) * (Im z))) + ((3 * ((Re z) ^2)) * (Im z)))) + (c * (Im z)) = 0 by NEWTON:6; then (((a * ((- ((Im z) |^ 2)) + (3 * ((Re z) ^2)))) + c) + 0) * (Im z) = 0 ; then (a * ((Im z) |^ 2)) + ((- (a * ((Im z) |^ 2))) + ((a * (3 * ((Re z) ^2))) + c)) = (a * ((Im z) |^ 2)) + 0 by A2, XCMPLX_1:6; then (Im z) |^ (1 + 1) = ((a * (3 * ((Re z) ^2))) + c) / a by A1, XCMPLX_1:89; then ((Im z) |^ 1) * (Im z) = ((a * (3 * ((Re z) ^2))) + c) / a by NEWTON:6; then A6: (Im z) ^2 = ((((3 * ((Re z) ^2)) * a) / a) + (c / a)) + (0 / a) by NEWTON:5; then A7: ( z = (Re z) + ((Im z) * ) & (Im z) ^2 = ((3 * ((Re z) ^2)) + (c / a)) + (0 * (a ")) ) by A1, COMPLEX1:13, XCMPLX_1:89; set q = - (d / (8 * a)); set pp = c / (4 * a); let u, v be Real; ::_thesis: ( Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) & not z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) implies z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) ) set m = 3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))); set n = 3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))); A8: (c / (4 * a)) / 3 = (1 / 3) * (c / (4 * a)) .= c / ((a * 4) * 3) by XCMPLX_1:103 .= c / (a * (4 * 3)) ; - ((- (d / (8 * a))) / 2) = (1 / 2) * (d / (8 * a)) ; then A9: - ((- (d / (8 * a))) / 2) = d / ((a * 8) * 2) by XCMPLX_1:103; ((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + (c * (Im z))) + 0 = 0 by A5, COMPLEX1:4, COMPLEX1:12; then ((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((3 * ((Re z) ^2)) + (c / a)))) + 0)) + (c * (Re z))) + d = 0 by A1, A5, A6, XCMPLX_1:89; then 0 = (((a * ((Re z) |^ 3)) - (a * ((9 * ((Re z) * ((Re z) ^2))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d .= (((a * ((Re z) |^ 3)) - (a * ((9 * ((((Re z) |^ 1) * (Re z)) * (Re z))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d by NEWTON:5 .= (((a * ((Re z) |^ 3)) - (a * ((9 * (((Re z) |^ (1 + 1)) * (Re z))) + ((3 * (Re z)) * (c / a))))) + (c * (Re z))) + d by NEWTON:6 .= (((a * ((Re z) |^ 3)) - (a * (((9 * ((Re z) |^ (2 + 1))) + ((3 * (Re z)) * (c / a))) + 0))) + (c * (Re z))) + d by NEWTON:6 .= (((a * ((Re z) |^ 3)) - ((a * (9 * ((Re z) |^ 3))) + ((3 * (Re z)) * (c * (a / a))))) + (c * (Re z))) + d .= (((a * ((Re z) |^ 3)) - ((a * (9 * ((Re z) |^ 3))) + ((3 * (Re z)) * c))) + (c * (Re z))) + d by A1, XCMPLX_1:88 .= (((- (8 * a)) * ((Re z) |^ 3)) + ((- (2 * c)) * (Re z))) + d ; then (- 1) * 0 = (((8 * a) * ((Re z) |^ 3)) + ((2 * c) * (Re z))) + (- d) ; then 0 = ((((Re z) |^ 3) * ((8 * a) / (8 * a))) + (((8 * a) ") * ((2 * c) * (Re z)))) + (((8 * a) ") * (- d)) ; then 0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2))) + (((2 * c) / (8 * a)) * (Re z))) + (((8 * a) ") * (- d)) by A1, XCMPLX_1:88; then 0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2))) + ((((2 / 8) * c) / a) * (Re z))) + ((- d) / (8 * a)) by XCMPLX_1:83; then 0 = (((1 * ((Re z) |^ 3)) + (0 * ((Re z) ^2))) + (((1 / a) * (c / 4)) * (Re z))) + ((- d) / (8 * a)) ; then A10: Polynom (1,0,(c / (4 * a)),(- (d / (8 * a))),(Re z)) = 0 by XCMPLX_1:103; assume ( Re z = u + v & ((3 * v) * u) + (c / (4 * a)) = 0 ) ; ::_thesis: ( z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) ) then A11: ( Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) or Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) or Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) ) by A10, POLYEQ_1:19; A12: now__::_thesis:_(_(_Re_z_=_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3)))))_+_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3)))))_&_(_z_=_((3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3)))))_+_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_+_((sqrt_((3_*_(((3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3)))))_+_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_^2))_+_(c_/_a)))_*_)_or_z_=_((3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3)))))_+_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_+_((-_(sqrt_((3_*_(((3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3)))))_+_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_^2))_+_(c_/_a))))_*_)_)_)_or_(_Re_z_=_2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3)))))_&_(_z_=_(2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_+_((sqrt_((3_*_((2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_^2))_+_(c_/_a)))_*_)_or_z_=_(2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_+_((-_(sqrt_((3_*_((2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_+_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_^2))_+_(c_/_a))))_*_)_)_)_or_(_Re_z_=_2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3)))))_&_(_z_=_(2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_+_((sqrt_((3_*_((2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_^2))_+_(c_/_a)))_*_)_or_z_=_(2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_+_((-_(sqrt_((3_*_((2_*_(3_-root_((-_((-_(d_/_(8_*_a)))_/_2))_-_(sqrt_((((-_(d_/_(8_*_a)))_^2)_/_4)_+_(((c_/_(4_*_a))_/_3)_|^_3))))))_^2))_+_(c_/_a))))_*_)_)_)_) percases ( Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) or Re z = 2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) or Re z = 2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) ) by A11; case Re z = (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) ; ::_thesis: ( z = ((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a))) * ) or z = ((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((- (sqrt ((3 * (((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a)))) * ) ) hence ( z = ((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a))) * ) or z = ((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((- (sqrt ((3 * (((3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) + (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a)))) * ) ) by A7, Th12; ::_thesis: verum end; case Re z = 2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) ; ::_thesis: ( z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((- (sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a)))) * ) ) hence ( z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((- (sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) + (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a)))) * ) ) by A7, Th12; ::_thesis: verum end; case Re z = 2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3))))) ; ::_thesis: ( z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((- (sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a)))) * ) ) hence ( z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) + ((- (sqrt ((3 * ((2 * (3 -root ((- ((- (d / (8 * a))) / 2)) - (sqrt ((((- (d / (8 * a))) ^2) / 4) + (((c / (4 * a)) / 3) |^ 3)))))) ^2)) + (c / a)))) * ) ) by A7, Th12; ::_thesis: verum end; end; end; ((- (d / (8 * a))) ^2) / 4 = ((1 / 2) * (d / (8 * a))) ^2 ; hence ( z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = ((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * (((3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3))))) + (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) + (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) + ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) or z = (2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) - ((sqrt ((3 * ((2 * (3 -root ((d / (16 * a)) - (sqrt (((d / (16 * a)) ^2) + ((c / (12 * a)) |^ 3)))))) ^2)) + (c / a))) * ) ) by A9, A12, A8; ::_thesis: verum end; theorem :: POLYEQ_3:15 for a, b, c, d being Real for z being Element of COMPLEX st a <> 0 & Polynom (a,b,c,d,z) = 0 & Im z = 0 holds for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) holds z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) proof let a, b, c, d be Real; ::_thesis: for z being Element of COMPLEX st a <> 0 & Polynom (a,b,c,d,z) = 0 & Im z = 0 holds for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) holds z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) let z be Element of COMPLEX ; ::_thesis: ( a <> 0 & Polynom (a,b,c,d,z) = 0 & Im z = 0 implies for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) holds z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) ) assume A1: a <> 0 ; ::_thesis: ( not Polynom (a,b,c,d,z) = 0 or not Im z = 0 or for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) holds z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) ) set p = (((3 * a) * c) - (b ^2)) / (3 * (a ^2)); set b9 = c / a; A2: a = a + (0 * ) ; set q = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))); set c9 = d / a; set a9 = b / a; set y = Im z; set x = Re z; assume that A3: Polynom (a,b,c,d,z) = 0 and A4: Im z = 0 ; ::_thesis: for u, v, x1 being Real st x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) holds z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) A5: z = (Re z) + ((Im z) * ) by COMPLEX1:13; 0 = (((a * ((Re (z ^3)) + ((Im (z ^3)) * ))) + (b * (z ^2))) + (c * z)) + d by A3, COMPLEX1:13 .= (((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + ((Im (z ^3)) * ))) + (b * (z ^2))) + (c * z)) + d by Th5 .= (((a * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) + (b * (z ^2))) + (c * z)) + d by Th5 .= ((((a + (0 * )) * ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:13 .= ((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) - ((Im a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:def_6 .= ((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) - (0 * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))))) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * (Im a))) * )) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * )))) + d by A2, COMPLEX1:12 .= ((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) - 0) + ((((Re a) * (Im ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) + ((Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * ))) * 0)) * )) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * )))) + d by A2, COMPLEX1:12 .= ((((((Re a) * (Re ((((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2))) + (((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z))) * )))) - 0) + ((((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) + 0) * )) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= ((((((Re a) * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) * )) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * )))) + d by COMPLEX1:12 .= (((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) - 0) + (((Re a) * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) * )) + (b * (z ^2))) + (c * ((Re z) + ((Im z) * )))) + d by A2, COMPLEX1:12 .= ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * ((Im z) ^2)))) + ((a * ((- ((Im z) |^ 3)) + ((3 * ((Re z) ^2)) * (Im z)))) * )) + (b * ((((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * )))) + ((c * (Re z)) + ((c * (Im z)) * ))) + d by A2, A5, COMPLEX1:12 ; then 0 = ((((a * (((Re z) |^ 3) - ((3 * (Re z)) * 0))) + (b * (((Re z) ^2) - 0))) + (c * (Re z))) + d) + ((((a * ((- (0 |^ 3)) + 0)) + (b * 0)) + 0) * ) by A4 .= ((((a * ((Re z) |^ 3)) + (b * ((Re z) ^2))) + (c * (Re z))) + d) + (((a * 0) + 0) * ) by NEWTON:11 ; then A6: Polynom (a,b,c,d,(Re z)) = 0 ; A7: d / a = d / a ; ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3 = (1 / 3) * ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) ; then A8: ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3 = (((3 * a) * c) - (b ^2)) / (((a ^2) * 3) * 3) by XCMPLX_1:103; A9: - (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2) = - (((b / (3 * a)) |^ 3) + ((1 / 2) * ((((3 * a) * d) - (b * c)) / (3 * (a ^2))))) .= - (((b / (3 * a)) |^ 3) + ((((3 * a) * d) - (b * c)) / (((a ^2) * 3) * 2))) by XCMPLX_1:103 .= (- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2))) ; let u, v, x1 be Real; ::_thesis: ( x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) & ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) & not z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) implies z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) ) assume that A10: ( x1 = (Re z) + (b / (3 * a)) & Re z = (u + v) - (b / (3 * a)) ) and A11: ((3 * u) * v) + ((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) = 0 ; ::_thesis: ( z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) ) ( b / a = b / a & c / a = c / a ) ; then Polynom (1,0,((((3 * a) * c) - (b ^2)) / (3 * (a ^2))),((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))),x1) = 0 by A1, A10, A6, A7, POLYEQ_1:16; then ( x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) or x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) or x1 = (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) + (3 -root ((- (((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) / 2)) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + ((((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) / 3) |^ 3))))) ) by A10, A11, POLYEQ_1:19; hence ( z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) + (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) or z = (((3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3))))) + (3 -root (((- ((b / (3 * a)) |^ 3)) - ((((3 * a) * d) - (b * c)) / (6 * (a ^2)))) - (sqrt (((((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) ^2) / 4) + (((((3 * a) * c) - (b ^2)) / (9 * (a ^2))) |^ 3)))))) - (b / (3 * a))) + (0 * ) ) by A4, A10, A8, A9, COMPLEX1:13; ::_thesis: verum end; theorem Th16: :: POLYEQ_3:16 for z1, z2, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,z) = 0 holds z = - (z2 / z1) proof let z1, z2, z be Element of COMPLEX ; ::_thesis: ( z1 <> 0 & Polynom (z1,z2,z) = 0 implies z = - (z2 / z1) ) assume ( z1 <> 0 & Polynom (z1,z2,z) = 0 ) ; ::_thesis: z = - (z2 / z1) then z = (- z2) * (z1 ") by XCMPLX_1:203; hence z = - (z2 / z1) ; ::_thesis: verum end; begin theorem :: POLYEQ_3:17 for z1, z2, z3, s1, s2, s3 being Element of COMPLEX st ( for z being Element of COMPLEX holds Polynom (z1,z2,z3,z) = Polynom (s1,s2,s3,z) ) holds ( z1 = s1 & z2 = s2 & z3 = s3 ) proof let z1, z2, z3, s1, s2, s3 be Element of COMPLEX ; ::_thesis: ( ( for z being Element of COMPLEX holds Polynom (z1,z2,z3,z) = Polynom (s1,s2,s3,z) ) implies ( z1 = s1 & z2 = s2 & z3 = s3 ) ) assume A1: for z being Element of COMPLEX holds Polynom (z1,z2,z3,z) = Polynom (s1,s2,s3,z) ; ::_thesis: ( z1 = s1 & z2 = s2 & z3 = s3 ) then A2: Polynom (z1,z2,z3,(- 1r)) = Polynom (s1,s2,s3,(- 1r)) ; ( Polynom (z1,z2,z3,0c) = Polynom (s1,s2,s3,0c) & Polynom (z1,z2,z3,1r) = Polynom (s1,s2,s3,1r) ) by A1; hence ( z1 = s1 & z2 = s2 & z3 = s3 ) by A2, COMPLEX1:def_4; ::_thesis: verum end; theorem :: POLYEQ_3:18 for a, b being Real holds ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) proof let a, b be Real; ::_thesis: ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) A1: b ^2 >= 0 by XREAL_1:63; A2: a ^2 >= 0 by XREAL_1:63; then A3: sqrt ((a ^2) + (b ^2)) >= 0 by A1, SQUARE_1:def_2; (a ^2) + (b ^2) >= 0 + (a ^2) by A1, XREAL_1:7; then A4: sqrt ((a ^2) + (b ^2)) >= sqrt (a ^2) by A2, SQUARE_1:26; percases ( a >= 0 or a < 0 ) ; supposeA5: a >= 0 ; ::_thesis: ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) then sqrt ((a ^2) + (b ^2)) >= a by A4, SQUARE_1:22; then (sqrt ((a ^2) + (b ^2))) - a >= a - a by XREAL_1:9; hence ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) by A3, A5; ::_thesis: verum end; supposeA6: a < 0 ; ::_thesis: ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) then sqrt ((a ^2) + (b ^2)) >= - a by A4, SQUARE_1:23; then (sqrt ((a ^2) + (b ^2))) - (- a) >= (- a) - (- a) by XREAL_1:9; hence ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) by A3, A6; ::_thesis: verum end; end; end; theorem Th19: :: POLYEQ_3:19 for z, s being Element of COMPLEX st z ^2 = s & Im s >= 0 & not z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) holds z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) proof let z, s be Element of COMPLEX ; ::_thesis: ( z ^2 = s & Im s >= 0 & not z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) implies z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) ) set a = Re s; set b = Im s; set u = Re z; set v = Im z; A1: z = (Re z) + ((Im z) * ) by COMPLEX1:13; assume z ^2 = s ; ::_thesis: ( not Im s >= 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) ) then A2: (((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ) = (Re s) + ((Im s) * ) by A1, COMPLEX1:13; assume Im s >= 0 ; ::_thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) ) then A3: ( ( Re z <= 0 & Im z <= 0 ) or ( Re z >= 0 & Im z >= 0 ) ) by A2, COMPLEX1:77; A4: ( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63; A5: ((Re z) ^2) - ((Im z) ^2) = Re s by A2, COMPLEX1:77; then (((Re z) ^2) + ((Im z) ^2)) ^2 = ((Re s) ^2) + ((Im s) ^2) by A2; then ((Re z) ^2) + ((Im z) ^2) = sqrt (((Re s) ^2) + ((Im s) ^2)) by A4, SQUARE_1:22; then ( ( - (Re z) = sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) & - (Im z) = sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) ) or ( Re z = sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) & Im z = sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) ) ) by A5, A3, SQUARE_1:22, SQUARE_1:23; hence ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) ) by COMPLEX1:13; ::_thesis: verum end; theorem :: POLYEQ_3:20 for z, s being Element of COMPLEX st z ^2 = s & Im s = 0 & Re s > 0 & not z = sqrt (Re s) holds z = - (sqrt (Re s)) proof let z, s be Element of COMPLEX ; ::_thesis: ( z ^2 = s & Im s = 0 & Re s > 0 & not z = sqrt (Re s) implies z = - (sqrt (Re s)) ) assume A1: z ^2 = s ; ::_thesis: ( not Im s = 0 or not Re s > 0 or z = sqrt (Re s) or z = - (sqrt (Re s)) ) assume that A2: Im s = 0 and A3: Re s > 0 ; ::_thesis: ( z = sqrt (Re s) or z = - (sqrt (Re s)) ) ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + (0 ^2)))) / 2))) * ) ) by A1, A2, Th19; then ( z = (sqrt (((Re s) + (Re s)) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2))) + (- ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * )) ) by A3, SQUARE_1:22; then ( z = (sqrt (((Re s) + (Re s)) / 2)) + ((sqrt (((- (Re s)) + (Re s)) / 2)) * ) or z = (- (sqrt (((Re s) + (Re s)) / 2))) + (- ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * )) ) by A3, SQUARE_1:22; then ( z = (sqrt (Re s)) + ((sqrt ((0 + ((Re s) - (Re s))) / 2)) * ) or z = (- (sqrt (Re s))) + (- ((sqrt ((0 + ((Re s) - (Re s))) / 2)) * )) ) by A3, SQUARE_1:22; hence ( z = sqrt (Re s) or z = - (sqrt (Re s)) ) by SQUARE_1:17; ::_thesis: verum end; theorem :: POLYEQ_3:21 for z, s being Element of COMPLEX st z ^2 = s & Im s = 0 & Re s < 0 & not z = (sqrt (- (Re s))) * holds z = - ((sqrt (- (Re s))) * ) proof let z, s be Element of COMPLEX ; ::_thesis: ( z ^2 = s & Im s = 0 & Re s < 0 & not z = (sqrt (- (Re s))) * implies z = - ((sqrt (- (Re s))) * ) ) assume A1: z ^2 = s ; ::_thesis: ( not Im s = 0 or not Re s < 0 or z = (sqrt (- (Re s))) * or z = - ((sqrt (- (Re s))) * ) ) assume that A2: Im s = 0 and A3: Re s < 0 ; ::_thesis: ( z = (sqrt (- (Re s))) * or z = - ((sqrt (- (Re s))) * ) ) ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + (0 ^2)))) / 2))) * ) ) by A1, A2, Th19; then ( z = (sqrt (((Re s) + (- (Re s))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + 0))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2))) * ) ) by A3, SQUARE_1:23; then ( z = (sqrt (((Re s) + (- (Re s))) / 2)) + ((sqrt (((- (Re s)) + (- (Re s))) / 2)) * ) or z = (- (sqrt (((Re s) + (- (Re s))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + 0))) / 2))) * ) ) by A3, SQUARE_1:23; then ( z = (sqrt (((Re s) + (- (Re s))) / 2)) + ((sqrt (((- (Re s)) + (- (Re s))) / 2)) * ) or z = (- (sqrt (((Re s) + (- (Re s))) / 2))) + ((- (sqrt (((- (Re s)) + (- (Re s))) / 2))) * ) ) by A3, SQUARE_1:23; hence ( z = (sqrt (- (Re s))) * or z = - ((sqrt (- (Re s))) * ) ) by SQUARE_1:17; ::_thesis: verum end; theorem :: POLYEQ_3:22 for z, s being Element of COMPLEX st z ^2 = s & Im s < 0 & not z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) holds z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) proof let z, s be Element of COMPLEX ; ::_thesis: ( z ^2 = s & Im s < 0 & not z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) implies z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) assume A1: z ^2 = s ; ::_thesis: ( not Im s < 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) set v = Im z; set u = Re z; set b = Im s; set a = Re s; z = (Re z) + ((Im z) * ) by COMPLEX1:13; then A2: ( s = (Re s) + ((Im s) * ) & z ^2 = (((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ) ) by COMPLEX1:13; assume Im s < 0 ; ::_thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) then 2 * ((Re z) * (Im z)) < 0 by A1, A2, COMPLEX1:77; then (Re z) * (Im z) < 0 ; then A3: ( ( Re z < 0 & Im z > 0 ) or ( Re z > 0 & Im z < 0 ) ) by XREAL_1:133; A4: ( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63; A5: ((Re z) ^2) - ((Im z) ^2) = Re s by A1, A2, COMPLEX1:77; then sqrt ((((Re z) ^2) + ((Im z) ^2)) ^2) = sqrt (((Re s) ^2) + ((Im s) ^2)) by A1, A2; then ((Re z) ^2) + ((Im z) ^2) = sqrt (((Re s) ^2) + ((Im s) ^2)) by A4, SQUARE_1:22; then ( ( - (Re z) = sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) & Im z = sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) ) or ( Re z = sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) & - (Im z) = sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) ) ) by A5, A3, SQUARE_1:22, SQUARE_1:23; hence ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) by COMPLEX1:13; ::_thesis: verum end; theorem Th23: :: POLYEQ_3:23 for z, s being Element of COMPLEX holds ( not z ^2 = s or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) proof let z, s be Element of COMPLEX ; ::_thesis: ( not z ^2 = s or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) set a = Re s; set b = Im s; set u = Re z; set v = Im z; A1: ( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63; z = (Re z) + ((Im z) * ) by COMPLEX1:13; then A2: ( s = (Re s) + ((Im s) * ) & z ^2 = (((Re z) ^2) - ((Im z) ^2)) + (((2 * (Re z)) * (Im z)) * ) ) by COMPLEX1:13; assume A3: z ^2 = s ; ::_thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) then A4: ((Re z) ^2) - ((Im z) ^2) = Re s by A2, COMPLEX1:77; then sqrt ((((Re z) ^2) + ((Im z) ^2)) ^2) = sqrt (((Re s) ^2) + ((Im s) ^2)) by A3, A2; then A5: ((Re z) ^2) + ((Im z) ^2) = sqrt (((Re s) ^2) + ((Im s) ^2)) by A1, SQUARE_1:22; percases ( Im s >= 0 or Im s < 0 ) ; suppose Im s >= 0 ; ::_thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) then ( ( Re z <= 0 & Im z <= 0 ) or ( Re z >= 0 & Im z >= 0 ) ) by A3, A2, COMPLEX1:77; then ( ( - (Re z) = sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) & - (Im z) = sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) ) or ( Re z = sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) & Im z = sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) ) ) by A4, A5, SQUARE_1:22, SQUARE_1:23; hence ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) by COMPLEX1:13; ::_thesis: verum end; suppose Im s < 0 ; ::_thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) then 2 * ((Re z) * (Im z)) < 0 by A3, A2, COMPLEX1:77; then (Re z) * (Im z) < 0 ; then ( ( Re z < 0 & Im z > 0 ) or ( Re z > 0 & Im z < 0 ) ) by XREAL_1:133; then ( ( - (Re z) = sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) & Im z = sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) ) or ( Re z = sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) & - (Im z) = sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2) ) ) by A4, A5, SQUARE_1:22, SQUARE_1:23; hence ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) by COMPLEX1:13; ::_thesis: verum end; end; end; theorem :: POLYEQ_3:24 for z1, z2, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,0,z) = 0 & not z = - (z2 / z1) holds z = 0 proof let z1, z2, z be Element of COMPLEX ; ::_thesis: ( z1 <> 0 & Polynom (z1,z2,0,z) = 0 & not z = - (z2 / z1) implies z = 0 ) assume that A1: z1 <> 0 and A2: Polynom (z1,z2,0,z) = 0 ; ::_thesis: ( z = - (z2 / z1) or z = 0 ) 0 = ((z1 * z) + z2) * z by A2; then ( Polynom (z1,z2,z) = 0 or z = 0 ) ; hence ( z = - (z2 / z1) or z = 0 ) by A1, Th16; ::_thesis: verum end; theorem Th25: :: POLYEQ_3:25 for z1, z3, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,0,z3,z) = 0 holds for s being Element of COMPLEX holds ( not s = - (z3 / z1) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) proof let z1, z3, z be Element of COMPLEX ; ::_thesis: ( z1 <> 0 & Polynom (z1,0,z3,z) = 0 implies for s being Element of COMPLEX holds ( not s = - (z3 / z1) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) ) assume ( z1 <> 0 & Polynom (z1,0,z3,z) = 0 ) ; ::_thesis: for s being Element of COMPLEX holds ( not s = - (z3 / z1) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) then A1: z ^2 = (- z3) / z1 by XCMPLX_1:89; let s be Element of COMPLEX ; ::_thesis: ( not s = - (z3 / z1) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) assume s = - (z3 / z1) ; ::_thesis: ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) hence ( z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) by A1, Th23; ::_thesis: verum end; theorem Th26: :: POLYEQ_3:26 for z1, z2, z3, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,z3,z) = 0 holds for h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t holds z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t proof let z1, z2, z3, z be Element of COMPLEX ; ::_thesis: ( z1 <> 0 & Polynom (z1,z2,z3,z) = 0 implies for h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t holds z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) assume that A1: z1 <> 0 and A2: Polynom (z1,z2,z3,z) = 0 ; ::_thesis: for h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t holds z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t (((z1 * (z ^2)) + (z2 * z)) + z3) / z1 = 0 by A2; then ((((z ^2) * z1) / z1) + ((z2 * z) / z1)) + (z3 / z1) = 0 ; then ((z ^2) + ((z2 / z1) * z)) + (z3 / z1) = 0 by A1, XCMPLX_1:89; then ((z ^2) + (((2 * z2) / (2 * z1)) * z)) + (z3 / z1) = 0 by XCMPLX_1:91; then A3: ((z + (z2 / (2 * z1))) ^2) - (((z2 / (2 * z1)) ^2) - (z3 / z1)) = 0 ; let h, t be Element of COMPLEX ; ::_thesis: ( h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t implies z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) assume ( h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) ) ; ::_thesis: ( z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) then ( (z + t) - t = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t or (z + t) - t = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or (z + t) - t = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or (z + t) - t = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) by A3, Th23; hence ( z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) ; ::_thesis: verum end; theorem :: POLYEQ_3:27 for z being Element of COMPLEX holds ( z |^ 3 = (z * z) * z & z |^ 3 = (z ^2) * z & z |^ 3 = z ^3 ) proof let z be Element of COMPLEX ; ::_thesis: ( z |^ 3 = (z * z) * z & z |^ 3 = (z ^2) * z & z |^ 3 = z ^3 ) z |^ 3 = z |^ (2 + 1) .= (z |^ (1 + 1)) * z by NEWTON:6 .= ((z |^ 1) * z) * z by NEWTON:6 .= (z * z) * z by NEWTON:5 ; hence ( z |^ 3 = (z * z) * z & z |^ 3 = (z ^2) * z & z |^ 3 = z ^3 ) ; ::_thesis: verum end; theorem :: POLYEQ_3:28 for z1, z2, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,0,0,z) = 0 & not z = - (z2 / z1) holds z = 0 proof let z1, z2, z be Element of COMPLEX ; ::_thesis: ( z1 <> 0 & Polynom (z1,z2,0,0,z) = 0 & not z = - (z2 / z1) implies z = 0 ) assume that A1: z1 <> 0 and A2: Polynom (z1,z2,0,0,z) = 0 ; ::_thesis: ( z = - (z2 / z1) or z = 0 ) 0 = ((z1 * z) + z2) * (z ^2) by A2; then ( Polynom (z1,z2,z) = 0 or ((1 * (z ^2)) + (0 * z)) + 0 = 0 ) ; hence ( z = - (z2 / z1) or z = 0 ) by A1, Th16; ::_thesis: verum end; theorem :: POLYEQ_3:29 for z1, z3, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,0,z3,0,z) = 0 holds for s being Element of COMPLEX holds ( not s = - (z3 / z1) or z = 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) proof let z1, z3, z be Element of COMPLEX ; ::_thesis: ( z1 <> 0 & Polynom (z1,0,z3,0,z) = 0 implies for s being Element of COMPLEX holds ( not s = - (z3 / z1) or z = 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) ) assume that A1: z1 <> 0 and A2: Polynom (z1,0,z3,0,z) = 0 ; ::_thesis: for s being Element of COMPLEX holds ( not s = - (z3 / z1) or z = 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) let s be Element of COMPLEX ; ::_thesis: ( not s = - (z3 / z1) or z = 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) 0 = ((z1 * (z ^2)) + z3) * z by A2; then A3: ( Polynom (z1,0,z3,z) = 0 or z = 0 ) ; assume s = - (z3 / z1) ; ::_thesis: ( z = 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) hence ( z = 0 or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) + ((- (sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) * ) or z = (- (sqrt (((Re s) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2))) + ((sqrt (((- (Re s)) + (sqrt (((Re s) ^2) + ((Im s) ^2)))) / 2)) * ) ) by A1, A3, Th25; ::_thesis: verum end; theorem :: POLYEQ_3:30 for z1, z2, z3, z being Element of COMPLEX st z1 <> 0 & Polynom (z1,z2,z3,0,z) = 0 holds for s, h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t holds z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t proof let z1, z2, z3, z be Element of COMPLEX ; ::_thesis: ( z1 <> 0 & Polynom (z1,z2,z3,0,z) = 0 implies for s, h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t holds z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) assume that A1: z1 <> 0 and A2: Polynom (z1,z2,z3,0,z) = 0 ; ::_thesis: for s, h, t being Element of COMPLEX st h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t holds z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t let s, h, t be Element of COMPLEX ; ::_thesis: ( h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) & not z = 0 & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t & not z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t & not z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t implies z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) 0 = (Polynom (z1,z2,z3,z)) * z by A2; then A3: ( z = 0 or Polynom (z1,z2,z3,z) = 0 ) ; assume ( h = ((z2 / (2 * z1)) ^2) - (z3 / z1) & t = z2 / (2 * z1) ) ; ::_thesis: ( z = 0 or z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) hence ( z = 0 or z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or z = ((sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) + ((- (sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) * )) - t or z = ((- (sqrt (((Re h) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2))) + ((sqrt (((- (Re h)) + (sqrt (((Re h) ^2) + ((Im h) ^2)))) / 2)) * )) - t ) by A1, A3, Th26; ::_thesis: verum end; Lm2: for n being Nat st n > 0 holds 0 |^ n = 0 proof let n be Nat; ::_thesis: ( n > 0 implies 0 |^ n = 0 ) assume n > 0 ; ::_thesis: 0 |^ n = 0 then n >= 0 + 1 by NAT_1:13; hence 0 |^ n = 0 by NEWTON:11; ::_thesis: verum end; theorem Th31: :: POLYEQ_3:31 for x being real number for n being Element of NAT holds ((cos x) + ((sin x) * )) |^ n = (cos (n * x)) + ((sin (n * x)) * ) proof let x be real number ; ::_thesis: for n being Element of NAT holds ((cos x) + ((sin x) * )) |^ n = (cos (n * x)) + ((sin (n * x)) * ) defpred S1[ Element of NAT ] means ((cos x) + ((sin x) * )) |^ $1 = (cos ($1 * x)) + ((sin ($1 * x)) * ); A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] then ((cos x) + ((sin x) * )) |^ (n + 1) = ((cos (n * x)) + ((sin (n * x)) * )) * ((cos x) + ((sin x) * )) by NEWTON:6 .= (((cos (n * x)) * (cos x)) - ((sin (n * x)) * (sin x))) + ((((cos (n * x)) * (sin x)) + ((cos x) * (sin (n * x)))) * ) .= (cos ((n * x) + x)) + ((((cos (n * x)) * (sin x)) + ((cos x) * (sin (n * x)))) * ) by SIN_COS:75 .= (cos ((n + 1) * x)) + ((sin ((n + 1) * x)) * ) by SIN_COS:75 ; hence S1[n + 1] ; ::_thesis: verum end; A2: S1[ 0 ] by NEWTON:4, SIN_COS:31; thus for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1); ::_thesis: verum end; theorem :: POLYEQ_3:32 for z being Element of COMPLEX for n being Element of NAT holds z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * ) proof let z be Element of COMPLEX ; ::_thesis: for n being Element of NAT holds z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * ) let n be Element of NAT ; ::_thesis: z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * ) z |^ n = (((|.z.| * (cos (Arg z))) - (0 * (sin (Arg z)))) + (((|.z.| * (sin (Arg z))) + ((cos (Arg z)) * 0)) * )) |^ n by COMPLEX2:12 .= (|.z.| * ((cos (Arg z)) + ((sin (Arg z)) * ))) |^ n .= (|.z.| |^ n) * (((cos (Arg z)) + ((sin (Arg z)) * )) |^ n) by NEWTON:7 ; hence z |^ n = (|.z.| to_power n) * ((cos (n * (Arg z))) + ((sin (n * (Arg z))) * )) by Th31 .= ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * ) ; ::_thesis: verum end; theorem Th33: :: POLYEQ_3:33 for n, k being Element of NAT for x being Real st n <> 0 holds ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos x) + ((sin x) * ) proof let n, k be Element of NAT ; ::_thesis: for x being Real st n <> 0 holds ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos x) + ((sin x) * ) let x be Real; ::_thesis: ( n <> 0 implies ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos x) + ((sin x) * ) ) assume A1: n <> 0 ; ::_thesis: ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos x) + ((sin x) * ) thus ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos (n * ((x + ((2 * PI) * k)) / n))) + ((sin (n * ((x + ((2 * PI) * k)) / n))) * ) by Th31 .= (cos (x + ((2 * PI) * k))) + ((sin (n * ((x + ((2 * PI) * k)) / n))) * ) by A1, XCMPLX_1:87 .= (cos (x + ((2 * PI) * k))) + ((sin (x + ((2 * PI) * k))) * ) by A1, XCMPLX_1:87 .= (cos . (x + ((2 * PI) * k))) + ((sin (x + ((2 * PI) * k))) * ) by SIN_COS:def_19 .= (cos . (x + ((2 * PI) * k))) + ((sin . (x + ((2 * PI) * k))) * ) by SIN_COS:def_17 .= (cos . (x + ((2 * PI) * k))) + ((sin . x) * ) by SIN_COS2:10 .= (cos . x) + ((sin . x) * ) by SIN_COS2:11 .= (cos . x) + ((sin x) * ) by SIN_COS:def_17 .= (cos x) + ((sin x) * ) by SIN_COS:def_19 ; ::_thesis: verum end; theorem Th34: :: POLYEQ_3:34 for z being complex number for n, k being Element of NAT st n <> 0 holds z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n proof let z be complex number ; ::_thesis: for n, k being Element of NAT st n <> 0 holds z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n let n, k be Element of NAT ; ::_thesis: ( n <> 0 implies z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n ) assume A1: n <> 0 ; ::_thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n then A2: n >= 0 + 1 by NAT_1:13; percases ( z <> 0 or z = 0 ) ; suppose z <> 0 ; ::_thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n then A3: |.z.| > 0 by COMPLEX1:47; thus (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n = ((n -root |.z.|) * ((cos (((Arg z) + ((2 * PI) * k)) / n)) + ((sin (((Arg z) + ((2 * PI) * k)) / n)) * ))) |^ n .= ((n -root |.z.|) |^ n) * (((cos (((Arg z) + ((2 * PI) * k)) / n)) + ((sin (((Arg z) + ((2 * PI) * k)) / n)) * )) |^ n) by NEWTON:7 .= ((n -root |.z.|) |^ n) * ((cos (Arg z)) + ((sin (Arg z)) * )) by A1, Th33 .= |.z.| * ((cos (Arg z)) + ((sin (Arg z)) * )) by A1, A3, COMPTRIG:4 .= ((|.z.| * (cos (Arg z))) - (0 * (sin (Arg z)))) + (((|.z.| * (sin (Arg z))) + (0 * (cos (Arg z)))) * ) .= z by COMPLEX2:12 ; ::_thesis: verum end; supposeA4: z = 0 ; ::_thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n hence (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n = ((0 * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root 0) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n by A2, COMPLEX1:44, POWER:5 .= ((0 * (sin (((Arg z) + ((2 * PI) * k)) / n))) * ) |^ n by A2, POWER:5 .= z by A1, A4, Lm2 ; ::_thesis: verum end; end; end; theorem :: POLYEQ_3:35 for z being Element of COMPLEX for n being non empty Element of NAT for k being Element of NAT holds ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * ) is CRoot of n,z proof let z be Element of COMPLEX ; ::_thesis: for n being non empty Element of NAT for k being Element of NAT holds ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * ) is CRoot of n,z let n be non empty Element of NAT ; ::_thesis: for k being Element of NAT holds ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * ) is CRoot of n,z let k be Element of NAT ; ::_thesis: ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * ) is CRoot of n,z (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n = z by Th34; hence ((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * ) is CRoot of n,z by COMPTRIG:def_2; ::_thesis: verum end; theorem :: POLYEQ_3:36 for z being complex number for v being CRoot of 1,z holds v = z proof let z be complex number ; ::_thesis: for v being CRoot of 1,z holds v = z let v be CRoot of 1,z; ::_thesis: v = z v |^ 1 = z by COMPTRIG:def_2; hence v = z by NEWTON:5; ::_thesis: verum end; theorem :: POLYEQ_3:37 for n being non empty Nat for v being CRoot of n, 0 holds v = 0 proof let n be non empty Nat; ::_thesis: for v being CRoot of n, 0 holds v = 0 let v be CRoot of n, 0 ; ::_thesis: v = 0 defpred S1[ Nat] means v |^ $1 = 0 ; A1: now__::_thesis:_for_k_being_non_empty_Nat_st_k_<>_1_&_S1[k]_holds_ ex_t_being_non_empty_Nat_st_ (_t_<_k_&_S1[t]_) let k be non empty Nat; ::_thesis: ( k <> 1 & S1[k] implies ex t being non empty Nat st ( t < k & S1[t] ) ) assume that A2: k <> 1 and A3: S1[k] ; ::_thesis: ex t being non empty Nat st ( t < k & S1[t] ) consider t being Nat such that A4: k = t + 1 by NAT_1:6; reconsider t = t as non empty Nat by A2, A4; take t = t; ::_thesis: ( t < k & S1[t] ) thus t < k by A4, NAT_1:13; ::_thesis: S1[t] v |^ k = (v |^ t) * v by A4, NEWTON:6; then ( v |^ t = 0 or v = 0 ) by A3; hence S1[t] by Lm2; ::_thesis: verum end; A5: ex n being non empty Nat st S1[n] proof take n ; ::_thesis: S1[n] thus S1[n] by COMPTRIG:def_2; ::_thesis: verum end; S1[1] from COMPTRIG:sch_1(A5, A1); hence v = 0 by NEWTON:5; ::_thesis: verum end; theorem :: POLYEQ_3:38 for n being non empty Element of NAT for z being complex number for v being CRoot of n,z st v = 0 holds z = 0 proof let n be non empty Element of NAT ; ::_thesis: for z being complex number for v being CRoot of n,z st v = 0 holds z = 0 let z be complex number ; ::_thesis: for v being CRoot of n,z st v = 0 holds z = 0 let v be CRoot of n,z; ::_thesis: ( v = 0 implies z = 0 ) assume v = 0 ; ::_thesis: z = 0 then 0 |^ n = z by COMPTRIG:def_2; hence z = 0 by Lm2; ::_thesis: verum end; theorem :: POLYEQ_3:39 for n being non empty Element of NAT for k being Element of NAT holds (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * ) is CRoot of n,1 proof let n be non empty Element of NAT ; ::_thesis: for k being Element of NAT holds (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * ) is CRoot of n,1 let k be Element of NAT ; ::_thesis: (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * ) is CRoot of n,1 ((cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * )) |^ n = (cos (n * (((2 * PI) * k) / n))) + ((sin (n * (((2 * PI) * k) / n))) * ) by Th31 .= (cos ((2 * PI) * k)) + ((sin (n * (((2 * PI) * k) / n))) * ) by XCMPLX_1:87 .= (cos (((2 * PI) * k) + 0)) + ((sin (((2 * PI) * k) + 0)) * ) by XCMPLX_1:87 .= (cos . (((2 * PI) * k) + 0)) + ((sin (((2 * PI) * k) + 0)) * ) by SIN_COS:def_19 .= (cos . (((2 * PI) * k) + 0)) + ((sin . (((2 * PI) * k) + 0)) * ) by SIN_COS:def_17 .= (cos . (((2 * PI) * k) + 0)) + ((sin . 0) * ) by SIN_COS2:10 .= 1 by SIN_COS:30, SIN_COS2:11 ; hence (cos (((2 * PI) * k) / n)) + ((sin (((2 * PI) * k) / n)) * ) is CRoot of n,1 by COMPTRIG:def_2; ::_thesis: verum end; theorem :: POLYEQ_3:40 for z, s being Element of COMPLEX for n being Element of NAT st s <> 0 & z <> 0 & n >= 1 & s |^ n = z |^ n holds |.s.| = |.z.| proof let z, s be Element of COMPLEX ; ::_thesis: for n being Element of NAT st s <> 0 & z <> 0 & n >= 1 & s |^ n = z |^ n holds |.s.| = |.z.| let n be Element of NAT ; ::_thesis: ( s <> 0 & z <> 0 & n >= 1 & s |^ n = z |^ n implies |.s.| = |.z.| ) assume that A1: s <> 0 and A2: z <> 0 and A3: n >= 1 and A4: s |^ n = z |^ n ; ::_thesis: |.s.| = |.z.| z |^ n = ((|.s.| * (cos (Arg s))) + ((|.s.| * (sin (Arg s))) * )) |^ n by A4, COMPLEX2:12 .= (|.s.| * ((cos (Arg s)) + ((sin (Arg s)) * ))) |^ n .= (|.s.| |^ n) * (((cos (Arg s)) + ((sin (Arg s)) * )) |^ n) by NEWTON:7 .= (|.s.| to_power n) * ((cos (n * (Arg s))) + ((sin (n * (Arg s))) * )) by Th31 .= ((|.s.| to_power n) * (cos (n * (Arg s)))) + (((|.s.| to_power n) * (sin (n * (Arg s)))) * ) ; then A5: ((|.s.| to_power n) * (cos (n * (Arg s)))) + (((|.s.| to_power n) * (sin (n * (Arg s)))) * ) = ((|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * )) |^ n by COMPLEX2:12 .= (|.z.| * ((cos (Arg z)) + ((sin (Arg z)) * ))) |^ n .= (|.z.| |^ n) * (((cos (Arg z)) + ((sin (Arg z)) * )) |^ n) by NEWTON:7 .= (|.z.| to_power n) * ((cos (n * (Arg z))) + ((sin (n * (Arg z))) * )) by Th31 .= ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * ) ; then (|.s.| to_power n) * (cos (n * (Arg s))) = (|.z.| to_power n) * (cos (n * (Arg z))) by COMPLEX1:77; then (((|.s.| to_power n) ^2) * ((cos (n * (Arg s))) ^2)) + (((|.s.| to_power n) * (sin (n * (Arg s)))) ^2) = (((|.z.| to_power n) * (cos (n * (Arg z)))) ^2) + (((|.z.| to_power n) * (sin (n * (Arg z)))) ^2) by A5, SQUARE_1:9; then ((|.s.| to_power n) ^2) * (((cos (n * (Arg s))) ^2) + ((sin (n * (Arg s))) ^2)) = ((|.z.| to_power n) ^2) * (((cos (n * (Arg z))) ^2) + ((sin (n * (Arg z))) ^2)) ; then ((|.s.| to_power n) ^2) * (((cos (n * (Arg s))) ^2) + ((sin (n * (Arg s))) ^2)) = ((|.z.| to_power n) ^2) * 1 by SIN_COS:29; then A6: ((|.s.| to_power n) ^2) * 1 = (|.z.| to_power n) ^2 by SIN_COS:29; A7: |.s.| > 0 by A1, COMPLEX1:47; then |.s.| to_power n > 0 by POWER:34; then A8: |.s.| to_power n = sqrt ((|.z.| to_power n) ^2) by A6, SQUARE_1:22; A9: |.z.| > 0 by A2, COMPLEX1:47; then |.z.| to_power n > 0 by POWER:34; then |.s.| |^ n = |.z.| |^ n by A8, SQUARE_1:22; then |.s.| = n -root (|.z.| |^ n) by A3, A7, POWER:4; hence |.s.| = |.z.| by A3, A9, POWER:4; ::_thesis: verum end;