The abstract of the Mizar article:

Fundamental Theorem of Algebra

by

Robert Milewski

Received August 21, 2000

MML identifier: POLYNOM5

[ Mizar article, MML identifier index ]

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;


begin  :: Preliminaries

  theorem :: POLYNOM5:1
   for n,m be Nat st n <> 0 & m <> 0 holds
    n*m - n - m + 1 >= 0;

  theorem :: POLYNOM5:2
   for x,y be real number st y > 0 holds
    min(x,y)/max(x,y) <= 1;

  theorem :: POLYNOM5:3
   for x,y be real number st
    for c be real number st c > 0 & c < 1 holds c*x >= y holds
     y <= 0;

  theorem :: POLYNOM5:4
   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;

  theorem :: POLYNOM5:5
   for x,y be Real holds
    -[**x,y**] = [**-x,-y**];

  theorem :: POLYNOM5:6
   for x1,y1,x2,y2 be Real holds
    [**x1,y1**] - [**x2,y2**] = [**x1 - x2,y1 - y2**];

  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);

  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);

canceled;

  theorem :: POLYNOM5:8
   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;

  definition
   let p be FinSequence of the carrier of F_Complex;
   func |.p.| -> FinSequence of REAL means
:: POLYNOM5:def 1
    len it = len p &
    for n be Nat st n in dom p holds it/.n = |.p/.n.|;
  end;

  theorem :: POLYNOM5:9
   |.<*>the carrier of F_Complex.| = <*>REAL;

  theorem :: POLYNOM5:10
   for x be Element of F_Complex holds
    |.<*x*>.| = <*|.x.|*>;

  theorem :: POLYNOM5:11
     for x,y be Element of F_Complex holds
    |.<*x,y*>.| = <*|.x.|,|.y.|*>;

  theorem :: POLYNOM5:12
     for x,y,z be Element of F_Complex holds
    |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>;

  theorem :: POLYNOM5:13
   for p,q be FinSequence of the carrier of F_Complex holds
    |.p^q.| = |.p.|^|.q.|;

  theorem :: POLYNOM5:14
     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.|;

  theorem :: POLYNOM5:15
   for p be FinSequence of the carrier of F_Complex holds
    |.Sum p.| <= Sum|.p.|;

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
:: POLYNOM5:def 2
    (power Polynom-Ring L).(p,n);
  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;
  end;

  theorem :: POLYNOM5:16
   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);

  theorem :: POLYNOM5:17
     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;

  theorem :: POLYNOM5:18
     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;

  theorem :: POLYNOM5:19
     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;

  theorem :: POLYNOM5:20
   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;

  theorem :: POLYNOM5:21
   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);

  theorem :: POLYNOM5:22
     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);

  theorem :: POLYNOM5:23
   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);

  theorem :: POLYNOM5:24
   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;

  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
:: POLYNOM5:def 3
    for n be Nat holds it.n = v*p.n;
  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;
  end;

  theorem :: POLYNOM5:25
   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;

  theorem :: POLYNOM5:26
   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;

  theorem :: POLYNOM5:27
   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);

  theorem :: POLYNOM5:28
   for L be left_unital (non empty multLoopStr)
   for p be sequence of L holds
    1_(L)*p = p;

  theorem :: POLYNOM5:29
   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);

  theorem :: POLYNOM5:30
   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%>;

  theorem :: POLYNOM5:31
   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);

  theorem :: POLYNOM5:32
   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;

  definition
   let L be non empty ZeroStr;
   let z0,z1 be Element of L;
   func <%z0,z1%> -> sequence of L equals
:: POLYNOM5:def 4
    0_.(L)+*(0,z0)+*(1,z1);
  end;

  theorem :: POLYNOM5:33
   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;

  theorem :: POLYNOM5:34
   for L be non empty ZeroStr
   for z0 be Element of L st z0 <> 0.L holds
    len <%z0%> = 1;

  theorem :: POLYNOM5:35
   for L be non empty ZeroStr holds
    <%0.L%> = 0_.(L);

  theorem :: POLYNOM5:36
   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%>;

  theorem :: POLYNOM5:37
   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)%>;

  theorem :: POLYNOM5:38
     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;

  theorem :: POLYNOM5:39
   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;

  definition
   let L be non empty ZeroStr;
   let z0,z1 be Element of L;
   cluster <%z0,z1%> -> finite-Support;
  end;

  theorem :: POLYNOM5:40
   for L be non empty ZeroStr
   for z0,z1 be Element of L holds
    len <%z0,z1%> <= 2;

  theorem :: POLYNOM5:41
   for L be non empty ZeroStr
   for z0,z1 be Element of L st z1 <> 0.L holds
    len <%z0,z1%> = 2;

  theorem :: POLYNOM5:42
   for L be non empty ZeroStr
   for z0 be Element of L st z0 <> 0.L holds
    len <%z0,0.L%> = 1;

  theorem :: POLYNOM5:43
   for L be non empty ZeroStr holds
    <%0.L,0.L%> = 0_.(L);

  theorem :: POLYNOM5:44
     for L be non empty ZeroStr
   for z0 be Element of L holds
    <%z0,0.L%> = <%z0%>;

  theorem :: POLYNOM5:45
   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;

  theorem :: POLYNOM5:46
     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;

  theorem :: POLYNOM5:47
     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;

  theorem :: POLYNOM5:48
   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;

  theorem :: POLYNOM5:49
     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;

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
:: POLYNOM5:def 5
    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));
  end;

  theorem :: POLYNOM5:50
   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);

  theorem :: POLYNOM5:51
     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%>;

  theorem :: POLYNOM5:52
     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;

  theorem :: POLYNOM5:53
   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;

  theorem :: POLYNOM5:54
   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));

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
:: POLYNOM5:def 6
    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
:: POLYNOM5:def 7
    ex x be Element of L st x is_a_root_of p;
  end;

  theorem :: POLYNOM5:55
   for L be unital (non empty doubleLoopStr) holds
    0_.(L) is with_roots;

  definition
   let L be unital (non empty doubleLoopStr);
   cluster 0_.(L) -> with_roots;
  end;

  theorem :: POLYNOM5:56
     for L be unital (non empty doubleLoopStr)
   for x be Element of L holds
    x is_a_root_of 0_.(L);

  definition
   let L be unital (non empty doubleLoopStr);
   cluster with_roots Polynomial of L;
  end;

  definition
   let L be unital (non empty doubleLoopStr);
   attr L is algebraic-closed means
:: POLYNOM5:def 8
    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
:: POLYNOM5:def 9
    for x be Element of L holds
     x in it iff x is_a_root_of p;
  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
:: POLYNOM5:def 10
    for n be Nat holds it.n = p.n / p.(len p-'1);
  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;
  end;

  theorem :: POLYNOM5:57
   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);

  theorem :: POLYNOM5:58
   for L be Field
   for p be Polynomial of L st len p <> 0 holds
    len NormPolynomial(p) = len p;

  theorem :: POLYNOM5:59
   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);

  theorem :: POLYNOM5:60
   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);

  theorem :: POLYNOM5:61
   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;

  theorem :: POLYNOM5:62
     for L be Field
   for p be Polynomial of L st len p <> 0 holds
    Roots(p) = Roots(NormPolynomial p);

  theorem :: POLYNOM5:63
   id(COMPLEX) is_continuous_on COMPLEX;

  theorem :: POLYNOM5:64
   for x be Element of COMPLEX holds
    COMPLEX --> x is_continuous_on COMPLEX;

  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
:: POLYNOM5:def 11
    for y be Element of L holds it.y = x*(power L).(y,n);
  end;

  theorem :: POLYNOM5:65
     for L be unital (non empty HGrStr) holds
    FPower(1.(L),1) = id(the carrier of L);

  theorem :: POLYNOM5:66
     FPower(1_(F_Complex),2) = id(COMPLEX)(#)id(COMPLEX);

  theorem :: POLYNOM5:67
   for L be unital (non empty HGrStr)
   for x be Element of L holds
    FPower(x,0) = (the carrier of L) --> x;

  theorem :: POLYNOM5:68
     for x be Element of F_Complex
   ex x1 be Element of COMPLEX st
    x = x1 & FPower(x,1) = x1(#)id(COMPLEX);

  theorem :: POLYNOM5:69
     for x be Element of F_Complex
   ex x1 be Element of COMPLEX st
    x = x1 & FPower(x,2) = x1(#)(id(COMPLEX)(#)id(COMPLEX));

  theorem :: POLYNOM5:70
   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);

  theorem :: POLYNOM5:71
   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;

  definition
   let L be unital (non empty doubleLoopStr);
   let p be Polynomial of L;
   func Polynomial-Function(L,p) -> map of L,L means
:: POLYNOM5:def 12
    for x be Element of L holds it.x = eval(p,x);
  end;

  theorem :: POLYNOM5:72
   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;

  theorem :: POLYNOM5:73
   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;

  theorem :: POLYNOM5:74
   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).|;

  theorem :: POLYNOM5:75
   for p be Polynomial of F_Complex st len p > 1 holds
    p is with_roots;

  definition
   cluster F_Complex -> algebraic-closed;
  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));
  end;