Theorem 1arithlem2

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	1arithlem2	$$⊢\left(N\in \mathbb{N}\wedge P\in \mathbb{P}\right)\to M\left(N\right)\left(P\right)=P\mathrm{pCnt}N$$

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	2	fveq1d	$$⊢N\in \mathbb{N}\to M\left(N\right)\left(P\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}N\right)\left(P\right)$$
4		oveq1	$$⊢p=P\to p\mathrm{pCnt}N=P\mathrm{pCnt}N$$
5		eqid	$$⊢\left(p\in \mathbb{P}⟼p\mathrm{pCnt}N\right)=\left(p\in \mathbb{P}⟼p\mathrm{pCnt}N\right)$$
6		ovex	$$⊢P\mathrm{pCnt}N\in \mathrm{V}$$
7	4 5 6	fvmpt	$$⊢P\in \mathbb{P}\to \left(p\in \mathbb{P}⟼p\mathrm{pCnt}N\right)\left(P\right)=P\mathrm{pCnt}N$$
8	3 7	sylan9eq	$$⊢\left(N\in \mathbb{N}\wedge P\in \mathbb{P}\right)\to M\left(N\right)\left(P\right)=P\mathrm{pCnt}N$$