Copyright (c) 2000 Association of Mizar Users
environ
vocabulary ARYTM_1, ARYTM, SQUARE_1, ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1,
RLVECT_1, BOOLE, FINSEQ_4, HAHNBAN1, COMPLEX1, BINOP_1, VECTSP_1,
LATTICES, NORMSP_1, COMPLFLD, GROUP_1, POWER, POLYNOM1, ORDINAL2,
ALGSEQ_1, POLYNOM3, POLYNOM2, ALGSTR_2, FUNCT_4, VECTSP_2, CQC_LANG,
FCONT_1, FUNCOP_1, PRE_TOPC, SEQ_1, FUNCT_2, QC_LANG1, PARTFUN1, SEQ_4,
SEQ_2, COMSEQ_1, SEQM_3, COMPTRIG, RFINSEQ, ABSVALUE, POLYNOM5;
notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0,
ORDINAL1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0,
REAL_1, SQUARE_1, NAT_1, ABSVALUE, POWER, PRE_TOPC, RLVECT_1, VECTSP_2,
VECTSP_1, BINOP_1, RELAT_1, FUNCT_1, FUNCT_2, FRAENKEL, FINSEQ_1,
FINSEQ_4, RFINSEQ, FINSOP_1, FUNCSDOM, CFCONT_1, SEQ_1, SEQ_2, SEQM_3,
SEQ_4, COMSEQ_1, COMSEQ_2, COMSEQ_3, PARTFUN1, TOPREAL1, COMPLEX1,
NORMSP_1, BINARITH, RVSUM_1, GROUP_1, COMPLFLD, HAHNBAN1,
POLYNOM1, ALGSEQ_1, POLYNOM3, POLYNOM4, COMPTRIG;
constructors REAL_1, ENUMSET1, FINSOP_1, SQUARE_1, POWER, MONOID_0, ALGSTR_2,
SEQ_2, SEQ_4, COMSEQ_1, COMSEQ_2, COMSEQ_3, RFINSEQ, FUNCSDOM, CFCONT_1,
TOPREAL1, COMPLSP1, BINARITH, HAHNBAN1, POLYNOM1, POLYNOM4, COMPTRIG,
COMPLEX1, ARYTM_0, ARYTM_3;
clusters XREAL_0, STRUCT_0, INT_1, RELSET_1, FINSEQ_5, SEQ_1, SEQM_3,
COMSEQ_1, COMSEQ_2, BINARITH, VECTSP_2, GROUP_1, ALGSTR_1, ENDALG,
COMPLFLD, POLYNOM1, POLYNOM3, TOPREAL1, MONOID_0, VECTSP_1, NAT_1,
COMPLEX1, MEMBERED, FUNCT_1, FUNCT_2, ORDINAL2, NUMBERS, POLYNOM4;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, ALGSEQ_1, SEQ_4, XBOOLE_0;
theorems AXIOMS, XREAL_0, TARSKI, ENUMSET1, STRUCT_0, REAL_1, REAL_2, NAT_1,
SQUARE_1, POWER, BINARITH, INT_1, ABSVALUE, NORMSP_1, 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, FUNCSDOM, PRE_TOPC, TOPREAL1,
TOPREAL3, INTEGRA5, RLVECT_1, VECTSP_1, RVSUM_1, SEQ_1, SEQ_2, SEQM_3,
SEQ_4, COMSEQ_1, COMSEQ_2, COMSEQ_3, CFUNCT_1, FVSUM_1, GROUP_1,
CQC_THE1, JORDAN8, GOBOARD9, AMI_5, ALGSEQ_1, COMPLEX1, COMPLFLD,
HAHNBAN1, POLYNOM1, POLYNOM2, POLYNOM3, POLYNOM4, COMPTRIG, XBOOLE_0,
XCMPLX_0, XCMPLX_1, VECTSP_2, ARYTM_0;
schemes NAT_1, FUNCT_2, FINSEQ_2, MATRIX_2, BINOP_1, BINARITH, GOBOARD2,
SEQ_1, CFCONT_1, COMPLSP1;
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;
n > 0 & m > 0 by A1,A2,NAT_1:19;
then n >= 0+1 & m >= 0+1 by NAT_1:38;
then n-1 >= 0+1-1 & m-1 >= 0+1-1 by REAL_1:49;
then (n-1)*(m-1) >= 0 by REAL_2:121;
then n*m - n*1 - 1*m + 1*1 >= 0 by XCMPLX_1:47;
hence thesis;
end;
theorem Th2:
for x,y be real number st y > 0 holds
min(x,y)/max(x,y) <= 1
proof
let x,y be real number;
assume that
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 SQUARE_1:def 1,def 2;
hence min(x,y)/max(x,y) <= 1 by A1,A3,REAL_2:143;
suppose A4: x < y;
then max(x,y) = y & min(x,y) = x by SQUARE_1:def 1,def 2;
hence min(x,y)/max(x,y) <= 1 by A2,A4,REAL_2:143;
end;
hence thesis;
suppose
A5: x <= 0;
then min (x,y) = x & max (x,y) = y by A1,SQUARE_1:def 1,def 2;
then min(x,y)/max(x,y) <= 0 by A1,A5,REAL_2:126;
hence thesis by AXIOMS:22;
end;
theorem Th3:
for x,y be real number st
for c be real number st c > 0 & c < 1 holds c*x >= y holds
y <= 0
proof
let x,y be real number;
assume that
A1: for c be real number st c > 0 & c < 1 holds c*x >= y;
assume A2: y > 0;
set mi = min(x,y);
set ma = max(x,y);
set c = mi/(2*ma);
A3: y*2 > y by A2,REAL_2:144;
per cases;
suppose A4: x > 0;
then A5: mi > 0 & ma > 0 by A2,SQUARE_1:38,49;
then 2*ma > 0 by REAL_2:122;
then A6: c > 0 by A5,REAL_2:127;
A7: mi/ma <= 1 by A4,Th2;
mi/ma > 0 by A5,REAL_2:127;
then mi/ma*2 > mi/ma by REAL_2:144;
then mi/ma > mi/ma/2 by REAL_2:178;
then mi/ma > mi/(ma*2) by XCMPLX_1:79;
then c < 1 by A7,AXIOMS:22;
then A8: c*x >= y by A1,A6;
now per cases;
suppose x >= y;
then ma = x & mi = y by SQUARE_1:def 1,def 2;
then c*x = y/2 by A4,XCMPLX_1:93;
hence contradiction by A3,A8,REAL_2:178;
suppose A9: x < y;
then A10: ma = y & mi = x by SQUARE_1:def 1,def 2;
2*y > 0 by A2,REAL_2:122;
then 0 < x/(2*y) by A4,REAL_2:127;
then c*x < x/(2*y)*y by A4,A9,A10,REAL_2:199;
then A11: c*x < x/2 by A2,XCMPLX_1:93;
x/2 < y/2 by A9,REAL_1:73;
then A12: c*x < y/2 by A11,AXIOMS:22;
y > y/2 by A3,REAL_2:178;
hence contradiction by A8,A12,AXIOMS:22;
end;
hence contradiction;
suppose x <= 0;
then 1/2*x <= 0 by REAL_2:123;
hence contradiction by A1,A2;
end;
Lm1:
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;
for c be real number st c > 0 & c < 1 holds c*x >= y
proof
let c be real number;
A2: c is Real by XREAL_0:def 1;
assume c > 0 & c < 1;
hence thesis by A1,A2;
end;
hence thesis by Th3;
end;
theorem Th4:
for p be FinSequence of REAL st for n be Nat st n in dom p holds p.n >= 0
for i be Nat st i in dom p holds
Sum p >= p.i
proof
defpred Q[FinSequence of REAL] means
(for n be Nat st n in dom $1 holds $1.n >= 0) implies
for i be Nat st i in dom $1 holds Sum $1 >= $1.i;
A1: Q[<*>(REAL)] by FINSEQ_1:26;
A2: 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 A3: (for n be Nat st n in dom p holds p.n >= 0) implies
for i be Nat st i in dom p holds Sum p >= p.i;
assume A4: for n be Nat st n in dom (p^<*x*>) holds (p^<*x*>).n >= 0;
let i be Nat;
assume A5: i in dom (p^<*x*>);
A6: dom p c= dom (p^<*x*>) by FINSEQ_1:39;
A7: now let n be Nat;
assume A8: n in dom p;
then (p^<*x*>).n >= 0 by A4,A6;
hence p.n >= 0 by A8,FINSEQ_1:def 7;
end;
len (p^<*x*>) = len p+1 by FINSEQ_2:19;
then A9: dom (p^<*x*>) = Seg (len p+1) by FINSEQ_1:def 3
.= Seg len p \/ {len p+1} by FINSEQ_1:11
.= dom p \/ {len p+1} by FINSEQ_1:def 3;
len p >= 0 by NAT_1:18;
then len p+1 >= 0+1 by AXIOMS:24;
then len (p^<*x*>) >= 1 by FINSEQ_2:19;
then len (p^<*x*>) in dom (p^<*x*>) by FINSEQ_3:27;
then (p^<*x*>).len (p^<*x*>) >= 0 by A4;
then (p^<*x*>).(len p+1) >= 0 by FINSEQ_2:19;
then x >= 0 by FINSEQ_1:59;
then A10: p.i + x >= p.i + 0 by AXIOMS:24;
defpred P[Nat] means Sum (p|$1) >= 0;
A11: P[0] by RVSUM_1:102;
A12: for j be Nat st P[j] holds P[j+1]
proof
let j be Nat;
assume A13: Sum (p|j) >= 0;
per cases;
suppose A14: j+1 <= len p;
j+1 >= 1 by NAT_1:29;
then A15: j+1 in dom p by A14,FINSEQ_3:27;
then p.(j+1) >= 0 by A7;
then A16: p/.(j+1) >= 0 by A15,FINSEQ_4:def 4;
p|(j+1) = p|j ^ <*p/.(j+1)*> by A14,JORDAN8:2;
then Sum (p|(j+1)) = Sum(p|j) + p/.(j+1) by RVSUM_1:104;
then Sum (p|(j+1)) >= 0+0 by A13,A16,REAL_1:55;
hence Sum (p|(j+1)) >= 0;
suppose A17: j+1 > len p;
then j >= len p by NAT_1:38;
then p|j = p & p|(j+1) = p by A17,TOPREAL1:2;
hence Sum (p|(j+1)) >= 0 by A13;
end;
A18: for j be Nat holds P[j] from Ind(A11,A12);
p|(len p) = p by TOPREAL1:2;
then A19: Sum p >= 0 by A18;
per cases by A5,A9,XBOOLE_0:def 2;
suppose A20: i in dom p;
then A21: Sum p >= p.i by A3,A7;
Sum (p^<*x*>) = Sum p + x by RVSUM_1:104;
then Sum (p^<*x*>) >= p.i + x by A21,AXIOMS:24;
then Sum (p^<*x*>) >= p.i by A10,AXIOMS:22;
hence Sum (p^<*x*>) >= (p^<*x*>).i by A20,FINSEQ_1:def 7;
suppose i in {len p+1};
then i = len p+1 by TARSKI:def 1;
then (p^<*x*>).i = x by FINSEQ_1:59;
then Sum p + x >= 0+(p^<*x*>).i by A19,AXIOMS:24;
hence Sum (p^<*x*>) >= (p^<*x*>).i by RVSUM_1:104;
end;
thus for p be FinSequence of REAL holds Q[p] from IndSeqD(A1,A2);
end;
theorem Th5:
for x,y be Real holds
-[**x,y**] = [**-x,-y**]
proof
let x,y be Real;
[**x,y**] = [*x,y*] by HAHNBAN1:def 1;
hence -[**x,y**] = -[*x,y*] by COMPLFLD:4
.= [*- Re[*x,y*],-Im [*x,y*]*] by COMPLEX1:def 11
.= [*-x,-Im [*x,y*]*] by COMPLEX1:7
.= [*-x,-y*] by COMPLEX1:7
.= [**-x,-y**] by HAHNBAN1:def 1;
end;
theorem Th6:
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**] by RLVECT_1:def 11
.= [**x1,y1**]+[**-x2,-y2**] by Th5
.= [**x1+-x2,y1+-y2**] by HAHNBAN1:10
.= [**x1-x2,y1+-y2**] by XCMPLX_0:def 8
.= [**x1-x2,y1-y2**] by XCMPLX_0:def 8;
end;
scheme ExDHGrStrSeq { R() -> non empty HGrStr,
F(set) -> Element of R() } :
ex S be sequence of R() st for n be Nat holds S.n = F(n)
proof
set Y = the carrier of R();
deffunc G(set) = F($1);
A1: for x be set st x in NAT holds G(x) in Y;
ex f be Function of NAT,Y st for x be set st x in NAT holds f.x = G(x)
from Lambda1(A1);
then consider f be Function of NAT,Y such that
A2: for x be set st x in NAT holds f.x = F(x);
reconsider f as sequence of R() by NORMSP_1:def 3;
take f;
thus thesis by A2;
end;
scheme ExDdoubleLoopStrSeq { R() -> non empty doubleLoopStr,
F(set) -> Element of R() } :
ex S be sequence of R() st for n be Nat holds S.n = F(n)
proof
set Y = the carrier of R();
deffunc G(set) = F($1);
A1: for x be set st x in NAT holds G(x) in Y;
ex f be Function of NAT,Y st for x be set st x in NAT holds f.x = G(x)
from Lambda1(A1);
then consider f be Function of NAT,Y such that
A2: for x be set st x in NAT holds f.x = F(x);
reconsider f as sequence of R() by NORMSP_1:def 3;
take f;
thus thesis by A2;
end;
canceled;
theorem Th8:
for z be Element of F_Complex st z <> 0.F_Complex
for n be Nat holds
|.(power F_Complex).(z,n).| = |.z.| to_power n
proof
let z be Element of F_Complex;
assume z <> 0.F_Complex;
then A1: |.z.| <> 0 by COMPLFLD:94;
A2: |.z.| >= 0 by COMPLFLD:95;
defpred P[Nat] means |.(power F_Complex).(z,$1).| = |.z.| to_power $1;
|.(power F_Complex).(z,0).| = |.1.F_Complex.| by GROUP_1:def 7
.= |.1_(F_Complex).| by POLYNOM2:3
.= 1 by COMPLEX1:134,COMPLFLD:10,def 3
.= |.z.| to_power 0 by POWER:29;
then A3: P[0];
A4: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A5: |.(power F_Complex).(z,n).| = |.z.| to_power n;
thus |.(power F_Complex).(z,n+1).| = |.(power F_Complex).(z,n)*z.|
by GROUP_1:def 7
.= (|.z.| to_power n)*|.z.| by A5,COMPLFLD:109
.= (|.z.| to_power n)*(|.z.| to_power 1) by POWER:30
.= |.z.| to_power (n+1) by A1,A2,POWER:32;
end;
thus for n be Nat holds P[n] from Ind(A3,A4);
end;
definition
let p be FinSequence of the carrier of F_Complex;
func |.p.| -> FinSequence of REAL means :Def1:
len it = len p &
for n be Nat st n in dom p holds it/.n = |.p/.n.|;
existence
proof
deffunc F(Nat) = |.p/.$1.|;
consider q be FinSequence of REAL such that
A1: len q = len p and
A2: for n be Nat st n in dom q holds q/.n = F(n) from PiLambdaD;
take q;
dom p = dom q by A1,FINSEQ_3:31;
hence thesis by A1,A2;
end;
uniqueness
proof
let q1,q2 be FinSequence of REAL such that
A3: len q1 = len p and
A4: for n be Nat st n in dom p holds q1/.n = |.p/.n.| and
A5: len q2 = len p and
A6: for n be Nat st n in dom p holds q2/.n = |.p/.n.|;
A7: dom q1 = dom p & dom q2 = dom p by A3,A5,FINSEQ_3:31;
now let n be Nat;
assume A8: n in dom p;
hence q1/.n = |.p/.n.| by A4
.= q2/.n by A6,A8;
end;
hence q1 = q2 by A7,FINSEQ_5:13;
end;
end;
theorem Th9:
|.<*>the carrier of F_Complex.| = <*>REAL
proof
len |.<*>the carrier of F_Complex.| = len <*>the carrier of F_Complex
by Def1
.= 0 by FINSEQ_1:32;
hence |.<*>the carrier of F_Complex.| = <*>REAL by FINSEQ_1:32;
end;
theorem Th10:
for x be Element of F_Complex holds
|.<*x*>.| = <*|.x.|*>
proof
let x be Element of F_Complex;
A1: len |.<*x*>.| = len <*x*> by Def1
.= 1 by FINSEQ_1:56;
A2: len <*|.x.|*> = 1 by FINSEQ_1:56;
0+1 in Seg (0+1) by FINSEQ_1:6;
then A3: 1 in dom <*x*> by FINSEQ_1:55;
len |.<*x*>.| = len <*x*> by Def1;
then A4: 1 in dom |.<*x*>.| by A3,FINSEQ_3:31;
now let n be Nat;
assume n in Seg 1;
then A5: n = 1 by FINSEQ_1:4,TARSKI:def 1;
hence |.<*x*>.|.n = |.<*x*>.|/.1 by A4,FINSEQ_4:def 4
.= |.<*x*>/.1 .| by A3,Def1
.= |.x.| by FINSEQ_4:25
.= <*|.x.|*>.n by A5,FINSEQ_1:57;
end;
hence thesis by A1,A2,FINSEQ_2:10;
end;
theorem
for x,y be Element of F_Complex holds
|.<*x,y*>.| = <*|.x.|,|.y.|*>
proof
let x,y be Element of F_Complex;
A1: len |.<*x,y*>.| = len <*x,y*> by Def1
.= 2 by FINSEQ_1:61;
A2: len <*|.x.|,|.y.|*> = 2 by FINSEQ_1:61;
now let n be Nat;
assume A3: n in Seg 2;
per cases by A3,FINSEQ_1:4,TARSKI:def 2;
suppose A4: n = 1;
then A5: 1 in dom <*x,y*> by A3,FINSEQ_3:29;
len |.<*x,y*>.| = len <*x,y*> by Def1;
then 1 in dom |.<*x,y*>.| by A5,FINSEQ_3:31;
then |.<*x,y*>.|.1 = |.<*x,y*>.|/.1 by FINSEQ_4:def 4
.= |.<*x,y*>/.1 .| by A5,Def1;
then |.<*x,y*>.|.1 = |.x.| by FINSEQ_4:26;
hence |.<*x,y*>.|.n = <*|.x.|,|.y.|*>.n by A4,FINSEQ_1:61;
suppose A6: n = 2;
then A7: 2 in dom <*x,y*> by A3,FINSEQ_3:29;
len |.<*x,y*>.| = len <*x,y*> by Def1;
then 2 in dom |.<*x,y*>.| by A7,FINSEQ_3:31;
then |.<*x,y*>.|.2 = |.<*x,y*>.|/.2 by FINSEQ_4:def 4
.= |.<*x,y*>/.2 .| by A7,Def1;
then |.<*x,y*>.|.2 = |.y.| by FINSEQ_4:26;
hence |.<*x,y*>.|.n = <*|.x.|,|.y.|*>.n by A6,FINSEQ_1:61;
end;
hence thesis by A1,A2,FINSEQ_2:10;
end;
theorem
for x,y,z be Element of F_Complex holds
|.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>
proof
let x,y,z be Element of F_Complex;
A1: len |.<*x,y,z*>.| = len <*x,y,z*> by Def1
.= 3 by FINSEQ_1:62;
A2: len <*|.x.|,|.y.|,|.z.|*> = 3 by FINSEQ_1:62;
now let n be Nat;
assume A3: n in Seg 3;
per cases by A3,ENUMSET1:13,FINSEQ_3:1;
suppose A4: n = 1;
A5: 1 in dom <*x,y,z*> by TOPREAL3:6;
len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then 1 in dom |.<*x,y,z*>.| by A5,FINSEQ_3:31;
then |.<*x,y,z*>.|.1 = |.<*x,y,z*>.|/.1 by FINSEQ_4:def 4
.= |.<*x,y,z*>/.1 .| by A5,Def1;
then |.<*x,y,z*>.|.1 = |.x.| by FINSEQ_4:27;
hence |.<*x,y,z*>.|.n = <*|.x.|,|.y.|,|.z.|*>.n by A4,FINSEQ_1:62;
suppose A6: n = 2;
A7: 2 in dom <*x,y,z*> by TOPREAL3:6;
len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then 2 in dom |.<*x,y,z*>.| by A7,FINSEQ_3:31;
then |.<*x,y,z*>.|.2 = |.<*x,y,z*>.|/.2 by FINSEQ_4:def 4
.= |.<*x,y,z*>/.2 .| by A7,Def1;
then |.<*x,y,z*>.|.2 = |.y.| by FINSEQ_4:27;
hence |.<*x,y,z*>.|.n = <*|.x.|,|.y.|,|.z.|*>.n by A6,FINSEQ_1:62;
suppose A8: n = 3;
A9: 3 in dom <*x,y,z*> by TOPREAL3:6;
len |.<*x,y,z*>.| = len <*x,y,z*> by Def1;
then 3 in dom |.<*x,y,z*>.| by A9,FINSEQ_3:31;
then |.<*x,y,z*>.|.3 = |.<*x,y,z*>.|/.3 by FINSEQ_4:def 4
.= |.<*x,y,z*>/.3 .| by A9,Def1;
then |.<*x,y,z*>.|.3 = |.z.| by FINSEQ_4:27;
hence |.<*x,y,z*>.|.n = <*|.x.|,|.y.|,|.z.|*>.n by A8,FINSEQ_1:62;
end;
hence thesis by A1,A2,FINSEQ_2:10;
end;
theorem Th13:
for p,q be FinSequence of the carrier of F_Complex holds
|.p^q.| = |.p.|^|.q.|
proof
let p,q be FinSequence of the carrier of F_Complex;
A1: len |.p^q.| = len (p^q) by Def1
.= len p + len q by FINSEQ_1:35
.= len p + len |.q.| by Def1
.= len |.p.| + len |.q.| by Def1
.= len (|.p.|^|.q.|) by FINSEQ_1:35;
now let n be Nat;
assume A2: n in Seg len |.p^q.|;
then A3: n >= 1 & n <= len |.p^q.| by FINSEQ_1:3;
A4: n in dom |.p^q.| by A2,FINSEQ_1:def 3;
A5: len |.p^q.| = len (p^q) by Def1;
then A6: n in dom (p^q) by A2,FINSEQ_1:def 3;
A7: len |.p.| = len p by Def1;
per cases;
suppose A8: n in dom p;
then A9: n in dom |.p.| by A7,FINSEQ_3:31;
A10: (p^q)/.n = (p^q).n by A6,FINSEQ_4:def 4
.= p.n by A8,FINSEQ_1:def 7
.= p/.n by A8,FINSEQ_4:def 4;
thus |.p^q.|.n = |.p^q.|/.n by A4,FINSEQ_4:def 4
.= |.(p^q)/.n.| by A6,Def1
.= |.p.|/.n by A8,A10,Def1
.= |.p.|.n by A9,FINSEQ_4:def 4
.= (|.p.|^|.q.|).n by A9,FINSEQ_1:def 7;
suppose not n in dom p;
then A11: n > 0 + len p by A3,FINSEQ_3:27;
then A12: n - len p > 0 by REAL_1:86;
n = len p + (n+-len p) by XCMPLX_1:139;
then A13: n = len p + (n-len p) by XCMPLX_0:def 8
.= len p + (n-'len p) by A12,BINARITH:def 3;
A14: 1 + len p <= n by A11,NAT_1:38;
n <= len (p^q) by A2,A5,FINSEQ_1:3;
then n <= len q + len p by FINSEQ_1:35;
then 1 <= n-len p & n-len p <= len q by A14,REAL_1:84,86;
then 1 <= n-'len p & n-'len p <= len q by A12,BINARITH:def 3;
then A15: (n-'len p) in Seg len q by FINSEQ_1:3;
then A16: (n-'len p) in dom q by FINSEQ_1:def 3;
len |.q.| = len q by Def1;
then A17: (n-'len p) in dom |.q.| by A15,FINSEQ_1:def 3;
A18: (p^q)/.n = (p^q).n by A6,FINSEQ_4:def 4
.= q.(n-'len p) by A13,A16,FINSEQ_1:def 7
.= q/.(n-'len p) by A16,FINSEQ_4:def 4;
thus |.p^q.|.n = |.p^q.|/.n by A4,FINSEQ_4:def 4
.= |.(p^q)/.n.| by A6,Def1
.= |.q.|/.(n-'len p) by A16,A18,Def1
.= |.q.|.(n-'len p) by A17,FINSEQ_4:def 4
.= (|.p.|^|.q.|).n by A7,A13,A17,FINSEQ_1:def 7;
end;
hence thesis by A1,FINSEQ_2:10;
end;
theorem
for p be FinSequence of the carrier of F_Complex
for x be Element of F_Complex holds
|.p^<*x*>.| = |.p.|^<*|.x.|*> &
|.<*x*>^p.| = <*|.x.|*>^|.p.|
proof
let p be FinSequence of the carrier of F_Complex;
let x be Element of F_Complex;
thus |.p^<*x*>.| = |.p.|^|.<*x*>.| by Th13
.= |.p.|^<*|.x.|*> by Th10;
thus |.<*x*>^p.| = |.<*x*>.|^|.p.| by Th13
.= <*|.x.|*>^|.p.| by Th10;
end;
theorem Th15:
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.|;
0.F_Complex = the Zero of F_Complex by RLVECT_1:def 2;
then A1: P[<*>D] by Th9,COMPLFLD:93,RLVECT_1:60,RVSUM_1:102;
A2: now let p be FinSequence of D;
let x be Element of D;
assume P[p];
then A3: |.Sum p.| + |.x.| <= Sum|.p.| + |.x.| by AXIOMS:24;
Sum (p^<*x*>) = Sum p + x by FVSUM_1:87;
then A4: |.Sum (p^<*x*>).| <= |.Sum p.| + |.x.| by COMPLFLD:100;
Sum|.p.| + |.x.| = Sum|.p.| + Sum <*|.x.|*> by RVSUM_1:103
.= Sum|.p.| + Sum |.<*x*>.| by Th10
.= Sum(|.p.|^|.<*x*>.|) by RVSUM_1:105
.= Sum|.p^<*x*>.| by Th13;
hence P[p^<*x*>] by A3,A4,AXIOMS:22;
end;
thus for p be FinSequence of D holds P[p] from IndSeqD(A1,A2);
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 :Def2:
(power Polynom-Ring L).(p,n);
coherence
proof
reconsider p1 = p as Element of Polynom-Ring L
by POLYNOM3:def 12;
(power Polynom-Ring L).(p1,n) is Element of Polynom-Ring L
;
hence thesis by POLYNOM3:def 12;
end;
end;
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;
cluster p`^n -> finite-Support;
coherence
proof
reconsider p1 = p as Element of Polynom-Ring L
by POLYNOM3:def 12;
(power Polynom-Ring L).(p1,n) is Polynomial of L by POLYNOM3:def 12;
hence thesis by Def2;
end;
end;
theorem Th16:
for L be Abelian add-associative right_zeroed right_complementable
right_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
right_unital commutative distributive (non empty doubleLoopStr);
let p be Polynomial of L;
reconsider p1=p as Element of Polynom-Ring L
by POLYNOM3:def 12;
thus p`^0 = (power Polynom-Ring L).(p1,0) by Def2
.= 1.(Polynom-Ring L) by GROUP_1:def 7
.= 1_(Polynom-Ring L) by POLYNOM2:3
.= 1_.(L) by POLYNOM3:def 12;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
right_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
right_unital commutative distributive (non empty doubleLoopStr);
let p be Polynomial of L;
reconsider p1=p as Element of Polynom-Ring L
by POLYNOM3:def 12;
thus p`^1 = (power Polynom-Ring L).(p1,0+1) by Def2
.= (power Polynom-Ring L).(p1,0)*p1 by GROUP_1:def 7
.= (1.Polynom-Ring L)*p1 by GROUP_1:def 7
.= p by GROUP_1:def 4;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
right_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
right_unital commutative distributive (non empty doubleLoopStr);
let p be Polynomial of L;
reconsider p1=p as Element of Polynom-Ring L
by POLYNOM3:def 12;
thus p`^2 = (power Polynom-Ring L).(p1,1+1) by Def2
.= (power Polynom-Ring L).(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 by GROUP_1:def 4
.= p*'p by POLYNOM3:def 12;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
right_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
right_unital commutative distributive (non empty doubleLoopStr);
let p be Polynomial of L;
reconsider p1=p as Element of Polynom-Ring L
by POLYNOM3:def 12;
reconsider pp=p1*p1 as Polynomial of L by POLYNOM3:def 12;
thus p`^3 = (power Polynom-Ring L).(p1,2+1) by Def2
.= (power Polynom-Ring L).(p1,1+1)*p1 by GROUP_1:def 7
.= (power Polynom-Ring L).(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 by GROUP_1:def 4
.= pp*'p by POLYNOM3:def 12
.= p*'p*'p by POLYNOM3:def 12;
end;
theorem Th20:
for L be Abelian add-associative right_zeroed right_complementable
right_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
right_unital commutative distributive (non empty doubleLoopStr);
let p be Polynomial of L;
let n be Nat;
reconsider p1=p as Element of Polynom-Ring L
by POLYNOM3:def 12;
A1: (power Polynom-Ring L).(p1,n) = p`^n by Def2;
thus p`^(n+1) = (power Polynom-Ring L).(p1,n+1) by Def2
.= (power Polynom-Ring L).(p1,n)*p1 by GROUP_1:def 7
.= (p`^n)*'p by A1,POLYNOM3:def 12;
end;
theorem Th21:
for L be Abelian add-associative right_zeroed right_complementable
right_unital commutative distributive (non empty doubleLoopStr)
for n be Nat holds
0_.(L)`^(n+1) = 0_.(L)
proof
let L be Abelian add-associative right_zeroed right_complementable
right_unital commutative distributive (non empty doubleLoopStr);
let n be Nat;
thus 0_.(L)`^(n+1) = (0_.(L)`^n)*'0_.(L) by Th20
.= 0_.(L) by POLYNOM3:35;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
right_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
right_unital commutative distributive (non empty doubleLoopStr);
defpred P[Nat] means 1_.(L)`^$1 = 1_.(L);
A1: P[0] by Th16;
A2: now let n be Nat;
assume P[n];
then 1_.(L)`^(n+1) = (1_.(L))*'1_.(L) by Th20
.= 1_.(L) by POLYNOM3:36;
hence P[n+1];
end;
thus for n be Nat holds P[n] from Ind(A1,A2);
end;
theorem Th23:
for L be Field
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 Field;
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);
eval(p`^0,x) = eval(1_.(L),x) by Th16
.= 1_(L) by POLYNOM4:21
.= 1.L by POLYNOM2:3
.= (power L).(eval(p,x),0) by GROUP_1:def 7;
then A1: P[0];
A2: now let n be Nat;
assume A3: P[n];
eval(p`^(n+1),x) = eval((p`^n)*'p,x) by Th20
.= (power L).(eval(p,x),n)*eval(p,x) by A3,POLYNOM4:27
.= (power L).(eval(p,x),n+1) by GROUP_1:def 7;
hence P[n+1];
end;
thus for n be Nat holds P[n] from Ind(A1,A2);
end;
LC1: ::this is as a theorem in UPROOTS
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
A: len p > 0; then consider k being Nat such that
B: len p = k+1 by NAT_1:22;
len p -'1 = k+1-'1 by B; then
len p = (len p -'1)+1 by B, BINARITH:39;
hence p.(len p -'1) <> 0.L by ALGSEQ_1:25;
end;
theorem Th24:
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;
assume A1: len p <> 0;
defpred P[Nat] means len(p`^$1) = $1*len p-$1+1;
len(p`^0) = len(1_.(L)) by Th16
.= 0*len p-0+1 by POLYNOM4:7;
then A2: P[0];
A3: now let n be Nat;
assume A4: P[n];
A5: n >= 0 by NAT_1:18;
A6: len p > 0 by A1,NAT_1:19;
then len p >= 0+1 by NAT_1:38;
then A7: len p-1 >= 0+1-1 by REAL_1:49;
then A8: len p-'1 = len p-1 by BINARITH:def 3;
n*(len p-1) >= n*0 by A5,A7,AXIOMS:25;
then n*(len p-'1)+1 >= 0+1 by A8,AXIOMS:24;
then n*(len p-1)+1 > 0 by A8,NAT_1:38;
then A9: n*len p-n*1+1 > 0 by XCMPLX_1:40; then
(p`^n).(len (p`^n)-'1) <> 0.L & p.(len p -'1) <> 0.L by A4, A6, LC1; then
A9a: (p`^n).(len (p`^n)-'1) * p.(len p -'1) <> 0.L by VECTSP_2:def 5;
len(p`^(n+1)) = len((p`^n)*'p) by Th20
.= n*len p - n + 1 + len p - 1 by A4,A6,A9a,POLYNOM4:13
.= n*len p - n + len p + 1 - 1 by XCMPLX_1:1
.= n*len p + 1*len p - n + 1 - 1 by XCMPLX_1:29
.= (n+1)*len p - n + 1 - 1 by XCMPLX_1:8
.= (n+1)*len p - n - 1 + 1 by XCMPLX_1:29
.= (n+1)*len p - (n+1) + 1 by XCMPLX_1:36;
hence P[n+1];
end;
thus for n be Nat holds P[n] from Ind(A2,A3);
end;
definition
let L be non empty HGrStr;
let p be sequence of L;
let v be Element of L;
func v*p -> sequence of L means :Def3:
for n be Nat holds it.n = v*p.n;
existence
proof
deffunc F(Nat) = v*p.$1;
consider r be sequence of L such that
A1: for n be Nat holds r.n = F(n) from ExDHGrStrSeq;
take r;
thus thesis by A1;
end;
uniqueness
proof
let p1,p2 be sequence of L such that
A2: for n be Nat holds p1.n = v*p.n and
A3: for n be Nat holds p2.n = v*p.n;
now let k be Nat;
thus p1.k = v*p.k by A2
.= p2.k by A3;
end;
hence p1 = p2 by FUNCT_2:113;
end;
end;
definition
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;
thus (v*p).i = v*p.i by Def3
.= v*0.L by A1,ALGSEQ_1:22
.= 0.L by VECTSP_1:36;
end;
end;
theorem Th25:
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;
A1: 0 is_at_least_length_of (0.L*p)
proof
let i be Nat;
assume i>=0;
thus (0.L*p).i = 0.L*p.i by Def3
.= 0.L by VECTSP_1:39;
end;
for n be Nat st n is_at_least_length_of (0.L*p) holds 0<=n by NAT_1:18;
hence thesis by A1,ALGSEQ_1:def 4;
end;
theorem Th26:
for L be add-associative right_zeroed right_complementable left_unital
commutative associative distributive Field-like (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 left_unital
commutative associative distributive Field-like (non empty doubleLoopStr);
let p be Polynomial of L;
let v be Element of L;
assume A1: v <> 0.L;
A2: len p is_at_least_length_of (v*p)
proof
let i be Nat;
assume A3: i >= len p;
thus (v*p).i = v*p.i by Def3
.= v*0.L by A3,ALGSEQ_1:22
.= 0.L by VECTSP_1:36;
end;
now let n be Nat;
assume A4: n is_at_least_length_of v*p;
n is_at_least_length_of p
proof
let i be Nat;
assume i >= n;
then (v*p).i = 0.L by A4,ALGSEQ_1:def 3;
then v*p.i = 0.L by Def3;
hence p.i = 0.L by A1,VECTSP_1:44;
end;
hence len p <= n by ALGSEQ_1:def 4;
end;
hence thesis by A2,ALGSEQ_1:def 4;
end;
theorem Th27:
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;
now let n be Nat;
thus (0_.(L)).n = 0.L by POLYNOM3:28
.= 0.L*p.n by VECTSP_1:39;
end;
hence thesis by Def3;
end;
theorem Th28:
for L be left_unital (non empty multLoopStr)
for p be sequence of L holds
1_(L)*p = p
proof
let L be left_unital (non empty multLoopStr);
let p be sequence of L;
for n be Nat holds p.n = 1_(L)*p.n by VECTSP_1:def 19;
hence thesis by Def3;
end;
theorem Th29:
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 Nat;
thus (0_.(L)).n = 0.L by POLYNOM3:28
.= v*0.L by VECTSP_1:36
.= v*(0_.(L)).n by POLYNOM3:28;
end;
hence thesis by Def3;
end;
theorem Th30:
for L be add-associative right_zeroed right_complementable right_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 right_unital
right-distributive (non empty doubleLoopStr);
let v be Element of L;
now let n be Nat;
per cases;
suppose A1: n=0;
hence <%v%>.n = v by ALGSEQ_1:def 6
.= v*1_(L) by VECTSP_1:def 13
.= v*(1_.(L)).n by A1,POLYNOM3:31;
suppose A2: n<>0;
then n > 0 by NAT_1:19;
then A3: n >= 0+1 by NAT_1:38;
len <%v%> <= 1 by ALGSEQ_1:def 6;
then n >= len <%v%> by A3,AXIOMS:22;
hence <%v%>.n = 0.L by ALGSEQ_1:22
.= v*0.L by VECTSP_1:36
.= v*(1_.(L)).n by A2,POLYNOM3:31;
end;
hence thesis by Def3;
end;
theorem Th31:
for L be add-associative right_zeroed right_complementable left_unital
distributive commutative associative Field-like (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 left_unital
distributive commutative associative Field-like (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 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 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,Th26;
then A7: dom F1 = dom F2 by FINSEQ_3:31;
now let i be set;
assume A8: i in dom F1;
then reconsider i1=i as Nat by FINSEQ_3:25;
A9: p.(i1-'1) * (power L).(x,i1-'1) = F1.i by A3,A8
.= F1/.i by A8,FINSEQ_4:def 4;
thus F2/.i = F2.i by A7,A8,FINSEQ_4:def 4
.= (v*p).(i1-'1) * (power L).(x,i1-'1) by A6,A7,A8
.= v*p.(i1-'1) * (power L).(x,i1-'1) by Def3
.= v*(F1/.i) by A9,VECTSP_1:def 16;
end;
then F2 = v*F1 by A7,POLYNOM1:def 2;
hence eval(v*p,x) = v*eval(p,x) by A1,A4,POLYNOM1:28;
suppose A10: v = 0.L;
hence eval(v*p,x) = eval(0_.(L),x) by Th27
.= 0.L by POLYNOM4:20
.= v*eval(p,x) by A10,VECTSP_1:39;
end;
theorem Th32:
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 Nat st n in dom F holds F.n = p.(n-'1) * (power L).(0.L,n-'1)
by POLYNOM4:def 2;
per cases by NAT_1:18;
suppose len F > 0;
then 0+1 <= len F by NAT_1:38;
then A4: 1 in dom F by FINSEQ_3:27;
now let i be Nat;
assume that
A5: i in dom F and
A6: i <> 1;
0+1 <= i by A5,FINSEQ_3:27;
then i > 0+1 by A6,REAL_1:def 5;
then i-1 > 0 by REAL_1:86;
then A7: i-'1 > 0 by BINARITH:def 3;
thus F/.i = F.i by A5,FINSEQ_4:def 4
.= p.(i-'1) * (power L).(0.L,i-'1) by A3,A5
.= p.(i-'1) * 0.L by A7,COMPTRIG:14
.= 0.L by VECTSP_1:36;
end;
hence eval(p,0.L) = F/.1 by A1,A4,POLYNOM2:5
.= F.1 by A4,FINSEQ_4:def 4
.= p.(1-'1) * (power L).(0.L,1-'1) by A3,A4
.= p.(1-'1) * (power L).(0.L,0) by GOBOARD9:1
.= p.(1-'1) * 1.L by GROUP_1:def 7
.= p.(1-'1) by GROUP_1:def 4
.= p.0 by GOBOARD9:1;
suppose len F = 0;
then A8: p = 0_.(L) by A2,POLYNOM4:8;
hence eval(p,0.L) = 0.L by POLYNOM4:20
.= p.0 by A8,POLYNOM3:28;
end;
definition
let L be non empty ZeroStr;
let z0,z1 be Element of L;
func <%z0,z1%> -> sequence of L equals :Def4:
0_.(L)+*(0,z0)+*(1,z1);
coherence by NORMSP_1:def 3;
end;
theorem Th33:
for L be non empty ZeroStr
for z0 be Element of L holds
<%z0%>.0 = z0 &
for n be 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 6;
let n be Nat;
assume A1: n >= 1;
len <%z0%> <= 1 by ALGSEQ_1:def 6;
then len <%z0%> <= n by A1,AXIOMS:22;
hence thesis by ALGSEQ_1:22;
end;
theorem Th34:
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 6;
then <%z0%> <> <%0.L%> by ALGSEQ_1:def 6;
then len <%z0%> <> 0 by ALGSEQ_1:31;
then len <%z0%> > 0 by NAT_1:19;
then A1: len <%z0%> >= 0+1 by NAT_1:38;
assume len <%z0%> <> 1;
then len <%z0%> > 1 by A1,REAL_1:def 5;
hence contradiction by ALGSEQ_1:def 6;
end;
theorem Th35:
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:31;
hence thesis by POLYNOM4:8;
end;
theorem Th36:
for L be add-associative right_zeroed right_complementable distributive
commutative associative left_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 left_unital domRing-like (non empty doubleLoopStr);
let x,y be Element of L;
A1: len <%x%> <= 1 & len <%y%> <= 1 by ALGSEQ_1:def 6;
per cases;
suppose A2: len <%x%> <> 0 & len <%y%> <> 0;
then len <%x%> > 0 & len <%y%> > 0 by NAT_1:19;
then len <%x%> >= 0+1 & len <%y%> >= 0+1 by NAT_1:38;
then Aa: len <%x%> = 1 & len <%y%> = 1 by A1,AXIOMS:21;
then <%x%>.(len <%x%> -'1) <> 0.L & <%y%>.(len <%y%> -'1) <> 0.L by LC1;
then <%x%>.(len <%x%> -'1)*<%y%>.(len <%y%> -'1)<>0.L by VECTSP_2:def 5;
then A3: len (<%x%>*'<%y%>) = 1+1-1 by Aa, POLYNOM4:13;
consider r be FinSequence of the carrier of L such that
A4: len r = 0+1 and
A5: (<%x%>*'<%y%>).0 = Sum r and
A6: for k be Nat st k in dom r holds r.k = <%x%>.(k-'1) * <%y%>.(0+1-'k)
by POLYNOM3:def 11;
1 in dom r by A4,FINSEQ_3:27;
then r.1 = <%x%>.(1-'1) * <%y%>.(0+1-'1) by A6
.= <%x%>.0 * <%y%>.(1-'1) by GOBOARD9:1
.= <%x%>.0 * <%y%>.0 by GOBOARD9:1
.= <%x%>.0 * y by ALGSEQ_1:def 6
.= x*y by ALGSEQ_1:def 6;
then A7: r = <*x*y*> by A4,FINSEQ_1:57;
A8: now let n be Nat;
assume n < 1;
then n < 0+1;
then n <= 0 by NAT_1:38;
then A9: n = 0 by NAT_1:18;
hence (<%x%>*'<%y%>).n = x*y by A5,A7,RLVECT_1:61
.= <%x*y%>.n by A9,ALGSEQ_1:def 6;
end;
x <> 0.L & y <> 0.L
proof
assume x = 0.L or y = 0.L;
then <%x%> = 0_.(L) or <%y%> = 0_.(L) by Th35;
hence contradiction by A2,POLYNOM4:6;
end;
then x*y <> 0.L by VECTSP_2:def 5;
then len <%x*y%> = 1 by Th34;
hence <%x%>*'<%y%> = <%x*y%> by A3,A8,ALGSEQ_1:28;
suppose A10: len <%x%> = 0;
then A11: <%x%> = 0_.(L) by POLYNOM4:8;
A12: x=0.L by A10,Th34;
thus <%x%>*'<%y%> = 0_.(L) by A11,POLYNOM4:5
.= <%0.L%> by Th35
.= <%x*y%> by A12,VECTSP_1:39;
suppose A13: len <%y%> = 0;
then A14: <%y%> = 0_.(L) by POLYNOM4:8;
A15: y=0.L by A13,Th34;
thus <%x%>*'<%y%> = 0_.(L) by A14,POLYNOM3:35
.= <%0.L%> by Th35
.= <%x*y%> by A15,VECTSP_1:39;
end;
theorem Th37:
for L be Abelian add-associative right_zeroed right_complementable
right_unital associative commutative distributive Field-like
(non empty doubleLoopStr)
for x be Element of L
for n be Nat holds
<%x%>`^n = <%(power L).(x,n)%>
proof
let L be Abelian add-associative right_zeroed right_complementable
right_unital associative commutative distributive Field-like
(non empty doubleLoopStr);
let x be Element of L;
defpred P[Nat] means <%x%>`^$1 = <%(power L).(x,$1)%>;
<%x%>`^0 = 1_.(L) by Th16
.= 1_(L)*1_.(L) by Th28
.= 1.L*1_.(L) by POLYNOM2:3
.= <%1.L%> by Th30
.= <%(power L).(x,0)%> by GROUP_1:def 7;
then A1: P[0];
A2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume <%x%>`^n = <%(power L).(x,n)%>;
hence <%x%>`^(n+1) = <%(power L).(x,n)%>*'<%x%> by Th20
.= <%(power L).(x,n)*x%> by Th36
.= <%(power L).(x,n+1)%> by GROUP_1:def 7;
end;
thus for n be Nat holds P[n] from Ind(A1,A2);
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 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 6;
per cases by A4,CQC_THE1:2;
suppose len F = 0;
then A5: <%z0%> = 0_.(L) by A2,POLYNOM4:8;
hence eval(<%z0%>,x) = 0.L by POLYNOM4:20
.= (0_.(L)).0 by POLYNOM3:28
.= z0 by A5,Th33;
suppose A6: len F = 1;
then 0+1 in Seg len F by FINSEQ_1:6;
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 GOBOARD9:1
.= <%z0%>.0 * (power L).(x,0) by GOBOARD9:1
.= z0 * (power L).(x,0) by Th33
.= z0 * 1.L by GROUP_1:def 7
.= z0 by GROUP_1:def 4;
then F = <*z0*> by A6,FINSEQ_1:57;
hence thesis by A1,RLVECT_1:61;
end;
theorem Th39:
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;
the carrier of L is non empty & 0 in NAT;
then A1: 0 in dom 0_.(L) by FUNCT_2:def 1;
the carrier of L is non empty & 1 in NAT;
then A2: 1 in dom (0_.(L)+*(0,z0)) by FUNCT_2:def 1;
thus <%z0,z1%>.0 = (0_.(L)+*(0,z0)+*(1,z1)).0 by Def4
.= (0_.(L)+*(0,z0)).0 by FUNCT_7:34
.= z0 by A1,FUNCT_7:33;
thus <%z0,z1%>.1 = (0_.(L)+*(0,z0)+*(1,z1)).1 by Def4
.= z1 by A2,FUNCT_7:33;
let n be Nat;
assume n >= 2;
then A3: n >= 1+1;
then A4: n > 0+1 by NAT_1:38;
A5: n > 0 by A3,NAT_1:38;
thus <%z0,z1%>.n = (0_.(L)+*(0,z0)+*(1,z1)).n by Def4
.= (0_.(L)+*(0,z0)).n by A4,FUNCT_7:34
.= (0_.(L)).n by A5,FUNCT_7:34
.= 0.L by POLYNOM3:28;
end;
definition
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;
assume n >= 2;
hence thesis by Th39;
end;
end;
theorem Th40:
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%>
proof
let n be Nat;
assume n >= 2;
hence <%z0,z1%>.n = 0.L by Th39;
end;
hence thesis by ALGSEQ_1:def 4;
end;
theorem Th41:
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 A1: <%z0,z1%>.1 <> 0.L by Th39;
A2: 2 is_at_least_length_of <%z0,z1%>
proof
let n be Nat;
assume n >= 2;
hence <%z0,z1%>.n = 0.L by Th39;
end;
now let n be Nat;
assume n is_at_least_length_of <%z0,z1%>;
then 1 < n by A1,ALGSEQ_1:def 3;
hence 1+1 <= n by NAT_1:38;
end;
hence thesis by A2,ALGSEQ_1:def 4;
end;
theorem Th42:
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;
assume z0 <> 0.L;
then A1: <%z0,0.L%>.0 <> 0.L by Th39;
A2: 1 is_at_least_length_of <%z0,0.L%>
proof
let n be Nat;
assume A3: n >= 1;
per cases by A3,REAL_1:def 5;
suppose n = 1;
hence <%z0,0.L%>.n = 0.L by Th39;
suppose n > 1;
then n >= 1+1 by NAT_1:38;
hence <%z0,0.L%>.n = 0.L by Th39;
end;
now let n be Nat;
assume n is_at_least_length_of <%z0,0.L%>;
then 0 < n by A1,ALGSEQ_1:def 3;
hence 0+1 <= n by NAT_1:38;
end;
hence thesis by A2,ALGSEQ_1:def 4;
end;
theorem Th43:
for L be non empty ZeroStr holds
<%0.L,0.L%> = 0_.(L)
proof
let L be non empty ZeroStr;
A1: 0 is_at_least_length_of <%0.L,0.L%>
proof
let n be Nat;
assume A2: n >= 0;
per cases by A2;
suppose n = 0;
hence <%0.L,0.L%>.n = 0.L by Th39;
suppose n > 0;
then A3: n >= 0+1 by NAT_1:38;
now per cases by A3,REAL_1:def 5;
suppose n = 1;
hence <%0.L,0.L%>.n = 0.L by Th39;
suppose n > 1;
then n >= 1+1 by NAT_1:38;
hence <%0.L,0.L%>.n = 0.L by Th39;
end;
hence <%0.L,0.L%>.n = 0.L;
end;
for n be Nat st n is_at_least_length_of <%0.L,0.L%> holds 0 <= n
by NAT_1:18;
then len <%0.L,0.L%> = 0 by A1,ALGSEQ_1:def 4;
hence thesis by POLYNOM4:8;
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 Th43
.= <%z0%> by A1,Th35;
suppose A2: z0 <> 0.L;
then A3: len <%z0%> = 0+1 by Th34;
A4: len <%z0,0.L%> = 1 by A2,Th42;
now let n be Nat;
assume n < len <%z0%>;
then n <= 0 by A3,NAT_1:38;
then A5: n = 0 by NAT_1:19;
hence <%z0,0.L%>.n = z0 by Th39
.= <%z0%>.n by A5,ALGSEQ_1:def 6;
end;
hence thesis by A3,A4,ALGSEQ_1:28;
end;
theorem Th45:
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 Nat st n in dom F holds
F.n = <%z0,z1%>.(n-'1) * (power L).(x,n-'1) by POLYNOM4:def 2;
A4: len F <= 2 by A2,Th40;
per cases by A4,CQC_THE1:3;
suppose len F = 0;
then A5: <%z0,z1%> = 0_.(L) by A2,POLYNOM4:8;
hence eval(<%z0,z1%>,x) = 0.L by POLYNOM4:20
.= (0_.(L)).0 by POLYNOM3:28
.= z0 by A5,Th39
.= z0 + 0.L by RLVECT_1:def 7
.= z0 + 0.L*x by VECTSP_1:39
.= z0 + (0_.(L)).1*x by POLYNOM3:28
.= z0 + z1*x by A5,Th39;
suppose A6: len F = 1;
then 0+1 in Seg len F by FINSEQ_1:6;
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 GOBOARD9:1
.= <%z0,z1%>.0 * (power L).(x,0) by GOBOARD9:1
.= z0 * (power L).(x,0) by Th39
.= z0 * 1.L by GROUP_1:def 7
.= z0 by GROUP_1:def 4;
then F = <*z0*> by A6,FINSEQ_1:57;
hence eval(<%z0,z1%>,x) = z0 by A1,RLVECT_1:61
.= z0 + 0.L by RLVECT_1:def 7
.= z0 + 0.L*x by VECTSP_1:39
.= z0 + <%z0,z1%>.1*x by A2,A6,ALGSEQ_1:22
.= z0 + z1*x by Th39;
suppose A7: len F = 2;
then A8: 1 in dom F & 2 in dom F by FINSEQ_3:27;
then A9: F.1 = <%z0,z1%>.(1-'1) * (power L).(x,1-'1) by A3
.= <%z0,z1%>.0 * (power L).(x,1-'1) by GOBOARD9:1
.= <%z0,z1%>.0 * (power L).(x,0) by GOBOARD9:1
.= z0 * (power L).(x,0) by Th39
.= z0 * 1.L by GROUP_1:def 7
.= z0 by GROUP_1:def 4;
A10: 2-'1 = 2-1 by BINARITH:def 3;
F.2 = <%z0,z1%>.(2-'1) * (power L).(x,2-'1) by A3,A8
.= z1 * (power L).(x,1) by A10,Th39
.= z1 * x by COMPTRIG:12;
then F = <*z0,z1*x*> by A7,A9,FINSEQ_1:61;
hence thesis by A1,RLVECT_1:62;
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(<%z0,0.L%>,x) = z0
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(<%z0,0.L%>,x) = z0+0.L*x by Th45
.= z0+0.L by VECTSP_1:39
.= z0 by RLVECT_1:def 7;
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 Th45
.= z1*x by RLVECT_1:10;
end;
theorem Th48:
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 Th45
.= z0+x by VECTSP_1:def 19;
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 Th45
.= 0.L+x by VECTSP_1:def 19
.= x by RLVECT_1:10;
end;
begin :: Substitution in Polynomials
definition
let L be Abelian add-associative right_zeroed right_complementable
right_unital commutative distributive (non empty doubleLoopStr);
let p,q be Polynomial of L;
func Subst(p,q) -> Polynomial of L means :Def5:
ex F be FinSequence of the carrier of Polynom-Ring L st
it = Sum F &
len F = len p &
for n be Nat st n in dom F holds F.n = p.(n-'1)*(q`^(n-'1));
existence
proof
set k = len p;
defpred P[Nat,set] means $2 = p.($1-'1)*(q`^($1-'1));
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 12;
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 and
A3: for n be Nat st n in Seg k holds P[n,F.n] from SeqDEx(A1);
reconsider r=Sum F as Polynomial of L by POLYNOM3:def 12;
take r,F;
thus thesis by A2,A3,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
A4: y1 = Sum F1 and
A5: len F1 = len p and
A6: for n be 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
A7: y2 = Sum F2 and
A8: len F2 = len p and
A9: for n be Nat st n in dom F2 holds F2.n = p.(n-'1)*(q`^(n-'1));
now let n be Nat;
assume n in Seg len F1;
then A10: n in dom F1 & n in dom F2 by A5,A8,FINSEQ_1:def 3;
hence F1.n = p.(n-'1)*(q`^(n-'1)) by A6
.= F2.n by A9,A10;
end;
hence y1 = y2 by A4,A5,A7,A8,FINSEQ_2:10;
end;
end;
theorem Th50:
for L be Abelian add-associative right_zeroed right_complementable
right_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
right_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 Nat st n in dom F holds F.n = (0_.(L)).(n-'1)*(p`^(n-'1))
by Def5;
now let n be Nat;
assume n in dom F;
hence F.n = (0_.(L)).(n-'1)*(p`^(n-'1)) by A2
.= 0.L*(p`^(n-'1)) by POLYNOM3:28
.= 0_.(L) by Th27
.= 0.(Polynom-Ring L) by POLYNOM3:def 12;
end;
hence Subst(0_.(L),p) = 0.(Polynom-Ring L) by A1,POLYNOM3:1
.= 0_.(L) by POLYNOM3:def 12;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
right_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
right_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 Nat st n in dom F holds F.n = p.(n-'1)*((0_.(L))`^(n-'1))
by Def5;
per cases;
suppose len F <> 0;
then len F > 0 by NAT_1:19;
then 0+1 <= len F by NAT_1:38;
then A4: 1 in dom F by FINSEQ_3:27;
now let n be Nat;
assume that
A5: n in dom F and
A6: n <> 1;
n >= 1 by A5,FINSEQ_3:27;
then A7: n > 0+1 by A6,REAL_1:def 5;
then n >= 1+1 by NAT_1:38;
then A8: n-2 >= 1+1-2 by REAL_1:49;
n-1 >= 0 by A7,REAL_1:84;
then A9: n-'1 = n-1 by BINARITH:def 3
.= n-1+-1+1 by XCMPLX_1:139
.= n-1-1+1 by XCMPLX_0:def 8
.= n-(1+1)+1 by XCMPLX_1:36
.= n-'2+1 by A8,BINARITH:def 3;
thus F/.n = F.n by A5,FINSEQ_4:def 4
.= p.(n-'1)*((0_.(L))`^(n-'1)) by A3,A5
.= p.(n-'1)*(0_.(L)) by A9,Th21
.= 0_.(L) by Th29
.= 0.(Polynom-Ring L) by POLYNOM3:def 12;
end;
hence Subst(p,0_.(L)) = F/.1 by A1,A4,POLYNOM2:5
.= F.1 by A4,FINSEQ_4:def 4
.= p.(1-'1)*((0_.(L))`^(1-'1)) by A3,A4
.= p.(1-'1)*((0_.(L))`^0) by GOBOARD9:1
.= p.0*((0_.(L))`^0) by GOBOARD9:1
.= p.0*(1_.(L)) by Th16
.= <%p.0%> by Th30;
suppose len F = 0;
then A10: p = 0_.(L) by A2,POLYNOM4:8;
hence Subst(p,0_.(L)) = 0_.(L) by Th50
.= <%0.L%> by Th35
.= <%p.0%> by A10,POLYNOM3:28;
end;
theorem
for L be Abelian add-associative right_zeroed right_complementable
right_unital associative commutative distributive Field-like
(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
right_unital associative commutative distributive Field-like
(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 Nat st n in dom F holds F.n = p.(n-'1)*(<%x%>`^(n-'1))
by Def5;
defpred P[Nat] means for p be Polynomial of L st p = Sum(F|$1) holds
len p <= 1;
A3: P[0]
proof
let p be Polynomial of L;
assume A4: p = Sum(F|0);
F|0 = <*>the carrier of Polynom-Ring L;
then p = 0.(Polynom-Ring L) by A4,RLVECT_1:60
.= 0_.(L) by POLYNOM3:def 12;
then len p = 0 by POLYNOM4:6;
hence len p <= 1;
end;
A5: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A6: for q be Polynomial of L st q = Sum(F|n) holds len q <= 1;
let q be Polynomial of L;
assume A7: q = Sum(F|(n+1));
reconsider F1 = Sum(F|n) as Polynomial of L by POLYNOM3:def 12;
reconsider maxFq = max(len F1,len (p.n*(<%x%>`^n))) as Nat
by FINSEQ_2:1;
A8: len F1 <= 1 by A6;
len (p.n*(<%x%>`^n)) <= 1
proof
per cases;
suppose p.n <> 0.L;
then len (p.n*(<%x%>`^n)) = len (<%x%>`^n) by Th26
.= len <%(power L).(x,n)%> by Th37;
hence len (p.n*(<%x%>`^n)) <= 1 by ALGSEQ_1:def 6;
suppose p.n = 0.L;
then len(p.n*(<%x%>`^n)) = 0 by Th25;
hence len (p.n*(<%x%>`^n)) <= 1;
end;
then A9: maxFq <= 1 by A8,SQUARE_1:50;
A10: maxFq >= len F1 & maxFq >= len (p.n*(<%x%>`^n)) by SQUARE_1:46;
now per cases;
suppose A11: n+1 <= len F;
n+1 >= 1 by NAT_1:29;
then A12: n+1 in dom F by A11,FINSEQ_3:27;
then A13: F/.(n+1) = F.(n+1) by FINSEQ_4:def 4
.= p.(n+1-'1)*(<%x%>`^(n+1-'1)) by A2,A12
.= p.n*(<%x%>`^(n+1-'1)) by BINARITH:39
.= p.n*(<%x%>`^n) by BINARITH:39;
F|(n+1) = F|n ^ <*F/.(n+1)*> by A11,JORDAN8:2;
then q = Sum(F|n) + F/.(n+1) by A7,FVSUM_1:87
.= F1 + p.n*(<%x%>`^n) by A13,POLYNOM3:def 12;
then len q <= maxFq by A10,POLYNOM4:9;
hence len q <= 1 by A9,AXIOMS:22;
suppose A14: n+1 > len F;
then n >= len F by NAT_1:38;
then F|n = F & F|(n+1) = F by A14,TOPREAL1:2;
hence len q <= 1 by A6,A7;
end;
hence len q <= 1;
end;
A15: for n be Nat holds P[n] from Ind(A3,A5);
F|(len F) = F by TOPREAL1:2;
hence len Subst(p,<%x%>) <= 1 by A1,A15;
end;
hence len Subst(p,<%x%>) <= 1;
end;
hence thesis;
end;
theorem Th53:
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;
A3: len q <> 0 by A2;
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 Nat st n in dom F holds F.n = p.(n-'1)*(q`^(n-'1))
by Def5;
len p * len q - len p - len q + 1 >= 0 by A1,A3,Th1;
then reconsider k = len p * len q - len p - len q + 1 as Nat by INT_1:16;
len F > 0 by A1,A5,NAT_1:19;
then A7: 0+1 <= len F by NAT_1:38;
then A8: 1 in dom F by FINSEQ_3:27;
defpred P[Nat] means for F1 be Polynomial of L st F1 = Sum(F|$1) holds
len F1 <= len (q`^($1-'1));
A9: P[1]
proof
let F1 be Polynomial of L;
assume A10: F1 = Sum(F|1);
F is non empty by A1,A5,FINSEQ_1:25;
then F|1 = <*F/.1*> by FINSEQ_5:23;
then Sum(F|1) = F/.1 by RLVECT_1:61
.= F.1 by A8,FINSEQ_4:def 4
.= p.(1-'1)*(q`^(1-'1)) by A6,A8
.= p.0*(q`^(1-'1)) by GOBOARD9:1
.= p.0*(q`^0) by GOBOARD9:1
.= p.0*(1_.(L)) by Th16
.= <%p.0%> by Th30;
then len F1 <= 1 by A10,ALGSEQ_1:def 6;
then len F1 <= len (1_.(L)) by POLYNOM4:7;
then len F1 <= len (q`^0) by Th16;
hence len F1 <= len (q`^(1-'1)) by GOBOARD9:1;
end;
A11: for n be non empty Nat st P[n] holds P[n+1]
proof
let n be non empty Nat;
assume A12: for F1 be Polynomial of L st F1 = Sum(F|n) holds
len F1 <= len (q`^(n-'1));
let F1 be Polynomial of L;
assume A13: F1 = Sum(F|(n+1));
reconsider F2 = Sum(F|n) as Polynomial of L by POLYNOM3:def 12;
n > 0 by NAT_1:19;
then n >= 0+1 by NAT_1:38;
then A14: n-1 >=0 by REAL_1:84;
len q > 0 by A3,NAT_1:19;
then len q >= 0+1 by NAT_1:38;
then A15: len q-1 >=0 by REAL_1:84;
A16: len(q`^(n-'1)) = (n-'1)*len q-(n-'1)+1 by A3,Th24
.= (n-1)*len q-(n-'1)+1 by A14,BINARITH:def 3
.= (n-1)*len q-(n-1)+1 by A14,BINARITH:def 3
.= n*len q-1*len q-(n-1)+1 by XCMPLX_1:40
.= n*len q-len q-n+1+1 by XCMPLX_1:37;
n*len q+(len q-'1) >= n*len q by NAT_1:29;
then n*len q-(len q-'1) <= n*len q by REAL_1:86;
then n*len q-(len q-1) <= n*len q by A15,BINARITH:def 3;
then n*len q-len q+1 <= n*len q by XCMPLX_1:37;
then n*len q-len q+1-n <= n*len q-n by REAL_1:49;
then n*len q-len q-n+1 <= n*len q-n by XCMPLX_1:29;
then n*len q-len q-n+1+1 <= n*len q-n+1 by AXIOMS:24;
then A17: len (q`^(n-'1)) <= len (q`^n) by A3,A16,Th24;
per cases;
suppose A18: n+1 <= len F;
n+1 >= 1 by NAT_1:29;
then A19: n+1 in dom F by A18,FINSEQ_3:27;
F|(n+1) = F|n ^ <*F/.(n+1)*> by A18,JORDAN8:2;
then A20: F1 = Sum(F|n) + F/.(n+1) by A13,FVSUM_1:87;
reconsider maxFq = max(len F2,len (p.n*(q`^n))) as Nat by FINSEQ_2:1;
A21: maxFq >= len F2 & maxFq >= len (p.n*(q`^n)) by SQUARE_1:46;
F/.(n+1) = F.(n+1) by A19,FINSEQ_4:def 4
.= p.(n+1-'1)*(q`^(n+1-'1)) by A6,A19
.= p.n*(q`^(n+1-'1)) by BINARITH:39
.= p.n*(q`^n) by BINARITH:39;
then F1 = F2 + p.n*(q`^n) by A20,POLYNOM3:def 12;
then A22: len F1 <= maxFq by A21,POLYNOM4:9;
len F2 <= len (q`^(n-'1)) by A12;
then A23: len F2 <= len (q`^n) by A17,AXIOMS:22;
len (p.n*(q`^n)) <= len (q`^n)
proof
per cases;
suppose p.n <> 0.L;
hence len (p.n*(q`^n)) <= len (q`^n) by Th26;
suppose p.n = 0.L;
then len(p.n*(q`^n)) = 0 by Th25;
hence len (p.n*(q`^n)) <= len (q`^n) by NAT_1:18;
end;
then maxFq <= len (q`^n) by A23,SQUARE_1:50;
then len F1 <= len (q`^n) by A22,AXIOMS:22;
hence len F1 <= len (q`^(n+1-'1)) by BINARITH:39;
suppose A24: n+1 > len F;
then n >= len F by NAT_1:38;
then F|n = F & F|(n+1) = F by A24,TOPREAL1:2;
then len F1 <= len (q`^(n-'1)) by A12,A13;
then len F1 <= len (q`^n) by A17,AXIOMS:22;
hence len F1 <= len (q`^(n+1-'1)) by BINARITH:39;
end;
A25: for n be non empty Nat holds P[n] from Ind_from_1(A9,A11);
len p > 0 by A1,NAT_1:19;
then len p >= 0+1 by NAT_1:38;
then A26: len p-1 >=0 by REAL_1:84;
F|len F = F by TOPREAL1:2;
then A27: len Subst(p,q) <= len (q`^(len F-'1)) by A1,A4,A5,A25;
A28: len (q`^(len F-'1)) = (len p-'1)*len q - (len p-'1) + 1 by A3,A5,Th24
.= (len p-'1)*len q-(len p-1)+1 by A26,BINARITH:def 3
.= (len p-1)*len q-(len p-1)+1 by A26,BINARITH:def 3
.= (len p)*(len q)-1*len q-(len p-1)+1 by XCMPLX_1:40
.= (len p)*(len q)-len q-len p+1+1 by XCMPLX_1:37
.= (len p)*(len q)-len p-len q+1+1 by XCMPLX_1:21
.= (len p)*(len q)-len p-len q+(1+1) by XCMPLX_1:1;
len Subst(p,q) >= (len p)*(len q)-len p-len q+(1+1)
proof
assume A29: len Subst(p,q) < (len p)*(len q)-len p-len q+(1+1);
then len Subst(p,q) < k+1 by XCMPLX_1:1;
then len Subst(p,q) <= k by NAT_1:38;
then A30: Subst(p,q).k = 0.L by ALGSEQ_1:22;
set lF1 = len F-'1;
set F1 = F|lF1;
reconsider sF1 = Sum F1 as Polynomial of L by POLYNOM3:def 12;
A31: len F = lF1+1 by A7,AMI_5:4;
then A32: F = F1^<*F/.len F*> by FINSEQ_5:24;
then A33: Sum F = Sum F1 + F/.len F by FVSUM_1:87;
A34: len F = len F1 + 1 by A32,FINSEQ_2:19;
then A35: len F1 = len F - 1 by XCMPLX_1:26;
now per cases;
suppose A36: len F1 <> {};
then len F1 > 0 by NAT_1:19;
then 0+1 <= len F1 by NAT_1:38;
then A37: 1 in dom F1 by FINSEQ_3:27;
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;
A38: P[1]
proof
let F2 be Polynomial of L;
assume A39: F2 = Sum(F1|1);
F1 is non empty by A36,FINSEQ_1:25;
then F1|1 = <*F1/.1*> by FINSEQ_5:23;
then Sum(F1|1) = F1/.1 by RLVECT_1:61
.= F1.1 by A37,FINSEQ_4:def 4
.= F.1 by A32,A37,FINSEQ_1:def 7
.= p.(1-'1)*(q`^(1-'1)) by A6,A8
.= p.0*(q`^(1-'1)) by GOBOARD9:1
.= p.0*(q`^0) by GOBOARD9:1
.= p.0*(1_.(L)) by Th16
.= <%p.0%> by Th30;
then len F2 <= 0-1+2 by A39,ALGSEQ_1:def 6;
hence len F2 <= 1*len q-len q-1+2 by XCMPLX_1:14;
end;
A40: for n be non empty Nat st P[n] holds P[n+1]
proof
let n be non empty Nat;
assume A41: for F2 be Polynomial of L st F2 = Sum(F1|n) holds
len F2 <= n*len q-len q-n+2;
let F2 be Polynomial of L;
assume A42: F2 = Sum(F1|(n+1));
reconsider F3 = Sum(F1|n) as Polynomial of L by POLYNOM3:def 12;
A43: len F3 <= n*len q-len q-n+2 by A41;
A44: n*len q-len q-n+2+0 <= n*len q-len q-n+2+1 by AXIOMS:24;
len q >= 0+(1+1) by A2,NAT_1:38;
then len q-2 >= 0 by REAL_1:84;
then n*len q-n+1+0 <= n*len q-n+1+(len q-2) by REAL_1:55;
then n*len q-n+1-(len q-2) <= n*len q-n+1 by REAL_1:86;
then n*len q-n+1-len q+2 <= n*len q-n+1 by XCMPLX_1:37;
then n*len q-n-len q+1+2 <= n*len q-n+1 by XCMPLX_1:29;
then n*len q-len q-n+1+2 <= n*len q-n+1 by XCMPLX_1:21;
then n*len q-len q-n+2+1 <= n*len q-n+1 by XCMPLX_1:1;
then n*len q-len q-n+2 <= n*len q-n+1 by A44,AXIOMS:22;
then A45: len F3 <= n*len q-n+1 by A43,AXIOMS:22;
now per cases;
suppose A46: n+1 <= len F1;
A47: n+1 >= 1 by NAT_1:29;
then A48: n+1 in dom F1 by A46,FINSEQ_3:27;
len F1 <= len F by A34,NAT_1:29;
then n+1 <= len F by A46,AXIOMS:22;
then A49: n+1 in dom F by A47,FINSEQ_3:27;
A50: F1/.(n+1) = F1.(n+1) by A48,FINSEQ_4:def 4
.= F.(n+1) by A32,A48,FINSEQ_1:def 7
.= p.(n+1-'1)*(q`^(n+1-'1)) by A6,A49
.= p.n*(q`^(n+1-'1)) by BINARITH:39
.= p.n*(q`^n) by BINARITH:39;
reconsider maxFq = max(len F3,len (p.n*(q`^n))) as Nat by FINSEQ_2:1;
A51: maxFq >= len F3 & maxFq >= len (p.n*(q`^n)) by SQUARE_1:46;
F1|(n+1) = F1|n ^ <*F1/.(n+1)*> by A46,JORDAN8:2;
then F2 = Sum(F1|n) + F1/.(n+1) by A42,FVSUM_1:87
.= F3 + p.n*(q`^n) by A50,POLYNOM3:def 12;
then A52: len F2 <= maxFq by A51,POLYNOM4:9;
len (p.n*(q`^n)) <= n*len q-n+1
proof
per cases;
suppose p.n <> 0.L;
then len (p.n*(q`^n)) = len (q`^n) by Th26;
hence len (p.n*(q`^n)) <= n*len q-n+1 by A3,Th24;
suppose p.n = 0.L;
then A53: len (p.n*(q`^n)) = 0 by Th25;
A54: n >= 0 by NAT_1:18;
len q > 0 by A3,NAT_1:19;
then len q >= 0+1 by NAT_1:38;
then len q-1 >= 0 by REAL_1:84;
then n*(len q-1) >= 0 by A54,REAL_2:121;
then A55: n*len q-n*1 >= 0 by XCMPLX_1:40;
n*len q <= n*len q+1 by NAT_1:29;
then n*len q-n <= n*len q+1-n by REAL_1:49;
hence len (p.n*(q`^n)) <= n*len q-n+1 by A53,A55,XCMPLX_1:29;
end;
then maxFq <= n*len q-n+1 by A45,SQUARE_1:50;
then len F2 <= n*len q-n+(2-1) by A52,AXIOMS:22;
then len F2 <= n*len q-n+2-1 by XCMPLX_1:29;
then len F2 <= n*len q-n-1+2 by XCMPLX_1:29;
then len F2 <= n*len q-(n+1)+2 by XCMPLX_1:36;
then len F2 <= n*len q+1*len q-len q-(n+1)+2 by XCMPLX_1:26;
hence len F2 <= (n+1)*len q-len q-(n+1)+2 by XCMPLX_1:8;
suppose A56: n+1 > len F1;
then n >= len F1 by NAT_1:38;
then F1|n = F1 & F1|(n+1) = F1 by A56,TOPREAL1:2;
then A57: len F2 <= n*len q-len q-n+2 by A41,A42;
-len q <= -1 by A2,REAL_1:50;
then n*len q-n+-len q <= n*len q-n+-1 by AXIOMS:24;
then n*len q-n-len q <= n*len q-n+-1 by XCMPLX_0:def 8;
then n*len q-n-len q <= n*len q-n-1 by XCMPLX_0:def 8;
then n*len q-len q-n <= n*len q-n-1 by XCMPLX_1:21;
then n*len q-len q-n <= n*len q-(n+1) by XCMPLX_1:36;
then n*len q-len q-n <= n*len q+1*len q-len q-(n+1) by XCMPLX_1:26;
then n*len q-len q-n <= (n+1)*len q-len q-(n+1) by XCMPLX_1:8;
then n*len q-len q-n+2 <= (n+1)*len q-len q-(n+1)+2 by AXIOMS:24;
hence len F2 <= (n+1)*len q-len q-(n+1)+2 by A57,AXIOMS:22;
end;
hence len F2 <= (n+1)*len q-len q-(n+1)+2;
end;
A58: for n be non empty Nat holds P[n] from Ind_from_1(A38,A40);
F1|(len F1) = F1 by TOPREAL1:2;
then len sF1 <= (len F1)*(len q)-len q-len F1+2 by A36,A58;
then len sF1 <= (len p)*(len q)-1*len q-len q-(len p-1)+2
by A5,A35,XCMPLX_1:40;
then len sF1 <= (len p)*(len q)-len q-(len p-1)-len q+2 by XCMPLX_1:21;
then len sF1 <= (len p)*(len q)-len q-len p+1-len q+2 by XCMPLX_1:37;
then A59: len sF1 <= k-len q+2 by XCMPLX_1:21;
0+len q >= 1+1 by A2,NAT_1:38;
then 2-len q <= 0 by REAL_1:86;
then 2-len q+k <= 0+k by AXIOMS:24;
then k+2-len q <= k by XCMPLX_1:29;
then k-len q+2 <= k by XCMPLX_1:29;
then k >= len sF1 by A59,AXIOMS:22;
then A60: sF1.k = 0.L by ALGSEQ_1:22;
A61: len F in dom F by A7,FINSEQ_3:27;
then F/.len F = F.len F by FINSEQ_4:def 4
.= p.lF1*(q`^lF1) by A6,A61;
then Subst(p,q) = sF1 + p.lF1*(q`^lF1) by A4,A33,POLYNOM3:def 12;
then A62: Subst(p,q).k = sF1.k + (p.lF1*(q`^lF1)).k by POLYNOM3:def 6
.= (p.lF1*(q`^lF1)).k by A60,RLVECT_1:def 7
.= p.lF1*((q`^lF1).k) by Def3;
A63: p.lF1 <> 0.L by A5,A31,ALGSEQ_1:25;
len (q`^lF1) = k+1 by A28,XCMPLX_1:1;
then (q`^lF1).k <> 0.L by ALGSEQ_1:25;
hence contradiction by A30,A62,A63,VECTSP_1:44;
suppose A64: len F1 = {};
then A65: F1 = <*>(the carrier of Polynom-Ring L)
by FINSEQ_1:32;
A66: len F = 0+1 by A32,A64,FINSEQ_2:19;
A67: F/.1 = F.1 by A8,FINSEQ_4:def 4
.= p.(1-'1)*(q`^(1-'1)) by A6,A8
.= p.0*(q`^(1-'1)) by GOBOARD9:1
.= p.0*(q`^0) by GOBOARD9:1
.= p.0*(1_.(L)) by Th16
.= <%p.0%> by Th30;
A68: 0.(Polynom-Ring L) = 0_.(L) by POLYNOM3:def 12;
A69: Sum F = 0.(Polynom-Ring L) + F/.1 by A33,A65,A66,RLVECT_1:60
.= 0_.(L) + <%p.0%> by A67,A68,POLYNOM3:def 12
.= <%p.0%> by POLYNOM3:29;
p.0 <> 0.L by A5,A66,ALGSEQ_1:25;
then len Subst(p,q) = 1 by A4,A69,Th34;
then 1 < len q-len q-1+(1+1) by A5,A29,A66,XCMPLX_1:21;
then 1 < 0-1+(1+1) by XCMPLX_1:14;
hence contradiction;
end;
hence contradiction;
end;
hence thesis by A27,A28,AXIOMS:21;
end;
theorem Th54:
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 F be FinSequence of the carrier of Polynom-Ring L such that
A1: Subst(p,q) = Sum F and
A2: len F = len p and
A3: for n be Nat st n in dom F holds F.n = p.(n-'1)*(q`^(n-'1))
by Def5;
consider F1 be FinSequence of the carrier of L such that
A4: eval(p,eval(q,x)) = Sum F1 and
A5: len F1 = len p and
A6: for n be Nat st n in dom F1 holds
F1.n = p.(n-'1)*(power L).(eval(q,x),n-'1) by POLYNOM4:def 2;
defpred P[Nat] means for r be Polynomial of L st r = Sum(F|$1) holds
eval(r,x) = Sum(F1|$1);
A7: P[0]
proof
let r be Polynomial of L;
assume A8: r = Sum(F|0);
A9: F|0 = <*>the carrier of Polynom-Ring L &
F1|0 = <*>the carrier of L;
then r = 0.(Polynom-Ring L) by A8,RLVECT_1:60
.= 0_.(L) by POLYNOM3:def 12;
hence eval(r,x) = 0.L by POLYNOM4:20
.= Sum(F1|0) by A9,RLVECT_1:60;
end;
A10: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A11: 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 A12: r = Sum(F|(n+1));
per cases;
suppose A13: n+1 <= len F;
n+1 >= 1 by NAT_1:29;
then A14: n+1 in dom F by A13,FINSEQ_3:27;
A15: dom F = dom F1 by A2,A5,FINSEQ_3:31;
reconsider r1 = Sum(F|n) as Polynomial of L by POLYNOM3:def 12;
F|(n+1) = F|n ^ <*F/.(n+1)*> by A13,JORDAN8:2;
then A16: r = Sum(F|n) + F/.(n+1) by A12,FVSUM_1:87;
A17: p.(n+1-'1)*(power L).(eval(q,x),n+1-'1) = F1.(n+1) by A6,A14,A15
.= F1/.(n+1) by A14,A15,FINSEQ_4:def 4;
A18: F1|(n+1) = F1|n ^ <*F1/.(n+1)*> by A2,A5,A13,JORDAN8:2;
F/.(n+1) = F.(n+1) by A14,FINSEQ_4:def 4
.= p.(n+1-'1)*(q`^(n+1-'1)) by A3,A14
.= p.n*(q`^(n+1-'1)) by BINARITH:39
.= p.n*(q`^n) by BINARITH:39;
then r = r1 + p.n*(q`^n) by A16,POLYNOM3:def 12;
hence eval(r,x) = eval(r1,x) + eval(p.n*(q`^n),x) by POLYNOM4:22
.= Sum(F1|n) + eval(p.n*(q`^n),x) by A11
.= Sum(F1|n) + p.n*eval(q`^n,x) by Th31
.= Sum(F1|n) + p.n*(power L).(eval(q,x),n) by Th23
.= Sum(F1|n) + p.(n+1-'1)*(power L).(eval(q,x),n) by BINARITH:39
.= Sum(F1|n) + F1/.(n+1) by A17,BINARITH:39
.= Sum(F1|(n+1)) by A18,FVSUM_1:87;
suppose A19: n+1 > len F;
then n >= len F by NAT_1:38;
then F|n = F & F|(n+1) = F & F1|n = F1 & F1|(n+1) = F1
by A2,A5,A19,TOPREAL1:2;
hence eval(r,x) = Sum(F1|(n+1)) by A11,A12;
end;
A20: for n be Nat holds P[n] from Ind(A7,A10);
F|(len F) = F & F1|(len F1) = F1 by TOPREAL1:2;
hence thesis by A1,A2,A4,A5,A20;
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 :Def6:
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 :Def7:
ex x be Element of L st x is_a_root_of p;
end;
theorem Th55:
for L be unital (non empty doubleLoopStr) holds
0_.(L) is with_roots
proof
let L be unital (non empty doubleLoopStr);
consider x be Element of L;
take x;
thus eval(0_.(L),x) = 0.L by POLYNOM4:20;
end;
definition
let L be unital (non empty doubleLoopStr);
cluster 0_.(L) -> with_roots;
coherence by Th55;
end;
theorem
for L be unital (non empty doubleLoopStr)
for x be Element of L holds
x is_a_root_of 0_.(L)
proof
let L be unital (non empty doubleLoopStr);
let x be Element of L;
thus eval(0_.(L),x) = 0.L by POLYNOM4:20;
end;
definition
let L be unital (non empty doubleLoopStr);
cluster with_roots 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 :Def8:
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 :Def9:
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 set;
assume y in {x where x is Element of L : x is_a_root_of p}
;
then consider x be Element of L such that
A1: x = y and
x is_a_root_of p;
thus y in the carrier of L by A1;
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 consider y be Element of L such that
A2: x = y and
A3: y is_a_root_of p;
thus x is_a_root_of p by A2,A3;
end;
assume x is_a_root_of p;
hence x in X;
end;
uniqueness
proof
let X1,X2 be Subset of L such that
A4: for x be Element of L holds
x in X1 iff x is_a_root_of p and
A5: for x be Element of L holds
x in X2 iff x is_a_root_of p;
thus X1 c= X2
proof
let x be set;
assume A6: x in X1;
then reconsider y=x as Element of L;
y is_a_root_of p by A4,A6;
hence x in X2 by A5;
end;
let x be set;
assume A7: x in X2;
then reconsider y=x as Element of L;
y is_a_root_of p by A5,A7;
hence x in X1 by A4;
end;
end;
definition
let L be commutative associative left_unital distributive Field-like
(non empty doubleLoopStr);
let p be Polynomial of L;
func NormPolynomial(p) -> sequence of L means :Def10:
for n be Nat holds it.n = p.n / p.(len p-'1);
existence
proof
deffunc F(Nat) = p.$1 / p.(len p-'1);
consider q be sequence of L such that
A1: for n be Nat holds q.n = F(n) from ExDdoubleLoopStrSeq;
take q;
thus thesis by A1;
end;
uniqueness
proof
let p1,p2 be sequence of L such that
A2: for n be Nat holds p1.n = p.n / p.(len p-'1) and
A3: for n be Nat holds p2.n = p.n / p.(len p-'1);
now let n be Nat;
thus p1.n = p.n / p.(len p-'1) by A2
.= p2.n by A3;
end;
hence p1 = p2 by FUNCT_2:113;
end;
end;
definition
let L be add-associative right_zeroed right_complementable commutative
associative left_unital distributive Field-like (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;
thus (NormPolynomial(p)).n = p.n / p.(len p-'1) by Def10
.= 0.L / p.(len p-'1) by A1,ALGSEQ_1:22
.= 0.L * (p.(len p-'1))" by VECTSP_1:def 23
.= 0.L by VECTSP_1:39;
end;
hence thesis by ALGSEQ_1:def 2;
end;
end;
theorem Th57:
for L be commutative associative left_unital distributive Field-like
(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 left_unital distributive Field-like
(non empty doubleLoopStr);
let p be Polynomial of L;
assume len p <> 0;
then len p > 0 by NAT_1:19;
then len p >= 0+1 by NAT_1:38;
then len p = len p-'1+1 by AMI_5:4;
then A1: p.(len p-'1) <> 0.L by ALGSEQ_1:25;
thus (NormPolynomial p).(len p-'1) = p.(len p-'1) / p.(len p-'1) by Def10
.= p.(len p-'1) * (p.(len p-'1))" by VECTSP_1:def 23
.= 1_(L) by A1,VECTSP_1:def 22;
end;
theorem Th58:
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 by NAT_1:19;
then len p >= 0+1 by NAT_1:38;
then len p = len p-'1+1 by AMI_5:4;
then p.(len p-'1) <> 0.L by ALGSEQ_1:25;
then A1: (p.(len p-'1))" <> 0.L by VECTSP_1:74;
A2: len p is_at_least_length_of NormPolynomial(p)
proof
let n be Nat;
assume A3: n >= len p;
thus (NormPolynomial(p)).n = p.n / p.(len p-'1) by Def10
.= 0.L / p.(len p-'1) by A3,ALGSEQ_1:22
.= 0.L * (p.(len p-'1))" by VECTSP_1:def 23
.= 0.L by VECTSP_1:39;
end;
now let n be Nat;
assume A4: n is_at_least_length_of NormPolynomial(p);
n is_at_least_length_of p
proof
let i be Nat;
assume i >= n;
then (NormPolynomial(p)).i = 0.L by A4,ALGSEQ_1:def 3;
then p.i / p.(len p-'1) = 0.L by Def10;
then p.i * (p.(len p-'1))" = 0.L by VECTSP_1:def 23;
hence p.i = 0.L by A1,VECTSP_1:44;
end;
hence len p <= n by ALGSEQ_1:def 4;
end;
hence thesis by A2,ALGSEQ_1:def 4;
end;
theorem Th59:
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;
let x be Element of L;
set NPp = NormPolynomial(p);
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 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 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,Th58;
then A8: dom F1 = dom F2 by FINSEQ_3:31;
now let i be set;
assume A9: i in dom F1;
then reconsider i1=i as Nat by FINSEQ_3:25;
A10: p.(i1-'1) * (power L).(x,i1-'1) = F1.i by A4,A9
.= F1/.i by A9,FINSEQ_4:def 4;
thus F2/.i = F2.i by A8,A9,FINSEQ_4:def 4
.= 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 Def10
.= p.(i1-'1) * (p.(len p-'1))" * (power L).(x,i1-'1) by VECTSP_1:def
23
.= (F1/.i)*(p.(len p-'1))" by A10,VECTSP_1:def 16;
end;
then F2 = F1*(p.(len p-'1))" by A8,POLYNOM1:def 3;
then eval(NormPolynomial(p),x) = eval(p,x) * (p.(len p-'1))"
by A2,A5,POLYNOM1:29;
hence thesis by VECTSP_1:def 23;
end;
theorem Th60:
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 by NAT_1:19;
then len p >= 0+1 by NAT_1:38;
then len p = len p-'1+1 by AMI_5:4;
then p.(len p-'1) <> 0.L by ALGSEQ_1:25;
then A2: (p.(len p-'1))" <> 0.L by VECTSP_1:74;
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 by Def6;
then eval(NormPolynomial(p),x) = 0.L/p.(len p-'1) by A1,Th59
.= 0.L * (p.(len p-'1))" by VECTSP_1:def 23
.= 0.L by VECTSP_1:39;
hence x is_a_root_of NormPolynomial(p) by Def6;
end;
assume x is_a_root_of NormPolynomial(p);
then 0.L = eval(NormPolynomial(p),x) by Def6
.= eval(p,x)/p.(len p-'1) by A1,Th59
.= eval(p,x) * (p.(len p-'1))" by VECTSP_1:def 23;
then eval(p,x) = 0.L by A2,VECTSP_1:44;
hence thesis by Def6;
end;
theorem Th61:
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 by Def7;
x is_a_root_of NormPolynomial(p) by A1,A2,Th60;
hence NormPolynomial(p) is with_roots by Def7;
end;
assume NormPolynomial(p) is with_roots;
then consider x be Element of L such that
A3: x is_a_root_of NormPolynomial(p) by Def7;
x is_a_root_of p by A1,A3,Th60;
hence thesis by Def7;
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 set;
assume A2: x in Roots(p);
then reconsider x1=x as Element of L;
x1 is_a_root_of p by A2,Def9;
then x1 is_a_root_of NormPolynomial p by A1,Th60;
hence x in Roots(NormPolynomial p) by Def9;
end;
thus Roots(NormPolynomial p) c= Roots(p)
proof
let x be set;
assume A3: x in Roots(NormPolynomial p);
then reconsider x1=x as Element of L;
x1 is_a_root_of NormPolynomial p by A3,Def9;
then x1 is_a_root_of p by A1,Th60;
hence thesis by Def9;
end;
end;
theorem Th63:
id(COMPLEX) is_continuous_on COMPLEX
proof
A1: dom id(COMPLEX) = COMPLEX by FUNCT_2:def 1;
now let x be Element of 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 Element of COMPLEX;
assume that
y in COMPLEX and
A3: |.y-x.| < s;
A4: id(COMPLEX)/.x = id(COMPLEX).x by A1,FINSEQ_4:def 4
.= x by FUNCT_1:35;
id(COMPLEX)/.y = id(COMPLEX).y by A1,FINSEQ_4:def 4;
hence |.id(COMPLEX)/.y - id(COMPLEX)/.x.| < r by A3,A4,FUNCT_1:35;
end;
hence thesis by A1,CFCONT_1:61;
end;
theorem Th64:
for x be Element of COMPLEX holds
COMPLEX --> x is_continuous_on COMPLEX
proof
let x be Element of COMPLEX;
A1: dom (COMPLEX --> x) = COMPLEX by FUNCOP_1:19;
now let x1 be Element of COMPLEX;
let r be Real;
assume that
x1 in COMPLEX and
A2: 0 < r;
take s=r;
thus 0 < s by A2;
let x2 be Element of COMPLEX;
assume that
x2 in COMPLEX and
|.x2-x1.| < s;
A3: (COMPLEX --> x)/.x1 = (COMPLEX --> x).x1 by A1,FINSEQ_4:def 4
.= x by FUNCOP_1:13;
(COMPLEX --> x)/.x2 = (COMPLEX --> x).x2 by A1,FINSEQ_4:def 4
.= x by FUNCOP_1:13;
hence |.(COMPLEX --> x)/.x2 - (COMPLEX --> x)/.x1 .| < r
by A2,A3,COMPLEX1:130,
XCMPLX_1:14;
end;
hence thesis by A1,CFCONT_1:61;
end;
definition
let L be unital (non empty HGrStr);
let x be Element of L;
let n be Nat;
func FPower(x,n) -> map of L,L means :Def11:
for y be Element of L holds it.y = x*(power L).(y,n);
existence
proof
deffunc F(Element of L) = x*(power L).($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 LambdaD;
reconsider f as map of L,L;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be map of L,L such that
A2: for y be Element of L holds f1.y=x*(power L).(y,n) and
A3: for y be Element of L holds f2.y=x*(power L).(y,n);
now let y be Element of L;
thus f1.y = x*(power L).(y,n) by A2
.= f2.y by A3;
end;
hence f1 = f2 by FUNCT_2:113;
end;
end;
theorem
for L be unital (non empty HGrStr) holds
FPower(1.(L),1) = id(the carrier of L)
proof
let L be unital (non empty HGrStr);
A1: dom FPower(1.(L),1) = the carrier of L by FUNCT_2:def 1;
now let x be set;
assume x in the carrier of L;
then reconsider x1=x as Element of L;
FPower(1.(L),1).x1 = 1.(L)*(power L).(x1,1) by Def11
.= (power L).(x1,1) by GROUP_1:def 4;
hence FPower(1.(L),1).x = x by COMPTRIG:12;
end;
hence thesis by A1,FUNCT_1:34;
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 map of F_Complex,F_Complex;
now let x be Element of F_Complex;
reconsider x1=x as Element of COMPLEX by COMPLFLD:def 1;
dom id(COMPLEX) = COMPLEX by FUNCT_2:def 1;
then A1: id(COMPLEX)/.x1 = id(COMPLEX).x1 by FINSEQ_4:def 4
.= x1 by FUNCT_1:35;
dom (id(COMPLEX)(#)id(COMPLEX)) = COMPLEX by FUNCT_2:def 1;
hence f.x = x1*x1 by A1,COMSEQ_1:def 3
.= x*x by COMPLFLD:6
.= (power F_Complex).(x,2) by COMPTRIG:13
.= 1_(F_Complex)*(power F_Complex).(x,2) by VECTSP_1:def 19;
end;
hence thesis by Def11;
end;
theorem Th67:
for L be unital (non empty HGrStr)
for x be Element of L holds
FPower(x,0) = (the carrier of L) --> x
proof
let L be unital (non empty HGrStr);
let x be Element of L;
reconsider f=(the carrier of L) --> x as map of L,L;
now let y be Element of L;
thus f.y = x by FUNCOP_1:13
.= x*1.L by GROUP_1:def 4
.= x*(power L).(y,0) by GROUP_1:def 7;
end;
hence thesis by Def11;
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 map 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 COMSEQ_1:def 7
.= x1*y1 by FUNCT_1:35
.= x*y by COMPLFLD:6
.= x*(power F_Complex).(y,1) by COMPTRIG:12;
end;
hence thesis by Def11;
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
map of F_Complex,F_Complex;
now let y be Element of F_Complex;
reconsider y1=y as Element of COMPLEX by COMPLFLD:def 1;
A1: y*y = y1*y1 by COMPLFLD:6;
thus f.y = x1*(id(COMPLEX)(#)id(COMPLEX)).y1 by COMSEQ_1:def 7
.= x1*(id(COMPLEX).y1*id(COMPLEX).y1) by COMSEQ_1:def 5
.= x1*(y1*id(COMPLEX).y1) by FUNCT_1:35
.= x1*(y1*y1) by FUNCT_1:35
.= x*(y*y) by A1,COMPLFLD:6
.= x*(power F_Complex).(y,2) by COMPTRIG:13;
end;
hence thesis by Def11;
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) & 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;
take f;
thus f = FPower(x,n);
reconsider g=f(#)id(COMPLEX) as map of F_Complex,F_Complex by A1;
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 COMSEQ_1:def 5
.= f.y1*y1 by FUNCT_1:35
.= FPower(x,n).y*y by COMPLFLD:6
.= x*(power F_Complex).(y,n)*y by Def11
.= x*((power F_Complex).(y,n)*y) by VECTSP_1:def 16
.= x*(power F_Complex).(y,n+1) by GROUP_1:def 7;
end;
hence thesis by Def11;
end;
theorem Th71:
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;
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
defpred P[Nat] means ex f be Function of COMPLEX,COMPLEX st
f = FPower(x,$1) & f is_continuous_on COMPLEX;
A2: 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 Th67;
hence f is_continuous_on COMPLEX by A1,Th64;
end;
A3: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
given f be Function of COMPLEX,COMPLEX such that
A4: f = FPower(x,n) and
A5: f is_continuous_on COMPLEX;
reconsider g=FPower(x,n+1) as Function of COMPLEX,COMPLEX by A1;
take g;
thus g = FPower(x,n+1);
consider f1 be Function of COMPLEX,COMPLEX such that
A6: f1 = FPower(x,n) and
A7: FPower(x,n+1) = f1(#)id(COMPLEX) by Th70;
thus g is_continuous_on COMPLEX by A4,A5,A6,A7,Th63,CFCONT_1:65;
end;
thus for n be Nat holds P[n] from Ind(A2,A3);
end;
definition
let L be unital (non empty doubleLoopStr);
let p be Polynomial of L;
func Polynomial-Function(L,p) -> map of L,L means :Def12:
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 LambdaD;
reconsider f as map of L,L;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be map 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:113;
end;
end;
theorem Th72:
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
let p be Polynomial of F_Complex;
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f = Polynomial-Function(F_Complex,p) as
Function of COMPLEX,COMPLEX;
take f;
thus f = Polynomial-Function(F_Complex,p);
set FuFF=Funcs(COMPLEX,COMPLEX);
deffunc F(Element of FuFF,Element of FuFF) = @($1+$2);
consider fadd be BinOp of FuFF such that
A2: for x,y be Element of FuFF holds fadd.(x,y) = F(x,y) from BinOpLambda;
reconsider fzero = COMPLEX --> 0c as Element of FuFF by FUNCT_2:12;
reconsider L=LoopStr(#FuFF,fadd,fzero#) as non empty LoopStr;
A3: now let u,v,w be Element of L;
reconsider u1=u, v1=v, w1=w as Function of COMPLEX,COMPLEX by FUNCT_2:121;
A4: u1+v1 in Funcs(COMPLEX,COMPLEX) & v1+w1 in Funcs(COMPLEX,COMPLEX)
by FUNCT_2:12;
thus (u+v)+w = fadd.(u+v,w) by RLVECT_1:5
.= fadd.(fadd.(u,v),w) by RLVECT_1:5
.= fadd.(@(u1+v1),w) by A2
.= fadd.(u1+v1,w) by FUNCSDOM:def 1
.= @(u1+v1+w1) by A2,A4
.= u1+v1+w1 by FUNCSDOM:def 1
.= u1+(v1+w1) by CFUNCT_1:22
.= @(u1+(v1+w1)) by FUNCSDOM:def 1
.= fadd.(u,v1+w1) by A2,A4
.= fadd.(u,@(v1+w1)) by FUNCSDOM:def 1
.= fadd.(u,fadd.(v,w)) by A2
.= fadd.(u,v+w) by RLVECT_1:5
.= u+(v+w) by RLVECT_1:5;
end;
A5: 0.L = fzero by RLVECT_1:def 2;
A6: now let v be Element of L;
reconsider v1=v as Function of COMPLEX,COMPLEX by FUNCT_2:121;
A7: now let x be Element of COMPLEX;
thus (v1+fzero).x = v1.x+fzero.x by COMSEQ_1:def 4
.= v1.x+0c by FUNCOP_1:13
.= v1.x by COMPLEX1:22;
end;
thus v + 0.L = fadd.(v,0.L) by RLVECT_1:5
.= @(v1+fzero) by A2,A5
.= v1+fzero by FUNCSDOM:def 1
.= v by A7,FUNCT_2:113;
end;
now let v be Element of L;
reconsider v1=v as Function of COMPLEX,COMPLEX by FUNCT_2:121;
reconsider w=-v1 as Element of L by FUNCT_2:12;
take w;
A8: now let x be Element of COMPLEX;
thus (v1+-v1).x = v1.x+(-v1).x by COMSEQ_1:def 4
.= v1.x+-v1.x by COMSEQ_1:def 9
.= 0c by XCMPLX_0:def 6
.= fzero.x by FUNCOP_1:13;
end;
thus v + w = fadd.(v,w) by RLVECT_1:5
.= @(v1+-v1) by A2
.= v1+-v1 by FUNCSDOM:def 1
.= 0.L by A5,A8,FUNCT_2:113;
end;
then reconsider L as add-associative right_zeroed right_complementable
(non empty LoopStr) by A3,A6,RLVECT_1:def 6,def 7,def 8;
defpred P[Nat,set] means $2 = FPower(p.($1-'1),$1-'1);
A9: now let n be Nat;
assume n in Seg len p;
reconsider x = FPower(p.(n-'1),n-'1) as Element of L
by A1,FUNCT_2:12;
take x;
thus P[n,x];
end;
consider F be FinSequence of the carrier of L such that
A10: dom F = Seg len p and
A11: for n be Nat st n in Seg len p holds P[n,F.n] from SeqDEx(A9);
A12: F|len F = F by TOPREAL1:2;
defpred P[Nat] means for g be PartFunc of COMPLEX,COMPLEX st g = Sum (F|$1)
holds g is_continuous_on COMPLEX;
A13: P[0]
proof
let g be PartFunc of COMPLEX,COMPLEX;
assume A14: g = Sum (F|0);
F|0 = <*>the carrier of L;
then g = 0.L by A14,RLVECT_1:60
.= COMPLEX --> 0c by RLVECT_1:def 2;
hence g is_continuous_on COMPLEX by Th64;
end;
A15: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A16: for g be PartFunc of COMPLEX,COMPLEX st g = Sum (F|k) holds
g is_continuous_on COMPLEX;
let g be PartFunc of COMPLEX,COMPLEX;
assume A17: g = Sum (F|(k+1));
reconsider g1 = Sum (F|k) as Function of COMPLEX,COMPLEX by FUNCT_2:121;
A18: g1 is_continuous_on COMPLEX by A16;
per cases;
suppose A19: len F > k;
then A20: k+1 <= len F by NAT_1:38;
k+1 >= 1 by NAT_1:29;
then A21: k+1 in dom F by A20,FINSEQ_3:27;
then A22: F/.(k+1) = F.(k+1) by FINSEQ_4:def 4
.= FPower(p.(k+1-'1),k+1-'1) by A10,A11,A21
.= FPower(p.k,k+1-'1) by BINARITH:39
.= FPower(p.k,k) by BINARITH:39;
consider g2 be Function of COMPLEX,COMPLEX such that
A23: g2 = FPower(p.k,k) and
A24: g2 is_continuous_on COMPLEX by Th71;
F|(k+1) = F|k ^ <*F.(k+1)*> by A19,POLYNOM3:19
.= F|k ^ <*F/.(k+1)*> by A21,FINSEQ_4:def 4;
then g = Sum(F|k) + F/.(k+1) by A17,FVSUM_1:87
.= fadd.(Sum(F|k),F/.(k+1)) by RLVECT_1:5
.= @(g1+g2) by A2,A22,A23
.= g1+g2 by FUNCSDOM:def 1;
hence g is_continuous_on COMPLEX by A18,A24,CFCONT_1:65;
suppose A25: len F <= k;
k <= k+1 by NAT_1:29;
then len F <= k+1 by A25,AXIOMS:22;
then F|(k+1) = F by TOPREAL1:2
.= F|k by A25,TOPREAL1:2;
hence g is_continuous_on COMPLEX by A16,A17;
end;
A26: for k be Nat holds P[k] from Ind(A13,A15);
reconsider SF = Sum F as Function of COMPLEX,COMPLEX by FUNCT_2:121;
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
A27: eval(p,x1) = Sum H and
A28: len H = len p and
A29: for n be Nat st n in dom H holds
H.n = p.(n-'1)*(power F_Complex).(x1,n-'1) by POLYNOM4:def 2;
A30: len F = len p by A10,FINSEQ_1:def 3;
defpred P[Nat] means for SFk be Function of COMPLEX,COMPLEX st
SFk = Sum (F|$1) holds Sum (H|$1) = SFk.x;
A31: P[0]
proof
let SFk be Function of COMPLEX,COMPLEX;
assume A32: SFk = Sum (F|0);
F|0 = <*>the carrier of L;
then A33: SFk = 0.L by A32,RLVECT_1:60
.= COMPLEX --> 0c by RLVECT_1:def 2;
H|0 = <*>the carrier of F_Complex;
hence Sum (H|0) = 0.F_Complex by RLVECT_1:60
.= SFk.x by A33,COMPLFLD:9,FUNCOP_1:13;
end;
A34: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A35: for SFk be Function of COMPLEX,COMPLEX st SFk = Sum
(F|k) holds
Sum (H|k) = SFk.x;
let SFk be Function of COMPLEX,COMPLEX;
assume A36: SFk = Sum (F|(k+1));
reconsider SFk1 = Sum
(F|k) as Function of COMPLEX,COMPLEX by FUNCT_2:121;
per cases;
suppose A37: len F > k;
then A38: k+1 <= len F by NAT_1:38;
A39: dom F = dom H by A10,A28,FINSEQ_1:def 3;
k+1 >= 1 by NAT_1:29;
then A40: k+1 in dom F by A38,FINSEQ_3:27;
then A41: H/.(k+1) = H.(k+1) by A39,FINSEQ_4:def 4
.= p.(k+1-'1)*(power F_Complex).(x1,k+1-'1) by A29,A39,A40
.= p.k*(power F_Complex).(x1,k+1-'1) by BINARITH:39
.= p.k*(power F_Complex).(x1,k) by BINARITH:39
.= FPower(p.k,k).x by Def11;
A42: F/.(k+1) = F.(k+1) by A40,FINSEQ_4:def 4
.= FPower(p.(k+1-'1),k+1-'1) by A10,A11,A40
.= FPower(p.k,k+1-'1) by BINARITH:39
.= FPower(p.k,k) by BINARITH:39;
reconsider g2 = FPower(p.k,k) as Function of COMPLEX,COMPLEX by A1;
F|(k+1) = F|k ^ <*F.(k+1)*> by A37,POLYNOM3:19
.= F|k ^ <*F/.(k+1)*> by A40,FINSEQ_4:def 4;
then A43: SFk = Sum(F|k) + F/.(k+1) by A36,FVSUM_1:87
.= fadd.(Sum(F|k),F/.(k+1)) by RLVECT_1:5
.= @(SFk1+g2) by A2,A42
.= SFk1+g2 by FUNCSDOM:def 1;
A44: Sum (H|k) = SFk1.x by A35;
H|(k+1) = H|k ^ <*H.(k+1)*> by A28,A30,A37,POLYNOM3:19
.= H|k ^ <*H/.(k+1)*> by A39,A40,FINSEQ_4:def 4;
hence Sum (H|(k+1)) = Sum(H|k) + H/.(k+1) by FVSUM_1:87
.= SFk1.x + g2.x by A41,A44,COMPLFLD:3
.= SFk.x by A43,COMSEQ_1:def 4;
suppose A45: len F <= k;
then A46: F|k = F & H|k = H by A28,A30,TOPREAL1:2;
k <= k+1 by NAT_1:29;
then len F <= k+1 by A45,AXIOMS:22;
then F|(k+1) = F & H|(k+1) = H by A28,A30,TOPREAL1:2;
hence Sum (H|(k+1)) = SFk.x by A35,A36,A46;
end;
A47: for k be Nat holds P[k] from Ind(A31,A34);
A48: Sum(F|len F) = SF by TOPREAL1:2;
thus f.x = Sum H by A27,Def12
.= Sum (H|len H) by TOPREAL1:2
.= SF.x by A28,A30,A47,A48;
end;
then f = SF by FUNCT_2:113;
hence thesis by A12,A26;
end;
theorem Th73:
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 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).| > |.p.0 .|+1
proof
let p be Polynomial of F_Complex;
assume that
A1: len p > 2 and
A2: |.p.(len p-'1).|=1;
A3: len p > 1 by A1,AXIOMS:22;
let F be FinSequence of REAL;
assume that
A4: len F = len p and
A5: for n be Nat st n in dom F holds F.n = |.p.(n-'1).|;
let z be Element of F_Complex;
assume A6: |.z.| > Sum F;
set lF1 = len F-'1;
set lF2 = len F-'2;
consider G be FinSequence of the carrier of F_Complex such that
A7: eval(p,z) = Sum G and
A8: len G = len p and
A9: for n be Nat st n in dom G holds
G.n = p.(n-'1)*(power F_Complex).(z,n-'1) by POLYNOM4:def 2;
A10: lF1+1 = len F by A3,A4,AMI_5:4;
A11: len F >= 1+1+0 by A1,A4;
then A12: lF1 >= 1 by A10,REAL_1:53;
A13: 1 in dom F & len F in dom F by A3,A4,FINSEQ_3:27;
A14: dom F = dom G by A4,A8,FINSEQ_3:31;
A15: F/.(lF1+1) = F.(lF1+1) by A10,A13,FINSEQ_4:def 4
.= 1 by A2,A4,A5,A10,A13;
F = F|(lF1+1) by A10,TOPREAL1:2
.= F|lF1 ^ <*F/.(lF1+1)*> by A10,JORDAN8:2;
then A16: Sum F = Sum(F|lF1) + 1 by A15,RVSUM_1:104;
G/.(lF1+1) = G.(lF1+1) by A10,A13,A14,FINSEQ_4:def 4
.= p.lF1*(power F_Complex).(z,lF1) by A9,A10,A13,A14;
then A17: |.G/.(lF1+1).| = 1*|.(power F_Complex).(z,lF1).|
by A2,A4,COMPLFLD:109;
G = G|(lF1+1) by A4,A8,A10,TOPREAL1:2
.= G|lF1 ^ <*G/.(lF1+1)*> by A4,A8,A10,JORDAN8:2;
then Sum G = Sum(G|lF1) + G/.(lF1+1) by FVSUM_1:87;
then A18: |.eval(p,z).| >= |.(power F_Complex).(z,lF1).|- |.Sum(G|lF1).|
by A7,A17,COMPLFLD:102;
A19: lF1 <= len F by A10,NAT_1:29;
then len (F|lF1) = lF1 by TOPREAL1:3;
then A20: 1 in dom (F|lF1) by A12,FINSEQ_3:27;
A21: 0.F_Complex = the Zero of F_Complex by RLVECT_1:def 2;
defpred P[Nat] means |.Sum(G|lF1|$1).| <=
(Sum (F|lF1|$1))*|.(power F_Complex).(z,lF2).|;
G|lF1|0 = <*>the carrier of F_Complex & F|lF1|0 = <*>REAL;
then A22: P[0] by A21,COMPLFLD:93,RLVECT_1:60,RVSUM_1:102;
A23: len (F|lF1) = lF1 by A19,TOPREAL1:3
.= len (G|lF1) by A4,A8,A19,TOPREAL1:3;
then A24: dom (F|lF1) = dom (G|lF1) by FINSEQ_3:31;
A25: now let n be Nat;
assume A26: n in dom (F|lF1);
A27: dom(F|lF1) c= dom F by FINSEQ_5:20;
(F|lF1).n = (F|lF1)/.n by A26,FINSEQ_4:def 4
.= F/.n by A26,TOPREAL1:1
.= F.n by A26,A27,FINSEQ_4:def 4
.= |.p.(n-'1).| by A5,A26,A27;
hence (F|lF1).n >= 0 by COMPLFLD:95;
end;
(F|lF1).1 = (F|lF1)/.1 by A20,FINSEQ_4:def 4
.= F/.1 by A20,TOPREAL1:1
.= F.1 by A13,FINSEQ_4:def 4
.= |.p.(1-'1).| by A5,A13
.= |.p.0 .| by GOBOARD9:1;
then Sum(F|lF1) >= |.p.0 .| by A20,A25,Th4;
then Sum F >= |.p.0 .|+1 by A16,AXIOMS:24;
then A28: |.z.| > |.p.0 .|+1 by A6,AXIOMS:22;
|.p.0 .| >= 0 by COMPLFLD:95;
then A29: |.p.0 .|+1 >= 0+1 by AXIOMS:24;
then A30: |.z.| > 1 by A28,AXIOMS:22;
|.z.| > 0 by A28,A29,AXIOMS:22;
then A31: z <> 0.F_Complex by COMPLFLD:96;
A32: len F-2 >=0 by A11,REAL_1:84;
1 = 1+0;
then A33: len F-1 >= 0 by A3,A4,REAL_1:84;
A34: lF2+1 = len F-2+1 by A32,BINARITH:def 3
.= len F-(2-1) by XCMPLX_1:37
.= lF1 by A33,BINARITH:def 3;
A35: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A36: |.Sum(G|lF1|n).| <= (Sum
(F|lF1|n))*|.(power F_Complex).(z,lF2).|;
then A37: |.Sum(G|lF1|n).|+|.(G|lF1)/.(n+1).| <=
(Sum (F|lF1|n))*|.(power F_Complex).(z,lF2).|+|.(G|lF1)/.(n+1).|
by AXIOMS:24;
per cases;
suppose A38: n+1 <= len (G|lF1);
n+1 >= 1 by NAT_1:29;
then A39: n+1 in dom (G|lF1) by A38,FINSEQ_3:27;
A40: dom (G|lF1) c= dom G by FINSEQ_5:20;
(G|lF1)|(n+1) = (G|lF1)|n ^ <*(G|lF1)/.(n+1)*> by A38,JORDAN8:2;
then Sum(G|lF1|(n+1)) = Sum((G|lF1)|n) + (G|lF1)/.(n+1) by FVSUM_1:87;
then |.Sum(G|lF1|(n+1)).| <= |.Sum((G|lF1)|n).|+|.(G|lF1)/.(n+1).|
by COMPLFLD:100;
then A41: |.Sum(G|lF1|(n+1)).| <=
(Sum (F|lF1|n))*|.(power F_Complex).(z,lF2).|+|.(G|lF1)/.(n+1).|
by A37,AXIOMS:22;
(F|lF1)|(n+1) = (F|lF1)|n ^ <*(F|lF1)/.(n+1)*> by A23,A38,JORDAN8:2;
then A42: Sum(F|lF1|(n+1)) = Sum
((F|lF1)|n) + (F|lF1)/.(n+1) by RVSUM_1:104;
A43: (F|lF1)/.(n+1) = F/.(n+1) by A24,A39,TOPREAL1:1
.= F.(n+1) by A14,A39,A40,FINSEQ_4:def 4
.= |.p.(n+1-'1).| by A5,A14,A39,A40
.= |.p.n.| by BINARITH:39;
(G|lF1)/.(n+1) = G/.(n+1) by A39,TOPREAL1:1
.= G.(n+1) by A39,A40,FINSEQ_4:def 4
.= p.(n+1-'1)*(power F_Complex).(z,n+1-'1) by A9,A39,A40
.= p.n*(power F_Complex).(z,n+1-'1) by BINARITH:39
.= p.n*(power F_Complex).(z,n) by BINARITH:39;
then A44: |.(G|lF1)/.(n+1).| =
(F|lF1)/.(n+1)*|.(power F_Complex).(z,n).| by A43,COMPLFLD:109;
A45: |.p.n.| >= 0 by COMPLFLD:95;
n+1 <= lF2+1 by A4,A8,A19,A34,A38,TOPREAL1:3;
then n <= lF2 by REAL_1:53;
then |.z.| to_power n <= |.z.| to_power lF2 by A30,PRE_FF:10;
then |.z.| to_power n <= |.(power F_Complex).(z,lF2).| by A31,Th8;
then |.(power F_Complex).(z,n).|<=|.(power F_Complex).(z,lF2).|
by A31,Th8;
then |.(G|lF1)/.(n+1).| <= (F|lF1)/.(n+1)*|.(power F_Complex).(z,lF2).|
by A43,A44,A45,AXIOMS:25;
then (Sum(F|lF1|n))*|.(power F_Complex).(z,lF2).|+|.(G|lF1)/.(n+1).| <=
(Sum((F|lF1)|n))*|.(power F_Complex).(z,lF2).|+
((F|lF1)/.(n+1))*|.(power F_Complex).(z,lF2).| by AXIOMS:24;
then |.Sum(G|lF1|(n+1)).| <= (Sum
((F|lF1)|n))*|.(power F_Complex).(z,lF2).|+
((F|lF1)/.(n+1))*|.(power F_Complex).(z,lF2).| by A41,AXIOMS:22;
hence |.Sum(G|lF1|(n+1)).| <=
(Sum (F|lF1|(n+1)))*|.(power F_Complex).(z,lF2).| by A42,XCMPLX_1:8;
suppose A46: n+1 > len (G|lF1);
then n >= len (G|lF1) by NAT_1:38;
then (G|lF1)|n = (G|lF1) & (G|lF1)|(n+1) = (G|lF1) &
(F|lF1)|n = (F|lF1) & (F|lF1)|(n+1) = (F|lF1) by A23,A46,TOPREAL1:2;
hence |.Sum(G|lF1|(n+1)).| <=
(Sum (F|lF1|(n+1)))*|.(power F_Complex).(z,lF2).| by A36;
end;
A47: for n be Nat holds P[n] from Ind(A22,A35);
F|lF1|(len (F|lF1)) = F|lF1 & G|lF1|(len (F|lF1)) = G|lF1
by A23,TOPREAL1:2;
then |.Sum(G|lF1).| <= (Sum (F|lF1))*|.(power F_Complex).(z,lF2).| by A47;
then |.(power F_Complex).(z,lF1).|- |.Sum(G|lF1).| >=
|.(power F_Complex).(z,lF1).|-(Sum (F|lF1))*|.(power F_Complex).(z,lF2).|
by REAL_1:92;
then A48: |.eval(p,z).| >= |.(power F_Complex).(z,lF1).|-
|.(power F_Complex).(z,lF2).|*Sum (F|lF1) by A18,AXIOMS:22;
A49: |.(power F_Complex).(z,lF2).| >= 0 by COMPLFLD:95;
|.z.|-Sum (F|lF1) > 1 by A6,A16,REAL_1:86;
then A50: |.(power F_Complex).(z,lF2).|*(|.z.|-Sum (F|lF1)) >=
|.(power F_Complex).(z,lF2).|*1 by A49,AXIOMS:25;
(power F_Complex).(z,lF1) = (power F_Complex).(z,lF2)*z
by A34,GROUP_1:def 7;
then |.(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:109
.= |.(power F_Complex).(z,lF2).|*(|.z.|-Sum (F|lF1)) by XCMPLX_1:40;
then A51: |.eval(p,z).| >= |.(power F_Complex).(z,lF2).|
by A48,A50,AXIOMS:22;
len F >= 2+1 by A1,A4,NAT_1:38;
then len F-2 >= 1 by REAL_1:84;
then lF2 >= 1 by A32,BINARITH:def 3;
then |.z.| to_power lF2 >= |.z.| to_power 1 by A30,PRE_FF:10;
then |.(power F_Complex).(z,lF2).| >= |.z.| to_power 1 by A31,Th8;
then |.(power F_Complex).(z,lF2).| >= |.(power F_Complex).(z,1).|
by A31,Th8;
then |.(power F_Complex).(z,lF2).| >= |.z.| by COMPTRIG:12;
then |.eval(p,z).| >= |.z.| by A51,AXIOMS:22;
hence thesis by A28,AXIOMS:22;
end;
theorem Th74:
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
let p be Polynomial of F_Complex;
assume A1: len p > 2;
then A2: len p > 1 by AXIOMS:22;
set np = NormPolynomial(p);
deffunc F(Element of F_Complex) = |.eval(np,$1).|;
defpred P[set] means not contradiction;
reconsider D = { F(z) where z is Element of the carrier
of F_Complex : P[z] } as Subset of REAL from SubsetFD;
set q = lower_bound D;
A3: |.eval(np,0.F_Complex).| in D;
A4: D is bounded_below
proof
take 0;
let b be real number;
assume b in D;
then consider z be Element of F_Complex such that
A5: b = |.eval(np,z).|;
thus 0 <= b by A5,COMPLFLD:95;
end;
defpred P[Nat,set] means ex g1 be Element of F_Complex st
g1 = $2 & |.eval(np,g1).| < q+1/($1+1);
A6: for n be Nat ex g be Element of COMPLEX st P[n,g]
proof
let n be Nat;
n+1 > 0 by NAT_1:18;
then 1/(n+1) > 0 by REAL_2:127;
then consider r be real number such that
A7: r in D and
A8: r < q+1/(n+1) by A3,A4,SEQ_4:def 5;
consider g1 be Element of F_Complex such that
A9: r = |.eval(np,g1).| by A7;
reconsider g=g1 as Element of COMPLEX by COMPLFLD:def 1;
take g,g1;
thus g1 = g;
thus |.eval(np,g1).| < q+1/(n+1) by A8,A9;
end;
consider G be Complex_Sequence such that
A10: for n be Nat holds P[n,G.n] from CompSeqChoice(A6);
deffunc G(Nat) = |.np.($1-'1).|;
consider F be FinSequence of REAL such that
A11: len F = len np and
A12: for n be Nat st n in Seg len np holds F.n = G(n) from SeqLambdaD;
A13: Seg len np = dom F by A11,FINSEQ_1:def 3;
A14: len p <> 0 by A1;
len p = len p-'1+1 by A2,AMI_5:4;
then A15: p.(len p-'1) <> 0.F_Complex by ALGSEQ_1:25;
then A16: p.(len p-'1) <> the Zero of F_Complex by RLVECT_1:def 2;
A17: |.p.(len p-'1).| > 0 by A15,COMPLFLD:96;
ex r be Real st for n be Nat holds |.G.n.| < r
proof
take r = Sum F + 1;
let n be Nat;
consider Gn be Element of F_Complex such that
A18: Gn = G.n and
A19: |.eval(np,Gn).| < q+1/(n+1) by A10;
A20: |.Gn.| = |.G.n.| by A18,COMPLFLD:def 3;
A21: len np = len p by A14,Th58;
then np.(len np-'1) = 1_(F_Complex) by A14,Th57;
then A22: |.np.(len np-'1).| = 1 by COMPLFLD:10,97,def 1;
n >= 0 by NAT_1:18;
then n+1>=0+1 by AXIOMS:24;
then A23: 1/(n+1) <= 1 by REAL_2:164;
|.G.n.| <= Sum F
proof
assume |.G.n.| > Sum F;
then A24: |.eval(np,Gn).| > |.np.0 .|+1
by A1,A11,A12,A13,A20,A21,A22,Th73;
eval(np,0.F_Complex) = np.0 by Th32;
then |.np.0 .| in D;
then |.np.0 .| >= q by A4,SEQ_4:def 5;
then |.np.0 .|+1 >= q+1/(n+1) by A23,REAL_1:55;
hence contradiction by A19,A24,AXIOMS:22;
end;
then |.G.n.|+0 < r by REAL_1:67;
hence |.G.n.| < r;
end;
then G is bounded by COMSEQ_2:def 3;
then consider G1 be Complex_Sequence such that
A25: G1 is_subsequence_of G and
A26: G1 is convergent by COMSEQ_3:51;
reconsider z0=lim G1 as Element of F_Complex
by COMPLFLD:def 1;
take z0;
let z be Element of F_Complex;
defpred P[Nat,set] means ex G1n be Element of F_Complex st
G1n = G1.$1 & $2 = eval(np,G1n);
A27: for n be Nat ex g be Element of COMPLEX st P[n,g]
proof
let n be Nat;
reconsider G1n = G1.n 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 g = eval(np,G1n);
end;
consider H be Complex_Sequence such that
A28: for n be Nat holds P[n,H.n] from CompSeqChoice(A27);
deffunc F(Nat) = 1/($1+1);
consider R be Real_Sequence such that
A29: for n be Nat holds R.n = F(n) from ExRealSeq;
deffunc G(Nat) = |.eval(np,z).|;
consider Rcons be Real_Sequence such that
A30: for n be Nat holds Rcons.n = G(n) from ExRealSeq;
A31: for H' be convergent Complex_Sequence holds |.H'.| is convergent;
consider Nseq be increasing Seq_of_Nat such that
A32: G1 = G(#)Nseq by A25,COMSEQ_3:def 9;
|.eval(np,z).| in D;
then A33: |.eval(np,z).| >= q by A4,SEQ_4:def 5;
consider g be Element of COMPLEX such that
A34: 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 A26,COMSEQ_2:def 4;
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;
assume A35: 0 < p;
consider fPF be Function of COMPLEX,COMPLEX such that
A36: fPF = Polynomial-Function(F_Complex,np) and
A37: fPF is_continuous_on COMPLEX by Th72;
consider p1 be Real such that
A38: 0 < p1 and
A39: for x1 be Element of COMPLEX st x1 in COMPLEX & |.x1-g.| < p1 holds
|.fPF/.x1 - fPF/.g.| < p by A35,A37,CFCONT_1:61;
consider n be Nat such that
A40: for m be Nat st n <= m holds |.G1.m-g.| < p1 by A34,A38;
take n;
let m be Nat;
assume n <= m;
then A41: |.G1.m-g.| < p1 by A40;
consider G1m be Element of F_Complex such that
A42: G1m = G1.m and
A43: H.m = eval(np,G1m) by A28;
A44: dom fPF = COMPLEX by FUNCT_2:def 1;
A45: H.m = fPF.(G1.m) by A36,A42,A43,Def12
.= fPF/.(G1.m) by A44,FINSEQ_4:def 4;
eg = fPF.g by A36,Def12
.= fPF/.g by A44,FINSEQ_4:def 4;
hence |.H.m-eg.| < p by A39,A41,A45;
end;
then A46: H is convergent by COMSEQ_2:def 4;
then A47: |.H.| is convergent by A31;
A48: R is convergent by A29,SEQ_4:43;
then A49: |.H.|-R is convergent by A47,SEQ_2:25;
A50: Rcons is constant by A30,SEQM_3:def 6;
then A51: Rcons is convergent by SEQ_4:39;
A52: Rcons.0 = |.eval(np,z).| by A30;
now let n be Nat;
A53: Rcons.n = |.eval(np,z).| by A30;
consider G1n be Element of F_Complex such that
A54: G1n = G1.n and
A55: H.n = eval(np,G1n) by A28;
dom (|.H.|-R) = NAT by FUNCT_2:def 1;
then A56: (|.H.|-R).n = |.H.|.n-R.n by SEQ_1:def 4
.= |.H.|.n-1/(n+1) by A29
.= |.H.n.|-1/(n+1) by COMSEQ_1:def 14
.= |.eval(np,G1n).|-1/(n+1) by A55,COMPLFLD:def 3;
consider gNn be Element of F_Complex such that
A57: gNn = G.(Nseq.n) and
A58: |.eval(np,gNn).| < q+1/((Nseq.n)+1) by A10;
A59: n+1 > 0 by NAT_1:19;
Nseq.n >= n by SEQM_3:33;
then Nseq.n+1 >= n+1 by AXIOMS:24;
then 1/(Nseq.n+1) <= 1/(n+1) by A59,REAL_2:152;
then q+1/(Nseq.n+1) <= q+1/(n+1) by AXIOMS:24;
then |.eval(np,gNn).| < q+1/(n+1) by A58,AXIOMS:22;
then q > |.eval(np,gNn).|-1/(n+1) by REAL_1:84;
then |.eval(np,z).| > |.eval(np,gNn).|-1/(n+1) by A33,AXIOMS:22;
hence Rcons.n >= (|.H.|-R).n by A32,A53,A54,A56,A57,COMSEQ_3:def 5;
end;
then lim (|.H.|-R) <= lim Rcons by A49,A51,SEQ_2:32;
then A60: lim (|.H.|-R) <= |.eval(np,z).| by A50,A52,SEQ_4:40;
A61: lim (|.H.|-R) = lim |.H.| - lim R by A47,A48,SEQ_2:26
.= |.lim H.| - lim R by A46,COMSEQ_2:11
.= |.lim H.| - 0 by A29,SEQ_4:44;
reconsider enp0 = eval(np,z0) as Element of COMPLEX by COMPLFLD:def 1;
consider PF be Function of COMPLEX,COMPLEX such that
A62: PF = Polynomial-Function(F_Complex,np) and
A63: PF is_continuous_on COMPLEX by Th72;
now let a be Real;
assume 0 < a;
then consider s be Real such that
A64: 0 < s and
A65: for x1 be Element of COMPLEX st
x1 in COMPLEX & |.x1-lim G1.| < s holds |.PF/.x1 - PF/.lim G1.| < a
by A63,CFCONT_1:61;
consider n be Nat such that
A66: for m be Nat st n <= m holds |.G1.m-lim G1.| < s
by A26,A64,COMSEQ_2:def 5;
take n;
let m be Nat;
assume n <= m;
then A67: |.G1.m-lim G1.| < s by A66;
consider G1m be Element of F_Complex such that
A68: G1m = G1.m and
A69: H.m = eval(np,G1m) by A28;
A70: dom PF = COMPLEX by FUNCT_2:def 1;
then A71: PF/.(G1.m) = PF.(G1.m) by FINSEQ_4:def 4
.= H.m by A62,A68,A69,Def12;
PF/.lim G1 = PF.lim G1 by A70,FINSEQ_4:def 4
.= eval(np,z0) by A62,Def12;
hence |.H.m - enp0 .| < a by A65,A67,A71;
end;
then enp0 = lim H by A46,COMSEQ_2:def 5;
then |.eval(np,z).| >= |.eval(np,z0).| by A60,A61,COMPLFLD:def 3;
then |.eval(p,z)/p.(len p-'1).| >= |.eval(np,z0).| by A14,Th59;
then |.eval(p,z)/p.(len p-'1).| >= |.eval(p,z0)/p.(len p-'1).|
by A14,Th59;
then |.eval(p,z).|/|.p.(len p-'1).| >= |.eval(p,z0)/p.(len p-'1).|
by A16,COMPLFLD:111;
then |.eval(p,z).|/|.p.(len p-'1).| >= |.eval(p,z0).|/|.p.(len p-'1).|
by A16,COMPLFLD:111;
hence thesis by A17,REAL_1:73;
end;
theorem Th75:
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:38;
per cases by A2,REAL_1:def 5;
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 Th74;
set q = Subst(p,<%z0,1_(F_Complex)%>);
A4: eval(p,z0) = eval(p,z0+0.F_Complex) by RLVECT_1:def 7
.= eval(p,eval(<%z0,1_(F_Complex)%>,0.F_Complex)) by Th48
.= eval(q,0.F_Complex) by Th54;
A5: now let z be Element of F_Complex;
eval(q,z) = eval(p,eval(<%z0,1_(F_Complex)%>,z)) by Th54
.= eval(p,z0+z) by Th48;
then |.eval(q,z).| >= |.eval(p,z0).| by A3;
hence |.eval(q,z).| >= |.q.0 .| by A4,Th32;
end;
A6: len p <> 0 by A1;
1_(F_Complex) <> 0.F_Complex by VECTSP_1:def 21;
then len <%z0,1_(F_Complex)%> = 2 by Th41;
then A7: len q = 2*len p - len p - 2 + 2 by A6,Th53
.= 2*len p - len p +- 2 + 2 by XCMPLX_0:def 8
.= 2*len p - len p by XCMPLX_1:139
.= len p + len p - len p by XCMPLX_1:11
.= len p by XCMPLX_1:26;
defpred P[Nat] means $1 >= 1 & q.$1 <> 0.F_Complex;
A8: ex k be Nat st P[k]
proof
len q-1 >= 1-1 by A1,A7,REAL_1:49;
then len q-1 = len q-'1 by BINARITH:def 3;
then reconsider k=len q-1 as Nat;
take k;
len q >= 1+1 by A1,A7,NAT_1:38;
hence k >= 1 by REAL_1:84;
len q = k+1 by XCMPLX_1:27;
hence q.k <> 0.F_Complex by ALGSEQ_1:25;
end;
consider k be Nat such that
A9: P[k] and
A10: for n be Nat st P[n] holds k <= n from Min(A8);
A11: k+1 > 1 by A9,NAT_1:38;
1=0+1;
then reconsider k1=k as non empty Nat by A9;
k < len q by A9,ALGSEQ_1:22;
then A12: k+1+0 <= len q by NAT_1:38;
consider sq be CRoot of k1,-(q.0/q.k);
deffunc O(Nat) = q.(k+$1)*(power F_Complex).(sq,k+$1);
consider F2 be FinSequence of the carrier of F_Complex such that
A13: len F2 = len q-'(k+1) and
A14: for n be Nat st n in Seg (len q-'(k+1)) holds F2.n = O(n)
from SeqLambdaD;
len q-(k+1) >= 0 by A12,REAL_1:84;
then A15: len F2 = len q-(k+1) by A13,BINARITH:def 3;
A16: now let n be Nat;
assume n in dom F2;
then n in Seg (len q-'(k+1)) by A13,FINSEQ_1:def 3;
hence F2.n = q.(k+n)*(power F_Complex).(sq,k+n) by A14;
end;
now let c be Real;
assume A17: 0 < c & c < 1;
set z1 = [**c,0**]*sq;
consider F1 be FinSequence of the carrier of F_Complex such that
A18: eval(q,z1) = Sum F1 and
A19: len F1 = len q and
A20: for n be Nat st n in dom F1 holds
F1.n = q.(n-'1)*(power F_Complex).(z1,n-'1) by POLYNOM4:def 2;
k+1 in Seg len F1 by A11,A12,A19,FINSEQ_1:3;
then A21: k+1 in dom F1 by FINSEQ_1:def 3;
then A22: F1.(k+1) = F1/.(k+1) by FINSEQ_4:def 4;
A23: k < len F1 by A9,A19,ALGSEQ_1:22;
1 in Seg k by A9,FINSEQ_1:3;
then 1 in Seg len (F1|k) by A23,TOPREAL1:3;
then A24: 1 in dom (F1|k) by FINSEQ_1:def 3;
A25: dom (F1|k) c= dom F1 by FINSEQ_5:20;
now let i be Nat;
assume that
A26: i in dom (F1|k) and
A27: i <> 1;
A28: 0+1 <= i & i <= len (F1|k) by A26,FINSEQ_3:27;
then A29: i-1 >= 0 by REAL_1:84;
i > 1 by A27,A28,REAL_1:def 5;
then i >= 1+1 by NAT_1:38;
then i-1 >= 1+1-1 by REAL_1:49;
then A30: i-'1 >= 1 by A29,BINARITH:def 3;
i <= k by A23,A28,TOPREAL1:3;
then i < k+1 by NAT_1:38;
then i-1 < k by REAL_1:84;
then A31: i-'1 < k by A29,BINARITH:def 3;
thus (F1|k)/.i = F1/.i by A26,TOPREAL1:1
.= F1.i by A25,A26,FINSEQ_4:def 4
.= q.(i-'1)*(power F_Complex).(z1,i-'1) by A20,A25,A26
.= 0.F_Complex*(power F_Complex).(z1,i-'1) by A10,A30,A31
.= 0.F_Complex by VECTSP_1:39;
end;
then A32: Sum (F1|k) = (F1|k)/.1 by A24,POLYNOM2:5
.= F1/.1 by A24,TOPREAL1:1
.= F1.1 by A24,A25,FINSEQ_4:def 4
.= q.(1-'1)*(power F_Complex).(z1,1-'1) by A20,A24,A25
.= q.0*(power F_Complex).(z1,1-'1) by GOBOARD9:1
.= q.0*(power F_Complex).(z1,0) by GOBOARD9:1
.= q.0*1.F_Complex by GROUP_1:def 7
.= q.0 by GROUP_1:def 4;
A33: F1/.(k+1) = F1.(k+1) by A21,FINSEQ_4:def 4
.= q.(k+1-'1)*(power F_Complex).(z1,k+1-'1) by A20,A21
.= q.k*(power F_Complex).(z1,k+1-'1) by BINARITH:39
.= q.k*(power F_Complex).(z1,k) by BINARITH:39
.= q.k*((power F_Complex).([**c,0**],k)*
(power F_Complex).(sq,k)) by COMPTRIG:15
.= q.k*((power F_Complex).([**c,0**],k)*(-(q.0/q.k)))
by COMPTRIG:def 2
.= q.k*(-(q.0/q.k))*(power F_Complex).([**c,0**],k)
by VECTSP_1:def 16
.= q.k*((-(q.0))/q.k)*(power F_Complex).([**c,0**],k)
by A9,COMPLFLD:78
.= (q.k* (-q.0))/q.k*(power F_Complex).([**c,0**],k)
by A9,COMPLFLD:64
.= (-q.0)*(power F_Complex).([**c,0**],k) by A9,COMPLFLD:66
.= (-q.0)*[**c to_power k,0**] by A17,COMPTRIG:16;
set gc = Sum(F1/^(k+1))/[**c to_power (k+1),0**];
A34: c to_power (k+1) > 0 by A17,POWER:39;
A35: c to_power k > 0 by A17,POWER:39;
0 + (c to_power k) <= 1 by A17,TBSP_1:2;
then A36: 1-(c to_power k) >= 0 by REAL_1:84;
A37: [**c to_power (k+1),0**] <> 0.F_Complex by A34,COMPTRIG:8,10;
then A38: [**c to_power (k+1),0**] <> the Zero of F_Complex by RLVECT_1:def 2;
A39: Sum(F1/^(k+1)) = [**c to_power (k+1),0**]*Sum(F1/^(k+1))/
[**c to_power (k+1),0**] by A37,COMPLFLD:66
.= [**c to_power (k+1),0**]*gc by A37,COMPLFLD:64;
F1 = (F1|(k+1-'1))^<*F1.(k+1)*>^(F1/^(k+1)) by A11,A12,A19,POLYNOM4:3;
then Sum F1 = Sum((F1|(k+1-'1))^<*F1/.(k+1)*>) + Sum(F1/^(k+1))
by A22,RLVECT_1:58
.= Sum(F1|(k+1-'1)) + Sum<*F1/.(k+1)*> + Sum
(F1/^(k+1)) by RLVECT_1:58
.= Sum(F1|k) + Sum<*F1/.(k+1)*> + Sum(F1/^(k+1)) by BINARITH:39
.= q.0 + (-q.0)*[**c to_power k,0**] + Sum(F1/^(k+1))
by A32,A33,RLVECT_1:61
.= q.0 + -q.0*[**c to_power k,0**] + Sum(F1/^(k+1)) by VECTSP_1:41
.= q.0 - q.0*[**c to_power k,0**] + Sum(F1/^(k+1)) by RLVECT_1:def 11
.= q.0*1_(F_Complex) - q.0*[**c to_power k,0**] + Sum(F1/^(k+1))
by VECTSP_1:def 13
.= q.0*(1_(F_Complex)-[**c to_power k,0**])+
[**c to_power (k+1),0**]*gc by A39,VECTSP_1:43;
then A40: |.q.0*(1_(F_Complex)-[**c to_power k,0**])+
[**c to_power (k+1),0**]*gc.| >= |.q.0 .| by A5,A18;
1r = [*1,0*] by ARYTM_0:def 7,COMPLEX1:def 7; then
A41: |.1_(F_Complex)-[**c to_power k,0**].| =
|.[**1,0**]-[**c to_power k,0**].|
by COMPLFLD:10,HAHNBAN1:def 1
.= |.[**1-(c to_power k),0-0**].| by Th6
.= abs(1-(c to_power k)) by HAHNBAN1:13
.= 1-(c to_power k) by A36,ABSVALUE:def 1;
|.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:100;
then |.q.0*(1_(F_Complex)-[**c to_power k,0**]).| +
|.[**c to_power (k+1),0**]*gc.| >= |.q.0 .| by A40,AXIOMS:22;
then |.q.0 .|*|.1_(F_Complex)-[**c to_power k,0**].| +
|.[**c to_power (k+1),0**]*gc.| >= |.q.0 .| by COMPLFLD:109;
then |.q.0 .|*|.1_(F_Complex)-[**c to_power k,0**].| +
|.[**c to_power (k+1),0**].|*|.gc.| >= |.q.0 .| by COMPLFLD:109;
then |.[**c to_power (k+1),0**].|*|.gc.| >= |.q.0 .|*1 -
|.q.0 .|*(1-(c to_power k)) by A41,REAL_1:86;
then |.[**c to_power (k+1),0**].|*|.gc.| >=
|.q.0 .|*(1-(1-(c to_power k))) by XCMPLX_1:40;
then |.[**c to_power (k+1),0**].|*|.gc.| >= |.q.0 .|*(c to_power k)
by XCMPLX_1:18;
then abs(c to_power (k+1))*|.gc.| >= |.q.0 .|*(c to_power k)
by HAHNBAN1:13;
then (c to_power (k+1))*|.gc.| >= |.q.0 .|*(c to_power k)
by A34,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 A35,REAL_1:73;
then (c to_power (k+1))*|.gc.|/(c to_power k)>=|.q.0 .|
by A35,XCMPLX_1:90;
then (c to_power (k+1))/(c to_power k)*|.gc.| >= |.q.0 .|
by XCMPLX_1:75;
then (c to_power (k+1-k))*|.gc.| >= |.q.0 .| by A17,POWER:34;
then (c to_power 1)*|.gc.| >= |.q.0 .| by XCMPLX_1:26;
then A42: c*|.gc.| >= |.q.0 .| by POWER:30;
gc = Sum(F1/^(k+1))*[**c to_power (k+1),0**]"
by VECTSP_1:def 23
.= Sum((F1/^(k+1))*[**c to_power (k+1),0**]") by POLYNOM1:29;
then A43: |.gc.| <= Sum |.(F1/^(k+1))*[**c to_power (k+1),0**]".|
by Th15;
A44: dom ((F1/^(k+1))*[**c to_power (k+1),0**]") = dom (F1/^(k+1))
by POLYNOM1:def 3;
A45: len |.(F1/^(k+1))*[**c to_power (k+1),0**]".| =
len ((F1/^(k+1))*[**c to_power (k+1),0**]") by Def1
.= len (F1/^(k+1)) by A44,FINSEQ_3:31
.= len F1-(k+1) by A12,A19,RFINSEQ:def 2
.= len |.F2.| by A15,A19,Def1;
now let i be Nat;
assume A46: i in dom |.(F1/^(k+1))*[**c to_power (k+1),0**]".|;
then A47: i in Seg len |.(F1/^(k+1))*[**c to_power (k+1),0**]".|
by FINSEQ_1:def 3;
then i in Seg len ((F1/^(k+1))*[**c to_power (k+1),0**]") by Def1;
then A48: i in dom ((F1/^(k+1))*[**c to_power (k+1),0**]")
by FINSEQ_1:def 3;
A49: k+i >= 0 by NAT_1:18;
then k+1+(i-1) >= 0 by XCMPLX_1:28;
then k+1+i-1 >= 0 by XCMPLX_1:29;
then A50: k+1+i-'1 = k+1+i-1 by BINARITH:def 3
.= k+i+1-1 by XCMPLX_1:1
.= k+i by XCMPLX_1:26;
A51: len F2 = len |.F2.| by Def1;
then A52: dom F2 = dom |.F2.| by FINSEQ_3:31;
A53: i in dom F2 by A45,A47,A51,FINSEQ_1:def 3;
k+i+1 >= 0+1 by A49,AXIOMS:24;
then A54: k+1+i >= 1 by XCMPLX_1:1;
i <= len |.F2.| by A45,A47,FINSEQ_1:3;
then i <= len F1-(k+1) by A15,A19,Def1;
then k+1+i <= len F1 by REAL_1:84;
then A55: k+1+i in dom F1 by A54,FINSEQ_3:27;
i >= 0+1 by A47,FINSEQ_1:3;
then A56: i-1 >= 0 by REAL_1:84;
c to_power (i-'1) <= 1 by A17,TBSP_1:2;
then A57: c to_power (i-1) <= 1 by A56,BINARITH:def 3;
A58: c to_power (k+i) > 0 by A17,POWER:39;
A59: |.q.(k+i)*(power F_Complex).(sq,k+i).| >= 0 by COMPLFLD:95;
A60: q.(k+i)*(power F_Complex).(sq,k+i) = F2.i by A16,A53
.= F2/.i by A53,FINSEQ_4:def 4;
A61: (F1/^(k+1))/.i = (F1/^(k+1)).i by A44,A48,FINSEQ_4:def 4
.= F1.(k+1+i) by A12,A19,A44,A48,RFINSEQ:def 2
.= q.(k+1+i-'1)*(power F_Complex).([**c,0**]*sq,k+1+i-'1) by A20,A55
.= q.(k+i)*((power F_Complex).(sq,k+i)*
(power F_Complex).([**c,0**],k+i)) by A50,COMPTRIG:15
.= q.(k+i)*(power F_Complex).(sq,k+i)*
(power F_Complex).([**c,0**],k+i) by VECTSP_1:def 16;
A62: k+i-(k+1) = i-1 by XCMPLX_1:32;
|.(F1/^(k+1))*[**c to_power (k+1),0**]".|.i =
|.(F1/^(k+1))*[**c to_power (k+1),0**]".|/.i by A46,FINSEQ_4:def 4
.= |.((F1/^(k+1))*[**c to_power (k+1),0**]")/.i.| by A48,Def1
.= |.((F1/^(k+1))/.i)*[**c to_power (k+1),0**]".|
by A44,A48,POLYNOM1:def 3
.= |.(F1/^(k+1))/.i.|*|.[**c to_power (k+1),0**]".| by COMPLFLD:109
.= |.(F1/^(k+1))/.i.|*|.[**c to_power (k+1),0**].|"
by A38,COMPLFLD:110
.= |.q.(k+i)*(power F_Complex).(sq,k+i)*
(power F_Complex).([**c,0**],k+i).|*abs(c to_power (k+1))"
by A61,HAHNBAN1:13
.= |.q.(k+i)*(power F_Complex).(sq,k+i).|*
|.(power F_Complex).([**c,0**],k+i).|*abs(c to_power (k+1))"
by COMPLFLD:109
.= |.q.(k+i)*(power F_Complex).(sq,k+i).|*
|.[**c to_power (k+i),0**].|*abs(c to_power (k+1))"
by A17,COMPTRIG:16
.= |.q.(k+i)*(power F_Complex).(sq,k+i).|*
abs(c to_power (k+i))*abs(c to_power (k+1))" by HAHNBAN1:13
.= |.q.(k+i)*(power F_Complex).(sq,k+i).|*
(c to_power (k+i))*abs(c to_power (k+1))" by A58,ABSVALUE:def 1
.= |.q.(k+i)*(power F_Complex).(sq,k+i).|*
(c to_power (k+i))*(c to_power (k+1))" by A34,ABSVALUE:def 1
.= |.q.(k+i)*(power F_Complex).(sq,k+i).|*
((c to_power (k+i))*(c to_power (k+1))") by XCMPLX_1:4
.= |.q.(k+i)*(power F_Complex).(sq,k+i).|*
((c to_power (k+i))/(c to_power (k+1))) by XCMPLX_0:def 9
.= |.q.(k+i)*(power F_Complex).(sq,k+i).|*(c to_power (i-1))
by A17,A62,POWER:34;
then |.(F1/^(k+1))*[**c to_power (k+1),0**]".|.i <= |.F2/.i.|
by A57,A59,A60,REAL_2:147;
then |.(F1/^(k+1))*[**c to_power (k+1),0**]".|.i <= |.F2.|/.i
by A53,Def1;
hence |.(F1/^(k+1))*[**c to_power (k+1),0**]".|.i <= |.F2.|.i
by A52,A53,FINSEQ_4:def 4;
end;
then Sum|.(F1/^(k+1))*[**c to_power (k+1),0**]".| <= Sum|.F2.|
by A45,INTEGRA5:3;
then |.gc.| <= Sum|.F2.| by A43,AXIOMS:22;
then c*|.gc.| <= c*Sum|.F2.| by A17,AXIOMS:25;
hence c*Sum|.F2.| >= |.q.0 .| by A42,AXIOMS:22;
end;
then |.q.0 .| <= 0 by Lm1;
then A63: q.0 = 0.F_Complex by COMPLFLD:96;
ex x be Element of F_Complex st x is_a_root_of p
proof
take z0;
eval(p,z0) = 0.F_Complex by A4,A63,Th32;
hence z0 is_a_root_of p by Def6;
end;
hence thesis by Def7;
suppose A64: len p = 2;
set np=NormPolynomial(p);
A65: len np = len p by A64,Th58;
1_(F_Complex) <> 0.F_Complex by VECTSP_1:def 21;
then A66: len <%np.0,1_(F_Complex)%> = 2 by Th41;
A67: len p-'1 = 2-1 by A64,BINARITH:def 3;
now let k be Nat;
assume A68: k < len np;
per cases by A64,A65,A68,ALGSEQ_1:4;
suppose k=0;
hence np.k = <%np.0,1_(F_Complex)%>.k by Th39;
suppose A69: k=1;
hence np.k = 1_(F_Complex) by A64,A67,Th57
.= <%np.0,1_(F_Complex)%>.k by A69,Th39;
end;
then A70: np = <%np.0,1_(F_Complex)%> by A64,A65,A66,ALGSEQ_1:28;
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 A70,Th48
.= 0.F_Complex by RLVECT_1:16;
hence z0 is_a_root_of np by Def6;
end;
then np is with_roots by Def7;
hence thesis by A64,Th61;
end;
definition
cluster F_Complex -> algebraic-closed;
coherence by Def8,Th75;
end;
definition
cluster algebraic-closed add-associative right_zeroed right_complementable
Abelian commutative associative distributive Field-like
non degenerated (left_unital right_unital (non empty doubleLoopStr));
existence
proof
take F_Complex;
thus thesis;
end;
end;