:: Fundamental Theorem of Algebra
:: by Robert Milewski
::
:: Received August 21, 2000
:: Copyright (c) 2000-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 NUMBERS, SUBSET_1, CARD_1, RELAT_1, ARYTM_1, ARYTM_3, XXREAL_0,
REAL_1, FINSEQ_1, FUNCT_1, CARD_3, ORDINAL4, TARSKI, PARTFUN1, XBOOLE_0,
HAHNBAN1, XCMPLX_0, COMPLFLD, SUPINF_2, COMPLEX1, GROUP_1, POWER,
STRUCT_0, NAT_1, RLVECT_1, ALGSTR_0, VECTSP_1, BINOP_1, LATTICES,
POLYNOM1, ALGSEQ_1, POLYNOM3, POLYNOM2, VECTSP_2, MESFUNC1, AFINSQ_1,
FUNCT_4, CQC_LANG, CFCONT_1, FUNCOP_1, VALUED_1, FUNCT_2, SEQ_4,
XXREAL_2, COMSEQ_1, VALUED_0, SEQ_2, ORDINAL2, SEQ_1, COMPTRIG, RFINSEQ,
POLYNOM5, FUNCT_7, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_2,
XREAL_0, COMPLEX1, REAL_1, POWER, BINOP_1, NAT_1, RELAT_1, FUNCT_1,
FUNCT_2, PARTFUN1, FUNCOP_1, FINSEQ_1, FINSEQ_4, POLYNOM1, RVSUM_1,
STRUCT_0, ALGSTR_0, RLVECT_1, FUNCSDOM, VECTSP_2, VECTSP_1, RFINSEQ,
CFCONT_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, SEQ_4, XXREAL_0, COMSEQ_1,
COMSEQ_2, NAT_D, COMPLFLD, HAHNBAN1, ALGSEQ_1, POLYNOM3, POLYNOM4,
FUNCT_7, RECDEF_1, GROUP_1;
constructors FINSEQ_4, ENUMSET1, REAL_1, SEQ_4, FINSOP_1, COMSEQ_2, RVSUM_1,
CFCONT_1, RFINSEQ, NAT_D, FUNCSDOM, VECTSP_2, ALGSTR_1, MATRIX_1,
HAHNBAN1, POLYNOM1, POLYNOM4, RECDEF_1, BINOP_2, POWER, SEQ_2, RELSET_1,
FUNCT_7, FVSUM_1, ALGSEQ_1, ORDINAL1, SEQ_1, GROUP_1;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, GROUP_1,
VECTSP_1, COMPLFLD, ALGSTR_1, POLYNOM3, POLYNOM4, VALUED_0, VALUED_1,
CARD_1, SEQ_2, CFUNCT_1, SEQ_1, RVSUM_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, ALGSEQ_1, XBOOLE_0, ALGSTR_0, XXREAL_2, COMSEQ_2;
equalities XBOOLE_0, RVSUM_1, POLYNOM3, HAHNBAN1, STRUCT_0, ALGSTR_0,
XCMPLX_0;
expansions TARSKI, ALGSEQ_1, COMSEQ_2;
theorems XREAL_0, TARSKI, ENUMSET1, NAT_1, POWER, INT_1, ABSVALUE, FUNCT_1,
FUNCT_2, FUNCT_7, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSEQ_5,
FUNCOP_1, TBSP_1, RFINSEQ, PRE_FF, CFCONT_1, TOPREAL3, INTEGRA5,
RLVECT_1, VECTSP_1, RVSUM_1, SEQ_2, SEQM_3, SEQ_4, COMSEQ_2, COMSEQ_3,
CFUNCT_1, FVSUM_1, GROUP_1, ALGSEQ_1, COMPLEX1, COMPLFLD, HAHNBAN1,
POLYNOM1, POLYNOM2, POLYNOM3, POLYNOM4, XBOOLE_0, XCMPLX_1, VECTSP_2,
XREAL_1, XXREAL_0, FINSOP_1, NORMSP_1, PARTFUN1, ORDINAL1, VALUED_1,
CARD_1, NAT_D, VALUED_0, XCMPLX_0, SEQ_1;
schemes NAT_1, FUNCT_2, FINSEQ_2, FINSEQ_1, FINSEQ_4, SEQ_1, CFCONT_1,
DOMAIN_1, FUNCT_7;
begin :: Preliminaries
theorem Th1:
for n,m be Nat st n <> 0 & m <> 0 holds n*m - n - m + 1 >= 0
proof
let n,m be Nat;
assume that
A1: n <> 0 and
A2: m <> 0;
m >= 0+1 by A2,NAT_1:13;
then
A3: m-1 >= 0+1-1;
n >= 0+1 by A1,NAT_1:13;
then n-1 >= 0+1-1;
then (n-1)*(m-1) >= 0 by A3;
hence thesis;
end;
theorem Th2:
for x,y be Real st y > 0 holds min(x,y)/max(x,y) <= 1
proof
let x,y be Real;
assume
A1: y > 0;
per cases;
suppose
A2: x > 0;
now
per cases;
suppose
A3: x >= y;
then max(x,y) = x & min(x,y) = y by XXREAL_0:def 9,def 10;
hence thesis by A1,A3,XREAL_1:183;
end;
suppose
A4: x < y;
then max(x,y) = y & min(x,y) = x by XXREAL_0:def 9,def 10;
hence thesis by A2,A4,XREAL_1:183;
end;
end;
hence thesis;
end;
suppose
A5: x <= 0;
then min (x,y) = x & max (x,y) = y by A1,XXREAL_0:def 9,def 10;
hence thesis by A1,A5;
end;
end;
theorem Th3:
for x,y be Real st for c be Real st c > 0 & c < 1
holds c*x >= y holds y <= 0
proof
let x,y be Real;
assume
A1: for c be Real st c > 0 & c < 1 holds c*x >= y;
set ma = max(x,y);
set mi = min(x,y);
set c = mi/(2*ma);
assume
A2: y > 0;
then
A3: y*2 > y by XREAL_1:155;
per cases;
suppose
A4: x > 0;
then
A5: mi > 0 & ma > 0 by A2,XXREAL_0:15,16;
then mi/ma*2 > mi/ma by XREAL_1:155;
then mi/ma > mi/ma/2 by XREAL_1:83;
then
A6: mi/ma > mi/(ma*2) by XCMPLX_1:78;
mi/ma <= 1 by A4,Th2;
then c < 1 by A6,XXREAL_0:2;
then
A7: c*x >= y by A1,A5;
now
per cases;
suppose
x >= y;
then ma = x & mi = y by XXREAL_0:def 9,def 10;
then c*x = y/2 by A4,XCMPLX_1:92;
hence contradiction by A3,A7,XREAL_1:83;
end;
suppose
A8: x < y;
then ma = y & mi = x by XXREAL_0:def 9,def 10;
then c*x < x/(2*y)*y by A4,A8,XREAL_1:98;
then
A9: c*x < x/2 by A2,XCMPLX_1:92;
A10: y > y/2 by A3,XREAL_1:83;
x/2 < y/2 by A8,XREAL_1:74;
then c*x < y/2 by A9,XXREAL_0:2;
hence contradiction by A7,A10,XXREAL_0:2;
end;
end;
hence contradiction;
end;
suppose
x <= 0;
then 1/2*x <= 0;
hence contradiction by A1,A2;
end;
end;
Lm1: for x,y be Real st
for c be Real st c > 0 & c < 1 holds c*x >= y holds y
<= 0
by Th3;
theorem Th4:
for p be FinSequence of REAL st for n be Element of NAT st n in
dom p holds p.n >= 0 for i be Element of NAT st i in dom p holds Sum p >= p.i
proof
defpred Q[FinSequence of REAL] means (for n be Element of NAT st n in dom $1
holds $1.n >= 0) implies for i be Element of NAT st i in dom $1 holds Sum $1 >=
$1.i;
A1: for p be FinSequence of REAL for x be Element of REAL st Q[p] holds Q[p^
<*x*>]
proof
let p be FinSequence of REAL;
let x be Element of REAL;
assume
A2: (for n be Element of NAT st n in dom p holds p.n >= 0) implies for
i be Element of NAT st i in dom p holds Sum p >= p.i;
defpred P[Nat] means Sum (p|$1) >= 0;
assume
A3: for n be Element of NAT st n in dom (p^<*x*>) holds (p^<*x*>).n >= 0;
A4: dom p c= dom (p^<*x*>) by FINSEQ_1:26;
A5: now
let n be Element of NAT;
assume
A6: n in dom p;
then (p^<*x*>).n >= 0 by A3,A4;
hence p.n >= 0 by A6,FINSEQ_1:def 7;
end;
A7: for j be Nat st P[j] holds P[j+1]
proof
let j be Nat;
assume
A8: Sum (p|j) >= 0;
per cases;
suppose
A9: j+1 <= len p;
then p|(j+1) = p|j ^ <*p/.(j+1)*> by FINSEQ_5:82; then
A10: Sum (p|(j+1)) = Sum(p|j) + p/.(j+1) by RVSUM_1:74;
j+1 >= 1 by NAT_1:11;
then
A11: j+1 in dom p by A9,FINSEQ_3:25;
then p.(j+1) >= 0 by A5;
then p/.(j+1) >= 0 by A11,PARTFUN1:def 6;
hence thesis by A8,A10;
end;
suppose
A12: j+1 > len p;
then j >= len p by NAT_1:13;
then p|j = p by FINSEQ_1:58;
hence thesis by A8,A12,FINSEQ_1:58;
end;
end;
let i be Element of NAT;
len p+1 >= 0+1 by XREAL_1:6;
then len (p^<*x*>) >= 1 by FINSEQ_2:16;
then len (p^<*x*>) in dom (p^<*x*>) by FINSEQ_3:25;
then (p^<*x*>).len (p^<*x*>) >= 0 by A3;
then (p^<*x*>).(len p+1) >= 0 by FINSEQ_2:16;
then x >= 0 by FINSEQ_1:42;
then
A13: p.i + x >= p.i + 0 by XREAL_1:6;
A14: p|(len p) = p by FINSEQ_1:58;
len (p^<*x*>) = len p+1 by FINSEQ_2:16;
then
A15: dom (p^<*x*>) = Seg (len p+1) by FINSEQ_1:def 3
.= Seg len p \/ {len p+1} by FINSEQ_1:9
.= dom p \/ {len p+1} by FINSEQ_1:def 3;
A16: P[0] by RVSUM_1:72;
for j be Nat holds P[j] from NAT_1:sch 2(A16,A7);
then
A17: Sum p >= 0 by A14;
assume
A18: i in dom (p^<*x*>);
per cases by A18,A15,XBOOLE_0:def 3;
suppose
A19: i in dom p;
A20: Sum (p^<*x*>) = Sum p + x by RVSUM_1:74;
Sum p >= p.i by A2,A5,A19;
then Sum (p^<*x*>) >= p.i + x by A20,XREAL_1:6;
then Sum (p^<*x*>) >= p.i by A13,XXREAL_0:2;
hence thesis by A19,FINSEQ_1:def 7;
end;
suppose
i in {len p+1};
then i = len p+1 by TARSKI:def 1;
then (p^<*x*>).i = x by FINSEQ_1:42;
then Sum p + x >= 0+(p^<*x*>).i by A17,XREAL_1:6;
hence thesis by RVSUM_1:74;
end;
end;
A21: Q[<*>(REAL)];
thus for p be FinSequence of REAL holds Q[p] from FINSEQ_2:sch 2(A21, A1);
end;
theorem
for x,y be Real holds -[**x,y**] = [**-x,-y**]
proof
let x,y be Real;
thus -[**x,y**] = -(x+y*<i>)
.= [**-x,-y**];
end;
theorem
for x1,y1,x2,y2 be Real holds
[**x1,y1**] - [**x2,y2**] = [**x1 - x2,y1 - y2**]
proof
let x1,y1,x2,y2 be Real;
thus [**x1,y1**]-[**x2,y2**] = [**x1,y1**]+[**-x2,-y2**]
.= [**x1-x2,y1-y2**];
end;
definition let R be non empty multMagma;
let z be Element of R, n be Nat;
func power(z,n) -> Element of R equals
power(R).(z,n);
coherence;
end;
theorem Th7:
for z be Element of F_Complex st z <> 0.F_Complex
for n be Nat holds |.power(z,n).| = |.z.| to_power n
proof
let z be Element of F_Complex;
defpred P[Nat] means |.power(z,$1).| = |.z.|
to_power $1;
assume z <> 0.F_Complex;
then
A1: |.z.| <> 0 by COMPLFLD:58;
A2: |.z.| >= 0 by COMPLEX1:46;
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: |.power(z,n).| = |.z.| to_power n;
thus |.power(z,n+1).| = |.(power F_Complex).(z,n)*z.| by
GROUP_1:def 7
.= (|.z.| to_power n)*|.z.| by A4,COMPLFLD:71
.= (|.z.| to_power n)*(|.z.| to_power 1) by POWER:25
.= |.z.| to_power (n+1) by A1,A2,POWER:27;
end;
|.(power F_Complex).(z,0).| = 1 by COMPLEX1:48,COMPLFLD:8,GROUP_1:def 7
.= |.z.| to_power 0 by POWER:24;
then
A5: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A5,A3);
end;
definition
let p be complex-valued FinSequence;
redefine func |.p.| -> FinSequence of REAL means :: redefines |. (VALUED_1, definition)
:Def2:
len it = len p &
for n be Nat st n in dom p holds it.n = |.p.n.|;
coherence by RVSUM_1:145;
compatibility
proof
let f be FinSequence of REAL;
hereby
assume
A1: f = |.p.|;
dom |.p.| = dom p by VALUED_1:def 11;
hence len f = len p by A1,FINSEQ_3:29;
let n be Nat such that n in dom p;
thus f.n = |.p.n.| by A1,VALUED_1:18;
end;
assume that
A1: len f = len p and
A2: for n be Nat st n in dom p holds f.n = |.p.n.|;
A3: dom f = dom p by A1,FINSEQ_3:29;
then for c be object st c in dom f holds f.c = |.p.c.| by A2;
hence f = |.p.| by A3,VALUED_1:def 11;
end;
end;
theorem Th8:
|.<*>the carrier of F_Complex.| = <*>REAL
proof
len |.<*>the carrier of F_Complex.| = len <*>the carrier of F_Complex by Def2
.= 0;
hence thesis;
end;
theorem Th9:
for x be Complex holds |.<*x*>.| = <*|.x.|*>
proof
let x be Complex;
0+1 in Seg (0+1) by FINSEQ_1:4;
then
A1: 1 in dom <*x*> by FINSEQ_1:38;
A2: len |.<*x*>.| = len <*x*> by Def2
.= 1 by FINSEQ_1:39;
then
A3: dom |.<*x*>.| = Seg 1 by FINSEQ_1:def 3;
A5: now
let n be Nat;
assume n in dom |.<*x*>.|;
then
A6: n = 1 by A3,FINSEQ_1:2,TARSKI:def 1;
hence |.<*x*>.|.n = |.<*x*>.1 .| by A1,Def2
.= |.x.|
.= <*|.x.|*>.n by A6;
end;
len <*|.x.|*> = 1 by FINSEQ_1:39;
hence thesis by A2,A5,FINSEQ_2:9;
end;
theorem
for x,y be Complex holds |.<*x,y*>.| = <*|.x.|,|.y.|*>
proof
let x,y be Complex;
A1: len |.<*x,y*>.| = len <*x,y*> by Def2
.= 2 by FINSEQ_1:44;
then
A2: dom |.<*x,y*>.| = Seg 2 by FINSEQ_1:def 3;
A3: now
let n be Nat;
assume
A4: n in dom |.<*x,y*>.|;
per cases by A2,A4,FINSEQ_1:2,TARSKI:def 2;
suppose
A5: n = 1;
then
A6: 1 in dom <*x,y*> by A2,A4,FINSEQ_1:89;
|.<*x,y*>.|.1 = |.<*x,y*>.1 .| by A6,Def2;
then |.<*x,y*>.|.1 = |.x.|;
hence |.<*x,y*>.|.n = <*|.x.|,|.y.|*>.n by A5;
end;
suppose
A7: n = 2;
then
A8: 2 in dom <*x,y*> by A2,A4,FINSEQ_1:89;
|.<*x,y*>.|.2 = |.<*x,y*>.2 .| by A8,Def2;
then |.<*x,y*>.|.2 = |.y.|;
hence |.<*x,y*>.|.n = <*|.x.|,|.y.|*>.n by A7;
end;
end;
len <*|.x.|,|.y.|*> = 2 by FINSEQ_1:44;
hence thesis by A1,A3,FINSEQ_2:9;
end;
theorem
for x,y,z be Complex holds |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>
proof
let x,y,z be Complex;
A1: len |.<*x,y,z*>.| = len <*x,y,z*> by Def2
.= 3 by FINSEQ_1:45;
then
A2: dom |.<*x,y,z*>.| = Seg 3 by FINSEQ_1:def 3;
A3: now
let n be Nat;
assume
A4: n in dom |.<*x,y,z*>.|;
per cases by A2,A4,ENUMSET1:def 1,FINSEQ_3:1;
suppose
A5: n = 1;
A6: 1 in dom <*x,y,z*> by FINSEQ_1:81;
|.<*x,y,z*>.|.1 = |.<*x,y,z*>.1 .| by A6,Def2;
then |.<*x,y,z*>.|.1 = |.x.|;
hence |.<*x,y,z*>.|.n = <*|.x.|,|.y.|,|.z.|*>.n by A5;
end;
suppose
A7: n = 2;
A8: 2 in dom <*x,y,z*> by FINSEQ_1:81;
|.<*x,y,z*>.|.2 = |.<*x,y,z*>.2 .| by A8,Def2;
then |.<*x,y,z*>.|.2 = |.y.|;
hence |.<*x,y,z*>.|.n = <*|.x.|,|.y.|,|.z.|*>.n by A7;
end;
suppose
A9: n = 3;
A10: 3 in dom <*x,y,z*> by FINSEQ_1:81;
|.<*x,y,z*>.|.3 = |.<*x,y,z*>.3 .| by A10,Def2;
then |.<*x,y,z*>.|.3 = |.z.|;
hence |.<*x,y,z*>.|.n = <*|.x.|,|.y.|,|.z.|*>.n by A9;
end;
end;
len <*|.x.|,|.y.|,|.z.|*> = 3 by FINSEQ_1:45;
hence thesis by A1,A3,FINSEQ_2:9;
end;
theorem Th12:
for p,q be complex-valued FinSequence holds |.p^q.| = |.p.|^|.q.|
proof
let p,q be complex-valued FinSequence;
A1: dom |.p^q.| = Seg len |.p^q.| by FINSEQ_1:def 3;
A2: now
let n be Nat;
A3: len |.p.| = len p by Def2;
assume
A4: n in dom |.p^q.|;
then
A5: n >= 1 by A1,FINSEQ_1:1;
A6: len |.p^q.| = len (p^q) by Def2;
then
A7: n in dom (p^q) by A1,A4,FINSEQ_1:def 3;
per cases;
suppose
A8: n in dom p;
A9: (p^q).n = p.n by A8,FINSEQ_1:def 7;
A10: n in dom |.p.| by A3,A8,FINSEQ_3:29;
thus |.p^q.|.n = |.(p^q).n.| by A7,Def2
.= |.p.|.n by A8,A9,Def2
.= (|.p.|^|.q.|).n by A10,FINSEQ_1:def 7;
end;
suppose
not n in dom p;
then
A11: n > 0 + len p by A5,FINSEQ_3:25;
then
A12: n - len p > 0 by XREAL_1:20;
A13: n = len p + (n-len p) .= len p + (n-'len p) by A12,XREAL_0:def 2;
n <= len (p^q) by A1,A4,A6,FINSEQ_1:1;
then n <= len q + len p by FINSEQ_1:22;
then n-len p <= len q by XREAL_1:20;
then
A14: n-'len p <= len q by XREAL_0:def 2;
1 + len p <= n by A11,NAT_1:13;
then 1 <= n-len p by XREAL_1:19;
then 1 <= n-'len p by XREAL_0:def 2;
then
A15: (n-'len p) in Seg len q by A14,FINSEQ_1:1;
then
A16: (n-'len p) in dom q by FINSEQ_1:def 3;
len |.q.| = len q by Def2;
then
A17: (n-'len p) in dom |.q.| by A15,FINSEQ_1:def 3;
A18: (p^q).n = q.(n-'len p) by A13,A16,FINSEQ_1:def 7;
thus |.p^q.|.n = |.(p^q).n.| by A7,Def2
.= |.q.|.(n-'len p) by A16,A18,Def2
.= (|.p.|^|.q.|).n by A3,A13,A17,FINSEQ_1:def 7;
end;
end;
len |.p^q.| = len (p^q) by Def2
.= len p + len q by FINSEQ_1:22
.= len p + len |.q.| by Def2
.= len |.p.| + len |.q.| by Def2
.= len (|.p.|^|.q.|) by FINSEQ_1:22;
hence thesis by A2,FINSEQ_2:9;
end;
theorem
for p be complex-valued FinSequence
for x be Complex holds
|.p^<*x*>.| = |.p.|^<*|.x.|*> & |.<*x*>^p.| = <*|.x.|*>^|.p.|
proof
let p be complex-valued FinSequence;
let x be Complex;
thus |.p^<*x*>.| = |.p.|^|.<*x*>.| by Th12
.= |.p.|^<*|.x.|*> by Th9;
thus |.<*x*>^p.| = |.<*x*>.|^|.p.| by Th12
.= <*|.x.|*>^|.p.| by Th9;
end;
theorem Th14:
for p be FinSequence of the carrier of F_Complex holds |.Sum p.| <= Sum|.p.|
proof
set D = the carrier of F_Complex;
defpred P[FinSequence of D] means |.Sum $1.| <= Sum|.$1.|;
A1: now
let p be FinSequence of D;
let x be Element of D;
assume P[p];
then
A2: |.Sum p.| + |.x.| <= Sum|.p.| + |.x.| by XREAL_1:6;
Sum (p^<*x*>) = Sum p + x by FVSUM_1:71;
then
A3: |.Sum (p^<*x*>).| <= |.Sum p.| + |.x.| by COMPLFLD:62;
reconsider xx = |.x.| as Element of REAL by XREAL_0:def 1;
Sum|.p.| + |.x.| = Sum|.p.| + Sum <*xx*> by FINSOP_1:11
.= Sum|.p.| + Sum |.<*x*>.| by Th9
.= Sum(|.p.|^|.<*x*>.|) by RVSUM_1:75
.= Sum|.p^<*x*>.| by Th12;
hence P[p^<*x*>] by A2,A3,XXREAL_0:2;
end;
A4: P[<*>D] by Th8,COMPLFLD:57,RLVECT_1:43,RVSUM_1:72;
thus for p be FinSequence of D holds P[p] from FINSEQ_2:sch 2(A4,A1 );
end;
begin :: Operations on Polynomials
definition
let L be Abelian add-associative right_zeroed right_complementable
right_unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
let n be Nat;
func p`^n -> sequence of L equals
(power Polynom-Ring L).(p,n);
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p as Element of Polynom-Ring L by POLYNOM3:def 10;
(power Polynom-Ring L).(p1,n) is Element of Polynom-Ring L;
hence thesis by POLYNOM3:def 10;
end;
end;
registration
let L be Abelian add-associative right_zeroed right_complementable
right_unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
let n be Nat;
cluster p`^n -> finite-Support;
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p as Element of Polynom-Ring L by POLYNOM3:def 10;
(power Polynom-Ring L).(p1,n) is Polynomial of L by POLYNOM3:def 10;
hence thesis;
end;
end;
theorem Th15:
for L be Abelian add-associative right_zeroed
right_complementable well-unital commutative distributive non empty
doubleLoopStr for p be Polynomial of L holds p`^0 = 1_.(L)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
reconsider p1=p as Element of Polynom-Ring L by POLYNOM3:def 10;
thus p`^0 = (power Polynom-Ring L).(p1,0)
.= 1_(Polynom-Ring L) by GROUP_1:def 7
.= 1_.(L) by POLYNOM3:37;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr for p be
Polynomial of L holds p`^1 = p
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
reconsider p1=p as Element of Polynom-Ring L by POLYNOM3:def 10;
thus p`^1 = (power Polynom-Ring L).(p1,0+1)
.= (power Polynom-Ring L).(p1,0)*p1 by GROUP_1:def 7
.= (1_Polynom-Ring L)*p1 by GROUP_1:def 7
.= p;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr for p be
Polynomial of L holds p`^2 = p*'p
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
reconsider p1=p as Element of Polynom-Ring L by POLYNOM3:def 10;
thus p`^2 = (power Polynom-Ring L).(p1,1+1)
.= power(p1,0+1)*p1 by GROUP_1:def 7
.= (power Polynom-Ring L).(p1,0)*p1*p1 by GROUP_1:def 7
.= (1_Polynom-Ring L)*p1*p1 by GROUP_1:def 7
.= p1*p1
.= p*'p by POLYNOM3:def 10;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr for p be
Polynomial of L holds p`^3 = p*'p*'p
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
reconsider p1=p as Element of Polynom-Ring L by POLYNOM3:def 10;
reconsider pp=p1*p1 as Polynomial of L by POLYNOM3:def 10;
thus p`^3 = (power Polynom-Ring L).(p1,2+1)
.= power(p1,1+1)*p1 by GROUP_1:def 7
.= power(p1,0+1)*p1*p1 by GROUP_1:def 7
.= (power Polynom-Ring L).(p1,0)*p1*p1*p1 by GROUP_1:def 7
.= (1_Polynom-Ring L)*p1*p1*p1 by GROUP_1:def 7
.= p1*p1*p1
.= pp*'p by POLYNOM3:def 10
.= p*'p*'p by POLYNOM3:def 10;
end;
theorem Th19:
for L be Abelian add-associative right_zeroed
right_complementable well-unital commutative distributive non empty
doubleLoopStr for p be Polynomial of L
for n be Nat holds p`^(n+1) = (p`^n)*'p
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
reconsider p1=p as Element of Polynom-Ring L by POLYNOM3:def 10;
thus p`^(n+1) = (power Polynom-Ring L).(p1,nn)*p1 by GROUP_1:def 7
.= (p`^n)*'p by POLYNOM3:def 10;
end;
theorem Th20:
for L be Abelian add-associative right_zeroed
right_complementable well-unital commutative distributive non empty
doubleLoopStr for n be Element of NAT holds 0_.(L)`^(n+1) = 0_.(L)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let n be Element of NAT;
thus 0_.(L)`^(n+1) = (0_.(L)`^n)*'0_.(L) by Th19
.= 0_.(L) by POLYNOM3:34;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr
for n be Nat holds 1_.(L)`^n = 1_.(L)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
defpred P[Nat] means 1_.(L)`^$1 = 1_.(L);
A1: now
let n be Nat;
assume P[n];
then 1_.(L)`^(n+1) = (1_.(L))*'1_.(L) by Th19
.= 1_.(L) by POLYNOM3:35;
hence P[n+1];
end;
A2: P[0] by Th15;
thus for n be Nat holds P[n] from NAT_1:sch 2(A2,A1);
end;
theorem Th22:
for L be non degenerated commutative
Abelian add-associative right_zeroed right_complementable
associative well-unital distributive non empty doubleLoopStr
for p be Polynomial of L for x be Element of L
for n be Nat holds eval(p`^n,x) = (power L).(eval(p,x),n)
proof
let L be non degenerated commutative
Abelian add-associative right_zeroed right_complementable
associative well-unital distributive non empty doubleLoopStr;
let p be Polynomial of L;
let x be Element of L;
defpred P[Nat] means eval(p`^$1,x) = (power L).(eval(p,x),$1);
A1: now
let n be Nat;
assume
A2: P[n];
eval(p`^(n+1),x) = eval((p`^n)*'p,x) by Th19
.= (power L).(eval(p,x),n)*eval(p,x) by A2,POLYNOM4:24
.= (power L).(eval(p,x),n+1) by GROUP_1:def 7;
hence P[n+1];
end;
eval(p`^0,x) = eval(1_.(L),x) by Th15
.= 1_(L) by POLYNOM4:18
.= (power L).(eval(p,x),0) by GROUP_1:def 7;
then
A3: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
end;
Lm2: for L being non empty ZeroStr, p being AlgSequence of L st len p > 0
holds p.(len p -'1) <> 0.L
proof
let L be non empty ZeroStr, p be AlgSequence of L;
assume len p > 0;
then ex k being Nat st len p = k+1 by NAT_1:6;
then len p = (len p -'1)+1 by NAT_D:34;
hence thesis by ALGSEQ_1:10;
end;
theorem Th23:
for L be domRing for p be Polynomial of L st len p <> 0
for n be Nat holds len(p`^n) = n*len p-n+1
proof
let L be domRing;
let p be Polynomial of L;
defpred P[Nat] means len(p`^$1) = $1*len p-$1+1;
assume
A1: len p <> 0;
A2: now
len p >= 0+1 by A1,NAT_1:13;
then len p-1 >= 0+1-1;
then
A3: len p-'1 = len p-1 by XREAL_0:def 2;
A4: p.(len p -'1) <> 0.L by A1,Lm2;
let n be Nat;
assume
A5: P[n];
n*(len p-'1)+1 >= 0+1 by XREAL_1:6;
then (p`^n).(len (p`^n)-'1) <> 0.L by A5,A3,Lm2;
then
A6: (p`^n).(len (p`^n)-'1) * p.(len p -'1) <> 0.L by A4,VECTSP_2:def 1;
len(p`^(n+1)) = len((p`^n)*'p) by Th19
.= n*len p - n + 1 + len p - 1 by A5,A6,POLYNOM4:10
.= (n+1)*len p - (n+1) + 1;
hence P[n+1];
end;
len(p`^0) = len(1_.(L)) by Th15
.= 0*len p-0+1 by POLYNOM4:4;
then
A7: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A7,A2);
end;
definition
let L be non empty multMagma;
let p be sequence of L;
let v be Element of L;
func v*p -> sequence of L means
:Def4:
for n be Element of NAT holds it.n = v*p.n;
existence
proof
deffunc F(Element of NAT) = v*p.$1;
consider r be sequence of L such that
A1: for n be Element of NAT holds r.n = F(n) from FUNCT_2:sch 4;
take r;
thus thesis by A1;
end;
uniqueness
proof
let p1,p2 be sequence of L such that
A2: for n be Element of NAT holds p1.n = v*p.n and
A3: for n be Element of NAT holds p2.n = v*p.n;
now
let k be Element of NAT;
thus p1.k = v*p.k by A2
.= p2.k by A3;
end;
hence p1 = p2 by FUNCT_2:63;
end;
end;
registration
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let p be Polynomial of L;
let v be Element of L;
cluster v*p -> finite-Support;
coherence
proof
take s = len p;
let i be Nat;
assume
A1: i >= s;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
thus (v*p).i = v*p.ii by Def4
.= v*0.L by A1,ALGSEQ_1:8
.= 0.L;
end;
end;
theorem Th24:
for L be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr for p be Polynomial of L holds len (0.L*
p) = 0
proof
let L be add-associative right_zeroed right_complementable distributive non
empty doubleLoopStr;
let p be Polynomial of L;
0 is_at_least_length_of (0.L*p)
proof
let i be Nat;
assume i>=0;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
thus (0.L*p).i = 0.L*p.ii by Def4
.= 0.L;
end;
hence thesis by ALGSEQ_1:def 3;
end;
theorem Th25:
for L be add-associative right_zeroed right_complementable
well-unital commutative associative distributive almost_left_invertible non
empty doubleLoopStr for p be Polynomial of L for v be Element of L st v <> 0.L
holds len (v*p) = len p
proof
let L be add-associative right_zeroed right_complementable well-unital
commutative associative distributive almost_left_invertible non empty
doubleLoopStr;
let p be Polynomial of L;
let v be Element of L;
assume
A1: v <> 0.L;
A2: now
let n be Nat;
assume
A3: n is_at_least_length_of v*p;
n is_at_least_length_of p
proof
let i be Nat;
reconsider i1=i as Element of NAT by ORDINAL1:def 12;
assume i >= n;
then (v*p).i = 0.L by A3;
then v*p.i1 = 0.L by Def4;
hence thesis by A1,VECTSP_1:12;
end;
hence len p <= n by ALGSEQ_1:def 3;
end;
len p is_at_least_length_of (v*p)
proof
let i be Nat;
assume
A4: i >= len p;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
thus (v*p).i = v*p.ii by Def4
.= v*0.L by A4,ALGSEQ_1:8
.= 0.L;
end;
hence thesis by A2,ALGSEQ_1:def 3;
end;
theorem Th26:
for L be add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr for p be sequence of L holds 0.L*p
= 0_.(L)
proof
let L be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr;
let p be sequence of L;
for n being Element of NAT holds (0_.(L)).n = 0.L*p.n by FUNCOP_1:7;
hence thesis by Def4;
end;
theorem Th27:
for L be well-unital non empty multLoopStr for p be sequence
of L holds 1.L*p = p
proof
let L be well-unital non empty multLoopStr;
let p be sequence of L;
for n be Element of NAT holds p.n = 1.L*p.n;
hence thesis by Def4;
end;
theorem Th28:
for L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr for v be Element of L holds v*0_.(
L) = 0_.(L)
proof
let L be add-associative right_zeroed right_complementable
right-distributive non empty doubleLoopStr;
let v be Element of L;
now
let n be Element of NAT;
thus (0_.(L)).n = 0.L by FUNCOP_1:7
.= v*0.L
.= v*(0_.(L)).n by FUNCOP_1:7;
end;
hence thesis by Def4;
end;
theorem Th29:
for L be add-associative right_zeroed right_complementable
well-unital right-distributive non empty doubleLoopStr for v be Element of L
holds v*1_.(L) = <%v%>
proof
let L be add-associative right_zeroed right_complementable well-unital
right-distributive non empty doubleLoopStr;
let v be Element of L;
now
let n be Element of NAT;
per cases;
suppose
A1: n=0;
hence <%v%>.n = v by ALGSEQ_1:def 5
.= v*1.L
.= v*(1_.(L)).n by A1,POLYNOM3:30;
end;
suppose
A2: n<>0;
A3: len <%v%> <= 1 by ALGSEQ_1:def 5;
n >= 0+1 by A2,NAT_1:13;
hence <%v%>.n = 0.L by A3,ALGSEQ_1:8,XXREAL_0:2
.= v*0.L
.= v*(1_.(L)).n by A2,POLYNOM3:30;
end;
end;
hence thesis by Def4;
end;
theorem Th30:
for L be add-associative right_zeroed right_complementable
well-unital distributive commutative associative almost_left_invertible non
empty doubleLoopStr for p be Polynomial of L for v,x be Element of L holds
eval(v*p,x) = v*eval(p,x)
proof
let L be add-associative right_zeroed right_complementable well-unital
distributive commutative associative almost_left_invertible non empty
doubleLoopStr;
let p be Polynomial of L;
let v,x be Element of L;
consider F1 be FinSequence of the carrier of L such that
A1: eval(p,x) = Sum F1 and
A2: len F1 = len p and
A3: for n be Element of NAT st n in dom F1 holds F1.n = p.(n-'1) * (
power L).(x,n-'1) by POLYNOM4:def 2;
consider F2 be FinSequence of the carrier of L such that
A4: eval(v*p,x) = Sum F2 and
A5: len F2 = len (v*p) and
A6: for n be Element of NAT st n in dom F2 holds F2.n = (v*p).(n-'1) * (
power L).(x,n-'1) by POLYNOM4:def 2;
per cases;
suppose
v <> 0.L;
then len F1 = len F2 by A2,A5,Th25;
then
A7: dom F1 = dom F2 by FINSEQ_3:29;
now
let i be object;
assume
A8: i in dom F1;
then reconsider i1=i as Element of NAT;
A9: p.(i1-'1) * (power L).(x,i1-'1) = F1.i by A3,A8
.= F1/.i by A8,PARTFUN1:def 6;
thus F2/.i = F2.i by A7,A8,PARTFUN1:def 6
.= (v*p).(i1-'1) * (power L).(x,i1-'1) by A6,A7,A8
.= v*p.(i1-'1) * (power L).(x,i1-'1) by Def4
.= v*(F1/.i) by A9,GROUP_1:def 3;
end;
then F2 = v*F1 by A7,POLYNOM1:def 1;
hence thesis by A1,A4,POLYNOM1:12;
end;
suppose
A10: v = 0.L;
hence eval(v*p,x) = eval(0_.(L),x) by Th26
.= 0.L by POLYNOM4:17
.= v*eval(p,x) by A10;
end;
end;
theorem Th31:
for L be add-associative right_zeroed right_complementable
right-distributive unital non empty doubleLoopStr for p be Polynomial of L
holds eval(p,0.L) = p.0
proof
let L be add-associative right_zeroed right_complementable
right-distributive unital non empty doubleLoopStr;
let p be Polynomial of L;
consider F be FinSequence of the carrier of L such that
A1: eval(p,0.L) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds F.n = p.(n-'1) * (power
L).(0.L,n-'1) by POLYNOM4:def 2;
per cases;
suppose
len F > 0;
then 0+1 <= len F by NAT_1:13;
then
A4: 1 in dom F by FINSEQ_3:25;
now
let i be Element of NAT;
assume that
A5: i in dom F and
A6: i <> 1;
0+1 <= i by A5,FINSEQ_3:25;
then i > 0+1 by A6,XXREAL_0:1;
then i-1 > 0 by XREAL_1:20;
then
A7: i-'1 > 0 by XREAL_0:def 2;
thus F/.i = F.i by A5,PARTFUN1:def 6
.= p.(i-'1) * (power L).(0.L,i-'1) by A3,A5
.= p.(i-'1) * 0.L by A7,VECTSP_1:36
.= 0.L;
end;
hence eval(p,0.L) = F/.1 by A1,A4,POLYNOM2:3
.= F.1 by A4,PARTFUN1:def 6
.= p.(1-'1) * (power L).(0.L,1-'1) by A3,A4
.= p.(1-'1) * (power L).(0.L,0) by XREAL_1:232
.= p.(1-'1) * 1_L by GROUP_1:def 7
.= p.(1-'1) by GROUP_1:def 4
.= p.0 by XREAL_1:232;
end;
suppose
len F = 0;
then
A8: p = 0_.(L) by A2,POLYNOM4:5;
hence eval(p,0.L) = 0.L by POLYNOM4:17
.= p.0 by A8,FUNCOP_1:7;
end;
end;
definition
let L be non empty ZeroStr;
let z0,z1 be Element of L;
func <%z0,z1%> -> sequence of L equals
0_.(L)+*(0,z0)+*(1,z1);
coherence;
end;
theorem Th32:
for L be non empty ZeroStr for z0 be Element of L holds <%z0%>.0
= z0 & for n be Element of NAT st n >= 1 holds <%z0%>.n = 0.L
proof
let L be non empty ZeroStr;
let z0 be Element of L;
thus <%z0%>.0 = z0 by ALGSEQ_1:def 5;
let n be Element of NAT;
A1: len <%z0%> <= 1 by ALGSEQ_1:def 5;
assume n >= 1;
hence thesis by A1,ALGSEQ_1:8,XXREAL_0:2;
end;
theorem Th33:
for L be non empty ZeroStr for z0 be Element of L st z0 <> 0.L
holds len <%z0%> = 1
proof
let L be non empty ZeroStr;
let z0 be Element of L;
assume z0 <> 0.L;
then <%z0%>.0 <> 0.L by ALGSEQ_1:def 5;
then <%z0%> <> <%0.L%> by ALGSEQ_1:def 5;
then len <%z0%> <> 0 by ALGSEQ_1:14;
then
A1: len <%z0%> >= 0+1 by NAT_1:13;
assume len <%z0%> <> 1;
then len <%z0%> > 1 by A1,XXREAL_0:1;
hence contradiction by ALGSEQ_1:def 5;
end;
theorem Th34:
for L be non empty ZeroStr holds <%0.L%> = 0_.(L)
proof
let L be non empty ZeroStr;
len <%0.L%> = 0 by ALGSEQ_1:14;
hence thesis by POLYNOM4:5;
end;
theorem Th35:
for L be add-associative right_zeroed right_complementable
distributive commutative associative well-unital domRing-like non empty
doubleLoopStr for x,y be Element of L holds <%x%>*'<%y%> = <%x*y%>
proof
let L be add-associative right_zeroed right_complementable distributive
commutative associative well-unital domRing-like non empty doubleLoopStr;
let x,y be Element of L;
A1: len <%x%> <= 1 by ALGSEQ_1:def 5;
A2: len <%y%> <= 1 by ALGSEQ_1:def 5;
per cases;
suppose
A3: len <%x%> <> 0 & len <%y%> <> 0;
x <> 0.L & y <> 0.L
proof
assume x = 0.L or y = 0.L;
then <%x%> = 0_.(L) or <%y%> = 0_.(L) by Th34;
hence contradiction by A3,POLYNOM4:3;
end;
then x*y <> 0.L by VECTSP_2:def 1;
then
A4: len <%x*y%> = 1 by Th33;
consider r be FinSequence of the carrier of L such that
A5: len r = 0+1 and
A6: (<%x%>*'<%y%>).0 = Sum r and
A7: for k be Element of NAT st k in dom r holds r.k = <%x%>.(k-'1) *
<%y%>.(0+1-'k) by POLYNOM3:def 9;
1 in dom r by A5,FINSEQ_3:25;
then r.1 = <%x%>.(1-'1) * <%y%>.(0+1-'1) by A7
.= <%x%>.0 * <%y%>.(1-'1) by XREAL_1:232
.= <%x%>.0 * <%y%>.0 by XREAL_1:232
.= <%x%>.0 * y by ALGSEQ_1:def 5
.= x*y by ALGSEQ_1:def 5;
then
A8: r = <*x*y*> by A5,FINSEQ_1:40;
A9: now
let n be Nat;
assume n < 1;
then n < 0+1;
then
A10: n = 0 by NAT_1:13;
hence (<%x%>*'<%y%>).n = x*y by A6,A8,RLVECT_1:44
.= <%x*y%>.n by A10,ALGSEQ_1:def 5;
end;
<%x%>.(len <%x%> -'1) <> 0.L & <%y%>.(len <%y%> -'1) <> 0.L by A3,Lm2;
then
A11: <%x%>.(len <%x%> -'1)*<%y%>.(len <%y%> -'1)<>0.L by VECTSP_2:def 1;
len <%y%> >= 0+1 by A3,NAT_1:13;
then
A12: len <%y%> = 1 by A2,XXREAL_0:1;
len <%x%> >= 0+1 by A3,NAT_1:13;
then len <%x%> = 1 by A1,XXREAL_0:1;
then len (<%x%>*'<%y%>) = 1+1-1 by A12,A11,POLYNOM4:10;
hence thesis by A9,A4,ALGSEQ_1:12;
end;
suppose
A13: len <%x%> = 0;
then
A14: x=0.L by Th33;
<%x%> = 0_.(L) by A13,POLYNOM4:5;
hence <%x%>*'<%y%> = 0_.(L) by POLYNOM4:2
.= <%0.L%> by Th34
.= <%x*y%> by A14;
end;
suppose
A15: len <%y%> = 0;
then
A16: y=0.L by Th33;
<%y%> = 0_.(L) by A15,POLYNOM4:5;
hence <%x%>*'<%y%> = 0_.(L) by POLYNOM3:34
.= <%0.L%> by Th34
.= <%x*y%> by A16;
end;
end;
theorem Th36:
for L be Abelian add-associative right_zeroed
right_complementable well-unital associative commutative distributive
almost_left_invertible non empty doubleLoopStr for x be Element of L
for n be Nat holds <%x%>`^n = <%power(x,n)%>
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let x be Element of L;
defpred P[Nat] means <%x%>`^$1 = <%power(x,$1)%>;
A1: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume <%x%>`^n = <%power(x,n)%>;
hence <%x%>`^(n+1) = <%(power L).(x,n)%>*'<%x%> by Th19
.= <%(power L).(x,n)*x%> by Th35
.= <%power(x,n+1)%> by GROUP_1:def 7;
end;
<%x%>`^0 = 1_.(L) by Th15
.= 1.L*1_.(L) by Th27
.= <%1_L%> by Th29
.= <%(power L).(x,0)%> by GROUP_1:def 7;
then
A2: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A2,A1);
end;
theorem
for L be add-associative right_zeroed right_complementable unital non
empty doubleLoopStr for z0,x be Element of L holds eval(<%z0%>,x) = z0
proof
let L be add-associative right_zeroed right_complementable unital non empty
doubleLoopStr;
let z0,x be Element of L;
consider F be FinSequence of the carrier of L such that
A1: eval(<%z0%>,x) = Sum F and
A2: len F = len <%z0%> and
A3: for n be Element of NAT st n in dom F holds F.n = <%z0%>.(n-'1) * (
power L).(x,n-'1) by POLYNOM4:def 2;
A4: len F <= 1 by A2,ALGSEQ_1:def 5;
per cases by A4,NAT_1:25;
suppose
len F = 0;
then
A5: <%z0%> = 0_.(L) by A2,POLYNOM4:5;
hence eval(<%z0%>,x) = 0.L by POLYNOM4:17
.= (0_.(L)).0 by FUNCOP_1:7
.= z0 by A5,Th32;
end;
suppose
A6: len F = 1;
then 0+1 in Seg len F by FINSEQ_1:4;
then 1 in dom F by FINSEQ_1:def 3;
then F.1 = <%z0%>.(1-'1) * (power L).(x,1-'1) by A3
.= <%z0%>.0 * (power L).(x,1-'1) by XREAL_1:232
.= <%z0%>.0 * (power L).(x,0) by XREAL_1:232
.= z0 * (power L).(x,0) by Th32
.= z0 * 1_L by GROUP_1:def 7
.= z0 by GROUP_1:def 4;
then F = <*z0*> by A6,FINSEQ_1:40;
hence thesis by A1,RLVECT_1:44;
end;
end;
theorem Th38:
for L be non empty ZeroStr for z0,z1 be Element of L holds <%z0,
z1%>.0 = z0 & <%z0,z1%>.1 = z1 & for n be Nat st n >= 2 holds <%z0,z1%>.n = 0.L
proof
let L be non empty ZeroStr;
let z0,z1 be Element of L;
0 in NAT;
then
A1: 0 in dom 0_.(L) by FUNCT_2:def 1;
thus <%z0,z1%>.0 = (0_.(L)+*(0,z0)).0 by FUNCT_7:32
.= z0 by A1,FUNCT_7:31;
1 in NAT;
then 1 in dom (0_.(L)+*(0,z0)) by FUNCT_2:def 1;
hence <%z0,z1%>.1 = z1 by FUNCT_7:31;
let n be Nat;
A2: n in NAT by ORDINAL1:def 12;
assume
A3: n >= 2;
then n >= 1+1;
then n > 0+1 by NAT_1:13;
hence <%z0,z1%>.n = (0_.(L)+*(0,z0)).n by FUNCT_7:32
.= (0_.(L)).n by A3,FUNCT_7:32
.= 0.L by A2,FUNCOP_1:7;
end;
registration
let L be non empty ZeroStr;
let z0,z1 be Element of L;
cluster <%z0,z1%> -> finite-Support;
coherence
proof
take 2;
let n be Nat;
thus thesis by Th38;
end;
end;
theorem Th39:
for L be non empty ZeroStr for z0,z1 be Element of L holds len <%z0,z1%> <= 2
proof
let L be non empty ZeroStr;
let z0,z1 be Element of L;
2 is_at_least_length_of <%z0,z1%>
by Th38;
hence thesis by ALGSEQ_1:def 3;
end;
theorem Th40:
for L be non empty ZeroStr for z0,z1 be Element of L st z1 <> 0.
L holds len <%z0,z1%> = 2
proof
let L be non empty ZeroStr;
let z0,z1 be Element of L;
assume z1 <> 0.L;
then <%z0,z1%>.1 <> 0.L by Th38;
then
A1: for n be Nat st n is_at_least_length_of <%z0,z1%> holds 1+1 <= n
by NAT_1:13;
2 is_at_least_length_of <%z0,z1%> by Th38;
hence thesis by A1,ALGSEQ_1:def 3;
end;
theorem Th41:
for L be non empty ZeroStr for z0 be Element of L st z0 <> 0.L
holds len <%z0,0.L%> = 1
proof
let L be non empty ZeroStr;
let z0 be Element of L;
A1: 1 is_at_least_length_of <%z0,0.L%>
proof
let n be Nat;
assume
A2: n >= 1;
per cases by A2,XXREAL_0:1;
suppose
n = 1;
hence thesis by Th38;
end;
suppose
n > 1;
then n >= 1+1 by NAT_1:13;
hence thesis by Th38;
end;
end;
assume z0 <> 0.L;
then <%z0,0.L%>.0 <> 0.L by Th38;
then for n be Nat st n is_at_least_length_of <%z0,0.L%> holds 0+1 <= n
by NAT_1:13;
hence thesis by A1,ALGSEQ_1:def 3;
end;
theorem Th42:
for L be non empty ZeroStr holds <%0.L,0.L%> = 0_.(L)
proof
let L be non empty ZeroStr;
0 is_at_least_length_of <%0.L,0.L%>
proof
let n be Nat;
assume n >= 0;
per cases;
suppose
n = 0;
hence thesis by Th38;
end;
suppose
n > 0;
then
A1: n >= 0+1 by NAT_1:13;
now
per cases by A1,XXREAL_0:1;
suppose
n = 1;
hence thesis by Th38;
end;
suppose
n > 1;
then n >= 1+1 by NAT_1:13;
hence thesis by Th38;
end;
end;
hence thesis;
end;
end;
then len <%0.L,0.L%> = 0 by ALGSEQ_1:def 3;
hence thesis by POLYNOM4:5;
end;
theorem
for L be non empty ZeroStr for z0 be Element of L holds <%z0,0.L%> = <%z0%>
proof
let L be non empty ZeroStr;
let z0 be Element of L;
per cases;
suppose
A1: z0 = 0.L;
hence <%z0,0.L%> = 0_.(L) by Th42
.= <%z0%> by A1,Th34;
end;
suppose
A2: z0 <> 0.L;
then
A3: len <%z0%> = 0+1 by Th33;
A4: now
let n be Nat;
assume n < len <%z0%>;
then
A5: n = 0 by A3,NAT_1:13;
hence <%z0,0.L%>.n = z0 by Th38
.= <%z0%>.n by A5,ALGSEQ_1:def 5;
end;
len <%z0,0.L%> = 1 by A2,Th41;
hence thesis by A2,A4,Th33,ALGSEQ_1:12;
end;
end;
theorem Th44:
for L be add-associative right_zeroed right_complementable
left-distributive unital non empty doubleLoopStr for z0,z1,x be Element of L
holds eval(<%z0,z1%>,x) = z0+z1*x
proof
let L be add-associative right_zeroed right_complementable left-distributive
unital non empty doubleLoopStr;
let z0,z1,x be Element of L;
consider F be FinSequence of the carrier of L such that
A1: eval(<%z0,z1%>,x) = Sum F and
A2: len F = len <%z0,z1%> and
A3: for n be Element of NAT st n in dom F holds F.n = <%z0,z1%>.(n-'1) *
(power L).(x,n-'1) by POLYNOM4:def 2;
len F <= 2 by A2,Th39;
then len F = 0 or ... or len F = 2;
then per cases;
suppose
len F = 0;
then
A4: <%z0,z1%> = 0_.(L) by A2,POLYNOM4:5;
hence eval(<%z0,z1%>,x) = 0.L by POLYNOM4:17
.= (0_.(L)).0 by FUNCOP_1:7
.= z0 by A4,Th38
.= z0 + 0.L by RLVECT_1:def 4
.= z0 + 0.L*x
.= z0 + (0_.(L)).1*x by FUNCOP_1:7
.= z0 + z1*x by A4,Th38;
end;
suppose
A5: len F = 1;
then 0+1 in Seg len F by FINSEQ_1:4;
then 1 in dom F by FINSEQ_1:def 3;
then F.1 = <%z0,z1%>.(1-'1) * (power L).(x,1-'1) by A3
.= <%z0,z1%>.0 * (power L).(x,1-'1) by XREAL_1:232
.= <%z0,z1%>.0 * (power L).(x,0) by XREAL_1:232
.= z0 * (power L).(x,0) by Th38
.= z0 * 1_L by GROUP_1:def 7
.= z0 by GROUP_1:def 4;
then F = <*z0*> by A5,FINSEQ_1:40;
hence eval(<%z0,z1%>,x) = z0 by A1,RLVECT_1:44
.= z0 + 0.L by RLVECT_1:def 4
.= z0 + 0.L*x
.= z0 + <%z0,z1%>.1*x by A2,A5,ALGSEQ_1:8
.= z0 + z1*x by Th38;
end;
suppose
A6: len F = 2;
then 1 in dom F by FINSEQ_3:25;
then
A7: F.1 = <%z0,z1%>.(1-'1) * (power L).(x,1-'1) by A3
.= <%z0,z1%>.0 * (power L).(x,1-'1) by XREAL_1:232
.= <%z0,z1%>.0 * (power L).(x,0) by XREAL_1:232
.= z0 * (power L).(x,0) by Th38
.= z0 * 1_L by GROUP_1:def 7
.= z0 by GROUP_1:def 4;
A8: 2-'1 = 2-1 by XREAL_0:def 2;
2 in dom F by A6,FINSEQ_3:25;
then F.2 = <%z0,z1%>.(2-'1) * (power L).(x,2-'1) by A3
.= z1 * (power L).(x,1) by A8,Th38
.= z1 * x by GROUP_1:50;
then F = <*z0,z1*x*> by A6,A7,FINSEQ_1:44;
hence thesis by A1,RLVECT_1:45;
end;
end;
theorem
for L be add-associative right_zeroed right_complementable
left-distributive well-unital non empty doubleLoopStr for z0,z1,x be Element
of L holds eval(<%z0,0.L%>,x) = z0
proof
let L be add-associative right_zeroed right_complementable left-distributive
well-unital non empty doubleLoopStr;
let z0,z1,x be Element of L;
thus eval(<%z0,0.L%>,x) = z0+0.L*x by Th44
.= z0+0.L
.= z0 by RLVECT_1:def 4;
end;
theorem
for L be add-associative right_zeroed right_complementable
left-distributive unital non empty doubleLoopStr for z0,z1,x be Element of L
holds eval(<%0.L,z1%>,x) = z1*x
proof
let L be add-associative right_zeroed right_complementable left-distributive
unital non empty doubleLoopStr;
let z0,z1,x be Element of L;
thus eval(<%0.L,z1%>,x) = 0.L+z1*x by Th44
.= z1*x by RLVECT_1:4;
end;
theorem Th47:
for L be add-associative right_zeroed right_complementable
left-distributive well-unital non empty doubleLoopStr for z0,z1,x be Element
of L holds eval(<%z0,1.L%>,x) = z0+x
proof
let L be add-associative right_zeroed right_complementable left-distributive
well-unital non empty doubleLoopStr;
let z0,z1,x be Element of L;
thus eval(<%z0,1.L%>,x) = z0+1.L*x by Th44
.= z0+x;
end;
theorem
for L be add-associative right_zeroed right_complementable
left-distributive well-unital non empty doubleLoopStr for z0,z1,x be Element
of L holds eval(<%0.L,1.L%>,x) = x
proof
let L be add-associative right_zeroed right_complementable left-distributive
well-unital non empty doubleLoopStr;
let z0,z1,x be Element of L;
thus eval(<%0.L,1.L%>,x) = 0.L+1.L*x by Th44
.= 0.L+x
.= x by RLVECT_1:4;
end;
begin :: Substitution in Polynomials
definition
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let p,q be Polynomial of L;
func Subst(p,q) -> Polynomial of L means
:Def6:
ex F be FinSequence of the
carrier of Polynom-Ring L st it = Sum F & len F = len p & for n be Element of
NAT st n in dom F holds F.n = p.(n-'1)*(q`^(n-'1));
existence
proof
defpred P[Nat,set] means $2 = p.($1-'1)*(q`^($1-'1));
set k = len p;
A1: now
let n be Nat;
assume n in Seg k;
reconsider x = p.(n-'1)*(q`^(n-'1)) as Element of Polynom-Ring L by
POLYNOM3:def 10;
take x;
thus P[n,x];
end;
consider F being FinSequence of the carrier of Polynom-Ring L such that
A2: dom F = Seg k & for n be Nat st n in Seg k holds P[n,F.n] from
FINSEQ_1:sch 5(A1);
reconsider r=Sum F as Polynomial of L by POLYNOM3:def 10;
take r,F;
thus thesis by A2,FINSEQ_1:def 3;
end;
uniqueness
proof
let y1,y2 be Polynomial of L;
given F1 be FinSequence of the carrier of Polynom-Ring L such that
A3: y1 = Sum F1 and
A4: len F1 = len p and
A5: for n be Element of NAT st n in dom F1 holds F1.n = p.(n-'1)*(q`^( n-'1));
given F2 be FinSequence of the carrier of Polynom-Ring L such that
A6: y2 = Sum F2 and
A7: len F2 = len p and
A8: for n be Element of NAT st n in dom F2 holds F2.n = p.(n-'1)*(q`^( n-'1));
A9: dom F1 = Seg len F1 by FINSEQ_1:def 3;
now
let n be Nat;
assume
A10: n in dom F1;
then
A11: n in dom F2 by A4,A7,A9,FINSEQ_1:def 3;
thus F1.n = p.(n-'1)*(q`^(n-'1)) by A5,A10
.= F2.n by A8,A11;
end;
hence y1 = y2 by A3,A4,A6,A7,FINSEQ_2:9;
end;
end;
theorem Th49:
for L be Abelian add-associative right_zeroed
right_complementable well-unital commutative distributive non empty
doubleLoopStr for p be Polynomial of L holds Subst(0_.(L),p) = 0_.(L)
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
consider F be FinSequence of the carrier of Polynom-Ring L such that
A1: Subst(0_.(L),p) = Sum F and
len F = len (0_.(L)) and
A2: for n be Element of NAT st n in dom F holds F.n = (0_.(L)).(n-'1)*(p
`^(n-'1)) by Def6;
now
let n be Element of NAT;
assume n in dom F;
hence F.n = (0_.(L)).(n-'1)*(p`^(n-'1)) by A2
.= 0.L*(p`^(n-'1)) by FUNCOP_1:7
.= 0_.(L) by Th26
.= 0.(Polynom-Ring L) by POLYNOM3:def 10;
end;
hence Subst(0_.(L),p) = 0.(Polynom-Ring L) by A1,POLYNOM3:1
.= 0_.(L) by POLYNOM3:def 10;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr for p be
Polynomial of L holds Subst(p,0_.(L)) = <%p.0%>
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr;
let p be Polynomial of L;
consider F be FinSequence of the carrier of Polynom-Ring L such that
A1: Subst(p,0_.(L)) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds F.n = p.(n-'1)*((0_.(L))
`^(n-'1)) by Def6;
per cases;
suppose
len F <> 0;
then 0+1 <= len F by NAT_1:13;
then
A4: 1 in dom F by FINSEQ_3:25;
now
let n be Element of NAT;
assume that
A5: n in dom F and
A6: n <> 1;
n >= 1 by A5,FINSEQ_3:25;
then
A7: n > 0+1 by A6,XXREAL_0:1;
then n >= 1+1 by NAT_1:13;
then
A8: n-2 >= 1+1-2 by XREAL_1:9;
n-1 >= 0 by A7;
then
A9: n-'1 = n-(1+1)+1 by XREAL_0:def 2
.= n-'2+1 by A8,XREAL_0:def 2;
thus F/.n = F.n by A5,PARTFUN1:def 6
.= p.(n-'1)*((0_.(L))`^(n-'1)) by A3,A5
.= p.(n-'1)*(0_.(L)) by A9,Th20
.= 0_.(L) by Th28
.= 0.(Polynom-Ring L) by POLYNOM3:def 10;
end;
hence Subst(p,0_.(L)) = F/.1 by A1,A4,POLYNOM2:3
.= F.1 by A4,PARTFUN1:def 6
.= p.(1-'1)*((0_.(L))`^(1-'1)) by A3,A4
.= p.(1-'1)*((0_.(L))`^0) by XREAL_1:232
.= p.0*((0_.(L))`^0) by XREAL_1:232
.= p.0*(1_.(L)) by Th15
.= <%p.0%> by Th29;
end;
suppose
len F = 0;
then
A10: p = 0_.(L) by A2,POLYNOM4:5;
hence Subst(p,0_.(L)) = 0_.(L) by Th49
.= <%0.L%> by Th34
.= <%p.0%> by A10,FUNCOP_1:7;
end;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr for p be Polynomial of L for x be Element of L holds len
Subst(p,<%x%>) <= 1
proof
let L be Abelian add-associative right_zeroed right_complementable
well-unital associative commutative distributive almost_left_invertible non
empty doubleLoopStr;
let p be Polynomial of L;
let x be Element of L;
now
now
consider F be FinSequence of the carrier of Polynom-Ring L such that
A1: Subst(p,<%x%>) = Sum F and
len F = len p and
A2: for n be Element of NAT st n in dom F holds F.n = p.(n-'1)*(<%x
%>`^(n-'1)) by Def6;
defpred P[Nat] means for p be Polynomial of L st p = Sum(F|$1) holds len
p <= 1;
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
reconsider F1 = Sum(F|n) as Polynomial of L by POLYNOM3:def 10;
reconsider maxFq = max(len F1,len (p.nn*(<%x%>`^n)))
as Element of NAT
by ORDINAL1:def 12;
A4: len (p.nn*(<%x%>`^n)) <= 1
proof
per cases;
suppose
p.n <> 0.L;
then len (p.nn*(<%x%>`^n)) = len (<%x%>`^n) by Th25
.= len <%power(x,n)%> by Th36;
hence thesis by ALGSEQ_1:def 5;
end;
suppose
p.n = 0.L;
hence thesis by Th24;
end;
end;
assume
A5: for q be Polynomial of L st q = Sum(F|n) holds len q <= 1;
then len F1 <= 1;
then
A6: maxFq <= 1 by A4,XXREAL_0:28;
let q be Polynomial of L;
assume
A7: q = Sum(F|(n+1));
A8: maxFq >= len F1 & maxFq >= len (p.nn*(<%x%>`^n)) by XXREAL_0:25;
now
per cases;
suppose
A9: n+1 <= len F;
n+1 >= 1 by NAT_1:11;
then
A10: n+1 in dom F by A9,FINSEQ_3:25;
then
A11: F/.(n+1) = F.(n+1) by PARTFUN1:def 6
.= p.(n+1-'1)*(<%x%>`^(n+1-'1)) by A2,A10
.= p.nn*(<%x%>`^(n+1-'1)) by NAT_D:34
.= p.nn*(<%x%>`^n) by NAT_D:34;
F|(n+1) = F|n ^ <*F/.(n+1)*> by A9,FINSEQ_5:82;
then q = Sum(F|n) + F/.(n+1) by A7,FVSUM_1:71
.= F1 + p.nn*(<%x%>`^n) by A11,POLYNOM3:def 10;
then len q <= maxFq by A8,POLYNOM4:6;
hence thesis by A6,XXREAL_0:2;
end;
suppose
A12: n+1 > len F;
then n >= len F by NAT_1:13;
then
A13: F|n = F by FINSEQ_1:58;
F|(n+1) = F by A12,FINSEQ_1:58;
hence thesis by A5,A7,A13;
end;
end;
hence thesis;
end;
A14: F|(len F) = F by FINSEQ_1:58;
A15: P[0]
proof
let p be Polynomial of L;
A16: F|0 = <*>the carrier of Polynom-Ring L;
assume p = Sum(F|0);
then p = 0.(Polynom-Ring L) by A16,RLVECT_1:43
.= 0_.(L) by POLYNOM3:def 10;
hence thesis by POLYNOM4:3;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A15,A3);
hence thesis by A1,A14;
end;
hence thesis;
end;
hence thesis;
end;
theorem Th52:
for L be Field for p,q be Polynomial of L st len p <> 0 & len q
> 1 holds len Subst(p,q) = (len p)*(len q)-len p-len q+2
proof
let L be Field;
let p,q be Polynomial of L;
assume that
A1: len p <> 0 and
A2: len q > 1;
consider F be FinSequence of the carrier of Polynom-Ring L such that
A3: Subst(p,q) = Sum F and
A4: len F = len p and
A5: for n be Element of NAT st n in dom F holds F.n = p.(n-'1)*(q`^(n-'1
)) by Def6;
A6: 0+1 <= len F by A1,A4,NAT_1:13;
then
A7: 1 in dom F by FINSEQ_3:25;
reconsider k = len p * len q - len p - len q + 1 as Element of NAT by A1,A2
,Th1,INT_1:3;
len p >= 0+1 by A1,NAT_1:13;
then
A8: len p-1 >=0;
A9: len (q`^(len F-'1)) = (len p-'1)*len q - (len p-'1) + 1 by A2,A4,Th23
.= (len p-'1)*len q-(len p-1)+1 by A8,XREAL_0:def 2
.= (len p-1)*len q-(len p-1)+1 by A8,XREAL_0:def 2
.= (len p)*(len q)-len p-len q+(1+1);
A10: len Subst(p,q) >= (len p)*(len q)-len p-len q+(1+1)
proof
set lF1 = len F-'1;
set F1 = F|lF1;
reconsider sF1 = Sum F1 as Polynomial of L by POLYNOM3:def 10;
A11: len F = lF1+1 by A6,XREAL_1:235;
then
A12: F = F1^<*F/.len F*> by FINSEQ_5:21;
then
A13: Sum F = Sum F1 + F/.len F by FVSUM_1:71;
A14: len F = len F1 + 1 by A12,FINSEQ_2:16;
assume
A15: len Subst(p,q) < (len p)*(len q)-len p-len q+(1+1);
then len Subst(p,q) < k+1;
then len Subst(p,q) <= k by NAT_1:13;
then
A16: Subst(p,q).k = 0.L by ALGSEQ_1:8;
now
per cases;
suppose
A17: len F1 <> {};
defpred P[Nat] means for F2 be Polynomial of L st F2 = Sum(F1|$1)
holds len F2 <= $1*len q-len q-$1+2;
A18: F1|(len F1) = F1 by FINSEQ_1:58;
A19: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A20: for F2 be Polynomial of L st F2 = Sum(F1|n) holds len F2 <=
n*len q-len q-n+2;
len q >= 0+(1+1) by A2,NAT_1:13;
then len q-2 >= 0 by XREAL_1:19;
then n*len q-n+1+0 <= n*len q-n+1+(len q-2) by XREAL_1:7;
then
n*len q-len q-n+2+0 <= n*len q-len q-n+2+1 & n*len q-n+1-(len q
-2) <= n*len q-n+1 by XREAL_1:6,20;
then
A21: n*len q-len q-n+2 <= n*len q-n+1 by XXREAL_0:2;
reconsider F3 = Sum(F1|n) as Polynomial of L by POLYNOM3:def 10;
let F2 be Polynomial of L;
assume
A22: F2 = Sum(F1|(n+1));
len F3 <= n*len q-len q-n+2 by A20;
then
A23: len F3 <= n*len q-n+1 by A21,XXREAL_0:2;
now
per cases;
suppose
A24: n+1 <= len F1;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A25: n+1 >= 1 by NAT_1:11;
reconsider maxFq = max(len F3,len (p.nn*(q`^nn))) as Element of
NAT by ORDINAL1:def 12;
A26: maxFq >= len F3 & maxFq >= len (p.nn*(q`^nn)) by XXREAL_0:25;
len (p.nn*(q`^nn)) <= n*len q-n+1
proof
per cases;
suppose
p.n <> 0.L;
then len (p.nn*(q`^nn)) = len (q`^nn) by Th25;
hence thesis by A2,Th23;
end;
suppose
A27: p.n = 0.L;
len q >= 0+1 by A2;
then len q-1 >= 0;
then
A28: n*(len q-1) >= 0;
n*len q <= n*len q+1 by NAT_1:11;
then n*len q-n <= n*len q+1-n by XREAL_1:9;
hence thesis by A27,A28,Th24;
end;
end;
then
A29: maxFq <= n*len q-n+1 by A23,XXREAL_0:28;
len F1 <= len F by A14,NAT_1:11;
then n+1 <= len F by A24,XXREAL_0:2;
then
A30: n+1 in dom F by A25,FINSEQ_3:25;
A31: n+1 in dom F1 by A24,A25,FINSEQ_3:25;
then
A32: F1/.(n+1) = F1.(n+1) by PARTFUN1:def 6
.= F.(n+1) by A12,A31,FINSEQ_1:def 7
.= p.(n+1-'1)*(q`^(n+1-'1)) by A5,A30
.= p.nn*(q`^(n+1-'1)) by NAT_D:34
.= p.nn*(q`^nn) by NAT_D:34;
F1|(nn+1) = F1|nn ^ <*F1/.(nn+1)*> by A24,FINSEQ_5:82;
then F2 = Sum(F1|n) + F1/.(n+1) by A22,FVSUM_1:71
.= F3 + p.nn*(q`^nn) by A32,POLYNOM3:def 10;
then len F2 <= maxFq by A26,POLYNOM4:6;
hence len F2 <= (n+1)*len q-len q-(n+1)+2 by A29,XXREAL_0:2;
end;
suppose
A33: n+1 > len F1;
-len q <= -1 by A2,XREAL_1:24;
then n*len q-n+-len q <= n*len q-n+-1 by XREAL_1:6;
then
A34: n*len q-len q-n+2 <= (n+1)*len q-len q-(n+1)+2 by XREAL_1:6;
n >= len F1 by A33,NAT_1:13;
then
A35: F1|n = F1 by FINSEQ_1:58;
F1|(n+1) = F1 by A33,FINSEQ_1:58;
then len F2 <= n*len q-len q-n+2 by A20,A22,A35;
hence len F2 <= (n+1)*len q-len q-(n+1)+2 by A34,XXREAL_0:2;
end;
end;
hence len F2 <= (n+1)*len q-len q-(n+1)+2;
end;
0+len q >= 1+1 by A2,NAT_1:13;
then 2-len q <= 0 by XREAL_1:20;
then
A36: 2-len q+k <= 0+k by XREAL_1:6;
0+1 <= len F1 by A17,NAT_1:13;
then
A37: 1 in dom F1 by FINSEQ_3:25;
A38: P[1]
proof
let F2 be Polynomial of L;
Z: F1.1 = F1/.1 by A37,PARTFUN1:def 6;
F1|1 = <*F1.1*> by A17,CARD_1:27,FINSEQ_5:20;
then
A39: Sum(F1|1) = F1.1 by Z,RLVECT_1:44
.= F.1 by A12,A37,FINSEQ_1:def 7
.= p.(1-'1)*(q`^(1-'1)) by A5,A7
.= p.0*(q`^(1-'1)) by XREAL_1:232
.= p.0*(q`^0) by XREAL_1:232
.= p.0*(1_.(L)) by Th15
.= <%p.0%> by Th29;
assume F2 = Sum(F1|1);
hence len F2 <= 1*len q-len q-1+2 by A39,ALGSEQ_1:def 5;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A38,A19);
then len sF1 <= (len F1)*(len q)-len q-len F1+2 by A17,A18;
then
A40: sF1.k = 0.L by A4,A14,A36,ALGSEQ_1:8,XXREAL_0:2;
A41: len F in dom F by A6,FINSEQ_3:25;
then F/.len F = F.len F by PARTFUN1:def 6
.= p.lF1*(q`^lF1) by A5,A41;
then Subst(p,q) = sF1 + p.lF1*(q`^lF1) by A3,A13,POLYNOM3:def 10;
then
A42: Subst(p,q).k = sF1.k + (p.lF1*(q`^lF1)).k by NORMSP_1:def 2
.= (p.lF1*(q`^lF1)).k by A40,RLVECT_1:def 4
.= p.lF1*((q`^lF1).k) by Def4;
len (q`^lF1) = k+1 by A9;
then
A43: (q`^lF1).k <> 0.L by ALGSEQ_1:10;
p.lF1 <> 0.L by A4,A11,ALGSEQ_1:10;
hence contradiction by A16,A42,A43,VECTSP_1:12;
end;
suppose
A44: len F1 = {};
A45: F/.1 = F.1 by A7,PARTFUN1:def 6
.= p.(1-'1)*(q`^(1-'1)) by A5,A7
.= p.0*(q`^(1-'1)) by XREAL_1:232
.= p.0*(q`^0) by XREAL_1:232
.= p.0*(1_.(L)) by Th15
.= <%p.0%> by Th29;
A46: 0.(Polynom-Ring L) = 0_.(L) by POLYNOM3:def 10;
A47: len F = 0+1 by A12,A44,FINSEQ_2:16;
then
A48: p.0 <> 0.L by A4,ALGSEQ_1:10;
F1 = <*>(the carrier of Polynom-Ring L) by A44;
then Sum F = 0.(Polynom-Ring L) + F/.1 by A13,A47,RLVECT_1:43
.= 0_.(L) + <%p.0%> by A45,A46,POLYNOM3:def 10
.= <%p.0%> by POLYNOM3:28;
hence contradiction by A3,A4,A15,A47,A48,Th33;
end;
end;
hence contradiction;
end;
defpred P[Nat] means for F1 be Polynomial of L st F1 = Sum(F|$1) holds len
F1 <= len (q`^($1-'1));
A49: for n be non zero Nat st P[n] holds P[n+1]
proof
let n be non zero Nat;
assume
A50: for F1 be Polynomial of L st F1 = Sum(F|n) holds len F1 <= len (q
`^(n-'1));
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider F2 = Sum(F|n) as Polynomial of L by POLYNOM3:def 10;
let F1 be Polynomial of L;
assume
A51: F1 = Sum(F|(n+1));
n*len q+(len q-'1) >= n*len q by NAT_1:11;
then
A52: n*len q-(len q-'1) <= n*len q by XREAL_1:20;
len q >= 0+1 by A2;
then len q-1 >=0;
then n*len q-(len q-1) <= n*len q by A52,XREAL_0:def 2;
then n*len q-len q+1-n <= n*len q-n by XREAL_1:9;
then
A53: n*len q-len q-n+1+1 <= n*len q-n+1 by XREAL_1:6;
len(q`^(n-'1)) = (n-'1)*len q-(n-'1)+1 by A2,Th23
.= (n-1)*len q-(n-'1)+1 by XREAL_0:def 2
.= n*len q-1*len q-(n-1)+1 by XREAL_0:def 2
.= n*len q-len q-n+1+1;
then
A54: len (q`^(n-'1)) <= len (q`^nn) by A2,A53,Th23;
per cases;
suppose
A55: n+1 <= len F;
reconsider maxFq = max(len F2,len (p.nn*(q`^nn))) as Element of NAT by
ORDINAL1:def 12;
p.n <> 0.L or p.n = 0.L;
then
A56: len (p.nn*(q`^nn)) <= len (q`^nn)by Th24,Th25;
len F2 <= len (q`^(n-'1)) by A50;
then len F2 <= len (q`^nn) by A54,XXREAL_0:2;
then
A57: maxFq <= len (q`^nn) by A56,XXREAL_0:28;
F|(n+1) = F|n ^ <*F/.(nn+1)*> by A55,FINSEQ_5:82;
then
A58: F1 = Sum(F|n) + F/.(n+1) by A51,FVSUM_1:71;
n+1 >= 1 by NAT_1:11;
then
A59: n+1 in dom F by A55,FINSEQ_3:25;
then F/.(n+1) = F.(n+1) by PARTFUN1:def 6
.= p.(n+1-'1)*(q`^(n+1-'1)) by A5,A59
.= p.nn*(q`^(n+1-'1)) by NAT_D:34
.= p.nn*(q`^nn) by NAT_D:34;
then
A60: F1 = F2 + p.nn*(q`^nn) by A58,POLYNOM3:def 10;
maxFq >= len F2 & maxFq >= len (p.nn*(q`^nn)) by XXREAL_0:25;
then len F1 <= maxFq by A60,POLYNOM4:6;
then len F1 <= len (q`^nn) by A57,XXREAL_0:2;
hence thesis by NAT_D:34;
end;
suppose
A61: n+1 > len F;
then n >= len F by NAT_1:13;
then
A62: F|n = F by FINSEQ_1:58;
F|(n+1) = F by A61,FINSEQ_1:58;
then len F1 <= len (q`^(n-'1)) by A50,A51,A62;
then len F1 <= len (q`^nn) by A54,XXREAL_0:2;
hence thesis by NAT_D:34;
end;
end;
A63: F|len F = F by FINSEQ_1:58;
A64: P[1]
proof
let F1 be Polynomial of L;
Z: F.1 = F/.1 by A7,PARTFUN1:def 6;
F|1 = <*F.1*> by A1,A4,CARD_1:27,FINSEQ_5:20;
::: .= <*F/.1*>;
then
A65: Sum(F|1) = F.1 by Z,RLVECT_1:44
.= p.(1-'1)*(q`^(1-'1)) by A5,A7
.= p.0*(q`^(1-'1)) by XREAL_1:232
.= p.0*(q`^0) by XREAL_1:232
.= p.0*(1_.(L)) by Th15
.= <%p.0%> by Th29;
assume F1 = Sum(F|1);
then len F1 <= 1 by A65,ALGSEQ_1:def 5;
then len F1 <= len (1_.(L)) by POLYNOM4:4;
then len F1 <= len (q`^0) by Th15;
hence thesis by XREAL_1:232;
end;
for n be non zero Nat holds P[n] from NAT_1:sch 10(A64,A49);
then len Subst(p,q) <= len (q`^(len F-'1)) by A1,A3,A4,A63;
hence thesis by A9,A10,XXREAL_0:1;
end;
theorem Th53:
for L be Field for p,q be Polynomial of L for x be Element of L
holds eval(Subst(p,q),x) = eval(p,eval(q,x))
proof
let L be Field;
let p,q be Polynomial of L;
let x be Element of L;
consider F1 be FinSequence of the carrier of L such that
A1: eval(p,eval(q,x)) = Sum F1 and
A2: len F1 = len p and
A3: for n be Element of NAT st n in dom F1 holds F1.n = p.(n-'1)*(power
L).(eval(q,x),n-'1) by POLYNOM4:def 2;
consider F be FinSequence of the carrier of Polynom-Ring L such that
A4: Subst(p,q) = Sum F and
A5: len F = len p and
A6: for n be Element of NAT st n in dom F holds F.n = p.(n-'1)*(q`^(n-'1
)) by Def6;
defpred P[Nat] means for r be Polynomial of L st r = Sum(F|$1)
holds eval(r,x) = Sum(F1|$1);
A7: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
assume
A8: for r be Polynomial of L st r = Sum(F|n) holds eval(r,x) = Sum(F1 |n);
let r be Polynomial of L;
assume
A9: r = Sum(F|(n+1));
per cases;
suppose
A10: n+1 <= len F;
then
A11: F1|(n+1) = F1|n ^ <*F1/.(n+1)*> by A5,A2,FINSEQ_5:82;
F|(n+1) = F|n ^ <*F/.(n+1)*> by A10,FINSEQ_5:82;
then
A12: r = Sum(F|n) + F/.(n+1) by A9,FVSUM_1:71;
reconsider r1 = Sum(F|n) as Polynomial of L by POLYNOM3:def 10;
n+1 >= 1 by NAT_1:11;
then
A13: n+1 in dom F by A10,FINSEQ_3:25;
A14: dom F = dom F1 by A5,A2,FINSEQ_3:29;
then
A15: p.(n+1-'1)*(power L).(eval(q,x),n+1-'1) = F1.(n+1) by A3,A13
.= F1/.(n+1) by A13,A14,PARTFUN1:def 6;
F/.(n+1) = F.(n+1) by A13,PARTFUN1:def 6
.= p.(n+1-'1)*(q`^(n+1-'1)) by A6,A13
.= p.nn*(q`^(n+1-'1)) by NAT_D:34
.= p.nn*(q`^n) by NAT_D:34;
then r = r1 + p.nn*(q`^n) by A12,POLYNOM3:def 10;
hence eval(r,x) = eval(r1,x) + eval(p.nn*(q`^n),x) by POLYNOM4:19
.= Sum(F1|n) + eval(p.nn*(q`^n),x) by A8
.= Sum(F1|n) + p.nn*eval(q`^n,x) by Th30
.= Sum(F1|n) + p.nn*(power L).(eval(q,x),n) by Th22
.= Sum(F1|n) + p.(n+1-'1)*(power L).(eval(q,x),n) by NAT_D:34
.= Sum(F1|n) + F1/.(n+1) by A15,NAT_D:34
.= Sum(F1|(n+1)) by A11,FVSUM_1:71;
end;
suppose
A16: n+1 > len F;
then n >= len F by NAT_1:13;
then
A17: F|n = F & F1|n = F1 by A5,A2,FINSEQ_1:58;
F|(n+1) = F & F1|(n+1) = F1 by A5,A2,A16,FINSEQ_1:58;
hence thesis by A8,A9,A17;
end;
end;
A18: F|(len F) = F & F1|(len F1) = F1 by FINSEQ_1:58;
A19: P[0]
proof
let r be Polynomial of L;
A20: F|0 = <*>the carrier of Polynom-Ring L;
A21: F1|0 = <*>the carrier of L;
assume r = Sum(F|0);
then r = 0.(Polynom-Ring L) by A20,RLVECT_1:43
.= 0_.(L) by POLYNOM3:def 10;
hence eval(r,x) = 0.L by POLYNOM4:17
.= Sum(F1|0) by A21,RLVECT_1:43;
end;
for n be Nat holds P[n] from NAT_1:sch 2(A19,A7);
hence thesis by A4,A5,A1,A2,A18;
end;
begin :: Fundamental Theorem of Algebra
definition
let L be unital non empty doubleLoopStr;
let p be Polynomial of L;
let x be Element of L;
pred x is_a_root_of p means
eval(p,x) = 0.L;
end;
definition
let L be unital non empty doubleLoopStr;
let p be Polynomial of L;
attr p is with_roots means
ex x be Element of L st x is_a_root_of p;
end;
theorem Th54:
for L be unital non empty doubleLoopStr holds 0_.(L) is with_roots
proof
let L be unital non empty doubleLoopStr;
set x = the Element of L;
take x;
thus eval(0_.(L),x) = 0.L by POLYNOM4:17;
end;
registration
let L be unital non empty doubleLoopStr;
cluster 0_.(L) -> with_roots;
coherence by Th54;
end;
theorem
for L be unital non empty doubleLoopStr for x be Element of L holds
x is_a_root_of 0_.(L)
by POLYNOM4:17;
registration
let L be unital non empty doubleLoopStr;
cluster with_roots for Polynomial of L;
existence
proof
take 0_.(L);
thus thesis;
end;
end;
definition
let L be unital non empty doubleLoopStr;
attr L is algebraic-closed means
for p be Polynomial of L st len p > 1 holds p is with_roots;
end;
definition
let L be unital non empty doubleLoopStr;
let p be Polynomial of L;
func Roots(p) -> Subset of L means
:Def10:
for x be Element of L holds x in it iff x is_a_root_of p;
existence
proof
{ x where x is Element of L : x is_a_root_of p } c= the carrier of L
proof
let y be object;
assume y in {x where x is Element of L : x is_a_root_of p};
then ex x be Element of L st x = y & x is_a_root_of p;
hence thesis;
end;
then reconsider
X = { x where x is Element of L : x is_a_root_of p } as Subset
of L;
take X;
let x be Element of L;
thus x in X implies x is_a_root_of p
proof
assume x in X;
then ex y be Element of L st x = y & y is_a_root_of p;
hence thesis;
end;
assume x is_a_root_of p;
hence thesis;
end;
uniqueness
proof
let X1,X2 be Subset of L such that
A1: for x be Element of L holds x in X1 iff x is_a_root_of p and
A2: for x be Element of L holds x in X2 iff x is_a_root_of p;
thus X1 c= X2
by A1,A2;
let x be object;
assume
A3: x in X2;
then reconsider y=x as Element of L;
y is_a_root_of p by A2,A3;
hence thesis by A1;
end;
end;
definition
let L be commutative associative well-unital distributive
almost_left_invertible non empty doubleLoopStr;
let p be Polynomial of L;
func NormPolynomial(p) -> sequence of L means
:Def11:
for n be Element of NAT holds it.n = p.n / p.(len p-'1);
existence
proof
deffunc F(Element of NAT) = p.$1 / p.(len p-'1);
consider q be sequence of L such that
A1: for n be Element of NAT holds q.n = F(n) from FUNCT_2:sch 4;
take q;
thus thesis by A1;
end;
uniqueness
proof
let p1,p2 be sequence of L such that
A2: for n be Element of NAT holds p1.n = p.n / p.(len p-'1) and
A3: for n be Element of NAT holds p2.n = p.n / p.(len p-'1);
now
let n be Element of NAT;
thus p1.n = p.n / p.(len p-'1) by A2
.= p2.n by A3;
end;
hence p1 = p2 by FUNCT_2:63;
end;
end;
registration
let L be add-associative right_zeroed right_complementable commutative
associative well-unital distributive almost_left_invertible non empty
doubleLoopStr;
let p be Polynomial of L;
cluster NormPolynomial(p) -> finite-Support;
coherence
proof
now
let n be Nat;
assume
A1: n >= len p;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
thus (NormPolynomial(p)).n = p.nn / p.(len p-'1) by Def11
.= 0.L / p.(len p-'1) by A1,ALGSEQ_1:8
.= 0.L * (p.(len p-'1))"
.= 0.L;
end;
hence thesis;
end;
end;
theorem Th56:
for L be commutative associative well-unital distributive
almost_left_invertible non empty doubleLoopStr for p be Polynomial of L st
len p <> 0 holds (NormPolynomial p).(len p-'1) = 1.L
proof
let L be commutative associative well-unital distributive
almost_left_invertible non empty doubleLoopStr;
let p be Polynomial of L;
assume len p <> 0;
then len p >= 0+1 by NAT_1:13;
then len p = len p-'1+1 by XREAL_1:235;
then
A1: p.(len p-'1) <> 0.L by ALGSEQ_1:10;
thus (NormPolynomial p).(len p-'1) = p.(len p-'1) / p.(len p-'1) by Def11
.= p.(len p-'1) * (p.(len p-'1))"
.= 1.L by A1,VECTSP_1:def 10;
end;
theorem Th57:
for L be Field for p be Polynomial of L st len p <> 0 holds len
NormPolynomial(p) = len p
proof
let L be Field;
let p be Polynomial of L;
assume len p <> 0;
then len p >= 0+1 by NAT_1:13;
then len p = len p-'1+1 by XREAL_1:235;
then p.(len p-'1) <> 0.L by ALGSEQ_1:10;
then
A1: (p.(len p-'1))" <> 0.L by VECTSP_1:25;
A2: now
let n be Nat;
assume
A3: n is_at_least_length_of NormPolynomial(p);
n is_at_least_length_of p
proof
let i be Nat;
reconsider ii = i as Element of NAT by ORDINAL1:def 12;
assume i >= n;
then (NormPolynomial(p)).i = 0.L by A3;
then p.ii / p.(len p-'1) = 0.L by Def11;
then p.ii * (p.(len p-'1))" = 0.L;
hence thesis by A1,VECTSP_1:12;
end;
hence len p <= n by ALGSEQ_1:def 3;
end;
len p is_at_least_length_of NormPolynomial(p)
proof
let n be Nat;
assume
A4: n >= len p;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
thus (NormPolynomial(p)).n = p.nn / p.(len p-'1) by Def11
.= 0.L / p.(len p-'1) by A4,ALGSEQ_1:8
.= 0.L * (p.(len p-'1))"
.= 0.L;
end;
hence thesis by A2,ALGSEQ_1:def 3;
end;
theorem Th58:
for L be Field for p be Polynomial of L st len p <> 0 for x be
Element of L holds eval(NormPolynomial(p),x) = eval(p,x)/p.(len p-'1)
proof
let L be Field;
let p be Polynomial of L;
assume
A1: len p <> 0;
set NPp = NormPolynomial(p);
let x be Element of L;
consider F1 be FinSequence of the carrier of L such that
A2: eval(p,x) = Sum F1 and
A3: len F1 = len p and
A4: for n be Element of NAT st n in dom F1 holds F1.n = p.(n-'1) * (
power L).(x,n-'1) by POLYNOM4:def 2;
consider F2 be FinSequence of the carrier of L such that
A5: eval(NPp,x) = Sum F2 and
A6: len F2 = len NPp and
A7: for n be Element of NAT st n in dom F2 holds F2.n = NPp.(n-'1) * (
power L).(x,n-'1) by POLYNOM4:def 2;
len F1 = len F2 by A1,A3,A6,Th57;
then
A8: dom F1 = dom F2 by FINSEQ_3:29;
now
let i be object;
assume
A9: i in dom F1;
then reconsider i1=i as Element of NAT;
A10: p.(i1-'1) * (power L).(x,i1-'1) = F1.i by A4,A9
.= F1/.i by A9,PARTFUN1:def 6;
thus F2/.i = F2.i by A8,A9,PARTFUN1:def 6
.= NPp.(i1-'1) * (power L).(x,i1-'1) by A7,A8,A9
.= p.(i1-'1) / p.(len p-'1) * (power L).(x,i1-'1) by Def11
.= p.(i1-'1) * (p.(len p-'1))" * (power L).(x,i1-'1)
.= (F1/.i)*(p.(len p-'1))" by A10,GROUP_1:def 3;
end;
then F2 = F1*(p.(len p-'1))" by A8,POLYNOM1:def 2;
then eval(NormPolynomial(p),x) = eval(p,x) * (p.(len p-'1))" by A2,A5,
POLYNOM1:13;
hence thesis;
end;
theorem Th59:
for L be Field for p be Polynomial of L st len p <> 0 for x be
Element of L holds x is_a_root_of p iff x is_a_root_of NormPolynomial(p)
proof
let L be Field;
let p be Polynomial of L;
assume
A1: len p <> 0;
then len p >= 0+1 by NAT_1:13;
then len p = len p-'1+1 by XREAL_1:235;
then p.(len p-'1) <> 0.L by ALGSEQ_1:10;
then
A2: (p.(len p-'1))" <> 0.L by VECTSP_1:25;
let x be Element of L;
thus x is_a_root_of p implies x is_a_root_of NormPolynomial(p)
proof
assume x is_a_root_of p;
then eval(p,x) = 0.L;
then eval(NormPolynomial(p),x) = 0.L/p.(len p-'1) by A1,Th58
.= 0.L * (p.(len p-'1))"
.= 0.L;
hence thesis;
end;
assume x is_a_root_of NormPolynomial(p);
then 0.L = eval(NormPolynomial(p),x)
.= eval(p,x)/p.(len p-'1) by A1,Th58
.= eval(p,x) * (p.(len p-'1))";
then eval(p,x) = 0.L by A2,VECTSP_1:12;
hence thesis;
end;
theorem Th60:
for L be Field for p be Polynomial of L st len p <> 0 holds p is
with_roots iff NormPolynomial(p) is with_roots
proof
let L be Field;
let p be Polynomial of L;
assume
A1: len p <> 0;
thus p is with_roots implies NormPolynomial(p) is with_roots
proof
assume p is with_roots;
then consider x be Element of L such that
A2: x is_a_root_of p;
x is_a_root_of NormPolynomial(p) by A1,A2,Th59;
hence thesis;
end;
assume NormPolynomial(p) is with_roots;
then consider x be Element of L such that
A3: x is_a_root_of NormPolynomial(p);
x is_a_root_of p by A1,A3,Th59;
hence thesis;
end;
theorem
for L be Field for p be Polynomial of L st len p <> 0 holds Roots(p) =
Roots(NormPolynomial p)
proof
let L be Field;
let p be Polynomial of L;
assume
A1: len p <> 0;
thus Roots(p) c= Roots(NormPolynomial p)
proof
let x be object;
assume
A2: x in Roots(p);
then reconsider x1=x as Element of L;
x1 is_a_root_of p by A2,Def10;
then x1 is_a_root_of NormPolynomial p by A1,Th59;
hence thesis by Def10;
end;
thus Roots(NormPolynomial p) c= Roots(p)
proof
let x be object;
assume
A3: x in Roots(NormPolynomial p);
then reconsider x1=x as Element of L;
x1 is_a_root_of NormPolynomial p by A3,Def10;
then x1 is_a_root_of p by A1,Th59;
hence thesis by Def10;
end;
end;
theorem Th62:
id(COMPLEX) is_continuous_on COMPLEX
proof
A1: now
let x be Complex;
let r be Real;
assume that
x in COMPLEX and
A2: 0 < r;
take s=r;
thus 0 < s by A2;
let y be Complex;
assume that
y in COMPLEX and
A3: |.y-x.| < s;
reconsider xx=x, yy=y as Element of COMPLEX by XCMPLX_0:def 2;
|.id(COMPLEX)/.yy - id(COMPLEX)/.xx.| < r by A3;
hence |.id(COMPLEX)/.y - id(COMPLEX)/.x.| < r;
end;
dom id(COMPLEX) = COMPLEX by FUNCT_2:def 1;
hence thesis by A1,CFCONT_1:39;
end;
theorem Th63:
for x be Element of COMPLEX holds COMPLEX --> x is_continuous_on COMPLEX
proof
let x be Element of COMPLEX;
A1: now
let x1 be Complex;
let r be Real;
assume that
A2: x1 in COMPLEX and
A3: 0 < r;
take s=r;
thus 0 < s by A3;
let x2 be Complex;
assume that
A4: x2 in COMPLEX and
|.x2-x1.| < s;
reconsider xx1=x1, xx2=x2 as Element of COMPLEX by A2,A4;
(COMPLEX --> x)/.xx1 = x & (COMPLEX --> x)/.xx2 = x by FUNCOP_1:7;
hence |.(COMPLEX --> x)/.x2 - (COMPLEX --> x)/.x1 .| < r by A3,COMPLEX1:44;
end;
dom (COMPLEX --> x) = COMPLEX by FUNCOP_1:13;
hence thesis by A1,CFCONT_1:39;
end;
definition
let L be unital non empty multMagma;
let x be Element of L;
let n be Nat;
func FPower(x,n) -> Function of L,L means
:Def12:
for y be Element of L holds it.y = x*power(y,n);
existence
proof
deffunc F(Element of L) = x*power($1,n);
consider f be Function of the carrier of L,the carrier of L such that
A1: for y be Element of L holds f.y = F(y) from FUNCT_2:sch 4;
reconsider f as Function of L,L;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of L,L such that
A2: for y be Element of L holds f1.y=x*power(y,n) and
A3: for y be Element of L holds f2.y=x*power(y,n);
now
let y be Element of L;
thus f1.y = x*power(y,n) by A2
.= f2.y by A3;
end;
hence f1 = f2 by FUNCT_2:63;
end;
end;
theorem
for L be unital non empty multMagma holds
FPower(1_L,1) = id the carrier of L
proof
let L be unital non empty multMagma;
A1: now
let x be object;
assume x in the carrier of L;
then reconsider x1=x as Element of L;
FPower(1_L,1).x1 = 1_L*power(x1,1) by Def12
.= (power L).(x1,1) by GROUP_1:def 4;
hence FPower(1_L,1).x = x by GROUP_1:50;
end;
dom FPower(1_L,1) = the carrier of L by FUNCT_2:def 1;
hence thesis by A1,FUNCT_1:17;
end;
theorem
FPower(1_F_Complex,2) = id(COMPLEX)(#)id(COMPLEX)
proof
the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider
f=id(COMPLEX)(#)id(COMPLEX) as Function of F_Complex,F_Complex;
now
let x be Element of F_Complex;
reconsider x1=x as Element of COMPLEX by COMPLFLD:def 1;
id(COMPLEX)/.x1 = x1 & dom (id(COMPLEX)(#)id(COMPLEX)) = COMPLEX by
FUNCT_2:def 1;
hence f.x = x*x by VALUED_1:def 4
.= (power F_Complex).(x,2) by GROUP_1:51
.= 1_F_Complex*power(x,2);
end;
hence thesis by Def12;
end;
theorem Th66:
for L be unital non empty multMagma for x be Element of L
holds FPower(x,0) = (the carrier of L) --> x
proof
let L be unital non empty multMagma;
let x be Element of L;
reconsider f=(the carrier of L) --> x as Function of L,L;
now
let y be Element of L;
thus f.y = x by FUNCOP_1:7
.= x*1_L by GROUP_1:def 4
.= x*power(y,0) by GROUP_1:def 7;
end;
hence thesis by Def12;
end;
theorem
for x be Element of F_Complex
ex x1 be Element of COMPLEX st x = x1 & FPower(x,1) = x1(#)id(COMPLEX)
proof
let x be Element of F_Complex;
reconsider x1=x as Element of COMPLEX by COMPLFLD:def 1;
take x1;
thus x = x1;
the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f=x1(#)id(COMPLEX) as Function of F_Complex,F_Complex;
now
let y be Element of F_Complex;
reconsider y1=y as Element of COMPLEX by COMPLFLD:def 1;
thus f.y = x1*id(COMPLEX).y1 by VALUED_1:6
.= x*y
.= x*power(y,1) by GROUP_1:50;
end;
hence thesis by Def12;
end;
theorem
for x be Element of F_Complex ex x1 be Element of COMPLEX st
x = x1 & FPower(x,2) = x1(#)(id(COMPLEX)(#)id(COMPLEX))
proof
let x be Element of F_Complex;
reconsider x1=x as Element of COMPLEX by COMPLFLD:def 1;
take x1;
thus x = x1;
the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f=x1(#)(id(COMPLEX)(#)id(COMPLEX)) as Function of F_Complex,
F_Complex;
now
let y be Element of F_Complex;
reconsider y1=y as Element of COMPLEX by COMPLFLD:def 1;
thus f.y = x1*(id(COMPLEX)(#)id(COMPLEX)).y1 by VALUED_1:6
.= x1*(id(COMPLEX).y1*id(COMPLEX).y1) by VALUED_1:5
.= x1*(y1*id(COMPLEX).y1)
.= x*(y*y)
.= x*power(y,2) by GROUP_1:51;
end;
hence thesis by Def12;
end;
theorem Th69:
for x be Element of F_Complex for n be Nat
ex f be Function of COMPLEX,COMPLEX
st f = FPower(x,n) & FPower(x,n+1) = f(#)id(COMPLEX)
proof
let x be Element of F_Complex;
let n be Nat;
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f=FPower(x,n) as Function of COMPLEX,COMPLEX;
reconsider g=f(#)id(COMPLEX) as Function of F_Complex,F_Complex by A1;
take f;
thus f = FPower(x,n);
now
let y be Element of F_Complex;
reconsider y1=y as Element of COMPLEX by COMPLFLD:def 1;
thus g.y = f.y1*id(COMPLEX).y1 by VALUED_1:5
.= FPower(x,n).y*y
.= x*power(y,n)*y by Def12
.= x*((power F_Complex).(y,n)*y)
.= x*power(y,n+1) by GROUP_1:def 7;
end;
hence thesis by Def12;
end;
theorem Th70:
for x be Element of F_Complex
for n be Nat ex f be Function of COMPLEX,COMPLEX st
f = FPower(x,n) & f is_continuous_on COMPLEX
proof
let x be Element of F_Complex;
defpred P[Nat] means
ex f be Function of COMPLEX,COMPLEX st f =
FPower(x,$1) & f is_continuous_on COMPLEX;
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
reconsider g=FPower(x,n+1) as Function of COMPLEX,COMPLEX by A1;
given f be Function of COMPLEX,COMPLEX such that
A3: f = FPower(x,n) & f is_continuous_on COMPLEX;
take g;
thus g = FPower(x,n+1);
ex f1 be Function of COMPLEX,COMPLEX st
f1 = FPower(x,n) & FPower(x,n+1) = f1(#)id(COMPLEX) by Th69;
hence thesis by A3,Th62,CFCONT_1:43;
end;
A4: P[0]
proof
reconsider f=FPower(x,0) as Function of COMPLEX,COMPLEX by A1;
take f;
thus f = FPower(x,0);
f = (the carrier of F_Complex) --> x by Th66;
hence thesis by A1,Th63;
end;
thus for n be Nat holds P[n] from NAT_1:sch 2(A4,A2);
end;
definition
let L be well-unital non empty doubleLoopStr;
let p be Polynomial of L;
func Polynomial-Function(L,p) -> Function of L,L means
:Def13:
for x be Element of L holds it.x = eval(p,x);
existence
proof
deffunc F(Element of L) = eval(p,$1);
consider f be Function of the carrier of L,the carrier of L such that
A1: for x be Element of L holds f.x = F(x) from FUNCT_2:sch 4;
reconsider f as Function of L,L;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of L,L such that
A2: for x be Element of L holds f1.x = eval(p,x) and
A3: for x be Element of L holds f2.x = eval(p,x);
now
let x be Element of L;
thus f1.x = eval(p,x) by A2
.= f2.x by A3;
end;
hence f1 = f2 by FUNCT_2:63;
end;
end;
theorem Th71:
for p be Polynomial of F_Complex
ex f be Function of COMPLEX,COMPLEX st
f = Polynomial-Function(F_Complex,p) & f is_continuous_on COMPLEX
proof
set FuFF=Funcs(COMPLEX,COMPLEX);
let p be Polynomial of F_Complex;
reconsider fzero = COMPLEX --> 0c as Element of FuFF by FUNCT_2:9;
defpred P[Nat,set] means $2 = FPower(p.($1-'1),$1-'1);
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f = Polynomial-Function(F_Complex,p) as Function of COMPLEX,
COMPLEX;
deffunc F(Element of FuFF,Element of FuFF) = $1+$2;
take f;
thus f = Polynomial-Function(F_Complex,p);
A2: for x,y being Element of FuFF holds F(x,y) in FuFF by FUNCT_2:8;
consider fadd be BinOp of FuFF such that
A3: for x,y be Element of FuFF holds fadd.(x,y) = F(x,y) from FUNCT_7:
sch 1(A2);
reconsider L=addLoopStr(#FuFF,fadd,fzero#) as non empty addLoopStr;
A4: now
let u,v,w be Element of L;
reconsider u1=u, v1=v, w1=w as Function of COMPLEX,COMPLEX by FUNCT_2:66;
A5: u1+v1 in Funcs(COMPLEX,COMPLEX) by FUNCT_2:9;
A6: v1+w1 in Funcs(COMPLEX,COMPLEX) by FUNCT_2:9;
thus (u+v)+w = fadd.(u1+v1,w) by A3
.= u1+v1+w1 by A3,A5
.= u1+(v1+w1) by CFUNCT_1:13
.= fadd.(u,v1+w1) by A3,A6
.= u+(v+w) by A3;
end;
A7: now
let v be Element of L;
reconsider v1=v as Function of COMPLEX,COMPLEX by FUNCT_2:66;
A8: now
let x be Element of COMPLEX;
thus (v1+fzero).x = v1.x+fzero.x by VALUED_1:1
.= v1.x+0c by FUNCOP_1:7
.= v1.x;
end;
thus v + 0.L = v1+fzero by A3
.= v by A8,FUNCT_2:63;
end;
L is right_complementable
proof
let v be Element of L;
reconsider v1=v as Function of COMPLEX,COMPLEX by FUNCT_2:66;
reconsider w=-v1 as Element of L by FUNCT_2:9;
take w;
A9: now
let x be Element of COMPLEX;
thus (v1+-v1).x = v1.x+(-v1).x by VALUED_1:1
.= v1.x+-v1.x by VALUED_1:8
.= fzero.x by FUNCOP_1:7;
end;
thus v + w = v1+-v1 by A3
.= 0.L by A9,FUNCT_2:63;
end;
then reconsider
L as add-associative right_zeroed right_complementable non empty
addLoopStr by A4,A7,RLVECT_1:def 3,def 4;
A10: now
let n be Nat;
reconsider x = FPower(p.(n-'1),n-'1) as Element of L by A1,FUNCT_2:9;
assume n in Seg len p;
take x;
thus P[n,x];
end;
consider F be FinSequence of the carrier of L such that
A11: dom F = Seg len p and
A12: for n be Nat st n in Seg len p holds P[n,F.n] from FINSEQ_1:sch 5(
A10 );
A13: F|len F = F by FINSEQ_1:58;
reconsider SF = Sum F as Function of COMPLEX,COMPLEX by FUNCT_2:66;
A14: now
let x be Element of COMPLEX;
reconsider x1=x as Element of F_Complex by COMPLFLD:def 1;
consider H be FinSequence of the carrier of F_Complex such that
A15: eval(p,x1) = Sum H and
A16: len H = len p and
A17: for n be Element of NAT st n in dom H holds H.n = p.(n-'1)*(power
F_Complex).(x1,n-'1) by POLYNOM4:def 2;
defpred P[Nat] means
for SFk be Function of COMPLEX,COMPLEX st
SFk = Sum (F|$1) holds Sum (H|$1) = SFk.x;
A18: len F = len p by A11,FINSEQ_1:def 3;
A19: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume
A20: for SFk be Function of COMPLEX,COMPLEX st SFk = Sum (F|k) holds
Sum (H|k) = SFk.x;
reconsider SFk1 = Sum (F|k) as Function of COMPLEX,COMPLEX by FUNCT_2:66;
let SFk be Function of COMPLEX,COMPLEX;
assume
A21: SFk = Sum (F|(k+1));
per cases;
suppose
A22: len F > k;
reconsider g2 = FPower(p.kk,k) as Function of COMPLEX,COMPLEX by A1;
A23: k+1 >= 1 by NAT_1:11;
k+1 <= len F by A22,NAT_1:13;
then
A24: k+1 in dom F by A23,FINSEQ_3:25;
then
A25: F/.(k+1) = F.(k+1) by PARTFUN1:def 6
.= FPower(p.(k+1-'1),k+1-'1) by A11,A12,A24
.= FPower(p.kk,k+1-'1) by NAT_D:34
.= FPower(p.kk,k) by NAT_D:34;
F|(k+1) = F|k ^ <*F.(k+1)*> by A22,FINSEQ_5:83
.= F|k ^ <*F/.(k+1)*> by A24,PARTFUN1:def 6;
then
A26: SFk = Sum(F|k) + F/.(k+1) by A21,FVSUM_1:71
.= SFk1+g2 by A3,A25;
A27: Sum (H|k) = SFk1.x by A20;
A28: dom F = dom H by A11,A16,FINSEQ_1:def 3;
then
A29: H/.(k+1) = H.(k+1) by A24,PARTFUN1:def 6
.= p.(k+1-'1)*(power F_Complex).(x1,k+1-'1) by A17,A28,A24
.= p.kk*(power F_Complex).(x1,k+1-'1) by NAT_D:34
.= p.kk*power(x1,k) by NAT_D:34
.= FPower(p.kk,k).x by Def12;
H|(k+1) = H|k ^ <*H.(k+1)*> by A16,A18,A22,FINSEQ_5:83
.= H|k ^ <*H/.(k+1)*> by A28,A24,PARTFUN1:def 6;
hence Sum (H|(k+1)) = Sum(H|k) + H/.(k+1) by FVSUM_1:71
.= SFk.x by A29,A26,A27,VALUED_1:1;
end;
suppose
A30: len F <= k;
k <= k+1 by NAT_1:11;
then
A31: F|(k+1) = F & H|(k+1) = H by A16,A18,A30,FINSEQ_1:58,XXREAL_0:2;
F|k = F & H|k = H by A16,A18,A30,FINSEQ_1:58;
hence thesis by A20,A21,A31;
end;
end;
A32: P[0]
proof
let SFk be Function of COMPLEX,COMPLEX;
A33: F|0 = <*>the carrier of L;
assume SFk = Sum (F|0);
then
A34: SFk = 0.L by A33,RLVECT_1:43
.= COMPLEX --> 0c;
H|0 = <*>the carrier of F_Complex;
hence Sum (H|0) = 0.F_Complex by RLVECT_1:43
.= SFk.x by A34,COMPLFLD:7,FUNCOP_1:7;
end;
A35: for k be Nat holds P[k] from NAT_1:sch 2(A32,A19);
A36: Sum(F|len F) = SF by FINSEQ_1:58;
thus f.x = Sum H by A15,Def13
.= Sum (H|len H) by FINSEQ_1:58
.= SF.x by A16,A18,A35,A36;
end;
defpred P[Nat] means
for g be PartFunc of COMPLEX,COMPLEX st g =
Sum (F|$1) holds g is_continuous_on COMPLEX;
A37: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
reconsider g1 = Sum (F|k) as Function of COMPLEX,COMPLEX by FUNCT_2:66;
assume
A38: for g be PartFunc of COMPLEX,COMPLEX st g = Sum (F|k) holds g
is_continuous_on COMPLEX;
then
A39: g1 is_continuous_on COMPLEX;
let g be PartFunc of COMPLEX,COMPLEX;
assume
A40: g = Sum (F|(k+1));
per cases;
suppose
A41: len F > k;
A42: k+1 >= 1 by NAT_1:11;
k+1 <= len F by A41,NAT_1:13;
then
A43: k+1 in dom F by A42,FINSEQ_3:25;
then
A44: F/.(k+1) = F.(k+1) by PARTFUN1:def 6
.= FPower(p.(k+1-'1),k+1-'1) by A11,A12,A43
.= FPower(p.kk,k+1-'1) by NAT_D:34
.= FPower(p.kk,k) by NAT_D:34;
consider g2 be Function of COMPLEX,COMPLEX such that
A45: g2 = FPower(p.kk,k) and
A46: g2 is_continuous_on COMPLEX by Th70;
F|(k+1) = F|k ^ <*F.(k+1)*> by A41,FINSEQ_5:83
.= F|k ^ <*F/.(k+1)*> by A43,PARTFUN1:def 6;
then g = Sum(F|k) + F/.(k+1) by A40,FVSUM_1:71
.= g1+g2 by A3,A44,A45;
hence thesis by A39,A46,CFCONT_1:43;
end;
suppose
A47: len F <= k;
k <= k+1 by NAT_1:11;
then F|(k+1) = F by A47,FINSEQ_1:58,XXREAL_0:2
.= F|k by A47,FINSEQ_1:58;
hence thesis by A38,A40;
end;
end;
A48: P[0]
proof
let g be PartFunc of COMPLEX,COMPLEX;
A49: F|0 = <*>the carrier of L;
assume g = Sum(F|0);
then g = 0.L by A49,RLVECT_1:43
.= COMPLEX --> 0c;
hence thesis by Th63;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A48,A37);
hence thesis by A13,A14,FUNCT_2:63;
end;
theorem Th72:
for p be Polynomial of F_Complex st len p > 2 & |.p.(len p-'1).|=1
for F be FinSequence of REAL st len F = len p & for n be Element of NAT st
n in dom F holds F.n = |.p.(n-'1).|
for z be Element of F_Complex st |.z.| > Sum F holds
|.eval(p,z).| >= |.z.| > |.p.0 .|+1
proof
let p be Polynomial of F_Complex;
assume that
A1: len p > 2 and
A2: |.p.(len p-'1).|=1;
let F be FinSequence of REAL;
assume that
A3: len F = len p and
A4: for n be Element of NAT st n in dom F holds F.n = |.p.(n-'1).|;
set lF1 = len F-'1;
A5: lF1+1 = len F by A1,A3,XREAL_1:235,XXREAL_0:2;
then
A6: F = F|(lF1+1) by FINSEQ_1:58
.= F|lF1 ^ <*F/.(lF1+1)*> by A5,FINSEQ_5:82;
A7: len p > 1 by A1,XXREAL_0:2;
then
A8: 1 in dom F by A3,FINSEQ_3:25;
A9: now
let n be Element of NAT;
A10: dom(F|lF1) c= dom F by FINSEQ_5:18;
assume
A11: n in dom (F|lF1);
then (F|lF1).n = (F|lF1)/.n by PARTFUN1:def 6
.= F/.n by A11,FINSEQ_4:70
.= F.n by A11,A10,PARTFUN1:def 6
.= |.p.(n-'1).| by A4,A11,A10;
hence (F|lF1).n >= 0 by COMPLEX1:46;
end;
A12: len (F|lF1) = lF1 by A5,FINSEQ_1:59,NAT_1:11;
|.p.0 .| >= 0 by COMPLEX1:46;
then
A13: |.p.0 .|+1 >= 0+1 by XREAL_1:6;
let z be Element of F_Complex;
consider G be FinSequence of the carrier of F_Complex such that
A14: eval(p,z) = Sum G and
A15: len G = len p and
A16: for n be Element of NAT st n in dom G holds G.n = p.(n-'1)*(power
F_Complex).(z,n-'1) by POLYNOM4:def 2;
set lF2 = len F-'2;
assume
A17: |.z.| > Sum F;
A18: len F in dom F by A7,A3,FINSEQ_3:25;
then F/.(lF1+1) = F.(lF1+1) by A5,PARTFUN1:def 6
.= 1 by A2,A3,A4,A5,A18;
then
A19: Sum F = Sum(F|lF1) + 1 by A6,RVSUM_1:74;
A20: len F >= 1+1+0 by A1,A3;
then lF1 >= 1 by A5,XREAL_1:6;
then
A21: 1 in dom (F|lF1) by A12,FINSEQ_3:25;
then (F|lF1).1 = (F|lF1)/.1 by PARTFUN1:def 6
.= F/.1 by A21,FINSEQ_4:70
.= F.1 by A8,PARTFUN1:def 6
.= |.p.(1-'1).| by A4,A8
.= |.p.0 .| by XREAL_1:232;
then Sum(F|lF1) >= |.p.0 .| by A21,A9,Th4;
then
A22: Sum F >= |.p.0 .|+1 by A19,XREAL_1:6;
then
A23: z <> 0.F_Complex by A17,A13,COMPLFLD:59;
G = G|(lF1+1) by A3,A15,A5,FINSEQ_1:58
.= G|lF1 ^ <*G/.(lF1+1)*> by A3,A15,A5,FINSEQ_5:82;
then
A24: Sum G = Sum(G|lF1) + G/.(lF1+1) by FVSUM_1:71;
A25: dom F = dom G by A3,A15,FINSEQ_3:29;
then G/.(lF1+1) = G.(lF1+1) by A5,A18,PARTFUN1:def 6
.= p.lF1*(power F_Complex).(z,lF1) by A16,A5,A18,A25;
then |.G/.(lF1+1).| = 1*|.(power F_Complex).(z,lF1).| by A2,A3,COMPLFLD:71;
then
A26: |.eval(p,z).| >= |.(power F_Complex).(z,lF1).|- |.Sum(G|lF1).| by A14,A24,
COMPLFLD:64;
A27: len F-1 >= 0 by A7,A3;
A28: len (F|lF1) = lF1 by A5,FINSEQ_1:59,NAT_1:11
.= len (G|lF1) by A3,A15,A5,FINSEQ_1:59,NAT_1:11;
then
A29: F|lF1|(len (F|lF1)) = F|lF1 & G|lF1|(len (F|lF1)) = G|lF1 by FINSEQ_1:58;
defpred P[Nat] means
|.Sum(G|lF1|$1).| <= (Sum (F|lF1|$1))*|.(
power F_Complex).(z,lF2).|;
len F-2 >=0 by A20,XREAL_1:19;
then
A30: lF2+1 = len F-2+1 by XREAL_0:def 2
.= lF1 by A27,XREAL_0:def 2;
then (power F_Complex).(z,lF1) = (power F_Complex).(z,lF2)*z by GROUP_1:def 7
;
then
A31: |.(power F_Complex).(z,lF1).|- |.(power F_Complex).(z,lF2).|*Sum (F|lF1
) = |.(power F_Complex).(z,lF2).|*|.z.|- |.(power F_Complex).(z,lF2).|*Sum (F|
lF1) by COMPLFLD:71
.= |.(power F_Complex).(z,lF2).|*(|.z.|-Sum (F|lF1));
A32: |.z.| > |.p.0 .|+1 by A17,A22,XXREAL_0:2;
then
A33: |.z.| > 1 by A13,XXREAL_0:2;
A34: dom (F|lF1) = dom (G|lF1) by A28,FINSEQ_3:29;
reconsider GG = G|lF1 as FinSequence of the carrier of F_Complex;
reconsider FF = F|lF1 as FinSequence of REAL;
A35: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
assume
A36: |.Sum(G|lF1|n).| <= (Sum (F|lF1|n))*|.(power F_Complex).(z,lF2).|;
then
A37: |.Sum(GG|n).|+|.GG/.(n+1).| <= (Sum (FF|n))*|.(power
F_Complex).(z,lF2).|+|.GG/.(n+1).| by XREAL_1:6;
per cases;
suppose
A38: n+1 <= len (G|lF1);
then n+1 <= lF2+1 by A3,A15,A5,A30,FINSEQ_1:59,NAT_1:11;
then n <= lF2 by XREAL_1:6;
then |.z.| to_power n <= |.z.| to_power lF2 by A33,PRE_FF:8;
then |.z.| to_power n <= |.power(z,lF2).| by A23,Th7;
then
A39: |.p.nn.| >= 0 & |.power(z,n).|<=|.power(z,lF2).|
by A23,Th7,COMPLEX1:46;
GG|(n+1) = GG|n ^ <*GG/.(n+1)*> by A38,FINSEQ_5:82;
then Sum(GG|(n+1)) = Sum(GG|n) + GG/.(n+1) by FVSUM_1:71;
then |.Sum(GG|(n+1)).| <= |.Sum(GG|n).|+|.GG/.(n+1).| by COMPLFLD:62;
then
A40: |.Sum(GG|(n+1)).| <= (Sum (FF|n))*|.(power F_Complex).(z,lF2)
.|+|.GG/.(n+1).| by A37,XXREAL_0:2;
A41: dom GG c= dom G by FINSEQ_5:18;
n+1 >= 1 by NAT_1:11;
then
A42: n+1 in dom GG by A38,FINSEQ_3:25;
then
A43: (F|lF1)/.(n+1) = F/.(n+1) by A34,FINSEQ_4:70
.= F.(n+1) by A25,A42,A41,PARTFUN1:def 6
.= |.p.(n+1-'1).| by A4,A25,A42,A41
.= |.p.nn.| by NAT_D:34;
GG/.(n+1) = G/.(n+1) by A42,FINSEQ_4:70
.= G.(n+1) by A42,A41,PARTFUN1:def 6
.= p.(n+1-'1)*(power F_Complex).(z,n+1-'1) by A16,A42,A41
.= p.nn*(power F_Complex).(z,n+1-'1) by NAT_D:34
.= p.nn*(power F_Complex).(z,n) by NAT_D:34;
then |.GG/.(n+1).| = (F|lF1)/.(n+1)*|.(power F_Complex).(z,n).|
by A43,COMPLFLD:71;
then |.GG/.(n+1).| <= (F|lF1)/.(n+1)*|.(power F_Complex).(z,lF2).|
by A43,A39,XREAL_1:64;
then
A44: (Sum(F|lF1|n))*|.(power F_Complex).(z,lF2).|+|.GG/.(n+1).| <=
(Sum((F|lF1)|n))*|.(power F_Complex).(z,lF2).|+ ((F|lF1)/.(n+1))*|.(power
F_Complex).(z,lF2).| by XREAL_1:6;
(F|lF1)|(n+1) = (F|lF1)|n ^ <*(F|lF1)/.(n+1)*> by A28,A38,FINSEQ_5:82;
then Sum(F|lF1|(n+1)) = Sum ((F|lF1)|n) + (F|lF1)/.(n+1) by RVSUM_1:74;
hence thesis by A40,A44,XXREAL_0:2;
end;
suppose
A45: n+1 > len GG;
then n >= len GG by NAT_1:13;
then
A46: GG|n = GG & (F|lF1)|n = (F|lF1) by A28,FINSEQ_1:58;
GG|(n+1) = GG by A45,FINSEQ_1:58;
hence thesis by A28,A36,A45,A46,FINSEQ_1:58;
end;
end;
G|lF1|0 = <*>the carrier of F_Complex;
then
A47: P[0] by COMPLFLD:57,RLVECT_1:43,RVSUM_1:72;
for n be Nat holds P[n] from NAT_1:sch 2(A47,A35);
then |.Sum(G|lF1).| <= (Sum (F|lF1))*|.(power F_Complex).(z,lF2).| by A29;
then
|.(power F_Complex).(z,lF1).|- |.Sum(G|lF1).| >= |.(power F_Complex).(z
,lF1).|-(Sum (F|lF1))*|.(power F_Complex).(z,lF2).| by XREAL_1:13;
then
A48: |.eval(p,z).| >= |.(power F_Complex).(z,lF1).|- |.(power F_Complex).(z,
lF2).|*Sum (F|lF1) by A26,XXREAL_0:2;
len F >= 2+1 by A1,A3,NAT_1:13;
then len F-2 >= 1 by XREAL_1:19;
then lF2 >= 1 by XREAL_0:def 2;
then |.z.| to_power lF2 >= |.z.| to_power 1 by A33,PRE_FF:8;
then |.power(z,lF2).| >= |.z.| to_power 1 by A23,Th7;
then
|.(power F_Complex).(z,lF2).| >= |.power(z,1).| by A23,Th7;
then
A49: |.(power F_Complex).(z,lF2).| >= |.z.| by GROUP_1:50;
|.(power F_Complex).(z,lF2).| >= 0 & |.z.|-Sum (F|lF1) > 1 by A17,A19,
COMPLEX1:46,XREAL_1:20;
then
|.(power F_Complex).(z,lF2).|*(|.z.|-Sum (F|lF1)) >= |.(power F_Complex
).(z,lF2).|*1 by XREAL_1:64;
then |.eval(p,z).| >= |.(power F_Complex).(z,lF2).| by A48,A31,XXREAL_0:2;
then |.eval(p,z).| >= |.z.| by A49,XXREAL_0:2;
hence thesis by A32;
end;
theorem Th73:
for p be Polynomial of F_Complex st len p > 2
ex z0 be Element of F_Complex st
for z be Element of F_Complex holds |.eval(p,z).| >= |.eval(p,z0).|
proof
defpred P[set] means not contradiction;
let p be Polynomial of F_Complex;
set np = NormPolynomial(p);
deffunc F(Element of F_Complex) = In(|.eval(np,$1).|,REAL);
reconsider D = { F(z) where z is Element of F_Complex : P[z] } as Subset of
REAL from DOMAIN_1:sch 8;
set q = lower_bound D;
A1: D is bounded_below
proof
take 0;
let b be ExtReal;
assume b in D;
then consider z be Element of F_Complex such that
A2: b = In(|.eval(np,z).|,REAL);
b = |.eval(np,z).| by A2;
hence thesis by COMPLEX1:46;
end;
defpred P[Nat,object] means ex g1 be Element of F_Complex st g1 = $2
& |.eval(np,g1).| < q+1/($1+1);
In(|.eval(np,0.F_Complex).|,REAL) = |.eval(np,0.F_Complex).|;
then
A3: |.eval(np,0.F_Complex).| in D;
A4: for n be Nat ex g be Complex st P[n,g]
proof
let n be Nat;
consider r be Real such that
A5: r in D and
A6: r < q+1/(n+1) by A3,A1,SEQ_4:def 2;
consider g1 be Element of F_Complex such that
A7: r = In(|.eval(np,g1).|,REAL) by A5;
reconsider g=g1 as Element of COMPLEX by COMPLFLD:def 1;
take g,g1;
thus g1 = g;
thus thesis by A6,A7;
end;
consider G be Complex_Sequence such that
A8: for n be Nat holds P[n,G.n] from CFCONT_1:sch 1(A4);
deffunc G(Nat) = In(|.np.($1-'1).|,REAL);
consider F be FinSequence of REAL such that
A9: len F = len np and
A10: for n be Nat st n in dom F holds F.n = G(n) from FINSEQ_2:sch 1;
assume
A11: len p > 2;
then
A12: len p = len p-'1+1 by XREAL_1:235,XXREAL_0:2;
then p.(len p-'1) <> 0.F_Complex by ALGSEQ_1:10;
then
A13: |.p.(len p-'1).| > 0 by COMPLFLD:59;
G is bounded
proof
take r = Sum F + 1;
let n be Nat;
consider Gn be Element of F_Complex such that
A14: Gn = G.n and
A15: |.eval(np,Gn).| < q+1/(n+1) by A8;
n+1>=0+1 by XREAL_1:6;
then
A16: 1/(n+1) <= 1 by XREAL_1:211;
A17: len np = len p by A11,Th57;
then
A18: np.(len np-'1) = 1_F_Complex by A11,Th56;
|.G.n.| <= Sum F
proof
A19: eval(np,0.F_Complex) = np.0 by Th31;
In(|.np.0 .|,REAL) = |.np.0 .|;
then |.np.0 .| in D by A19;
then |.np.0 .| >= q by A1,SEQ_4:def 2;
then
A20: |.np.0 .|+1 >= q+1/(n+1) by A16,XREAL_1:7;
A21: for n be Element of NAT st n in dom F holds F.n = |.np.(n-'1).|
proof let n be Element of NAT;
assume n in dom F;
then F.n = G(n) by A10;
hence F.n = |.np.(n-'1).|;
end;
assume |.G.n.| > Sum F;
then |.eval(np,Gn).| >= |.Gn.| > |.np.0 .|+1
by A11,A9,A14,A17,A18,A21,COMPLFLD:60,Th72;
then |.eval(np,Gn).| > |.np.0 .|+1 by XXREAL_0:2;
hence contradiction by A15,A20,XXREAL_0:2;
end;
then |.G.n.|+0 < r by XREAL_1:8;
hence thesis;
end;
then consider G1 be Complex_Sequence such that
A22: G1 is subsequence of G and
A23: G1 is convergent by COMSEQ_3:50;
defpred P[Nat,object] means ex G1n be Element of F_Complex st G1n =
G1.$1 & $2 = eval(np,G1n);
lim G1 in COMPLEX by XCMPLX_0:def 2;
then reconsider z0=lim G1 as Element of F_Complex by COMPLFLD:def 1;
A24: for n be Nat ex g be Complex st P[n,g]
proof
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
reconsider G1n = G1.nn as Element of F_Complex by COMPLFLD:def 1;
reconsider g = eval(np,G1n) as Element of COMPLEX by COMPLFLD:def 1;
take g,G1n;
thus G1n = G1.n;
thus thesis;
end;
consider H be Complex_Sequence such that
A25: for n be Nat holds P[n,H.n] from CFCONT_1:sch 1(A24);
reconsider enp0 = eval(np,z0) as Element of COMPLEX by COMPLFLD:def 1;
consider g be Complex such that
A26: for p be Real st 0 < p
ex n be Nat st for m be Nat st n <= m holds |.G1.m-g.| < p
by A23;
A27: g in COMPLEX by XCMPLX_0:def 2;
then reconsider g1 = g as Element of F_Complex by COMPLFLD:def 1;
reconsider eg = eval(np,g1) as Element of COMPLEX by COMPLFLD:def 1;
now
let p be Real;
consider fPF be Function of COMPLEX,COMPLEX such that
A28: fPF = Polynomial-Function(F_Complex,np) and
A29: fPF is_continuous_on COMPLEX by Th71;
assume 0 < p;
then consider p1 be Real such that
A30: 0 < p1 and
A31: for x1 be Complex st x1 in COMPLEX & |.x1-g.| < p1
holds |.fPF/.x1 - fPF/.g.| < p by A29,CFCONT_1:39,A27;
consider n be Nat such that
A32: for m be Nat st n <= m holds |.G1.m-g.| < p1 by A26,A30;
take n;
let m be Nat;
reconsider mm= m as Element of NAT by ORDINAL1:def 12;
assume n <= m;
then
A33: |.G1.m-g.| < p1 by A32;
ex G1m be Element of F_Complex st G1m = G1.m & H.m = eval(np,G1m) by A25;
then
A34: H.m = fPF/.(G1.mm) by A28,Def13;
eg = fPF/.g by A28,Def13;
hence |.H.m-eg.| < p by A31,A33,A34;
end;
then
A35: H is convergent;
consider PF be Function of COMPLEX,COMPLEX such that
A36: PF = Polynomial-Function(F_Complex,np) and
A37: PF is_continuous_on COMPLEX by Th71;
now
let a be Real;
A38: lim G1 in COMPLEX by XCMPLX_0:def 2;
assume 0 < a;
then consider s be Real such that
A39: 0 < s and
A40: for x1 be Complex st x1 in COMPLEX & |.x1-lim G1.| < s
holds |.PF/.x1 - PF/.lim G1.| < a by A37,CFCONT_1:39,A38;
consider n be Nat such that
A41: for m be Nat st n <= m holds |.G1.m-lim G1.| < s by A23,A39,
COMSEQ_2:def 6;
take n;
let m be Nat;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
assume n <= m;
then
A42: |.G1.m-lim G1.| < s by A41;
ex G1m be Element of F_Complex st G1m = G1.m & H.m = eval(np,G1m) by A25;
then
A43: PF/.(G1.mm) = H.m by A36,Def13;
PF/.lim G1 = eval(np,z0) by A36,Def13;
hence |.H.m - enp0 .| < a by A40,A42,A43;
end;
then
A44: enp0 = lim H by A35,COMSEQ_2:def 6;
deffunc F(Nat) = 1/($1+1);
consider R be Real_Sequence such that
A45: for n be Nat holds R.n = F(n) from SEQ_1:sch 1;
take z0;
let z be Element of F_Complex;
reconsider v = |.eval(np,z).| as Element of REAL by XREAL_0:def 1;
set Rcons = seq_const |.eval(np,z).|;
consider Nseq be increasing sequence of NAT such that
A46: G1 = G*Nseq by A22,VALUED_0:def 17;
In(|.eval(np,z).|,REAL) = |.eval(np,z).|;
then |.eval(np,z).| in D;
then
A47: |.eval(np,z).| >= q by A1,SEQ_4:def 2;
A48: now
let n be Nat;
A49: n in NAT by ORDINAL1:def 12;
consider G1n be Element of F_Complex such that
A50: G1n = G1.n and
A51: H.n = eval(np,G1n) by A25;
consider gNn be Element of F_Complex such that
A52: gNn = G.(Nseq.n) and
A53: |.eval(np,gNn).| < q+1/((Nseq.n)+1) by A8;
Nseq.n >= n by SEQM_3:14;
then Nseq.n+1 >= n+1 by XREAL_1:6;
then 1/(Nseq.n+1) <= 1/(n+1) by XREAL_1:85;
then q+1/(Nseq.n+1) <= q+1/(n+1) by XREAL_1:6;
then |.eval(np,gNn).| < q+1/(n+1) by A53,XXREAL_0:2;
then q > |.eval(np,gNn).|-1/(n+1) by XREAL_1:19;
then
A54: Rcons.n = |.eval(np,z).| & |.eval(np,z).| > |.eval(np,gNn).|-1/(n+1)
by A47,SEQ_1:57,XXREAL_0:2;
dom (|.H.|-R) = NAT by FUNCT_2:def 1;
then (|.H.|-R).n = |.H.|.n-R.n by VALUED_1:13,A49
.= |.H.|.n-1/(n+1) by A45
.= |.eval(np,G1n).|-1/(n+1) by A51,VALUED_1:18;
hence Rcons.n >= (|.H.|-R).n by A46,A50,A52,A54,FUNCT_2:15,A49;
end;
A55: R is convergent by A45,SEQ_4:31;
then |.H.|-R is convergent by A35;
then Rcons.0 = |.eval(np,z).| & lim (|.H.|-R) <= lim Rcons by A48,SEQ_1:57
,SEQ_2:18;
then
A56: lim (|.H.|-R) <= |.eval(np,z).| by SEQ_4:25;
lim (|.H.|-R) = lim |.H.| - lim R by A35,A55,SEQ_2:12
.= |.lim H.| - lim R by A35,SEQ_2:27
.= |.lim H.| - 0 by A45,SEQ_4:31;
then |.eval(p,z)/p.(len p-'1).| >= |.eval(np,z0).| by A11,A56,A44,Th58;
then |.eval(p,z)/p.(len p-'1).| >= |.eval(p,z0)/p.(len p-'1).| by A11,Th58;
then |.eval(p,z).|/|.p.(len p-'1).| >= |.eval(p,z0)/p.(len p-'1).| by A12,
ALGSEQ_1:10,COMPLFLD:73;
then |.eval(p,z).|/|.p.(len p-'1).| >= |.eval(p,z0).|/|.p.(len p-'1).| by A12
,ALGSEQ_1:10,COMPLFLD:73;
hence thesis by A13,XREAL_1:74;
end;
::$N Fundamental Theorem of Algebra
::$L https://en.wikipedia.org/wiki/Fundamental_theorem_of_algebra Fundamental Theorem of Algebra
theorem Th74:
for p be Polynomial of F_Complex st len p > 1 holds p is with_roots
proof
let p be Polynomial of F_Complex;
assume
A1: len p > 1;
then
A2: len p >= 1+1 by NAT_1:13;
per cases by A2,XXREAL_0:1;
suppose
len p > 2;
then consider z0 be Element of F_Complex such that
A3: for z be Element of F_Complex holds |.eval(p,z).| >= |.eval(p,z0)
.| by Th73;
set q = Subst(p,<%z0,1_F_Complex%>);
defpred P[Nat] means $1 >= 1 & q.$1 <> 0.F_Complex;
len <%z0,1_F_Complex%> = 2 by Th40;
then
A4: len q = 2*len p - len p - 2 + 2 by A1,Th52
.= len p;
A5: ex k be Nat st P[k]
proof
len q-1 = len q-'1 by A1,A4,XREAL_0:def 2;
then reconsider k=len q-1 as Element of NAT;
take k;
len q >= 1+1 by A1,A4,NAT_1:13;
hence k >= 1 by XREAL_1:19;
len q = k+1;
hence q.k <> 0.F_Complex by ALGSEQ_1:10;
end;
consider k be Nat such that
A6: P[k] and
A7: for n be Nat st P[n] holds k <= n from NAT_1:sch 5(A5);
A8: k+1 > 1 by A6,NAT_1:13;
reconsider k1=k as non zero Element of NAT by A6,ORDINAL1:def 12;
set sq = the CRoot of k1,-(q.0/q.k1);
deffunc O(Nat) =
(q.In(k1+$1,NAT))*((power F_Complex).(sq,In(k1+$1,NAT)));
consider F2 be FinSequence of the carrier of F_Complex such that
A9: len F2 = len q-'(k1+1) and
A10: for n be Nat st n in dom F2 holds F2.n = O(n) from FINSEQ_2:sch 1;
k1 < len q by A6,ALGSEQ_1:8;
then
A11: k+1+0 <= len q by NAT_1:13;
then len q-(k+1) >= 0 by XREAL_1:19;
then
A12: len F2 = len q-(k+1) by A9,XREAL_0:def 2;
A13: eval(p,z0) = eval(p,z0+0.F_Complex) by RLVECT_1:def 4
.= eval(p,eval(<%z0,1_F_Complex%>,0.F_Complex)) by Th47
.= eval(q,0.F_Complex) by Th53;
A14: now
let z be Element of F_Complex;
eval(q,z) = eval(p,eval(<%z0,1_F_Complex%>,z)) by Th53
.= eval(p,z0+z) by Th47;
then |.eval(q,z).| >= |.eval(p,z0).| by A3;
hence |.eval(q,z).| >= |.q.0 .| by A13,Th31;
end;
now
let c be Real;
assume that
A15: 0 < c and
A16: c < 1;
set z1 = [**c,0**]*sq;
consider F1 be FinSequence of the carrier of F_Complex such that
A17: eval(q,z1) = Sum F1 and
A18: len F1 = len q and
A19: for n be Element of NAT st n in dom F1 holds F1.n = q.(n-'1)*(
power F_Complex).(z1,n-'1) by POLYNOM4:def 2;
A20: dom ((F1/^(k+1))*[**c to_power (k+1),0**]") = dom (F1/^(k+1))
by POLYNOM1:def 2;
A21: k1 < len F1 by A6,A18,ALGSEQ_1:8;
reconsider FF = F1|k1 as FinSequence of the carrier of F_Complex;
1 in Seg k by A6,FINSEQ_1:1;
then 1 in Seg len (F1|k) by A21,FINSEQ_1:59;
then
A22: 1 in dom FF by FINSEQ_1:def 3;
A23: dom FF c= dom F1 by FINSEQ_5:18;
now
let i be Element of NAT;
assume that
A24: i in dom FF and
A25: i <> 1;
A26: 0+1 <= i by A24,FINSEQ_3:25;
then i > 1 by A25,XXREAL_0:1;
then i >= 1+1 by NAT_1:13;
then i-1 >= 1+1-1 by XREAL_1:9;
then
A27: i-'1 >= 1 by XREAL_0:def 2;
i <= len (F1|k) by A24,FINSEQ_3:25;
then i <= k by A21,FINSEQ_1:59;
then i < k+1 by NAT_1:13;
then
A28: i-1 < k by XREAL_1:19;
i-1 >= 0 by A26;
then
A29: i-'1 < k by A28,XREAL_0:def 2;
thus FF/.i = F1/.i by A24,FINSEQ_4:70
.= F1.i by A23,A24,PARTFUN1:def 6
.= q.(i-'1)*(power F_Complex).(z1,i-'1) by A19,A23,A24
.= 0.F_Complex*(power F_Complex).(z1,i-'1) by A7,A27,A29
.= 0.F_Complex;
end;
then
A30: Sum FF = FF/.1 by A22,POLYNOM2:3
.= F1/.1 by A22,FINSEQ_4:70
.= F1.1 by A22,A23,PARTFUN1:def 6
.= q.(1-'1)*(power F_Complex).(z1,1-'1) by A19,A22,A23
.= q.0*(power F_Complex).(z1,1-'1) by XREAL_1:232
.= q.0*(power F_Complex).(z1,0) by XREAL_1:232
.= q.0*1_F_Complex by GROUP_1:def 7
.= q.0;
k+1 in Seg len F1 by A8,A11,A18,FINSEQ_1:1;
then
A31: k+1 in dom F1 by FINSEQ_1:def 3;
then
A32: F1.(k+1) = F1/.(k+1) by PARTFUN1:def 6;
set gc = Sum(F1/^(k+1))/[**c to_power (k+1),0**];
A33: c to_power (k+1) > 0 by A15,POWER:34;
then
A34: Sum(F1/^(k+1)) = [**c to_power (k+1),0**]*Sum(F1/^(k+1))/ [**c
to_power (k+1),0**] by COMPLFLD:7,30
.= [**c to_power (k+1),0**]*gc;
A35: F1/.(k+1) = F1.(k+1) by A31,PARTFUN1:def 6
.= q.(k+1-'1)*(power F_Complex).(z1,k+1-'1) by A19,A31
.= q.k1*(power F_Complex).(z1,k+1-'1) by NAT_D:34
.= q.k1*(power F_Complex).(z1,k1) by NAT_D:34
.= q.k1*((power F_Complex).([**c,0**],k1)* (power F_Complex).(sq,k1)
) by GROUP_1:52
.= q.k1*((power F_Complex).([**c,0**],k1)*(-(q.0/q.k1))) by
COMPLFLD:def 2
.= q.k1*(-(q.0/q.k1))*(power F_Complex).([**c,0**],k1)
.= q.k1*((-(q.0))/q.k1)*(power F_Complex).([**c,0**],k1)
.= (q.k1* (-q.0))/q.k1*(power F_Complex).([**c,0**],k1)
.= (-q.0)*(power F_Complex).([**c,0**],k1) by A6,COMPLFLD:30
.= (-q.0)*[**c to_power k,0**] by A15,HAHNBAN1:29;
A36: |.q.0*(1_F_Complex-[**c to_power k,0**])+[**c to_power (k+1),0**]*
gc.| <= |.q.0*(1_F_Complex-[**c to_power k,0**]).| + |.[**c to_power (k+1),0**]
*gc.| by COMPLFLD:62;
F1 = (F1|(k+1-'1))^<*F1.(k+1)*>^(F1/^(k+1)) by A8,A11,A18,POLYNOM4:1;
then Sum F1 = Sum((F1|(k+1-'1))^<*F1/.(k+1)*>) + Sum(F1/^(k+1)) by A32,
RLVECT_1:41
.= Sum(F1|(k+1-'1)) + Sum<*F1/.(k+1)*> + Sum (F1/^(k+1)) by RLVECT_1:41
.= Sum(F1|k) + Sum<*F1/.(k+1)*> + Sum(F1/^(k+1)) by NAT_D:34
.= q.0 + (-q.0)*[**c to_power k,0**] + Sum(F1/^(k+1)) by A30,A35,
RLVECT_1:44
.= q.0 + -q.0*[**c to_power k,0**] + Sum(F1/^(k+1))
.= q.0*1_F_Complex - q.0*[**c to_power k,0**] + Sum(F1/^(k+1))
.= q.0*(1_F_Complex-[**c to_power k,0**])+ [**c to_power (k+1),0**]*
gc by A34;
then
|.q.0*(1_F_Complex-[**c to_power k,0**])+ [**c to_power (k+1),0**]*
gc.| >= |.q.0 .| by A14,A17;
then
|.q.0*(1_F_Complex-[**c to_power k,0**]).| + |.[**c to_power (k+1),
0**]*gc.| >= |.q.0 .| by A36,XXREAL_0:2;
then
|.q.0 .|*|.1_F_Complex-[**c to_power k,0**].| + |.[**c to_power (k+
1),0**]*gc.| >= |.q.0 .| by COMPLFLD:71;
then
A37: |.q.0 .|*|.1_F_Complex-[**c to_power k,0**].| + |.[**c to_power (k+
1),0**].|*|.gc.| >= |.q.0 .| by COMPLFLD:71;
0 + (c to_power k1) <= 1 by A15,A16,TBSP_1:2;
then
A38: 1-(c to_power k) >= 0 by XREAL_1:19;
A39: c to_power k > 0 by A15,POWER:34;
A40: len |.(F1/^(k+1))*[**c to_power (k+1),0**]".| = len ((F1/^(k+1))*
[**c to_power (k+1),0**]") by Def2
.= len (F1/^(k+1)) by A20,FINSEQ_3:29
.= len F1-(k+1) by A11,A18,RFINSEQ:def 1
.= len |.F2.| by A12,A18,Def2;
now
let i be Element of NAT;
A41: k+1+i-'1 = k+i+1-1 by XREAL_0:def 2
.= k+i;
assume i in dom |.(F1/^(k+1))*[**c to_power (k+1),0**]".|;
then
A43: i in Seg len |.(F1/^(k+1))*[**c to_power (k+1),0**]".| by
FINSEQ_1:def 3;
then i <= len |.F2.| by A40,FINSEQ_1:1;
then i <= len F1-(k+1) by A12,A18,Def2;
then k+i+1 >= 0+1 & k+1+i <= len F1 by XREAL_1:6,19;
then
A44: k+1+i in dom F1 by FINSEQ_3:25;
i >= 0+1 by A43,FINSEQ_1:1;
then
A45: i-1 >= 0;
c to_power (i-'1) <= 1 by A15,A16,TBSP_1:2;
then
A46: c to_power (i-1) <= 1 by A45,XREAL_0:def 2;
A47: c to_power (k+i) > 0 by A15,POWER:34;
A48: k+i-(k+1) = i-1;
i in Seg len ((F1/^(k+1))*[**c to_power (k+1),0**]") by A43,Def2;
then
A49: i in dom ((F1/^(k+1))*[**c to_power (k+1),0**]") by FINSEQ_1:def 3;
then
A50: (F1/^(k+1))/.i = (F1/^(k+1)).i by A20,PARTFUN1:def 6
.= F1.(k+1+i) by A11,A18,A20,A49,RFINSEQ:def 1
.= q.In(k+1+i-'1,NAT)*(power F_Complex).([**c,0**]*sq,k+1+i-'1)
by A19,A44
.= q.In(k+i,NAT)*(power(sq,k+i)* power([**c,0**],k+i))
by A41,GROUP_1:52
.= q.In(k+i,NAT)*power(sq,k+i)* power([**c,0**],k+i);
A51: len F2 = len |.F2.| by Def2;
A53: |.(F1/^(k+1))*[**c to_power (k+1),0**]".|.i
= |.((F1/^(k+1))*[**c to_power (k+1),0**]").i.| by A49,Def2
.= |.((F1/^(k+1))*[**c to_power (k+1),0**]")/.i.|
by A49,PARTFUN1:def 6
.= |.((F1/^(k+1))/.i)*[**c to_power (k+1),0**]".|
by A20,A49,POLYNOM1:def 2
.= |.(F1/^(k+1))/.i.|*|.[**c to_power (k+1),0**]".| by COMPLFLD:71
.= |.q.In(k+i,NAT)*power(sq,k+i)*
power([**c,0**],k+i).|*|.c to_power (k+1).|"
by A33,A50,COMPLFLD:7,72
.= |.q.In(k+i,NAT)*power(sq,k+i).|*
|.power([**c,0**],k+i).|*|.c to_power (k+1).|" by COMPLFLD:71
.= |.q.In(k+i,NAT)*power(sq,k+i).|* |.[**c to_power (k+i),0
**].|*|.c to_power (k+1).|" by A15,HAHNBAN1:29
.= |.q.In(k+i,NAT)*power(sq,k+i).|* (c to_power (k+i))*|.
c to_power (k+1).|" by A47,ABSVALUE:def 1
.= |.q.In(k+i,NAT)*power(sq,k+i).|* (c to_power (k+i))*(c
to_power In(k+1,NAT))" by A33,ABSVALUE:def 1
.= |.q.In(k+i,NAT)*power(sq,k+i).|* ((c to_power (k+i))*(c
to_power (k+1))")
.= |.q.In(k+i,NAT)*power(sq,k+i).|* ((c to_power (k+i))/(c
to_power (k+1)))
.= |.q.In(k+i,NAT)*power(sq,k+i).|*(c to_power (i-1))
by A15,A48,POWER:29;
A54: i in dom F2 by A40,A43,A51,FINSEQ_1:def 3;
(q.In(k+i,NAT))*power(sq,k+i)
= q.In(k+i,NAT)*(power F_Complex).(sq,In(k+i,NAT))
.= O(i)
.= F2.i by A54,A10;
then |.(F1/^(k+1))*[**c to_power (k+1),0**]".|.i <= |.F2.i.|
by A46,A53,COMPLEX1:46,XREAL_1:153;
hence |.(F1/^(k+1))*[**c to_power (k+1),0**]".|.i <= |.F2.|.i
by A54,Def2;
end;
then
A55: Sum|.(F1/^(k+1))*[**c to_power (k+1),0**]".| <= Sum|.F2.|
by A40,INTEGRA5:3;
|.1_F_Complex-[**c to_power k,0**].| = |.[**1,0**]-[**c to_power k,
0**].| by COMPLEX1:def 4,COMPLFLD:8
.= |.[**1-(c to_power k1),0-0**].|
.= 1-(c to_power k) by A38,ABSVALUE:def 1;
then |.[**c to_power (k+1),0**].|*|.gc.| >= |.q.0 .|*1 - |.q.0 .|*(1-(c
to_power k)) by A37,XREAL_1:20;
then (c to_power (k+1))*|.gc.| >= |.q.0 .|*(c to_power k) by A33,
ABSVALUE:def 1;
then
(c to_power (k+1))*|.gc.|/(c to_power k) >= |.q.0 .|*(c to_power k)
/(c to_power k) by A39,XREAL_1:72;
then (c to_power (k+1))/(c to_power k)*|.gc.| >= |.q.0 .| by A39,
XCMPLX_1:89;
then (c to_power (k+1-k))*|.gc.| >= |.q.0 .| by A15,POWER:29;
then
A56: c*|.gc.| >= |.q.0 .| by POWER:25;
gc = Sum(F1/^(k+1))*[**c to_power (k+1),0**]"
.= Sum((F1/^(k+1))*[**c to_power (k+1),0**]") by POLYNOM1:13;
then |.gc.| <= Sum |.(F1/^(k+1))*[**c to_power (k+1),0**]".| by Th14;
then |.gc.| <= Sum|.F2.| by A55,XXREAL_0:2;
then c*|.gc.| <= c*Sum|.F2.| by A15,XREAL_1:64;
hence c*Sum|.F2.| >= |.q.0 .| by A56,XXREAL_0:2;
end;
then |.q.0 .| <= 0 by Lm1;
then
A57: q.0 = 0.F_Complex by COMPLFLD:59;
ex x be Element of F_Complex st x is_a_root_of p
proof
take z0;
eval(p,z0) = 0.F_Complex by A13,A57,Th31;
hence thesis;
end;
hence thesis;
end;
suppose
A58: len p = 2;
set np=NormPolynomial(p);
A59: len p-'1 = 2-1 by A58,XREAL_0:def 2;
A60: len np = len p by A58,Th57;
A61: now
let k be Nat;
assume
A62: k < len np;
per cases by A58,A60,A62,NAT_1:23;
suppose
k=0;
hence np.k = <%np.0,1_F_Complex%>.k by Th38;
end;
suppose
A63: k=1;
hence np.k = 1_F_Complex by A58,A59,Th56
.= <%np.0,1_F_Complex%>.k by A63,Th38;
end;
end;
len <%np.0,1_F_Complex%> = 2 by Th40;
then
A64: np = <%np.0,1_F_Complex%> by A58,A61,Th57,ALGSEQ_1:12;
ex x be Element of F_Complex st x is_a_root_of np
proof
take z0 = -np.0;
eval(np,z0) = np.0+z0 by A64,Th47
.= 0.F_Complex by RLVECT_1:5;
hence thesis;
end;
then np is with_roots;
hence thesis by A58,Th60;
end;
end;
registration
cluster F_Complex -> algebraic-closed;
coherence by Th74;
end;
registration
cluster algebraic-closed add-associative right_zeroed right_complementable
Abelian commutative associative distributive almost_left_invertible non
degenerated for well-unital non empty doubleLoopStr;
existence
proof
take F_Complex;
thus thesis;
end;
end;