### Abstract

In this work, we prove the lower bound ln(H_n) - ln(5/3) for the partial sum of the Prime Harmonic series and, based on this, the divergence of the Prime Harmonic Series ∑[p prime] · 1/p.

The proof relies on the unique squarefree decomposition of natural numbers. This is similar to Euler's original proof (which was highly informal and morally questionable). Its advantage over proofs by contradiction, like the famous one by Paul Erdős, is that it provides a relatively good lower bound for the partial sums.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Prime_Harmonic_Series

- Prime_Harmonic_Misc
- Squarefree_Nat
- Prime_Harmonic

## Cite

×

Prime_Harmonic_Series-AFP

    @article{Prime_Harmonic_Series-AFP,
      author  = {Manuel Eberl},
      title   = {The Divergence of the Prime Harmonic Series},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Prime_Harmonic_Series.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Jan 5, 2016 : Isabelle2015