# All Liouville Numbers are Transcendental

Artur Korniłowicz; Adam Naumowicz; Adam Grabowski

Formalized Mathematics (2017)

- Volume: 25, Issue: 1, page 49-54
- ISSN: 1426-2630

## Access Full Article

top## Abstract

top## How to cite

topArtur Korniłowicz, Adam Naumowicz, and Adam Grabowski. "All Liouville Numbers are Transcendental." Formalized Mathematics 25.1 (2017): 49-54. <http://eudml.org/doc/288123>.

@article{ArturKorniłowicz2017,

abstract = {In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 [15] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real number x is a Liouville number iff for every positive integer n, there exist integers p and q such that q > 1 and [...] It is easy to show that all Liouville numbers are irrational. The definition and basic notions are contained in [10], [1], and [12]. Liouvile constant, which is defined formally in [12], is the first explicit transcendental (not algebraic) number, another notable examples are e and π [5], [11], and [4]. Algebraic numbers were formalized with the help of the Mizar system [13] very recently, by Yasushige Watase in [23] and now we expand these techniques into the area of not only pure algebraic domains (as fields, rings and formal polynomials), but also for more settheoretic fields. Finally we show that all Liouville numbers are transcendental, based on Liouville’s theorem on Diophantine approximation.},

author = {Artur Korniłowicz, Adam Naumowicz, Adam Grabowski},

journal = {Formalized Mathematics},

keywords = {Liouville numbers; Diophantine approximation; transcendental numbers; Liouville’s constant; transcendental number; Liouville's constant},

language = {eng},

number = {1},

pages = {49-54},

title = {All Liouville Numbers are Transcendental},

url = {http://eudml.org/doc/288123},

volume = {25},

year = {2017},

}

TY - JOUR

AU - Artur Korniłowicz

AU - Adam Naumowicz

AU - Adam Grabowski

TI - All Liouville Numbers are Transcendental

JO - Formalized Mathematics

PY - 2017

VL - 25

IS - 1

SP - 49

EP - 54

AB - In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 [15] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real number x is a Liouville number iff for every positive integer n, there exist integers p and q such that q > 1 and [...] It is easy to show that all Liouville numbers are irrational. The definition and basic notions are contained in [10], [1], and [12]. Liouvile constant, which is defined formally in [12], is the first explicit transcendental (not algebraic) number, another notable examples are e and π [5], [11], and [4]. Algebraic numbers were formalized with the help of the Mizar system [13] very recently, by Yasushige Watase in [23] and now we expand these techniques into the area of not only pure algebraic domains (as fields, rings and formal polynomials), but also for more settheoretic fields. Finally we show that all Liouville numbers are transcendental, based on Liouville’s theorem on Diophantine approximation.

LA - eng

KW - Liouville numbers; Diophantine approximation; transcendental numbers; Liouville’s constant; transcendental number; Liouville's constant

UR - http://eudml.org/doc/288123

ER -

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.