Definition df-pc 12176

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.)

Assertion

Ref	Expression
df-pc	|- pCnt = ( p e. Prime , r e. QQ |-> if ( r = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) ) ) )

Distinct variable group:   r, p, z, x, y, n

Detailed syntax breakdown of Definition df-pc

Step	Hyp	Ref	Expression
1		cpc 12175	. 2 class pCnt
2		vp	. . 3 setvar p
3		vr	. . 3 setvar r
4		cprime 12000	. . 3 class Prime
5		cq 9535	. . 3 class QQ
6	3	cv 1334	. . . . 5 class r
7		cc0 7735	. . . . 5 class 0
8	6, 7	wceq 1335	. . . 4 wff r = 0
9		cpnf 7912	. . . 4 class +oo
10		vx	. . . . . . . . . . 11 setvar x
11	10	cv 1334	. . . . . . . . . 10 class x
12		vy	. . . . . . . . . . 11 setvar y
13	12	cv 1334	. . . . . . . . . 10 class y
14		cdiv 8550	. . . . . . . . . 10 class /
15	11, 13, 14	co 5827	. . . . . . . . 9 class ( x / y )
16	6, 15	wceq 1335	. . . . . . . 8 wff r = ( x / y )
17		vz	. . . . . . . . . 10 setvar z
18	17	cv 1334	. . . . . . . . 9 class z
19	2	cv 1334	. . . . . . . . . . . . . 14 class p
20		vn	. . . . . . . . . . . . . . 15 setvar n
21	20	cv 1334	. . . . . . . . . . . . . 14 class n
22		cexp 10428	. . . . . . . . . . . . . 14 class ^
23	19, 21, 22	co 5827	. . . . . . . . . . . . 13 class ( p ^ n )
24		cdvds 11695	. . . . . . . . . . . . 13 class ||
25	23, 11, 24	wbr 3967	. . . . . . . . . . . 12 wff ( p ^ n ) || x
26		cn0 9096	. . . . . . . . . . . 12 class NN0
27	25, 20, 26	crab 2439	. . . . . . . . . . 11 class { n e. NN0 | ( p ^ n ) || x }
28		cr 7734	. . . . . . . . . . 11 class RR
29		clt 7915	. . . . . . . . . . 11 class <
30	27, 28, 29	csup 6929	. . . . . . . . . 10 class sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < )
31	23, 13, 24	wbr 3967	. . . . . . . . . . . 12 wff ( p ^ n ) || y
32	31, 20, 26	crab 2439	. . . . . . . . . . 11 class { n e. NN0 | ( p ^ n ) || y }
33	32, 28, 29	csup 6929	. . . . . . . . . 10 class sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < )
34		cmin 8051	. . . . . . . . . 10 class -
35	30, 33, 34	co 5827	. . . . . . . . 9 class ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) )
36	18, 35	wceq 1335	. . . . . . . 8 wff z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) )
37	16, 36	wa 103	. . . . . . 7 wff ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) )
38		cn 8839	. . . . . . 7 class NN
39	37, 12, 38	wrex 2436	. . . . . 6 wff E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) )
40		cz 9173	. . . . . 6 class ZZ
41	39, 10, 40	wrex 2436	. . . . 5 wff E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) )
42	41, 17	cio 5136	. . . 4 class ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) )
43	8, 9, 42	cif 3506	. . 3 class if ( r = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) ) )
44	2, 3, 4, 5, 43	cmpo 5829	. 2 class ( p e. Prime , r e. QQ |-> if ( r = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) ) ) )
45	1, 44	wceq 1335	1 wff pCnt = ( p e. Prime , r e. QQ |-> if ( r = 0 , +oo , ( iota z E. x e. ZZ E. y e. NN ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) ) ) ) )

This definition is referenced by:  pcval  12187  pc0  12195