Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpc 
 |-  pCnt
1 vp 
 |-  p
2 cprime 
 |-  Prime
3 vr 
 |-  r
4 cq 
 |-  QQ
5 3 cv 
 |-  r
6 cc0 
 |-  0
7 5 6 wceq 
 |-  r = 0
8 cpnf 
 |-  +oo
9 vz 
 |-  z
10 vx 
 |-  x
11 cz 
 |-  ZZ
12 vy 
 |-  y
13 cn 
 |-  NN
14 10 cv 
 |-  x
15 cdiv 
 |-  /
16 12 cv 
 |-  y
17 14 16 15 co 
 |-  ( x / y )
18 5 17 wceq 
 |-  r = ( x / y )
19 9 cv 
 |-  z
20 vn 
 |-  n
21 cn0 
 |-  NN0
22 1 cv 
 |-  p
23 cexp 
 |-  ^
24 20 cv 
 |-  n
25 22 24 23 co 
 |-  ( p ^ n )
26 cdvds 
 |-  ||
27 25 14 26 wbr 
 |-  ( p ^ n ) || x
28 27 20 21 crab 
 |-  { n e. NN0 | ( p ^ n ) || x }
29 cr 
 |-  RR
30 clt 
 |-  <
31 28 29 30 csup 
 |-  sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < )
32 cmin 
 |-  -
33 25 16 26 wbr 
 |-  ( p ^ n ) || y
34 33 20 21 crab 
 |-  { n e. NN0 | ( p ^ n ) || y }
35 34 29 30 csup 
 |-  sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < )
36 31 35 32 co 
 |-  ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) )
37 19 36 wceq 
 |-  z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) )
38 18 37 wa 
 |-  ( r = ( x / y ) /\ z = ( sup ( { n e. NN0 | ( p ^ n ) || x } , RR , < ) - sup ( { n e. NN0 | ( p ^ n ) || y } , RR , < ) ) )
39 38 12 13 wrex 
 |-  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 39 10 11 wrex 
 |-  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 , < ) ) )
41 40 9 cio 
 |-  ( 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 , < ) ) ) )
42 7 8 41 cif 
 |-  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 , < ) ) ) ) )
43 1 3 2 4 42 cmpo 
 |-  ( 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 , < ) ) ) ) ) )
44 0 43 wceq 
 |-  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 , < ) ) ) ) ) )