:: POLYNOM5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: POLYNOM5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m being Nat st n <> 0 & m <> 0 holds
(((n * m) - n) - m) + 1 >= 0
proof end;

theorem Th2: :: POLYNOM5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number st y > 0 holds
(min x,y) / (max x,y) <= 1
proof end;

theorem Th3: :: POLYNOM5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being real number st ( for c being real number st c > 0 & c < 1 holds
c * x >= y ) holds
y <= 0
proof end;

Lm1: for x, y being Real st ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) holds
y <= 0
proof end;

theorem Th4: :: POLYNOM5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of REAL st ( for n being Nat st n in dom p holds
p . n >= 0 ) holds
for i being Nat st i in dom p holds
Sum p >= p . i
proof end;

theorem Th5: :: POLYNOM5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Real holds - [**x,y**] = [**(- x),(- y)**]
proof end;

theorem Th6: :: POLYNOM5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, y1, x2, y2 being Real holds [**x1,y1**] - [**x2,y2**] = [**(x1 - x2),(y1 - y2)**]
proof end;

theorem :: POLYNOM5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th8: :: POLYNOM5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z being Element of F_Complex st z <> 0. F_Complex holds
for n being Nat holds |.((power F_Complex ) . z,n).| = |.z.| to_power n
proof end;

definition
let p be FinSequence of the carrier of F_Complex ;
func |.p.| -> FinSequence of REAL means :Def1: :: POLYNOM5:def 1
( len it = len p & ( for n being Nat st n in dom p holds
it /. n = |.(p /. n).| ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len p & ( for n being Nat st n in dom p holds
b1 /. n = |.(p /. n).| ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len p & ( for n being Nat st n in dom p holds
b1 /. n = |.(p /. n).| ) & len b2 = len p & ( for n being Nat st n in dom p holds
b2 /. n = |.(p /. n).| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines |. POLYNOM5:def 1 :
for p being FinSequence of the carrier of F_Complex
for b2 being FinSequence of REAL holds
( b2 = |.p.| iff ( len b2 = len p & ( for n being Nat st n in dom p holds
b2 /. n = |.(p /. n).| ) ) );

theorem Th9: :: POLYNOM5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
|.(<*> the carrier of F_Complex ).| = <*> REAL
proof end;

theorem Th10: :: POLYNOM5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of F_Complex holds |.<*x*>.| = <*|.x.|*>
proof end;

theorem :: POLYNOM5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of F_Complex holds |.<*x,y*>.| = <*|.x.|,|.y.|*>
proof end;

theorem :: POLYNOM5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Element of F_Complex holds |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>
proof end;

theorem Th13: :: POLYNOM5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence of the carrier of F_Complex holds |.(p ^ q).| = |.p.| ^ |.q.|
proof end;

theorem :: POLYNOM5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of the carrier of F_Complex
for x being Element of F_Complex holds
( |.(p ^ <*x*>).| = |.p.| ^ <*|.x.|*> & |.(<*x*> ^ p).| = <*|.x.|*> ^ |.p.| )
proof end;

theorem Th15: :: POLYNOM5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of the carrier of F_Complex holds |.(Sum p).| <= Sum |.p.|
proof end;

definition
let L be non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr ;
let p be Polynomial of L;
let n be Nat;
func p `^ n -> sequence of L equals :: POLYNOM5:def 2
(power (Polynom-Ring L)) . p,n;
coherence
(power (Polynom-Ring L)) . p,n is sequence of L
proof end;
end;

:: deftheorem defines `^ POLYNOM5:def 2 :
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p being Polynomial of L
for n being Nat holds p `^ n = (power (Polynom-Ring L)) . p,n;

registration
let L be non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr ;
let p be Polynomial of L;
let n be Nat;
cluster p `^ n -> finite-Support ;
coherence
p `^ n is finite-Support
proof end;
end;

theorem Th16: :: POLYNOM5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 0 = 1_. L
proof end;

theorem :: POLYNOM5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 1 = p
proof end;

theorem :: POLYNOM5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 2 = p *' p
proof end;

theorem :: POLYNOM5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p being Polynomial of L holds p `^ 3 = (p *' p) *' p
proof end;

theorem Th20: :: POLYNOM5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p being Polynomial of L
for n being Nat holds p `^ (n + 1) = (p `^ n) *' p
proof end;

theorem Th21: :: POLYNOM5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for n being Nat holds (0_. L) `^ (n + 1) = 0_. L
proof end;

theorem :: POLYNOM5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for n being Nat holds (1_. L) `^ n = 1_. L
proof end;

theorem Th23: :: POLYNOM5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Field
for p being Polynomial of L
for x being Element of L
for n being Nat holds eval (p `^ n),x = (power L) . (eval p,x),n
proof end;

Lm2: for L being non empty ZeroStr
for p being AlgSequence of L st len p > 0 holds
p . ((len p) -' 1) <> 0. L
proof end;

theorem Th24: :: POLYNOM5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being domRing
for p being Polynomial of L st len p <> 0 holds
for n being Nat holds len (p `^ n) = ((n * (len p)) - n) + 1
proof end;

definition
let L be non empty HGrStr ;
let p be sequence of L;
let v be Element of L;
func v * p -> sequence of L means :Def3: :: POLYNOM5:def 3
for n being Nat holds it . n = v * (p . n);
existence
ex b1 being sequence of L st
for n being Nat holds b1 . n = v * (p . n)
proof end;
uniqueness
for b1, b2 being sequence of L st ( for n being Nat holds b1 . n = v * (p . n) ) & ( for n being Nat holds b2 . n = v * (p . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines * POLYNOM5:def 3 :
for L being non empty HGrStr
for p being sequence of L
for v being Element of L
for b4 being sequence of L holds
( b4 = v * p iff for n being Nat holds b4 . n = v * (p . n) );

registration
let L be non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr ;
let p be Polynomial of L;
let v be Element of L;
cluster v * p -> finite-Support ;
coherence
v * p is finite-Support
proof end;
end;

theorem Th25: :: POLYNOM5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable distributive doubleLoopStr
for p being Polynomial of L holds len ((0. L) * p) = 0
proof end;

theorem Th26: :: POLYNOM5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital Field-like doubleLoopStr
for p being Polynomial of L
for v being Element of L st v <> 0. L holds
len (v * p) = len p
proof end;

theorem Th27: :: POLYNOM5:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for p being sequence of L holds (0. L) * p = 0_. L
proof end;

theorem Th28: :: POLYNOM5:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty left_unital multLoopStr
for p being sequence of L holds (1. L) * p = p
proof end;

theorem Th29: :: POLYNOM5:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for v being Element of L holds v * (0_. L) = 0_. L
proof end;

theorem Th30: :: POLYNOM5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty add-associative right_zeroed right_complementable right-distributive right_unital doubleLoopStr
for v being Element of L holds v * (1_. L) = <%v%>
proof end;

theorem Th31: :: POLYNOM5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital Field-like doubleLoopStr
for p being Polynomial of L
for v, x being Element of L holds eval (v * p),x = v * (eval p,x)
proof end;

theorem Th32: :: POLYNOM5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable right-distributive doubleLoopStr
for p being Polynomial of L holds eval p,(0. L) = p . 0
proof end;

definition
let L be non empty ZeroStr ;
let z0, z1 be Element of L;
func <%z0,z1%> -> sequence of L equals :: POLYNOM5:def 4
((0_. L) +* 0,z0) +* 1,z1;
coherence
((0_. L) +* 0,z0) +* 1,z1 is sequence of L
;
end;

:: deftheorem defines <% POLYNOM5:def 4 :
for L being non empty ZeroStr
for z0, z1 being Element of L holds <%z0,z1%> = ((0_. L) +* 0,z0) +* 1,z1;

theorem Th33: :: POLYNOM5:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for z0 being Element of L holds
( <%z0%> . 0 = z0 & ( for n being Nat st n >= 1 holds
<%z0%> . n = 0. L ) )
proof end;

theorem Th34: :: POLYNOM5:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for z0 being Element of L st z0 <> 0. L holds
len <%z0%> = 1
proof end;

theorem Th35: :: POLYNOM5:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr holds <%(0. L)%> = 0_. L
proof end;

theorem Th36: :: POLYNOM5:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital domRing-like doubleLoopStr
for x, y being Element of L holds <%x%> *' <%y%> = <%(x * y)%>
proof end;

theorem Th37: :: POLYNOM5:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty associative commutative Abelian add-associative right_zeroed right_complementable right_unital distributive Field-like doubleLoopStr
for x being Element of L
for n being Nat holds <%x%> `^ n = <%((power L) . x,n)%>
proof end;

theorem :: POLYNOM5:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable doubleLoopStr
for z0, x being Element of L holds eval <%z0%>,x = z0
proof end;

theorem Th39: :: POLYNOM5:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for z0, z1 being Element of L holds
( <%z0,z1%> . 0 = z0 & <%z0,z1%> . 1 = z1 & ( for n being Nat st n >= 2 holds
<%z0,z1%> . n = 0. L ) )
proof end;

registration
let L be non empty ZeroStr ;
let z0, z1 be Element of L;
cluster <%z0,z1%> -> finite-Support ;
coherence
<%z0,z1%> is finite-Support
proof end;
end;

theorem Th40: :: POLYNOM5:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for z0, z1 being Element of L holds len <%z0,z1%> <= 2
proof end;

theorem Th41: :: POLYNOM5:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for z0, z1 being Element of L st z1 <> 0. L holds
len <%z0,z1%> = 2
proof end;

theorem Th42: :: POLYNOM5:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for z0 being Element of L st z0 <> 0. L holds
len <%z0,(0. L)%> = 1
proof end;

theorem Th43: :: POLYNOM5:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr holds <%(0. L),(0. L)%> = 0_. L
proof end;

theorem :: POLYNOM5:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ZeroStr
for z0 being Element of L holds <%z0,(0. L)%> = <%z0%>
proof end;

theorem Th45: :: POLYNOM5:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval <%z0,z1%>,x = z0 + (z1 * x)
proof end;

theorem :: POLYNOM5:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval <%z0,(0. L)%>,x = z0
proof end;

theorem :: POLYNOM5:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval <%(0. L),z1%>,x = z1 * x
proof end;

theorem Th48: :: POLYNOM5:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval <%z0,(1. L)%>,x = z0 + x
proof end;

theorem :: POLYNOM5:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital add-associative right_zeroed right_complementable left-distributive doubleLoopStr
for z0, z1, x being Element of L holds eval <%(0. L),(1. L)%>,x = x
proof end;

definition
let L be non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr ;
let p, q be Polynomial of L;
func Subst p,q -> Polynomial of L means :Def5: :: POLYNOM5:def 5
ex F being FinSequence of the carrier of (Polynom-Ring L) st
( it = Sum F & len F = len p & ( for n being Nat st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) );
existence
ex b1 being Polynomial of L ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b1 = Sum F & len F = len p & ( for n being Nat st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) )
proof end;
uniqueness
for b1, b2 being Polynomial of L st ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b1 = Sum F & len F = len p & ( for n being Nat st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) & ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b2 = Sum F & len F = len p & ( for n being Nat st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Subst POLYNOM5:def 5 :
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p, q, b4 being Polynomial of L holds
( b4 = Subst p,q iff ex F being FinSequence of the carrier of (Polynom-Ring L) st
( b4 = Sum F & len F = len p & ( for n being Nat st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) ) ) );

theorem Th50: :: POLYNOM5:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p being Polynomial of L holds Subst (0_. L),p = 0_. L
proof end;

theorem :: POLYNOM5:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty commutative Abelian add-associative right_zeroed right_complementable right_unital distributive doubleLoopStr
for p being Polynomial of L holds Subst p,(0_. L) = <%(p . 0)%>
proof end;

theorem :: POLYNOM5:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty associative commutative Abelian add-associative right_zeroed right_complementable right_unital distributive Field-like doubleLoopStr
for p being Polynomial of L
for x being Element of L holds len (Subst p,<%x%>) <= 1
proof end;

theorem Th53: :: POLYNOM5:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Field
for p, q being Polynomial of L st len p <> 0 & len q > 1 holds
len (Subst p,q) = ((((len p) * (len q)) - (len p)) - (len q)) + 2
proof end;

theorem Th54: :: POLYNOM5:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Field
for p, q being Polynomial of L
for x being Element of L holds eval (Subst p,q),x = eval p,(eval q,x)
proof end;

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
let x be Element of L;
pred x is_a_root_of p means :Def6: :: POLYNOM5:def 6
eval p,x = 0. L;
end;

:: deftheorem Def6 defines is_a_root_of POLYNOM5:def 6 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L
for x being Element of L holds
( x is_a_root_of p iff eval p,x = 0. L );

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
attr p is with_roots means :Def7: :: POLYNOM5:def 7
ex x being Element of L st x is_a_root_of p;
end;

:: deftheorem Def7 defines with_roots POLYNOM5:def 7 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L holds
( p is with_roots iff ex x being Element of L st x is_a_root_of p );

theorem Th55: :: POLYNOM5:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital doubleLoopStr holds 0_. L is with_roots
proof end;

registration
let L be non empty unital doubleLoopStr ;
cluster 0_. L -> with_roots ;
coherence
0_. L is with_roots
by Th55;
end;

theorem :: POLYNOM5:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital doubleLoopStr
for x being Element of L holds x is_a_root_of 0_. L
proof end;

registration
let L be non empty unital doubleLoopStr ;
cluster with_roots M5( NAT ,the carrier of L);
existence
ex b1 being Polynomial of L st b1 is with_roots
proof end;
end;

definition
let L be non empty unital doubleLoopStr ;
attr L is algebraic-closed means :Def8: :: POLYNOM5:def 8
for p being Polynomial of L st len p > 1 holds
p is with_roots;
end;

:: deftheorem Def8 defines algebraic-closed POLYNOM5:def 8 :
for L being non empty unital doubleLoopStr holds
( L is algebraic-closed iff for p being Polynomial of L st len p > 1 holds
p is with_roots );

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
func Roots p -> Subset of L means :Def9: :: POLYNOM5:def 9
for x being Element of L holds
( x in it iff x is_a_root_of p );
existence
ex b1 being Subset of L st
for x being Element of L holds
( x in b1 iff x is_a_root_of p )
proof end;
uniqueness
for b1, b2 being Subset of L st ( for x being Element of L holds
( x in b1 iff x is_a_root_of p ) ) & ( for x being Element of L holds
( x in b2 iff x is_a_root_of p ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines Roots POLYNOM5:def 9 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L
for b3 being Subset of L holds
( b3 = Roots p iff for x being Element of L holds
( x in b3 iff x is_a_root_of p ) );

definition
let L be non empty associative commutative distributive left_unital Field-like doubleLoopStr ;
let p be Polynomial of L;
func NormPolynomial p -> sequence of L means :Def10: :: POLYNOM5:def 10
for n being Nat holds it . n = (p . n) / (p . ((len p) -' 1));
existence
ex b1 being sequence of L st
for n being Nat holds b1 . n = (p . n) / (p . ((len p) -' 1))
proof end;
uniqueness
for b1, b2 being sequence of L st ( for n being Nat holds b1 . n = (p . n) / (p . ((len p) -' 1)) ) & ( for n being Nat holds b2 . n = (p . n) / (p . ((len p) -' 1)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines NormPolynomial POLYNOM5:def 10 :
for L being non empty associative commutative distributive left_unital Field-like doubleLoopStr
for p being Polynomial of L
for b3 being sequence of L holds
( b3 = NormPolynomial p iff for n being Nat holds b3 . n = (p . n) / (p . ((len p) -' 1)) );

registration
let L be non empty associative commutative add-associative right_zeroed right_complementable distributive left_unital Field-like doubleLoopStr ;
let p be Polynomial of L;
cluster NormPolynomial p -> finite-Support ;
coherence
NormPolynomial p is finite-Support
proof end;
end;

theorem Th57: :: POLYNOM5:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty associative commutative distributive left_unital Field-like doubleLoopStr
for p being Polynomial of L st len p <> 0 holds
(NormPolynomial p) . ((len p) -' 1) = 1. L
proof end;

theorem Th58: :: POLYNOM5:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Field
for p being Polynomial of L st len p <> 0 holds
len (NormPolynomial p) = len p
proof end;

theorem Th59: :: POLYNOM5:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Field
for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds eval (NormPolynomial p),x = (eval p,x) / (p . ((len p) -' 1))
proof end;

theorem Th60: :: POLYNOM5:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Field
for p being Polynomial of L st len p <> 0 holds
for x being Element of L holds
( x is_a_root_of p iff x is_a_root_of NormPolynomial p )
proof end;

theorem Th61: :: POLYNOM5:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Field
for p being Polynomial of L st len p <> 0 holds
( p is with_roots iff NormPolynomial p is with_roots )
proof end;

theorem :: POLYNOM5:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being Field
for p being Polynomial of L st len p <> 0 holds
Roots p = Roots (NormPolynomial p)
proof end;

theorem Th63: :: POLYNOM5:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
id COMPLEX is_continuous_on COMPLEX
proof end;

theorem Th64: :: POLYNOM5:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of COMPLEX holds COMPLEX --> x is_continuous_on COMPLEX
proof end;

definition
let L be non empty unital HGrStr ;
let x be Element of L;
let n be Nat;
func FPower x,n -> Function of L,L means :Def11: :: POLYNOM5:def 11
for y being Element of L holds it . y = x * ((power L) . y,n);
existence
ex b1 being Function of L,L st
for y being Element of L holds b1 . y = x * ((power L) . y,n)
proof end;
uniqueness
for b1, b2 being Function of L,L st ( for y being Element of L holds b1 . y = x * ((power L) . y,n) ) & ( for y being Element of L holds b2 . y = x * ((power L) . y,n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines FPower POLYNOM5:def 11 :
for L being non empty unital HGrStr
for x being Element of L
for n being Nat
for b4 being Function of L,L holds
( b4 = FPower x,n iff for y being Element of L holds b4 . y = x * ((power L) . y,n) );

theorem :: POLYNOM5:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital HGrStr holds FPower (1. L),1 = id the carrier of L
proof end;

theorem :: POLYNOM5:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
FPower (1. F_Complex ),2 = (id COMPLEX ) (#) (id COMPLEX )
proof end;

theorem Th67: :: POLYNOM5:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty unital HGrStr
for x being Element of L holds FPower x,0 = the carrier of L --> x
proof end;

theorem :: POLYNOM5:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of F_Complex ex x1 being Element of COMPLEX st
( x = x1 & FPower x,1 = x1 (#) (id COMPLEX ) )
proof end;

theorem :: POLYNOM5:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of F_Complex ex x1 being Element of COMPLEX st
( x = x1 & FPower x,2 = x1 (#) ((id COMPLEX ) (#) (id COMPLEX )) )
proof end;

theorem Th70: :: POLYNOM5:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of F_Complex
for n being Nat ex f being Function of COMPLEX , COMPLEX st
( f = FPower x,n & FPower x,(n + 1) = f (#) (id COMPLEX ) )
proof end;

theorem Th71: :: POLYNOM5:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of F_Complex
for n being Nat ex f being Function of COMPLEX , COMPLEX st
( f = FPower x,n & f is_continuous_on COMPLEX )
proof end;

definition
let L be non empty unital doubleLoopStr ;
let p be Polynomial of L;
func Polynomial-Function L,p -> Function of L,L means :Def12: :: POLYNOM5:def 12
for x being Element of L holds it . x = eval p,x;
existence
ex b1 being Function of L,L st
for x being Element of L holds b1 . x = eval p,x
proof end;
uniqueness
for b1, b2 being Function of L,L st ( for x being Element of L holds b1 . x = eval p,x ) & ( for x being Element of L holds b2 . x = eval p,x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines Polynomial-Function POLYNOM5:def 12 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L
for b3 being Function of L,L holds
( b3 = Polynomial-Function L,p iff for x being Element of L holds b3 . x = eval p,x );

theorem Th72: :: POLYNOM5:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Polynomial of F_Complex ex f being Function of COMPLEX , COMPLEX st
( f = Polynomial-Function F_Complex ,p & f is_continuous_on COMPLEX )
proof end;

theorem Th73: :: POLYNOM5:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Polynomial of F_Complex st len p > 2 & |.(p . ((len p) -' 1)).| = 1 holds
for F being FinSequence of REAL st len F = len p & ( for n being Nat st n in dom F holds
F . n = |.(p . (n -' 1)).| ) holds
for z being Element of F_Complex st |.z.| > Sum F holds
|.(eval p,z).| > |.(p . 0).| + 1
proof end;

theorem Th74: :: POLYNOM5:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Polynomial of F_Complex st len p > 2 holds
ex z0 being Element of F_Complex st
for z being Element of F_Complex holds |.(eval p,z).| >= |.(eval p,z0).|
proof end;

theorem Th75: :: POLYNOM5:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Polynomial of F_Complex st len p > 1 holds
p is with_roots
proof end;

registration
cluster F_Complex -> algebraic-closed ;
coherence
F_Complex is algebraic-closed
by Def8, Th75;
end;

registration
cluster non empty associative commutative Abelian add-associative right_zeroed right_complementable right_unital distributive left_unital Field-like non degenerated algebraic-closed doubleLoopStr ;
existence
ex b1 being non empty right_unital left_unital doubleLoopStr st
( b1 is algebraic-closed & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is Abelian & b1 is commutative & b1 is associative & b1 is distributive & b1 is Field-like & not b1 is degenerated )
proof end;
end;