This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( 𝐴 ∈ ℕ → ( ( Λ ‘ 𝐴 ) ≠ 0 → ( Λ ‘ 𝐴 ) ∈ ℝ ) )
14 13 imp ⊢ ( ( 𝐴 ∈ ℕ ∧ ( Λ ‘ 𝐴 ) ≠ 0 ) → ( Λ ‘ 𝐴 ) ∈ ℝ )
15 0red ⊢ ( 𝐴 ∈ ℕ → 0 ∈ ℝ )
16 1 14 15 pm2.61ne ⊢ ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) ∈ ℝ )