Abstract: 
This entry is a formalisation of Chapter 4 (and parts of
Chapter 3) of Apostol's Introduction
to Analytic Number Theory. The main topics that
are addressed are properties of the distribution of prime numbers that
can be shown in an elementary way (i. e. without the Prime
Number Theorem), the various equivalent forms of the PNT (which imply
each other in elementary ways), and consequences that follow from the
PNT in elementary ways. The latter include, most notably, asymptotic
bounds for the number of distinct prime factors of
n, the divisor function
d(n), Euler's totient function
φ(n), and
lcm(1,…,n). 
BibTeX: 
@article{Prime_Distribution_ElementaryAFP,
author = {Manuel Eberl},
title = {Elementary Facts About the Distribution of Primes},
journal = {Archive of Formal Proofs},
month = feb,
year = 2019,
note = {\url{https://isaafp.org/entries/Prime_Distribution_Elementary.html},
Formal proof development},
ISSN = {2150914x},
}
