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 \mathbb{P}\to \Lambda \left(P\right)=\log P$$

Proof

Step	Hyp	Ref	Expression
1		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
2	1	nncnd	$$⊢P\in \mathbb{P}\to P\in ℂ$$
3	2	exp1d	$$⊢P\in \mathbb{P}\to P^1=P$$
4	3	fveq2d	$$⊢P\in \mathbb{P}\to \Lambda \left(P^1\right)=\Lambda \left(P\right)$$
5		1nn	$$⊢1\in \mathbb{N}$$
6		vmappw	$$⊢\left(P\in \mathbb{P}\wedge 1\in \mathbb{N}\right)\to \Lambda \left(P^1\right)=\log P$$
7	5 6	mpan2	$$⊢P\in \mathbb{P}\to \Lambda \left(P^1\right)=\log P$$
8	4 7	eqtr3d	$$⊢P\in \mathbb{P}\to \Lambda \left(P\right)=\log P$$