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	⊢ ( 𝐴 ∈ ℕ → ( Λ ‘ 𝐴 ) ∈ ℝ )