@MISC{LIOUVIL2.MIZ,
  AUTHOR = {Korni{\l}owicz, Artur and Naumowicz, Adam and Grabowski, Adam},
  TITLE = {All Liouville Numbers are Transcendental},
  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},
  ADDRESS3 = {Institute of Informatics\\University of Bia{\l}ystok\\Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {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.
  Liouville numbers were 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 and
  such definition and basic notions are contained in \cite{LIOUVIL1.ABS}.
  Liouville constant, which is also defined formally, is the
  first transcendental (not algebraic) number.
  Algebraic numbers were formalized with the help of the Mizar system
  very recently, by Yasushige Watase in \cite{ALGNUM_1.ABS} and now we
  expand these techniques into the are of not only pure algebraic
  domains (as field, rings and formal polynomials), but also for more
  set-theoretic fields. Finally we show that all Liouville numbers are
  transcendental, based on Liouville's theorem on diophantine
  approximation.}}

@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}}


