Definition df-pc 16466

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

Step	Hyp	Ref	Expression
1		cpc 16465	. 2 class pCnt
2		vp	. . 3 setvar 𝑝
3		vr	. . 3 setvar 𝑟
4		cprime 16304	. . 3 class ℙ
5		cq 12617	. . 3 class ℚ
6	3	cv 1538	. . . . 5 class 𝑟
7		cc0 10802	. . . . 5 class 0
8	6, 7	wceq 1539	. . . 4 wff 𝑟 = 0
9		cpnf 10937	. . . 4 class +∞
10		vx	. . . . . . . . . . 11 setvar 𝑥
11	10	cv 1538	. . . . . . . . . 10 class 𝑥
12		vy	. . . . . . . . . . 11 setvar 𝑦
13	12	cv 1538	. . . . . . . . . 10 class 𝑦
14		cdiv 11562	. . . . . . . . . 10 class /
15	11, 13, 14	co 7255	. . . . . . . . 9 class (𝑥 / 𝑦)
16	6, 15	wceq 1539	. . . . . . . 8 wff 𝑟 = (𝑥 / 𝑦)
17		vz	. . . . . . . . . 10 setvar 𝑧
18	17	cv 1538	. . . . . . . . 9 class 𝑧
19	2	cv 1538	. . . . . . . . . . . . . 14 class 𝑝
20		vn	. . . . . . . . . . . . . . 15 setvar 𝑛
21	20	cv 1538	. . . . . . . . . . . . . 14 class 𝑛
22		cexp 13710	. . . . . . . . . . . . . 14 class ↑
23	19, 21, 22	co 7255	. . . . . . . . . . . . 13 class (𝑝↑𝑛)
24		cdvds 15891	. . . . . . . . . . . . 13 class ∥
25	23, 11, 24	wbr 5070	. . . . . . . . . . . 12 wff (𝑝↑𝑛) ∥ 𝑥
26		cn0 12163	. . . . . . . . . . . 12 class ℕ0
27	25, 20, 26	crab 3067	. . . . . . . . . . 11 class {𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}
28		cr 10801	. . . . . . . . . . 11 class ℝ
29		clt 10940	. . . . . . . . . . 11 class <
30	27, 28, 29	csup 9129	. . . . . . . . . 10 class sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < )
31	23, 13, 24	wbr 5070	. . . . . . . . . . . 12 wff (𝑝↑𝑛) ∥ 𝑦
32	31, 20, 26	crab 3067	. . . . . . . . . . 11 class {𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}
33	32, 28, 29	csup 9129	. . . . . . . . . 10 class sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < )
34		cmin 11135	. . . . . . . . . 10 class −
35	30, 33, 34	co 7255	. . . . . . . . 9 class (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < ))
36	18, 35	wceq 1539	. . . . . . . 8 wff 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < ))
37	16, 36	wa 395	. . . . . . 7 wff (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < )))
38		cn 11903	. . . . . . 7 class ℕ
39	37, 12, 38	wrex 3064	. . . . . 6 wff ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < )))
40		cz 12249	. . . . . 6 class ℤ
41	39, 10, 40	wrex 3064	. . . . 5 wff ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < )))
42	41, 17	cio 6374	. . . 4 class (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < ))))
43	8, 9, 42	cif 4456	. . 3 class if(𝑟 = 0, +∞, (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < )))))
44	2, 3, 4, 5, 43	cmpo 7257	. 2 class (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < ))))))
45	1, 44	wceq 1539	1 wff pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < ))))))

This definition is referenced by:  pcval  16473  pc0  16483