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 ⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 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 𝑁 ) )