Niven’s Theorem

This article formalizes the proof of Niven’s theorem [12] which states that if x/π and sin(x) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞fWiki (https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name). For this proof, we have also formalized the rational and integral root theorems setting constraints on solutions of polynomial equations with integer coefficients [8, 9].Korniłowicz Artur - Institute of Informatics, University of Białystok, PolandNaumowicz Adam - Institute of Informatics, University of Białystok, PolandGrzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990.Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990.Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485–492, 1996.Czesław Byliński. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661–668, 1990.Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990.Yuzhong Ding and Xiquan Liang. Formulas and identities of trigonometric functions. Formalized Mathematics, 12(3):243–246, 2004.Magdalena Jastrzębska and Adam Grabowski. Some properties of Fibonacci numbers. Formalized Mathematics, 12(3):307–313, 2004.J.D. King. Integer roots of polynomials. The Mathematical Gazette, 90(519):455–456, 2006. doi:http://dx.doi.org/10.1017/S0025557200180295.Serge Lang. Algebra. Addison-Wesley, 1980.Robert Milewski. The evaluation of polynomials. Formalized Mathematics, 9(2):391–395, 2001.Robert Milewski. Fundamental theorem of algebra. Formalized Mathematics, 9(3):461–470, 2001.Ivan Niven. Irrational numbers. The Carus Mathematical Monographs, No. 11. The Mathematical Association of America. Distributed by John Wiley and Sons, Inc., New York, N.Y., 1956.Piotr Rudnicki. Little Bezout theorem (factor theorem). Formalized Mathematics, 12(1): 49–58, 2004.Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329–334, 1990.Michał J. Trybulec. Integers. Formalized Mathematics, 1(3):501–505, 1990.Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291–296, 1990