hurwitz2.miz

begin

 theorem :: HURWITZ2:1



 Th1: for x,y be Complex st ( Im x) = 0 & ( Re y) = 0 holds ( Re (x / y)) = 0

 proof

 let x,y be Complex;

 reconsider R2 = (( Re y) ^2 ), I2 = (( Im y) ^2 ) as Real;

 assume

 A1: ( Im x) = 0 & ( Re y) = 0 ;



 then ( Re (x / y)) = (((( Re x) * 0 ) + (( Im x) * ( Im y))) / (R2 + I2)) by COMPLEX1: 24

 .= ( 0 / (R2 + I2)) by A1;

 hence ( Re (x / y)) = 0 ;

 end;

 theorem :: HURWITZ2:2

 for a be Complex holds (a * (a *' )) = ( |.a.| ^2 )

 proof

 let a be Complex;

 set ac = a;

 reconsider b = (a *' ) as Complex;

 reconsider Ra = ( Re ac), Ia = ( Im ac) as Real;

 reconsider Ra2 = (Ra ^2 ), Ia2 = (Ia ^2 ) as Real;



 A1: |.a.| = ( sqrt (Ra2 + Ia2)) by COMPLEX1:def 12;

 reconsider xx = (Ra2 + Ia2) as Real;

 Ra2 >= 0 & 0 <= Ia2 by XREAL_1: 63;



 then ( |.a.| ^2 ) = (((( Re ac) * ( Re ac)) - (( Im ac) * ( - ( Im ac)))) + (((( Re ac) * ( - ( Im ac))) + (( Re ac) * ( Im ac))) * )) by A1, SQUARE_1:def 2

 .= (((( Re ac) * ( Re ac)) - (( Im ac) * ( - ( Im ac)))) + (((( Re ac) * ( Im b)) + (( Re ac) * ( Im ac))) * )) by COMPLEX1: 27

 .= (((( Re ac) * ( Re ac)) - (( Im ac) * ( Im b))) + (((( Re ac) * ( Im b)) + (( Re ac) * ( Im ac))) * )) by COMPLEX1: 27

 .= (((( Re ac) * ( Re ac)) - (( Im ac) * ( Im b))) + (((( Re ac) * ( Im b)) + (( Re b) * ( Im ac))) * )) by COMPLEX1: 27

 .= (((( Re ac) * ( Re b)) - (( Im ac) * ( Im b))) + (((( Re ac) * ( Im b)) + (( Re b) * ( Im ac))) * )) by COMPLEX1: 27

 .= (ac * b) by COMPLEX1: 82;

 hence thesis;

 end;

 registration

 cluster Hurwitz for Polynomial of F_Complex ;

 existence

 proof

 take (( 1. F_Complex ) * ( 1_. F_Complex ));

 thus thesis by HURWITZ: 38;

 end;

 end



 Lm1: ((2 * 0 ) + 1) = 1;

 registration

 cluster 0 -> even;

 coherence ;

 end

 theorem :: HURWITZ2:3



 Th3: for L be add-associative right_zeroed right_complementable associative distributive non empty doubleLoopStr holds for k be even Element of NAT holds for x be Element of L holds (( power L) . (( - x),k)) = (( power L) . (x,k))

 proof

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

 let k be even Element of NAT ;

 let x be Element of L;

 defpred P[ Nat] means $1 is even implies (( power L) . (( - x),$1)) = (( power L) . (x,$1));

 A1:

 now

 let k be Nat;

 assume

 A2: for n be Nat st n < k holds P[n];

 now

 assume

 A3: k is even;

 now

 per cases by NAT_1: 23;

 case

 A4: k = 0 ;



 hence (( power L) . (( - x),k)) = ( 1_ L) by GROUP_1:def 7

 .= (( power L) . (x,k)) by A4, GROUP_1:def 7;

 end;

 case k = 1;

 hence (( power L) . (( - x),k)) = (( power L) . (x,k)) by Lm1, A3;

 end;

 case

 A5: k >= 2;

 then

 reconsider k2 = (k - 2) as Element of NAT by NAT_1: 21;

 (k - 1) >= (2 - 1) by A5, XREAL_1: 9;

 then

 reconsider k1 = (k - 1) as Element of NAT by INT_1: 3;



 A6: (k1 + 1) = k;



 A7: (k - 2) < (k - 0 ) by XREAL_1: 10;

 consider l be Nat such that

 A8: k = (2 * l) by A3, ABIAN:def 2;



 A9: (2 * (l - 1)) = (k - 2) by A8;

 reconsider a = (( power L) . (( - x),k1)) as Element of L;

 reconsider b = (( power L) . (x,k1)) as Element of L;

 reconsider y = (( power L) . (( - x),k2)) as Element of L;

 reconsider z = (( power L) . (x,k2)) as Element of L;



 A10: (( power L) . (( - x),(k2 + 1))) = (y * ( - x)) by GROUP_1:def 7;



 A11: (( power L) . (x,(k2 + 1))) = (z * x) by GROUP_1:def 7;



 thus (( power L) . (( - x),k)) = ((y * ( - x)) * ( - x)) by A10, A6, GROUP_1:def 7

 .= ((z * ( - x)) * ( - x)) by A7, A2, A9

 .= (z * (( - x) * ( - x))) by GROUP_1:def 3

 .= (z * (x * x)) by VECTSP_1: 10

 .= (b * x) by A11, GROUP_1:def 3

 .= (( power L) . (x,k)) by A6, GROUP_1:def 7;

 end;

 end;

 hence (( power L) . (( - x),k)) = (( power L) . (x,k));

 end;

 hence P[k];

 end;

 for k be Nat holds P[k] from NAT_1:sch 4( A1);

 hence thesis;

 end;

 theorem :: HURWITZ2:4



 Th4: for L be add-associative right_zeroed right_complementable associative distributive non empty doubleLoopStr holds for k be odd Element of NAT holds for x be Element of L holds (( power L) . (( - x),k)) = ( - (( power L) . (x,k)))

 proof

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

 let k be odd Element of NAT ;

 let x be Element of L;

 per cases by NAT_1: 14;

 suppose k = 0 ;

 hence (( power L) . (( - x),k)) = ( - (( power L) . (x,k)));

 end;

 suppose k >= 1;

 then

 reconsider k1 = (k - 1) as Element of NAT by INT_1: 5;



 A1: (k1 + 1) = k;

 reconsider a = (( power L) . (( - x),k1)) as Element of L;

 reconsider b = (( power L) . (x,k1)) as Element of L;

 (( power L) . (( - x),k1)) = (( power L) . (x,k1)) by Th3;



 hence (( power L) . (( - x),k)) = (b * ( - x)) by A1, GROUP_1:def 7

 .= ( - (b * x)) by VECTSP_1: 8

 .= ( - (( power L) . (x,k))) by A1, GROUP_1:def 7;

 end;

 end;

 theorem :: HURWITZ2:5



 Th5: for k be even Element of NAT holds for x be Element of F_Complex st ( Re x) = 0 holds ( Im (( power F_Complex ) . (x,k))) = 0

 proof

 let k be even Element of NAT ;

 let x be Element of F_Complex ;

 assume

 A1: ( Re x) = 0 ;

 defpred P[ Nat] means for k1 be Element of NAT st k1 = $1 & k1 is even holds for x be Element of F_Complex st ( Re x) = 0 holds ( Im (( power F_Complex ) . (x,k1))) = 0 ;

 A2:

 now

 let k be Nat;

 assume

 A3: for n be Nat st n < k holds P[n];

 now

 per cases by NAT_1: 23;

 case

 A4: k = 0 ;

 now

 let k1 be Element of NAT ;

 assume

 A5: k1 = k & k1 is even;

 let x be Element of F_Complex ;

 assume ( Re x) = 0 ;

 (( power F_Complex ) . (x, 0 )) = ( 1_ F_Complex ) by GROUP_1:def 7

 .= 1r by COMPLFLD:def 1;

 hence ( Im (( power F_Complex ) . (x,k1))) = 0 by A4, A5, COMPLEX1: 6;

 end;

 hence P[k];

 end;

 case k = 1;

 hence P[k] by Lm1;

 end;

 case k >= 2;

 then

 reconsider n = (k - 2) as Element of NAT by INT_1: 5;

 reconsider n1 = (n + 1) as Element of NAT ;



 A6: (n1 + 1) = k & (n + 1) = n1;

 now

 let k1 be Element of NAT ;

 assume

 A7: k1 = k & k1 is even;

 let x be Element of F_Complex ;

 assume

 A8: ( Re x) = 0 ;



 A9: n is even

 proof

 consider t be Nat such that

 A10: k = (2 * t) by A7, ABIAN:def 2;

 n = (2 * (t - 1)) by A10;

 hence thesis;

 end;

 A11:

 now

 assume n >= k;

 then ((k - 2) - k) >= (k - k) by XREAL_1: 11;

 hence contradiction;

 end;



 A12: (( power F_Complex ) . (x,k1)) = ((( power F_Complex ) . (x,n1)) * x) by A7, A6, GROUP_1:def 7

 .= (((( power F_Complex ) . (x,n)) * x) * x) by GROUP_1:def 7

 .= ((( power F_Complex ) . (x,n)) * (x * x));

 set z1 = (( power F_Complex ) . (x,n)), z2 = (x * x);



 A13: ( Im z2) = ((( Re x) * ( Im x)) + (( Re x) * ( Im x))) by COMPLEX1: 9

 .= 0 by A8;



 A14: ( Im z1) = 0 by A9, A11, A3, A8;



 thus ( Im (( power F_Complex ) . (x,k1))) = ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1))) by A12, COMPLEX1: 9

 .= 0 by A13, A14;

 end;

 hence P[k];

 end;

 end;

 hence P[k];

 end;

 for k be Nat holds P[k] from NAT_1:sch 4( A2);

 hence thesis by A1;

 end;

 theorem :: HURWITZ2:6



 Th6: for k be odd Element of NAT holds for x be Element of F_Complex st ( Re x) = 0 holds ( Re (( power F_Complex ) . (x,k))) = 0

 proof

 let k be odd Element of NAT ;

 let x be Element of F_Complex ;

 assume

 A1: ( Re x) = 0 ;

 defpred P[ Nat] means for k1 be Element of NAT st k1 = $1 & k1 is odd holds for x be Element of F_Complex st ( Re x) = 0 holds ( Re (( power F_Complex ) . (x,k1))) = 0 ;

 A2:

 now

 let k be Nat;

 assume

 A3: for n be Nat st n < k holds P[n];

 now

 per cases by NAT_1: 23;

 case

 A4: k = 1;

 now

 let k1 be Element of NAT ;

 assume

 A5: k1 = k & k1 is odd;

 let x be Element of F_Complex ;

 assume

 A6: ( Re x) = 0 ;

 reconsider z = 0 as Element of NAT by ORDINAL1:def 12;

 1 = ( 0 + 1);



 then (( power F_Complex ) . (x,1)) = ((( power F_Complex ) . (x,z)) * x) by GROUP_1:def 7

 .= (( 1_ F_Complex ) * x) by GROUP_1:def 7

 .= x;

 hence ( Re (( power F_Complex ) . (x,k1))) = 0 by A6, A5, A4;

 end;

 hence P[k];

 end;

 case k = 0 ;

 hence P[k];

 end;

 case k >= 2;

 then

 reconsider n = (k - 2) as Element of NAT by INT_1: 5;

 reconsider n1 = (n + 1) as Element of NAT ;



 A7: (n1 + 1) = k & (n + 1) = n1;

 now

 let k1 be Element of NAT ;

 assume

 A8: k1 = k & k1 is odd;

 let x be Element of F_Complex ;

 assume

 A9: ( Re x) = 0 ;



 A10: n is odd

 proof

 consider t be Integer such that

 A11: k = ((2 * t) + 1) by A8, ABIAN: 1;

 n = ((2 * (t - 1)) + 1) by A11;

 hence thesis;

 end;

 A12:

 now

 assume n >= k;

 then ((k - 2) - k) >= (k - k) by XREAL_1: 11;

 hence contradiction;

 end;



 A13: (( power F_Complex ) . (x,k1)) = ((( power F_Complex ) . (x,n1)) * x) by A8, A7, GROUP_1:def 7

 .= (((( power F_Complex ) . (x,n)) * x) * x) by GROUP_1:def 7

 .= ((( power F_Complex ) . (x,n)) * (x * x));

 set z1 = (( power F_Complex ) . (x,n)), z2 = (x * x);



 A14: ( Im z2) = ((( Re x) * ( Im x)) + (( Re x) * ( Im x))) by COMPLEX1: 9

 .= 0 by A9;



 A15: ( Re z1) = 0 by A10, A12, A3, A9;



 thus ( Re (( power F_Complex ) . (x,k1))) = ((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))) by A13, COMPLEX1: 9

 .= 0 by A14, A15;

 end;

 hence P[k];

 end;

 end;

 hence P[k];

 end;

 for k be Nat holds P[k] from NAT_1:sch 4( A2);

 hence thesis by A1;

 end;

 begin

 definition

 let L be non empty ZeroStr;

 let p be sequence of L;

 :: HURWITZ2:def1

 func even_part p -> sequence of L means

 : Def1: for i be even Nat holds (it . i) = (p . i) & for i be odd Nat holds (it . i) = ( 0. L);

 existence

 proof

 defpred P[ object, object] means for i be Nat st i = $1 holds (i is even implies $2 = (p . $1)) & (i is odd implies $2 = ( 0. L));

 A1:

 now

 let x be object;

 assume

 A2: x in NAT ;

 thus ex y be object st y in the carrier of L & P[x, y]

 proof

 reconsider m = x as Nat by A2;

 per cases ;

 suppose

 A3: m is even;

 take (p . m);

 thus thesis by A3;

 end;

 suppose

 A4: m is odd;

 take ( 0. L);

 thus thesis by A4;

 end;

 end;

 end;

 consider f be Function of NAT , the carrier of L such that

 A5: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

 take f;

 A6:

 now

 let i be even Nat;

 i is Element of NAT by ORDINAL1:def 12;

 hence (f . i) = (p . i) by A5;

 end;

 now

 let i be odd Nat;

 i is Element of NAT by ORDINAL1:def 12;

 hence (f . i) = ( 0. L) by A5;

 end;

 hence thesis by A6;

 end;

 uniqueness

 proof

 let z1,z2 be sequence of L;

 assume

 A7: for i be even Nat holds (z1 . i) = (p . i) & for i be odd Nat holds (z1 . i) = ( 0. L);

 assume

 A8: for i be even Nat holds (z2 . i) = (p . i) & for i be odd Nat holds (z2 . i) = ( 0. L);



 A9: ( dom z1) = NAT by FUNCT_2:def 1

 .= ( dom z2) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom z1);

 then

 reconsider m = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case

 A10: m is even;



 hence (z1 . m) = (p . m) by A7

 .= (z2 . m) by A10, A8;

 end;

 case

 A11: m is odd;



 hence (z1 . m) = ( 0. L) by A7

 .= (z2 . m) by A11, A8;

 end;

 end;

 hence (z1 . x) = (z2 . x);

 end;

 hence z1 = z2 by A9, FUNCT_1: 2;

 end;

 :: HURWITZ2:def2

 func odd_part p -> sequence of L means

 : Def2: for i be even Nat holds (it . i) = ( 0. L) & for i be odd Nat holds (it . i) = (p . i);

 existence

 proof

 defpred P[ object, object] means for i be Nat st i = $1 holds (i is even implies $2 = ( 0. L)) & (i is odd implies $2 = (p . $1));

 A12:

 now

 let x be object;

 assume

 A13: x in NAT ;

 thus ex y be object st y in the carrier of L & P[x, y]

 proof

 reconsider m = x as Nat by A13;

 per cases ;

 suppose

 A14: m is even;

 take ( 0. L);

 thus thesis by A14;

 end;

 suppose

 A15: m is odd;

 take (p . m);

 thus thesis by A15;

 end;

 end;

 end;

 consider f be Function of NAT , the carrier of L such that

 A16: for x be object st x in NAT holds P[x, (f . x)] from FUNCT_2:sch 1( A12);

 take f;

 A17:

 now

 let i be even Nat;

 i is Element of NAT by ORDINAL1:def 12;

 hence (f . i) = ( 0. L) by A16;

 end;

 now

 let i be odd Nat;

 i is Element of NAT by ORDINAL1:def 12;

 hence (f . i) = (p . i) by A16;

 end;

 hence thesis by A17;

 end;

 uniqueness

 proof

 let z1,z2 be sequence of L;

 assume

 A18: for i be even Nat holds (z1 . i) = ( 0. L) & for i be odd Nat holds (z1 . i) = (p . i);

 assume

 A19: for i be even Nat holds (z2 . i) = ( 0. L) & for i be odd Nat holds (z2 . i) = (p . i);



 A20: ( dom z1) = NAT by FUNCT_2:def 1

 .= ( dom z2) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom z1);

 then

 reconsider m = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case

 A21: m is even;



 hence (z1 . m) = ( 0. L) by A18

 .= (z2 . m) by A21, A19;

 end;

 case

 A22: m is odd;



 hence (z1 . m) = (p . m) by A18

 .= (z2 . m) by A22, A19;

 end;

 end;

 hence (z1 . x) = (z2 . x);

 end;

 hence z1 = z2 by A20, FUNCT_1: 2;

 end;

 end

 registration

 let L be non empty ZeroStr;

 let p be Polynomial of L;

 cluster ( even_part p) -> finite-Support;

 coherence

 proof

 set e = ( even_part p);

 ex n be Nat st for i be Nat st i >= n holds (e . i) = ( 0. L)

 proof

 set l = ( len p);

 take l;

 now

 let x be Nat;

 reconsider i = x as Element of NAT by ORDINAL1:def 12;

 assume

 A1: x >= l;

 now

 per cases ;

 case i is even;



 hence (e . i) = (p . i) by Def1

 .= ( 0. L) by A1, ALGSEQ_1: 8;

 end;

 case i is odd;

 hence (e . i) = ( 0. L) by Def1;

 end;

 end;

 hence (e . x) = ( 0. L);

 end;

 hence thesis;

 end;

 hence thesis;

 end;

 cluster ( odd_part p) -> finite-Support;

 coherence

 proof

 set o = ( odd_part p);

 ex n be Nat st for i be Nat st i >= n holds (o . i) = ( 0. L)

 proof

 set l = ( len p);

 take l;

 now

 let x be Nat;

 reconsider i = x as Element of NAT by ORDINAL1:def 12;

 assume

 A2: x >= l;

 now

 per cases ;

 case i is odd;



 hence (o . i) = (p . i) by Def2

 .= ( 0. L) by A2, ALGSEQ_1: 8;

 end;

 case i is even;

 hence (o . i) = ( 0. L) by Def2;

 end;

 end;

 hence (o . x) = ( 0. L);

 end;

 hence thesis;

 end;

 hence thesis;

 end;

 end

 theorem :: HURWITZ2:7



 Th7: for L be non empty ZeroStr holds ( even_part ( 0_. L)) = ( 0_. L) & ( odd_part ( 0_. L)) = ( 0_. L)

 proof

 let L be non empty ZeroStr;

 set e = ( even_part ( 0_. L)), p = ( 0_. L);



 A1: ( dom p) = NAT by FUNCT_2:def 1

 .= ( dom e) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom p);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case i is even;

 hence (e . i) = (p . i) by Def1;

 end;

 case i is odd;



 hence (e . i) = ( 0. L) by Def1

 .= (p . i) by FUNCOP_1: 7;

 end;

 end;

 hence (p . x) = (e . x);

 end;

 hence ( even_part ( 0_. L)) = ( 0_. L) by A1, FUNCT_1: 2;

 set o = ( odd_part ( 0_. L));



 A2: ( dom p) = NAT by FUNCT_2:def 1

 .= ( dom o) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom p);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case i is odd;

 hence (o . i) = (p . i) by Def2;

 end;

 case i is even;



 hence (o . i) = ( 0. L) by Def2

 .= (p . i) by FUNCOP_1: 7;

 end;

 end;

 hence (p . x) = (o . x);

 end;

 hence ( odd_part ( 0_. L)) = ( 0_. L) by A2, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:8

 for L be non empty multLoopStr_0 holds ( even_part ( 1_. L)) = ( 1_. L) & ( odd_part ( 1_. L)) = ( 0_. L)

 proof

 let L be non empty multLoopStr_0;

 set e = ( even_part ( 1_. L)), p = ( 1_. L);



 A1: ( dom p) = NAT by FUNCT_2:def 1

 .= ( dom e) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom p);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case i is even;

 hence (e . i) = (p . i) by Def1;

 end;

 case

 A2: i is odd;



 hence (e . i) = ( 0. L) by Def1

 .= (p . i) by A2, POLYNOM3: 30;

 end;

 end;

 hence (p . x) = (e . x);

 end;

 hence ( even_part ( 1_. L)) = ( 1_. L) by A1, FUNCT_1: 2;

 set o = ( odd_part ( 1_. L)), p = ( 0_. L);



 A3: ( dom p) = NAT by FUNCT_2:def 1

 .= ( dom o) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom p);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case

 A4: i is odd;



 hence (o . i) = (( 1_. L) . i) by Def2

 .= ( 0. L) by A4, POLYNOM3: 30

 .= (p . i) by FUNCOP_1: 7;

 end;

 case i is even;



 hence (o . i) = ( 0. L) by Def2

 .= (p . i) by FUNCOP_1: 7;

 end;

 end;

 hence (p . x) = (o . x);

 end;

 hence ( odd_part ( 1_. L)) = ( 0_. L) by A3, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:9



 Th9: for L be left_zeroed right_zeroed non empty addLoopStr, p be Polynomial of L holds (( even_part p) + ( odd_part p)) = p

 proof

 let L be left_zeroed right_zeroed non empty addLoopStr, p be Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);



 A1: ( dom p) = NAT by FUNCT_2:def 1

 .= ( dom (e + o)) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom p);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case

 A2: i is even;



 hence ((e . i) + (o . i)) = ((e . i) + ( 0. L)) by Def2

 .= (e . i) by RLVECT_1:def 4

 .= (p . i) by Def1, A2;

 end;

 case

 A3: i is odd;



 hence ((e . i) + (o . i)) = (( 0. L) + (o . i)) by Def1

 .= (o . i) by ALGSTR_1:def 2

 .= (p . i) by Def2, A3;

 end;

 end;

 hence (p . x) = ((e + o) . x) by NORMSP_1:def 2;

 end;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:10



 Th10: for L be left_zeroed right_zeroed non empty addLoopStr, p be Polynomial of L holds (( odd_part p) + ( even_part p)) = p

 proof

 let L be left_zeroed right_zeroed non empty addLoopStr, p be Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);



 A1: ( dom p) = NAT by FUNCT_2:def 1

 .= ( dom (o + e)) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom p);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case

 A2: i is even;



 hence ((o /. i) + (e /. i)) = (( 0. L) + (e . i)) by Def2

 .= (e . i) by ALGSTR_1:def 2

 .= (p /. i) by Def1, A2;

 end;

 case

 A3: i is odd;



 hence ((o /. i) + (e /. i)) = ((o . i) + ( 0. L)) by Def1

 .= (o . i) by RLVECT_1:def 4

 .= (p /. i) by Def2, A3;

 end;

 end;

 hence (p . x) = ((o + e) . x) by NORMSP_1:def 2;

 end;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:11

 for L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of L holds (p - ( odd_part p)) = ( even_part p)

 proof

 let L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);



 A1: ( dom (p - o)) = NAT by FUNCT_2:def 1

 .= ( dom e) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom e);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 p = (e + o) by Th9;

 then (p . i) = ((e . i) + (o . i)) by NORMSP_1:def 2;



 then ((p . i) - (o . i)) = ((e . i) + ((o . i) + ( - (o . i)))) by RLVECT_1:def 3

 .= ((e . i) + ( 0. L)) by RLVECT_1: 5

 .= (e . i) by RLVECT_1:def 4;

 hence ((p - o) . x) = (e . x) by POLYNOM3: 27;

 end;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:12

 for L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of L holds (p - ( even_part p)) = ( odd_part p)

 proof

 let L be add-associative right_zeroed right_complementable non empty addLoopStr, p be Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);



 A1: ( dom (p - e)) = NAT by FUNCT_2:def 1

 .= ( dom o) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom o);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 p = (o + e) by Th10;

 then (p . i) = ((o . i) + (e . i)) by NORMSP_1:def 2;



 then ((p . i) - (e . i)) = ((o . i) + ((e . i) + ( - (e . i)))) by RLVECT_1:def 3

 .= ((o . i) + ( 0. L)) by RLVECT_1: 5

 .= (o . i) by RLVECT_1:def 4;

 hence ((p - e) . x) = (o . x) by POLYNOM3: 27;

 end;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:13

 for L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, p be Polynomial of L holds (( even_part p) - p) = ( - ( odd_part p))

 proof

 let L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, p be Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);



 A1: ( dom (e - p)) = NAT by FUNCT_2:def 1

 .= ( dom ( - o)) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom ( - o));

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 p = (e + o) by Th9;

 then (p . i) = ((e . i) + (o . i)) by NORMSP_1:def 2;



 then ((e . i) - (p . i)) = ((e . i) + (( - (o . i)) + ( - (e . i)))) by RLVECT_1: 31

 .= (((e . i) + ( - (e . i))) + ( - (o . i))) by RLVECT_1:def 3

 .= (( - (o . i)) + ( 0. L)) by RLVECT_1: 5

 .= ( - (o . i)) by RLVECT_1:def 4

 .= (( - o) . i) by BHSP_1: 44;

 hence ((e - p) . x) = (( - o) . x) by POLYNOM3: 27;

 end;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:14

 for L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, p be Polynomial of L holds (( odd_part p) - p) = ( - ( even_part p))

 proof

 let L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, p be Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);



 A1: ( dom (o - p)) = NAT by FUNCT_2:def 1

 .= ( dom ( - e)) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom ( - e));

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 p = (o + e) by Th9;

 then (p . i) = ((o . i) + (e . i)) by NORMSP_1:def 2;



 then ((o . i) - (p . i)) = ((o . i) + (( - (e . i)) + ( - (o . i)))) by RLVECT_1: 31

 .= (((o . i) + ( - (o . i))) + ( - (e . i))) by RLVECT_1:def 3

 .= (( 0. L) + ( - (e . i))) by RLVECT_1: 5

 .= ( - (e . i)) by RLVECT_1:def 4

 .= (( - e) . i) by BHSP_1: 44;

 hence ((o - p) . x) = (( - e) . x) by POLYNOM3: 27;

 end;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:15



 Th15: for L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, p,q be Polynomial of L holds ( even_part (p + q)) = (( even_part p) + ( even_part q))

 proof

 let L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr;

 let p,q be Polynomial of L;

 set epq = ( even_part (p + q)), ep = ( even_part p), eq = ( even_part q);



 A1: ( dom epq) = NAT by FUNCT_2:def 1

 .= ( dom (ep + eq)) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom epq);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case

 A2: i is even;



 thus ((ep + eq) . i) = ((ep . i) + (eq . i)) by NORMSP_1:def 2

 .= ((p . i) + (eq . i)) by A2, Def1

 .= ((p . i) + (q . i)) by A2, Def1

 .= ((p + q) . i) by NORMSP_1:def 2

 .= (epq . i) by A2, Def1;

 end;

 case

 A3: i is odd;



 thus ((ep + eq) . i) = ((ep . i) + (eq . i)) by NORMSP_1:def 2

 .= (( 0. L) + (eq . i)) by A3, Def1

 .= (( 0. L) + ( 0. L)) by A3, Def1

 .= ( 0. L) by RLVECT_1:def 4

 .= (epq . i) by A3, Def1;

 end;

 end;

 hence ((ep + eq) . x) = (epq . x);

 end;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:16



 Th16: for L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr, p,q be Polynomial of L holds ( odd_part (p + q)) = (( odd_part p) + ( odd_part q))

 proof

 let L be add-associative right_zeroed right_complementable Abelian non empty addLoopStr;

 let p,q be Polynomial of L;

 set opq = ( odd_part (p + q)), op = ( odd_part p), oq = ( odd_part q);



 A1: ( dom opq) = NAT by FUNCT_2:def 1

 .= ( dom (op + oq)) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom opq);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case

 A2: i is odd;



 thus ((op + oq) . i) = ((op . i) + (oq . i)) by NORMSP_1:def 2

 .= ((p . i) + (oq . i)) by A2, Def2

 .= ((p . i) + (q . i)) by A2, Def2

 .= ((p + q) . i) by NORMSP_1:def 2

 .= (opq . i) by A2, Def2;

 end;

 case

 A3: i is even;



 thus ((op + oq) . i) = ((op . i) + (oq . i)) by NORMSP_1:def 2

 .= (( 0. L) + (oq . i)) by A3, Def2

 .= (( 0. L) + ( 0. L)) by A3, Def2

 .= ( 0. L) by RLVECT_1:def 4

 .= (opq . i) by A3, Def2;

 end;

 end;

 hence ((op + oq) . x) = (opq . x);

 end;

 hence thesis by A1, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:17



 Th17: for L be well-unital non empty doubleLoopStr holds for p be Polynomial of L st ( deg p) is even holds ( even_part ( Leading-Monomial p)) = ( Leading-Monomial p)

 proof

 let L be well-unital non empty doubleLoopStr;

 let p be Polynomial of L;

 assume

 A1: ( deg p) is even;

 set LMp = ( Leading-Monomial p);

 set e = ( even_part LMp);



 A2: ( dom e) = NAT by FUNCT_2:def 1

 .= ( dom LMp) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom e);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case ( len p) = 0 ;

 then p = ( 0_. L) by POLYNOM4: 5;

 then LMp = ( 0_. L) by POLYNOM4: 13;

 hence (e . x) = (LMp . x) by Th7;

 end;

 case ( len p) <> 0 ;

 then (( len p) + 1) > ( 0 + 1) by XREAL_1: 8;

 then ( len p) >= 1 by NAT_1: 13;

 then

 A3: (( len p) -' 1) = ( deg p) by XREAL_1: 233;

 now

 per cases ;

 case i is even;

 hence (e . i) = (LMp . i) by Def1;

 end;

 case

 A4: i is odd;



 hence (LMp . i) = ( 0. L) by A3, A1, POLYNOM4:def 1

 .= (e . i) by A4, Def1;

 end;

 end;

 hence (e . x) = (LMp . x);

 end;

 end;

 hence (e . x) = (LMp . x);

 end;

 hence thesis by A2, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:18



 Th18: for L be well-unital non empty doubleLoopStr holds for p be Polynomial of L st ( deg p) is odd holds ( even_part ( Leading-Monomial p)) = ( 0_. L)

 proof

 let L be well-unital non empty doubleLoopStr;

 let p be Polynomial of L;

 assume

 A1: ( deg p) is odd;

 set LMp = ( Leading-Monomial p);

 set e = ( even_part LMp);



 A2: ( dom ( 0_. L)) = NAT by FUNCT_2:def 1

 .= ( dom e) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom ( 0_. L));

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case ( len p) = 0 ;

 then p = ( 0_. L) by POLYNOM4: 5;

 then LMp = ( 0_. L) by POLYNOM4: 13;

 hence (e . x) = (( 0_. L) . x) by Th7;

 end;

 case ( len p) <> 0 ;

 then (( len p) + 1) > ( 0 + 1) by XREAL_1: 8;

 then ( len p) >= 1 by NAT_1: 13;

 then

 A3: (( len p) -' 1) = ( deg p) by XREAL_1: 233;

 now

 per cases ;

 case

 A4: i is even;



 hence (e . i) = (LMp . i) by Def1

 .= ( 0. L) by A4, A3, A1, POLYNOM4:def 1

 .= (( 0_. L) . i) by FUNCOP_1: 7;

 end;

 case i is odd;



 hence (e . i) = ( 0. L) by Def1

 .= (( 0_. L) . i) by FUNCOP_1: 7;

 end;

 end;

 hence (e . x) = (( 0_. L) . x);

 end;

 end;

 hence (e . x) = (( 0_. L) . x);

 end;

 hence thesis by A2, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:19



 Th19: for L be well-unital non empty doubleLoopStr holds for p be Polynomial of L st ( deg p) is even holds ( odd_part ( Leading-Monomial p)) = ( 0_. L)

 proof

 let L be well-unital non empty doubleLoopStr;

 let p be Polynomial of L;

 assume

 A1: ( deg p) is even;

 set LMp = ( Leading-Monomial p);

 set o = ( odd_part LMp);



 A2: ( dom ( 0_. L)) = NAT by FUNCT_2:def 1

 .= ( dom o) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom ( 0_. L));

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case ( len p) = 0 ;

 then p = ( 0_. L) by POLYNOM4: 5;

 then LMp = ( 0_. L) by POLYNOM4: 13;

 hence (o . x) = (( 0_. L) . x) by Th7;

 end;

 case ( len p) <> 0 ;

 then (( len p) + 1) > ( 0 + 1) by XREAL_1: 8;

 then ( len p) >= 1 by NAT_1: 13;

 then

 A3: (( len p) -' 1) = ( deg p) by XREAL_1: 233;

 now

 per cases ;

 case

 A4: i is odd;



 hence (o . i) = (LMp . i) by Def2

 .= ( 0. L) by A4, A3, A1, POLYNOM4:def 1

 .= (( 0_. L) . i) by FUNCOP_1: 7;

 end;

 case i is even;



 hence (o . i) = ( 0. L) by Def2

 .= (( 0_. L) . i) by FUNCOP_1: 7;

 end;

 end;

 hence (o . x) = (( 0_. L) . x);

 end;

 end;

 hence (o . x) = (( 0_. L) . x);

 end;

 hence thesis by A2, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:20



 Th20: for L be well-unital non empty doubleLoopStr holds for p be Polynomial of L st ( deg p) is odd holds ( odd_part ( Leading-Monomial p)) = ( Leading-Monomial p)

 proof

 let L be well-unital non empty doubleLoopStr;

 let p be Polynomial of L;

 assume

 A1: ( deg p) is odd;

 set LMp = ( Leading-Monomial p);

 set o = ( odd_part LMp);



 A2: ( dom o) = NAT by FUNCT_2:def 1

 .= ( dom LMp) by FUNCT_2:def 1;

 now

 let x be object;

 assume x in ( dom o);

 then

 reconsider i = x as Element of NAT by FUNCT_2:def 1;

 now

 per cases ;

 case ( len p) = 0 ;

 then p = ( 0_. L) by POLYNOM4: 5;

 then LMp = ( 0_. L) by POLYNOM4: 13;

 hence (o . x) = (LMp . x) by Th7;

 end;

 case ( len p) <> 0 ;

 then (( len p) + 1) > ( 0 + 1) by XREAL_1: 8;

 then ( len p) >= 1 by NAT_1: 13;

 then

 A3: (( len p) -' 1) = ( deg p) by XREAL_1: 233;

 now

 per cases ;

 case i is odd;

 hence (o . i) = (LMp . i) by Def2;

 end;

 case

 A4: i is even;



 hence (LMp . i) = ( 0. L) by A3, A1, POLYNOM4:def 1

 .= (o . i) by A4, Def2;

 end;

 end;

 hence (o . x) = (LMp . x);

 end;

 end;

 hence (o . x) = (LMp . x);

 end;

 hence thesis by A2, FUNCT_1: 2;

 end;

 theorem :: HURWITZ2:21



 Th21: for L be well-unital add-associative right_zeroed right_complementable Abelian associative distributive non degenerated doubleLoopStr holds for p be non zero Polynomial of L holds ( deg ( even_part p)) <> ( deg ( odd_part p))

 proof

 let L be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non degenerated doubleLoopStr;

 let p be non zero Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);

 per cases ;

 suppose

 A1: o = ( 0_. L) or e = ( 0_. L);

 then

 A2: ( deg o) = ( - 1) or ( deg e) = ( - 1) by HURWITZ: 20;



 A3: (( 0_. L) + ( 0_. L)) = ( 0_. L) by POLYNOM3: 28;

 now

 per cases by A1;

 case o = ( 0_. L);

 then e <> ( 0_. L) by A3, Th9;

 hence thesis by A2, HURWITZ: 20;

 end;

 case e = ( 0_. L);

 then o <> ( 0_. L) by A3, Th9;

 hence thesis by A2, HURWITZ: 20;

 end;

 end;

 hence thesis;

 end;

 suppose o <> ( 0_. L) & e <> ( 0_. L);

 then

 reconsider e, o as non zero Polynomial of L by UPROOTS:def 5;

 reconsider de = ( degree e) as Element of NAT by ORDINAL1:def 12;

 reconsider deo = ( degree o) as Element of NAT by ORDINAL1:def 12;

 now

 assume

 A4: ( deg e) = ( deg o);

 (( degree e) + 1) = ( len e);

 then

 A5: (e . de) <> ( 0. L) by ALGSEQ_1: 10;

 (( degree o) + 1) = ( len o);

 then

 A6: (o . deo) <> ( 0. L) by ALGSEQ_1: 10;

 now

 per cases ;

 case ( degree e) is even;

 hence contradiction by A6, A4, Def2;

 end;

 case ( degree e) is odd;

 hence contradiction by A5, Def1;

 end;

 end;

 hence contradiction;

 end;

 hence thesis;

 end;

 end;

 theorem :: HURWITZ2:22

 for L be well-unital add-associative right_zeroed right_complementable associative Abelian distributive non degenerated doubleLoopStr holds for p be Polynomial of L holds ( deg ( even_part p)) <= ( deg p) & ( deg ( odd_part p)) <= ( deg p)

 proof

 let L be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non degenerated doubleLoopStr;

 let p be Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);

 per cases ;

 suppose p = ( 0_. L);

 hence thesis by Th7;

 end;

 suppose p <> ( 0_. L);

 then

 reconsider pp = p as non zero Polynomial of L by UPROOTS:def 5;

 p = (e + o) by Th9;

 then

 A1: ( deg pp) = ( max (( deg e),( deg o))) by Th21, HURWITZ: 21;

 hence ( deg ( even_part p)) <= ( deg p) by XXREAL_0: 25;

 thus ( deg ( odd_part p)) <= ( deg p) by A1, XXREAL_0: 25;

 end;

 end;

 theorem :: HURWITZ2:23



 Th23: for L be well-unital add-associative right_zeroed right_complementable associative Abelian distributive non degenerated doubleLoopStr holds for p be Polynomial of L holds ( deg p) = ( max (( deg ( even_part p)),( deg ( odd_part p))))

 proof

 let L be add-associative right_zeroed right_complementable associative Abelian well-unital distributive non degenerated doubleLoopStr;

 let p be Polynomial of L;

 set e = ( even_part p), o = ( odd_part p);

 per cases ;

 suppose

 A1: p = ( 0_. L);

 then e = ( 0_. L) & o = ( 0_. L) by Th7;

 hence thesis by A1;

 end;

 suppose p <> ( 0_. L);

 then

 reconsider pp = p as non zero Polynomial of L by UPROOTS:def 5;

 p = (e + o) by Th9;

 then ( deg pp) = ( max (( deg e),( deg o))) by Th21, HURWITZ: 21;

 hence thesis;

 end;

 end;

 begin

 definition

 let L be non empty addLoopStr;

 let f be Function of L, L;

 :: HURWITZ2:def3

 attr f is even means

 : Def3: for x be Element of L holds (f . ( - x)) = (f . x);

 :: HURWITZ2:def4

 attr f is odd means

 : Def4: for x be Element of L holds (f . ( - x)) = ( - (f . x));

 end

 definition

 let L be well-unital non empty doubleLoopStr;

 let p be Polynomial of L;

 :: HURWITZ2:def5

 attr p is even means

 : Def5: ( Polynomial-Function (L,p)) is even;

 :: HURWITZ2:def6

 attr p is odd means

 : Def6: ( Polynomial-Function (L,p)) is odd;

 end

 definition

 let L be well-unital non trivial doubleLoopStr;

 let Z be rational_function of L;

 :: HURWITZ2:def7

 attr Z is odd means ((Z `1 ) is even & (Z `2 ) is odd) or ((Z `1 ) is odd & (Z `2 ) is even);

 end

 notation

 let L be well-unital non trivial doubleLoopStr;

 let Z be rational_function of L;

 antonym Z is even for Z is odd;

 end

 registration

 let L be well-unital non empty doubleLoopStr;

 cluster even for Polynomial of L;

 existence

 proof

 set p = ( 0_. L);

 take p;

 set f = ( Polynomial-Function (L,p));

 A1:

 now

 let x be Element of L;



 thus (f . x) = ( eval (p,x)) by POLYNOM5:def 13

 .= ( 0. L) by POLYNOM4: 17;

 end;

 now

 let x be Element of L;



 thus (f . ( - x)) = ( 0. L) by A1

 .= (f . x) by A1;

 end;

 hence thesis by Def3;

 end;

 end

 registration

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

 cluster odd for Polynomial of L;

 existence

 proof

 set p = ( 0_. L);

 take p;

 set f = ( Polynomial-Function (L,p));

 A1:

 now

 let x be Element of L;



 thus (f . x) = ( eval (p,x)) by POLYNOM5:def 13

 .= ( 0. L) by POLYNOM4: 17;

 end;

 now

 let x be Element of L;



 thus (f . ( - x)) = ( 0. L) by A1

 .= ( - ( 0. L)) by RLVECT_1: 12

 .= ( - (f . x)) by A1;

 end;

 hence thesis by Def4;

 end;

 end

 registration

 let L be well-unital add-associative right_zeroed right_complementable associative non degenerated doubleLoopStr;

 cluster non zero even for Polynomial of L;

 existence

 proof

 set p = ( 1_. L);

 take p;

 set f = ( Polynomial-Function (L,p));

 A1:

 now

 let x be Element of L;



 thus (f . x) = ( eval (p,x)) by POLYNOM5:def 13

 .= ( 1. L) by POLYNOM4: 18;

 end;

 now

 let x be Element of L;



 thus (f . ( - x)) = ( 1. L) by A1

 .= (f . x) by A1;

 end;

 hence thesis by Def3;

 end;

 end

 registration

 let L be add-associative right_zeroed right_complementable Abelian well-unital non degenerated doubleLoopStr;

 cluster non zero odd for Polynomial of L;

 existence

 proof

 set p = ( rpoly (1,( 0. L)));

 take p;

 set f = ( Polynomial-Function (L,p));

 now

 let x be Element of L;



 thus (f . ( - x)) = ( eval (p,( - x))) by POLYNOM5:def 13

 .= (( - x) - ( 0. L)) by HURWITZ: 29

 .= ( - x) by RLVECT_1: 13

 .= ( - (x - ( 0. L))) by RLVECT_1: 13

 .= ( - ( eval (p,x))) by HURWITZ: 29

 .= ( - (f . x)) by POLYNOM5:def 13;

 end;

 then f is odd;

 hence thesis;

 end;

 end

 theorem :: HURWITZ2:24



 Th24: for L be well-unital non empty doubleLoopStr holds for p be even Polynomial of L holds for x be Element of L holds ( eval (p,( - x))) = ( eval (p,x))

 proof

 let L be well-unital non empty doubleLoopStr;

 let p be even Polynomial of L;

 let x be Element of L;



 thus ( eval (p,( - x))) = (( Polynomial-Function (L,p)) . ( - x)) by POLYNOM5:def 13

 .= (( Polynomial-Function (L,p)) . x) by Def3, Def5

 .= ( eval (p,x)) by POLYNOM5:def 13;

 end;

 theorem :: HURWITZ2:25



 Th25: for L be add-associative right_zeroed right_complementable Abelian well-unital non degenerated doubleLoopStr holds for p be odd Polynomial of L holds for x be Element of L holds ( eval (p,( - x))) = ( - ( eval (p,x)))

 proof

 let L be add-associative right_zeroed right_complementable Abelian well-unital non degenerated doubleLoopStr;

 let p be odd Polynomial of L;

 let x be Element of L;



 A1: ( Polynomial-Function (L,p)) is odd by Def6;



 thus ( eval (p,( - x))) = (( Polynomial-Function (L,p)) . ( - x)) by POLYNOM5:def 13

 .= ( - (( Polynomial-Function (L,p)) . x)) by A1

 .= ( - ( eval (p,x))) by POLYNOM5:def 13;

 end;

 registration

 let L be well-unital non empty doubleLoopStr;

 cluster ( 0_. L) -> even;

 coherence

 proof

 set f = ( Polynomial-Function (L,( 0_. L)));

 now

 let x be Element of L;



 thus (f . ( - x)) = ( eval (( 0_. L),( - x))) by POLYNOM5:def 13

 .= ( 0. L) by POLYNOM4: 17

 .= ( eval (( 0_. L),x)) by POLYNOM4: 17

 .= (f . x) by POLYNOM5:def 13;

 end;

 then f is even;

 hence thesis;

 end;

 end

 registration

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

 cluster ( 0_. L) -> odd;

 coherence

 proof

 set f = ( Polynomial-Function (L,( 0_. L)));

 now

 let x be Element of L;



 thus (f . ( - x)) = ( eval (( 0_. L),( - x))) by POLYNOM5:def 13

 .= ( 0. L) by POLYNOM4: 17

 .= ( - ( 0. L)) by RLVECT_1: 12

 .= ( - ( eval (( 0_. L),x))) by POLYNOM4: 17

 .= ( - (f . x)) by POLYNOM5:def 13;

 end;

 hence thesis by Def4;

 end;

 end

 registration

 let L be well-unital add-associative right_zeroed right_complementable associative non degenerated doubleLoopStr;

 cluster ( 1_. L) -> even;

 coherence

 proof

 set f = ( Polynomial-Function (L,( 1_. L)));

 now

 let x be Element of L;



 thus (f . ( - x)) = ( eval (( 1_. L),( - x))) by POLYNOM5:def 13

 .= ( 1. L) by POLYNOM4: 18

 .= ( eval (( 1_. L),x)) by POLYNOM4: 18

 .= (f . x) by POLYNOM5:def 13;

 end;

 then f is even;

 hence ( 1_. L) is even;

 end;

 end

 registration

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

 let p,q be even Polynomial of L;

 cluster (p + q) -> even;

 coherence

 proof

 set g = ( Polynomial-Function (L,(p + q)));

 now

 let x be Element of L;



 thus (g . ( - x)) = ( eval ((p + q),( - x))) by POLYNOM5:def 13

 .= (( eval (p,( - x))) + ( eval (q,( - x)))) by POLYNOM4: 19

 .= (( eval (p,x)) + ( eval (q,( - x)))) by Th24

 .= (( eval (p,x)) + ( eval (q,x))) by Th24

 .= ( eval ((p + q),x)) by POLYNOM4: 19

 .= (g . x) by POLYNOM5:def 13;

 end;

 hence thesis by Def3;

 end;

 end

 registration

 let L be Abelian add-associative right_zeroed right_complementable well-unital left-distributive non degenerated doubleLoopStr;

 let p,q be odd Polynomial of L;

 cluster (p + q) -> odd;

 coherence

 proof

 set g = ( Polynomial-Function (L,(p + q)));

 now

 let x be Element of L;



 thus (g . ( - x)) = ( eval ((p + q),( - x))) by POLYNOM5:def 13

 .= (( eval (p,( - x))) + ( eval (q,( - x)))) by POLYNOM4: 19

 .= (( - ( eval (p,x))) + ( eval (q,( - x)))) by Th25

 .= (( - ( eval (p,x))) + ( - ( eval (q,x)))) by Th25

 .= ( - (( eval (p,x)) + ( eval (q,x)))) by RLVECT_1: 31

 .= ( - ( eval ((p + q),x))) by POLYNOM4: 19

 .= ( - (g . x)) by POLYNOM5:def 13;

 end;

 then g is odd;

 hence thesis;

 end;

 end

 registration

 let L be Abelian add-associative right_zeroed right_complementable associative well-unital distributive non degenerated doubleLoopStr;

 let p be Polynomial of L;

 cluster ( even_part p) -> even;

 coherence

 proof

 defpred P[ Nat] means for p be Polynomial of L st ( len p) = $1 holds ( even_part p) is even;

 A1:

 now

 let k be Nat;

 assume

 A2: for n be Nat st n < k holds P[n];

 now

 let p be Polynomial of L;

 assume

 A3: ( len p) = k;

 now

 per cases ;

 case k = 0 ;

 then p = ( 0_. L) by A3, POLYNOM4: 5;

 hence ( even_part p) is even by Th7;

 end;

 case

 A4: k <> 0 ;

 set LMp = ( Leading-Monomial p);

 set g = ( Polynomial-Function (L,LMp));

 (LMp + (p - LMp)) = ((LMp + ( - LMp)) + p) by POLYNOM3: 26

 .= ((LMp - LMp) + p)

 .= (( 0_. L) + p) by POLYNOM3: 29

 .= p by POLYNOM3: 28;

 then

 A5: ( even_part p) = (( even_part LMp) + ( even_part (p - LMp))) by Th15;

 consider t be Polynomial of L such that

 A6: ( len t) < ( len p) & p = (t + ( Leading-Monomial p)) & for n be Element of NAT st n < (( len p) - 1) holds (t . n) = (p . n) by A4, A3, POLYNOM4: 16;

 (p - LMp) = (t + (LMp - LMp)) by A6, POLYNOM3: 26

 .= (t + ( 0_. L)) by POLYNOM3: 29

 .= t by POLYNOM3: 28;

 then

 A7: ( even_part (p - LMp)) is even by A6, A2, A3;

 now

 per cases ;

 case

 A8: ( deg p) is even;

 now

 let x be Element of L;

 (( len p) + 1) > ( 0 + 1) by A3, A4, XREAL_1: 8;

 then ( len p) >= 1 by NAT_1: 13;

 then

 A9: (( len p) -' 1) = ( deg p) by XREAL_1: 233;



 thus (g . x) = ( eval (LMp,x)) by POLYNOM5:def 13

 .= ((p . (( len p) -' 1)) * (( power L) . (x,(( len p) -' 1)))) by POLYNOM4: 22

 .= ((p . (( len p) -' 1)) * (( power L) . (( - x),(( len p) -' 1)))) by A9, A8, Th3

 .= ( eval (LMp,( - x))) by POLYNOM4: 22

 .= (g . ( - x)) by POLYNOM5:def 13;

 end;

 then g is even;

 hence ( even_part LMp) is even by A8, Th17;

 end;

 case ( deg p) is odd;

 then ( even_part LMp) = ( 0_. L) by Th18;

 hence ( even_part LMp) is even;

 end;

 end;

 hence ( even_part p) is even by A7, A5;

 end;

 end;

 hence ( even_part p) is even;

 end;

 hence P[k];

 end;



 A10: for k be Nat holds P[k] from NAT_1:sch 4( A1);

 consider k be Nat such that

 A11: ( len p) = k;

 thus thesis by A11, A10;

 end;

 cluster ( odd_part p) -> odd;

 coherence

 proof

 defpred P[ Nat] means for p be Polynomial of L st ( len p) = $1 holds ( odd_part p) is odd;

 A12:

 now

 let k be Nat;

 assume

 A13: for n be Nat st n < k holds P[n];

 now

 let p be Polynomial of L;

 assume

 A14: ( len p) = k;

 now

 per cases ;

 case k = 0 ;

 then p = ( 0_. L) by A14, POLYNOM4: 5;

 hence ( odd_part p) is odd by Th7;

 end;

 case

 A15: k <> 0 ;

 set LMp = ( Leading-Monomial p);

 set g = ( Polynomial-Function (L,LMp));

 (LMp + (p - LMp)) = ((LMp + ( - LMp)) + p) by POLYNOM3: 26

 .= ((LMp - LMp) + p)

 .= (( 0_. L) + p) by POLYNOM3: 29

 .= p by POLYNOM3: 28;

 then

 A16: ( odd_part p) = (( odd_part LMp) + ( odd_part (p - LMp))) by Th16;

 consider t be Polynomial of L such that

 A17: ( len t) < ( len p) & p = (t + ( Leading-Monomial p)) & for n be Element of NAT st n < (( len p) - 1) holds (t . n) = (p . n) by A15, A14, POLYNOM4: 16;

 (p - LMp) = (t + (LMp - LMp)) by A17, POLYNOM3: 26

 .= (t + ( 0_. L)) by POLYNOM3: 29

 .= t by POLYNOM3: 28;

 then

 A18: ( odd_part (p - LMp)) is odd by A17, A13, A14;

 now

 per cases ;

 case

 A19: ( deg p) is odd;

 then

 A20: ( odd_part LMp) = LMp by Th20;

 now

 let x be Element of L;

 (( len p) + 1) > ( 0 + 1) by A14, A15, XREAL_1: 8;

 then ( len p) >= 1 by NAT_1: 13;

 then

 A21: (( len p) -' 1) = ( deg p) by XREAL_1: 233;



 thus ( - (g . x)) = ( - ( eval (LMp,x))) by POLYNOM5:def 13

 .= ( - ((p . (( len p) -' 1)) * (( power L) . (x,(( len p) -' 1))))) by POLYNOM4: 22

 .= ((p . (( len p) -' 1)) * ( - (( power L) . (x,(( len p) -' 1))))) by VECTSP_1: 8

 .= ((p . (( len p) -' 1)) * (( power L) . (( - x),(( len p) -' 1)))) by A21, A19, Th4

 .= ( eval (LMp,( - x))) by POLYNOM4: 22

 .= (g . ( - x)) by POLYNOM5:def 13;

 end;

 hence ( odd_part LMp) is odd by A20, Def4;

 end;

 case ( deg p) is even;

 then ( odd_part LMp) = ( 0_. L) by Th19;

 hence ( odd_part LMp) is odd;

 end;

 end;

 hence ( odd_part p) is odd by A18, A16;

 end;

 end;

 hence ( odd_part p) is odd;

 end;

 hence P[k];

 end;



 A22: for k be Nat holds P[k] from NAT_1:sch 4( A12);

 consider k be Nat such that

 A23: ( len p) = k;

 thus thesis by A23, A22;

 end;

 end

 theorem :: HURWITZ2:26



 Th26: for L be Abelian add-associative right_zeroed right_complementable well-unital distributive non degenerated doubleLoopStr holds for p be even Polynomial of L holds for q be odd Polynomial of L holds for x be Element of L st x is_a_common_root_of (p,q) holds ( - x) is_a_root_of (p + q)

 proof

 let L be Abelian add-associative right_zeroed right_complementable well-unital distributive non degenerated doubleLoopStr;

 let p be even Polynomial of L;

 let q be odd Polynomial of L;

 let x be Element of L;

 assume

 A1: x is_a_common_root_of (p,q);

 then

 A2: ( eval (p,x)) = ( 0. L) by POLYNOM5:def 7;

 ( eval ((p + q),( - x))) = (( eval (p,( - x))) + ( eval (q,( - x)))) by POLYNOM4: 19

 .= (( eval (p,x)) + ( eval (q,( - x)))) by Th24

 .= (( eval (p,x)) + ( - ( eval (q,x)))) by Th25

 .= (( 0. L) + ( - ( 0. L))) by A2, A1, POLYNOM5:def 7

 .= ( 0. L) by RLVECT_1: 5;

 hence ( - x) is_a_root_of (p + q) by POLYNOM5:def 7;

 end;

 theorem :: HURWITZ2:27

 for p be Hurwitz Polynomial of F_Complex holds (( even_part p),( odd_part p)) have_no_common_roots

 proof

 let p be Hurwitz Polynomial of F_Complex ;

 set e = ( even_part p), o = ( odd_part p);

 let x be Element of F_Complex ;

 assume

 A1: x is_a_common_root_of (e,o);



 A2: x is_a_root_of (e + o) by A1, RATFUNC1: 16;

 (e + o) = p by Th9;

 then

 A3: ( Re x) < 0 & ( Re ( - x)) < 0 by A1, Th26, A2, HURWITZ:def 8;

 reconsider s = x as Complex;

 ( Re ( - s)) = ( - ( Re s)) by COMPLEX1: 17;

 hence contradiction by A3, COMPLFLD: 2;

 end;

 begin

 definition

 let p be Polynomial of F_Complex ;

 :: HURWITZ2:def8

 attr p is real means

 : Def8: for i be Nat holds (p . i) is Real;

 :: HURWITZ2:def9

 attr p is positive means for x be Element of F_Complex holds ( Re x) > 0 implies ( Re ( eval (p,x))) > 0 ;

 end

 registration

 cluster ( 0_. F_Complex ) -> real non positive;

 coherence

 proof

 set p = ( 0_. F_Complex );

 now

 let i be Nat;

 (p . i) = ( 0. F_Complex ) by FUNCOP_1: 7, ORDINAL1:def 12

 .= 0 by COMPLFLD:def 1;

 hence (p . i) is Real;

 end;

 hence p is real;



 A1: ( Re ( 1. F_Complex )) > 0 by COMPLEX1: 6, COMPLFLD:def 1;

 ( eval (p,( 1. F_Complex ))) = ( 0. F_Complex ) by POLYNOM4: 17

 .= 0 by COMPLFLD:def 1;

 hence p is non positive by A1, COMPLEX1: 4;

 end;

 cluster ( 1_. F_Complex ) -> real positive;

 coherence

 proof

 set p = ( 1_. F_Complex );

 now

 let i be Nat;

 now

 per cases ;

 case i = 0 ;



 then (p . i) = ( 1. F_Complex ) by POLYNOM3: 30

 .= 1 by COMPLEX1:def 4, COMPLFLD:def 1;

 hence (p . i) is Real;

 end;

 case i <> 0 ;



 then (p . i) = ( 0. F_Complex ) by POLYNOM3: 30

 .= 0 by COMPLFLD:def 1;

 hence (p . i) is Real;

 end;

 end;

 hence (p . i) is Real;

 end;

 hence p is real;

 thus p is positive by POLYNOM4: 18, COMPLFLD: 8, COMPLEX1: 6;

 end;

 end

 registration

 cluster non zero real positive for Polynomial of F_Complex ;

 existence

 proof

 set p = ( 1_. F_Complex );

 take p;

 thus p is non zero;

 thus p is real;

 thus p is positive;

 end;

 end

 registration

 cluster real -> real-valued for Polynomial of F_Complex ;

 coherence

 proof

 let p be Polynomial of F_Complex ;

 assume

 A1: p is real;

 now

 let y be object;

 assume y in ( rng p);

 then

 consider x be object such that

 A2: x in ( dom p) & (p . x) = y by FUNCT_1:def 3;

 reconsider x as Element of NAT by A2, FUNCT_2:def 1;

 (p . x) is Real by A1;

 hence y in REAL by A2, XREAL_0:def 1;

 end;

 hence thesis by VALUED_0:def 3, TARSKI:def 3;

 end;

 end

 registration

 let p be real Polynomial of F_Complex ;

 cluster ( even_part p) -> real;

 coherence

 proof

 set e = ( even_part p);

 now

 let i be Nat;

 now

 per cases ;

 case i is odd;



 then (e . i) = ( 0. F_Complex ) by Def1

 .= 0 by COMPLFLD:def 1;

 hence (e . i) is Real;

 end;

 case i is even;

 then (e . i) = (p . i) by Def1;

 hence (e . i) is Real;

 end;

 end;

 hence (e . i) is Real;

 end;

 hence thesis;

 end;

 cluster ( odd_part p) -> real;

 coherence

 proof

 set o = ( odd_part p);

 now

 let i be Nat;

 now

 per cases ;

 case i is even;



 then (o . i) = ( 0. F_Complex ) by Def2

 .= 0 by COMPLFLD:def 1;

 hence (o . i) is Real;

 end;

 case i is odd;

 then (o . i) = (p . i) by Def2;

 hence (o . i) is Real;

 end;

 end;

 hence (o . i) is Real;

 end;

 hence thesis;

 end;

 end

 definition

 let L be non empty addLoopStr;

 let p be Polynomial of L;

 :: HURWITZ2:def10

 attr p is with_all_coefficients means

 : Def10: for i be Nat st i <= ( deg p) holds (p . i) <> 0 ;

 end

 definition

 let p be real Polynomial of F_Complex ;

 :: HURWITZ2:def11

 attr p is with_positive_coefficients means for i be Nat st i <= ( deg p) holds (p . i) > 0 ;

 :: HURWITZ2:def12

 attr p is with_negative_coefficients means for i be Nat st i <= ( deg p) holds (p . i) < 0 ;

 end

 registration

 cluster with_positive_coefficients -> with_all_coefficients for real Polynomial of F_Complex ;

 coherence ;

 cluster with_negative_coefficients -> with_all_coefficients for real Polynomial of F_Complex ;

 coherence ;

 end

 registration

 cluster non constant with_positive_coefficients for real Polynomial of F_Complex ;

 existence

 proof

 set L = F_Complex ;

 set x = ( 1. F_Complex );

 set p = ((( 0_. L) +* ( 0 ,x)) +* (1,x));



 A1: ( dom ( 0_. L)) = NAT by FUNCOP_1: 13;

 then

 A2: ( dom (( 0_. L) +* ( 0 ,x))) = NAT by FUNCT_7: 30;

 reconsider z = 0 as Element of NAT by ORDINAL1:def 12;



 A3: (p . 0 ) = ((( 0_. L) +* (z,x)) . z) by FUNCT_7: 32

 .= x by A1, FUNCT_7: 31

 .= 1 by COMPLFLD:def 1, COMPLEX1:def 4;



 A4: (p . 1) = x by A2, FUNCT_7: 31

 .= 1 by COMPLFLD:def 1, COMPLEX1:def 4;

 A5:

 now

 let i be Nat;

 now

 per cases by NAT_1: 23;

 case i = 0 ;

 hence (p . i) is Real by A3;

 end;

 case i = 1;

 hence (p . i) is Real by A4;

 end;

 case

 A6: i >= 2;

 then i <> 1;



 then (p . i) = ((( 0_. L) +* ( 0 ,x)) . i) by FUNCT_7: 32

 .= (( 0_. L) . i) by A6, FUNCT_7: 32

 .= ( 0. L) by FUNCOP_1: 7, ORDINAL1:def 12

 .= 0 by COMPLFLD:def 1;

 hence (p . i) is Real;

 end;

 end;

 hence (p . i) is Real;

 end;

 ex n be Nat st for i be Nat st i >= n holds (p . i) = ( 0. L)

 proof

 take 2;

 now

 let i be Nat;

 assume

 A7: i >= 2;

 then 1 <> i;



 hence (p . i) = ((( 0_. L) +* ( 0 ,x)) . i) by FUNCT_7: 32

 .= (( 0_. L) . i) by A7, FUNCT_7: 32

 .= ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

 end;

 hence thesis;

 end;

 then

 reconsider p as Polynomial of L by ALGSEQ_1:def 1;

 now

 let i be Nat;

 assume

 A8: i >= 2;

 then 1 <> i;



 hence (p . i) = ((( 0_. L) +* ( 0 ,x)) . i) by FUNCT_7: 32

 .= (( 0_. L) . i) by A8, FUNCT_7: 32

 .= ( 0. L) by ORDINAL1:def 12, FUNCOP_1: 7;

 end;

 then

 A9: 2 is_at_least_length_of p;

 now

 let m be Nat;

 assume

 A10: m is_at_least_length_of p;

 now

 assume m < 2;

 then m < (1 + 1);

 then (p . 1) = ( 0. L) by A10, INT_1: 7;

 hence contradiction by A2, FUNCT_7: 31;

 end;

 hence 2 <= m;

 end;

 then

 A11: ( len p) = 2 by A9, ALGSEQ_1:def 3;

 reconsider p as real Polynomial of F_Complex by A5, Def8;

 take p;

 thus p is non constant by A11;

 now

 let i be Nat;

 assume i <= ( deg p);

 then

 A12: i < (1 + 1) by A11, NAT_1: 13;

 now

 per cases by A12, NAT_1: 23;

 case i = 0 ;

 hence (p . i) > 0 by A3;

 end;

 case i = 1;

 hence (p . i) > 0 by A4;

 end;

 end;

 hence (p . i) > 0 ;

 end;

 hence p is with_positive_coefficients;

 end;

 end

 registration

 let p be non zero with_all_coefficients real Polynomial of F_Complex ;

 cluster ( even_part p) -> non zero;

 coherence

 proof

 set e = ( even_part p);

 reconsider z = 0 as Element of NAT by ORDINAL1:def 12;

 0 <= ( degree p);

 then

 A1: (p . z) <> z by Def10;

 (e . z) = (p . z) by Def1;

 then (e . z) <> ( 0. F_Complex ) by A1, COMPLFLD:def 1;

 hence thesis by FUNCOP_1: 7;

 end;

 end

 registration

 let p be non constant with_all_coefficients real Polynomial of F_Complex ;

 cluster ( odd_part p) -> non zero;

 coherence

 proof

 set o = ( odd_part p);

 ( 0 + 1) <= ( degree p) by INT_1: 7, RATFUNC1:def 2;

 then

 A1: (p . 1) <> 0 by Def10;

 (o . 1) = (p . 1) by Def2, Lm1;

 then (o . 1) <> ( 0. F_Complex ) by A1, COMPLFLD:def 1;

 hence thesis by FUNCOP_1: 7;

 end;

 end

 definition

 let Z be rational_function of F_Complex ;

 :: HURWITZ2:def13

 attr Z is real means for i be Nat holds ((Z `1 ) . i) is Real & ((Z `2 ) . i) is Real;

 :: HURWITZ2:def14

 attr Z is positive means for x be Element of F_Complex st ( Re x) > 0 & ( eval ((Z `2 ),x)) <> 0 holds ( Re ( eval (Z,x))) > 0 ;

 end

 registration

 cluster non zero odd real positive for rational_function of F_Complex ;

 existence

 proof

 set f = ( rpoly (1,( 0. F_Complex )));

 set p = [f, ( 1_. F_Complex )];

 A1:

 now

 let x be Element of F_Complex ;



 thus ( eval (f,x)) = (x - ( 0. F_Complex )) by HURWITZ: 29

 .= x by RLVECT_1: 13;

 end;

 take p;

 thus p is non zero;

 set fp = ( Polynomial-Function ( F_Complex ,f));

 now

 let x be Element of F_Complex ;



 thus (fp . ( - x)) = ( eval (f,( - x))) by POLYNOM5:def 13

 .= (( - x) - ( 0. F_Complex )) by HURWITZ: 29

 .= ( - x) by RLVECT_1: 13

 .= ( - (x - ( 0. F_Complex ))) by RLVECT_1: 13

 .= ( - ( eval (f,x))) by HURWITZ: 29

 .= ( - (fp . x)) by POLYNOM5:def 13;

 end;

 then fp is odd;

 then f is odd;

 hence p is odd;

 reconsider z = 0 as Element of NAT by ORDINAL1:def 12;

 now

 let i be Nat;



 A2: i in NAT by ORDINAL1:def 12;

 now

 per cases ;

 case

 A3: i = 0 ;



 A4: ( 0 + 1) = 1;

 (f . i) = ( - (( power F_Complex ) . (( 0. F_Complex ),1))) by A3, HURWITZ: 25

 .= ( - ((( power F_Complex ) . (( 0. F_Complex ),z)) * ( 0. F_Complex ))) by A4, GROUP_1:def 7

 .= ( 0. F_Complex ) by RLVECT_1: 12;

 hence (f . i) is Real by COMPLFLD:def 1;

 end;

 case i = 1;



 then (f . i) = ( 1. F_Complex ) by HURWITZ: 25

 .= 1r by COMPLFLD:def 1;

 hence (f . i) is Real by COMPLEX1:def 4;

 end;

 case i <> 1 & i <> 0 ;



 then (f . i) = ( 0. F_Complex ) by HURWITZ: 26, A2

 .= 0 by COMPLFLD:def 1;

 hence (f . i) is Real;

 end;

 end;

 hence ((p `1 ) . i) is Real;

 thus ((p `2 ) . i) is Real;

 end;

 hence p is real;

 now

 let x be Element of F_Complex ;

 assume

 A5: ( Re x) > 0 & ( eval ((p `2 ),x)) <> 0 ;



 A6: ( eval (( 1_. F_Complex ),x)) = ( 1_ F_Complex ) by POLYNOM4: 18;

 ( 1. F_Complex ) <> ( 0. F_Complex );

 then

 A7: ((( 1. F_Complex ) " ) * ( 1. F_Complex )) = ( 1. F_Complex ) by VECTSP_1:def 10;

 ( eval (p,x)) = (x * (( 1. F_Complex ) " )) by A1, A6

 .= (x * ( 1. F_Complex )) by A7

 .= x;

 hence ( Re ( eval (p,x))) > 0 by A5;

 end;

 hence p is positive;

 end;

 end

 registration

 let p1 be real Polynomial of F_Complex ;

 let p2 be non zero real Polynomial of F_Complex ;

 cluster [p1, p2] -> real;

 coherence ;

 end

 begin

 definition

 mode one_port_function is real positive rational_function of F_Complex ;

 mode reactance_one_port_function is odd real positive rational_function of F_Complex ;

 end

 theorem :: HURWITZ2:28



 Th28: for p be real Polynomial of F_Complex holds for x be Element of F_Complex st ( Re x) = 0 holds ( Im ( eval (( even_part p),x))) = 0

 proof

 let p be real Polynomial of F_Complex ;

 let x be Element of F_Complex ;

 defpred P[ Nat] means for p be Polynomial of F_Complex st p is real & ( len p) = $1 holds (for x be Element of F_Complex st ( Re x) = 0 holds ( Im ( eval (( even_part p),x))) = 0 );

 A1:

 now

 let k be Nat;

 assume

 A2: for n be Nat st n < k holds P[n];

 now

 let p be Polynomial of F_Complex ;

 assume

 A3: p is real & ( len p) = k;

 now

 per cases by NAT_1: 14;

 case k = 0 ;

 then p = ( 0_. F_Complex ) by A3, POLYNOM4: 5;

 then

 A4: ( even_part p) = ( 0_. F_Complex ) by Th7;

 thus for x be Element of F_Complex st ( Re x) = 0 holds ( Im ( eval (( even_part p),x))) = 0

 proof

 let x be Element of F_Complex ;

 assume ( Re x) = 0 ;

 ( eval (( even_part p),x)) = ( 0. F_Complex ) by A4, POLYNOM4: 17

 .= 0 by COMPLFLD:def 1;

 hence thesis by COMPLEX1: 4;

 end;

 end;

 case

 A5: k >= 1;

 set LMp = ( Leading-Monomial p);

 (LMp + (p - LMp)) = ((LMp + ( - LMp)) + p) by POLYNOM3: 26

 .= ((LMp - LMp) + p)

 .= (( 0_. F_Complex ) + p) by POLYNOM3: 29

 .= p by POLYNOM3: 28;

 then

 A6: ( even_part p) = (( even_part LMp) + ( even_part (p - LMp))) by Th15;

 thus for x be Element of F_Complex st ( Re x) = 0 holds ( Im ( eval (( even_part p),x))) = 0

 proof

 let x be Element of F_Complex ;

 assume

 A7: ( Re x) = 0 ;

 consider t be Polynomial of F_Complex such that

 A8: ( len t) < ( len p) & p = (t + ( Leading-Monomial p)) & for n be Element of NAT st n < (( len p) - 1) holds (t . n) = (p . n) by A5, A3, POLYNOM4: 16;



 A9: (p - LMp) = (t + (LMp - LMp)) by A8, POLYNOM3: 26

 .= (t + ( 0_. F_Complex )) by POLYNOM3: 29

 .= t by POLYNOM3: 28;

 now

 let n be Nat;



 A10: n in NAT by ORDINAL1:def 12;

 now

 per cases ;

 case n < (( len p) - 1);

 then (t . n) = (p . n) by A8, A10;

 hence (t . n) is Real by A3;

 end;

 case

 A11: n >= (( len p) - 1);

 reconsider lp = (( len p) - 1) as Element of NAT by A5, A3, INT_1: 5;

 ( len t) < (lp + 1) by A8;

 then lp >= ( len t) by NAT_1: 13;

 then (t . n) = ( 0. F_Complex ) by ALGSEQ_1: 8, A11, XXREAL_0: 2;

 hence (t . n) is Real by COMPLFLD:def 1;

 end;

 end;

 hence (t . n) is Real;

 end;

 then

 A12: t is real;



 A13: ( Im ( eval (( even_part LMp),x))) = 0

 proof

 now

 per cases ;

 case ( deg p) is odd;

 then ( even_part LMp) = ( 0_. F_Complex ) by Th18;



 then ( eval (( even_part LMp),x)) = ( 0. F_Complex ) by POLYNOM4: 17

 .= 0 by COMPLFLD:def 1;

 hence thesis by COMPLEX1: 4;

 end;

 case

 A14: ( deg p) is even;



 then

 A15: ( eval (( even_part LMp),x)) = ( eval (LMp,x)) by Th17

 .= ((p . (( len p) -' 1)) * (( power F_Complex ) . (x,(( len p) -' 1)))) by POLYNOM4: 22;

 set z1 = (p . (( len p) -' 1)), z2 = (( power F_Complex ) . (x,(( len p) -' 1)));

 (( len p) -' 1) = ( deg p) by A3, A5, XREAL_1: 233;

 then

 A16: ( Im z2) = 0 by A7, A14, Th5;

 z1 in REAL by A3, XREAL_0:def 1;

 then

 A17: ( Im z1) = 0 by COMPLEX1:def 2;



 thus ( Im ( eval (( even_part LMp),x))) = ((( Re z1) * ( Im z2)) + (( Re z2) * ( Im z1))) by A15, COMPLEX1: 9

 .= 0 by A16, A17;

 end;

 end;

 hence thesis;

 end;



 thus ( Im ( eval (( even_part p),x))) = ( Im (( eval (( even_part LMp),x)) + ( eval (( even_part (p - LMp)),x)))) by A6, POLYNOM4: 19

 .= ( 0 + ( Im ( eval (( even_part (p - LMp)),x)))) by A13, COMPLEX1: 8

 .= 0 by A12, A8, A9, A7, A3, A2;

 end;

 end;

 end;

 hence for x be Element of F_Complex st ( Re x) = 0 holds ( Im ( eval (( even_part p),x))) = 0 ;

 end;

 hence P[k];

 end;



 A18: for k be Nat holds P[k] from NAT_1:sch 4( A1);

 consider n be Nat such that

 A19: ( len p) = n;

 thus thesis by A18, A19;

 end;

 theorem :: HURWITZ2:29



 Th29: for p be real Polynomial of F_Complex holds for x be Element of F_Complex st ( Re x) = 0 holds ( Re ( eval (( odd_part p),x))) = 0

 proof

 let p be real Polynomial of F_Complex ;

 let x be Element of F_Complex ;

 defpred P[ Nat] means for p be Polynomial of F_Complex st p is real & ( len p) = $1 holds (for x be Element of F_Complex st ( Re x) = 0 holds ( Re ( eval (( odd_part p),x))) = 0 );

 A1:

 now

 let k be Nat;

 assume

 A2: for n be Nat st n < k holds P[n];

 now

 let p be Polynomial of F_Complex ;

 assume

 A3: p is real & ( len p) = k;

 now

 per cases by NAT_1: 14;

 case k = 0 ;

 then p = ( 0_. F_Complex ) by A3, POLYNOM4: 5;

 then

 A4: ( odd_part p) = ( 0_. F_Complex ) by Th7;

 thus for x be Element of F_Complex st ( Re x) = 0 holds ( Re ( eval (( odd_part p),x))) = 0

 proof

 let x be Element of F_Complex ;

 assume ( Re x) = 0 ;

 ( eval (( odd_part p),x)) = ( 0. F_Complex ) by A4, POLYNOM4: 17

 .= 0 by COMPLFLD:def 1;

 hence thesis by COMPLEX1: 4;

 end;

 end;

 case

 A5: k >= 1;

 set LMp = ( Leading-Monomial p);

 (LMp + (p - LMp)) = ((LMp + ( - LMp)) + p) by POLYNOM3: 26

 .= ((LMp - LMp) + p)

 .= (( 0_. F_Complex ) + p) by POLYNOM3: 29

 .= p by POLYNOM3: 28;

 then

 A6: ( odd_part p) = (( odd_part LMp) + ( odd_part (p - LMp))) by Th16;

 thus for x be Element of F_Complex st ( Re x) = 0 holds ( Re ( eval (( odd_part p),x))) = 0

 proof

 let x be Element of F_Complex ;

 assume

 A7: ( Re x) = 0 ;

 consider t be Polynomial of F_Complex such that

 A8: ( len t) < ( len p) & p = (t + ( Leading-Monomial p)) & for n be Element of NAT st n < (( len p) - 1) holds (t . n) = (p . n) by A5, A3, POLYNOM4: 16;



 A9: (p - LMp) = (t + (LMp - LMp)) by A8, POLYNOM3: 26

 .= (t + ( 0_. F_Complex )) by POLYNOM3: 29

 .= t by POLYNOM3: 28;

 now

 let n be Nat;



 A10: n in NAT by ORDINAL1:def 12;

 now

 per cases ;

 case n < (( len p) - 1);

 then (t . n) = (p . n) by A8, A10;

 hence (t . n) is Real by A3;

 end;

 case

 A11: n >= (( len p) - 1);

 reconsider lp = (( len p) - 1) as Element of NAT by A5, A3, INT_1: 5;

 ( len t) < (lp + 1) by A8;

 then lp >= ( len t) by NAT_1: 13;

 then (t . n) = ( 0. F_Complex ) by A11, XXREAL_0: 2, ALGSEQ_1: 8;

 hence (t . n) is Real by COMPLFLD:def 1;

 end;

 end;

 hence (t . n) is Real;

 end;

 then

 A12: t is real;



 A13: ( Re ( eval (( odd_part LMp),x))) = 0

 proof

 now

 per cases ;

 case ( deg p) is even;

 then ( odd_part LMp) = ( 0_. F_Complex ) by Th19;



 then ( eval (( odd_part LMp),x)) = ( 0. F_Complex ) by POLYNOM4: 17

 .= 0 by COMPLFLD:def 1;

 hence thesis by COMPLEX1: 4;

 end;

 case

 A14: ( deg p) is odd;



 then

 A15: ( eval (( odd_part LMp),x)) = ( eval (LMp,x)) by Th20

 .= ((p . (( len p) -' 1)) * (( power F_Complex ) . (x,(( len p) -' 1)))) by POLYNOM4: 22;

 set z1 = (p . (( len p) -' 1)), z2 = (( power F_Complex ) . (x,(( len p) -' 1)));

 (( len p) -' 1) = ( deg p) by A3, A5, XREAL_1: 233;

 then

 A16: ( Re z2) = 0 by A7, A14, Th6;

 z1 in REAL by A3, XREAL_0:def 1;

 then

 A17: ( Im z1) = 0 by COMPLEX1:def 2;



 thus ( Re ( eval (( odd_part LMp),x))) = ((( Re z1) * ( Re z2)) - (( Im z1) * ( Im z2))) by A15, COMPLEX1: 9

 .= 0 by A17, A16;

 end;

 end;

 hence thesis;

 end;



 thus ( Re ( eval (( odd_part p),x))) = ( Re (( eval (( odd_part LMp),x)) + ( eval (( odd_part (p - LMp)),x)))) by A6, POLYNOM4: 19

 .= ( 0 + ( Re ( eval (( odd_part (p - LMp)),x)))) by A13, COMPLEX1: 8

 .= 0 by A12, A8, A9, A7, A3, A2;

 end;

 end;

 end;

 hence for x be Element of F_Complex st ( Re x) = 0 holds ( Re ( eval (( odd_part p),x))) = 0 ;

 end;

 hence P[k];

 end;



 A18: for k be Nat holds P[k] from NAT_1:sch 4( A1);

 consider n be Nat such that

 A19: ( len p) = n;

 thus thesis by A18, A19;

 end;

 theorem :: HURWITZ2:30



 Th30: for p be non constant with_positive_coefficients real Polynomial of F_Complex st [( even_part p), ( odd_part p)] is positive & (( even_part p),( odd_part p)) have_no_common_roots holds (for x be Element of F_Complex st ( Re x) = 0 & ( eval (( odd_part p),x)) <> 0 holds ( Re ( eval ( [( even_part p), ( odd_part p)],x))) >= 0 ) & (( even_part p) + ( odd_part p)) is Hurwitz

 proof

 let p be non constant with_positive_coefficients real Polynomial of F_Complex ;

 assume

 A1: [( even_part p), ( odd_part p)] is positive & (( even_part p),( odd_part p)) have_no_common_roots ;

 set p1 = ( even_part p), p2 = ( odd_part p);

 set z = [p1, p2];

 per cases ;

 suppose (p1 - p2) = ( 0_. F_Complex );

 then (p1 + (p2 + ( - p2))) = (( 0_. F_Complex ) + p2) by POLYNOM3: 26;

 then (p1 + (p2 - p2)) = (( 0_. F_Complex ) + p2);

 then (p1 + ( 0_. F_Complex )) = (( 0_. F_Complex ) + p2) by POLYNOM3: 29;

 then

 A2: p1 = (( 0_. F_Complex ) + p2) by POLYNOM3: 28;



 A3: for x be Element of F_Complex holds ( eval (p2,x)) <> ( 0. F_Complex )

 proof

 let x be Element of F_Complex ;

 assume ( eval (p2,x)) = ( 0. F_Complex );

 then x is_a_root_of p2 by POLYNOM5:def 7;

 then x is_a_common_root_of (p1,p2) by A2, POLYNOM3: 28;

 hence thesis by A1;

 end;



 A4: for x be Element of F_Complex holds ( eval (z,x)) = ( 1. F_Complex )

 proof

 let x be Element of F_Complex ;



 A5: ( eval (p2,x)) <> ( 0. F_Complex ) by A3;



 thus ( eval (z,x)) = (( eval (p2,x)) * (( eval (p2,x)) " )) by A2, POLYNOM3: 28

 .= ( 1. F_Complex ) by A5, VECTSP_1:def 10;

 end;



 A6: ( Re ( 1. F_Complex )) = 1 by COMPLFLD:def 1, COMPLEX1: 6;

 now

 let x be Element of F_Complex ;

 assume x is_a_root_of (p1 + p2);



 then ( 0. F_Complex ) = ( eval ((p1 + p2),x)) by POLYNOM5:def 7

 .= (( eval (p1,x)) + ( eval (p2,x))) by POLYNOM4: 19

 .= (( eval (p2,x)) + ( eval (p2,x))) by A2, POLYNOM3: 28;

 then (2 * ( eval (p2,x))) = 0 by COMPLFLD:def 1;

 then ( 0. F_Complex ) = ( eval (p2,x)) by COMPLFLD:def 1;

 hence ( Re x) < 0 by A3;

 end;

 hence ((for x be Element of F_Complex st ( Re x) = 0 & ( eval (p2,x)) <> 0 holds ( Re ( eval (z,x))) >= 0 ) & (p1 + p2) is Hurwitz) by A4, A6;

 end;

 suppose (p1 - p2) <> ( 0_. F_Complex );

 then

 reconsider pp = (p1 - p2) as non zero Polynomial of F_Complex by UPROOTS:def 5;

 set w = [(p1 + p2), pp];

 A7:

 now

 let x be Element of F_Complex ;

 assume

 A8: ( eval ((z `2 ),x)) = ( 0. F_Complex );



 A9: ( eval (pp,x)) = (( eval (p1,x)) - ( eval (p2,x))) by POLYNOM4: 21

 .= ( eval (p1,x)) by RLVECT_1: 13, A8;



 A10: ( eval ((p1 + p2),x)) = (( eval (p1,x)) + ( eval (p2,x))) by POLYNOM4: 19

 .= ( eval (p1,x)) by RLVECT_1:def 4, A8;

 A11:

 now

 assume ( eval (p1,x)) = ( 0. F_Complex );

 then x is_a_common_root_of (p1,p2) by A8, POLYNOM5:def 7;

 hence contradiction by A1;

 end;



 thus ( eval (w,x)) = ((( eval (p1,x)) " ) * ( eval (p1,x))) by A10, A9

 .= ( 1. F_Complex ) by VECTSP_1:def 10, A11;

 end;

 A12:

 now

 let x be Element of F_Complex ;

 assume

 A13: ( eval (w,x)) = ( 1. F_Complex ) & ( eval (p2,x)) <> ( 0. F_Complex ) & ( eval (p2,x)) <> ( eval (p1,x));

 A14:

 now

 assume ( eval (pp,x)) = ( 0. F_Complex );

 then (( eval (p1,x)) - ( eval (p2,x))) = ( 0. F_Complex ) by POLYNOM4: 21;



 then ( eval (p2,x)) = ((( eval (p1,x)) - ( eval (p2,x))) + ( eval (p2,x))) by RLVECT_1:def 4

 .= (( eval (p1,x)) + (( - ( eval (p2,x))) + ( eval (p2,x))))

 .= (( eval (p1,x)) + ( 0. F_Complex )) by RLVECT_1: 5

 .= ( eval (p1,x)) by RLVECT_1:def 4;

 hence contradiction by A13;

 end;

 reconsider a = ( eval (p2,x)) as Complex;

 (( 1. F_Complex ) * ( eval (pp,x))) = (( eval ((p1 + p2),x)) * ((( eval (pp,x)) " ) * ( eval (pp,x)))) by A13

 .= (( eval ((p1 + p2),x)) * ( 1. F_Complex )) by A14, VECTSP_1:def 10

 .= ( eval ((p1 + p2),x));



 then ( eval ((p1 + p2),x)) = ( eval (pp,x))

 .= (( eval (p1,x)) - ( eval (p2,x))) by POLYNOM4: 21;

 then (( eval (p1,x)) + ( eval (p2,x))) = (( eval (p1,x)) - ( eval (p2,x))) by POLYNOM4: 19;

 then a = ( - a) by COMPLFLD: 2;

 hence ( eval ((z `2 ),x)) = ( 0. F_Complex ) by COMPLFLD:def 1;

 end;

 A15:

 now

 let x be Element of F_Complex ;

 assume

 A16: ( eval (p2,x)) <> ( 0. F_Complex ) & ( eval (p2,x)) <> ( eval (p1,x));

 (( eval (w,x)) - ( 1. F_Complex )) <> (( 1. F_Complex ) - ( 1. F_Complex )) by A16, A12;

 then

 A17: (( eval (w,x)) - ( 1. F_Complex )) <> ( 0. F_Complex ) by RLVECT_1: 15;



 A18: 1 = ( 1. F_Complex ) by COMPLFLD:def 1, COMPLEX1:def 4;

 then

 A19: (( eval (w,x)) - 1) = (( eval (w,x)) - ( 1. F_Complex )) by COMPLFLD: 3;



 A20: ( eval ((p1 - p2),x)) = (( eval (p1,x)) - ( eval (p2,x))) by POLYNOM4: 21;

 A21:

 now

 assume ( eval ((p1 - p2),x)) = ( 0. F_Complex );

 then (( eval (p1,x)) - ( eval (p2,x))) = ( 0. F_Complex ) by POLYNOM4: 21;

 hence contradiction by A16, RLVECT_1: 21;

 end;



 A22: (( eval ((p1 - p2),x)) + ( eval ((p1 + p2),x))) = ((( eval (p1,x)) - ( eval (p2,x))) + (( eval (p1,x)) + ( eval (p2,x)))) by A20, POLYNOM4: 19

 .= ((( eval (p2,x)) - ( eval (p2,x))) + (( eval (p1,x)) + ( eval (p1,x))))

 .= (( 0. F_Complex ) + (( eval (p1,x)) + ( eval (p1,x)))) by RLVECT_1:def 10

 .= (( eval (p1,x)) + ( eval (p1,x))) by RLVECT_1:def 4;



 A23: ((( eval ((p1 + p2),x)) * (( eval ((p1 - p2),x)) " )) - (( eval ((p1 - p2),x)) * (( eval ((p1 - p2),x)) " ))) = ((( eval ((p1 + p2),x)) * (( eval ((p1 - p2),x)) " )) + (( - ( eval ((p1 - p2),x))) * (( eval ((p1 - p2),x)) " ))) by VECTSP_1: 8

 .= ((( eval ((p1 + p2),x)) + ( - ( eval ((p1 - p2),x)))) * (( eval ((p1 - p2),x)) " ))

 .= (((( eval (p1,x)) + ( eval (p2,x))) - ( eval ((p1 - p2),x))) * (( eval ((p1 - p2),x)) " )) by POLYNOM4: 19

 .= (((( eval (p1,x)) + ( eval (p2,x))) - (( eval (p1,x)) - ( eval (p2,x)))) * (( eval ((p1 - p2),x)) " )) by POLYNOM4: 21

 .= (((( eval (p1,x)) + ( eval (p2,x))) + (( eval (p2,x)) + ( - ( eval (p1,x))))) * (( eval ((p1 - p2),x)) " )) by RLVECT_1: 33

 .= ((((( eval (p1,x)) + ( - ( eval (p1,x)))) + ( eval (p2,x))) + ( eval (p2,x))) * (( eval ((p1 - p2),x)) " ))

 .= (((( 0. F_Complex ) + ( eval (p2,x))) + ( eval (p2,x))) * (( eval ((p1 - p2),x)) " )) by RLVECT_1:def 10

 .= ((( eval (p2,x)) + ( eval (p2,x))) * (( eval ((p1 - p2),x)) " )) by ALGSTR_1:def 2

 .= (( eval ((p2 + p2),x)) * (( eval ((p1 - p2),x)) " )) by POLYNOM4: 19;



 A24: (( eval (z,x)) * (( eval (w,x)) - 1)) = ((( eval (p1,x)) * (( eval (p2,x)) " )) * (( eval (w,x)) - ( 1. F_Complex ))) by COMPLEX1:def 4, COMPLFLD: 8, COMPLFLD: 3

 .= ((( eval (p1,x)) * (( eval (p2,x)) " )) * (( eval (w,x)) - (( eval ((p1 - p2),x)) * (( eval ((p1 - p2),x)) " )))) by A21, VECTSP_1:def 10

 .= ((( eval (p1,x)) * (( eval (p2,x)) " )) * ((( eval (p2,x)) + ( eval (p2,x))) * (( eval ((p1 - p2),x)) " ))) by A23, POLYNOM4: 19

 .= (((( eval (p1,x)) * 2) * ((( eval (p2,x)) " ) * ( eval (p2,x)))) * (( eval ((p1 - p2),x)) " ))

 .= (((( eval (p1,x)) * 2) * ( 1. F_Complex )) * (( eval ((p1 - p2),x)) " )) by A16, VECTSP_1:def 10

 .= ((2 * ( eval (p1,x))) * (( eval ((p1 - p2),x)) " )) by A18;

 (1 + ( eval (w,x))) = ((( eval ((p1 - p2),x)) * (( eval ((p1 - p2),x)) " )) + (( eval ((p1 + p2),x)) * (( eval ((p1 - p2),x)) " ))) by A18, A21, VECTSP_1:def 10

 .= ((( eval (p1,x)) + ( eval (p1,x))) * (( eval ((p1 - p2),x)) " )) by A22;



 then ((1 + ( eval (w,x))) * ((( eval (w,x)) - 1) " )) = ((( eval (z,x)) * (( eval (w,x)) - 1)) * ((( eval (w,x)) - 1) " )) by A24

 .= (( eval (z,x)) * ((( eval (w,x)) - 1) * ((( eval (w,x)) - 1) " )))

 .= (( eval (z,x)) * ((( eval (w,x)) - ( 1. F_Complex )) * ((( eval (w,x)) - ( 1. F_Complex )) " ))) by A19, A17, COMPLFLD: 5

 .= (( eval (z,x)) * ( 1. F_Complex )) by A17, VECTSP_1:def 10

 .= ( eval (z,x));

 hence ((1 + ( eval (w,x))) / (( eval (w,x)) - 1)) = ( eval (z,x));

 end;

 A25:

 now

 let x be Real;

 assume 0 <= x & (x * x) = 1;

 then 0 < x & x = (x " ) by XCMPLX_1: 210;

 hence x = 1 by XCMPLX_1: 223;

 end;



 A26: for x be Element of F_Complex , E2,E1 be Real st E2 = ( |.( eval (w,x)).| ^2 ) & E1 = ( |.(( eval (w,x)) - 1).| ^2 ) & ( eval (p2,x)) <> ( 0. F_Complex ) & ( eval (p2,x)) <> ( eval (p1,x)) holds ( Re ( eval (z,x))) = ((E2 - 1) / E1)

 proof

 let x be Element of F_Complex , E2,E1 be Real;

 assume

 A27: E2 = ( |.( eval (w,x)).| ^2 ) & E1 = ( |.(( eval (w,x)) - 1).| ^2 );

 assume

 A28: ( eval (p2,x)) <> ( 0. F_Complex ) & ( eval (p2,x)) <> ( eval (p1,x));

 set z1 = (1 + ( eval (w,x))), z2 = (( eval (w,x)) - 1);



 A29: ( Re z1) = (( Re ( eval (w,x))) + 1) by COMPLEX1: 8, COMPLEX1: 6, COMPLEX1:def 4;



 A30: ( Re z2) = (( Re ( eval (w,x))) - 1) by COMPLEX1:def 4, COMPLEX1: 6, COMPLEX1: 19;



 A31: ( Im z1) = ( 0 + ( Im ( eval (w,x)))) by COMPLEX1: 8, COMPLEX1: 6, COMPLEX1:def 4;



 A32: ( Im z2) = (( Im ( eval (w,x))) - ( Im 1r )) by COMPLEX1: 19, COMPLEX1:def 4

 .= (( Im ( eval (w,x))) + 0 ) by COMPLEX1: 6;

 reconsider R2 = (( Re z2) ^2 ), I2 = (( Im z2) ^2 ) as Real;

 reconsider RR = (( Re ( eval (w,x))) ^2 ), II = (( Im ( eval (w,x))) ^2 ) as Real;

 ( Re ((1 + ( eval (w,x))) / (( eval (w,x)) - 1))) = (((( Re z1) * ( Re z2)) + (( Im z1) * ( Im z2))) / (R2 + I2)) by COMPLEX1: 24

 .= (((RR + II) - 1) / (R2 + I2)) by A29, A30, A31, A32

 .= (( |.(( eval (w,x)) * ( eval (w,x))).| - 1) / (R2 + I2)) by COMPLEX1: 68

 .= ((( |.( eval (w,x)).| * |.( eval (w,x)).|) - 1) / (R2 + I2)) by COMPLEX1: 65

 .= ((E2 - 1) / |.(z2 * z2).|) by COMPLEX1: 68, A27

 .= ((E2 - 1) / E1) by COMPLEX1: 65, A27;

 hence ( Re ( eval (z,x))) = ((E2 - 1) / E1) by A28, A15;

 end;



 A33: for x be Element of F_Complex holds (( eval (p2,x)) <> ( eval (p1,x)) & ( Re ( eval (z,x))) >= 0 ) implies |.( eval (w,x)).| >= 1

 proof

 let x be Element of F_Complex ;

 reconsider E2 = ( |.(( eval (w,x)) - 1).| ^2 ) as Real;

 reconsider E1 = ( |.( eval (w,x)).| ^2 ) as Real;

 assume

 A34: ( eval (p2,x)) <> ( eval (p1,x)) & ( Re ( eval (z,x))) >= 0 ;



 A35: E2 >= 0 by XREAL_1: 63;

 now

 per cases by A34;

 case ( eval (p2,x)) = ( 0. F_Complex );



 then ( eval (w,x)) = ( 1. F_Complex ) by A7

 .= 1 by COMPLFLD:def 1, COMPLEX1:def 4;

 hence |.( eval (w,x)).| >= 1 by COMPLEX1: 48;

 end;

 case ( Re ( eval (z,x))) > 0 & ( eval (p2,x)) <> ( 0. F_Complex );

 then

 A36: ((E1 - 1) / E2) > 0 by A34, A26;

 then (E1 - 1) > 0 by A35;

 then

 A37: ((E1 - 1) + 1) > ( 0 + 1) by XREAL_1: 8;

 now

 per cases ;

 case ( eval (w,x)) = 0 ;

 hence |.( eval (w,x)).| >= 1 by A35, A36, COMPLEX1: 44;

 end;

 case ( eval (w,x)) <> 0 ;

 then

 A38: |.( eval (w,x)).| > 0 by COMPLEX1: 47;

 now

 assume

 A39: |.( eval (w,x)).| < 1;

 then E1 <= |.( eval (w,x)).| by A38, SQUARE_1: 42;

 hence contradiction by A37, A39, XXREAL_0: 2;

 end;

 hence |.( eval (w,x)).| >= 1;

 end;

 end;

 hence |.( eval (w,x)).| >= 1;

 end;

 case ( Re ( eval (z,x))) = 0 & ( eval (p2,x)) <> ( 0. F_Complex );

 then

 A40: ((E1 - 1) / E2) = 0 by A34, A26;

 now

 per cases ;

 case ( |.(( eval (w,x)) - 1).| ^2 ) = 0 ;

 then |.(( eval (w,x)) - 1).| = 0 ;

 then (( eval (w,x)) - 1) = 0 by COMPLEX1: 45;

 hence |.( eval (w,x)).| = 1 by COMPLEX1: 48;

 end;

 case ( |.(( eval (w,x)) - 1).| ^2 ) <> 0 ;

 then (E1 - 1) = 0 by A40;

 hence |.( eval (w,x)).| = 1 by A25, COMPLEX1: 46;

 end;

 end;

 hence |.( eval (w,x)).| >= 1;

 end;

 end;

 hence |.( eval (w,x)).| >= 1;

 end;

 thus for x be Element of F_Complex st ( Re x) = 0 & ( eval (p2,x)) <> 0 holds ( Re ( eval (z,x))) >= 0

 proof

 let x be Element of F_Complex ;

 assume

 A41: ( Re x) = 0 & ( eval (p2,x)) <> 0 ;

 then

 A42: ( Im ( eval (p1,x))) = 0 by Th28;



 A43: ( Re ( eval (p2,x))) = 0 by A41, Th29;



 A44: ( eval (p2,x)) <> ( 0. F_Complex ) by A41, COMPLFLD:def 1;

 reconsider y1 = ( eval (p1,x)) as Complex;

 reconsider y2 = ( eval (p2,x)) as Complex;

 ( Re (( eval (p1,x)) / ( eval (p2,x)))) = ( Re (y1 / y2)) by A44, COMPLFLD: 6

 .= 0 by A42, A43, Th1;

 hence thesis;

 end;

 now

 let x be Element of F_Complex ;

 assume

 A45: ( Re x) >= 0 ;

 reconsider RW = ( |.( eval (w,x)).| ^2 ) as Real;

 now

 per cases ;

 case

 A46: ( eval (p2,x)) = ( eval (p1,x));

 A47:

 now

 assume ( eval (p1,x)) = ( 0. F_Complex );

 then x is_a_common_root_of (p1,p2) by A46, POLYNOM5:def 7;

 hence contradiction by A1;

 end;

 now

 assume ( eval ((p1 + p2),x)) = ( 0. F_Complex );



 then

 A48: (( eval (p1,x)) + ( eval (p1,x))) = ( 0. F_Complex ) by A46, POLYNOM4: 19

 .= 0 by COMPLFLD:def 1;

 reconsider a = ( eval (p1,x)) as Complex;

 thus contradiction by A48, A47, COMPLFLD:def 1;

 end;

 hence not (x is_a_root_of (p1 + p2)) by POLYNOM5:def 7;

 end;

 case

 A49: ( eval (p2,x)) <> ( eval (p1,x));

 now

 per cases by A45;

 case

 A50: ( Re x) = 0 ;

 then

 A51: ( Im ( eval (p1,x))) = 0 by Th28;



 A52: ( Re ( eval (p2,x))) = 0 by A50, Th29;

 now

 per cases ;

 case

 A53: ( eval (p2,x)) = 0 ;

 then

 A54: ( eval (p2,x)) = ( 0. F_Complex ) by COMPLFLD:def 1;



 A55: ( eval (pp,x)) = (( eval (p1,x)) - ( eval (p2,x))) by POLYNOM4: 21

 .= (( eval (p1,x)) - ( 0. F_Complex )) by A53, COMPLFLD:def 1

 .= ( eval (p1,x)) by RLVECT_1: 13;



 A56: ( eval ((p1 + p2),x)) = (( eval (p1,x)) + ( eval (p2,x))) by POLYNOM4: 19

 .= ( eval (p1,x)) by A53;

 A57:

 now

 assume ( eval (p1,x)) = ( 0. F_Complex );

 then x is_a_common_root_of (p1,p2) by A54, POLYNOM5:def 7;

 hence contradiction by A1;

 end;

 ( eval (w,x)) = ((( eval (p1,x)) " ) * ( eval (p1,x))) by A55, A56

 .= ( 1. F_Complex ) by VECTSP_1:def 10, A57

 .= 1r by COMPLFLD:def 1;

 hence |.( eval (w,x)).| = 1 by COMPLEX1: 48;

 end;

 case

 A58: ( eval (p2,x)) <> 0 ;

 then

 A59: ( eval (p2,x)) <> ( 0. F_Complex ) by COMPLFLD:def 1;



 A60: ( eval (p2,x)) <> ( 0. F_Complex ) by A58, COMPLFLD:def 1;

 reconsider y1 = ( eval (p1,x)) as Complex;

 reconsider y2 = ( eval (p2,x)) as Complex;

 reconsider E1 = ( |.(( eval (w,x)) - 1).| ^2 ) as Real;

 ( Re (( eval (p1,x)) / ( eval (p2,x)))) = ( Re (y1 / y2)) by A59, COMPLFLD: 6

 .= 0 by A51, A52, Th1;

 then ( Re ( eval (z,x))) = 0 ;

 then

 A61: ((RW - 1) / E1) = 0 by A49, A60, A26;

 now

 per cases ;

 case ( |.(( eval (w,x)) - 1).| ^2 ) = 0 ;

 then |.(( eval (w,x)) - 1).| = 0 ;

 then (( eval (w,x)) - 1) = 0 by COMPLEX1: 45;

 hence |.( eval (w,x)).| = 1 by COMPLEX1: 48;

 end;

 case ( |.(( eval (w,x)) - 1).| ^2 ) <> 0 ;

 then (RW - 1) = 0 by A61;

 hence |.( eval (w,x)).| = 1 by A25, COMPLEX1: 46;

 end;

 end;

 hence |.( eval (w,x)).| = 1;

 end;

 end;

 then ( eval ((w `1 ),x)) <> 0 by COMPLEX1: 47;

 then ( eval ((p1 + p2),x)) <> ( 0. F_Complex ) by COMPLFLD:def 1;

 hence not (x is_a_root_of (p1 + p2)) by POLYNOM5:def 7;

 end;

 case ( Re x) > 0 & ( eval ((z `2 ),x)) <> 0 ;

 then ( Re ( eval (z,x))) > 0 by A1;

 then |.( eval (w,x)).| >= 1 by A33, A49;

 then ( eval ((w `1 ),x)) <> 0 by COMPLEX1: 47;

 then ( eval ((p1 + p2),x)) <> ( 0. F_Complex ) by COMPLFLD:def 1;

 hence not (x is_a_root_of (p1 + p2)) by POLYNOM5:def 7;

 end;

 case ( Re x) > 0 & ( eval ((z `2 ),x)) = 0 ;

 then

 A62: ( eval (p2,x)) = ( 0. F_Complex ) by COMPLFLD:def 1;



 A63: ( eval (pp,x)) = (( eval (p1,x)) - ( eval (p2,x))) by POLYNOM4: 21

 .= ( eval (p1,x)) by A62, RLVECT_1: 13;



 A64: ( eval ((p1 + p2),x)) = (( eval (p1,x)) + ( eval (p2,x))) by POLYNOM4: 19

 .= ( eval (p1,x)) by A62, RLVECT_1:def 4;

 A65:

 now

 assume ( eval (p1,x)) = ( 0. F_Complex );

 then x is_a_common_root_of (p1,p2) by A62, POLYNOM5:def 7;

 hence contradiction by A1;

 end;

 ( eval (w,x)) = ((( eval (p1,x)) " ) * ( eval (p1,x))) by A63, A64

 .= ( 1. F_Complex ) by VECTSP_1:def 10, A65

 .= 1r by COMPLFLD:def 1;

 then ( eval ((w `1 ),x)) <> 0 by COMPLEX1: 47, COMPLEX1: 48;

 then ( eval ((p1 + p2),x)) <> ( 0. F_Complex ) by COMPLFLD:def 1;

 hence not (x is_a_root_of (p1 + p2)) by POLYNOM5:def 7;

 end;

 end;

 hence not (x is_a_root_of (p1 + p2));

 end;

 end;

 hence not (x is_a_root_of (p1 + p2));

 end;

 hence (p1 + p2) is Hurwitz;

 end;

 end;

 theorem :: HURWITZ2:31

 for p be non constant with_positive_coefficients real Polynomial of F_Complex st [( even_part p), ( odd_part p)] is one_port_function & ( degree [( even_part p), ( odd_part p)]) = ( degree p) holds p is Hurwitz

 proof

 let p be non constant with_positive_coefficients real Polynomial of F_Complex ;

 set e = ( even_part p), o = ( odd_part p);

 set f = [e, o];

 assume

 A1: [e, o] is one_port_function & ( degree [e, o]) = ( degree p);



 A2: f is non zero;

 ( degree f) = ( max (( degree (f `1 )),( degree (f `2 )))) by A1, Th23;

 then f is irreducible by A2, RATFUNC1: 30;

 then (e + o) is Hurwitz by A1, Th30;

 hence p is Hurwitz by Th9;

 end;