Theorem 1arithlem2

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

	Ref	Expression
Hypothesis	1arith.1	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
Assertion	1arithlem2	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( ( 𝑀 ‘ 𝑁 ) ‘ 𝑃 ) = ( 𝑃 pCnt 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		1arith.1	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
2	1	1arithlem1	⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ‘ 𝑁 ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) ) )
3	2	fveq1d	⊢ ( 𝑁 ∈ ℕ → ( ( 𝑀 ‘ 𝑁 ) ‘ 𝑃 ) = ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) ) ‘ 𝑃 ) )
4		oveq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 pCnt 𝑁 ) = ( 𝑃 pCnt 𝑁 ) )
5		eqid	⊢ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) )
6		ovex	⊢ ( 𝑃 pCnt 𝑁 ) ∈ V
7	4 5 6	fvmpt	⊢ ( 𝑃 ∈ ℙ → ( ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) ) ‘ 𝑃 ) = ( 𝑃 pCnt 𝑁 ) )
8	3 7	sylan9eq	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ) → ( ( 𝑀 ‘ 𝑁 ) ‘ 𝑃 ) = ( 𝑃 pCnt 𝑁 ) )