# Metamath Proof Explorer

## Theorem vmacl

Description: Closure for the von Mangoldt function. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion vmacl ${⊢}{A}\in ℕ\to \Lambda \left({A}\right)\in ℝ$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}\Lambda \left({A}\right)=0\to \left(\Lambda \left({A}\right)\in ℝ↔0\in ℝ\right)$
2 isppw2 ${⊢}{A}\in ℕ\to \left(\Lambda \left({A}\right)\ne 0↔\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\right)$
3 vmappw ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \Lambda \left({{p}}^{{k}}\right)=\mathrm{log}{p}$
4 prmnn ${⊢}{p}\in ℙ\to {p}\in ℕ$
5 4 nnrpd ${⊢}{p}\in ℙ\to {p}\in {ℝ}^{+}$
6 5 relogcld ${⊢}{p}\in ℙ\to \mathrm{log}{p}\in ℝ$
7 6 adantr ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \mathrm{log}{p}\in ℝ$
8 3 7 eqeltrd ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \Lambda \left({{p}}^{{k}}\right)\in ℝ$
9 fveq2 ${⊢}{A}={{p}}^{{k}}\to \Lambda \left({A}\right)=\Lambda \left({{p}}^{{k}}\right)$
10 9 eleq1d ${⊢}{A}={{p}}^{{k}}\to \left(\Lambda \left({A}\right)\in ℝ↔\Lambda \left({{p}}^{{k}}\right)\in ℝ\right)$
11 8 10 syl5ibrcom ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \left({A}={{p}}^{{k}}\to \Lambda \left({A}\right)\in ℝ\right)$
12 11 rexlimivv ${⊢}\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\to \Lambda \left({A}\right)\in ℝ$
13 2 12 syl6bi ${⊢}{A}\in ℕ\to \left(\Lambda \left({A}\right)\ne 0\to \Lambda \left({A}\right)\in ℝ\right)$
14 13 imp ${⊢}\left({A}\in ℕ\wedge \Lambda \left({A}\right)\ne 0\right)\to \Lambda \left({A}\right)\in ℝ$
15 0red ${⊢}{A}\in ℕ\to 0\in ℝ$
16 1 14 15 pm2.61ne ${⊢}{A}\in ℕ\to \Lambda \left({A}\right)\in ℝ$