:: POLYEQ_4 semantic presentation

theorem Th1: :: POLYEQ_4:1

for a, b, c being Real st a <> 0 & 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 end;

theorem :: POLYEQ_4:2

for a, b, c being Real st a <> 0 & 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 end;

theorem :: POLYEQ_4:3

for a, c, b being Real st a <> 0 & c / a < 0 & not ( ((- b) + (sqrt (delta a,b,c))) / (2 * a) > 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) < 0 ) holds
( ((- b) + (sqrt (delta a,b,c))) / (2 * a) < 0 & ((- b) - (sqrt (delta a,b,c))) / (2 * a) > 0 )

proof end;

theorem Th4: :: POLYEQ_4:4

for a, x being Real
for n being Nat st a > 0 & ex m being Nat st
( n = 2 * m & m >= 1 ) & x |^ n = a & not x = n -root a holds
x = - (n -root a)

proof end;

theorem Th5: :: POLYEQ_4:5

for a, b, x being Real st a <> 0 & Poly2 a,b,0,x = 0 & not x = 0 holds
x = - (b / a)

proof end;

theorem :: POLYEQ_4:6

for a, x being Real st a <> 0 & Poly2 a,0,0,x = 0 holds
x = 0

proof end;

theorem :: POLYEQ_4:7

for a, b, c, x being Real
for n being Nat st a <> 0 & ex m being Nat st n = (2 * m) + 1 & delta a,b,c >= 0 & Poly2 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 end;

theorem :: POLYEQ_4:8

for a, b, c, x being Real
for n being Nat st a <> 0 & b / a < 0 & c / a > 0 & ex m being Nat st
( n = 2 * m & m >= 1 ) & delta a,b,c >= 0 & Poly2 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 end;

theorem :: POLYEQ_4:9

for a, b, x being Real
for n being Nat st a <> 0 & ex m being Nat st n = (2 * m) + 1 & Poly2 a,b,0,(x |^ n) = 0 & not x = 0 holds
x = n -root (- (b / a))

proof end;

theorem :: POLYEQ_4:10

for a, b, x being Real
for n being Nat st a <> 0 & b / a < 0 & ex m being Nat st
( n = 2 * m & m >= 1 ) & Poly2 a,b,0,(x |^ n) = 0 & not x = 0 & not x = n -root (- (b / a)) holds
x = - (n -root (- (b / a)))

proof 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 end;

theorem :: POLYEQ_4:12

for a, b, x being Real st a <> 0 & ((b ^2 ) - ((2 * a) * b)) - (3 * (a ^2 )) >= 0 & Poly3 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 end;

definition

let a, b, c, d, e, f, x be Real;
func Poly5 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 ;

end;

:: deftheorem defines Poly5 POLYEQ_4:def 1 :

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 & Poly5 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 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 end;

theorem :: POLYEQ_4:15

for x, y, p, q being Real
for n being Nat st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2 ) - (4 * q) >= 0 & ex m being Nat st n = (2 * m) + 1 & 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 end;

theorem :: POLYEQ_4:16

for x, y, p, q being Real
for n being Nat st (x |^ n) + (y |^ n) = p & (x |^ n) * (y |^ n) = q & (p ^2 ) - (4 * q) >= 0 & p > 0 & q > 0 & ex m being Nat st
( n = 2 * m & m >= 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 end;

theorem :: POLYEQ_4:17

canceled;

theorem :: POLYEQ_4:18

for x, y, a, b being Real
for n being Nat st (x |^ n) + (y |^ n) = a & (x |^ n) - (y |^ n) = b & ex m being Nat st
( n = 2 * m & m >= 1 ) & a > 0 & 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 end;

theorem :: POLYEQ_4:19

for a, x, b, y, p being Real
for n being Nat st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & ex m being Nat st n = (2 * m) + 1 & a * b <> 0 & not ( x = 0 & y = n -root (p / b) ) holds
( x = n -root (p / a) & y = 0 )

proof end;

theorem :: POLYEQ_4:20

for a, x, b, y, p being Real
for n being Nat st (a * (x |^ n)) + (b * (y |^ n)) = p & x * y = 0 & ex m being Nat st
( n = 2 * m & m >= 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 end;

theorem :: POLYEQ_4:21

for a, x, p, y, q being Real
for n being Nat st a * (x |^ n) = p & x * y = q & ex m being Nat st n = (2 * m) + 1 & p * a <> 0 holds
( x = n -root (p / a) & y = q * (n -root (a / p)) )

proof end;

theorem :: POLYEQ_4:22

for a, x, p, y, q being Real
for n being Nat st a * (x |^ n) = p & x * y = q & ex m being Nat st
( n = 2 * m & m >= 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 end;

theorem :: POLYEQ_4:23

canceled;

theorem :: POLYEQ_4:24

for a, x being Real st a > 0 & a <> 1 & a to_power x = 1 holds
x = 0

proof end;

theorem :: POLYEQ_4:25

for a, x being Real st a > 0 & a <> 1 & a to_power x = a holds
x = 1

proof end;

theorem :: POLYEQ_4:26

canceled;

theorem :: POLYEQ_4:27

for a, b, x being Real st a > 0 & a <> 1 & x > 0 & log a,x = 0 holds
x = 1

proof end;

theorem :: POLYEQ_4:28

for a, b, x being Real st a > 0 & a <> 1 & x > 0 & log a,x = 1 holds
x = a

proof end;