@MISC{IRRAT_1.MIZ,
  AUTHOR = {Wiedijk, Freek},
  TITLE = {Irrationality of $e$},
  SECTION1 = {Square Roots of Primes are Irrational},
  SECTION2 = {A proof that $e = e$},
  SECTION3 = {The Number $e$ is Irrational},
  DAY = {02},
  MONTH = {July},
  YEAR = {1999},
  ADDRESS1 = {University of Nijmegen},
  SUMMARY = {We prove the irrationality of square roots of prime numbers
and of the number $e$.  In order to be able to prove the last, a proof
is given that {\tt number\_e = exp(1)} as defined in the Mizar library,
that is that
  $$\lim_{n\rightarrow\infty} (1+{1\over n})^n =
  \sum_{k=0}^\infty {1\over k!}$$}}

