# Metamath Proof Explorer

## Theorem efvmacl

Description: The von Mangoldt is closed in the log-integers. (Contributed by Mario Carneiro, 7-Apr-2016)

Ref Expression
Assertion efvmacl ${⊢}{A}\in ℕ\to {\mathrm{e}}^{\Lambda \left({A}\right)}\in ℕ$

### Proof

Step Hyp Ref Expression
1 fveq2 ${⊢}\Lambda \left({A}\right)=0\to {\mathrm{e}}^{\Lambda \left({A}\right)}={\mathrm{e}}^{0}$
2 ef0 ${⊢}{\mathrm{e}}^{0}=1$
3 1 2 eqtrdi ${⊢}\Lambda \left({A}\right)=0\to {\mathrm{e}}^{\Lambda \left({A}\right)}=1$
4 3 eleq1d ${⊢}\Lambda \left({A}\right)=0\to \left({\mathrm{e}}^{\Lambda \left({A}\right)}\in ℕ↔1\in ℕ\right)$
5 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)$
6 vmappw ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \Lambda \left({{p}}^{{k}}\right)=\mathrm{log}{p}$
7 6 fveq2d ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to {\mathrm{e}}^{\Lambda \left({{p}}^{{k}}\right)}={\mathrm{e}}^{\mathrm{log}{p}}$
8 prmnn ${⊢}{p}\in ℙ\to {p}\in ℕ$
9 8 nnrpd ${⊢}{p}\in ℙ\to {p}\in {ℝ}^{+}$
10 9 reeflogd ${⊢}{p}\in ℙ\to {\mathrm{e}}^{\mathrm{log}{p}}={p}$
11 10 8 eqeltrd ${⊢}{p}\in ℙ\to {\mathrm{e}}^{\mathrm{log}{p}}\in ℕ$
12 11 adantr ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to {\mathrm{e}}^{\mathrm{log}{p}}\in ℕ$
13 7 12 eqeltrd ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to {\mathrm{e}}^{\Lambda \left({{p}}^{{k}}\right)}\in ℕ$
14 fveq2 ${⊢}{A}={{p}}^{{k}}\to \Lambda \left({A}\right)=\Lambda \left({{p}}^{{k}}\right)$
15 14 fveq2d ${⊢}{A}={{p}}^{{k}}\to {\mathrm{e}}^{\Lambda \left({A}\right)}={\mathrm{e}}^{\Lambda \left({{p}}^{{k}}\right)}$
16 15 eleq1d ${⊢}{A}={{p}}^{{k}}\to \left({\mathrm{e}}^{\Lambda \left({A}\right)}\in ℕ↔{\mathrm{e}}^{\Lambda \left({{p}}^{{k}}\right)}\in ℕ\right)$
17 13 16 syl5ibrcom ${⊢}\left({p}\in ℙ\wedge {k}\in ℕ\right)\to \left({A}={{p}}^{{k}}\to {\mathrm{e}}^{\Lambda \left({A}\right)}\in ℕ\right)$
18 17 rexlimivv ${⊢}\exists {p}\in ℙ\phantom{\rule{.4em}{0ex}}\exists {k}\in ℕ\phantom{\rule{.4em}{0ex}}{A}={{p}}^{{k}}\to {\mathrm{e}}^{\Lambda \left({A}\right)}\in ℕ$
19 5 18 syl6bi ${⊢}{A}\in ℕ\to \left(\Lambda \left({A}\right)\ne 0\to {\mathrm{e}}^{\Lambda \left({A}\right)}\in ℕ\right)$
20 19 imp ${⊢}\left({A}\in ℕ\wedge \Lambda \left({A}\right)\ne 0\right)\to {\mathrm{e}}^{\Lambda \left({A}\right)}\in ℕ$
21 1nn ${⊢}1\in ℕ$
22 21 a1i ${⊢}{A}\in ℕ\to 1\in ℕ$
23 4 20 22 pm2.61ne ${⊢}{A}\in ℕ\to {\mathrm{e}}^{\Lambda \left({A}\right)}\in ℕ$