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 15589
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 15588 . 2 class pCnt
2 vp . . 3 setvar 𝑝
3 vr . . 3 setvar 𝑟
4 cprime 15432 . . 3 class
5 cq 11826 . . 3 class
63cv 1522 . . . . 5 class 𝑟
7 cc0 9974 . . . . 5 class 0
86, 7wceq 1523 . . . 4 wff 𝑟 = 0
9 cpnf 10109 . . . 4 class +∞
10 vx . . . . . . . . . . 11 setvar 𝑥
1110cv 1522 . . . . . . . . . 10 class 𝑥
12 vy . . . . . . . . . . 11 setvar 𝑦
1312cv 1522 . . . . . . . . . 10 class 𝑦
14 cdiv 10722 . . . . . . . . . 10 class /
1511, 13, 14co 6690 . . . . . . . . 9 class (𝑥 / 𝑦)
166, 15wceq 1523 . . . . . . . 8 wff 𝑟 = (𝑥 / 𝑦)
17 vz . . . . . . . . . 10 setvar 𝑧
1817cv 1522 . . . . . . . . 9 class 𝑧
192cv 1522 . . . . . . . . . . . . . 14 class 𝑝
20 vn . . . . . . . . . . . . . . 15 setvar 𝑛
2120cv 1522 . . . . . . . . . . . . . 14 class 𝑛
22 cexp 12900 . . . . . . . . . . . . . 14 class
2319, 21, 22co 6690 . . . . . . . . . . . . 13 class (𝑝𝑛)
24 cdvds 15027 . . . . . . . . . . . . 13 class
2523, 11, 24wbr 4685 . . . . . . . . . . . 12 wff (𝑝𝑛) ∥ 𝑥
26 cn0 11330 . . . . . . . . . . . 12 class 0
2725, 20, 26crab 2945 . . . . . . . . . . 11 class {𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}
28 cr 9973 . . . . . . . . . . 11 class
29 clt 10112 . . . . . . . . . . 11 class <
3027, 28, 29csup 8387 . . . . . . . . . 10 class sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < )
3123, 13, 24wbr 4685 . . . . . . . . . . . 12 wff (𝑝𝑛) ∥ 𝑦
3231, 20, 26crab 2945 . . . . . . . . . . 11 class {𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}
3332, 28, 29csup 8387 . . . . . . . . . 10 class sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )
34 cmin 10304 . . . . . . . . . 10 class
3530, 33, 34co 6690 . . . . . . . . 9 class (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))
3618, 35wceq 1523 . . . . . . . 8 wff 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))
3716, 36wa 383 . . . . . . 7 wff (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
38 cn 11058 . . . . . . 7 class
3937, 12, 38wrex 2942 . . . . . 6 wff 𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
40 cz 11415 . . . . . 6 class
4139, 10, 40wrex 2942 . . . . 5 wff 𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))
4241, 17cio 5887 . . . 4 class (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))
438, 9, 42cif 4119 . . 3 class if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < )))))
442, 3, 4, 5, 43cmpt2 6692 . 2 class (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))))
451, 44wceq 1523 1 wff pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝𝑛) ∥ 𝑦}, ℝ, < ))))))
Colors of variables: wff setvar class
This definition is referenced by:  pcval  15596  pc0  15606
  Copyright terms: Public domain W3C validator