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 16163
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 16162 . 2 class pCnt
2 vp . . 3 setvar 𝑝
3 vr . . 3 setvar 𝑟
4 cprime 16004 . . 3 class
5 cq 12336 . . 3 class
63cv 1537 . . . . 5 class 𝑟
7 cc0 10526 . . . . 5 class 0
86, 7wceq 1538 . . . 4 wff 𝑟 = 0
9 cpnf 10661 . . . 4 class +∞
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1537 . . . . . . . . . 10 class 𝑥
12 vy . . . . . . . . . . 11 setvar 𝑦
1312cv 1537 . . . . . . . . . 10 class 𝑦
14 cdiv 11286 . . . . . . . . . 10 class /
1511, 13, 14co 7140 . . . . . . . . 9 class (𝑥 / 𝑦)
166, 15wceq 1538 . . . . . . . 8 wff 𝑟 = (𝑥 / 𝑦)
17 vz . . . . . . . . . 10 setvar 𝑧
1817cv 1537 . . . . . . . . 9 class 𝑧
192cv 1537 . . . . . . . . . . . . . 14 class 𝑝
20 vn . . . . . . . . . . . . . . 15 setvar 𝑛
2120cv 1537 . . . . . . . . . . . . . 14 class 𝑛
22 cexp 13425 . . . . . . . . . . . . . 14 class
2319, 21, 22co 7140 . . . . . . . . . . . . 13 class (𝑝𝑛)
24 cdvds 15598 . . . . . . . . . . . . 13 class
2523, 11, 24wbr 5042 . . . . . . . . . . . 12 wff (𝑝𝑛) ∥ 𝑥
26 cn0 11885 . . . . . . . . . . . 12 class 0
2725, 20, 26crab 3134 . . . . . . . . . . 11 class {𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}
28 cr 10525 . . . . . . . . . . 11 class
29 clt 10664 . . . . . . . . . . 11 class <
3027, 28, 29csup 8892 . . . . . . . . . 10 class sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < )
3123, 13, 24wbr 5042 . . . . . . . . . . . 12 wff (𝑝𝑛) ∥ 𝑦
3231, 20, 26crab 3134 . . . . . . . . . . 11 class {𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}
3332, 28, 29csup 8892 . . . . . . . . . 10 class sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )
34 cmin 10859 . . . . . . . . . 10 class
3530, 33, 34co 7140 . . . . . . . . 9 class (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))
3618, 35wceq 1538 . . . . . . . 8 wff 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))
3716, 36wa 399 . . . . . . 7 wff (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
38 cn 11625 . . . . . . 7 class
3937, 12, 38wrex 3131 . . . . . 6 wff 𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
40 cz 11969 . . . . . 6 class
4139, 10, 40wrex 3131 . . . . 5 wff 𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
4241, 17cio 6291 . . . 4 class (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))
438, 9, 42cif 4439 . . 3 class if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))))
442, 3, 4, 5, 43cmpo 7142 . 2 class (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))))
451, 44wceq 1538 1 wff pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))))
Colors of variables: wff setvar class
This definition is referenced by:  pcval  16170  pc0  16180
  Copyright terms: Public domain W3C validator