{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T00:55:40Z","timestamp":1777424140633,"version":"3.51.4"},"reference-count":16,"publisher":"Walter de Gruyter GmbH","issue":"4","license":[{"start":{"date-parts":[[2016,12,1]],"date-time":"2016-12-01T00:00:00Z","timestamp":1480550400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-sa\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,12,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n               <jats:p>This article formalizes the proof of Niven\u2019s theorem [12] which states that if <jats:italic>x\/\u03c0<\/jats:italic> and <jats:italic>sin<\/jats:italic>(<jats:italic>x<\/jats:italic>) are both rational, then the sine takes values 0, \u00b11\/2, and \u00b11. The main part of the formalization follows the informal proof presented at Pr\u221efWiki (<jats:ext-link xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" ext-link-type=\"uri\" xlink:href=\"https:\/\/proofwiki.org\/wiki\/Niven\u2019s_Theorem#Source_of_Name\">https:\/\/proofwiki.org\/wiki\/Niven\u2019s_Theorem#Source_of_Name<\/jats:ext-link>). 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].<\/jats:p>","DOI":"10.1515\/forma-2016-0026","type":"journal-article","created":{"date-parts":[[2017,2,25]],"date-time":"2017-02-25T10:00:53Z","timestamp":1488016853000},"page":"301-308","source":"Crossref","is-referenced-by-count":4,"title":["Niven\u2019s Theorem"],"prefix":"10.1515","volume":"24","author":[{"given":"Artur","family":"Korni\u0142owicz","sequence":"first","affiliation":[{"name":"Institute of Informatics, University of Bia\u0142ystok, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Naumowicz","sequence":"additional","affiliation":[{"name":"Institute of Informatics, University of Bia\u0142ystok, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2017,2,23]]},"reference":[{"key":"2021040711054614162_j_forma-2016-0026_ref_001_w2aab2b8c11b1b7b1ab1ab1Aa","unstructured":"[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41\u201346, 1990."},{"key":"2021040711054614162_j_forma-2016-0026_ref_002_w2aab2b8c11b1b7b1ab1ab2Aa","unstructured":"[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107\u2013114, 1990."},{"key":"2021040711054614162_j_forma-2016-0026_ref_003_w2aab2b8c11b1b7b1ab1ab3Aa","unstructured":"[3] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485\u2013492, 1996."},{"key":"2021040711054614162_j_forma-2016-0026_ref_004_w2aab2b8c11b1b7b1ab1ab4Aa","unstructured":"[4] Czes\u0142aw Byli\u0144ski. The sum and product of finite sequences of real numbers. Formalized Mathematics, 1(4):661\u2013668, 1990."},{"key":"2021040711054614162_j_forma-2016-0026_ref_005_w2aab2b8c11b1b7b1ab1ab5Aa","unstructured":"[5] Czes\u0142aw Byli\u0144ski. Some basic properties of sets. Formalized Mathematics, 1(1):47\u201353, 1990."},{"key":"2021040711054614162_j_forma-2016-0026_ref_006_w2aab2b8c11b1b7b1ab1ab6Aa","unstructured":"[6] Yuzhong Ding and Xiquan Liang. Formulas and identities of trigonometric functions. Formalized Mathematics, 12(3):243\u2013246, 2004."},{"key":"2021040711054614162_j_forma-2016-0026_ref_007_w2aab2b8c11b1b7b1ab1ab7Aa","unstructured":"[7] Magdalena Jastrz\u0119bska and Adam Grabowski. Some properties of Fibonacci numbers. Formalized Mathematics, 12(3):307\u2013313, 2004."},{"key":"2021040711054614162_j_forma-2016-0026_ref_008_w2aab2b8c11b1b7b1ab1ab8Aa","doi-asserted-by":"crossref","unstructured":"[8] J.D. King. Integer roots of polynomials. The Mathematical Gazette, 90(519):455\u2013456, 2006. doi:http:\/\/dx.doi.org\/10.1017\/S0025557200180295.","DOI":"10.1017\/S0025557200180295"},{"key":"2021040711054614162_j_forma-2016-0026_ref_009_w2aab2b8c11b1b7b1ab1ab9Aa","unstructured":"[9] Serge Lang. Algebra. Addison-Wesley, 1980."},{"key":"2021040711054614162_j_forma-2016-0026_ref_010_w2aab2b8c11b1b7b1ab1ac10Aa","unstructured":"[10] Robert Milewski. The evaluation of polynomials. Formalized Mathematics, 9(2):391\u2013395, 2001."},{"key":"2021040711054614162_j_forma-2016-0026_ref_011_w2aab2b8c11b1b7b1ab1ac11Aa","unstructured":"[11] Robert Milewski. Fundamental theorem of algebra. Formalized Mathematics, 9(3):461\u2013470, 2001."},{"key":"2021040711054614162_j_forma-2016-0026_ref_012_w2aab2b8c11b1b7b1ab1ac12Aa","unstructured":"[12] 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."},{"key":"2021040711054614162_j_forma-2016-0026_ref_013_w2aab2b8c11b1b7b1ab1ac13Aa","unstructured":"[13] Piotr Rudnicki. Little Bezout theorem (factor theorem). Formalized Mathematics, 12(1): 49\u201358, 2004."},{"key":"2021040711054614162_j_forma-2016-0026_ref_014_w2aab2b8c11b1b7b1ab1ac14Aa","unstructured":"[14] Andrzej Trybulec. Binary operations applied to functions. Formalized Mathematics, 1 (2):329\u2013334, 1990."},{"key":"2021040711054614162_j_forma-2016-0026_ref_015_w2aab2b8c11b1b7b1ab1ac15Aa","unstructured":"[15] Micha\u0142 J. Trybulec. Integers. Formalized Mathematics, 1(3):501\u2013505, 1990."},{"key":"2021040711054614162_j_forma-2016-0026_ref_016_w2aab2b8c11b1b7b1ab1ac16Aa","unstructured":"[16] Wojciech A. Trybulec. Vectors in real linear space. Formalized Mathematics, 1(2):291\u2013296, 1990."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/content.sciendo.com\/view\/journals\/forma\/24\/4\/article-p301.xml","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0026","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,8]],"date-time":"2021-04-08T00:43:54Z","timestamp":1617842634000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.1515\/forma-2016-0026"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,1]]},"references-count":16,"journal-issue":{"issue":"4","published-online":{"date-parts":[[2017,2,23]]},"published-print":{"date-parts":[[2016,12,1]]}},"alternative-id":["10.1515\/forma-2016-0026"],"URL":"https:\/\/doi.org\/10.1515\/forma-2016-0026","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2016,12,1]]}}}