:: POLYEQ_4 semantic presentation

theorem Th1: :: POLYEQ_4:1

for b₁, b₂, b₃ being Real st b₁ <> 0 & b₂ / b₁ < 0 & b₃ / b₁ > 0 & delta b₁,b₂,b₃ >= 0 holds
( ((- b₂) + (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) > 0 & ((- b₂) - (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) > 0 )

proof end;

theorem Th2: :: POLYEQ_4:2

for b₁, b₂, b₃ being Real st b₁ <> 0 & b₂ / b₁ > 0 & b₃ / b₁ > 0 & delta b₁,b₂,b₃ >= 0 holds
( ((- b₂) + (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) < 0 & ((- b₂) - (sqrt (delta b₁,b₂,b₃))) / (2 * b₁) < 0 )

proof end;

theorem Th3: :: POLYEQ_4:3

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

proof end;

theorem Th4: :: POLYEQ_4:4

for b₁, b₂ being Real
for b₃ being Nat st b₁ > 0 & ex b₄ being Nat st
( b₃ = 2 * b₄ & b₄ >= 1 ) & b₂ |^ b₃ = b₁ & not b₂ = b₃ -root b₁ holds
b₂ = - (b₃ -root b₁)

proof end;

theorem Th5: :: POLYEQ_4:5

for b₁, b₂, b₃ being Real st b₁ <> 0 & Poly2 b₁,b₂,0,b₃ = 0 & not b₃ = 0 holds
b₃ = - (b₂ / b₁)

proof end;

theorem Th6: :: POLYEQ_4:6

for b₁, b₂ being Real st b₁ <> 0 & Poly2 b₁,0,0,b₂ = 0 holds
b₂ = 0

proof end;

theorem Th7: :: POLYEQ_4:7

for b₁, b₂, b₃, b₄ being Real
for b₅ being Nat st b₁ <> 0 & ex b₆ being Nat st b₅ = (2 * b₆) + 1 & delta b₁,b₂,b₃ >= 0 & Poly2 b₁,b₂,b₃,(b₄ |^ b₅) = 0 & not b₄ = b₅ -root (((- b₂) + (sqrt (delta b₁,b₂,b₃))) / (2 * b₁)) holds
b₄ = b₅ -root (((- b₂) - (sqrt (delta b₁,b₂,b₃))) / (2 * b₁))

proof end;

theorem Th8: :: POLYEQ_4:8

for b₁, b₂, b₃, b₄ being Real
for b₅ being Nat st b₁ <> 0 & b₂ / b₁ < 0 & b₃ / b₁ > 0 & ex b₆ being Nat st
( b₅ = 2 * b₆ & b₆ >= 1 ) & delta b₁,b₂,b₃ >= 0 & Poly2 b₁,b₂,b₃,(b₄ |^ b₅) = 0 & not b₄ = b₅ -root (((- b₂) + (sqrt (delta b₁,b₂,b₃))) / (2 * b₁)) & not b₄ = - (b₅ -root (((- b₂) + (sqrt (delta b₁,b₂,b₃))) / (2 * b₁))) & not b₄ = b₅ -root (((- b₂) - (sqrt (delta b₁,b₂,b₃))) / (2 * b₁)) holds
b₄ = - (b₅ -root (((- b₂) - (sqrt (delta b₁,b₂,b₃))) / (2 * b₁)))

proof end;

theorem Th9: :: POLYEQ_4:9

for b₁, b₂, b₃ being Real
for b₄ being Nat st b₁ <> 0 & ex b₅ being Nat st b₄ = (2 * b₅) + 1 & Poly2 b₁,b₂,0,(b₃ |^ b₄) = 0 & not b₃ = 0 holds
b₃ = b₄ -root (- (b₂ / b₁))

proof end;

theorem Th10: :: POLYEQ_4:10

for b₁, b₂, b₃ being Real
for b₄ being Nat st b₁ <> 0 & b₂ / b₁ < 0 & ex b₅ being Nat st
( b₄ = 2 * b₅ & b₅ >= 1 ) & Poly2 b₁,b₂,0,(b₃ |^ b₄) = 0 & not b₃ = 0 & not b₃ = b₄ -root (- (b₂ / b₁)) holds
b₃ = - (b₄ -root (- (b₂ / b₁)))

proof end;

theorem Th11: :: POLYEQ_4:11

for b₁, b₂ being Real holds
( (b₁ |^ 3) + (b₂ |^ 3) = (b₁ + b₂) * (((b₁ ^2 ) - (b₁ * b₂)) + (b₂ ^2 )) & (b₁ |^ 5) + (b₂ |^ 5) = (b₁ + b₂) * (((((b₁ |^ 4) - ((b₁ |^ 3) * b₂)) + ((b₁ |^ 2) * (b₂ |^ 2))) - (b₁ * (b₂ |^ 3))) + (b₂ |^ 4)) )

proof end;

theorem Th12: :: POLYEQ_4:12

for b₁, b₂, b₃ being Real st b₁ <> 0 & ((b₂ ^2 ) - ((2 * b₁) * b₂)) - (3 * (b₁ ^2 )) >= 0 & Poly3 b₁,b₂,b₂,b₁,b₃ = 0 & not b₃ = - 1 & not b₃ = ((b₁ - b₂) + (sqrt (((b₂ ^2 ) - ((2 * b₁) * b₂)) - (3 * (b₁ ^2 ))))) / (2 * b₁) holds
b₃ = ((b₁ - b₂) - (sqrt (((b₂ ^2 ) - ((2 * b₁) * b₂)) - (3 * (b₁ ^2 ))))) / (2 * b₁)

proof end;

definition

let c₁, c₂, c₃, c₄, c₅, c₆, c₇ be Real;
func Poly5 c₁,c₂,c₃,c₄,c₅,c₆,c₇ -> set equals :: POLYEQ_4:def 1
(((((a₁ * (a₇ |^ 5)) + (a₂ * (a₇ |^ 4))) + (a₃ * (a₇ |^ 3))) + (a₄ * (a₇ ^2 ))) + (a₅ * a₇)) + a₆;
coherence ;

end;

:: deftheorem Def1 defines Poly5 POLYEQ_4:def 1 :

theorem Th13: :: POLYEQ_4:13

for b₁, b₂, b₃, b₄ being Real st b₁ <> 0 & (((b₂ ^2 ) + ((2 * b₁) * b₂)) + (5 * (b₁ ^2 ))) - ((4 * b₁) * b₃) > 0 & Poly5 b₁,b₂,b₃,b₃,b₂,b₁,b₄ = 0 holds
for b₅, b₆ being Real st b₅ = ((b₁ - b₂) + (sqrt ((((b₂ ^2 ) + ((2 * b₁) * b₂)) + (5 * (b₁ ^2 ))) - ((4 * b₁) * b₃)))) / (2 * b₁) & b₆ = ((b₁ - b₂) - (sqrt ((((b₂ ^2 ) + ((2 * b₁) * b₂)) + (5 * (b₁ ^2 ))) - ((4 * b₁) * b₃)))) / (2 * b₁) & not b₄ = - 1 & not b₄ = (b₅ + (sqrt (delta 1,(- b₅),1))) / 2 & not b₄ = (b₆ + (sqrt (delta 1,(- b₆),1))) / 2 & not b₄ = (b₅ - (sqrt (delta 1,(- b₅),1))) / 2 holds
b₄ = (b₆ - (sqrt (delta 1,(- b₆),1))) / 2

proof end;

theorem Th14: :: POLYEQ_4:14

for b₁, b₂, b₃, b₄ being Real st b₁ + b₂ = b₃ & b₁ * b₂ = b₄ & (b₃ ^2 ) - (4 * b₄) >= 0 & not ( b₁ = (b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2 & b₂ = (b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2 ) holds
( b₁ = (b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2 & b₂ = (b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2 )

proof end;

theorem Th15: :: POLYEQ_4:15

for b₁, b₂, b₃, b₄ being Real
for b₅ being Nat st (b₁ |^ b₅) + (b₂ |^ b₅) = b₃ & (b₁ |^ b₅) * (b₂ |^ b₅) = b₄ & (b₃ ^2 ) - (4 * b₄) >= 0 & ex b₆ being Nat st b₅ = (2 * b₆) + 1 & not ( b₁ = b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) & b₂ = b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) ) holds
( b₁ = b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) & b₂ = b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) )

proof end;

theorem Th16: :: POLYEQ_4:16

for b₁, b₂, b₃, b₄ being Real
for b₅ being Nat st (b₁ |^ b₅) + (b₂ |^ b₅) = b₃ & (b₁ |^ b₅) * (b₂ |^ b₅) = b₄ & (b₃ ^2 ) - (4 * b₄) >= 0 & b₃ > 0 & b₄ > 0 & ex b₆ being Nat st
( b₅ = 2 * b₆ & b₆ >= 1 ) & not ( b₁ = b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) & b₂ = b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) ) & not ( b₁ = - (b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2)) & b₂ = b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) ) & not ( b₁ = b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) & b₂ = - (b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2)) ) & not ( b₁ = - (b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2)) & b₂ = - (b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2)) ) & not ( b₁ = b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) & b₂ = b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) ) & not ( b₁ = - (b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2)) & b₂ = b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) ) & not ( b₁ = b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2) & b₂ = - (b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2)) ) holds
( b₁ = - (b₅ -root ((b₃ - (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2)) & b₂ = - (b₅ -root ((b₃ + (sqrt ((b₃ ^2 ) - (4 * b₄)))) / 2)) )

proof end;

theorem Th17: :: POLYEQ_4:17

canceled;

theorem Th18: :: POLYEQ_4:18

for b₁, b₂, b₃, b₄ being Real
for b₅ being Nat st (b₁ |^ b₅) + (b₂ |^ b₅) = b₃ & (b₁ |^ b₅) - (b₂ |^ b₅) = b₄ & ex b₆ being Nat st
( b₅ = 2 * b₆ & b₆ >= 1 ) & b₃ > 0 & b₃ + b₄ > 0 & b₃ - b₄ > 0 & not ( b₁ = b₅ -root ((b₃ + b₄) / 2) & b₂ = b₅ -root ((b₃ - b₄) / 2) ) & not ( b₁ = b₅ -root ((b₃ + b₄) / 2) & b₂ = - (b₅ -root ((b₃ - b₄) / 2)) ) & not ( b₁ = - (b₅ -root ((b₃ + b₄) / 2)) & b₂ = b₅ -root ((b₃ - b₄) / 2) ) holds
( b₁ = - (b₅ -root ((b₃ + b₄) / 2)) & b₂ = - (b₅ -root ((b₃ - b₄) / 2)) )

proof end;

theorem Th19: :: POLYEQ_4:19

for b₁, b₂, b₃, b₄, b₅ being Real
for b₆ being Nat st (b₁ * (b₂ |^ b₆)) + (b₃ * (b₄ |^ b₆)) = b₅ & b₂ * b₄ = 0 & ex b₇ being Nat st b₆ = (2 * b₇) + 1 & b₁ * b₃ <> 0 & not ( b₂ = 0 & b₄ = b₆ -root (b₅ / b₃) ) holds
( b₂ = b₆ -root (b₅ / b₁) & b₄ = 0 )

proof end;

theorem Th20: :: POLYEQ_4:20

for b₁, b₂, b₃, b₄, b₅ being Real
for b₆ being Nat st (b₁ * (b₂ |^ b₆)) + (b₃ * (b₄ |^ b₆)) = b₅ & b₂ * b₄ = 0 & ex b₇ being Nat st
( b₆ = 2 * b₇ & b₇ >= 1 ) & b₅ / b₃ > 0 & b₅ / b₁ > 0 & b₁ * b₃ <> 0 & not ( b₂ = 0 & b₄ = b₆ -root (b₅ / b₃) ) & not ( b₂ = 0 & b₄ = - (b₆ -root (b₅ / b₃)) ) & not ( b₂ = b₆ -root (b₅ / b₁) & b₄ = 0 ) holds
( b₂ = - (b₆ -root (b₅ / b₁)) & b₄ = 0 )

proof end;

theorem Th21: :: POLYEQ_4:21

for b₁, b₂, b₃, b₄, b₅ being Real
for b₆ being Nat st b₁ * (b₂ |^ b₆) = b₃ & b₂ * b₄ = b₅ & ex b₇ being Nat st b₆ = (2 * b₇) + 1 & b₃ * b₁ <> 0 holds
( b₂ = b₆ -root (b₃ / b₁) & b₄ = b₅ * (b₆ -root (b₁ / b₃)) )

proof end;

theorem Th22: :: POLYEQ_4:22

for b₁, b₂, b₃, b₄, b₅ being Real
for b₆ being Nat st b₁ * (b₂ |^ b₆) = b₃ & b₂ * b₄ = b₅ & ex b₇ being Nat st
( b₆ = 2 * b₇ & b₇ >= 1 ) & b₃ / b₁ > 0 & b₁ <> 0 & not ( b₂ = b₆ -root (b₃ / b₁) & b₄ = b₅ * (b₆ -root (b₁ / b₃)) ) holds
( b₂ = - (b₆ -root (b₃ / b₁)) & b₄ = - (b₅ * (b₆ -root (b₁ / b₃))) )

proof end;

theorem Th23: :: POLYEQ_4:23

canceled;

theorem Th24: :: POLYEQ_4:24

for b₁, b₂ being Real st b₁ > 0 & b₁ <> 1 & b₁ to_power b₂ = 1 holds
b₂ = 0

proof end;

theorem Th25: :: POLYEQ_4:25

for b₁, b₂ being Real st b₁ > 0 & b₁ <> 1 & b₁ to_power b₂ = b₁ holds
b₂ = 1

proof end;

theorem Th26: :: POLYEQ_4:26

canceled;

theorem Th27: :: POLYEQ_4:27

for b₁, b₂, b₃ being Real st b₁ > 0 & b₁ <> 1 & b₃ > 0 & log b₁,b₃ = 0 holds
b₃ = 1

proof end;

theorem Th28: :: POLYEQ_4:28

for b₁, b₂, b₃ being Real st b₁ > 0 & b₁ <> 1 & b₃ > 0 & log b₁,b₃ = 1 holds
b₃ = b₁

proof end;