:: Niven's Theorem
::  by Artur Korni{\l}owicz and Adam Naumowicz
::
:: Received December 15, 2016
:: Copyright (c) 2016-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 REAL_1, XXREAL_0, CARD_1, SIN_COS, ARYTM_3, RAT_1, ARYTM_1,
      RELAT_1, NAT_1, POLYNOM1, VECTSP_1, SUBSET_1, POLYNOM2, XCMPLX_0,
      HURWITZ, POLYNOM3, FUNCT_4, STRUCT_0, XBOOLE_0, GROUP_1, ALGSTR_0,
      ALGSEQ_1, FUNCT_1, SUPINF_2, NUMBERS, CAT_1, VALUED_0, MESFUNC1,
      FINSEQ_1, AFINSQ_1, RLVECT_1, CARD_3, BINOP_1, TARSKI, SQUARE_1, INT_1,
      XXREAL_1, COMPLEX1, RATFUNC1, POLYNOM5, PARTFUN1, LATTICES, ORDINAL4,
      RFINSEQ, NEWTON, FINSEQ_2, VECTSP_2;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      RELSET_1, PARTFUN1, FUNCT_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
      SQUARE_1, NAT_1, INT_1, RAT_1, VALUED_0, COMPLEX1, INT_2, NAT_D,
      XXREAL_1, FINSEQ_1, FINSEQ_2, RVSUM_1, RFINSEQ, FUNCT_7, NEWTON, SIN_COS,
      STRUCT_0, ALGSTR_0, ALGSTR_1, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2,
      VFUNCT_1, NORMSP_1, FVSUM_1, ALGSEQ_1, POLYNOM3, POLYNOM4, POLYNOM5,
      UPROOTS, HURWITZ, RATFUNC1, RING_4;
 constructors SIN_COS, ALGSEQ_1, POLYNOM4, HURWITZ, FUNCT_7, TOPMETR, POLYNOM5,
      BINOP_2, NAT_D, FINSEQ_4, SQUARE_1, RATFUNC1, RCOMP_1, NEWTON, VFUNCT_1,
      UPROOTS, GR_CY_1, RFINSEQ, FVSUM_1, VECTSP_2, ALGSTR_1;
 registrations XREAL_0, RELAT_1, FUNCT_1, ORDINAL1, RAT_1, SIN_COS, SIN_COS6,
      INT_1, XXREAL_0, INT_6, VECTSP_1, CARD_1, POLYNOM3, FUNCT_7, PRE_POLY,
      STRUCT_0, RLVECT_1, MEMBERED, RELSET_1, POLYNOM5, SQUARE_1, RING_4,
      XCMPLX_0, NUMBERS, FUNCT_2, XBOOLE_0, NAT_1, VFUNCT_1, VALUED_0,
      FINSEQ_1, NEWTON, FINSEQ_2, WSIERP_1, VECTSP_2, ALGSTR_1;
 requirements BOOLE, SUBSET, NUMERALS, REAL, ARITHM;


begin

reserve r,t for Real;
reserve i for Integer;
reserve k,n for Nat;
reserve p for Polynomial of F_Real;
reserve e for Element of F_Real;
reserve L for non empty ZeroStr;
reserve z,z0,z1,z2 for Element of L;

theorem :: NIVEN:1
  for a,b,c,d being Complex st b <> 0 & a/b = c/d holds a = b*c/d;

theorem :: NIVEN:2
  for a,b being Real st |.a.| = b holds a = b or a = -b;

theorem :: NIVEN:3
  |.i.| <= 2 implies i = -2 or i = -1 or i = 0 or i = 1 or i = 2;

theorem :: NIVEN:4
  n <> 0 implies i divides i |^ n;

theorem :: NIVEN:5
  t > 0 implies ex i st t*i <= r <= t*(i+1);

theorem :: NIVEN:6  ::: MATRPROB:36
  for p being FinSequence of F_Real
  for q being real-valued FinSequence st p = q holds Sum p = Sum q;

theorem :: NIVEN:7
  for i being Nat, r being Element of F_Real
  holds power(F_Real).(r,i) = r |^ i;

theorem :: NIVEN:8
  sin(5*PI/6) = 1/2;

theorem :: NIVEN:9
  sin(5*PI/6+2*PI*i) = 1/2;

theorem :: NIVEN:10
  sin(7*PI/6) = -1/2;

theorem :: NIVEN:11
  sin(7*PI/6+2*PI*i) = -1/2;

theorem :: NIVEN:12
  sin(11*PI/6) = -1/2;

theorem :: NIVEN:13
  sin(11*PI/6+2*PI*i) = -1/2;

theorem :: NIVEN:14
  cos(4*PI/3) = -1/2;

theorem :: NIVEN:15
  cos(4*PI/3+2*PI*i) = -1/2;

theorem :: NIVEN:16
  cos(5*PI/3) = 1/2;

theorem :: NIVEN:17
  cos(5*PI/3+2*PI*i) = 1/2;

theorem :: NIVEN:18
  0 <= r <= PI/2 & cos r = 1/2 implies r = PI/3;

theorem :: NIVEN:19  :: POLYNOM3:34'
  for L being add-associative right_zeroed right_complementable
        left-distributive non empty doubleLoopStr
  for p being sequence of L holds
  (0_.L) *' p = 0_.L;

registration
  let L,z,n;
  cluster 0_.L +* (n,z) -> finite-Support for sequence of L;
end;

theorem :: NIVEN:20
  z <> 0.L implies
  for p being Polynomial of L st p = 0_.L +* (n,z) holds len p = n+1;

theorem :: NIVEN:21
  z <> 0.L implies
  for p being Polynomial of L st p = 0_.L +* (n,z) holds deg p = n;

registration
  cluster 0_.F_Real -> INT -valued;
  cluster 1_.F_Real -> INT -valued;
end;

registration
  cluster integer for Element of F_Real;
end;

theorem :: NIVEN:22
  rng <%z%> = {z,0.L};

definition
  let L,z0,z1,z2;
  func <%z0,z1,z2%> -> sequence of L equals
:: NIVEN:def 1
  0_.L +* (0,z0) +* (1,z1) +* (2,z2);
end;

theorem :: NIVEN:23
  <%z0,z1,z2%>.0 = z0;

theorem :: NIVEN:24
  <%z0,z1,z2%>.1 = z1;

theorem :: NIVEN:25
  <%z0,z1,z2%>.2 = z2;

theorem :: NIVEN:26
  3 <= n implies <%z0,z1,z2%>.n = 0.L;

registration
  let L,z0,z1,z2;
  cluster <%z0,z1,z2%> -> finite-Support;
end;

theorem :: NIVEN:27
  len <%z0,z1,z2%> <= 3;

theorem :: NIVEN:28
  z2 <> 0.L implies len <%z0,z1,z2%> = 3;

theorem :: NIVEN:29
  for L being right_zeroed non empty addLoopStr
  for z0,z1 being Element of L holds
  <%z0%> + <%z1%> = <%z0+z1%>;

theorem :: NIVEN:30
  for L being right_zeroed non empty addLoopStr
  for z0,z1,z2,z3 being Element of L holds
  <%z0,z1%> + <%z2,z3%> = <%z0+z2,z1+z3%>;

theorem :: NIVEN:31
  for L being right_zeroed non empty addLoopStr
  for z0,z1,z2,z3,z4,z5 being Element of L holds
  <%z0,z1,z2%> + <%z3,z4,z5%> = <%z0+z3,z1+z4,z2+z5%>;

theorem :: NIVEN:32
  for L being add-associative right_zeroed right_complementable
        non empty addLoopStr
  for z0 being Element of L holds
  - <%z0%> = <%-z0%>;

theorem :: NIVEN:33
  for L being add-associative right_zeroed right_complementable
        non empty addLoopStr
  for z0,z1 being Element of L holds
  - <%z0,z1%> = <%-z0,-z1%>;

theorem :: NIVEN:34
  for L being add-associative right_zeroed right_complementable
        non empty addLoopStr
  for z0,z1,z2 being Element of L holds
  - <%z0,z1,z2%> = <%-z0,-z1,-z2%>;

theorem :: NIVEN:35
  for L being add-associative right_zeroed right_complementable
      non empty addLoopStr
  for z0,z1 being Element of L holds
  <%z0%> - <%z1%> = <%z0-z1%>;

theorem :: NIVEN:36
  for L being add-associative right_zeroed right_complementable
      non empty addLoopStr
  for z0,z1,z2,z3 being Element of L holds
  <%z0,z1%> - <%z2,z3%> = <%z0-z2,z1-z3%>;

theorem :: NIVEN:37
  for L being add-associative right_zeroed right_complementable
      non empty addLoopStr
  for z0,z1,z2,z3,z4,z5 being Element of L holds
  <%z0,z1,z2%> - <%z3,z4,z5%> = <%z0-z3,z1-z4,z2-z5%>;

theorem :: NIVEN:38
  for L being add-associative right_zeroed right_complementable
      left-distributive unital associative non empty doubleLoopStr
  for z0,z1,z2,x being Element of L
  holds eval(<%z0,z1,z2%>,x) = z0+z1*x+z2*x*x;

registration
  let a be integer Element of F_Real;
  cluster <%a%> -> INT -valued;
end;

registration
  let a,b be integer Element of F_Real;
  cluster <%a,b%> -> INT -valued;
end;

registration
  let a,b,c be integer Element of F_Real;
  cluster <%a,b,c%> -> INT -valued;
end;

registration
  cluster monic INT -valued for Polynomial of F_Real;
end;

registration
  cluster INT -valued for FinSequence of F_Real;
end;

registration
  let F be INT -valued FinSequence of F_Real;
  cluster Sum F -> integer;
end;

registration
  let f be INT -valued sequence of F_Real;
  cluster -f -> INT -valued;
  let g be INT -valued sequence of F_Real;
  cluster f+g -> INT -valued;
  cluster f-g -> INT -valued;
  cluster f*'g -> INT -valued;
end;

theorem :: NIVEN:39
  for L being non degenerated non empty doubleLoopStr, z being Element of L
  holds LC <%z,1.L%> = 1.L;

registration
  let L be non degenerated non empty doubleLoopStr;
  let z be Element of L;
  cluster <%z,1.L%> -> monic;
end;

theorem :: NIVEN:40
  for L being non degenerated non empty doubleLoopStr, z1,z2 being Element of L
  holds LC <%z1,z2,1.L%> = 1.L;

registration
  let L be non degenerated non empty doubleLoopStr;
  let z1,z2 be Element of L;
  cluster <%z1,z2,1.L%> -> monic;
end;

registration
  let p be INT -valued Polynomial of F_Real;
  cluster LC p -> integer;
end;

theorem :: NIVEN:41
  for L being add-associative right_zeroed right_complementable
      non empty addLoopStr
  for p being Polynomial of L holds
  deg(-p) = deg p;

theorem :: NIVEN:42
  for L being add-associative right_zeroed right_complementable
      non empty addLoopStr
  for p,q being Polynomial of L st deg p > deg q holds
  deg(p+q) = deg p;

theorem :: NIVEN:43
  for L being add-associative right_zeroed right_complementable
      non empty addLoopStr
  for p,q being Polynomial of L st deg p > deg q holds
  deg(p-q) = deg p;

theorem :: NIVEN:44
  for L being add-associative right_zeroed right_complementable
      non empty addLoopStr
  for p,q being Polynomial of L st deg p < deg q holds
  deg(p-q) = deg q;

theorem :: NIVEN:45
  for L being add-associative right_zeroed right_complementable distributive
      non degenerated doubleLoopStr
  for p being Polynomial of L holds
  LC p = -LC -p;

theorem :: NIVEN:46
for L being add-associative right_zeroed right_complementable
            distributive associative well-unital domRing-like
            non degenerated doubleLoopStr
for p,q being Polynomial of L holds LC(p *' q) = LC(p) * LC(q);

theorem :: NIVEN:47
  for L being add-associative right_zeroed right_complementable distributive
      non degenerated doubleLoopStr
  for p being monic Polynomial of L
  for q being Polynomial of L st deg p > deg q holds
  p+q is monic;

theorem :: NIVEN:48
  for L being add-associative right_zeroed right_complementable distributive
         non degenerated doubleLoopStr
  for p being monic Polynomial of L
  for q being Polynomial of L st deg p > deg q holds
  p-q is monic;

registration
  let L be add-associative right_zeroed right_complementable
  associative well-unital almost_left_invertible distributive non
  degenerated doubleLoopStr;
  let p,q be monic Polynomial of L;
  cluster p*'q -> monic;
end;

theorem :: NIVEN:49
  for L being Abelian add-associative right_zeroed right_complementable
        unital distributive non empty doubleLoopStr
  for z1,z2 being Element of L
  for p being Polynomial of L st eval(p,z1) = z2
  holds eval(p-<%z2%>,z1) = 0.L;

::$N Rational root theorem
theorem :: NIVEN:50
  for p being INT -valued Polynomial of F_Real
  for e being Element of F_Real st e is_a_root_of p
  for k,l being Integer st l <> 0 & e = k/l & k,l are_coprime
  holds k divides p.0 & l divides LC p;

::$N Integral root theorem
theorem :: NIVEN:51
  for p being monic INT -valued Polynomial of F_Real
  for e being rational Element of F_Real st e is_a_root_of p
  holds e is integer;

theorem :: NIVEN:52
  1 <= n & e = 2*cos t implies
  ex p being monic INT -valued Polynomial of F_Real
  st eval(p,e) = 2*cos(n*t) & deg p = n &
  (n = 1 implies p = <%0.F_Real,1.F_Real%>) &
  (n = 2 implies
    ex r being Element of F_Real st r = -2 & p = <%r,0.F_Real,1.F_Real%>);

theorem :: NIVEN:53
  0 <= r <= PI/2 & r/PI is rational & cos r is rational implies
  r in {0,PI/3,PI/2};

theorem :: NIVEN:54
  2*PI*i <= r <= PI/2 + 2*PI*i & r/PI is rational & cos r is rational implies
  r in { 2*PI*i , PI/3+2*PI*i , PI/2+2*PI*i };

theorem :: NIVEN:55
  PI/2 <= r <= PI & r/PI is rational & cos r is rational implies
  r in {PI/2,2*PI/3,PI};

theorem :: NIVEN:56
  PI/2 + 2*PI*i <= r <= PI + 2*PI*i & r/PI is rational & cos r is rational
  implies
  r in { PI/2+2*PI*i , 2*PI/3+2*PI*i , PI+2*PI*i };

theorem :: NIVEN:57
  PI <= r <= 3*PI/2 & r/PI is rational & cos r is rational implies
  r in {PI,4*PI/3,3*PI/2};

theorem :: NIVEN:58
  PI + 2*PI*i <= r <= 3*PI/2 + 2*PI*i & r/PI is rational & cos r is rational
  implies
  r in { PI+2*PI*i , 4*PI/3+2*PI*i , 3*PI/2+2*PI*i };

theorem :: NIVEN:59
  3*PI/2 <= r <= 2*PI & r/PI is rational & cos r is rational implies
  r in {3*PI/2,5*PI/3,2*PI};

theorem :: NIVEN:60
  3*PI/2 + 2*PI*i <= r <= 2*PI + 2*PI*i & r/PI is rational & cos r is rational
  implies
  r in { 3*PI/2+2*PI*i , 5*PI/3+2*PI*i , 2*PI+2*PI*i };

theorem :: NIVEN:61
  r/PI is rational & cos r is rational implies cos r in {0,1,-1,1/2,-1/2};

theorem :: NIVEN:62
  0 <= r <= PI/2 & r/PI is rational & sin r is rational implies
  r in {0,PI/6,PI/2};

theorem :: NIVEN:63
  2*PI*i <= r <= PI/2 + 2*PI*i & r/PI is rational & sin r is rational implies
  r in { 2*PI*i , PI/6+2*PI*i , PI/2+2*PI*i };

theorem :: NIVEN:64
  PI/2 <= r <= PI & r/PI is rational & sin r is rational implies
  r in {PI/2,5*PI/6,PI};

theorem :: NIVEN:65
  PI/2 + 2*PI*i <= r <= PI + 2*PI*i & r/PI is rational & sin r is rational
  implies
  r in { PI/2+2*PI*i , 5*PI/6+2*PI*i , PI+2*PI*i };

theorem :: NIVEN:66
  PI <= r <= 3*PI/2 & r/PI is rational & sin r is rational implies
  r in {PI,7*PI/6,3*PI/2};

theorem :: NIVEN:67
  PI + 2*PI*i <= r <= 3*PI/2 + 2*PI*i & r/PI is rational & sin r is rational
  implies
  r in { PI+2*PI*i , 7*PI/6+2*PI*i , 3*PI/2+2*PI*i };

theorem :: NIVEN:68
  3*PI/2 <= r <= 2*PI & r/PI is rational & sin r is rational implies
  r in {3*PI/2,11*PI/6,2*PI};

theorem :: NIVEN:69
  3*PI/2 + 2*PI*i <= r <= 2*PI + 2*PI*i & r/PI is rational & sin r is rational
  implies
  r in { 3*PI/2+2*PI*i , 11*PI/6+2*PI*i , 2*PI+2*PI*i };

::$N Niven's Theorem
theorem :: NIVEN:70
  r/PI is rational & sin r is rational implies sin r in {0, 1, -1, 1/2, -1/2};