MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-pc Structured version   Visualization version   GIF version

Definition df-pc 15753
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 = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))))
Distinct variable group:   𝑟,𝑝,𝑧,𝑥,𝑦,𝑛

Detailed syntax breakdown of Definition df-pc
StepHypRef Expression
1 cpc 15752 . 2 class pCnt
2 vp . . 3 setvar 𝑝
3 vr . . 3 setvar 𝑟
4 cprime 15597 . . 3 class
5 cq 12001 . . 3 class
63cv 1636 . . . . 5 class 𝑟
7 cc0 10215 . . . . 5 class 0
86, 7wceq 1637 . . . 4 wff 𝑟 = 0
9 cpnf 10350 . . . 4 class +∞
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1636 . . . . . . . . . 10 class 𝑥
12 vy . . . . . . . . . . 11 setvar 𝑦
1312cv 1636 . . . . . . . . . 10 class 𝑦
14 cdiv 10963 . . . . . . . . . 10 class /
1511, 13, 14co 6868 . . . . . . . . 9 class (𝑥 / 𝑦)
166, 15wceq 1637 . . . . . . . 8 wff 𝑟 = (𝑥 / 𝑦)
17 vz . . . . . . . . . 10 setvar 𝑧
1817cv 1636 . . . . . . . . 9 class 𝑧
192cv 1636 . . . . . . . . . . . . . 14 class 𝑝
20 vn . . . . . . . . . . . . . . 15 setvar 𝑛
2120cv 1636 . . . . . . . . . . . . . 14 class 𝑛
22 cexp 13077 . . . . . . . . . . . . . 14 class
2319, 21, 22co 6868 . . . . . . . . . . . . 13 class (𝑝𝑛)
24 cdvds 15197 . . . . . . . . . . . . 13 class
2523, 11, 24wbr 4837 . . . . . . . . . . . 12 wff (𝑝𝑛) ∥ 𝑥
26 cn0 11553 . . . . . . . . . . . 12 class 0
2725, 20, 26crab 3096 . . . . . . . . . . 11 class {𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}
28 cr 10214 . . . . . . . . . . 11 class
29 clt 10353 . . . . . . . . . . 11 class <
3027, 28, 29csup 8579 . . . . . . . . . 10 class sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < )
3123, 13, 24wbr 4837 . . . . . . . . . . . 12 wff (𝑝𝑛) ∥ 𝑦
3231, 20, 26crab 3096 . . . . . . . . . . 11 class {𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}
3332, 28, 29csup 8579 . . . . . . . . . 10 class sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )
34 cmin 10545 . . . . . . . . . 10 class
3530, 33, 34co 6868 . . . . . . . . 9 class (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))
3618, 35wceq 1637 . . . . . . . 8 wff 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))
3716, 36wa 384 . . . . . . 7 wff (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
38 cn 11299 . . . . . . 7 class
3937, 12, 38wrex 3093 . . . . . 6 wff 𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
40 cz 11637 . . . . . 6 class
4139, 10, 40wrex 3093 . . . . 5 wff 𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
4241, 17cio 6056 . . . 4 class (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))
438, 9, 42cif 4273 . . 3 class if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))))
442, 3, 4, 5, 43cmpt2 6870 . 2 class (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))))
451, 44wceq 1637 1 wff pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))))
Colors of variables: wff setvar class
This definition is referenced by:  pcval  15760  pc0  15770
  Copyright terms: Public domain W3C validator