Definition df-pc

Description: Define the prime count function, which returns the largest exponent of a given prime (or other positive integer) that divides the number. For rational numbers, it returns negative values according to the power of a prime in the denominator. (Contributed by Mario Carneiro, 23-Feb-2014)

	Ref	Expression
Assertion	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)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpc	$$class\mathrm{pCnt}$$
1		vp	$$setvarp$$
2		cprime	$$class\mathbb{P}$$
3		vr	$$setvarr$$
4		cq	$$class\mathbb{Q}$$
5	3	cv	$$setvarr$$
6		cc0	$$class0$$
7	5 6	wceq	$$wffr=0$$
8		cpnf	$$class\mathrm{+\infty }$$
9		vz	$$setvarz$$
10		vx	$$setvarx$$
11		cz	$$class\mathbb{Z}$$
12		vy	$$setvary$$
13		cn	$$class\mathbb{N}$$
14	10	cv	$$setvarx$$
15		cdiv	$$class÷$$
16	12	cv	$$setvary$$
17	14 16 15	co	$$class\left(\frac{x}{y}\right)$$
18	5 17	wceq	$$wffr=\frac{x}{y}$$
19	9	cv	$$setvarz$$
20		vn	$$setvarn$$
21		cn0	$$class{\mathbb{N}}_0$$
22	1	cv	$$setvarp$$
23		cexp	$$class^$$
24	20	cv	$$setvarn$$
25	22 24 23	co	$$class{p}^n$$
26		cdvds	$$class\parallel$$
27	25 14 26	wbr	$$wff{p}^n\parallel x$$
28	27 20 21	crab	$$class\left\{n\in {\mathbb{N}}_0|p^n\parallel x\right\}$$
29		cr	$$classℝ$$
30		clt	$$class<$$
31	28 29 30	csup	$$classsup\left(\left\{n\in {\mathbb{N}}_0|p^n\parallel x\right\},ℝ,<\right)$$
32		cmin	$$class-$$
33	25 16 26	wbr	$$wff{p}^n\parallel y$$
34	33 20 21	crab	$$class\left\{n\in {\mathbb{N}}_0|p^n\parallel y\right\}$$
35	34 29 30	csup	$$classsup\left(\left\{n\in {\mathbb{N}}_0|p^n\parallel y\right\},ℝ,<\right)$$
36	31 35 32	co	$$class\left(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)$$
37	19 36	wceq	$$wffz=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)$$
38	18 37	wa	$$wff\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)$$
39	38 12 13	wrex	$$wff\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)$$
40	39 10 11	wrex	$$wff\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)$$
41	40 9	cio	$$class\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)$$
42	7 8 41	cif	$$classif\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)$$
43	1 3 2 4 42	cmpo	$$class\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)$$
44	0 43	wceq	$$wff\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)$$