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

Metamath Proof Explorer

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 ) )