:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller

::

:: Received October 19, 2006

:: Copyright (c) 2006-2019 Association of Mizar Users

Lm1: for L being non empty right_complementable add-associative right_zeroed addLoopStr

for F being FinSequence of L

for G being FinSequence

for k being Nat st G = F | (Seg k) & len F = k + 1 holds

( G is FinSequence of L & dom G c= dom F & len G = k & F = G ^ <*(F /. (k + 1))*> )

proof end;

theorem Th1: :: HURWITZ:1

for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for x being Element of L st x <> 0. L holds

- (x ") = (- x) "

for x being Element of L st x <> 0. L holds

- (x ") = (- x) "

proof end;

theorem Th2: :: HURWITZ:2

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for k being Element of NAT holds (power L) . ((- (1_ L)),k) <> 0. L

for k being Element of NAT holds (power L) . ((- (1_ L)),k) <> 0. L

proof end;

theorem Th3: :: HURWITZ:3

for L being non empty well-unital associative multLoopStr

for x being Element of L

for k1, k2 being Element of NAT holds ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2))

for x being Element of L

for k1, k2 being Element of NAT holds ((power L) . (x,k1)) * ((power L) . (x,k2)) = (power L) . (x,(k1 + k2))

proof end;

Lm2: ( Im (1_ F_Complex) = 0 & Im (- (1_ F_Complex)) = 0 & Im (0. F_Complex) = 0 )

proof end;

theorem Th4: :: HURWITZ:4

for L being non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr

for k being Element of NAT holds

( (power L) . ((- (1_ L)),(2 * k)) = 1_ L & (power L) . ((- (1_ L)),((2 * k) + 1)) = - (1_ L) )

for k being Element of NAT holds

( (power L) . ((- (1_ L)),(2 * k)) = 1_ L & (power L) . ((- (1_ L)),((2 * k) + 1)) = - (1_ L) )

proof end;

theorem Th5: :: HURWITZ:5

for z being Element of F_Complex

for k being Element of NAT holds ((power F_Complex) . (z,k)) *' = (power F_Complex) . ((z *'),k)

for k being Element of NAT holds ((power F_Complex) . (z,k)) *' = (power F_Complex) . ((z *'),k)

proof end;

theorem Th6: :: HURWITZ:6

for F, G being FinSequence of F_Complex st len G = len F & ( for i being Element of NAT st i in dom G holds

G /. i = (F /. i) *' ) holds

Sum G = (Sum F) *'

G /. i = (F /. i) *' ) holds

Sum G = (Sum F) *'

proof end;

theorem Th7: :: HURWITZ:7

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for F1, F2 being FinSequence of L st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds

F1 /. i = - (F2 /. i) ) holds

Sum F1 = - (Sum F2)

for F1, F2 being FinSequence of L st len F1 = len F2 & ( for i being Element of NAT st i in dom F1 holds

F1 /. i = - (F2 /. i) ) holds

Sum F1 = - (Sum F2)

proof end;

theorem Th8: :: HURWITZ:8

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for x being Element of L

for F being FinSequence of L holds x * (Sum F) = Sum (x * F)

for x being Element of L

for F being FinSequence of L holds x * (Sum F) = Sum (x * F)

proof end;

Lm3: for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of L holds - (- p) = p

proof end;

theorem Th9: :: HURWITZ:9

for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0_. L) = 0_. L

proof end;

Lm4: for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for p being Polynomial of L

for f being Element of (Polynom-Ring L) st f = p holds

- f = - p

proof end;

theorem :: HURWITZ:10

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of L holds - (- p) = p by Lm3;

for p being Polynomial of L holds - (- p) = p by Lm3;

theorem Th11: :: HURWITZ:11

for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr

for p1, p2 being Polynomial of L holds - (p1 + p2) = (- p1) + (- p2)

for p1, p2 being Polynomial of L holds - (p1 + p2) = (- p1) + (- p2)

proof end;

theorem Th12: :: HURWITZ:12

for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr

for p1, p2 being Polynomial of L holds

( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) )

for p1, p2 being Polynomial of L holds

( - (p1 *' p2) = (- p1) *' p2 & - (p1 *' p2) = p1 *' (- p2) )

proof end;

definition

let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ;

let F be FinSequence of (Polynom-Ring L);

let i be Element of NAT ;

ex b_{1} being FinSequence of L st

( len b_{1} = len F & ( for j being Element of NAT st j in dom b_{1} holds

ex p being Polynomial of L st

( p = F . j & b_{1} . j = p . i ) ) )

for b_{1}, b_{2} being FinSequence of L st len b_{1} = len F & ( for j being Element of NAT st j in dom b_{1} holds

ex p being Polynomial of L st

( p = F . j & b_{1} . j = p . i ) ) & len b_{2} = len F & ( for j being Element of NAT st j in dom b_{2} holds

ex p being Polynomial of L st

( p = F . j & b_{2} . j = p . i ) ) holds

b_{1} = b_{2}

end;
let F be FinSequence of (Polynom-Ring L);

let i be Element of NAT ;

func Coeff (F,i) -> FinSequence of L means :Def1: :: HURWITZ:def 1

( len it = len F & ( for j being Element of NAT st j in dom it holds

ex p being Polynomial of L st

( p = F . j & it . j = p . i ) ) );

existence ( len it = len F & ( for j being Element of NAT st j in dom it holds

ex p being Polynomial of L st

( p = F . j & it . j = p . i ) ) );

ex b

( len b

ex p being Polynomial of L st

( p = F . j & b

proof end;

uniqueness for b

ex p being Polynomial of L st

( p = F . j & b

ex p being Polynomial of L st

( p = F . j & b

b

proof end;

:: deftheorem Def1 defines Coeff HURWITZ:def 1 :

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for F being FinSequence of (Polynom-Ring L)

for i being Element of NAT

for b_{4} being FinSequence of L holds

( b_{4} = Coeff (F,i) iff ( len b_{4} = len F & ( for j being Element of NAT st j in dom b_{4} holds

ex p being Polynomial of L st

( p = F . j & b_{4} . j = p . i ) ) ) );

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for F being FinSequence of (Polynom-Ring L)

for i being Element of NAT

for b

( b

ex p being Polynomial of L st

( p = F . j & b

theorem Th13: :: HURWITZ:13

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr

for p being Polynomial of L

for F being FinSequence of (Polynom-Ring L) st p = Sum F holds

for i being Element of NAT holds p . i = Sum (Coeff (F,i))

for p being Polynomial of L

for F being FinSequence of (Polynom-Ring L) st p = Sum F holds

for i being Element of NAT holds p . i = Sum (Coeff (F,i))

proof end;

Lm5: for L being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr

for p1, p2 being Polynomial of L

for p29 being Element of (Polynom-Ring L) st p29 = p2 holds

for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds

p2 *' p1 = Sum (p29 * F)

proof end;

theorem Th14: :: HURWITZ:14

for L being non empty associative doubleLoopStr

for p being Polynomial of L

for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p

for p being Polynomial of L

for x1, x2 being Element of L holds x1 * (x2 * p) = (x1 * x2) * p

proof end;

theorem Th15: :: HURWITZ:15

for L being non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr

for p being Polynomial of L

for x being Element of L holds - (x * p) = (- x) * p

for p being Polynomial of L

for x being Element of L holds - (x * p) = (- x) * p

proof end;

theorem Th16: :: HURWITZ:16

for L being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr

for p being Polynomial of L

for x being Element of L holds - (x * p) = x * (- p)

for p being Polynomial of L

for x being Element of L holds - (x * p) = x * (- p)

proof end;

theorem Th17: :: HURWITZ:17

for L being non empty left-distributive doubleLoopStr

for p being Polynomial of L

for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p)

for p being Polynomial of L

for x1, x2 being Element of L holds (x1 + x2) * p = (x1 * p) + (x2 * p)

proof end;

theorem Th18: :: HURWITZ:18

for L being non empty right-distributive doubleLoopStr

for p1, p2 being Polynomial of L

for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2)

for p1, p2 being Polynomial of L

for x being Element of L holds x * (p1 + p2) = (x * p1) + (x * p2)

proof end;

theorem Th19: :: HURWITZ:19

for L being non empty right_complementable distributive add-associative right_zeroed associative commutative doubleLoopStr

for p1, p2 being Polynomial of L

for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)

for p1, p2 being Polynomial of L

for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)

proof end;

definition
end;

:: deftheorem defines degree HURWITZ:def 2 :

for L being non empty ZeroStr

for p being Polynomial of L holds degree p = (len p) - 1;

for L being non empty ZeroStr

for p being Polynomial of L holds degree p = (len p) - 1;

Lm6: for L being non empty ZeroStr

for s being AlgSequence of L st len s > 0 holds

s . ((len s) - 1) <> 0. L

proof end;

Lm7: for L being non empty ZeroStr

for p being Polynomial of L st deg p <> - 1 holds

p . (deg p) <> 0. L

proof end;

Lm8: for L being non empty ZeroStr

for p being Polynomial of L holds

( deg p is Element of NAT iff p <> 0_. L )

proof end;

theorem :: HURWITZ:21

for L being non empty right_complementable add-associative right_zeroed addLoopStr

for p1, p2 being Polynomial of L st deg p1 <> deg p2 holds

deg (p1 + p2) = max ((deg p1),(deg p2))

for p1, p2 being Polynomial of L st deg p1 <> deg p2 holds

deg (p1 + p2) = max ((deg p1),(deg p2))

proof end;

Lm9: for L being non empty ZeroStr

for p being Polynomial of L holds deg p >= - 1

proof end;

theorem Th22: :: HURWITZ:22

for L being non empty right_complementable Abelian add-associative right_zeroed addLoopStr

for p1, p2 being Polynomial of L holds deg (p1 + p2) <= max ((deg p1),(deg p2))

for p1, p2 being Polynomial of L holds deg (p1 + p2) <= max ((deg p1),(deg p2))

proof end;

theorem Th23: :: HURWITZ:23

for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative domRing-like doubleLoopStr

for p1, p2 being Polynomial of L st p1 <> 0_. L & p2 <> 0_. L holds

deg (p1 *' p2) = (deg p1) + (deg p2)

for p1, p2 being Polynomial of L st p1 <> 0_. L & p2 <> 0_. L holds

deg (p1 *' p2) = (deg p1) + (deg p2)

proof end;

theorem Th24: :: HURWITZ:24

for L being non empty right_complementable add-associative right_zeroed unital doubleLoopStr

for p being Polynomial of L st deg p = 0 holds

not p is with_roots

for p being Polynomial of L st deg p = 0 holds

not p is with_roots

proof end;

Lm10: for L being non empty unital doubleLoopStr

for z being Element of L

for k being Element of NAT st k <> 0 holds

( ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . 0 = - ((power L) . (z,k)) & ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . k = 1_ L )

proof end;

Lm11: for L being non empty unital doubleLoopStr

for z being Element of L

for k being Element of NAT

for i being Nat st i <> 0 & i <> k holds

((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . i = 0. L

proof end;

:: the polynomials x^k - z^k

definition

let L be non empty unital doubleLoopStr ;

let z be Element of L;

let k be Element of NAT ;

(0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) is Polynomial of L

end;
let z be Element of L;

let k be Element of NAT ;

func rpoly (k,z) -> Polynomial of L equals :: HURWITZ:def 3

(0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)));

coherence (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)));

(0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) is Polynomial of L

proof end;

:: deftheorem defines rpoly HURWITZ:def 3 :

for L being non empty unital doubleLoopStr

for z being Element of L

for k being Element of NAT holds rpoly (k,z) = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)));

for L being non empty unital doubleLoopStr

for z being Element of L

for k being Element of NAT holds rpoly (k,z) = (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)));

theorem :: HURWITZ:25

theorem :: HURWITZ:26

theorem Th27: :: HURWITZ:27

for L being non empty non degenerated well-unital doubleLoopStr

for z being Element of L

for k being Element of NAT holds deg (rpoly (k,z)) = k

for z being Element of L

for k being Element of NAT holds deg (rpoly (k,z)) = k

proof end;

theorem Th28: :: HURWITZ:28

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for p being Polynomial of L holds

( deg p = 1 iff ex x, z being Element of L st

( x <> 0. L & p = x * (rpoly (1,z)) ) )

for p being Polynomial of L holds

( deg p = 1 iff ex x, z being Element of L st

( x <> 0. L & p = x * (rpoly (1,z)) ) )

proof end;

theorem Th29: :: HURWITZ:29

for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr

for x, z being Element of L holds eval ((rpoly (1,z)),x) = x - z

for x, z being Element of L holds eval ((rpoly (1,z)),x) = x - z

proof end;

theorem Th30: :: HURWITZ:30

for L being non empty non degenerated right_complementable well-unital Abelian add-associative right_zeroed doubleLoopStr

for z being Element of L holds z is_a_root_of rpoly (1,z)

for z being Element of L holds z is_a_root_of rpoly (1,z)

proof end;

:: the polynomials x^(k-1) + x^(k-2)*z + x^(k-3)*z^2 + ... + x*z^(k-2) + z^(k-1)

definition

let L be non empty well-unital doubleLoopStr ;

let z be Element of L;

let k be Nat;

ex b_{1} being Polynomial of L st

( ( for i being Nat st i < k holds

b_{1} . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds

b_{1} . i = 0. L ) )

for b_{1}, b_{2} being Polynomial of L st ( for i being Nat st i < k holds

b_{1} . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds

b_{1} . i = 0. L ) & ( for i being Nat st i < k holds

b_{2} . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds

b_{2} . i = 0. L ) holds

b_{1} = b_{2}

end;
let z be Element of L;

let k be Nat;

func qpoly (k,z) -> Polynomial of L means :Def4: :: HURWITZ:def 4

( ( for i being Nat st i < k holds

it . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds

it . i = 0. L ) );

existence ( ( for i being Nat st i < k holds

it . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds

it . i = 0. L ) );

ex b

( ( for i being Nat st i < k holds

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

:: deftheorem Def4 defines qpoly HURWITZ:def 4 :

for L being non empty well-unital doubleLoopStr

for z being Element of L

for k being Nat

for b_{4} being Polynomial of L holds

( b_{4} = qpoly (k,z) iff ( ( for i being Nat st i < k holds

b_{4} . i = (power L) . (z,((k - i) - 1)) ) & ( for i being Nat st i >= k holds

b_{4} . i = 0. L ) ) );

for L being non empty well-unital doubleLoopStr

for z being Element of L

for k being Nat

for b

( b

b

b

theorem :: HURWITZ:31

for L being non empty non degenerated well-unital doubleLoopStr

for z being Element of L

for k being Element of NAT st k >= 1 holds

deg (qpoly (k,z)) = k - 1

for z being Element of L

for k being Element of NAT st k >= 1 holds

deg (qpoly (k,z)) = k - 1

proof end;

theorem Th32: :: HURWITZ:32

for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed commutative doubleLoopStr

for z being Element of L

for k being Element of NAT st k > 1 holds

(rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z)

for z being Element of L

for k being Element of NAT st k > 1 holds

(rpoly (1,z)) *' (qpoly (k,z)) = rpoly (k,z)

proof end;

theorem Th33: :: HURWITZ:33

for L being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p being Polynomial of L

for z being Element of L st z is_a_root_of p holds

ex s being Polynomial of L st p = (rpoly (1,z)) *' s

for p being Polynomial of L

for z being Element of L st z is_a_root_of p holds

ex s being Polynomial of L st p = (rpoly (1,z)) *' s

proof end;

definition

let L be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ;

let p, s be Polynomial of L;

assume A1: s <> 0_. L ;

ex b_{1}, t being Polynomial of L st

( p = (b_{1} *' s) + t & deg t < deg s )

for b_{1}, b_{2} being Polynomial of L st ex t being Polynomial of L st

( p = (b_{1} *' s) + t & deg t < deg s ) & ex t being Polynomial of L st

( p = (b_{2} *' s) + t & deg t < deg s ) holds

b_{1} = b_{2}

end;
let p, s be Polynomial of L;

assume A1: s <> 0_. L ;

func p div s -> Polynomial of L means :Def5: :: HURWITZ:def 5

ex t being Polynomial of L st

( p = (it *' s) + t & deg t < deg s );

existence ex t being Polynomial of L st

( p = (it *' s) + t & deg t < deg s );

ex b

( p = (b

proof end;

uniqueness for b

( p = (b

( p = (b

b

proof end;

:: deftheorem Def5 defines div HURWITZ:def 5 :

for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p, s being Polynomial of L st s <> 0_. L holds

for b_{4} being Polynomial of L holds

( b_{4} = p div s iff ex t being Polynomial of L st

( p = (b_{4} *' s) + t & deg t < deg s ) );

for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p, s being Polynomial of L st s <> 0_. L holds

for b

( b

( p = (b

definition

let L be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ;

let p, s be Polynomial of L;

coherence

p - ((p div s) *' s) is Polynomial of L ;

end;
let p, s be Polynomial of L;

coherence

p - ((p div s) *' s) is Polynomial of L ;

:: deftheorem defines mod HURWITZ:def 6 :

for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p, s being Polynomial of L holds p mod s = p - ((p div s) *' s);

for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p, s being Polynomial of L holds p mod s = p - ((p div s) *' s);

definition

let L be non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ;

let p, s be Polynomial of L;

end;
let p, s be Polynomial of L;

:: deftheorem defines divides HURWITZ:def 7 :

for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p, s being Polynomial of L holds

( s divides p iff p mod s = 0_. L );

for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p, s being Polynomial of L holds

( s divides p iff p mod s = 0_. L );

theorem Th34: :: HURWITZ:34

for L being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p, s being Polynomial of L st s <> 0_. L holds

( s divides p iff ex t being Polynomial of L st t *' s = p )

for p, s being Polynomial of L st s <> 0_. L holds

( s divides p iff ex t being Polynomial of L st t *' s = p )

proof end;

theorem :: HURWITZ:35

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p being Polynomial of L

for z being Element of L st z is_a_root_of p holds

rpoly (1,z) divides p

for p being Polynomial of L

for z being Element of L st z is_a_root_of p holds

rpoly (1,z) divides p

proof end;

theorem :: HURWITZ:36

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for p being Polynomial of L

for z being Element of L st p <> 0_. L & z is_a_root_of p holds

deg (p div (rpoly (1,z))) = (deg p) - 1

for p being Polynomial of L

for z being Element of L st p <> 0_. L & z is_a_root_of p holds

deg (p div (rpoly (1,z))) = (deg p) - 1

proof end;

definition

let f be Polynomial of F_Complex;

end;
attr f is Hurwitz means :: HURWITZ:def 8

for z being Element of F_Complex st z is_a_root_of f holds

Re z < 0 ;

for z being Element of F_Complex st z is_a_root_of f holds

Re z < 0 ;

:: deftheorem defines Hurwitz HURWITZ:def 8 :

for f being Polynomial of F_Complex holds

( f is Hurwitz iff for z being Element of F_Complex st z is_a_root_of f holds

Re z < 0 );

for f being Polynomial of F_Complex holds

( f is Hurwitz iff for z being Element of F_Complex st z is_a_root_of f holds

Re z < 0 );

theorem Th39: :: HURWITZ:39

for x, z being Element of F_Complex st x <> 0. F_Complex holds

( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 )

( x * (rpoly (1,z)) is Hurwitz iff Re z < 0 )

proof end;

theorem Th40: :: HURWITZ:40

for f being Polynomial of F_Complex

for z being Element of F_Complex st z <> 0. F_Complex holds

( f is Hurwitz iff z * f is Hurwitz )

for z being Element of F_Complex st z <> 0. F_Complex holds

( f is Hurwitz iff z * f is Hurwitz )

proof end;

Lm12: for f, g, h being Polynomial of F_Complex st f = g *' h holds

for x being Element of F_Complex st ( x is_a_root_of g or x is_a_root_of h ) holds

x is_a_root_of f

proof end;

theorem Th41: :: HURWITZ:41

for f, g being Polynomial of F_Complex holds

( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) )

( f *' g is Hurwitz iff ( f is Hurwitz & g is Hurwitz ) )

proof end;

definition

let f be Polynomial of F_Complex;

ex b_{1} being Polynomial of F_Complex st

for i being Element of NAT holds b_{1} . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *')

for b_{1}, b_{2} being Polynomial of F_Complex st ( for i being Element of NAT holds b_{1} . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) & ( for i being Element of NAT holds b_{2} . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being Polynomial of F_Complex st ( for i being Element of NAT holds b_{1} . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((b_{2} . i) *') ) holds

for i being Element of NAT holds b_{2} . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((b_{1} . i) *')

end;
func f *' -> Polynomial of F_Complex means :Def9: :: HURWITZ:def 9

for i being Element of NAT holds it . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *');

existence for i being Element of NAT holds it . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *');

ex b

for i being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

involutiveness for b

for i being Element of NAT holds b

proof end;

:: deftheorem Def9 defines *' HURWITZ:def 9 :

for f, b_{2} being Polynomial of F_Complex holds

( b_{2} = f *' iff for i being Element of NAT holds b_{2} . i = ((power F_Complex) . ((- (1_ F_Complex)),i)) * ((f . i) *') );

for f, b

( b

::$CT

theorem Th43: :: HURWITZ:44

for f being Polynomial of F_Complex

for z being Element of F_Complex holds (z * f) *' = (z *') * (f *')

for z being Element of F_Complex holds (z * f) *' = (z *') * (f *')

proof end;

Lm13: for x, xv being Element of COMPLEX

for u, v, uv, vv being Element of REAL st x = u + (v * <i>) & xv = uv + (vv * <i>) holds

(|.(x + (xv *')).| ^2) - (|.(x - xv).| ^2) = (4 * u) * uv

proof end;

Lm14: for x, xv being Element of COMPLEX

for u, v, uv, vv being Element of REAL st x = u + (v * <i>) & xv = uv + (vv * <i>) & uv < 0 holds

( ( u < 0 implies |.(x - xv).| < |.(x + (xv *')).| ) & ( u > 0 implies |.(x - xv).| > |.(x + (xv *')).| ) & ( u = 0 implies |.(x - xv).| = |.(x + (xv *')).| ) )

proof end;

theorem Th48: :: HURWITZ:49

for f being Polynomial of F_Complex st f is Hurwitz holds

for x being Element of F_Complex st Re x >= 0 holds

0 < |.(eval (f,x)).|

for x being Element of F_Complex st Re x >= 0 holds

0 < |.(eval (f,x)).|

proof end;

theorem Th49: :: HURWITZ:50

for f being Polynomial of F_Complex st deg f >= 1 & f is Hurwitz holds

for x being Element of F_Complex holds

( ( Re x < 0 implies |.(eval (f,x)).| < |.(eval ((f *'),x)).| ) & ( Re x > 0 implies |.(eval (f,x)).| > |.(eval ((f *'),x)).| ) & ( Re x = 0 implies |.(eval (f,x)).| = |.(eval ((f *'),x)).| ) )

for x being Element of F_Complex holds

( ( Re x < 0 implies |.(eval (f,x)).| < |.(eval ((f *'),x)).| ) & ( Re x > 0 implies |.(eval (f,x)).| > |.(eval ((f *'),x)).| ) & ( Re x = 0 implies |.(eval (f,x)).| = |.(eval ((f *'),x)).| ) )

proof end;

definition

let f be Polynomial of F_Complex;

let z be Element of F_Complex;

((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *')) is Polynomial of F_Complex ;

end;
let z be Element of F_Complex;

func F* (f,z) -> Polynomial of F_Complex equals :: HURWITZ:def 10

((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *'));

coherence ((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *'));

((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *')) is Polynomial of F_Complex ;

:: deftheorem defines F* HURWITZ:def 10 :

for f being Polynomial of F_Complex

for z being Element of F_Complex holds F* (f,z) = ((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *'));

for f being Polynomial of F_Complex

for z being Element of F_Complex holds F* (f,z) = ((eval ((f *'),z)) * f) - ((eval (f,z)) * (f *'));

theorem Th50: :: HURWITZ:51

for a, b being Element of F_Complex st |.a.| > |.b.| holds

for f being Polynomial of F_Complex st deg f >= 1 holds

( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz )

for f being Polynomial of F_Complex st deg f >= 1 holds

( f is Hurwitz iff (a * f) - (b * (f *')) is Hurwitz )

proof end;

theorem Th51: :: HURWITZ:52

for f being Polynomial of F_Complex st deg f >= 1 holds

for rho being Element of F_Complex st Re rho < 0 & f is Hurwitz holds

(F* (f,rho)) div (rpoly (1,rho)) is Hurwitz

for rho being Element of F_Complex st Re rho < 0 & f is Hurwitz holds

(F* (f,rho)) div (rpoly (1,rho)) is Hurwitz

proof end;

theorem :: HURWITZ:53

theorem :: HURWITZ:54

for f being Polynomial of F_Complex st deg f >= 1 holds

for rho being Element of F_Complex st Re rho < 0 & |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| holds

( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz )

for rho being Element of F_Complex st Re rho < 0 & |.(eval (f,rho)).| < |.(eval ((f *'),rho)).| holds

( f is Hurwitz iff (F* (f,rho)) div (rpoly (1,rho)) is Hurwitz )

proof end;