:: POLYEQ_4 semantic presentation begin theorem Th1: :: POLYEQ_4:1 for b, a, c being Real st b / a < 0 & c / a > 0 & delta (a,b,c) >= 0 holds ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) proof let b, a, c be Real; ::_thesis: ( b / a < 0 & c / a > 0 & delta (a,b,c) >= 0 implies ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) assume that A1: b / a < 0 and A2: c / a > 0 and A3: delta (a,b,c) >= 0 ; ::_thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) A4: (b ^2) - ((4 * a) * c) >= 0 by A3, QUIN_1:def_1; now__::_thesis:_(_(_b_<_0_&_a_>_0_&_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_)_or_(_b_>_0_&_a_<_0_&_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_)_) percases ( ( b < 0 & a > 0 ) or ( b > 0 & a < 0 ) ) by A1, XREAL_1:143; caseA5: ( b < 0 & a > 0 ) ; ::_thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) A6: 0 <= sqrt ((b ^2) - ((4 * a) * c)) by A4, SQUARE_1:17, SQUARE_1:26; A7: 2 * a > 0 by A5, XREAL_1:129; - b > 0 by A5, XREAL_1:58; then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) > 0 + 0 by A6, XREAL_1:8; then A8: ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A7, XREAL_1:139; ( c > 0 & 4 * a > 0 ) by A2, A5, XREAL_1:129, XREAL_1:144; then - (- ((4 * a) * c)) > 0 by XREAL_1:129; then - ((4 * a) * c) < 0 ; then (b ^2) + (- ((4 * a) * c)) < (b ^2) + 0 by XREAL_1:8; then sqrt ((b ^2) - ((4 * a) * c)) < sqrt (b ^2) by A4, SQUARE_1:27; then sqrt ((b ^2) - ((4 * a) * c)) < - b by A5, SQUARE_1:23; then - (sqrt ((b ^2) - ((4 * a) * c))) > - (- b) by XREAL_1:24; then (- (sqrt ((b ^2) - ((4 * a) * c)))) + (- b) > (- (- b)) + (- b) by XREAL_1:8; then ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A7, XREAL_1:139; hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) by A8, QUIN_1:def_1; ::_thesis: verum end; caseA9: ( b > 0 & a < 0 ) ; ::_thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) then A10: a * 2 < 0 * 2 by XREAL_1:68; c < 0 by A2, A9, XREAL_1:144; then a * c > 0 by A9, XREAL_1:130; then 4 * (a * c) > 0 by XREAL_1:129; then - (- ((4 * a) * c)) > 0 ; then - ((4 * a) * c) < 0 ; then (b ^2) + (- ((4 * a) * c)) < (b ^2) + 0 by XREAL_1:8; then sqrt ((b ^2) - ((4 * a) * c)) < sqrt (b ^2) by A4, SQUARE_1:27; then sqrt ((b ^2) - ((4 * a) * c)) < b by A9, SQUARE_1:22; then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) < (0 + b) + (- b) by XREAL_1:8; then A11: ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A10, XREAL_1:140; A12: 0 <= sqrt ((b ^2) - ((4 * a) * c)) by A4, SQUARE_1:17, SQUARE_1:26; - (- b) > 0 by A9; then (- b) + 0 < 0 + (sqrt ((b ^2) - ((4 * a) * c))) by A12; then - (- ((sqrt ((b ^2) - ((4 * a) * c))) + b)) > 0 by XREAL_1:62; then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ; then ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A10, XREAL_1:140; hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) by A11, QUIN_1:def_1; ::_thesis: verum end; end; end; hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ; ::_thesis: verum end; theorem :: POLYEQ_4:2 for b, a, c being Real st b / a > 0 & c / a > 0 & delta (a,b,c) >= 0 holds ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) proof let b, a, c be Real; ::_thesis: ( b / a > 0 & c / a > 0 & delta (a,b,c) >= 0 implies ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) ) assume that A1: b / a > 0 and A2: c / a > 0 and A3: delta (a,b,c) >= 0 ; ::_thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) A4: (b ^2) - ((4 * a) * c) >= 0 by A3, QUIN_1:def_1; now__::_thesis:_(_(_b_>_0_&_a_>_0_&_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_)_or_(_b_<_0_&_a_<_0_&_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_)_) percases ( ( b > 0 & a > 0 ) or ( b < 0 & a < 0 ) ) by A1, XREAL_1:144; caseA5: ( b > 0 & a > 0 ) ; ::_thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) then ( c > 0 & 4 * a > 0 ) by A2, XREAL_1:129, XREAL_1:144; then - (- ((4 * a) * c)) > 0 by XREAL_1:129; then - ((4 * a) * c) < 0 ; then (b ^2) + (- ((4 * a) * c)) < (b ^2) + 0 by XREAL_1:8; then sqrt ((b ^2) - ((4 * a) * c)) < sqrt (b ^2) by A4, SQUARE_1:27; then sqrt ((b ^2) - ((4 * a) * c)) < b by A5, SQUARE_1:22; then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) < 0 + (b + (- b)) by XREAL_1:8; then A6: ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0 by A5, XREAL_1:129, XREAL_1:141; 0 <= sqrt ((b ^2) - ((4 * a) * c)) by A4, SQUARE_1:17, SQUARE_1:26; then 0 + 0 < b + (sqrt ((b ^2) - ((4 * a) * c))) by A5, XREAL_1:8; then - (- (b + (sqrt ((b ^2) - ((4 * a) * c))))) > 0 ; then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ; then ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0 by A5, XREAL_1:129, XREAL_1:141; hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) by A6, QUIN_1:def_1; ::_thesis: verum end; caseA7: ( b < 0 & a < 0 ) ; ::_thesis: ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) A8: 0 <= sqrt ((b ^2) - ((4 * a) * c)) by A4, SQUARE_1:17, SQUARE_1:26; A9: a * 2 < 0 * 2 by A7, XREAL_1:68; - b > 0 by A7, XREAL_1:58; then 0 + 0 < (- b) + (sqrt ((b ^2) - ((4 * a) * c))) by A8, XREAL_1:8; then A10: ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0 by A9, XREAL_1:142; c < 0 by A2, A7, XREAL_1:144; then a * c > 0 by A7, XREAL_1:130; then 4 * (a * c) > 0 by XREAL_1:129; then - (- ((4 * a) * c)) > 0 ; then - ((4 * a) * c) < 0 ; then (b ^2) + (- ((4 * a) * c)) < (b ^2) + 0 by XREAL_1:8; then sqrt ((b ^2) - ((4 * a) * c)) < sqrt (b ^2) by A4, SQUARE_1:27; then sqrt ((b ^2) - ((4 * a) * c)) < - b by A7, SQUARE_1:23; then b + (sqrt ((b ^2) - ((4 * a) * c))) < (0 + b) + (- b) by XREAL_1:8; then - (b + (sqrt ((b ^2) - ((4 * a) * c)))) > 0 by XREAL_1:58; then ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0 by A9, XREAL_1:142; hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) by A10, QUIN_1:def_1; ::_thesis: verum end; end; end; hence ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) ; ::_thesis: verum end; theorem :: POLYEQ_4:3 for c, a, b being Real holds ( not c / a < 0 or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) proof let c, a, b be Real; ::_thesis: ( not c / a < 0 or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) assume A1: c / a < 0 ; ::_thesis: ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) now__::_thesis:_(_(_c_>_0_&_a_<_0_&_(_(_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_)_or_(_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_)_)_)_or_(_c_<_0_&_a_>_0_&_(_(_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_)_or_(_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_)_)_)_) percases ( ( c > 0 & a < 0 ) or ( c < 0 & a > 0 ) ) by A1, XREAL_1:143; caseA2: ( c > 0 & a < 0 ) ; ::_thesis: ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) then 4 * a < 4 * 0 by XREAL_1:68; then (4 * a) * c < 0 * c by A2, XREAL_1:68; then A3: - ((4 * a) * c) > 0 by XREAL_1:58; then (b ^2) + (- ((4 * a) * c)) > (b ^2) + 0 by XREAL_1:8; then A4: sqrt ((b ^2) - ((4 * a) * c)) > sqrt (b ^2) by SQUARE_1:27, XREAL_1:63; A5: 2 * a < 2 * 0 by A2, XREAL_1:68; (- ((4 * a) * c)) + (b ^2) > 0 + 0 by A3, XREAL_1:8, XREAL_1:63; then A6: - (- (sqrt ((b ^2) - ((4 * a) * c)))) > 0 by SQUARE_1:17, SQUARE_1:27; then A7: - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ; now__::_thesis:_(_(_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_)_or_(_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_)_) percases ( b >= 0 or b < 0 ) ; supposeA8: b >= 0 ; ::_thesis: ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) then - b <= - 0 ; then (- (sqrt ((b ^2) - ((4 * a) * c)))) + (- b) < 0 + 0 by A7; then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ; then A9: (- b) - (sqrt (delta (a,b,c))) < 0 by QUIN_1:def_1; sqrt ((b ^2) - ((4 * a) * c)) > b by A4, A8, SQUARE_1:22; then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) > (0 + b) + (- b) by XREAL_1:8; then ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0 by A5, XREAL_1:142; hence ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) by A5, A9, QUIN_1:def_1, XREAL_1:140; ::_thesis: verum end; supposeA10: b < 0 ; ::_thesis: ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) then sqrt ((b ^2) - ((4 * a) * c)) > - b by A4, SQUARE_1:23; then - (- (b + (sqrt ((b ^2) - ((4 * a) * c))))) > 0 by XREAL_1:62; then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ; then A11: ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A5, XREAL_1:140; - b > 0 by A10, XREAL_1:58; then (sqrt ((b ^2) - ((4 * a) * c))) + (- b) > 0 + 0 by A6, XREAL_1:8; then (sqrt (delta (a,b,c))) + (- b) > 0 + 0 by QUIN_1:def_1; hence ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) by A5, A11, QUIN_1:def_1, XREAL_1:142; ::_thesis: verum end; end; end; hence ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) ; ::_thesis: verum end; caseA12: ( c < 0 & a > 0 ) ; ::_thesis: ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) then 4 * a > 0 by XREAL_1:129; then (4 * a) * c < (4 * a) * 0 by A12, XREAL_1:68; then A13: - ((4 * a) * c) > 0 by XREAL_1:58; then (b ^2) + (- ((4 * a) * c)) > (b ^2) + 0 by XREAL_1:8; then A14: sqrt ((b ^2) - ((4 * a) * c)) > sqrt (b ^2) by SQUARE_1:27, XREAL_1:63; A15: 2 * a > 0 by A12, XREAL_1:129; (- ((4 * a) * c)) + (b ^2) > 0 + 0 by A13, XREAL_1:8, XREAL_1:63; then A16: - (- (sqrt ((b ^2) - ((4 * a) * c)))) > 0 by SQUARE_1:17, SQUARE_1:27; then A17: - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ; now__::_thesis:_(_(_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_)_or_(_((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_<_0_&_((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)_>_0_)_) percases ( b >= 0 or b < 0 ) ; supposeA18: b >= 0 ; ::_thesis: ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) then - b <= - 0 ; then (- (sqrt ((b ^2) - ((4 * a) * c)))) + (- b) < 0 + 0 by A17; then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ; then A19: (- b) - (sqrt (delta (a,b,c))) < 0 by QUIN_1:def_1; sqrt ((b ^2) - ((4 * a) * c)) > b by A14, A18, SQUARE_1:22; then (- b) + (sqrt ((b ^2) - ((4 * a) * c))) > (0 + b) + (- b) by XREAL_1:8; then ((- b) + (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) > 0 by A15, XREAL_1:139; hence ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) by A12, A19, QUIN_1:def_1, XREAL_1:129, XREAL_1:141; ::_thesis: verum end; supposeA20: b < 0 ; ::_thesis: ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) then sqrt ((b ^2) - ((4 * a) * c)) > - b by A14, SQUARE_1:23; then - (- (b + (sqrt ((b ^2) - ((4 * a) * c))))) > 0 by XREAL_1:62; then (- b) - (sqrt ((b ^2) - ((4 * a) * c))) < 0 ; then A21: ((- b) - (sqrt ((b ^2) - ((4 * a) * c)))) / (2 * a) < 0 by A12, XREAL_1:129, XREAL_1:141; - b > 0 by A20, XREAL_1:58; then (sqrt ((b ^2) - ((4 * a) * c))) + (- b) > 0 + 0 by A16, XREAL_1:8; then (sqrt (delta (a,b,c))) + (- b) > 0 by QUIN_1:def_1; hence ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) by A15, A21, QUIN_1:def_1, XREAL_1:139; ::_thesis: verum end; end; end; hence ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) ; ::_thesis: verum end; end; end; hence ( ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) > 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) < 0 ) or ( ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) < 0 & ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) > 0 ) ) ; ::_thesis: verum end; theorem Th4: :: POLYEQ_4:4 for a, x being Real for n being Element of NAT st a > 0 & n is even & n >= 1 & x |^ n = a & not x = n -root a holds x = - (n -root a) proof let a, x be Real; ::_thesis: for n being Element of NAT st a > 0 & n is even & n >= 1 & x |^ n = a & not x = n -root a holds x = - (n -root a) let n be Element of NAT ; ::_thesis: ( a > 0 & n is even & n >= 1 & x |^ n = a & not x = n -root a implies x = - (n -root a) ) assume that A1: a > 0 and A2: n is even and A3: n >= 1 ; ::_thesis: ( not x |^ n = a or x = n -root a or x = - (n -root a) ) assume A4: x |^ n = a ; ::_thesis: ( x = n -root a or x = - (n -root a) ) then A5: x <> 0 by A1, A3, NEWTON:11; now__::_thesis:_(_(_x_>_0_&_(_x_=_n_-root_a_or_x_=_-_(n_-root_a)_)_)_or_(_x_<_0_&_(_x_=_n_-root_a_or_x_=_-_(n_-root_a)_)_)_) percases ( x > 0 or x < 0 ) by A5, XXREAL_0:1; case x > 0 ; ::_thesis: ( x = n -root a or x = - (n -root a) ) hence ( x = n -root a or x = - (n -root a) ) by A4, A3, POWER:4; ::_thesis: verum end; case x < 0 ; ::_thesis: ( x = n -root a or x = - (n -root a) ) then A6: - x > 0 by XREAL_1:58; n -root a = n -root ((- x) |^ n) by A2, A4, POWER:1; then (- 1) * (n -root a) = (- 1) * (- x) by A3, A6, POWER:4; hence ( x = n -root a or x = - (n -root a) ) ; ::_thesis: verum end; end; end; hence ( x = n -root a or x = - (n -root a) ) ; ::_thesis: verum end; theorem Th5: :: POLYEQ_4:5 for a, b, x being Real st a <> 0 & Polynom (a,b,0,x) = 0 & not x = 0 holds x = - (b / a) proof let a, b, x be Real; ::_thesis: ( a <> 0 & Polynom (a,b,0,x) = 0 & not x = 0 implies x = - (b / a) ) assume that A1: a <> 0 and A2: Polynom (a,b,0,x) = 0 ; ::_thesis: ( x = 0 or x = - (b / a) ) ((a * (x ^2)) + (b * x)) + 0 = 0 by A2, POLYEQ_1:def_2; then (((a * x) + b) + 0) * x = 0 ; then ( ((a * x) + b) + (- b) = 0 + (- b) or x = 0 ) by XCMPLX_1:6; then ( x = (- b) / a or x = 0 ) by A1, XCMPLX_1:89; hence ( x = 0 or x = - (b / a) ) by XCMPLX_1:187; ::_thesis: verum end; theorem :: POLYEQ_4:6 for a, x being Real st a <> 0 & Polynom (a,0,0,x) = 0 holds x = 0 proof let a, x be Real; ::_thesis: ( a <> 0 & Polynom (a,0,0,x) = 0 implies x = 0 ) assume that A1: a <> 0 and A2: Polynom (a,0,0,x) = 0 ; ::_thesis: x = 0 ((a * (x ^2)) + (0 * x)) + 0 = 0 by A2, POLYEQ_1:def_2; then x ^2 = 0 by A1, XCMPLX_1:6; hence x = 0 by XCMPLX_1:6; ::_thesis: verum end; theorem :: POLYEQ_4:7 for a, b, c, x being Real for n being Element of NAT st a <> 0 & n is odd & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) holds x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) proof let a, b, c, x be Real; ::_thesis: for n being Element of NAT st a <> 0 & n is odd & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) holds x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) let n be Element of NAT ; ::_thesis: ( a <> 0 & n is odd & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) implies x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) ) assume that A1: a <> 0 and A2: n is odd and A3: ( delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 ) ; ::_thesis: ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) ) ( x |^ n = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x |^ n = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by A1, A3, POLYEQ_1:5; hence ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) ) by A2, POWER:4; ::_thesis: verum end; theorem :: POLYEQ_4:8 for a, b, c, x being Real for n being Element of NAT st a <> 0 & b / a < 0 & c / a > 0 & n is even & n >= 1 & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) & not x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) & not x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) holds x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) proof let a, b, c, x be Real; ::_thesis: for n being Element of NAT st a <> 0 & b / a < 0 & c / a > 0 & n is even & n >= 1 & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) & not x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) & not x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) holds x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) let n be Element of NAT ; ::_thesis: ( a <> 0 & b / a < 0 & c / a > 0 & n is even & n >= 1 & delta (a,b,c) >= 0 & Polynom (a,b,c,(x |^ n)) = 0 & not x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) & not x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) & not x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) implies x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) ) assume that A1: a <> 0 and A2: ( b / a < 0 & c / a > 0 & n is even & n >= 1 ) and A3: delta (a,b,c) >= 0 and A4: Polynom (a,b,c,(x |^ n)) = 0 ; ::_thesis: ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) ) now__::_thesis:_(_x_=_n_-root_(((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a))_or_x_=_-_(n_-root_(((-_b)_+_(sqrt_(delta_(a,b,c))))_/_(2_*_a)))_or_x_=_n_-root_(((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a))_or_x_=_-_(n_-root_(((-_b)_-_(sqrt_(delta_(a,b,c))))_/_(2_*_a)))_) percases ( x |^ n = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) or x |^ n = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ) by A1, A3, A4, POLYEQ_1:5; suppose x |^ n = ((- b) + (sqrt (delta (a,b,c)))) / (2 * a) ; ::_thesis: ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) ) hence ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) ) by A2, A3, Th1, Th4; ::_thesis: verum end; suppose x |^ n = ((- b) - (sqrt (delta (a,b,c)))) / (2 * a) ; ::_thesis: ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) ) hence ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) ) by A2, A3, Th1, Th4; ::_thesis: verum end; end; end; hence ( x = n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) + (sqrt (delta (a,b,c)))) / (2 * a))) or x = n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a)) or x = - (n -root (((- b) - (sqrt (delta (a,b,c)))) / (2 * a))) ) ; ::_thesis: verum end; theorem :: POLYEQ_4:9 for a, b, x being Real for n being Element of NAT st a <> 0 & n is odd & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 holds x = n -root (- (b / a)) proof let a, b, x be Real; ::_thesis: for n being Element of NAT st a <> 0 & n is odd & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 holds x = n -root (- (b / a)) let n be Element of NAT ; ::_thesis: ( a <> 0 & n is odd & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 implies x = n -root (- (b / a)) ) assume that A1: a <> 0 and A2: n is odd and A3: Polynom (a,b,0,(x |^ n)) = 0 ; ::_thesis: ( x = 0 or x = n -root (- (b / a)) ) now__::_thesis:_(_x_=_0_or_x_=_n_-root_(-_(b_/_a))_) percases ( x |^ n = 0 or x |^ n = - (b / a) ) by A1, A3, Th5; suppose x |^ n = 0 ; ::_thesis: ( x = 0 or x = n -root (- (b / a)) ) hence ( x = 0 or x = n -root (- (b / a)) ) by PREPOWER:5; ::_thesis: verum end; suppose x |^ n = - (b / a) ; ::_thesis: ( x = 0 or x = n -root (- (b / a)) ) hence ( x = 0 or x = n -root (- (b / a)) ) by A2, POWER:4; ::_thesis: verum end; end; end; hence ( x = 0 or x = n -root (- (b / a)) ) ; ::_thesis: verum end; theorem :: POLYEQ_4:10 for a, b, x being Real for n being Element of NAT st a <> 0 & b / a < 0 & n is even & n >= 1 & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 & not x = n -root (- (b / a)) holds x = - (n -root (- (b / a))) proof let a, b, x be Real; ::_thesis: for n being Element of NAT st a <> 0 & b / a < 0 & n is even & n >= 1 & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 & not x = n -root (- (b / a)) holds x = - (n -root (- (b / a))) let n be Element of NAT ; ::_thesis: ( a <> 0 & b / a < 0 & n is even & n >= 1 & Polynom (a,b,0,(x |^ n)) = 0 & not x = 0 & not x = n -root (- (b / a)) implies x = - (n -root (- (b / a))) ) assume that A1: a <> 0 and A2: b / a < 0 and A3: ( n is even & n >= 1 ) and A4: Polynom (a,b,0,(x |^ n)) = 0 ; ::_thesis: ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) ) A5: - (b / a) > 0 by A2, XREAL_1:58; now__::_thesis:_(_x_=_0_or_x_=_n_-root_(-_(b_/_a))_or_x_=_-_(n_-root_(-_(b_/_a)))_) percases ( x |^ n = 0 or x |^ n = - (b / a) ) by A1, A4, Th5; suppose x |^ n = 0 ; ::_thesis: ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) ) hence ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) ) by PREPOWER:5; ::_thesis: verum end; suppose x |^ n = - (b / a) ; ::_thesis: ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) ) hence ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) ) by A3, A5, Th4; ::_thesis: verum end; end; end; hence ( x = 0 or x = n -root (- (b / a)) or x = - (n -root (- (b / a))) ) ; ::_thesis: verum end; theorem Th11: :: POLYEQ_4:11 for a, b being Real holds ( (a |^ 3) + (b |^ 3) = (a + b) * (((a ^2) - (a * b)) + (b ^2)) & (a |^ 5) + (b |^ 5) = (a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) ) proof let a, b be Real; ::_thesis: ( (a |^ 3) + (b |^ 3) = (a + b) * (((a ^2) - (a * b)) + (b ^2)) & (a |^ 5) + (b |^ 5) = (a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) ) A1: (a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) = (((((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) .= (((((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) by NEWTON:5 .= (((((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) by NEWTON:8 .= (((((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))))) - ((a * (a * (b |^ 3))) + (b * (a * (b |^ 3))))) + ((a * (b |^ 4)) + (b * (b |^ 4))) .= (((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) by POLYEQ_2:4 .= (((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) by POLYEQ_2:4 .= (((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) by NEWTON:6 .= (((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + ((b |^ 4) * b)) by NEWTON:6 .= (((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) by NEWTON:6 .= (((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) by NEWTON:5 .= (((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) by NEWTON:5 .= (((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ 5)) by NEWTON:6 .= (((a |^ 5) + ((a |^ 2) * (b |^ 3))) - (((a |^ 2) * (b |^ 3)) + (a * (b |^ 4)))) + ((a * (b |^ 4)) + (b |^ 5)) by NEWTON:6 .= (a |^ 5) + (b |^ 5) ; (((a ^2) - (a * b)) + (b ^2)) * (a + b) = ((((a ^2) * a) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b)))) + (((a * (b ^2)) + (b * (b ^2))) + (0 * (b ^2))) .= (((a |^ 3) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b)))) + ((a * (b ^2)) + (b * (b ^2))) by POLYEQ_2:4 .= (((a |^ 3) + (b * (a ^2))) - (((a ^2) * b) + ((b * b) * a))) + ((a * (b ^2)) + (b |^ 3)) by POLYEQ_2:4 .= (a |^ 3) + (b |^ 3) ; hence ( (a |^ 3) + (b |^ 3) = (a + b) * (((a ^2) - (a * b)) + (b ^2)) & (a |^ 5) + (b |^ 5) = (a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) ) by A1; ::_thesis: verum end; theorem :: POLYEQ_4:12 for a, b, x being Real st a <> 0 & ((b ^2) - ((2 * a) * b)) - (3 * (a ^2)) >= 0 & Polynom (a,b,b,a,x) = 0 & not x = - 1 & not x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) holds x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) proof let a, b, x be Real; ::_thesis: ( a <> 0 & ((b ^2) - ((2 * a) * b)) - (3 * (a ^2)) >= 0 & Polynom (a,b,b,a,x) = 0 & not x = - 1 & not x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) implies x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) assume that A1: ( a <> 0 & ((b ^2) - ((2 * a) * b)) - (3 * (a ^2)) >= 0 ) and A2: Polynom (a,b,b,a,x) = 0 ; ::_thesis: ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) (((a * (x |^ 3)) + (b * (x ^2))) + (b * x)) + a = 0 by A2, POLYEQ_1:def_4; then (((x |^ 3) + 1) * a) + ((((x ^2) + x) + 0) * b) = 0 ; then (((x |^ 3) + (1 to_power 3)) * a) + (((x + 1) * x) * b) = 0 by POWER:26; then (((x + 1) * (((x ^2) - (x * 1)) + (1 ^2))) * a) + (((x + 1) * x) * b) = 0 by Th11; then A3: (((((x ^2) * a) - (x * a)) + (x * b)) + a) * (x + 1) = 0 ; now__::_thesis:_(_(_x_+_1_=_0_&_(_x_=_-_1_or_x_=_((a_-_b)_+_(sqrt_(((b_^2)_-_((2_*_a)_*_b))_-_(3_*_(a_^2)))))_/_(2_*_a)_or_x_=_((a_-_b)_-_(sqrt_(((b_^2)_-_((2_*_a)_*_b))_-_(3_*_(a_^2)))))_/_(2_*_a)_)_)_or_(_((a_*_(x_^2))_-_((a_-_b)_*_x))_+_a_=_0_&_(_x_=_-_1_or_x_=_((a_-_b)_+_(sqrt_(((b_^2)_-_((2_*_a)_*_b))_-_(3_*_(a_^2)))))_/_(2_*_a)_or_x_=_((a_-_b)_-_(sqrt_(((b_^2)_-_((2_*_a)_*_b))_-_(3_*_(a_^2)))))_/_(2_*_a)_)_)_) percases ( x + 1 = 0 or ((a * (x ^2)) - ((a - b) * x)) + a = 0 ) by A3, XCMPLX_1:6; case x + 1 = 0 ; ::_thesis: ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) hence ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) ; ::_thesis: verum end; caseA4: ((a * (x ^2)) - ((a - b) * x)) + a = 0 ; ::_thesis: ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) A5: delta (a,((- a) + b),a) = (((- a) + b) ^2) - ((4 * a) * a) by QUIN_1:def_1 .= ((b ^2) - ((2 * a) * b)) + ((- (4 - 1)) * (a ^2)) ; ((a * (x ^2)) + (((- a) + b) * x)) + a = 0 by A4; then Polynom (a,((- a) + b),a,x) = 0 by POLYEQ_1:def_2; then ( x = ((- ((- a) + b)) + (sqrt (delta (a,((- a) + b),a)))) / (2 * a) or x = ((- ((- a) + b)) - (sqrt (delta (a,((- a) + b),a)))) / (2 * a) ) by A1, A5, POLYEQ_1:5; hence ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) by A5; ::_thesis: verum end; end; end; hence ( x = - 1 or x = ((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) or x = ((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) ) ; ::_thesis: verum end; definition let a, b, c, d, e, f, x be complex number ; func Polynom (a,b,c,d,e,f,x) -> set equals :: POLYEQ_4:def 1 (((((a * (x |^ 5)) + (b * (x |^ 4))) + (c * (x |^ 3))) + (d * (x ^2))) + (e * x)) + f; coherence (((((a * (x |^ 5)) + (b * (x |^ 4))) + (c * (x |^ 3))) + (d * (x ^2))) + (e * x)) + f is set ; end; :: deftheorem defines Polynom POLYEQ_4:def_1_:_ for a, b, c, d, e, f, x being complex number holds Polynom (a,b,c,d,e,f,x) = (((((a * (x |^ 5)) + (b * (x |^ 4))) + (c * (x |^ 3))) + (d * (x ^2))) + (e * x)) + f; registration let a, b, c, d, e, f, x be complex number ; cluster Polynom (a,b,c,d,e,f,x) -> complex ; coherence Polynom (a,b,c,d,e,f,x) is complex ; end; registration let a, b, c, d, e, f, x be real number ; cluster Polynom (a,b,c,d,e,f,x) -> real ; coherence Polynom (a,b,c,d,e,f,x) is real ; end; theorem :: POLYEQ_4:13 for a, b, c, x being Real st a <> 0 & (((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c) > 0 & Polynom (a,b,c,c,b,a,x) = 0 holds for y1, y2 being Real st y1 = ((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & y2 = ((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & not x = - 1 & not x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 & not x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 & not x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 holds x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 proof let a, b, c, x be Real; ::_thesis: ( a <> 0 & (((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c) > 0 & Polynom (a,b,c,c,b,a,x) = 0 implies for y1, y2 being Real st y1 = ((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & y2 = ((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & not x = - 1 & not x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 & not x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 & not x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 holds x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) assume that A1: ( a <> 0 & (((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c) > 0 ) and A2: Polynom (a,b,c,c,b,a,x) = 0 ; ::_thesis: for y1, y2 being Real st y1 = ((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & y2 = ((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & not x = - 1 & not x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 & not x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 & not x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 holds x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 let y1, y2 be Real; ::_thesis: ( y1 = ((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & y2 = ((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) & not x = - 1 & not x = (y1 + (sqrt (delta (1,(- y1),1)))) / 2 & not x = (y2 + (sqrt (delta (1,(- y2),1)))) / 2 & not x = (y1 - (sqrt (delta (1,(- y1),1)))) / 2 implies x = (y2 - (sqrt (delta (1,(- y2),1)))) / 2 ) assume that A3: y1 = ((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) and A4: y2 = ((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * c)))) / (2 * a) ; ::_thesis: ( x = - 1 or 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: 0 = ((((x |^ 5) + 1) * a) + ((((x |^ 4) + x) + 0) * b)) + (((c * (x |^ 3)) + (c * (x ^2))) + (0 * c)) by A2 .= ((((x |^ 5) + (1 |^ 5)) * a) + (((x |^ (3 + 1)) + x) * b)) + (((x |^ 3) + (x ^2)) * c) by NEWTON:10 .= ((((x |^ 5) + (1 |^ 5)) * a) + ((((x |^ 3) * x) + x) * b)) + (((x |^ (2 + 1)) + (x ^2)) * c) by NEWTON:6 .= ((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0) * x) * b)) + ((((x * (x |^ (1 + 1))) + (1 * (x ^2))) + (0 * (x ^2))) * c) by NEWTON:6 .= ((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0) * x) * b)) + ((((x * ((x |^ 1) * x)) + (1 * (x ^2))) + (0 * (x ^2))) * c) by NEWTON:6 .= ((((x |^ 5) + (1 |^ 5)) * a) + (((((x |^ 3) + 1) + 0) * x) * b)) + ((((x * (x ^2)) + (1 * (x ^2))) + (0 * (x ^2))) * c) by NEWTON:5 .= ((((x + 1) * (((((x |^ 4) - ((x |^ 3) * 1)) + ((x |^ 2) * (1 |^ 2))) - (x * (1 |^ 3))) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0) * (x ^2)) * c) by Th11 .= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + ((x |^ 2) * 1)) - (x * (1 |^ 3))) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0) * (x ^2)) * c) by NEWTON:10 .= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - (x * 1)) + (1 |^ 4))) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0) * (x ^2)) * c) by NEWTON:10 .= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x |^ 3) + 1) * x) * b)) + ((((x + 1) + 0) * (x ^2)) * c) by NEWTON:10 .= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x |^ 3) + (1 |^ 3)) * x) * b)) + (((x + 1) * (x ^2)) * c) by NEWTON:10 .= ((((x + 1) * (((((x |^ 4) - (x |^ 3)) + (x |^ 2)) - x) + 1)) * a) + ((((x + 1) * (((x ^2) - (x * 1)) + (1 ^2))) * x) * b)) + (((x + 1) * (x ^2)) * c) by Th11 .= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + (((((x * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x * x) * c)) * (x + 1) .= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x * x) * c)) * (x + 1) by NEWTON:5 .= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + (((x |^ 1) * x) * c)) * (x + 1) by NEWTON:5 .= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((((x |^ 1) * x) * x) * b) - ((x * x) * b)) + (b * x))) + ((x |^ (1 + 1)) * c)) * (x + 1) by NEWTON:6 .= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + (((((x |^ (1 + 1)) * x) * b) - ((x * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1) by NEWTON:6 .= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ (2 + 1)) * b) - ((x * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1) by NEWTON:6 .= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ 3) * b) - (((x |^ 1) * x) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1) by NEWTON:5 .= (((((((a * (x |^ 4)) - (a * (x |^ 3))) + (a * (x |^ 2))) - (a * x)) + a) + ((((x |^ 3) * b) - ((x |^ (1 + 1)) * b)) + (b * x))) + ((x |^ 2) * c)) * (x + 1) by NEWTON:6 .= (((((a * (x |^ 4)) - ((a - b) * (x |^ 3))) + (((a + c) - b) * (x |^ 2))) - ((a - b) * x)) + a) * (x + 1) ; now__::_thesis:_(_(_x_+_1_=_0_&_(_x_=_-_1_or_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_)_)_or_(_((((a_*_(x_|^_4))_-_((a_-_b)_*_(x_|^_3)))_+_(((a_+_c)_-_b)_*_(x_|^_2)))_-_((a_-_b)_*_x))_+_a_=_0_&_(_x_=_-_1_or_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_)_)_) percases ( x + 1 = 0 or ((((a * (x |^ 4)) - ((a - b) * (x |^ 3))) + (((a + c) - b) * (x |^ 2))) - ((a - b) * x)) + a = 0 ) by A5, XCMPLX_1:6; case x + 1 = 0 ; ::_thesis: ( x = - 1 or 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 ) hence ( x = - 1 or 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 ) ; ::_thesis: verum end; caseA6: ((((a * (x |^ 4)) - ((a - b) * (x |^ 3))) + (((a + c) - b) * (x |^ 2))) - ((a - b) * x)) + a = 0 ; ::_thesis: ( x = - 1 or 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 ) set y = x + (1 / x); 0 = ((((a * (x |^ 4)) + (((- a) + b) * (x |^ 3))) + (((a + c) - b) * (x |^ (1 + 1)))) + (((- a) + b) * x)) + a by A6 .= ((((a * (x |^ 4)) + (((- a) + b) * (x |^ 3))) + (((a + c) - b) * ((x |^ 1) * x))) + (((- a) + b) * x)) + a by NEWTON:6 .= ((((a * (x |^ 4)) + (((- a) + b) * (x |^ 3))) + (((a + c) - b) * (x ^2))) + (((- a) + b) * x)) + a by NEWTON:5 ; then A7: Polynom (a,((- a) + b),((a + c) - b),((- a) + b),a,x) = 0 by POLYEQ_2:def_1; ( x + (1 / x) = x + (1 / x) & y1 = ((- ((- a) + b)) + (sqrt (((((- a) + b) ^2) - ((4 * a) * ((a + c) - b))) + (8 * (a ^2))))) / (2 * a) ) by A3; hence ( x = - 1 or 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, A4, A7, POLYEQ_2:3; ::_thesis: verum end; end; end; hence ( x = - 1 or 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 ) ; ::_thesis: verum end; theorem Th14: :: POLYEQ_4:14 for x, y, p, q being Real st x + y = p & x * y = q & (p ^2) - (4 * q) >= 0 & not ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) holds ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) proof let x, y, p, q be Real; ::_thesis: ( x + y = p & x * y = q & (p ^2) - (4 * q) >= 0 & not ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) implies ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) assume that A1: x + y = p and A2: x * y = q and A3: (p ^2) - (4 * q) >= 0 ; ::_thesis: ( ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) A4: delta (1,(- p),q) = ((- p) ^2) - ((4 * 1) * q) by QUIN_1:def_1 .= (p ^2) - (4 * q) ; ((1 * (y ^2)) + ((- p) * y)) + q = 0 by A1, A2; then Polynom (1,(- p),q,y) = 0 by POLYEQ_1:def_2; then A5: ( y = ((- (- p)) + (sqrt (delta (1,(- p),q)))) / (2 * 1) or y = ((- (- p)) - (sqrt (delta (1,(- p),q)))) / (2 * 1) ) by A3, A4, POLYEQ_1:5; now__::_thesis:_(_(_x_=_(p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2_&_y_=_(p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2_)_or_(_x_=_(p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2_&_y_=_(p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2_)_) percases ( y = (p + (sqrt (delta (1,(- p),q)))) / 2 or y = (p - (sqrt (delta (1,(- p),q)))) / 2 ) by A5; supposeA6: y = (p + (sqrt (delta (1,(- p),q)))) / 2 ; ::_thesis: ( ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) then x = ((p * 2) / 2) - ((p / 2) + ((sqrt (delta (1,(- p),q))) / 2)) by A1 .= ((p * 2) / 2) - ((p / 2) + ((sqrt ((p ^2) - (4 * q))) / 2)) by A4 ; hence ( ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) by A4, A6; ::_thesis: verum end; supposeA7: y = (p - (sqrt (delta (1,(- p),q)))) / 2 ; ::_thesis: ( ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) then x = p - (((p - (sqrt (delta (1,(- p),q)))) + 0) / 2) by A1 .= p - (((p - (sqrt ((p ^2) - (4 * q)))) + 0) / 2) by A4 ; hence ( ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) by A4, A7; ::_thesis: verum end; end; end; hence ( ( x = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) ; ::_thesis: verum end; theorem :: POLYEQ_4:15 for x, y, p, q being Real for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & n is odd & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) holds ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) proof let x, y, p, q be Real; ::_thesis: for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & n is odd & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) holds ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) let n be Element of NAT ; ::_thesis: ( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & n is odd & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) implies ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) ) assume that A1: ( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 ) and A2: n is odd ; ::_thesis: ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) ) ( ( x |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) by A1, Th14; hence ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) ) by A2, POWER:4; ::_thesis: verum end; theorem :: POLYEQ_4:16 for x, y, p, q being Real for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & p > 0 & q > 0 & n is even & n >= 1 & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) holds ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) proof let x, y, p, q be Real; ::_thesis: for n being Element of NAT st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & p > 0 & q > 0 & n is even & n >= 1 & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) holds ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) let n be Element of NAT ; ::_thesis: ( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2) - (4 * q) >= 0 & p > 0 & q > 0 & n is even & n >= 1 & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) & not ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) implies ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) ) assume A1: ( (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q ) ; ::_thesis: ( not (p ^2) - (4 * q) >= 0 or not p > 0 or not q > 0 or not n is even or not n >= 1 or ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) ) assume that A2: (p ^2) - (4 * q) >= 0 and A3: p > 0 and A4: q > 0 and A5: ( n is even & n >= 1 ) ; ::_thesis: ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) ) - (- (4 * q)) > 0 by A4, XREAL_1:129; then - (4 * q) < 0 ; then (p ^2) + (- (4 * q)) < (p ^2) + 0 by XREAL_1:8; then sqrt ((p ^2) - (4 * q)) < sqrt (p ^2) by A2, SQUARE_1:27; then sqrt ((p ^2) - (4 * q)) < p by A3, SQUARE_1:22; then - (sqrt ((p ^2) - (4 * q))) > - p by XREAL_1:24; then (- (sqrt ((p ^2) - (4 * q)))) + p > ((- p) + 0) + p by XREAL_1:8; then A6: ((0 + p) - (sqrt ((p ^2) - (4 * q)))) / 2 > 0 by XREAL_1:139; A7: delta (1,(- p),q) = ((- p) ^2) - ((4 * 1) * q) by QUIN_1:def_1 .= (p ^2) - (4 * q) ; then 0 <= sqrt (delta (1,(- p),q)) by A2, SQUARE_1:17, SQUARE_1:26; then (- (- p)) + (sqrt (delta (1,(- p),q))) > 0 + 0 by A3, XREAL_1:8; then A8: ((0 + p) + (sqrt ((p ^2) - (4 * q)))) / 2 > 0 by A7, XREAL_1:139; now__::_thesis:_(_(_x_=_n_-root_((p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2)_&_y_=_n_-root_((p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2)_)_or_(_x_=_-_(n_-root_((p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2))_&_y_=_n_-root_((p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2)_)_or_(_x_=_n_-root_((p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2)_&_y_=_-_(n_-root_((p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2))_)_or_(_x_=_-_(n_-root_((p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2))_&_y_=_-_(n_-root_((p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2))_)_or_(_x_=_n_-root_((p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2)_&_y_=_n_-root_((p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2)_)_or_(_x_=_-_(n_-root_((p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2))_&_y_=_n_-root_((p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2)_)_or_(_x_=_n_-root_((p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2)_&_y_=_-_(n_-root_((p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2))_)_or_(_x_=_-_(n_-root_((p_-_(sqrt_((p_^2)_-_(4_*_q))))_/_2))_&_y_=_-_(n_-root_((p_+_(sqrt_((p_^2)_-_(4_*_q))))_/_2))_)_) percases ( ( x |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) or ( x |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ) by A1, A2, Th14; suppose ( x |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 ) ; ::_thesis: ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) ) hence ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) ) by A5, A8, A6, Th4; ::_thesis: verum end; suppose ( x |^ n = (p - (sqrt ((p ^2) - (4 * q)))) / 2 & y |^ n = (p + (sqrt ((p ^2) - (4 * q)))) / 2 ) ; ::_thesis: ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) ) hence ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) ) by A5, A8, A6, Th4; ::_thesis: verum end; end; end; hence ( ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2) ) or ( x = n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) or ( x = - (n -root ((p - (sqrt ((p ^2) - (4 * q)))) / 2)) & y = - (n -root ((p + (sqrt ((p ^2) - (4 * q)))) / 2)) ) ) ; ::_thesis: verum end; theorem :: POLYEQ_4:17 for x, y, a, b being Real for n being Element of NAT st (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b & n is even & n >= 1 & a + b > 0 & a - b > 0 & not ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) & not ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) & not ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) holds ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) proof let x, y, a, b be Real; ::_thesis: for n being Element of NAT st (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b & n is even & n >= 1 & a + b > 0 & a - b > 0 & not ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) & not ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) & not ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) holds ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) let n be Element of NAT ; ::_thesis: ( (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b & n is even & n >= 1 & a + b > 0 & a - b > 0 & not ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) & not ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) & not ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) implies ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) ) assume A1: ( (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b ) ; ::_thesis: ( not n is even or not n >= 1 or not a + b > 0 or not a - b > 0 or ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) or ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) or ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) or ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) ) assume that A2: ( n is even & n >= 1 ) and A3: ( a + b > 0 & a - b > 0 ) ; ::_thesis: ( ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) or ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) or ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) or ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) ) ( (a + b) / 2 > 0 & (a - b) / 2 > 0 ) by A3, XREAL_1:139; hence ( ( x = n -root ((a + b) / 2) & y = n -root ((a - b) / 2) ) or ( x = n -root ((a + b) / 2) & y = - (n -root ((a - b) / 2)) ) or ( x = - (n -root ((a + b) / 2)) & y = n -root ((a - b) / 2) ) or ( x = - (n -root ((a + b) / 2)) & y = - (n -root ((a - b) / 2)) ) ) by A1, A2, Th4; ::_thesis: verum end; theorem :: POLYEQ_4:18 for a, x, b, y, p being Real for n being Element of NAT st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) holds ( x = n -root (p / a) & y = 0 ) proof let a, x, b, y, p be Real; ::_thesis: for n being Element of NAT st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) holds ( x = n -root (p / a) & y = 0 ) let n be Element of NAT ; ::_thesis: ( (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is odd & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) implies ( x = n -root (p / a) & y = 0 ) ) assume that A1: (a * (x |^ n)) + (b * (y |^ n)) = p and A2: x * y = 0 and A3: n is odd and A4: a * b <> 0 ; ::_thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) consider m being Element of NAT such that A5: n = (2 * m) + 1 by A3, ABIAN:9; 2 * m >= 0 by NAT_1:2; then (2 * m) + 1 >= 0 + 1 by XREAL_1:7; then A6: n > 0 by A5, XXREAL_0:2; now__::_thesis:_(_(_x_=_0_&_y_=_n_-root_(p_/_b)_)_or_(_x_=_n_-root_(p_/_a)_&_y_=_0_)_) percases ( x = 0 or y = 0 ) by A2, XCMPLX_1:6; supposeA7: x = 0 ; ::_thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) then (a * (0 to_power n)) + (b * (y |^ n)) = p by A1; then (a * 0) + (b * (y |^ n)) = p by A6, POWER:def_2; then y |^ n = p / b by A4, XCMPLX_1:89; hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) by A3, A7, POWER:4; ::_thesis: verum end; supposeA8: y = 0 ; ::_thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) then (a * (x |^ n)) + (b * (0 to_power n)) = p by A1; then (a * (x |^ n)) + (b * 0) = p by A6, POWER:def_2; then x |^ n = p / a by A4, XCMPLX_1:89; hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) by A3, A8, POWER:4; ::_thesis: verum end; end; end; hence ( ( x = 0 & y = n -root (p / b) ) or ( x = n -root (p / a) & y = 0 ) ) ; ::_thesis: verum end; theorem :: POLYEQ_4:19 for a, x, b, y, p being Real for n being Element of NAT st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is even & n >= 1 & p / b > 0 & p / a > 0 & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) & not ( x = 0 & y = - (n -root (p / b)) ) & not ( x = n -root (p / a) & y = 0 ) holds ( x = - (n -root (p / a)) & y = 0 ) proof let a, x, b, y, p be Real; ::_thesis: for n being Element of NAT st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is even & n >= 1 & p / b > 0 & p / a > 0 & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) & not ( x = 0 & y = - (n -root (p / b)) ) & not ( x = n -root (p / a) & y = 0 ) holds ( x = - (n -root (p / a)) & y = 0 ) let n be Element of NAT ; ::_thesis: ( (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & n is even & n >= 1 & p / b > 0 & p / a > 0 & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) & not ( x = 0 & y = - (n -root (p / b)) ) & not ( x = n -root (p / a) & y = 0 ) implies ( x = - (n -root (p / a)) & y = 0 ) ) assume that A1: (a * (x |^ n)) + (b * (y |^ n)) = p and A2: x * y = 0 and A3: ( n is even & n >= 1 ) and A4: p / b > 0 and A5: p / a > 0 and A6: a * b <> 0 ; ::_thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) ) n >= 1 by A3; then A7: n > 0 by XXREAL_0:2; percases ( x = 0 or y = 0 ) by A2, XCMPLX_1:6; supposeA8: x = 0 ; ::_thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) ) then (a * (0 to_power n)) + (b * (y |^ n)) = p by A1; then (a * 0) + (b * (y |^ n)) = p by A7, POWER:def_2; then y |^ n = p / b by A6, XCMPLX_1:89; hence ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) ) by A3, A4, A8, Th4; ::_thesis: verum end; supposeA9: y = 0 ; ::_thesis: ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) ) then (a * (x |^ n)) + (b * (0 to_power n)) = p by A1; then (a * (x |^ n)) + (b * 0) = p by A7, POWER:def_2; then x |^ n = p / a by A6, XCMPLX_1:89; hence ( ( x = 0 & y = n -root (p / b) ) or ( x = 0 & y = - (n -root (p / b)) ) or ( x = n -root (p / a) & y = 0 ) or ( x = - (n -root (p / a)) & y = 0 ) ) by A3, A5, A9, Th4; ::_thesis: verum end; end; end; theorem :: POLYEQ_4:20 for a, x, p, y, q being Real for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is odd & p * a <> 0 holds ( x = n -root (p / a) & y = q * (n -root (a / p)) ) proof let a, x, p, y, q be Real; ::_thesis: for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is odd & p * a <> 0 holds ( x = n -root (p / a) & y = q * (n -root (a / p)) ) let n be Element of NAT ; ::_thesis: ( a * (x |^ n) = p & x * y = q & n is odd & p * a <> 0 implies ( x = n -root (p / a) & y = q * (n -root (a / p)) ) ) assume that A1: a * (x |^ n) = p and A2: x * y = q and A3: n is odd and A4: p * a <> 0 ; ::_thesis: ( x = n -root (p / a) & y = q * (n -root (a / p)) ) consider m being Element of NAT such that A5: n = (2 * m) + 1 by A3, ABIAN:9; A6: a <> 0 by A4; then A7: x |^ n = p / a by A1, XCMPLX_1:89; then x = n -root (p / a) by A3, POWER:4; then y * ((n -root (p / a)) * (n -root (a / p))) = q * (n -root (a / p)) by A2; then y * (n -root ((p / a) * (a / p))) = q * (n -root (a / p)) by A3, POWER:11; then y * (n -root ((p / a) * (a * (p ")))) = q * (n -root (a / p)) by XCMPLX_0:def_9; then y * (n -root (((p / a) * a) * (p "))) = q * (n -root (a / p)) ; then y * (n -root (p * (p "))) = q * (n -root (a / p)) by A6, XCMPLX_1:87; then A8: y * (n -root (p / p)) = q * (n -root (a / p)) by XCMPLX_0:def_9; 2 * m >= 0 by NAT_1:2; then A9: (2 * m) + 1 >= 0 + 1 by XREAL_1:7; p <> 0 by A4; then y * (n -root 1) = q * (n -root (a / p)) by A8, XCMPLX_1:60; then y * 1 = q * (n -root (a / p)) by A5, A9, POWER:6; hence ( x = n -root (p / a) & y = q * (n -root (a / p)) ) by A3, A7, POWER:4; ::_thesis: verum end; theorem :: POLYEQ_4:21 for a, x, p, y, q being Real for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is even & n >= 1 & p / a > 0 & a <> 0 & not ( x = n -root (p / a) & y = q * (n -root (a / p)) ) holds ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) proof let a, x, p, y, q be Real; ::_thesis: for n being Element of NAT st a * (x |^ n) = p & x * y = q & n is even & n >= 1 & p / a > 0 & a <> 0 & not ( x = n -root (p / a) & y = q * (n -root (a / p)) ) holds ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) let n be Element of NAT ; ::_thesis: ( a * (x |^ n) = p & x * y = q & n is even & n >= 1 & p / a > 0 & a <> 0 & not ( x = n -root (p / a) & y = q * (n -root (a / p)) ) implies ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) ) assume that A1: a * (x |^ n) = p and A2: x * y = q and A3: ( n is even & n >= 1 ) and A4: p / a > 0 and A5: a <> 0 ; ::_thesis: ( ( x = n -root (p / a) & y = q * (n -root (a / p)) ) or ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) ) A6: x |^ n = p / a by A1, A5, XCMPLX_1:89; (p / a) " > 0 by A4, XREAL_1:122; then 1 / (p / a) > 0 by XCMPLX_1:215; then A7: (1 * a) / p > 0 by XCMPLX_1:77; A8: p <> 0 by A4; percases ( x = n -root (p / a) or x = - (n -root (p / a)) ) by A3, A4, A6, Th4; supposeA9: x = n -root (p / a) ; ::_thesis: ( ( x = n -root (p / a) & y = q * (n -root (a / p)) ) or ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) ) then y * ((n -root (p / a)) * (n -root (a / p))) = q * (n -root (a / p)) by A2; then y * (n -root ((p / a) * (a / p))) = q * (n -root (a / p)) by A4, A3, A7, POWER:11; then y * (n -root ((p / a) * (a * (p ")))) = q * (n -root (a / p)) by XCMPLX_0:def_9; then y * (n -root (((p / a) * a) * (p "))) = q * (n -root (a / p)) ; then y * (n -root (p * (p "))) = q * (n -root (a / p)) by A5, XCMPLX_1:87; then y * (n -root (p / p)) = q * (n -root (a / p)) by XCMPLX_0:def_9; then y * (n -root 1) = q * (n -root (a / p)) by A8, XCMPLX_1:60; then y * 1 = q * (n -root (a / p)) by A3, POWER:6; hence ( ( x = n -root (p / a) & y = q * (n -root (a / p)) ) or ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) ) by A9; ::_thesis: verum end; supposeA10: x = - (n -root (p / a)) ; ::_thesis: ( ( x = n -root (p / a) & y = q * (n -root (a / p)) ) or ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) ) then y * ((n -root (p / a)) * (n -root (a / p))) = - (q * (n -root (a / p))) by A2; then y * (n -root ((p / a) * (a / p))) = - (q * (n -root (a / p))) by A4, A3, A7, POWER:11; then y * (n -root ((p / a) * (a * (p ")))) = - (q * (n -root (a / p))) by XCMPLX_0:def_9; then y * (n -root (((p / a) * a) * (p "))) = - (q * (n -root (a / p))) ; then y * (n -root (p * (p "))) = - (q * (n -root (a / p))) by A5, XCMPLX_1:87; then y * (n -root (p / p)) = - (q * (n -root (a / p))) by XCMPLX_0:def_9; then y * (n -root 1) = - (q * (n -root (a / p))) by A8, XCMPLX_1:60; then y * 1 = - (q * (n -root (a / p))) by A3, POWER:6; hence ( ( x = n -root (p / a) & y = q * (n -root (a / p)) ) or ( x = - (n -root (p / a)) & y = - (q * (n -root (a / p))) ) ) by A10; ::_thesis: verum end; end; end; theorem :: POLYEQ_4:22 for a, x being Real st a > 0 & a <> 1 & a to_power x = 1 holds x = 0 proof let a, x be Real; ::_thesis: ( a > 0 & a <> 1 & a to_power x = 1 implies x = 0 ) assume that A1: ( a > 0 & a <> 1 ) and A2: a to_power x = 1 ; ::_thesis: x = 0 x = log (a,1) by A1, A2, POWER:def_3; hence x = 0 by A1, POWER:51; ::_thesis: verum end; theorem :: POLYEQ_4:23 for a, x being Real st a > 0 & a <> 1 & a to_power x = a holds x = 1 proof let a, x be Real; ::_thesis: ( a > 0 & a <> 1 & a to_power x = a implies x = 1 ) assume that A1: ( a > 0 & a <> 1 ) and A2: a to_power x = a ; ::_thesis: x = 1 x = log (a,a) by A1, A2, POWER:def_3; hence x = 1 by A1, POWER:52; ::_thesis: verum end; theorem :: POLYEQ_4:24 for a, b, x being Real st a > 0 & a <> 1 & x > 0 & log (a,x) = 0 holds x = 1 proof let a, b, x be Real; ::_thesis: ( a > 0 & a <> 1 & x > 0 & log (a,x) = 0 implies x = 1 ) assume ( a > 0 & a <> 1 & x > 0 & log (a,x) = 0 ) ; ::_thesis: x = 1 then a to_power 0 = x by POWER:def_3; hence x = 1 by POWER:24; ::_thesis: verum end; theorem :: POLYEQ_4:25 for a, b, x being Real st a > 0 & a <> 1 & x > 0 & log (a,x) = 1 holds x = a proof let a, b, x be Real; ::_thesis: ( a > 0 & a <> 1 & x > 0 & log (a,x) = 1 implies x = a ) assume ( a > 0 & a <> 1 & x > 0 & log (a,x) = 1 ) ; ::_thesis: x = a then a to_power 1 = x by POWER:def_3; hence x = a by POWER:25; ::_thesis: verum end;