Theorem 1arithlem3

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

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

Proof

Step	Hyp	Ref	Expression
1		1arith.1	⊢ 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
2	1	1arithlem1	⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ‘ 𝑁 ) = ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑁 ) ) )
3		pccl	⊢ ( ( 𝑝 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑝 pCnt 𝑁 ) ∈ ℕ0 )
4	3	ancoms	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑝 ∈ ℙ ) → ( 𝑝 pCnt 𝑁 ) ∈ ℕ0 )
5	2 4	fmpt3d	⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ‘ 𝑁 ) : ℙ ⟶ ℕ0 )