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].
@article{bwmeta1.element.doi-10_1515_forma-2016-0026,
author = {Artur Korni\l owicz and Adam Naumowicz},
title = {Niven's Theorem},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {301-308},
zbl = {1357.12004},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0026}
}
Artur Korniłowicz; Adam Naumowicz. Niven’s Theorem. Formalized Mathematics, Tome 24 (2016) pp. 301-308. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0026/