Theorem 1arithlem2

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	1arithlem2	|- ( ( N e. NN /\ P e. Prime ) -> ( ( M ` N ) ` P ) = ( P pCnt N ) )

Proof

Step	Hyp	Ref	Expression
1		1arith.1	|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
2	1	1arithlem1	|- ( N e. NN -> ( M ` N ) = ( p e. Prime |-> ( p pCnt N ) ) )
3	2	fveq1d	|- ( N e. NN -> ( ( M ` N ) ` P ) = ( ( p e. Prime |-> ( p pCnt N ) ) ` P ) )
4		oveq1	|- ( p = P -> ( p pCnt N ) = ( P pCnt N ) )
5		eqid	|- ( p e. Prime |-> ( p pCnt N ) ) = ( p e. Prime |-> ( p pCnt N ) )
6		ovex	|- ( P pCnt N ) e. _V
7	4 5 6	fvmpt	|- ( P e. Prime -> ( ( p e. Prime |-> ( p pCnt N ) ) ` P ) = ( P pCnt N ) )
8	3 7	sylan9eq	|- ( ( N e. NN /\ P e. Prime ) -> ( ( M ` N ) ` P ) = ( P pCnt N ) )