:: POLYEQ_1 semantic presentation begin definition let a, b, x be complex number ; func Polynom (a,b,x) -> set equals :: POLYEQ_1:def 1 (a * x) + b; coherence (a * x) + b is set ; end; :: deftheorem defines Polynom POLYEQ_1:def_1_:_ for a, b, x being complex number holds Polynom (a,b,x) = (a * x) + b; registration let a, b, x be complex number ; cluster Polynom (a,b,x) -> complex ; coherence Polynom (a,b,x) is complex ; end; registration let a, b, x be real number ; cluster Polynom (a,b,x) -> real ; coherence Polynom (a,b,x) is real ; end; definition let a, b, x be Real; :: original: Polynom redefine func Polynom (a,b,x) -> Real; coherence Polynom (a,b,x) is Real by XREAL_0:def_1; end; theorem :: POLYEQ_1:1 for a, b, x being complex number st a <> 0 & Polynom (a,b,x) = 0 holds x = - (b / a) proof let a, b, x be complex number ; ::_thesis: ( a <> 0 & Polynom (a,b,x) = 0 implies x = - (b / a) ) assume that A1: a <> 0 and A2: Polynom (a,b,x) = 0 ; ::_thesis: x = - (b / a) (a ") * (- b) = (a ") * (a * x) by A2 .= ((a ") * a) * x ; then 1 * x = (a ") * (- b) by A1, XCMPLX_0:def_7; then x = - ((a ") * b) ; hence x = - (b / a) by XCMPLX_0:def_9; ::_thesis: verum end; theorem :: POLYEQ_1:2 for x being complex number holds Polynom (0,0,x) = 0 ; theorem :: POLYEQ_1:3 for b being complex number st b <> 0 holds for x being complex number holds not Polynom (0,b,x) = 0 ; definition let a, b, c, x be complex number ; func Polynom (a,b,c,x) -> set equals :: POLYEQ_1:def 2 ((a * (x ^2)) + (b * x)) + c; coherence ((a * (x ^2)) + (b * x)) + c is set ; end; :: deftheorem defines Polynom POLYEQ_1:def_2_:_ for a, b, c, x being complex number holds Polynom (a,b,c,x) = ((a * (x ^2)) + (b * x)) + c; registration let a, b, c, x be real number ; cluster Polynom (a,b,c,x) -> real ; coherence Polynom (a,b,c,x) is real ; end; registration let a, b, c, x be complex number ; cluster Polynom (a,b,c,x) -> complex ; coherence Polynom (a,b,c,x) is complex ; end; definition let a, b, c, x be Real; :: original: Polynom redefine func Polynom (a,b,c,x) -> Real; coherence Polynom (a,b,c,x) is Real by XREAL_0:def_1; end; theorem Th4: :: POLYEQ_1:4 for a, b, c, a9, b9, c9 being complex number st ( for x being real number holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) holds ( a = a9 & b = b9 & c = c9 ) proof let a, b, c, a9, b9, c9 be complex number ; ::_thesis: ( ( for x being real number holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ) implies ( a = a9 & b = b9 & c = c9 ) ) assume A1: for x being real number holds Polynom (a,b,c,x) = Polynom (a9,b9,c9,x) ; ::_thesis: ( a = a9 & b = b9 & c = c9 ) then A2: Polynom (a,b,c,(- 1)) = Polynom (a9,b9,c9,(- 1)) ; ( Polynom (a,b,c,0) = Polynom (a9,b9,c9,0) & Polynom (a,b,c,1) = Polynom (a9,b9,c9,1) ) by A1; hence ( a = a9 & b = b9 & c = c9 ) by A2; ::_thesis: verum end; theorem Th5: :: POLYEQ_1:5 for a, b, c being real number st a <> 0 & delta (a,b,c) >= 0 holds for x being real number holds ( not Polynom (a,b,c,x) = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) proof let a, b, c be real number ; ::_thesis: ( a <> 0 & delta (a,b,c) >= 0 implies for x being real number holds ( not Polynom (a,b,c,x) = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) ) assume that A1: a <> 0 and A2: delta (a,b,c) >= 0 ; ::_thesis: for x being real number holds ( not Polynom (a,b,c,x) = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) now__::_thesis:_for_y_being_real_number_holds_ (_not_Polynom_(a,b,c,y)_=_0_or_y_=_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_or_y_=_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_) set e = a * c; let y be real number ; ::_thesis: ( not Polynom (a,b,c,y) = 0 or y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) set t = ((a ^2) * (y ^2)) + ((a * b) * y); assume Polynom (a,b,c,y) = 0 ; ::_thesis: ( y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) then a * (((a * (y ^2)) + (b * y)) + c) = a * 0 ; then ((a * (a * (y ^2))) + (a * (b * y))) + (a * c) = 0 ; then A3: ((((a ^2) * (y ^2)) + ((a * b) * y)) + ((b ^2) / 4)) - ((b ^2) * (4 ")) = - ((4 * (a * c)) * (4 ")) ; A4: delta (a,b,c) = (b ^2) - ((4 * a) * c) by QUIN_1:def_1; A5: now__::_thesis:_(_((a_*_y)_+_(b_/_2))_-_(sqrt_(((b_^2)_-_(4_*_(a_*_c)))_/_4))_=_0_implies_y_=_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_) assume ((a * y) + (b / 2)) - (sqrt (((b ^2) - (4 * (a * c))) / 4)) = 0 ; ::_thesis: y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) then (a * y) + (b / 2) = (sqrt ((b ^2) - (4 * (a * c)))) / 2 by A2, A4, SQUARE_1:20, SQUARE_1:30; then a * y = - ((b * (2 ")) - ((sqrt ((b ^2) - (4 * (a * c)))) * (2 "))) .= ((- b) * (2 ")) + ((sqrt (delta (a,b,c))) * (2 ")) by A4 ; then y = (((- b) * (2 ")) + ((sqrt (delta (a,b,c))) * (2 "))) / a by A1, XCMPLX_1:89 .= (((- b) * (2 ")) + ((sqrt (delta (a,b,c))) * (2 "))) * (a ") by XCMPLX_0:def_9 .= ((- b) + (sqrt (delta (a,b,c)))) * ((2 ") * (a ")) .= ((- b) + (sqrt (delta (a,b,c)))) * ((2 * a) ") by XCMPLX_1:204 ; hence y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) by XCMPLX_0:def_9; ::_thesis: verum end; A6: now__::_thesis:_(_((a_*_y)_+_(b_/_2))_+_(sqrt_(((b_^2)_-_(4_*_(a_*_c)))_/_4))_=_0_implies_y_=_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_) assume ((a * y) + (b / 2)) + (sqrt (((b ^2) - (4 * (a * c))) / 4)) = 0 ; ::_thesis: y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) then (a * y) + (b / 2) = - (sqrt (((b ^2) - (4 * (a * c))) / 4)) ; then (a * y) + (b / 2) = - ((sqrt ((b ^2) - (4 * (a * c)))) / 2) by A2, A4, SQUARE_1:20, SQUARE_1:30; then a * y = - ((b * (2 ")) + ((sqrt ((b ^2) - (4 * (a * c)))) * (2 "))) .= ((- b) * (2 ")) - ((sqrt (delta (a,b,c))) * (2 ")) by A4 ; then y = (((- b) * (2 ")) - ((sqrt (delta (a,b,c))) * (2 "))) / a by A1, XCMPLX_1:89 .= (((- b) * (2 ")) - ((sqrt (delta (a,b,c))) * (2 "))) * (a ") by XCMPLX_0:def_9 .= ((- b) - (sqrt (delta (a,b,c)))) * ((2 ") * (a ")) .= ((- b) - (sqrt (delta (a,b,c)))) * ((2 * a) ") by XCMPLX_1:204 ; hence y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) by XCMPLX_0:def_9; ::_thesis: verum end; ((b ^2) - (4 * (a * c))) / 4 >= 0 / 4 by A2, A4, XREAL_1:72; then ((a * y) + (b / 2)) ^2 = (sqrt (((b ^2) - (4 * (a * c))) / 4)) ^2 by A3, SQUARE_1:def_2; then (((a * y) + (b / 2)) - (sqrt (((b ^2) - (4 * (a * c))) / 4))) * (((a * y) + (b / 2)) + (sqrt (((b ^2) - (4 * (a * c))) / 4))) = 0 ; hence ( y = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by A5, A6, XCMPLX_1:6; ::_thesis: verum end; hence for x being real number holds ( not Polynom (a,b,c,x) = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) ; ::_thesis: verum end; theorem :: POLYEQ_1:6 for a, b, c, x being complex number st a <> 0 & delta (a,b,c) = 0 & Polynom (a,b,c,x) = 0 holds x = - (b / (2 * a)) proof let a, b, c, x be complex number ; ::_thesis: ( a <> 0 & delta (a,b,c) = 0 & Polynom (a,b,c,x) = 0 implies x = - (b / (2 * a)) ) assume that A1: a <> 0 and A2: delta (a,b,c) = 0 ; ::_thesis: ( not Polynom (a,b,c,x) = 0 or x = - (b / (2 * a)) ) set y = x; set t = ((a ^2) * (x ^2)) + ((a * b) * x); A3: (b ^2) - ((4 * a) * c) = delta (a,b,c) by QUIN_1:def_1; assume Polynom (a,b,c,x) = 0 ; ::_thesis: x = - (b / (2 * a)) then a * (((a * (x ^2)) + (b * x)) + c) = 0 ; then (((a ^2) * (x ^2)) + ((a * b) * x)) + (a * c) = 0 ; then (((a * x) ^2) + (2 * (((a * x) * b) * (2 ")))) + ((b / 2) ^2) = 0 by A2, A3; then ((a * x) + (b / 2)) ^2 = 0 ; then (a * x) + (b / 2) = 0 by XCMPLX_1:6; then x = (- (b * (2 "))) / a by A1, XCMPLX_1:89 .= ((- 1) * (b * (2 "))) * (a ") by XCMPLX_0:def_9 .= - ((b * ((2 ") * (a "))) * 1) .= - (b * ((2 * a) ")) by XCMPLX_1:204 ; hence x = - (b / (2 * a)) by XCMPLX_0:def_9; ::_thesis: verum end; theorem :: POLYEQ_1:7 for a, b, c being real number st delta (a,b,c) < 0 holds for x being real number holds not Polynom (a,b,c,x) = 0 proof let a, b, c be real number ; ::_thesis: ( delta (a,b,c) < 0 implies for x being real number holds not Polynom (a,b,c,x) = 0 ) set e = a * c; assume delta (a,b,c) < 0 ; ::_thesis: for x being real number holds not Polynom (a,b,c,x) = 0 then (b ^2) - ((4 * a) * c) < 0 by QUIN_1:def_1; then A1: ((b ^2) - (4 * (a * c))) * (4 ") < 0 by XREAL_1:132; given y being real number such that A2: Polynom (a,b,c,y) = 0 ; ::_thesis: contradiction set t = ((a ^2) * (y ^2)) + ((a * b) * y); a * (((a * (y ^2)) + (b * y)) + c) = a * 0 by A2; then ((((a ^2) * (y ^2)) + ((a * b) * y)) + ((b ^2) / 4)) - (((b ^2) * (4 ")) - ((4 * (a * c)) * (4 "))) = 0 ; then A3: ((a * y) + (b / 2)) ^2 = ((b ^2) - (4 * (a * c))) * (4 ") ; then (a * y) + (b / 2) > 0 by A1, XREAL_1:133; hence contradiction by A3, A1, XREAL_1:133; ::_thesis: verum end; theorem :: POLYEQ_1:8 for x being real number for b, c being complex number st b <> 0 & ( for x being real number holds Polynom (0,b,c,x) = 0 ) holds x = - (c / b) proof let x be real number ; ::_thesis: for b, c being complex number st b <> 0 & ( for x being real number holds Polynom (0,b,c,x) = 0 ) holds x = - (c / b) let b, c be complex number ; ::_thesis: ( b <> 0 & ( for x being real number holds Polynom (0,b,c,x) = 0 ) implies x = - (c / b) ) assume A1: b <> 0 ; ::_thesis: ( ex x being real number st not Polynom (0,b,c,x) = 0 or x = - (c / b) ) set y = x; assume for x being real number holds Polynom (0,b,c,x) = 0 ; ::_thesis: x = - (c / b) then Polynom (0,b,c,x) = 0 ; then x = (- c) / b by A1, XCMPLX_1:89 .= ((- 1) * c) * (b ") by XCMPLX_0:def_9 .= (- 1) * (c * (b ")) .= (- 1) * (c / b) by XCMPLX_0:def_9 ; hence x = - (c / b) ; ::_thesis: verum end; theorem :: POLYEQ_1:9 for x being complex number holds Polynom (0,0,0,x) = 0 ; theorem :: POLYEQ_1:10 for c being complex number st c <> 0 holds for x being complex number holds not Polynom (0,0,c,x) = 0 ; definition let a, x, x1, x2 be complex number ; func Quard (a,x1,x2,x) -> set equals :: POLYEQ_1:def 3 a * ((x - x1) * (x - x2)); coherence a * ((x - x1) * (x - x2)) is set ; end; :: deftheorem defines Quard POLYEQ_1:def_3_:_ for a, x, x1, x2 being complex number holds Quard (a,x1,x2,x) = a * ((x - x1) * (x - x2)); registration let a, x, x1, x2 be real number ; cluster Quard (a,x1,x2,x) -> real ; coherence Quard (a,x1,x2,x) is real ; end; definition let a, x, x1, x2 be Real; :: original: Quard redefine func Quard (a,x1,x2,x) -> Real; coherence Quard (a,x1,x2,x) is Real by XREAL_0:def_1; end; theorem :: POLYEQ_1:11 for x1, x2 being real number for a, b, c being complex number st a <> 0 & ( for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) holds ( b / a = - (x1 + x2) & c / a = x1 * x2 ) proof let x1, x2 be real number ; ::_thesis: for a, b, c being complex number st a <> 0 & ( for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) holds ( b / a = - (x1 + x2) & c / a = x1 * x2 ) let a, b, c be complex number ; ::_thesis: ( a <> 0 & ( for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ) implies ( b / a = - (x1 + x2) & c / a = x1 * x2 ) ) assume A1: a <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a,b,c,x) = Quard (a,x1,x2,x) or ( b / a = - (x1 + x2) & c / a = x1 * x2 ) ) assume A2: for x being real number holds Polynom (a,b,c,x) = Quard (a,x1,x2,x) ; ::_thesis: ( b / a = - (x1 + x2) & c / a = x1 * x2 ) now__::_thesis:_for_z_being_real_number_holds_Polynom_(1,(-_(x1_+_x2)),(x1_*_x2),z)_=_Polynom_(1,(b_/_a),(c_/_a),z) let z be real number ; ::_thesis: Polynom (1,(- (x1 + x2)),(x1 * x2),z) = Polynom (1,(b / a),(c / a),z) set h = z - x1; set t = z - x2; set e = ((z - x1) * (z - x2)) - (z ^2); Polynom (a,b,c,z) = Quard (a,x1,x2,z) by A2; then a * (((z - x1) * (z - x2)) - (z ^2)) = (b * z) + c ; then ((z - x1) * (z - x2)) - (z ^2) = ((b * z) + c) / a by A1, XCMPLX_1:89 .= (a ") * ((b * z) + c) by XCMPLX_0:def_9 .= ((a ") * (b * z)) + ((a ") * c) ; then (((z * z) - (z * x2)) - (x1 * z)) + (x1 * x2) = ((z ^2) + (((a ") * b) * z)) + ((a ") * c) ; then ((z ^2) - ((x1 + x2) * z)) + (x1 * x2) = ((z ^2) + ((b / a) * z)) + ((a ") * c) by XCMPLX_0:def_9 .= ((z ^2) + ((b / a) * z)) + (c / a) by XCMPLX_0:def_9 ; hence Polynom (1,(- (x1 + x2)),(x1 * x2),z) = Polynom (1,(b / a),(c / a),z) ; ::_thesis: verum end; hence ( b / a = - (x1 + x2) & c / a = x1 * x2 ) by Th4; ::_thesis: verum end; begin definition let a, b, c, d, x be complex number ; func Polynom (a,b,c,d,x) -> set equals :: POLYEQ_1:def 4 (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d; coherence (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d is set ; end; :: deftheorem defines Polynom POLYEQ_1:def_4_:_ for a, b, c, d, x being complex number holds Polynom (a,b,c,d,x) = (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d; registration let a, b, c, d, x be complex number ; cluster Polynom (a,b,c,d,x) -> complex ; coherence Polynom (a,b,c,d,x) is complex ; end; registration let a, b, c, d, x be real number ; cluster Polynom (a,b,c,d,x) -> real ; coherence Polynom (a,b,c,d,x) is real ; end; definition let a, b, c, d, x be Real; :: original: Polynom redefine func Polynom (a,b,c,d,x) -> Real; coherence Polynom (a,b,c,d,x) is Real by XREAL_0:def_1; end; 3 = (2 * 1) + 1 ; then Lm1: 3 is odd by ABIAN:1; theorem Th12: :: POLYEQ_1:12 for a, b, c, d, a9, b9, c9, d9 being real number st ( for x being real number holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ) holds ( a = a9 & b = b9 & c = c9 & d = d9 ) proof let a, b, c, d, a9, b9, c9, d9 be real number ; ::_thesis: ( ( for x being real number holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ) implies ( a = a9 & b = b9 & c = c9 & d = d9 ) ) (- 1) |^ 3 = - (1 |^ (2 + 1)) by Lm1, POWER:2 .= - ((1 |^ 2) * 1) by NEWTON:6 ; then A1: ( 0 |^ 3 = 0 & (- 1) |^ 3 = - 1 ) by NEWTON:10, NEWTON:11; A2: 2 |^ 1 = 2 to_power 1 by POWER:41 .= 2 by POWER:25 ; A3: 2 |^ 3 = 2 |^ (2 + 1) .= (2 |^ (1 + 1)) * 2 by NEWTON:6 .= ((2 |^ 1) * 2) * 2 by NEWTON:6 .= (2 |^ 1) * (2 * 2) ; assume A4: for x being real number holds Polynom (a,b,c,d,x) = Polynom (a9,b9,c9,d9,x) ; ::_thesis: ( a = a9 & b = b9 & c = c9 & d = d9 ) then A5: Polynom (a,b,c,d,2) = Polynom (a9,b9,c9,d9,2) ; Polynom (a,b,c,d,1) = Polynom (a9,b9,c9,d9,1) by A4; then (((a * 1) + (b * 1)) + (c * 1)) + d = Polynom (a9,b9,c9,d9,1) by NEWTON:10; then A6: ((a + b) + c) + d = (((a9 * 1) + (b9 * 1)) + (c9 * 1)) + d9 by NEWTON:10 .= ((a9 + b9) + c9) + d9 ; ( Polynom (a,b,c,d,0) = Polynom (a9,b9,c9,d9,0) & Polynom (a,b,c,d,(- 1)) = Polynom (a9,b9,c9,d9,(- 1)) ) by A4; hence ( a = a9 & b = b9 & c = c9 & d = d9 ) by A6, A1, A5, A3, A2; ::_thesis: verum end; definition let a, x, x1, x2, x3 be real number ; func Tri (a,x1,x2,x3,x) -> set equals :: POLYEQ_1:def 5 a * (((x - x1) * (x - x2)) * (x - x3)); coherence a * (((x - x1) * (x - x2)) * (x - x3)) is set ; end; :: deftheorem defines Tri POLYEQ_1:def_5_:_ for a, x, x1, x2, x3 being real number holds Tri (a,x1,x2,x3,x) = a * (((x - x1) * (x - x2)) * (x - x3)); registration let a, x, x1, x2, x3 be real number ; cluster Tri (a,x1,x2,x3,x) -> real ; coherence Tri (a,x1,x2,x3,x) is real ; end; definition let a, x, x1, x2, x3 be Real; :: original: Tri redefine func Tri (a,x1,x2,x3,x) -> Real; coherence Tri (a,x1,x2,x3,x) is Real by XREAL_0:def_1; end; theorem :: POLYEQ_1:13 for a, b, c, d, x1, x2, x3 being real number st a <> 0 & ( for x being real number holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ) holds ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) proof let a, b, c, d, x1, x2, x3 be real number ; ::_thesis: ( a <> 0 & ( for x being real number holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ) implies ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) ) assume A1: a <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) or ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) ) set t3 = d / a; set t2 = c / a; set t1 = b / a; set d9 = - ((x1 * x2) * x3); set c9 = ((x1 * x2) + (x2 * x3)) + (x1 * x3); set b9 = - ((x1 + x2) + x3); assume A2: for x being real number holds Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) ; ::_thesis: ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) now__::_thesis:_for_x_being_real_number_holds_Polynom_(1,(b_/_a),(c_/_a),(d_/_a),x)_=_Polynom_(1,(-_((x1_+_x2)_+_x3)),(((x1_*_x2)_+_(x2_*_x3))_+_(x1_*_x3)),(-_((x1_*_x2)_*_x3)),x) let x be real number ; ::_thesis: Polynom (1,(b / a),(c / a),(d / a),x) = Polynom (1,(- ((x1 + x2) + x3)),(((x1 * x2) + (x2 * x3)) + (x1 * x3)),(- ((x1 * x2) * x3)),x) set t = (((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d; set r8 = ((x - x1) * (x - x2)) * (x - x3); A3: x |^ 1 = x to_power 1 by POWER:41; x |^ 3 = x |^ (2 + 1) .= (x |^ (1 + 1)) * x by NEWTON:6 .= ((x |^ 1) * x) * x by NEWTON:6 ; then A4: x |^ 3 = (x * x) * x by A3, POWER:25; Polynom (a,b,c,d,x) = Tri (a,x1,x2,x3,x) by A2; then A5: ((((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d) / a = ((x - x1) * (x - x2)) * (x - x3) by A1, XCMPLX_1:89; (a ") * ((((a * (x |^ 3)) + (b * (x ^2))) + (c * x)) + d) = ((((a ") * a) * (x |^ 3)) + (((a ") * b) * (x ^2))) + ((a ") * ((c * x) + d)) .= ((1 * (x |^ 3)) + (((a ") * b) * (x ^2))) + ((((a ") * c) * x) + ((a ") * d)) by A1, XCMPLX_0:def_7 .= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + ((((a ") * c) * x) + ((a ") * d)) by XCMPLX_0:def_9 .= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + (((c / a) * x) + ((a ") * d)) by XCMPLX_0:def_9 .= ((1 * (x |^ 3)) + ((b / a) * (x ^2))) + (((c / a) * x) + (d / a)) by XCMPLX_0:def_9 .= Polynom (1,(b / a),(c / a),(d / a),x) ; hence Polynom (1,(b / a),(c / a),(d / a),x) = Polynom (1,(- ((x1 + x2) + x3)),(((x1 * x2) + (x2 * x3)) + (x1 * x3)),(- ((x1 * x2) * x3)),x) by A5, A4, XCMPLX_0:def_9; ::_thesis: verum end; hence ( b / a = - ((x1 + x2) + x3) & c / a = ((x1 * x2) + (x2 * x3)) + (x1 * x3) & d / a = - ((x1 * x2) * x3) ) by Th12; ::_thesis: verum end; theorem Th14: :: POLYEQ_1:14 for y, h being real number holds (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3) proof let y, h be real number ; ::_thesis: (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3) (y + h) |^ 3 = (y + h) |^ (2 + 1) ; then A1: (y + h) |^ 3 = ((y + h) |^ (1 + 1)) * (y + h) by NEWTON:6 .= (((y + h) |^ 1) * (y + h)) * (y + h) by NEWTON:6 .= ((y + h) |^ 1) * ((y + h) ^2) .= ((y + h) to_power 1) * (((y ^2) + ((2 * y) * h)) + (h ^2)) by POWER:41 .= (y + h) * (((y ^2) + ((2 * y) * h)) + (h ^2)) by POWER:25 .= ((y * (y ^2)) + (((3 * h) * (y ^2)) + (((2 + 1) * (h ^2)) * y))) + (h * (h ^2)) ; y |^ 3 = y |^ (2 + 1) .= (y |^ (1 + 1)) * y by NEWTON:6 .= ((y |^ 1) * y) * y by NEWTON:6 .= (y |^ 1) * (y ^2) ; then A2: y |^ 3 = (y to_power 1) * (y ^2) by POWER:41; h |^ 3 = h |^ (2 + 1) .= (h |^ (1 + 1)) * h by NEWTON:6 .= ((h |^ 1) * h) * h by NEWTON:6 .= (h |^ 1) * (h ^2) .= (h to_power 1) * (h ^2) by POWER:41 .= h * (h ^2) by POWER:25 ; hence (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3) by A1, A2, POWER:25; ::_thesis: verum end; theorem Th15: :: POLYEQ_1:15 for a, b, c, d, x being real number st a <> 0 & Polynom (a,b,c,d,x) = 0 holds for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 proof let a, b, c, d, x be real number ; ::_thesis: ( a <> 0 & Polynom (a,b,c,d,x) = 0 implies for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 ) assume A1: a <> 0 ; ::_thesis: ( not Polynom (a,b,c,d,x) = 0 or for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 ) assume A2: Polynom (a,b,c,d,x) = 0 ; ::_thesis: for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 let a1, a2, a3, h, y be real number ; ::_thesis: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a implies ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 ) assume that A3: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) ) and A4: ( a1 = b / a & a2 = c / a & a3 = d / a ) ; ::_thesis: ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 0 = (a ") * (((a * (x |^ 3)) + (b * (x ^2))) + ((c * x) + d)) by A2 .= ((((a ") * a) * (x |^ 3)) + ((a ") * (b * (x ^2)))) + ((a ") * ((c * x) + d)) .= ((1 * (x |^ 3)) + ((a ") * (b * (x ^2)))) + ((a ") * ((c * x) + d)) by A1, XCMPLX_0:def_7 .= (((x |^ 3) + (((a ") * b) * (x ^2))) + (((a ") * c) * x)) + ((a ") * d) .= (((x |^ 3) + ((b / a) * (x ^2))) + (((a ") * c) * x)) + ((a ") * d) by XCMPLX_0:def_9 .= (((x |^ 3) + ((b / a) * (x ^2))) + ((c / a) * x)) + ((a ") * d) by XCMPLX_0:def_9 .= (((x |^ 3) + (a1 * (x ^2))) + (a2 * x)) + a3 by A4, XCMPLX_0:def_9 ; then 0 = (((((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3)) + (((a1 * (y ^2)) + ((2 * (a1 * h)) * y)) + (a1 * (h ^2)))) + (a2 * (y + h))) + a3 by A3, Th14 .= (((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (((2 * (a1 * h)) * y) + (a1 * (y ^2)))) + ((a2 * y) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3))) ; hence ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 ; ::_thesis: verum end; theorem :: POLYEQ_1:16 for a, b, c, d, x being real number st a <> 0 & Polynom (a,b,c,d,x) = 0 holds for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 proof let a, b, c, d, x be real number ; ::_thesis: ( a <> 0 & Polynom (a,b,c,d,x) = 0 implies for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 ) assume A1: a <> 0 ; ::_thesis: ( not Polynom (a,b,c,d,x) = 0 or for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 ) then A2: 3 * a <> 0 ; assume A3: Polynom (a,b,c,d,x) = 0 ; ::_thesis: for a1, a2, a3, h, y being real number st y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a holds (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 let a1, a2, a3, h, y be real number ; ::_thesis: ( y = x + (b / (3 * a)) & h = - (b / (3 * a)) & a1 = b / a & a2 = c / a & a3 = d / a implies (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 ) assume that A4: y = x + (b / (3 * a)) and A5: h = - (b / (3 * a)) and A6: a1 = b / a and A7: a2 = c / a and A8: a3 = d / a ; ::_thesis: (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 set p0 = (3 * h) + a1; A9: (3 * h) + a1 = (- (3 * (b / (3 * a)))) + a1 by A5 .= (- (3 * (((3 * a) ") * b))) + a1 by XCMPLX_0:def_9 .= (- (3 * (((3 ") * (a ")) * b))) + a1 by XCMPLX_1:204 .= (- (((3 * (3 ")) * (a ")) * b)) + a1 .= (- (b / a)) + a1 by XCMPLX_0:def_9 ; set q2 = ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3); A10: ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3) = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) proof set t = 3 * a; set a6 = b / (3 * a); A11: b / a = (3 * b) / (3 * a) by XCMPLX_1:91; A12: (b / (3 * a)) |^ 3 = (b / (3 * a)) |^ (2 + 1) .= ((b / (3 * a)) |^ (1 + 1)) * (b / (3 * a)) by NEWTON:6 .= (((b / (3 * a)) |^ 1) * (b / (3 * a))) * (b / (3 * a)) by NEWTON:6 .= ((b / (3 * a)) |^ 1) * ((b / (3 * a)) ^2) .= ((b / (3 * a)) to_power 1) * ((b / (3 * a)) ^2) by POWER:41 ; ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3) = (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((c / a) * (b / (3 * a)))) + (d / a)) by A5, A6, A7, A8 .= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((b * c) / ((3 * a) * a))) + (d / a)) by XCMPLX_1:76 .= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((b * c) / (3 * (a ^2)))) + (1 * (d / a))) .= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((- ((b * c) / (3 * (a ^2)))) + (((3 * a) / (3 * a)) * (d / a))) by A2, XCMPLX_1:60 .= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + (((3 * a) / (3 * a)) * (d / a))) - ((b * c) / (3 * (a ^2))) .= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + (((3 * a) * d) / ((3 * a) * a))) - ((b * c) / (3 * (a ^2))) by XCMPLX_1:76 .= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + (((3 * a) * d) * ((3 * (a ^2)) "))) - ((b * c) / (3 * (a ^2))) by XCMPLX_0:def_9 .= ((((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + (((3 * a) * d) * ((3 * (a ^2)) "))) - ((b * c) * ((3 * (a ^2)) ")) by XCMPLX_0:def_9 .= (((- (b / (3 * a))) |^ 3) + ((b / a) * ((- (b / (3 * a))) ^2))) + ((((3 * a) * d) - (b * c)) * ((3 * (a ^2)) ")) .= (((- (b / (3 * a))) |^ (2 + 1)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_0:def_9 .= ((((- (b / (3 * a))) |^ (1 + 1)) * (- (b / (3 * a)))) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by NEWTON:6 .= (((((- (b / (3 * a))) |^ 1) * (- (b / (3 * a)))) * (- (b / (3 * a)))) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by NEWTON:6 .= ((((- (b / (3 * a))) |^ 1) * ((- (b / (3 * a))) ^2)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) .= ((((- (b / (3 * a))) to_power 1) * ((- (b / (3 * a))) ^2)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by POWER:41 .= (((- (b / (3 * a))) * ((b / (3 * a)) ^2)) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by POWER:25 .= (((- (b / (3 * a))) * ((b ^2) / ((3 * a) ^2))) + ((b / a) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_1:76 .= (((- (b / (3 * a))) * ((b ^2) / ((3 * a) ^2))) + ((b / a) * ((b ^2) / ((3 * a) ^2)))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_1:76 .= (((b / a) - (b / (3 * a))) * ((b ^2) / ((3 * a) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) .= ((((3 * b) * ((3 * a) ")) - ((1 * b) / (3 * a))) * ((b ^2) / ((3 * a) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by A11, XCMPLX_0:def_9 .= ((((3 * b) * ((3 * a) ")) - ((1 * b) * ((3 * a) "))) * ((b ^2) / ((3 * a) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_0:def_9 .= (2 * ((b * ((3 * a) ")) * ((b ^2) / ((3 * a) ^2)))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) .= (2 * ((b / (3 * a)) * ((b ^2) / ((3 * a) ^2)))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_0:def_9 .= (2 * ((b / (3 * a)) * ((b / (3 * a)) ^2))) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by XCMPLX_1:76 ; hence ((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3) = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) by A12, POWER:25; ::_thesis: verum end; set p2 = ((3 * (h ^2)) + (2 * (a1 * h))) + a2; A13: ((3 * (h ^2)) + (2 * (a1 * h))) + a2 = (((3 * a) * c) - (b ^2)) / (3 * (a ^2)) proof set t = ((3 * a) ") * b; A14: (3 * a) / (3 * a) = 1 by A2, XCMPLX_1:60; ((3 * (h ^2)) + (2 * (a1 * h))) + a2 = ((3 * ((b / (3 * a)) ^2)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by A5 .= ((3 * ((((3 * a) ") * b) ^2)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def_9 .= ((((3 * ((3 * a) ")) * b) * (((3 * a) ") * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 .= ((((3 * ((3 ") * (a "))) * b) * (((3 * a) ") * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_1:204 .= (((b / a) * (((3 * a) ") * b)) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def_9 .= (((b / a) * (b / (3 * a))) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_0:def_9 .= (((b * b) / (a * (3 * a))) + (2 * (a1 * (- (b / (3 * a)))))) + a2 by XCMPLX_1:76 .= (((b ^2) / (3 * (a ^2))) - (2 * ((b / a) * (b / (3 * a))))) + (c / a) by A6, A7 .= (((b ^2) / (3 * (a ^2))) - (2 * ((b * b) / (a * (3 * a))))) + (c / a) by XCMPLX_1:76 .= (- ((b ^2) / (3 * (a ^2)))) + (((3 * a) / (3 * a)) * (c / a)) by A14 .= (- ((b ^2) / (3 * (a ^2)))) + (((3 * a) * c) / ((3 * a) * a)) by XCMPLX_1:76 .= (((3 * a) * c) / (3 * (a ^2))) - ((b ^2) / (3 * (a ^2))) .= (((3 * a) * c) * ((3 * (a ^2)) ")) - ((b ^2) / (3 * (a ^2))) by XCMPLX_0:def_9 .= (((3 * a) * c) * ((3 * (a ^2)) ")) - ((b ^2) * ((3 * (a ^2)) ")) by XCMPLX_0:def_9 .= (((3 * a) * c) - (b ^2)) * ((3 * (a ^2)) ") ; hence ((3 * (h ^2)) + (2 * (a1 * h))) + a2 = (((3 * a) * c) - (b ^2)) / (3 * (a ^2)) by XCMPLX_0:def_9; ::_thesis: verum end; ((y |^ 3) + ((((3 * h) + a1) * (y ^2)) + ((((3 * (h ^2)) + (2 * (a1 * h))) + a2) * y))) + (((h |^ 3) + (a1 * (h ^2))) + ((a2 * h) + a3)) = 0 by A1, A3, A4, A5, A6, A7, A8, Th15; hence (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 by A6, A9, A13, A10; ::_thesis: verum end; theorem :: POLYEQ_1:17 for y, a, c, b, d being real number st (((y |^ 3) + (0 * (y ^2))) + (((((3 * a) * c) - (b ^2)) / (3 * (a ^2))) * y)) + ((2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2)))) = 0 holds for p, q being real number st p = (((3 * a) * c) - (b ^2)) / (3 * (a ^2)) & q = (2 * ((b / (3 * a)) |^ 3)) + ((((3 * a) * d) - (b * c)) / (3 * (a ^2))) holds Polynom (1,0,p,q,y) = 0 ; theorem Th18: :: POLYEQ_1:18 for p, q, y being real number st Polynom (1,0,p,q,y) = 0 holds for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 holds ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) proof let p, q, y be real number ; ::_thesis: ( Polynom (1,0,p,q,y) = 0 implies for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 holds ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) ) assume A1: Polynom (1,0,p,q,y) = 0 ; ::_thesis: for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 holds ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) let u, v be real number ; ::_thesis: ( y = u + v & ((3 * v) * u) + p = 0 implies ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) ) assume that A2: y = u + v and A3: ((3 * v) * u) + p = 0 ; ::_thesis: ( (u |^ 3) + (v |^ 3) = - q & (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 ) (u + v) |^ 3 = ((u |^ 3) + (((3 * v) * (u ^2)) + ((3 * (v ^2)) * u))) + (v |^ 3) by Th14 .= ((u |^ 3) + (((3 * v) * u) * (u + v))) + (v |^ 3) ; then 0 = (((u |^ 3) + (v |^ 3)) + ((((3 * v) * u) + p) * (u + v))) + q by A1, A2; hence (u |^ 3) + (v |^ 3) = - q by A3; ::_thesis: (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 3 * (v * u) = - p by A3; hence (u |^ 3) * (v |^ 3) = (- (p / 3)) |^ 3 by NEWTON:7; ::_thesis: verum end; theorem Th19: :: POLYEQ_1:19 for p, q, y being real number st Polynom (1,0,p,q,y) = 0 holds for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) holds y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) proof let p, q, y be real number ; ::_thesis: ( Polynom (1,0,p,q,y) = 0 implies for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) holds y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) set e1 = 1; assume A1: Polynom (1,0,p,q,y) = 0 ; ::_thesis: for u, v being real number st y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) holds y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) set e3 = (- (p / 3)) |^ 3; set e2 = q; let u, v be real number ; ::_thesis: ( y = u + v & ((3 * v) * u) + p = 0 & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) & not y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) implies y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) assume that A2: y = u + v and A3: ((3 * v) * u) + p = 0 ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) set z2 = v |^ 3; set z1 = u |^ 3; A4: now__::_thesis:_for_z_being_real_number_holds_(z_-_(u_|^_3))_*_(z_-_(v_|^_3))_=_((z_^2)_+_(q_*_z))_+_((-_(p_/_3))_|^_3) let z be real number ; ::_thesis: (z - (u |^ 3)) * (z - (v |^ 3)) = ((z ^2) + (q * z)) + ((- (p / 3)) |^ 3) thus (z - (u |^ 3)) * (z - (v |^ 3)) = ((z ^2) - (((u |^ 3) + (v |^ 3)) * z)) + ((u |^ 3) * (v |^ 3)) .= ((z ^2) - ((- q) * z)) + ((u |^ 3) * (v |^ 3)) by A1, A2, A3, Th18 .= ((z ^2) + (q * z)) + ((- (p / 3)) |^ 3) by A1, A2, A3, Th18 ; ::_thesis: verum end; A5: (u |^ 3) + (v |^ 3) = - q by A1, A2, A3, Th18; then q ^2 = ((u |^ 3) + (v |^ 3)) ^2 by SQUARE_1:3; then A6: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) = (- (- ((((u |^ 3) ^2) + ((2 * (u |^ 3)) * (v |^ 3))) + ((v |^ 3) ^2)))) - (4 * ((u |^ 3) * (v |^ 3))) by A1, A2, A3, Th18 .= ((u |^ 3) - (v |^ 3)) ^2 ; then A7: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) >= 0 by XREAL_1:63; then A8: delta (1,q,((- (p / 3)) |^ 3)) >= 0 by QUIN_1:def_1; ((u |^ 3) - (u |^ 3)) * ((u |^ 3) - (v |^ 3)) = 0 * ((u |^ 3) - (v |^ 3)) ; then A9: Polynom (1,q,((- (p / 3)) |^ 3),(u |^ 3)) = 0 by A4; ((v |^ 3) - (u |^ 3)) * ((v |^ 3) - (v |^ 3)) = ((v |^ 3) - (u |^ 3)) * 0 ; then A10: Polynom (1,q,((- (p / 3)) |^ 3),(v |^ 3)) = 0 by A4; A11: (v |^ 3) * (u |^ 3) = (- (p / 3)) |^ 3 by A1, A2, A3, Th18; now__::_thesis:_(_(_u_|^_3_=_((-_q)_+_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_or_(_u_|^_3_=_((-_q)_-_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_u_|^_3_=_(-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_-_((-_(p_/_3))_|^_3)))_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_) percases ( u |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or u |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A9, A8, Th5; caseA12: u |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) A13: (p / 3) |^ 3 = (p / 3) |^ (2 + 1) .= ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6 .= (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6 .= ((p / 3) |^ 1) * ((p / 3) ^2) .= ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41 .= (p / 3) * ((p / 3) ^2) by POWER:25 ; A14: (q ^2) - (4 * ((- (p / 3)) |^ 3)) >= 0 by A6, XREAL_1:63; A15: (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) .= ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6 .= (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6 .= ((- (p / 3)) |^ 1) * ((- (p / 3)) ^2) ; then A16: (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41 .= (- (p / 3)) * ((p / 3) ^2) by POWER:25 .= - ((p / 3) * ((p / 3) ^2)) ; A17: u |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A12, QUIN_1:def_1 .= ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62 .= ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A14, SQUARE_1:30 .= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ; A18: now__::_thesis:_(_(_u_>_0_&_u_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_u_=_0_&_u_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_u_<_0_&_u_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_) percases ( u > 0 or u = 0 or u < 0 ) by XXREAL_0:1; caseA19: u > 0 ; ::_thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A20: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A17, A16, A13, PREPOWER:6; then u = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A17, A16, A13, A19, PREPOWER:def_2; hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A20, POWER:def_1; ::_thesis: verum end; caseA21: u = 0 ; ::_thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A22: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A17, A16, A13, NEWTON:11; then 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) = 0 by PREPOWER:def_2; hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A21, A22, POWER:def_1; ::_thesis: verum end; case u < 0 ; ::_thesis: u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A23: - u > 0 by XREAL_1:58; set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))); A24: 3 -root (- 1) = - 1 by Lm1, POWER:8; (- u) |^ 3 = (- u) |^ (2 + 1) .= ((- u) |^ (1 + 1)) * (- u) by NEWTON:6 .= (((- u) |^ 1) * (- u)) * (- u) by NEWTON:6 .= ((- u) |^ 1) * ((- u) ^2) ; then (- u) |^ 3 = ((- u) to_power 1) * ((- u) ^2) by POWER:41; then A25: (- u) |^ 3 = (- u) * (u ^2) by POWER:25 .= - (u * (u ^2)) ; u |^ 3 = u |^ (2 + 1) .= (u |^ (1 + 1)) * u by NEWTON:6 .= ((u |^ 1) * u) * u by NEWTON:6 .= (u |^ 1) * (u * u) ; then A26: u |^ 3 = (u to_power 1) * (u ^2) by POWER:41; then A27: (- u) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A17, A16, A13, A25, POWER:25; A28: (- u) |^ 3 = - (u |^ 3) by A25, A26, POWER:25; then A29: - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A17, A16, A13, A23, PREPOWER:6; - (u |^ 3) > 0 by A23, A28, PREPOWER:6; then - u = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A17, A16, A13, A23, A27, PREPOWER:def_2; then - u = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A29, POWER:def_1; then - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11; hence u = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A24; ::_thesis: verum end; end; end; now__::_thesis:_(_(_v_|^_3_=_((-_q)_+_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_or_(_v_|^_3_=_((-_q)_-_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_) percases ( v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A8, A10, Th5; case v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) then v |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by QUIN_1:def_1; then v |^ 3 = ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62; then A30: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:30 .= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ; A31: (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by A15, POWER:41 .= (- (p / 3)) * ((p / 3) ^2) by POWER:25 ; now__::_thesis:_(_(_v_>_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_=_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_<_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_) percases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1; caseA32: v > 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A33: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A13, A30, A31, PREPOWER:6; then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A13, A30, A31, A32, PREPOWER:def_2; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A33, POWER:def_1; ::_thesis: verum end; caseA34: v = 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A13, A30, A31, NEWTON:11; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A34, POWER:5; ::_thesis: verum end; case v < 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A35: - v > 0 by XREAL_1:58; then A36: (- v) |^ 3 > 0 by PREPOWER:6; (- v) |^ 3 = (- v) |^ (2 + 1) ; then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6; then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6; then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ; then (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41; then (- v) |^ 3 = (- v) * ((- v) ^2) by POWER:25; then A37: (- v) |^ 3 = - (v * (v ^2)) ; v |^ 3 = v |^ (2 + 1) ; then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6; then v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6; then v |^ 3 = (v |^ 1) * (v * v) ; then A38: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41; then (- v) |^ 3 = - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A13, A30, A31, A37, POWER:25; then A39: - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A35, A36, PREPOWER:def_2; set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))); A40: 3 -root (- 1) = - 1 by Lm1, POWER:8; - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A13, A30, A31, A36, A37, A38, POWER:25; then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A39, POWER:def_1; then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A40; ::_thesis: verum end; end; end; hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A18; ::_thesis: verum end; case v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) then v |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by QUIN_1:def_1; then v |^ 3 = ((- q) / 2) - ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / 2) ; then A41: v |^ 3 = (- (q / 2)) - (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:20, SQUARE_1:30 .= (- (q / 2)) - (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ; now__::_thesis:_(_(_v_>_0_&_v_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_=_0_&_v_=_3_-Root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_&_v_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_<_0_&_v_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_) percases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1; caseA42: v > 0 ; ::_thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A16, A13, A41, PREPOWER:6; then A43: v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A16, A13, A41, A42, PREPOWER:def_2; (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A16, A13, A41, A42, PREPOWER:6; hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A43, POWER:def_1; ::_thesis: verum end; caseA44: v = 0 ; ::_thesis: ( v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) & v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) ) then A45: (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A16, A13, A41, NEWTON:11; hence v = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A44, PREPOWER:def_2; ::_thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A45, POWER:def_1; ::_thesis: verum end; case v < 0 ; ::_thesis: v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A46: - v > 0 by XREAL_1:58; set r = (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))); A47: 3 -root (- 1) = - 1 by Lm1, POWER:8; v |^ 3 = v |^ (2 + 1) ; then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6; then A48: v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6; (- v) |^ 3 = (- v) |^ (2 + 1) ; then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6; then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6; then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ; then A49: (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41 .= (- v) * (v ^2) by POWER:25 .= - (v * (v ^2)) ; A50: v to_power 1 = v by POWER:25; then (- v) |^ 3 = - (v |^ 3) by A49, A48, POWER:41; then A51: - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A16, A13, A41, A46, PREPOWER:6; (- v) |^ 3 = - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A16, A13, A41, A49, A48, A50, POWER:41; then - v = 3 -Root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A46, A51, PREPOWER:def_2; then - v = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A51, POWER:def_1; then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11; hence v = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A47; ::_thesis: verum end; end; end; hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A18; ::_thesis: verum end; end; end; hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; ::_thesis: verum end; caseA52: u |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( u |^ 3 = (- (q / 2)) - (sqrt (((q ^2) / 4) - ((- (p / 3)) |^ 3))) & ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ) (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) ; then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6; then (- (p / 3)) |^ 3 = (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6; then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ; then (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41; then (- (p / 3)) |^ 3 = (- (p / 3)) * ((- (p / 3)) ^2) by POWER:25; then A53: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ; u |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A52, QUIN_1:def_1; then A54: u |^ 3 = ((- q) * (2 ")) - ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / 2) .= (- (q / 2)) - (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:20, SQUARE_1:30 .= (- (q / 2)) - (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ; hence u |^ 3 = (- (q / 2)) - (sqrt (((q ^2) / 4) - ((- (p / 3)) |^ 3))) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) (p / 3) |^ 3 = (p / 3) |^ (2 + 1) ; then (p / 3) |^ 3 = ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6; then (p / 3) |^ 3 = (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6; then (p / 3) |^ 3 = ((p / 3) |^ 1) * ((p / 3) * (p / 3)) ; then (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41; then A55: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A53, POWER:25; A56: now__::_thesis:_(_(_u_>_0_&_u_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_u_=_0_&_u_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_u_<_0_&_u_=_3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_) percases ( u > 0 or u = 0 or u < 0 ) by XXREAL_0:1; caseA57: u > 0 ; ::_thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A54, A55, PREPOWER:6; then A58: u = 3 -Root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A54, A55, A57, PREPOWER:def_2; (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A54, A55, A57, PREPOWER:6; hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A58, POWER:def_1; ::_thesis: verum end; caseA59: u = 0 ; ::_thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A54, A55, NEWTON:11; hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A59, POWER:5; ::_thesis: verum end; case u < 0 ; ::_thesis: u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A60: - u > 0 by XREAL_1:58; then A61: (- u) |^ 3 > 0 by PREPOWER:6; (- u) |^ 3 = (- u) |^ (2 + 1) ; then (- u) |^ 3 = ((- u) |^ (1 + 1)) * (- u) by NEWTON:6; then (- u) |^ 3 = (((- u) |^ 1) * (- u)) * (- u) by NEWTON:6; then (- u) |^ 3 = ((- u) |^ 1) * ((- u) * (- u)) ; then (- u) |^ 3 = ((- u) to_power 1) * ((- u) ^2) by POWER:41; then (- u) |^ 3 = (- u) * ((- u) ^2) by POWER:25; then A62: (- u) |^ 3 = - (u * (u ^2)) ; u |^ 3 = u |^ (2 + 1) ; then u |^ 3 = (u |^ (1 + 1)) * u by NEWTON:6; then u |^ 3 = ((u |^ 1) * u) * u by NEWTON:6; then u |^ 3 = (u |^ 1) * (u * u) ; then A63: u |^ 3 = (u to_power 1) * (u ^2) by POWER:41; then - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A54, A55, A61, A62, POWER:25; then A64: 3 -Root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) = 3 -root (- ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by POWER:def_1; set r = (- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))); (- u) |^ 3 = - ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A54, A55, A62, A63, POWER:25; then - u = 3 -root ((- 1) * ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A60, A61, A64, PREPOWER:def_2; then A65: - u = (3 -root (- 1)) * (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11; 3 -root (- 1) = - 1 by Lm1, POWER:8; hence u = 3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A65; ::_thesis: verum end; end; end; now__::_thesis:_(_(_v_|^_3_=_((-_q)_+_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_(_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_or_y_=_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_)_or_(_v_|^_3_=_((-_q)_-_(sqrt_(delta_(1,q,((-_(p_/_3))_|^_3)))))_/_(2_*_1)_&_y_=_(3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_+_(3_-root_((-_(q_/_2))_-_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3)))))_)_) percases ( v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) or v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ) by A8, A10, Th5; caseA66: v |^ 3 = ((- q) + (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) ; then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6; then (- (p / 3)) |^ 3 = (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6; then (- (p / 3)) |^ 3 = ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ; then (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41; then (- (p / 3)) |^ 3 = (- (p / 3)) * ((- (p / 3)) ^2) by POWER:25; then A67: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ; (p / 3) |^ 3 = (p / 3) |^ (2 + 1) ; then (p / 3) |^ 3 = ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6; then (p / 3) |^ 3 = (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6; then (p / 3) |^ 3 = ((p / 3) |^ 1) * ((p / 3) * (p / 3)) ; then (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41; then A68: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A67, POWER:25; v |^ 3 = ((- q) + (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A66, QUIN_1:def_1; then v |^ 3 = ((- q) / 2) + ((sqrt ((q ^2) - (4 * ((- (p / 3)) |^ 3)))) / (sqrt 4)) by SQUARE_1:20, XCMPLX_1:62; then A69: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A7, SQUARE_1:30 .= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ; now__::_thesis:_(_(_v_>_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_=_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_<_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_) percases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1; caseA70: v > 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A71: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A69, A68, PREPOWER:6; then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A69, A68, A70, PREPOWER:def_2; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A71, POWER:def_1; ::_thesis: verum end; caseA72: v = 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) = 0 by A69, A68, NEWTON:11; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A72, POWER:5; ::_thesis: verum end; case v < 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A73: - v > 0 by XREAL_1:58; then A74: (- v) |^ 3 > 0 by PREPOWER:6; (- v) |^ 3 = (- v) |^ (2 + 1) ; then (- v) |^ 3 = ((- v) |^ (1 + 1)) * (- v) by NEWTON:6; then (- v) |^ 3 = (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6; then (- v) |^ 3 = ((- v) |^ 1) * ((- v) * (- v)) ; then (- v) |^ 3 = ((- v) to_power 1) * ((- v) ^2) by POWER:41; then (- v) |^ 3 = (- v) * ((- v) ^2) by POWER:25; then A75: (- v) |^ 3 = - (v * (v ^2)) ; v |^ 3 = v |^ (2 + 1) ; then v |^ 3 = (v |^ (1 + 1)) * v by NEWTON:6; then v |^ 3 = ((v |^ 1) * v) * v by NEWTON:6; then v |^ 3 = (v |^ 1) * (v * v) ; then A76: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41; then A77: - ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) > 0 by A69, A68, A74, A75, POWER:25; set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))); A78: 3 -root (- 1) = - 1 by Lm1, POWER:8; v |^ 3 = v * (v ^2) by A76, POWER:25; then - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A69, A68, A73, A74, A75, PREPOWER:def_2; then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A77, POWER:def_1; then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A78; ::_thesis: verum end; end; end; hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) by A2, A56; ::_thesis: verum end; caseA79: v |^ 3 = ((- q) - (sqrt (delta (1,q,((- (p / 3)) |^ 3))))) / (2 * 1) ; ::_thesis: y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) q ^2 = ((u |^ 3) + (v |^ 3)) ^2 by A5, SQUARE_1:3; then A80: (q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3)) = ((u |^ 3) - (v |^ 3)) ^2 by A11; (- (p / 3)) |^ 3 = (- (p / 3)) |^ (2 + 1) .= ((- (p / 3)) |^ (1 + 1)) * (- (p / 3)) by NEWTON:6 .= (((- (p / 3)) |^ 1) * (- (p / 3))) * (- (p / 3)) by NEWTON:6 .= ((- (p / 3)) |^ 1) * ((- (p / 3)) * (- (p / 3))) ; then (- (p / 3)) |^ 3 = ((- (p / 3)) to_power 1) * ((- (p / 3)) ^2) by POWER:41 .= (- (p / 3)) * ((p / 3) ^2) by POWER:25 ; then A81: (- (p / 3)) |^ 3 = - ((p / 3) * ((p / 3) ^2)) ; (p / 3) |^ 3 = (p / 3) |^ (2 + 1) .= ((p / 3) |^ (1 + 1)) * (p / 3) by NEWTON:6 .= (((p / 3) |^ 1) * (p / 3)) * (p / 3) by NEWTON:6 .= ((p / 3) |^ 1) * ((p / 3) ^2) ; then (p / 3) |^ 3 = ((p / 3) to_power 1) * ((p / 3) ^2) by POWER:41; then A82: (- (p / 3)) |^ 3 = - ((p / 3) |^ 3) by A81, POWER:25; v |^ 3 = ((- q) - (sqrt ((q ^2) - ((4 * 1) * ((- (p / 3)) |^ 3))))) / (2 * 1) by A79, QUIN_1:def_1; then A83: v |^ 3 = ((- q) / 2) + (sqrt (((q ^2) - (4 * ((- (p / 3)) |^ 3))) / 4)) by A52, A79, A80, SQUARE_1:17 .= ((- q) / 2) + (sqrt (((q ^2) / 4) - (1 * ((- (p / 3)) |^ 3)))) ; now__::_thesis:_(_(_v_>_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_=_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_or_(_v_<_0_&_v_=_3_-root_((-_(q_/_2))_+_(sqrt_(((q_^2)_/_4)_+_((p_/_3)_|^_3))))_)_) percases ( v > 0 or v = 0 or v < 0 ) by XXREAL_0:1; caseA84: v > 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A85: (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))) > 0 by A83, A82, PREPOWER:6; then v = 3 -Root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A83, A82, A84, PREPOWER:def_2; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A85, POWER:def_1; ::_thesis: verum end; caseA86: v = 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then v |^ 3 = 0 by NEWTON:11; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A83, A82, A86, POWER:5; ::_thesis: verum end; case v < 0 ; ::_thesis: v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) then A87: - v > 0 by XREAL_1:58; then A88: (- v) |^ 3 > 0 by PREPOWER:6; set r = (- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))); v |^ 3 = v |^ (2 + 1) .= (v |^ (1 + 1)) * v by NEWTON:6 .= ((v |^ 1) * v) * v by NEWTON:6 .= (v |^ 1) * (v ^2) ; then A89: v |^ 3 = (v to_power 1) * (v ^2) by POWER:41; (- v) |^ 3 = (- v) |^ (2 + 1) .= ((- v) |^ (1 + 1)) * (- v) by NEWTON:6 .= (((- v) |^ 1) * (- v)) * (- v) by NEWTON:6 .= ((- v) |^ 1) * ((- v) ^2) .= ((- v) to_power 1) * ((- v) ^2) by POWER:41 .= (- v) * (v ^2) by POWER:25 ; then A90: (- v) |^ 3 = - (v * (v ^2)) ; then A91: - (v |^ 3) > 0 by A88, A89, POWER:25; A92: 3 -root (- 1) = - 1 by Lm1, POWER:8; (- v) |^ 3 = - (v |^ 3) by A90, A89, POWER:25; then - v = 3 -Root (- ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A83, A82, A87, A88, PREPOWER:def_2; then - v = 3 -root ((- 1) * ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A83, A82, A91, POWER:def_1; then - v = (3 -root (- 1)) * (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by Lm1, POWER:11; hence v = 3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3)))) by A92; ::_thesis: verum end; end; end; hence y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) by A2, A56; ::_thesis: verum end; end; end; hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; ::_thesis: verum end; end; end; hence ( y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) + (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) or y = (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) + (3 -root ((- (q / 2)) - (sqrt (((q ^2) / 4) + ((p / 3) |^ 3))))) ) ; ::_thesis: verum end; theorem :: POLYEQ_1:20 for b, c, d, x being real number st b <> 0 & delta (b,c,d) > 0 & Polynom (0,b,c,d,x) = 0 & not x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) holds x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) proof let b, c, d, x be real number ; ::_thesis: ( b <> 0 & delta (b,c,d) > 0 & Polynom (0,b,c,d,x) = 0 & not x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) implies x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) ) assume A1: ( b <> 0 & delta (b,c,d) > 0 ) ; ::_thesis: ( not Polynom (0,b,c,d,x) = 0 or x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) ) assume Polynom (0,b,c,d,x) = 0 ; ::_thesis: ( x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) ) then Polynom (b,c,d,x) = 0 ; hence ( x = ((- c) + (sqrt (delta (b,c,d)))) / (2 * b) or x = ((- c) - (sqrt (delta (b,c,d)))) / (2 * b) ) by A1, Th5; ::_thesis: verum end; theorem :: POLYEQ_1:21 for a, p, c, q, d, x being real number st a <> 0 & p = c / a & q = d / a & Polynom (a,0,c,d,x) = 0 holds for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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 x = (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, p, c, q, d, x be real number ; ::_thesis: ( a <> 0 & p = c / a & q = d / a & Polynom (a,0,c,d,x) = 0 implies for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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 x = (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 that A1: a <> 0 and A2: p = c / a and A3: q = d / a ; ::_thesis: ( not Polynom (a,0,c,d,x) = 0 or for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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 x = (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: ( p / 3 = c / (3 * a) & - (q / 2) = - (d / (2 * a)) ) by A2, A3, XCMPLX_1:78; assume Polynom (a,0,c,d,x) = 0 ; ::_thesis: for u, v being real number st x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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 x = (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))))) then (a ") * (((a * (x |^ 3)) + (c * x)) + d) = 0 ; then (((a ") * a) * (x |^ 3)) + ((a ") * ((c * x) + d)) = 0 ; then (1 * (x |^ 3)) + ((a ") * ((c * x) + d)) = 0 by A1, XCMPLX_0:def_7; then (x |^ 3) + ((((a ") * c) * x) + ((a ") * d)) = 0 ; then (x |^ 3) + (((c / a) * x) + ((a ") * d)) = 0 by XCMPLX_0:def_9; then (x |^ 3) + (((c / a) * x) + (d / a)) = 0 by XCMPLX_0:def_9; then A5: Polynom (1,0,p,q,x) = 0 by A2, A3; (q ^2) / 4 = ((d ^2) / (a ^2)) / 4 by A3, XCMPLX_1:76; then A6: (q ^2) / 4 = (d ^2) / (4 * (a ^2)) by XCMPLX_1:78; let u, v be real number ; ::_thesis: ( x = u + v & ((3 * v) * u) + p = 0 & not x = (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 x = (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 x = (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 ( x = u + v & ((3 * v) * u) + p = 0 ) ; ::_thesis: ( x = (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 x = (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 x = (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))))) ) hence ( x = (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 x = (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 x = (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 A5, A4, A6, Th19; ::_thesis: verum end; theorem :: POLYEQ_1:22 for a, b, c, x being real number st a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,0,x) = 0 & not x = 0 & not x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) holds x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) proof let a, b, c, x be real number ; ::_thesis: ( a <> 0 & delta (a,b,c) >= 0 & Polynom (a,b,c,0,x) = 0 & not x = 0 & not x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) implies x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) assume A1: ( a <> 0 & delta (a,b,c) >= 0 ) ; ::_thesis: ( not Polynom (a,b,c,0,x) = 0 or x = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) x |^ 3 = x |^ (2 + 1) ; then x |^ 3 = (x |^ (1 + 1)) * x by NEWTON:6; then A2: x |^ 3 = ((x |^ 1) * x) * x by NEWTON:6; x |^ 1 = x to_power 1 by POWER:41; then A3: x |^ 3 = (x ^2) * x by A2, POWER:25; assume Polynom (a,b,c,0,x) = 0 ; ::_thesis: ( x = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) then (((a * (x ^2)) + (b * x)) + c) * x = 0 by A3; then ( x = 0 or Polynom (a,b,c,x) = 0 ) by XCMPLX_1:6; hence ( x = 0 or x = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by A1, Th5; ::_thesis: verum end; theorem :: POLYEQ_1:23 for a, c, x being real number st a <> 0 & c / a < 0 & Polynom (a,0,c,0,x) = 0 & not x = 0 & not x = sqrt (- (c / a)) holds x = - (sqrt (- (c / a))) proof let a, c, x be real number ; ::_thesis: ( a <> 0 & c / a < 0 & Polynom (a,0,c,0,x) = 0 & not x = 0 & not x = sqrt (- (c / a)) implies x = - (sqrt (- (c / a))) ) assume that A1: a <> 0 and A2: c / a < 0 ; ::_thesis: ( not Polynom (a,0,c,0,x) = 0 or x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) x |^ 3 = x |^ (2 + 1) ; then x |^ 3 = (x |^ (1 + 1)) * x by NEWTON:6; then A3: x |^ 3 = ((x |^ 1) * x) * x by NEWTON:6; x |^ 1 = x to_power 1 by POWER:41; then A4: x |^ 3 = (x ^2) * x by A3, POWER:25; assume Polynom (a,0,c,0,x) = 0 ; ::_thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) then ((a * (x ^2)) + c) * x = 0 by A4; then A5: ( x = 0 or (a * (x ^2)) + c = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_x_>_0_&_(_x_=_0_or_x_=_sqrt_(-_(c_/_a))_or_x_=_-_(sqrt_(-_(c_/_a)))_)_)_or_(_x_<_0_&_(_x_=_0_or_x_=_sqrt_(-_(c_/_a))_or_x_=_-_(sqrt_(-_(c_/_a)))_)_)_or_(_x_=_0_&_(_x_=_0_or_x_=_sqrt_(-_(c_/_a))_or_x_=_-_(sqrt_(-_(c_/_a)))_)_)_) percases ( x > 0 or x < 0 or x = 0 ) by XXREAL_0:1; caseA6: x > 0 ; ::_thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) x |^ 2 = x |^ (1 + 1) ; then x |^ 2 = (x |^ 1) * x by NEWTON:6; then x |^ 2 = (x to_power 1) * x by POWER:41; then A7: x |^ 2 = x * x by POWER:25; A8: - (c / a) > 0 by A2, XREAL_1:58; x ^2 = (- c) / a by A1, A5, A6, XCMPLX_1:89; then x ^2 = (- c) * (a ") by XCMPLX_0:def_9; then x ^2 = - (c * (a ")) ; then x ^2 = - (c / a) by XCMPLX_0:def_9; then x = 2 -Root (- (c / a)) by A6, A8, A7, PREPOWER:def_2; hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) by A8, PREPOWER:32; ::_thesis: verum end; caseA9: x < 0 ; ::_thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) (- x) |^ 2 = (- x) |^ (1 + 1) ; then (- x) |^ 2 = ((- x) |^ 1) * (- x) by NEWTON:6; then (- x) |^ 2 = ((- x) to_power 1) * (- x) by POWER:41; then A10: (- x) |^ 2 = (- x) * (- x) by POWER:25; x ^2 = (- c) / a by A1, A5, A9, XCMPLX_1:89; then x ^2 = (- c) * (a ") by XCMPLX_0:def_9; then x ^2 = - (c * (a ")) ; then A11: (- x) ^2 = - (c / a) by XCMPLX_0:def_9; A12: - (c / a) > 0 by A2, XREAL_1:58; - x > 0 by A9, XREAL_1:58; then - x = 2 -Root (- (c / a)) by A11, A12, A10, PREPOWER:def_2; then - x = sqrt (- (c / a)) by A12, PREPOWER:32; hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; ::_thesis: verum end; case x = 0 ; ::_thesis: ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; ::_thesis: verum end; end; end; hence ( x = 0 or x = sqrt (- (c / a)) or x = - (sqrt (- (c / a))) ) ; ::_thesis: verum end;