Theorem 1arithlem3

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

	Ref	Expression
Hypothesis	1arith.1	$$⊢M=\left(n\in \mathbb{N}⟼\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\right)$$
Assertion	1arithlem3	$$⊢N\in \mathbb{N}\to M\left(N\right):\mathbb{P}⟶{\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		1arith.1	$$⊢M=\left(n\in \mathbb{N}⟼\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\right)$$
2	1	1arithlem1	$$⊢N\in \mathbb{N}\to M\left(N\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}N\right)$$
3		pccl	$$⊢\left(p\in \mathbb{P}\wedge N\in \mathbb{N}\right)\to p\mathrm{pCnt}N\in {\mathbb{N}}_0$$
4	3	ancoms	$$⊢\left(N\in \mathbb{N}\wedge p\in \mathbb{P}\right)\to p\mathrm{pCnt}N\in {\mathbb{N}}_0$$
5	2 4	fmpt3d	$$⊢N\in \mathbb{N}\to M\left(N\right):\mathbb{P}⟶{\mathbb{N}}_0$$