# Metamath Proof Explorer

## Theorem vmacl

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

Ref Expression
Assertion vmacl ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) ∈ ℝ )

### Proof

Step Hyp Ref Expression
1 eleq1 ( ( Λ ‘ 𝐴 ) = 0 → ( ( Λ ‘ 𝐴 ) ∈ ℝ ↔ 0 ∈ ℝ ) )
2 isppw2 ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 ↔ ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝𝑘 ) ) )
3 vmappw ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝𝑘 ) ) = ( log ‘ 𝑝 ) )
4 prmnn ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ )
5 4 nnrpd ( 𝑝 ∈ ℙ → 𝑝 ∈ ℝ+ )
6 5 relogcld ( 𝑝 ∈ ℙ → ( log ‘ 𝑝 ) ∈ ℝ )
7 6 adantr ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( log ‘ 𝑝 ) ∈ ℝ )
8 3 7 eqeltrd ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( Λ ‘ ( 𝑝𝑘 ) ) ∈ ℝ )
9 fveq2 ( 𝐴 = ( 𝑝𝑘 ) → ( Λ ‘ 𝐴 ) = ( Λ ‘ ( 𝑝𝑘 ) ) )
10 9 eleq1d ( 𝐴 = ( 𝑝𝑘 ) → ( ( Λ ‘ 𝐴 ) ∈ ℝ ↔ ( Λ ‘ ( 𝑝𝑘 ) ) ∈ ℝ ) )
11 8 10 syl5ibrcom ( ( 𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ ) → ( 𝐴 = ( 𝑝𝑘 ) → ( Λ ‘ 𝐴 ) ∈ ℝ ) )
12 11 rexlimivv ( ∃ 𝑝 ∈ ℙ ∃ 𝑘 ∈ ℕ 𝐴 = ( 𝑝𝑘 ) → ( Λ ‘ 𝐴 ) ∈ ℝ )
13 2 12 syl6bi ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 → ( Λ ‘ 𝐴 ) ∈ ℝ ) )
14 13 imp ( ( 𝐴 ∈ ℕ ∧ ( Λ ‘ 𝐴 ) ≠ 0 ) → ( Λ ‘ 𝐴 ) ∈ ℝ )
15 0red ( 𝐴 ∈ ℕ → 0 ∈ ℝ )
16 1 14 15 pm2.61ne ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) ∈ ℝ )