:: Niven's Theorem :: by Artur Korni{\l}owicz and Adam Naumowicz :: :: Received December 15, 2016 :: Copyright (c) 2016-2018 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, RATFUNC1, 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};