:: POLYEQ_2 semantic presentation begin 4 = 2 * 2 ; then 2 divides 4 by INT_1:def_3; then Lm1: 4 is even by ABIAN:def_1; 3 = (2 * 1) + 1 ; then Lm2: 3 is odd by ABIAN:1; definition let a, b, c, d, e, x be complex number ; func Polynom (a,b,c,d,e,x) -> set equals :: POLYEQ_2:def 1 ((((a * (x |^ 4)) + (b * (x |^ 3))) + (c * (x ^2))) + (d * x)) + e; correctness coherence ((((a * (x |^ 4)) + (b * (x |^ 3))) + (c * (x ^2))) + (d * x)) + e is set ; ; end; :: deftheorem defines Polynom POLYEQ_2:def_1_:_ for a, b, c, d, e, x being complex number holds Polynom (a,b,c,d,e,x) = ((((a * (x |^ 4)) + (b * (x |^ 3))) + (c * (x ^2))) + (d * x)) + e; registration let a, b, c, d, e, x be complex number ; cluster Polynom (a,b,c,d,e,x) -> complex ; coherence Polynom (a,b,c,d,e,x) is complex ; end; registration let a, b, c, d, e, x be real number ; cluster Polynom (a,b,c,d,e,x) -> real ; coherence Polynom (a,b,c,d,e,x) is real ; end; theorem :: POLYEQ_2:1 for a, c, e, x being real number st a <> 0 & e <> 0 & (c ^2) - ((4 * a) * e) > 0 & Polynom (a,0,c,0,e,x) = 0 holds ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) ) proof let a, c, e, x be real number ; ::_thesis: ( a <> 0 & e <> 0 & (c ^2) - ((4 * a) * e) > 0 & Polynom (a,0,c,0,e,x) = 0 implies ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) ) ) assume that A1: a <> 0 and A2: e <> 0 and A3: (c ^2) - ((4 * a) * e) > 0 ; ::_thesis: ( not Polynom (a,0,c,0,e,x) = 0 or ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) ) ) set y = x ^2 ; assume A4: Polynom (a,0,c,0,e,x) = 0 ; ::_thesis: ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) ) A5: now__::_thesis:_not_x_=_0 assume x = 0 ; ::_thesis: contradiction then ((a * 0) + (0 * (0 |^ 3))) + e = 0 by A4, NEWTON:11; hence contradiction by A2; ::_thesis: verum end; percases ( x > 0 or x < 0 ) by A5, XXREAL_0:1; supposeA6: x > 0 ; ::_thesis: ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) ) x |^ 4 = x to_power (2 + 2) by POWER:41 .= (x to_power 2) * (x to_power 2) by A6, POWER:27 .= (x ^2) * (x to_power 2) by POWER:46 .= (x ^2) * (x ^2) by POWER:46 ; then ((a * ((x ^2) ^2)) + (c * (x ^2))) + e = 0 by A4; then A7: Polynom (a,c,e,(x ^2)) = 0 by POLYEQ_1:def_2; delta (a,c,e) >= 0 by A3, QUIN_1:def_1; then ( x ^2 = ((- c) + (sqrt (delta (a,c,e)))) / (2 * a) or x ^2 = ((- c) - (sqrt (delta (a,c,e)))) / (2 * a) ) by A1, A7, POLYEQ_1:5; then ( abs x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or abs x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) ) by COMPLEX1:72; hence ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) ) by A6, ABSVALUE:def_1; ::_thesis: verum end; supposeA8: x < 0 ; ::_thesis: ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) ) then A9: 0 < - x by XREAL_1:58; (- x) |^ 4 = x |^ 4 by Lm1, POWER:1; then x |^ 4 = (- x) to_power (2 + 2) by POWER:41 .= ((- x) to_power 2) * ((- x) to_power 2) by A9, POWER:27 .= ((- x) ^2) * ((- x) to_power 2) by POWER:46 .= (x ^2) * (x ^2) by POWER:46 ; then ((a * ((x ^2) ^2)) + (c * (x ^2))) + e = 0 by A4; then A10: Polynom (a,c,e,(x ^2)) = 0 by POLYEQ_1:def_2; (c ^2) - ((4 * a) * e) = delta (a,c,e) by QUIN_1:def_1; then ( x ^2 = ((- c) + (sqrt (delta (a,c,e)))) / (2 * a) or x ^2 = ((- c) - (sqrt (delta (a,c,e)))) / (2 * a) ) by A1, A3, A10, POLYEQ_1:5; then ( abs x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or abs x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) ) by COMPLEX1:72; then ( (- 1) * (- x) = (- 1) * (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or (- 1) * (- x) = (- 1) * (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) by A8, ABSVALUE:def_1; hence ( x <> 0 & ( x = sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a)) or x = sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a)) or x = - (sqrt (((- c) + (sqrt (delta (a,c,e)))) / (2 * a))) or x = - (sqrt (((- c) - (sqrt (delta (a,c,e)))) / (2 * a))) ) ) by A5; ::_thesis: verum end; end; end; theorem Th2: :: POLYEQ_2:2 for a, b, c, x, y being real number st a <> 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 holds ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) proof let a, b, c, x, y be real number ; ::_thesis: ( a <> 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 implies ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) ) assume that A1: a <> 0 and A2: y = x + (1 / x) ; ::_thesis: ( not Polynom (a,b,c,b,a,x) = 0 or ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) ) assume A3: Polynom (a,b,c,b,a,x) = 0 ; ::_thesis: ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) A4: x <> 0 proof assume x = 0 ; ::_thesis: contradiction then ((a * (0 to_power 4)) + (b * (0 |^ 3))) + a = 0 by A3; then ((a * 0) + (b * (0 |^ 3))) + a = 0 by POWER:def_2; then ((a * 0) + (b * 0)) + a = 0 by NEWTON:11; hence contradiction by A1; ::_thesis: verum end; then A5: x ^2 > 0 by SQUARE_1:12; A6: x |^ 4 = x to_power (2 + 2) by POWER:41; A7: now__::_thesis:_(_(_x_>_0_&_a_*_((x_^2)_+_(1_/_(x_^2)))_=_(-_(b_*_(x_+_(1_/_x))))_-_c_&_((x_^2)_-_(x_*_y))_+_1_=_0_)_or_(_x_<_0_&_a_*_((x_^2)_+_(1_/_(x_^2)))_=_(-_(b_*_(x_+_(1_/_x))))_-_c_&_((x_^2)_-_(x_*_y))_+_1_=_0_)_) percases ( x > 0 or x < 0 ) by A4, XXREAL_0:1; caseA8: x > 0 ; ::_thesis: ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) set n = - ((b * x) + a); set m = (a * (x ^2)) + ((b * x) + c); x |^ 3 = x to_power (2 + 1) by POWER:41 .= (x to_power 2) * (x to_power 1) by A8, POWER:27 ; then A9: x |^ 3 = (x to_power 2) * x by POWER:25 .= (x ^2) * x by POWER:46 ; x |^ 4 = (x to_power 2) * (x to_power 2) by A6, A8, POWER:27 .= (x ^2) * (x to_power 2) by POWER:46 .= (x ^2) * (x ^2) by POWER:46 ; then ((a * (x ^2)) + ((b * x) + c)) * (x ^2) = (- ((b * x) + a)) * 1 by A3, A9; then ((a * (x ^2)) + ((b * x) + c)) / 1 = (- ((b * x) + a)) / (x ^2) by A5, XCMPLX_1:94; then (a * (x ^2)) + ((b * x) + c) = (- ((b * x) + a)) * (1 / (x ^2)) by XCMPLX_1:99 .= (- ((b * x) + a)) * ((x ^2) ") by XCMPLX_1:215 .= (- (b * (x * ((x ^2) ")))) - (a * ((x ^2) ")) ; then a * ((x ^2) + ((x ^2) ")) = (- (b * ((x * ((x ^2) ")) + x))) - c ; then A10: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((x * ((x ^2) ")) + x))) - c by XCMPLX_1:215 .= (- (b * ((x * (1 / (x ^2))) + x))) - c by XCMPLX_1:215 ; 1 / (x * x) = (1 / x) * (1 / x) by XCMPLX_1:102; then a * ((x ^2) + (1 / (x ^2))) = (- (b * (((x * (1 / x)) * (1 / x)) + x))) - c by A10; then A11: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((1 * (1 / x)) + x))) - c by A8, XCMPLX_1:106; x * y = (x * x) + (x * (1 / x)) by A2; then (x * y) + 0 = (x ^2) + 1 by A4, XCMPLX_1:106; hence ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) by A11; ::_thesis: verum end; caseA12: x < 0 ; ::_thesis: ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) set n = - ((b * x) + a); set m = (a * (x ^2)) + ((b * x) + c); ((- x) |^ 3) + (x |^ 3) = - ((x |^ 3) + (- (x |^ 3))) by Lm2, POWER:2 .= (x |^ 3) - (x |^ 3) ; then A13: x |^ 3 = - ((- x) |^ 3) ; A14: 0 < - x by A12, XREAL_1:58; (- x) |^ 4 = x |^ 4 by Lm1, POWER:1; then A15: x |^ 4 = (- x) to_power (2 + 2) by POWER:41 .= ((- x) to_power 2) * ((- x) to_power 2) by A14, POWER:27 .= ((- x) ^2) * ((- x) to_power 2) by POWER:46 .= (x ^2) * ((- x) ^2) by POWER:46 ; (- x) |^ 3 = (- x) to_power (2 + 1) by POWER:41 .= ((- x) to_power 2) * ((- x) to_power 1) by A14, POWER:27 ; then A16: (- x) |^ 3 = ((- x) to_power 2) * (- x) by POWER:25; (- x) to_power 2 = (- x) ^2 by POWER:46 .= x ^2 ; then ((a * (x ^2)) + ((b * x) + c)) * (x ^2) = (- ((b * x) + a)) * 1 by A3, A15, A16, A13; then ((a * (x ^2)) + ((b * x) + c)) / 1 = (- ((b * x) + a)) / (x ^2) by A5, XCMPLX_1:94; then (a * (x ^2)) + ((b * x) + c) = (- ((b * x) + a)) * (1 / (x ^2)) by XCMPLX_1:99 .= (- ((b * x) + a)) * ((x ^2) ") by XCMPLX_1:215 .= (- (b * (x * ((x ^2) ")))) - (a * ((x ^2) ")) ; then a * ((x ^2) + ((x ^2) ")) = (- (b * ((x * ((x ^2) ")) + x))) - c ; then a * ((x ^2) + (1 / (x ^2))) = (- (b * ((x * ((x ^2) ")) + x))) - c by XCMPLX_1:215 .= (- (b * ((x * (1 / (x ^2))) + x))) - c by XCMPLX_1:215 ; then a * ((x ^2) + (1 / (x ^2))) = (- (b * ((x * ((1 / x) * (1 / x))) + x))) - c by XCMPLX_1:102 .= (- (b * (((x * (1 / x)) * (1 / x)) + x))) - c ; then A17: a * ((x ^2) + (1 / (x ^2))) = (- (b * ((1 * (1 / x)) + x))) - c by A12, XCMPLX_1:106; x * y = (x * x) + (x * (1 / x)) by A2 .= (x * x) + 1 by A12, XCMPLX_1:106 ; hence ( a * ((x ^2) + (1 / (x ^2))) = (- (b * (x + (1 / x)))) - c & ((x ^2) - (x * y)) + 1 = 0 ) by A17; ::_thesis: verum end; end; end; y ^2 = ((x ^2) + (2 * (x * (1 / x)))) + ((1 / x) ^2) by A2 .= ((x ^2) + (2 * 1)) + ((1 / x) ^2) by A4, XCMPLX_1:106 .= ((x ^2) + 2) + ((1 ^2) / (x ^2)) by XCMPLX_1:76 .= (x ^2) - ((- 2) - (1 / (x ^2))) ; then (a * (y ^2)) - (2 * a) = (- (b * y)) - c by A2, A7; hence ( x <> 0 & (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 ) by A4; ::_thesis: verum end; theorem :: POLYEQ_2:3 for a, b, c, x, y being real number st a <> 0 & ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) > 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 holds for y1, y2 being real number st y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) holds ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) proof let a, b, c, x, y be real number ; ::_thesis: ( a <> 0 & ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) > 0 & y = x + (1 / x) & Polynom (a,b,c,b,a,x) = 0 implies for y1, y2 being real number st y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) holds ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) ) assume that A1: a <> 0 and A2: ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) > 0 and A3: y = x + (1 / x) and A4: Polynom (a,b,c,b,a,x) = 0 ; ::_thesis: for y1, y2 being real number st y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) holds ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) A5: x <> 0 by A1, A3, A4, Th2; set f = c - (2 * a); (((a * (y ^2)) + (b * y)) + c) - (2 * a) = 0 by A1, A3, A4, Th2; then ((a * (y ^2)) + (b * y)) + (c - (2 * a)) = 0 ; then A6: Polynom (a,b,(c - (2 * a)),y) = 0 by POLYEQ_1:def_2; let y1, y2 be real number ; ::_thesis: ( y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) implies ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) ) assume A7: ( y1 = ((- b) + (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) & y2 = ((- b) - (sqrt (((b ^2) - ((4 * a) * c)) + (8 * (a ^2))))) / (2 * a) ) ; ::_thesis: ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) x * y = (x ^2) + (x * (1 / x)) by A3; then (x * y) + 0 = (x ^2) + 1 by A5, XCMPLX_1:106; then ((1 * (x ^2)) + ((- y) * x)) + 1 = 0 ; then A8: Polynom (1,(- y),1,x) = 0 by POLYEQ_1:def_2; delta (1,(- y),1) = ((- y) ^2) - ((4 * 1) * 1) by QUIN_1:def_1 .= (((x ^2) + (2 * (x * (1 / x)))) + ((1 / x) ^2)) - 4 by A3 .= (((x ^2) + (2 * 1)) + ((1 / x) ^2)) - 4 by A5, XCMPLX_1:106 .= (x ^2) + ((- (2 * 1)) + ((1 / x) ^2)) .= (x ^2) + ((- (2 * (x * (1 / x)))) + ((1 / x) ^2)) by A5, XCMPLX_1:106 .= (x - (1 / x)) ^2 ; then A9: ( x = ((- (- y)) + (sqrt (delta (1,(- y),1)))) / (2 * 1) or x = ((- (- y)) - (sqrt (delta (1,(- y),1)))) / (2 * 1) ) by A8, POLYEQ_1:5, XREAL_1:63; A10: (b ^2) - ((4 * a) * (c - (2 * a))) = ((b ^2) - ((4 * a) * c)) + (8 * (a ^2)) ; then delta (a,b,(c - (2 * a))) > 0 by A2, QUIN_1:def_1; then ( y = ((- b) + (sqrt (delta (a,b,(c - (2 * a)))))) / (2 * a) or y = ((- b) - (sqrt (delta (a,b,(c - (2 * a)))))) / (2 * a) ) by A1, A6, POLYEQ_1:5; then ( y = y1 or y = y2 ) by A7, A10, QUIN_1:def_1; hence ( x <> 0 & ( x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 or x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 or x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) ) by A1, A3, A4, A9, Th2; ::_thesis: verum end; theorem Th4: :: POLYEQ_2:4 for x being real number holds ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) proof let x be real number ; ::_thesis: ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) percases ( x = 0 or x > 0 or x < 0 ) by XXREAL_0:1; suppose x = 0 ; ::_thesis: ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) hence ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) by NEWTON:11; ::_thesis: verum end; supposeA1: x > 0 ; ::_thesis: ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) (x |^ 3) * x = (x |^ 3) * (x to_power 1) by POWER:25 .= (x to_power 3) * (x to_power 1) ; then A2: (x |^ 3) * x = x to_power (3 + 1) by A1, POWER:27; x ^2 = x to_power 2 by POWER:46; then (x ^2) * x = (x to_power 2) * (x to_power 1) by POWER:25 .= x to_power (2 + 1) by A1, POWER:27 .= x |^ 3 by POWER:41 ; hence ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) by A2, POWER:41; ::_thesis: verum end; suppose x < 0 ; ::_thesis: ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) then A3: - x > 0 by XREAL_1:58; ((- x) |^ 3) + (x |^ 3) = - ((x |^ 3) + (- (x |^ 3))) by Lm2, POWER:2 .= (x |^ 3) - (x |^ 3) ; then A4: (x |^ 3) + (((- x) |^ 3) - ((- x) |^ 3)) = 0 - ((- x) |^ 3) ; A5: (- x) to_power 2 = (- x) ^2 by POWER:46 .= x ^2 ; (- x) |^ 3 = (- x) to_power (2 + 1) by POWER:41 .= ((- x) to_power 2) * ((- x) to_power 1) by A3, POWER:27 ; then A6: (- x) |^ 3 = ((- x) to_power 2) * (- x) by POWER:25; (- x) |^ 4 = x |^ 4 by Lm1, POWER:1; then x |^ 4 = (- x) to_power (3 + 1) by POWER:41 .= ((- x) to_power 3) * ((- x) to_power 1) by A3, POWER:27 .= ((- x) |^ 3) * ((- x) to_power 1) ; then x |^ 4 = ((- x) |^ 3) * (- x) by POWER:25 .= (x ^2) * (x * x) by A6, A5 ; hence ( x |^ 3 = (x ^2) * x & (x |^ 3) * x = x |^ 4 & (x ^2) * (x ^2) = x |^ 4 ) by A6, A5, A4; ::_thesis: verum end; end; end; theorem Th5: :: POLYEQ_2:5 for x, y being real number st x + y <> 0 holds (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) proof let x, y be real number ; ::_thesis: ( x + y <> 0 implies (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) ) assume A1: x + y <> 0 ; ::_thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) percases ( x + y > 0 or x + y < 0 ) by A1, XXREAL_0:1; supposeA2: x + y > 0 ; ::_thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) (x + y) |^ 4 = (x + y) to_power (3 + 1) by POWER:41 .= ((x + y) to_power 3) * ((x + y) to_power 1) by A2, POWER:27 .= ((x + y) to_power 3) * (x + y) by POWER:25 ; then (x + y) |^ 4 = ((x + y) |^ 3) * (x + y) .= (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * (x + y) by POLYEQ_1:14 ; hence (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) ; ::_thesis: verum end; suppose x + y < 0 ; ::_thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) then A3: - (x + y) > 0 by XREAL_1:58; (- (x + y)) |^ 4 = (x + y) |^ 4 by Lm1, POWER:1; then (x + y) |^ 4 = (- (x + y)) to_power (3 + 1) by POWER:41 .= ((- (x + y)) to_power 3) * ((- (x + y)) to_power 1) by A3, POWER:27 .= ((- (x + y)) |^ 3) * ((- (x + y)) to_power 1) ; then (x + y) |^ 4 = ((- (x + y)) |^ 3) * (- (x + y)) by POWER:25; then (x + y) |^ 4 = (- ((x + y) |^ 3)) * (- (x + y)) by Lm2, POWER:2 .= ((x + y) |^ 3) * (x + y) .= (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * (x + y) by POLYEQ_1:14 ; hence (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) ; ::_thesis: verum end; end; end; theorem :: POLYEQ_2:6 for x, y being real number st x + y <> 0 holds (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4) proof let x, y be real number ; ::_thesis: ( x + y <> 0 implies (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4) ) set g = (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x; set h = (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y; set p = y |^ 3; set q = x |^ 3; set u = x |^ 4; set v = y |^ 4; A1: (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x = (((x |^ 3) * x) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * x)) + ((y |^ 3) * x) ; A2: y |^ 3 = (y ^2) * y by Th4; assume x + y <> 0 ; ::_thesis: (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4) then A3: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) by Th5; (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y = (((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + ((y |^ 3) * y) .= (((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4) by Th4 ; then (x + y) |^ 4 = (((x |^ 4) + (((3 * y) * ((x ^2) * x)) - ((- ((3 * (y ^2)) * x)) * x))) + ((y |^ 3) * x)) + ((((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4)) by A3, A1, Th4 .= (((x |^ 4) + (((3 * y) * (x |^ 3)) - (- ((3 * (y ^2)) * (x ^2))))) + ((y |^ 3) * x)) + ((((x |^ 3) * y) + ((((3 * y) * (x ^2)) + ((3 * (y ^2)) * x)) * y)) + (y |^ 4)) by Th4 .= (((x |^ 4) + ((3 * y) * (x |^ 3))) + (((3 * (y ^2)) * (x ^2)) + ((y |^ 3) * x))) + ((((x |^ 3) * y) + (((3 * (y ^2)) * (x ^2)) + (((3 * (y ^2)) * x) * y))) + (y |^ 4)) ; hence (x + y) |^ 4 = ((x |^ 4) + ((((4 * y) * (x |^ 3)) + ((6 * (y ^2)) * (x ^2))) + ((4 * (y |^ 3)) * x))) + (y |^ 4) by A2; ::_thesis: verum end; theorem Th7: :: POLYEQ_2:7 for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) proof set x = - 1; let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be real number ; ::_thesis: ( ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) implies ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) ) A1: ( 0 |^ 3 = 0 & 0 |^ 4 = 0 ) by NEWTON:11; assume A2: for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ; ::_thesis: ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) then A3: Polynom (a1,a2,a3,a4,a5,(- 1)) = Polynom (b1,b2,b3,b4,b5,(- 1)) ; A4: ( 1 |^ 3 = 1 & 1 |^ 4 = 1 ) by NEWTON:10; A5: ( (- 1) |^ 3 = ((- 1) ^2) * (- 1) & ((- 1) |^ 3) * (- 1) = (- 1) |^ 4 ) by Th4; ( Polynom (a1,a2,a3,a4,a5,0) = Polynom (b1,b2,b3,b4,b5,0) & Polynom (a1,a2,a3,a4,a5,1) = Polynom (b1,b2,b3,b4,b5,1) ) by A2; hence ( a5 = b5 & ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) by A1, A4, A3, A5; ::_thesis: verum end; theorem Th8: :: POLYEQ_2:8 for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) proof let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be real number ; ::_thesis: ( ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) implies ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) ) assume for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ; ::_thesis: ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) then ( ((a1 - a2) + a3) - a4 = ((b1 - b2) + b3) - b4 & ((a1 + a2) + a3) + a4 = ((b1 + b2) + b3) + b4 ) by Th7; hence ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) ; ::_thesis: verum end; theorem Th9: :: POLYEQ_2:9 for a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 being real number st ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) holds ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) proof A1: (- 2) |^ 3 = ((- 2) ^2) * (- 2) by Th4 .= - (4 * 2) ; A2: (- 2) |^ 4 = 16 by Lm1, POWER:1, POWER:62; let a1, a2, a3, a4, a5, b1, b2, b3, b4, b5 be real number ; ::_thesis: ( ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ) implies ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) ) assume A3: for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Polynom (b1,b2,b3,b4,b5,x) ; ::_thesis: ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) then A4: Polynom (a1,a2,a3,a4,a5,(- 2)) = Polynom (b1,b2,b3,b4,b5,(- 2)) ; A5: ( a5 = b5 & Polynom (a1,a2,a3,a4,a5,2) = Polynom (b1,b2,b3,b4,b5,2) ) by A3, Th7; ( a1 - b1 = b3 - a3 & a2 - b2 = b4 - a4 ) by A3, Th8; hence ( a1 = b1 & a2 = b2 & a3 = b3 & a4 = b4 & a5 = b5 ) by A5, A4, A2, A1, POWER:61, POWER:62; ::_thesis: verum end; definition let a1, x1, x2, x3, x4, x be real number ; func Four0 (a1,x1,x2,x3,x4,x) -> set equals :: POLYEQ_2:def 2 a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)); correctness coherence a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) is set ; ; end; :: deftheorem defines Four0 POLYEQ_2:def_2_:_ for a1, x1, x2, x3, x4, x being real number holds Four0 (a1,x1,x2,x3,x4,x) = a1 * ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)); registration let a1, x1, x2, x3, x4, x be real number ; cluster Four0 (a1,x1,x2,x3,x4,x) -> real ; coherence Four0 (a1,x1,x2,x3,x4,x) is real ; end; theorem Th10: :: POLYEQ_2:10 for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) holds (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) proof let a1, a2, a3, a4, a5, x, x1, x2, x3, x4 be real number ; ::_thesis: ( a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) implies (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) ) assume A1: a1 <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) or (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) ) set z = (((x - x1) * (x - x2)) * (x - x3)) * (x - x4); set w = ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5; assume for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ; ::_thesis: (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) then Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ; then (((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) * a1) - (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) = (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) - (((((x - x1) * (x - x2)) * (x - x3)) * (x - x4)) * a1) by A1, XCMPLX_1:87; then (((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) - ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4))) * a1 = 0 ; then ((((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1) + (- ((((x - x1) * (x - x2)) * (x - x3)) * (x - x4))) = 0 - 0 by A1, XCMPLX_1:6; hence (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) ; ::_thesis: verum end; theorem Th11: :: POLYEQ_2:11 for a1, a2, a3, a4, a5, x, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) holds (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) proof let a1, a2, a3, a4, a5, x, x1, x2, x3, x4 be real number ; ::_thesis: ( a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) implies (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) ) assume A1: a1 <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) or (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) ) set w = ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5; assume for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ; ::_thesis: (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) then (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - (((x1 + x2) + x3) * ((x ^2) * x))) + ((((x1 * x3) + (x2 * x3)) + (x1 * x2)) * (x ^2))) - (((x1 * x2) * x3) * x)) - ((((x - x1) * (x - x2)) * (x - x3)) * x4) by A1, Th10; then (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = (((((x ^2) * (x ^2)) - ((((x1 + x2) + x3) + x4) * ((x ^2) * x))) + (((((x1 * x3) + (x2 * x3)) + (x1 * x2)) + (((x2 * x4) + (x1 * x4)) + (x3 * x4))) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + (- (- ((x1 * x3) * x4)))) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) ; then (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * ((x ^2) * x))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) by Th4; hence (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) by Th4; ::_thesis: verum end; theorem :: POLYEQ_2:12 for a1, a2, a3, a4, a5, x1, x2, x3, x4 being real number st a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) holds ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) proof set b1 = 1; let a1, a2, a3, a4, a5, x1, x2, x3, x4 be real number ; ::_thesis: ( a1 <> 0 & ( for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ) implies ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) ) assume A1: a1 <> 0 ; ::_thesis: ( ex x being real number st not Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) or ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) ) set b5 = ((x1 * x2) * x3) * x4; set b4 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)); set b3 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4); set b2 = - (((x1 + x2) + x3) + x4); assume A2: for x being real number holds Polynom (a1,a2,a3,a4,a5,x) = Four0 (a1,x1,x2,x3,x4,x) ; ::_thesis: ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) now__::_thesis:_for_x_being_real_number_holds_Polynom_(1,(a2_/_a1),(a3_/_a1),(a4_/_a1),(a5_/_a1),x)_=_Polynom_(1,(-_(((x1_+_x2)_+_x3)_+_x4)),(((((x1_*_x2)_+_(x1_*_x3))_+_(x1_*_x4))_+_((x2_*_x3)_+_(x2_*_x4)))_+_(x3_*_x4)),(-_(((((x1_*_x2)_*_x3)_+_((x1_*_x2)_*_x4))_+_((x1_*_x3)_*_x4))_+_((x2_*_x3)_*_x4))),(((x1_*_x2)_*_x3)_*_x4),x) let x be real number ; ::_thesis: Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x) = Polynom (1,(- (((x1 + x2) + x3) + x4)),(((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)),(- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))),(((x1 * x2) * x3) * x4),x) set t = ((((1 * (x |^ 4)) + ((- (((x1 + x2) + x3) + x4)) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) + ((- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))) * x)) + (((x1 * x2) * x3) * x4); (((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + (a3 * (x ^2))) + (a4 * x)) + a5) / a1 = ((((x |^ 4) - ((((x1 + x2) + x3) + x4) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) - ((((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) * x)) + (((x1 * x2) * x3) * x4) by A1, A2, Th11; then ((((1 * (x |^ 4)) + ((- (((x1 + x2) + x3) + x4)) * (x |^ 3))) + ((((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)) * (x ^2))) + ((- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))) * x)) + (((x1 * x2) * x3) * x4) = (a1 ") * ((((a1 * (x |^ 4)) + (a2 * (x |^ 3))) + ((a3 * (x ^2)) + (a4 * x))) + a5) by XCMPLX_0:def_9 .= ((((a1 ") * a1) * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5)) .= (((a1 / a1) * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5)) by XCMPLX_0:def_9 .= ((1 * (x |^ 4)) + ((a1 ") * (a2 * (x |^ 3)))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5)) by A1, XCMPLX_1:60 .= ((x |^ 4) + (((a1 ") * a2) * (x |^ 3))) + ((((a1 ") * (a3 * (x ^2))) + ((a1 ") * (a4 * x))) + ((a1 ") * a5)) .= ((x |^ 4) + ((a2 / a1) * (x |^ 3))) + (((((a1 ") * a3) * (x ^2)) + ((a1 ") * (a4 * x))) + ((a1 ") * a5)) by XCMPLX_0:def_9 .= ((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + (((a1 ") * a4) * x)) + ((a1 ") * a5)) by XCMPLX_0:def_9 .= ((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + ((a4 / a1) * x)) + ((a1 ") * a5)) by XCMPLX_0:def_9 .= ((x |^ 4) + ((a2 / a1) * (x |^ 3))) + ((((a3 / a1) * (x ^2)) + ((a4 / a1) * x)) + (a5 / a1)) by XCMPLX_0:def_9 .= Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x) ; hence Polynom (1,(a2 / a1),(a3 / a1),(a4 / a1),(a5 / a1),x) = Polynom (1,(- (((x1 + x2) + x3) + x4)),(((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4)),(- (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4))),(((x1 * x2) * x3) * x4),x) ; ::_thesis: verum end; hence ( a2 / a1 = - (((x1 + x2) + x3) + x4) & a3 / a1 = ((((x1 * x2) + (x1 * x3)) + (x1 * x4)) + ((x2 * x3) + (x2 * x4))) + (x3 * x4) & a4 / a1 = - (((((x1 * x2) * x3) + ((x1 * x2) * x4)) + ((x1 * x3) * x4)) + ((x2 * x3) * x4)) & a5 / a1 = ((x1 * x2) * x3) * x4 ) by Th9; ::_thesis: verum end; theorem :: POLYEQ_2:13 for a, k, y being real number st a <> 0 & ( for x being real number holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ) holds (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0 proof let a, k, y be real number ; ::_thesis: ( a <> 0 & ( for x being real number holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ) implies (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0 ) assume that A1: a <> 0 and A2: for x being real number holds (x |^ 4) + (a |^ 4) = ((k * a) * x) * ((x ^2) + (a ^2)) ; ::_thesis: (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0 ((a * y) |^ 4) + (a |^ 4) = ((k * a) * (a * y)) * (((a * y) ^2) + (a ^2)) by A2 .= (k * ((a ^2) * y)) * (((a ^2) * (y ^2)) + ((a ^2) * 1)) ; then ((a * y) |^ 4) + (a |^ 4) = k * ((((a ^2) * (a ^2)) * y) * ((y ^2) + 1)) .= k * (((a |^ 4) * y) * ((y ^2) + 1)) by Th4 .= ((a |^ 4) * (k * y)) * ((y ^2) + 1) ; then ((a |^ 4) * (y |^ 4)) + ((a |^ 4) * 1) = (a |^ 4) * ((k * y) * ((y ^2) + 1)) by NEWTON:7; then ((a |^ 4) ") * ((a |^ 4) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1)))) = 0 ; then (((a |^ 4) ") * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0 ; then A3: ((1 / (a |^ 4)) * (a |^ 4)) * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0 by XCMPLX_1:215; a |^ 4 <> 0 by A1, PREPOWER:5; then 1 * (((y |^ 4) + 1) - ((k * y) * ((y ^2) + 1))) = 0 by A3, XCMPLX_1:106; then (((y |^ 4) - (k * ((y ^2) * y))) - (k * y)) + 1 = 0 ; hence (((y |^ 4) - (k * (y |^ 3))) - (k * y)) + 1 = 0 by Th4; ::_thesis: verum end;