Theorem 1arithlem1

Description: Lemma for 1arith . (Contributed by Mario Carneiro, 30-May-2014)

	Ref	Expression
Hypothesis	1arith.1	|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
Assertion	1arithlem1	|- ( N e. NN -> ( M ` N ) = ( p e. Prime |-> ( p pCnt N ) ) )

Proof

Step	Hyp	Ref	Expression
1		1arith.1	|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
2		oveq2	|- ( n = N -> ( p pCnt n ) = ( p pCnt N ) )
3	2	mpteq2dv	|- ( n = N -> ( p e. Prime |-> ( p pCnt n ) ) = ( p e. Prime |-> ( p pCnt N ) ) )
4		prmex	|- Prime e. _V
5	4	mptex	|- ( p e. Prime |-> ( p pCnt N ) ) e. _V
6	3 1 5	fvmpt	|- ( N e. NN -> ( M ` N ) = ( p e. Prime |-> ( p pCnt N ) ) )