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

Metamath Proof Explorer

Theorem vmaprm

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

		Ref	Expression
	Assertion	vmaprm	$⊢ P \in ℙ \to Λ (P) = \log P$

Step	Hyp	Ref	Expression
1		prmnn	$⊢ P \in ℙ \to P \in ℕ$
2	1	nncnd	$⊢ P \in ℙ \to P \in ℂ$
3	2	exp1d	$⊢ P \in ℙ \to P^{1} = P$
4	3	fveq2d	$⊢ P \in ℙ \to Λ (P^{1}) = Λ (P)$
5		1nn	$⊢ 1 \in ℕ$
6		vmappw	$⊢ (P \in ℙ \land 1 \in ℕ) \to Λ (P^{1}) = \log P$
7	5 6	mpan2	$⊢ P \in ℙ \to Λ (P^{1}) = \log P$
8	4 7	eqtr3d	$⊢ P \in ℙ \to Λ (P) = \log P$