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. 
BibTeX: 
@article{Prime_Harmonic_SeriesAFP,
author = {Manuel Eberl},
title = {The Divergence of the Prime Harmonic Series},
journal = {Archive of Formal Proofs},
month = dec,
year = 2015,
note = {\url{http://isaafp.org/entries/Prime_Harmonic_Series.shtml},
Formal proof development},
ISSN = {2150914x},
}
