Detailed syntax breakdown of Definition df-eqp
Step | Hyp | Ref
| Expression |
1 | | ceqp 33605 |
. 2
class
~Qp |
2 | | vp |
. . 3
setvar 𝑝 |
3 | | cprime 16374 |
. . 3
class
ℙ |
4 | | vf |
. . . . . . . 8
setvar 𝑓 |
5 | 4 | cv 1538 |
. . . . . . 7
class 𝑓 |
6 | | vg |
. . . . . . . 8
setvar 𝑔 |
7 | 6 | cv 1538 |
. . . . . . 7
class 𝑔 |
8 | 5, 7 | cpr 4565 |
. . . . . 6
class {𝑓, 𝑔} |
9 | | cz 12317 |
. . . . . . 7
class
ℤ |
10 | | cmap 8613 |
. . . . . . 7
class
↑m |
11 | 9, 9, 10 | co 7277 |
. . . . . 6
class (ℤ
↑m ℤ) |
12 | 8, 11 | wss 3888 |
. . . . 5
wff {𝑓, 𝑔} ⊆ (ℤ ↑m
ℤ) |
13 | | vn |
. . . . . . . . . . 11
setvar 𝑛 |
14 | 13 | cv 1538 |
. . . . . . . . . 10
class 𝑛 |
15 | 14 | cneg 11204 |
. . . . . . . . 9
class -𝑛 |
16 | | cuz 12580 |
. . . . . . . . 9
class
ℤ≥ |
17 | 15, 16 | cfv 6435 |
. . . . . . . 8
class
(ℤ≥‘-𝑛) |
18 | | vk |
. . . . . . . . . . . . 13
setvar 𝑘 |
19 | 18 | cv 1538 |
. . . . . . . . . . . 12
class 𝑘 |
20 | 19 | cneg 11204 |
. . . . . . . . . . 11
class -𝑘 |
21 | 20, 5 | cfv 6435 |
. . . . . . . . . 10
class (𝑓‘-𝑘) |
22 | 20, 7 | cfv 6435 |
. . . . . . . . . 10
class (𝑔‘-𝑘) |
23 | | cmin 11203 |
. . . . . . . . . 10
class
− |
24 | 21, 22, 23 | co 7277 |
. . . . . . . . 9
class ((𝑓‘-𝑘) − (𝑔‘-𝑘)) |
25 | 2 | cv 1538 |
. . . . . . . . . 10
class 𝑝 |
26 | | c1 10870 |
. . . . . . . . . . . 12
class
1 |
27 | | caddc 10872 |
. . . . . . . . . . . 12
class
+ |
28 | 14, 26, 27 | co 7277 |
. . . . . . . . . . 11
class (𝑛 + 1) |
29 | 19, 28, 27 | co 7277 |
. . . . . . . . . 10
class (𝑘 + (𝑛 + 1)) |
30 | | cexp 13780 |
. . . . . . . . . 10
class
↑ |
31 | 25, 29, 30 | co 7277 |
. . . . . . . . 9
class (𝑝↑(𝑘 + (𝑛 + 1))) |
32 | | cdiv 11630 |
. . . . . . . . 9
class
/ |
33 | 24, 31, 32 | co 7277 |
. . . . . . . 8
class (((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) |
34 | 17, 33, 18 | csu 15395 |
. . . . . . 7
class
Σ𝑘 ∈
(ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) |
35 | 34, 9 | wcel 2106 |
. . . . . 6
wff
Σ𝑘 ∈
(ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ |
36 | 35, 13, 9 | wral 3064 |
. . . . 5
wff
∀𝑛 ∈
ℤ Σ𝑘 ∈
(ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ |
37 | 12, 36 | wa 396 |
. . . 4
wff ({𝑓, 𝑔} ⊆ (ℤ ↑m
ℤ) ∧ ∀𝑛
∈ ℤ Σ𝑘
∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ) |
38 | 37, 4, 6 | copab 5138 |
. . 3
class
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m
ℤ) ∧ ∀𝑛
∈ ℤ Σ𝑘
∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)} |
39 | 2, 3, 38 | cmpt 5159 |
. 2
class (𝑝 ∈ ℙ ↦
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m
ℤ) ∧ ∀𝑛
∈ ℤ Σ𝑘
∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)}) |
40 | 1, 39 | wceq 1539 |
1
wff ~Qp =
(𝑝 ∈ ℙ ↦
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ (ℤ ↑m
ℤ) ∧ ∀𝑛
∈ ℤ Σ𝑘
∈ (ℤ≥‘-𝑛)(((𝑓‘-𝑘) − (𝑔‘-𝑘)) / (𝑝↑(𝑘 + (𝑛 + 1)))) ∈ ℤ)}) |