<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

Online veröffentlicht: 23. Feb. 2017

Seitenbereich: 301 - 308

Eingereicht: 15. Dez. 2016

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

Schlüsselwörter
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

Online veröffentlicht: 23. Feb. 2017

Seitenbereich: 301 - 308

Eingereicht: 15. Dez. 2016

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

SchlüsselwörterNiven’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.

Schlüsselwörter
Niven’s theorem, rational root theorem, integral root theorem