@MISC{LIOUVIL1.MIZ,
  AUTHOR = {Grabowski, Adam and Korni{\l}owicz, Artur},
  TITLE = {Introduction to {L}iouville Numbers},
  SECTION1 = {Preliminaries},
  SECTION2 = {Sequences},
  SECTION3 = {Transformations between Real Functions and Finite Sequences},
  SECTION4 = {Sequences not Vanishing at Infinity},
  SECTION5 = {Liouville Numbers},
  SECTION6 = {Liouville Constant},
  DAY = {23},
  MONTH = {February},
  YEAR = {2017},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  ADDRESS2 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {The article defines Liouville numbers, the object
  introduced by Joseph Liouville in 1844 \cite{Liouville1844}
  as an example of an object which
  can be approximated ``quite closely" by a sequence of rational
  numbers.
  $x$ is a Liouville number iff for every positive
  integer $n$, there exist integers $p$ and $q$ such that $q > 1$ and
  $$0< |x - \frac{p}{q}|<\frac{1}{q^n}.$$
  It is easy to show that all Liouville numbers are irrational.
  Liouville constant, which is also defined formally, is the
  first trascendental (not algebraic) number. At the end, we show that
  the construction of an arbitrary Liouville number leads to Liouville
  numbers. We show additionally, that the set of all Liouville numbers
  is infinite, opening the next item from Abad and Abad's list of ``Top 100
  Theorems". We show also some preliminary constructions linking real
  sequences and finite sequences, where summing formulas are involved.
  In the Mizar proof, we follow closely
  \url{https://en.wikipedia.org/wiki/Liouville_number}. The aim is to
  show that all Liouville numbers are transcendental.}}

@ARTICLE{Liouville1844,
AUTHOR = {Liouville, Joseph},
TITLE = {Nouvelle demonstration d'un theoreme sur les irrationalles
  algebraiques, insere dans le Compte rendu de la derniere
  seance},
JOURNAL = {C. R. Acad. Sci. Paris},
NUMBER = {18},
PAGES = {910--911},
YEAR = {1844}}


