This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpc ⊢ pCnt
1 vp ⊢ 𝑝
2 cprime ⊢ ℙ
3 vr ⊢ 𝑟
4 cq ⊢ ℚ
5 3 cv ⊢ 𝑟
6 cc0 ⊢ 0
7 5 6 wceq ⊢ 𝑟 = 0
8 cpnf ⊢ +∞
9 vz ⊢ 𝑧
10 vx ⊢ 𝑥
11 cz ⊢ ℤ
12 vy ⊢ 𝑦
13 cn ⊢ ℕ
14 10 cv ⊢ 𝑥
15 cdiv ⊢ /
16 12 cv ⊢ 𝑦
17 14 16 15 co ⊢ ( 𝑥 / 𝑦 )
18 5 17 wceq ⊢ 𝑟 = ( 𝑥 / 𝑦 )
19 9 cv ⊢ 𝑧
20 vn ⊢ 𝑛
21 cn0 ⊢ ℕ0
22 1 cv ⊢ 𝑝
23 cexp ⊢ ↑
24 20 cv ⊢ 𝑛
25 22 24 23 co ⊢ ( 𝑝 ↑ 𝑛 )
26 cdvds ⊢ ∥
27 25 14 26 wbr ⊢ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥
28 27 20 21 crab ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 }
29 cr ⊢ ℝ
30 clt ⊢ <
31 28 29 30 csup ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < )
32 cmin ⊢ −
33 25 16 26 wbr ⊢ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦
34 33 20 21 crab ⊢ { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 }
35 34 29 30 csup ⊢ sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < )
36 31 35 32 co ⊢ ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) )
37 19 36 wceq ⊢ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) )
38 18 37 wa ⊢ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) )
39 38 12 13 wrex ⊢ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) )
40 39 10 11 wrex ⊢ ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) )
41 40 9 cio ⊢ ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) )
42 7 8 41 cif ⊢ if ( 𝑟 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) )
43 1 3 2 4 42 cmpo ⊢ ( 𝑝 ∈ ℙ , 𝑟 ∈ ℚ ↦ if ( 𝑟 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) ) )
44 0 43 wceq ⊢ pCnt = ( 𝑝 ∈ ℙ , 𝑟 ∈ ℚ ↦ if ( 𝑟 = 0 , +∞ , ( ℩ 𝑧 ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℕ ( 𝑟 = ( 𝑥 / 𝑦 ) ∧ 𝑧 = ( sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑥 } , ℝ , < ) − sup ( { 𝑛 ∈ ℕ0 ∣ ( 𝑝 ↑ 𝑛 ) ∥ 𝑦 } , ℝ , < ) ) ) ) ) )