Theorem: Sum of Reciprocals of Primes is Divergent

Let $n \in \N: n \ge 1$.
There exists a (strictly) positive real number $C \in \R_{>0}$ such that:
:$(1): \quad \ds \sum_{\substack {p \mathop \in \Bbb P \\ p \mathop \le n} } \frac 1 p > \map \ln {\ln n} - C$
where $\Bbb P$ is the set of all prime numbers.
:$(2): \quad \ds \lim_{n \mathop \to \infty} \paren {\map \ln {\ln n} - C} = +\infty$

Proof:
By Sum of Reciprocals of Primes is Divergent: Lemma:
:$\ds \lim_{n \mathop \to \infty} \paren {\map \ln {\map \ln n} - \frac 1 2} = +\infty$
{{qed|lemma}}
It remains to be proved that:
:$\ds \sum_{\substack {p \mathop \in \Bbb P \\ p \mathop \le n} } \frac 1 p > \map \ln {\ln n} - \frac 1 2$
Assume all sums and product over $p$ are over the set of prime numbers.
Let $n \ge 1$.
{{begin-eqn}}
{{eqn | l = \prod_{p \mathop \le n} \paren {1 - \frac 1 p}^{-1}
      | r = \prod_{p \mathop \le n} \frac p {p - 1}
      | c = 
}}
{{eqn | r = \prod_{p \mathop \le n} \frac p {p - 1} \times \dfrac {\frac 1 p} {\frac 1 p}
      | c = multiplying top and bottom by $\dfrac 1 p$
}}
{{eqn | r = \prod_{p \mathop \le n} \frac 1 {1 - \frac 1 p}
      | c = 
}}
{{eqn | r = \prod_{p \mathop \le n} \sum_{k \mathop = 0}^\infty \paren {\frac 1 p}^k
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | o = \ge
      | r = \sum_{k \mathop = 1}^n \frac 1 k 
      | c = Fundamental Theorem of Arithmetic
}}
{{eqn | o = >
      | r = \int_1^n \frac 1 x \rd x
      | c = Cauchy Integral Test
}}
{{eqn | n = 1
      | ll = \leadsto 
      | l = \prod_{p \mathop \le n} \paren {1 - \frac 1 p}^{-1}
      | o = >
      | r = \ln n
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \ln \prod_{p \mathop \le n} \paren {1 - \frac 1 p}^{-1}
      | r = \sum_{p \mathop \le n} \map \ln {1 - \frac 1 p}^{-1}
      | c = Sum of Logarithms
}}
{{eqn | r = -\sum_{p \mathop \le n} \map \ln {1 - \frac 1 p}
      | c = Log of Power
}}
{{eqn | r = -\sum_{p \mathop \le n} \sum_{k \mathop = 1}^\infty \paren {-1}^{k - 1} \frac {\paren {-\frac 1 p }^k } k
      | c = Power Series Expansion for $\map \ln {1 + x}$
}}
{{eqn | r = \sum_{p \mathop \le n} \sum_{k \mathop = 1}^\infty \frac {\paren {\frac 1 p }^k } k
      | c = 
}}
{{eqn | r = \sum_{p \mathop \le n} \sum_{k \mathop = 1}^\infty \frac 1 {k p^k}
      | c = 
}}
{{eqn | r = \sum_{p \mathop \le n} \paren {\frac 1 {p^1} + \frac 1 {2 p^2} + \frac 1 {3 p^3} + \frac 1 {4 p^4} + \cdots}
      | c = 
}}
{{eqn | o = <
      | r = \sum_{p \mathop \le n} \frac 1 p + \sum_{p \mathop \le n} \frac 1 {2 p^2} + \frac 1 {2 p^3} + \frac 1 {2 p^4} + \frac 1 {2 p^5} + \cdots
      | c = 
}}
{{eqn | r = \sum_{p \mathop \le n} \frac 1 p + \sum_{p \mathop \le n} \frac 1 {2 p^2} \paren {\frac 1 1 + \frac 1 {p^1} + \frac 1 {p^2} + \frac 1 {p^3} + \frac 1 {p^4} + \cdots}
      | c = 
}}
{{eqn | r = \sum_{p \mathop \le n} \frac 1 p + \sum_{p \mathop \le n} \frac 1 {2 p^2} \paren {\sum_{k \mathop = 0}^\infty \frac 1 {p^k} }
      | c = 
}}
{{eqn | r = \sum_{p \mathop \le n} \frac 1 p + \frac 1 2 \sum_{p \mathop \le n} \frac 1 {p^2} \paren {\frac 1 {1 - \frac 1 p} }
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \sum_{p \mathop \le n} \frac 1 p + \frac 1 2 \sum_{p \mathop \le n} \frac 1 {p \paren {p - 1} }
      | c = 
}}
{{eqn | o = <
      | r = \sum_{p \mathop \le n} \frac 1 p + \frac 1 2 \sum_{n \mathop = 2}^\infty \frac 1 {n \paren {n - 1} }
      | c = 
}}
{{eqn | r = \sum_{p \mathop \le n} \frac 1 p + \frac 1 2 \paren {\sum_{n \mathop = 2}^\infty \frac 1 {\paren {n - 1} } - \frac 1 n}
      | c = 
}}
{{eqn | r = \sum_{p \mathop \le n} \frac 1 p + \frac 1 2 \paren {\paren {1 - \frac 1 2} + \paren {\frac 1 2 - \frac 1 3} + \paren {\frac 1 3 - \frac 1 4} + \cdots}
      | c = 
}}
{{eqn | r = \sum_{p \mathop \le n} \frac 1 p + \frac 1 2
      | c = {{Defof|Telescoping Series}}
}}
{{eqn | ll = \leadsto
      | l = \ln \prod_{p \mathop \le n} \paren {1 - \frac 1 p}^{-1}
      | o = \lt
      | r = \sum_{p \mathop \le n} \frac 1 p + \frac 1 2
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \sum_{p \mathop \le n} \frac 1 p
      | o = >
      | r = \ln \prod_{p \mathop \le n} \paren {1 - \frac 1 p}^{-1} - \frac 1 2
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \sum_{p \mathop \le n} \frac 1 p
      | o = >
      | r = \map \ln {\ln n} - \frac 1 2
      | c = by $(1)$
}}
{{end-eqn}}
{{qed}}