<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

Pubblicato online: 23 feb 2017

Pagine: 301 - 308

Ricevuto: 15 dic 2016

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

Parole chiave
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

Pubblicato online: 23 feb 2017

Pagine: 301 - 308

Ricevuto: 15 dic 2016

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

Parole chiaveNiven’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.

Parole chiave
Niven’s theorem, rational root theorem, integral root theorem