Theorem pc0

Description: The value of the prime power function at zero. (Contributed by Mario Carneiro, 3-Oct-2014)

	Ref	Expression
Assertion	pc0	$$⊢P\in \mathbb{P}\to P\mathrm{pCnt}0=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		zq	$$⊢0\in \mathbb{Z}\to 0\in \mathbb{Q}$$
3	1 2	ax-mp	$$⊢0\in \mathbb{Q}$$
4		iftrue	$$⊢r=0\to if\left(r=0,\mathrm{+\infty },\left(\iota z|\exists x\in \mathbb{Z}\exists y\in \mathbb{N}\left(r=\frac{x}{y}\wedge z=sup\left(\left\{n\in {\mathbb{N}}_0|p^n\parallel x\right\},ℝ,<\right)-sup\left(\left\{n\in {\mathbb{N}}_0|p^n\parallel y\right\},ℝ,<\right)\right)\right)\right)=\mathrm{+\infty }$$
5	4	adantl	$$⊢\left(p=P\wedge r=0\right)\to if\left(r=0,\mathrm{+\infty },\left(\iota z|\exists x\in \mathbb{Z}\exists y\in \mathbb{N}\left(r=\frac{x}{y}\wedge z=sup\left(\left\{n\in {\mathbb{N}}_0|p^n\parallel x\right\},ℝ,<\right)-sup\left(\left\{n\in {\mathbb{N}}_0|p^n\parallel y\right\},ℝ,<\right)\right)\right)\right)=\mathrm{+\infty }$$
6		df-pc	$$⊢\mathrm{pCnt}=\left(p\in \mathbb{P},r\in \mathbb{Q}⟼if\left(r=0,\mathrm{+\infty },\left(\iota z|\exists x\in \mathbb{Z}\exists y\in \mathbb{N}\left(r=\frac{x}{y}\wedge z=sup\left(\left\{n\in {\mathbb{N}}_0|p^n\parallel x\right\},ℝ,<\right)-sup\left(\left\{n\in {\mathbb{N}}_0|p^n\parallel y\right\},ℝ,<\right)\right)\right)\right)\right)$$
7		pnfex	$$⊢\mathrm{+\infty }\in \mathrm{V}$$
8	5 6 7	ovmpoa	$$⊢\left(P\in \mathbb{P}\wedge 0\in \mathbb{Q}\right)\to P\mathrm{pCnt}0=\mathrm{+\infty }$$
9	3 8	mpan2	$$⊢P\in \mathbb{P}\to P\mathrm{pCnt}0=\mathrm{+\infty }$$