:: Fundamental Theorem of Algebra
::  by Robert Milewski
::
:: Received August 21, 2000
:: Copyright (c) 2000-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, CARD_1, RELAT_1, ARYTM_1, ARYTM_3, XXREAL_0,
      REAL_1, FINSEQ_1, FUNCT_1, CARD_3, ORDINAL4, TARSKI, PARTFUN1, XBOOLE_0,
      HAHNBAN1, XCMPLX_0, COMPLFLD, SUPINF_2, COMPLEX1, GROUP_1, POWER,
      STRUCT_0, NAT_1, RLVECT_1, ALGSTR_0, VECTSP_1, BINOP_1, LATTICES,
      POLYNOM1, ALGSEQ_1, POLYNOM3, POLYNOM2, VECTSP_2, MESFUNC1, AFINSQ_1,
      FUNCT_4, CQC_LANG, CFCONT_1, FUNCOP_1, VALUED_1, FUNCT_2, SEQ_4,
      XXREAL_2, COMSEQ_1, VALUED_0, SEQ_2, ORDINAL2, SEQ_1, COMPTRIG, RFINSEQ,
      POLYNOM5, FUNCT_7, ASYMPT_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_2,
      XREAL_0, COMPLEX1, REAL_1, POWER, BINOP_1, NAT_1, RELAT_1, FUNCT_1,
      FUNCT_2, PARTFUN1, FUNCOP_1, FINSEQ_1, FINSEQ_4, POLYNOM1, RVSUM_1,
      STRUCT_0, ALGSTR_0, RLVECT_1, FUNCSDOM, VECTSP_2, VECTSP_1, RFINSEQ,
      CFCONT_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, SEQ_4, XXREAL_0, COMSEQ_1,
      COMSEQ_2, NAT_D, COMPLFLD, HAHNBAN1, ALGSEQ_1, POLYNOM3, POLYNOM4,
      FUNCT_7, RECDEF_1, GROUP_1;
 constructors FINSEQ_4, ENUMSET1, REAL_1, SEQ_4, FINSOP_1, COMSEQ_2, RVSUM_1,
      CFCONT_1, RFINSEQ, NAT_D, FUNCSDOM, VECTSP_2, ALGSTR_1, MATRIX_1,
      HAHNBAN1, POLYNOM1, POLYNOM4, RECDEF_1, BINOP_2, POWER, SEQ_2, RELSET_1,
      FUNCT_7, FVSUM_1, ALGSEQ_1, ORDINAL1, SEQ_1, GROUP_1;
 registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, STRUCT_0, GROUP_1,
      VECTSP_1, COMPLFLD, ALGSTR_1, POLYNOM3, POLYNOM4, VALUED_0, VALUED_1,
      CARD_1, SEQ_2, CFUNCT_1, SEQ_1, RVSUM_1;
 requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;


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 st y > 0 holds min(x,y)/max(x,y) <= 1;

theorem :: POLYNOM5:3
  for x,y be Real st for c be Real 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 Element of NAT st n in
  dom p holds p.n >= 0 for i be Element of NAT st i in dom p holds Sum p >= p.i
;

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**];

definition let R be non empty multMagma;
 let z be Element of R, n be Nat;
 func power(z,n) -> Element of R equals
:: POLYNOM5:def 1
 power(R).(z,n);
end;

theorem :: POLYNOM5:7
  for z be Element of F_Complex st z <> 0.F_Complex
   for n be Nat holds |.power(z,n).| = |.z.| to_power n;

definition
  let p be complex-valued FinSequence;
  redefine func |.p.| -> FinSequence of REAL means
:: POLYNOM5:def 2

  len it = len p &
  for n be Nat st n in dom p holds it.n = |.p.n.|;
end;

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

theorem :: POLYNOM5:9
  for x be Complex holds |.<*x*>.| = <*|.x.|*>;

theorem :: POLYNOM5:10
  for x,y be Complex holds |.<*x,y*>.| = <*|.x.|,|.y.|*>;

theorem :: POLYNOM5:11
  for x,y,z be Complex holds |.<*x,y,z*>.| = <*|.x.|,|.y.|,|.z.|*>;

theorem :: POLYNOM5:12
  for p,q be complex-valued FinSequence holds |.p^q.| = |.p.|^|.q.|;

theorem :: POLYNOM5:13
  for p be complex-valued FinSequence
  for x be Complex holds
  |.p^<*x*>.| = |.p.|^<*|.x.|*> & |.<*x*>^p.| = <*|.x.|*>^|.p.|;

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

registration
  let L be Abelian add-associative right_zeroed right_complementable
  right_unital commutative distributive non empty doubleLoopStr;
  let p be Polynomial of L;
  let n be Nat;
  cluster p`^n -> finite-Support;
end;

theorem :: POLYNOM5:15
  for L be Abelian add-associative right_zeroed
  right_complementable well-unital commutative distributive non empty
  doubleLoopStr for p be Polynomial of L holds p`^0 = 1_.(L);

theorem :: POLYNOM5:16
  for L be Abelian add-associative right_zeroed right_complementable
  well-unital commutative distributive non empty doubleLoopStr for p be
  Polynomial of L holds p`^1 = p;

theorem :: POLYNOM5:17
  for L be Abelian add-associative right_zeroed right_complementable
  well-unital commutative distributive non empty doubleLoopStr for p be
  Polynomial of L holds p`^2 = p*'p;

theorem :: POLYNOM5:18
  for L be Abelian add-associative right_zeroed right_complementable
  well-unital commutative distributive non empty doubleLoopStr for p be
  Polynomial of L holds p`^3 = p*'p*'p;

theorem :: POLYNOM5:19
  for L be Abelian add-associative right_zeroed
  right_complementable well-unital commutative distributive non empty
doubleLoopStr for p be Polynomial of L for n be Nat holds p`^(n+1)
  = (p`^n)*'p;

theorem :: POLYNOM5:20
  for L be Abelian add-associative right_zeroed
  right_complementable well-unital commutative distributive non empty
  doubleLoopStr for n be Element of NAT holds 0_.(L)`^(n+1) = 0_.(L);

theorem :: POLYNOM5:21
  for L be Abelian add-associative right_zeroed right_complementable
well-unital commutative distributive non empty doubleLoopStr
  for n be Nat holds 1_.(L)`^n = 1_.(L);

theorem :: POLYNOM5:22
  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:23
  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 multMagma;
  let p be sequence of L;
  let v be Element of L;
  func v*p -> sequence of L means
:: POLYNOM5:def 4

  for n be Element of NAT holds it.n = v*p.n;
end;

registration
  let L be add-associative right_zeroed right_complementable
  right-distributive non empty doubleLoopStr;
  let p be Polynomial of L;
  let v be Element of L;
  cluster v*p -> finite-Support;
end;

theorem :: POLYNOM5:24
  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:25
  for L be add-associative right_zeroed right_complementable
  well-unital commutative associative distributive almost_left_invertible non
empty doubleLoopStr for p be Polynomial of L for v be Element of L st v <> 0.L
  holds len (v*p) = len p;

theorem :: POLYNOM5:26
  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:27
  for L be well-unital non empty multLoopStr for p be sequence
  of L holds 1.L*p = p;

theorem :: POLYNOM5:28
  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:29
  for L be add-associative right_zeroed right_complementable
well-unital right-distributive non empty doubleLoopStr for v be Element of L
  holds v*1_.(L) = <%v%>;

theorem :: POLYNOM5:30
  for L be add-associative right_zeroed right_complementable
  well-unital distributive commutative associative almost_left_invertible non
  empty doubleLoopStr for p be Polynomial of L for v,x be Element of L holds
  eval(v*p,x) = v*eval(p,x);

theorem :: POLYNOM5:31
  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 5
  0_.(L)+*(0,z0)+*(1,z1);
end;

theorem :: POLYNOM5:32
  for L be non empty ZeroStr for z0 be Element of L holds <%z0%>.0
  = z0 & for n be Element of NAT st n >= 1 holds <%z0%>.n = 0.L;

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

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

theorem :: POLYNOM5:35
  for L be add-associative right_zeroed right_complementable
  distributive commutative associative well-unital domRing-like non empty
  doubleLoopStr for x,y be Element of L holds <%x%>*'<%y%> = <%x*y%>;

theorem :: POLYNOM5:36
  for L be Abelian add-associative right_zeroed
  right_complementable well-unital associative commutative distributive
almost_left_invertible non empty doubleLoopStr for x be Element of L
  for n be Nat holds <%x%>`^n = <%power(x,n)%>;

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

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

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

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

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

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

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

theorem :: POLYNOM5:44
  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:45
  for L be add-associative right_zeroed right_complementable
left-distributive well-unital non empty doubleLoopStr for z0,z1,x be Element
  of L holds eval(<%z0,0.L%>,x) = z0;

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(<%0.L,z1%>,x) = z1*x;

theorem :: POLYNOM5:47
  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: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(<%0.L,1.L%>,x) = x;

begin  :: Substitution in Polynomials

definition
  let L be Abelian add-associative right_zeroed right_complementable
  well-unital commutative distributive non empty doubleLoopStr;
  let p,q be Polynomial of L;
  func Subst(p,q) -> Polynomial of L means
:: POLYNOM5:def 6

  ex F be FinSequence of the
  carrier of Polynom-Ring L st it = Sum F & len F = len p & for n be Element of
  NAT st n in dom F holds F.n = p.(n-'1)*(q`^(n-'1));
end;

theorem :: POLYNOM5:49
  for L be Abelian add-associative right_zeroed
  right_complementable well-unital commutative distributive non empty
  doubleLoopStr for p be Polynomial of L holds Subst(0_.(L),p) = 0_.(L);

theorem :: POLYNOM5:50
  for L be Abelian add-associative right_zeroed right_complementable
  well-unital commutative distributive non empty doubleLoopStr for p be
  Polynomial of L holds Subst(p,0_.(L)) = <%p.0%>;

theorem :: POLYNOM5:51
  for L be Abelian add-associative right_zeroed right_complementable
  well-unital associative commutative distributive almost_left_invertible non
  empty doubleLoopStr for p be Polynomial of L for x be Element of L holds len
  Subst(p,<%x%>) <= 1;

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

  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 8

  ex x be Element of L st x is_a_root_of p;
end;

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

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

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

registration
  let L be unital non empty doubleLoopStr;
  cluster with_roots for Polynomial of L;
end;

definition
  let L be unital non empty doubleLoopStr;
  attr L is algebraic-closed means
:: POLYNOM5:def 9

  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 10

  for x be Element of L holds x in it iff x is_a_root_of p;
end;

definition
  let L be commutative associative well-unital distributive
  almost_left_invertible non empty doubleLoopStr;
  let p be Polynomial of L;
  func NormPolynomial(p) -> sequence of L means
:: POLYNOM5:def 11

  for n be Element of NAT holds it.n = p.n / p.(len p-'1);
end;

registration
  let L be add-associative right_zeroed right_complementable commutative
  associative well-unital distributive almost_left_invertible non empty
  doubleLoopStr;
  let p be Polynomial of L;
  cluster NormPolynomial(p) -> finite-Support;
end;

theorem :: POLYNOM5:56
  for L be commutative associative well-unital distributive
  almost_left_invertible non empty doubleLoopStr for p be Polynomial of L st
  len p <> 0 holds (NormPolynomial p).(len p-'1) = 1.L;

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

theorem :: POLYNOM5:58
  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:59
  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:60
  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:61
  for L be Field for p be Polynomial of L st len p <> 0 holds Roots(p) =
  Roots(NormPolynomial p);

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

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

definition
  let L be unital non empty multMagma;
  let x be Element of L;
  let n be Nat;
  func FPower(x,n) -> Function of L,L means
:: POLYNOM5:def 12

  for y be Element of L holds it.y = x*power(y,n);
end;

theorem :: POLYNOM5:64
  for L be unital non empty multMagma holds FPower(1_L,1) = id(the
  carrier of L);

theorem :: POLYNOM5:65
  FPower(1_F_Complex,2) = id(COMPLEX)(#)id(COMPLEX);

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

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

theorem :: POLYNOM5:68
  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:69
  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:70
  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 well-unital non empty doubleLoopStr;
  let p be Polynomial of L;
  func Polynomial-Function(L,p) -> Function of L,L means
:: POLYNOM5:def 13

  for x be Element of L holds it.x = eval(p,x);
end;

theorem :: POLYNOM5:71
  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:72
  for p be Polynomial of F_Complex st len p > 2 & |.p.(len p-'1).|
=1 for F be FinSequence of REAL st len F = len p & for n be Element of NAT st n
in dom F holds F.n = |.p.(n-'1).| for z be Element of F_Complex st |.z.| > Sum
  F holds |.eval(p,z).| > |.p.0 .|+1;

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

::$N Fundamental Theorem of Algebra
theorem :: POLYNOM5:74
  for p be Polynomial of F_Complex st len p > 1 holds p is with_roots;

registration
  cluster F_Complex -> algebraic-closed;
end;

registration
  cluster algebraic-closed add-associative right_zeroed right_complementable
    Abelian commutative associative distributive almost_left_invertible non
    degenerated for well-unital non empty doubleLoopStr;
end;