<abstract xmlns="http://www.w3.org/1999/xhtml"><p>This article formalizes the proof of Niven’s theorem [<xref ref-type="bibr" rid="j_forma-2016-0026_ref_012_w2aab2b8c11b1b7b1ab1ac12Aa">12</xref>] which states that if <italic>x/π</italic> and <italic>sin</italic>(<italic>x</italic>) 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 (<ext-link ext-link-type="uri" xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name">https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name</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 [<xref ref-type="bibr" rid="j_forma-2016-0026_ref_008_w2aab2b8c11b1b7b1ab1ab8Aa">8</xref>, <xref ref-type="bibr" rid="j_forma-2016-0026_ref_009_w2aab2b8c11b1b7b1ab1ab9Aa">9</xref>].</p></abstract>

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].

Niven’s Theorem

Institute of Informatics, University of Białystok,

Formalized Mathematics

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

{"article-title":"Niven\u2019s 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....

Niven’s Theorem

Publicado en línea: 23 feb 2017

Páginas: 301 - 308

Recibido: 15 dic 2016

DOI: https://doi.org/10.1515/forma-2016-0026

Palabras clave
Niven’s theorem, rational root theorem, integral root theorem

© 2016 Artur Korniłowicz et al., published by De Gruyter Open

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Niven’s Theorem

Publicado en línea: 23 feb 2017

Páginas: 301 - 308

Recibido: 15 dic 2016

DOI: https://doi.org/10.1515/forma-2016-0026

Palabras claveNiven’s theorem, rational root theorem, integral root theorem

© 2016 Artur Korniłowicz et al., published by De Gruyter Open

This work is licensed under version 3.0 of the Creative Commons Attribution–ShareAlike License.

Palabras clave
Niven’s theorem, rational root theorem, integral root theorem