:: A Test for the Stability of Networks
:: by Agnieszka Rowi\'nska-Schwarzweller and Christoph Schwarzweller
::
:: Received January 17, 2013
:: Copyright (c) 2013-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, POLYNOM2, COMPLFLD, POLYNOM1, ARYTM_1, FUNCT_1, REAL_1,
COMPLEX1, POLYNOM3, RELAT_1, RLVECT_1, FINSEQ_1, ZFMISC_1, INT_1,
VECTSP_1, ALGSEQ_1, GROUP_1, ALGSTR_1, POLYNOM5, SGRAPH1, ALGSTR_0,
FUNCT_4, RATFUNC1, MCART_1, HURWITZ, HURWITZ2, XBOOLE_0, POLYNOM4,
BINOP_1, PARTFUN1, LATTICES, XREAL_0, ABIAN, XCMPLX_0, SQUARE_1,
STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, NUMBERS, CARD_1, MESFUNC1, XXREAL_0,
VALUED_0, YELLOW_8;
notations TARSKI, SUBSET_1, VALUED_0, NUMBERS, ORDINAL1, XCMPLX_0, COMPLEX1,
COMPLFLD, XREAL_0, SQUARE_1, RELAT_1, ALGSTR_0, FUNCT_7, VECTSP_1,
ARYTM_3, FUNCT_1, FUNCT_2, NAT_1, NAT_D, INT_1, GROUP_1, ABIAN, BINOP_1,
XXREAL_0, STRUCT_0, ALGSTR_1, RLVECT_1, VFUNCT_1, NORMSP_1, ALGSEQ_1,
POLYNOM3, POLYNOM4, POLYNOM5, RATFUNC1, HURWITZ;
constructors BINOP_1, REAL_1, BINARITH, ALGSTR_1, POLYNOM5, BHSP_1, RELSET_1,
FUNCT_4, ARYTM_3, ABIAN, NAT_D, SQUARE_1, POLYNOM4, VFUNCT_1, RATFUNC1,
HURWITZ, ALGSEQ_1, BINOP_2, XXREAL_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, INT_1, NAT_1,
MEMBERED, STRUCT_0, VECTSP_1, COMPLFLD, ALGSTR_1, POLYNOM4, POLYNOM5,
XREAL_0, VALUED_0, ABIAN, FUNCT_2, RATFUNC1, POLYNOM3, VFUNCT_1,
XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions RATFUNC1;
equalities POLYNOM3, ALGSTR_0, SQUARE_1, XCMPLX_0, HURWITZ, RATFUNC1;
expansions ALGSEQ_1, HURWITZ, RATFUNC1, UPROOTS;
theorems VECTSP_1, ALGSEQ_1, FUNCT_1, FUNCT_2, POLYNOM3, FUNCOP_1, RLVECT_1,
POLYNOM4, GROUP_1, TARSKI, RATFUNC1, HURWITZ, INT_1, COMPLFLD, POLYNOM5,
ALGSTR_1, COMPLEX1, FUNCT_7, NAT_1, BHSP_1, NORMSP_1, ORDINAL1, XREAL_0,
VALUED_0, XREAL_1, XXREAL_0, ABIAN, XCMPLX_1, SQUARE_1, UPROOTS;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
theorem Th1:
for x,y being 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
for a being 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) * <i> by A1,SQUARE_1:def 2
.= Re ac * Re ac - Im ac * (- Im ac) +
(Re ac * Im b + Re ac * Im ac) * <i> by COMPLEX1:27
.= Re ac * Re ac - Im ac * Im b +
(Re ac * Im b + Re ac * Im ac) * <i> by COMPLEX1:27
.= Re ac * Re ac - Im ac * Im b +
(Re ac * Im b + Re b * Im ac) * <i> by COMPLEX1:27
.= Re ac * Re b - Im ac * Im b +
(Re ac * Im b + Re b * Im ac) * <i> 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 Th3:
for L being add-associative right_zeroed right_complementable
associative distributive non empty doubleLoopStr
for k being even Element of NAT
for x being 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 being 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 being 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 being Nat holds P[k] from NAT_1:sch 4(A1);
hence thesis;
end;
theorem Th4:
for L being add-associative right_zeroed right_complementable
associative distributive non empty doubleLoopStr
for k being odd Element of NAT
for x being 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 Th5:
for k being even Element of NAT
for x being 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 being Element of NAT st k1 = $1 & k1 is even
for x being 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 being 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 being 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 being Nat holds P[k] from NAT_1:sch 4(A2);
hence thesis by A1;
end;
theorem Th6:
for k being odd Element of NAT
for x being 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 being Element of NAT st k1 = $1 & k1 is odd
for x being 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 being 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 being 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 being Nat holds P[k] from NAT_1:sch 4(A2);
hence thesis by A1;
end;
begin :: Even and Odd Part of Polynomials
definition
let L be non empty ZeroStr;
let p be sequence of L;
func even_part p -> sequence of L means :Def1:
for i being even Nat holds it.i = p.i &
for i being odd Nat holds it.i = 0.L;
existence
proof
defpred P[object,object] means
for i being 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 being 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 being Function of NAT,the carrier of L such that
A5: for x being 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 being even Nat holds z1.i = p.i &
for i being odd Nat holds z1.i = 0.L;
assume A8: for i being even Nat holds z2.i = p.i &
for i being 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;
func odd_part p -> sequence of L means :Def2:
for i being even Nat holds it.i = 0.L &
for i being odd Nat holds it.i = p.i;
existence
proof
defpred P[object, object] means
for i being 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 being 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 being Function of NAT,the carrier of L such that
A16: for x being 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 being even Nat holds z1.i = 0.L &
for i being odd Nat holds z1.i = p.i;
assume A19: for i being even Nat holds z2.i = 0.L &
for i being 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 being Nat st for i being 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 being Nat st for i being 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 Th7:
for L being 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
for L being 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 Th9:
for L being left_zeroed right_zeroed non empty addLoopStr,
p being 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 Th10:
for L being left_zeroed right_zeroed non empty addLoopStr,
p being 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
for L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being 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
for L being add-associative right_zeroed right_complementable
non empty addLoopStr,
p being 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
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p being 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
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p being 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 Th15:
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p,q being 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 Th16:
for L being add-associative right_zeroed right_complementable
Abelian non empty addLoopStr,
p,q being 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 Th17:
for L being well-unital non empty doubleLoopStr
for p being 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 Th18:
for L being well-unital non empty doubleLoopStr
for p being 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 Th19:
for L being well-unital non empty doubleLoopStr
for p being 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 Th20:
for L being well-unital non empty doubleLoopStr
for p being 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 Th21:
for L being well-unital add-associative right_zeroed right_complementable
Abelian associative distributive non degenerated doubleLoopStr
for p being 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
for L being well-unital add-associative right_zeroed right_complementable
associative Abelian distributive non degenerated doubleLoopStr
for p being 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 Th23:
for L being well-unital add-associative right_zeroed right_complementable
associative Abelian distributive non degenerated doubleLoopStr
for p being 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 :: Even and Odd Polynomials and Rational Functions
definition
let L be non empty addLoopStr;
let f be Function of L,L;
attr f is even means :Def3:
for x being Element of L holds f.(-x) = f.x;
attr f is odd means :Def4:
for x being Element of L holds f.(-x) = - f.x;
end;
definition
let L be well-unital non empty doubleLoopStr;
let p be Polynomial of L;
attr p is even means :Def5:
Polynomial-Function(L,p) is even;
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;
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 Th24:
for L being well-unital non empty doubleLoopStr
for p being even Polynomial of L
for x being 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 Th25:
for L being add-associative right_zeroed right_complementable Abelian
well-unital non degenerated doubleLoopStr
for p being odd Polynomial of L
for x being 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 being Polynomial of L st len p = $1
holds even_part(p) is even;
A1: now let k be Nat;
assume A2: for n being 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 being Polynomial of L such that
A6: len t < len p & p = t + Leading-Monomial(p) &
for n being 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 being Nat holds P[k] from NAT_1:sch 4(A1);
consider k being 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 being Polynomial of L st len p = $1
holds odd_part(p) is odd;
A12: now let k be Nat;
assume A13: for n being 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 being Polynomial of L such that
A17: len t < len p & p = t + Leading-Monomial(p) &
for n being 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 being Nat holds P[k] from NAT_1:sch 4(A12);
consider k being Nat such that A23: len p = k;
thus thesis by A23,A22;
end;
end;
theorem Th26:
for L being Abelian add-associative right_zeroed right_complementable
well-unital distributive non degenerated doubleLoopStr
for p being even Polynomial of L
for q being odd Polynomial of L
for x being 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
for p being 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;
end;
begin :: Real Positive Polynomials and Rational Functions
definition
let p be Polynomial of F_Complex;
attr p is real means :Def8:
for i being Nat holds p.i is Real;
attr p is positive means
for x being 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 being 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;
attr p is with_all_coefficients means :Def10:
for i being Nat st i <= deg p holds p.i <> 0;
end;
definition
let p be real Polynomial of F_Complex;
attr p is with_positive_coefficients means
for i being Nat st i <= deg p holds p.i > 0;
attr p is with_negative_coefficients means
for i being 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 being Nat st for i being 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;
attr Z is real means
for i being Nat holds (Z`1).i is Real & (Z`2).i is Real;
attr Z is positive means
for x being 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 for rational_function of F_Complex;
coherence;
end;
begin :: The Theorem
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 Th28:
for p being real Polynomial of F_Complex
for x being 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 being Polynomial of F_Complex st p is real & len p = $1 holds
(for x being 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 being 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 being 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 being 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 being Polynomial of F_Complex such that
A8: len t < len p & p = t + Leading-Monomial(p) &
for n being 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 being Element of F_Complex st Re(x) = 0
holds Im(eval(even_part(p),x)) = 0;
end;
hence P[k];
end;
A18: for k being Nat holds P[k] from NAT_1:sch 4(A1);
consider n being Nat such that A19: len p = n;
thus thesis by A18,A19;
end;
theorem Th29:
for p being real Polynomial of F_Complex
for x being 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 being Polynomial of F_Complex st p is real & len p = $1 holds
(for x being 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 being 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 being 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 being 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 being Polynomial of F_Complex such that
A8: len t < len p & p = t + Leading-Monomial(p) &
for n being 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 being Element of F_Complex st Re(x) = 0
holds Re(eval(odd_part(p),x)) = 0;
end;
hence P[k];
end;
A18: for k being Nat holds P[k] from NAT_1:sch 4(A1);
consider n being Nat such that A19: len p = n;
thus thesis by A18,A19;
end;
theorem 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 being 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 being 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 being 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 being 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;
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;
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))"
.= (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))"
.= ((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
.= (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 being 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 being 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 being 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
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;