Theorem 1arithlem1

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

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

Proof

Step	Hyp	Ref	Expression
1		1arith.1	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
2		oveq2	⊢ ( 𝑛 = 𝑁 → ( 𝑝 pCnt 𝑛 ) = ( 𝑝 pCnt 𝑁 ) )
3	2	mpteq2dv	⊢ ( 𝑛 = 𝑁 → ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) ) )
4		prmex	⊢ ℙ ∈ V
5	4	mptex	⊢ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) ) ∈ V
6	3 1 5	fvmpt	⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ‘ 𝑁 ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) ) )