:: 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;