Theorem vmaprm

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

	Ref	Expression
Assertion	vmaprm	|- ( P e. Prime -> ( Lam ` P ) = ( log ` P ) )

Proof

Step	Hyp	Ref	Expression
1		prmnn	|- ( P e. Prime -> P e. NN )
2	1	nncnd	|- ( P e. Prime -> P e. CC )
3	2	exp1d	|- ( P e. Prime -> ( P ^ 1 ) = P )
4	3	fveq2d	|- ( P e. Prime -> ( Lam ` ( P ^ 1 ) ) = ( Lam ` P ) )
5		1nn	|- 1 e. NN
6		vmappw	|- ( ( P e. Prime /\ 1 e. NN ) -> ( Lam ` ( P ^ 1 ) ) = ( log ` P ) )
7	5 6	mpan2	|- ( P e. Prime -> ( Lam ` ( P ^ 1 ) ) = ( log ` P ) )
8	4 7	eqtr3d	|- ( P e. Prime -> ( Lam ` P ) = ( log ` P ) )