### Abstract

An elementary proof is formalised: that exp r is irrational for every nonzero rational number r. The mathematical development comes from the well-known volume Proofs from THE BOOK, by Aigner and Ziegler, who credit the idea to Hermite. The development illustrates a number of basic Isabelle techniques: the manipulation of summations, the calculation of quite complicated derivatives and the estimation of integrals. We also see how to import another AFP entry (Stirling's formula). As for the theorem itself, note that a much stronger and more general result (the Hermite--Lindemann--Weierstraß transcendence theorem) is already available in the AFP.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Irrationals_From_THEBOOK

- Irrationals_From_THEBOOK

### Depends on

- Stirling’s formula

### Auto-related entries

- A Verified Efficient Implementation of the Weighted Path Order
- The Hales–Jewett Theorem
- Compositional BD Security
- The Safely Composable DOM
- An Abstract Formalization of Gödel’s Incompleteness Theorems

## Cite

×

Irrationals_From_THEBOOK-AFP

    @article{Irrationals_From_THEBOOK-AFP,
      author  = {Lawrence C. Paulson},
      title   = {Irrational numbers from THE BOOK},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Irrationals_From_THEBOOK.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jan 31, 2022 : Isabelle2021-1