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 ∈ ℕ → e Λ ⁡ A ∈ ℕ

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ Λ ⁡ A = 0 → e Λ ⁡ A = e 0
2 ef0 ⊢ e 0 = 1
3 1 2 eqtrdi ⊢ Λ ⁡ A = 0 → e Λ ⁡ A = 1
4 3 eleq1d ⊢ Λ ⁡ A = 0 → e Λ ⁡ A ∈ ℕ ↔ 1 ∈ ℕ
5 isppw2 ⊢ A ∈ ℕ → Λ ⁡ A ≠ 0 ↔ ∃ p ∈ ℙ ∃ k ∈ ℕ A = p k
6 vmappw ⊢ p ∈ ℙ ∧ k ∈ ℕ → Λ ⁡ p k = log ⁡ p
7 6 fveq2d ⊢ p ∈ ℙ ∧ k ∈ ℕ → e Λ ⁡ p k = e log ⁡ p
8 prmnn ⊢ p ∈ ℙ → p ∈ ℕ
9 8 nnrpd ⊢ p ∈ ℙ → p ∈ ℝ +
10 9 reeflogd ⊢ p ∈ ℙ → e log ⁡ p = p
11 10 8 eqeltrd ⊢ p ∈ ℙ → e log ⁡ p ∈ ℕ
12 11 adantr ⊢ p ∈ ℙ ∧ k ∈ ℕ → e log ⁡ p ∈ ℕ
13 7 12 eqeltrd ⊢ p ∈ ℙ ∧ k ∈ ℕ → e Λ ⁡ p k ∈ ℕ
14 fveq2 ⊢ A = p k → Λ ⁡ A = Λ ⁡ p k
15 14 fveq2d ⊢ A = p k → e Λ ⁡ A = e Λ ⁡ p k
16 15 eleq1d ⊢ A = p k → e Λ ⁡ A ∈ ℕ ↔ e Λ ⁡ p k ∈ ℕ
17 13 16 syl5ibrcom ⊢ p ∈ ℙ ∧ k ∈ ℕ → A = p k → e Λ ⁡ A ∈ ℕ
18 17 rexlimivv ⊢ ∃ p ∈ ℙ ∃ k ∈ ℕ A = p k → e Λ ⁡ A ∈ ℕ
19 5 18 syl6bi ⊢ A ∈ ℕ → Λ ⁡ A ≠ 0 → e Λ ⁡ A ∈ ℕ
20 19 imp ⊢ A ∈ ℕ ∧ Λ ⁡ A ≠ 0 → e Λ ⁡ A ∈ ℕ
21 1nn ⊢ 1 ∈ ℕ
22 21 a1i ⊢ A ∈ ℕ → 1 ∈ ℕ
23 4 20 22 pm2.61ne ⊢ A ∈ ℕ → e Λ ⁡ A ∈ ℕ