Theorem vmaprm

Description: Value of the von Mangoldt function at a prime. (Contributed by Mario Carneiro, 7-Apr-2016)

	Ref	Expression
Assertion	vmaprm	⊢ ( 𝑃 ∈ ℙ → ( Λ ‘ 𝑃 ) = ( log ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
2	1	nncnd	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℂ )
3	2	exp1d	⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ↑ 1 ) = 𝑃 )
4	3	fveq2d	⊢ ( 𝑃 ∈ ℙ → ( Λ ‘ ( 𝑃 ↑ 1 ) ) = ( Λ ‘ 𝑃 ) )
5		1nn	⊢ 1 ∈ ℕ
6		vmappw	⊢ ( ( 𝑃 ∈ ℙ ∧ 1 ∈ ℕ ) → ( Λ ‘ ( 𝑃 ↑ 1 ) ) = ( log ‘ 𝑃 ) )
7	5 6	mpan2	⊢ ( 𝑃 ∈ ℙ → ( Λ ‘ ( 𝑃 ↑ 1 ) ) = ( log ‘ 𝑃 ) )
8	4 7	eqtr3d	⊢ ( 𝑃 ∈ ℙ → ( Λ ‘ 𝑃 ) = ( log ‘ 𝑃 ) )