Theorem pczcl

Description: Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Assertion	pczcl	$$⊢\left(P\in \mathbb{P}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to P\mathrm{pCnt}N\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢sup\left(\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\},ℝ,<\right)=sup\left(\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\},ℝ,<\right)$$
2	1	pczpre	$$⊢\left(P\in \mathbb{P}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to P\mathrm{pCnt}N=sup\left(\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\},ℝ,<\right)$$
3		prmuz2	$$⊢P\in \mathbb{P}\to P\in {\mathbb{Z}}_{\ge 2}$$
4		eqid	$$⊢\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\}=\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\}$$
5	4 1	pcprecl	$$⊢\left(P\in {\mathbb{Z}}_{\ge 2}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \left(sup\left(\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\},ℝ,<\right)\in {\mathbb{N}}_0\wedge P^{sup\left(\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\},ℝ,<\right)}\parallel N\right)$$
6	3 5	sylan	$$⊢\left(P\in \mathbb{P}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to \left(sup\left(\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\},ℝ,<\right)\in {\mathbb{N}}_0\wedge P^{sup\left(\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\},ℝ,<\right)}\parallel N\right)$$
7	6	simpld	$$⊢\left(P\in \mathbb{P}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to sup\left(\left\{x\in {\mathbb{N}}_0|P^x\parallel N\right\},ℝ,<\right)\in {\mathbb{N}}_0$$
8	2 7	eqeltrd	$$⊢\left(P\in \mathbb{P}\wedge \left(N\in \mathbb{Z}\wedge N\ne 0\right)\right)\to P\mathrm{pCnt}N\in {\mathbb{N}}_0$$