Detailed syntax breakdown of Definition df-qp
Step | Hyp | Ref
| Expression |
1 | | cqp 33606 |
. 2
class
Qp |
2 | | vp |
. . 3
setvar 𝑝 |
3 | | cprime 16374 |
. . 3
class
ℙ |
4 | | vb |
. . . 4
setvar 𝑏 |
5 | | vh |
. . . . . . . . . 10
setvar ℎ |
6 | 5 | cv 1541 |
. . . . . . . . 9
class ℎ |
7 | 6 | ccnv 5589 |
. . . . . . . 8
class ◡ℎ |
8 | | cz 12319 |
. . . . . . . . 9
class
ℤ |
9 | | cc0 10872 |
. . . . . . . . . 10
class
0 |
10 | 9 | csn 4567 |
. . . . . . . . 9
class
{0} |
11 | 8, 10 | cdif 3889 |
. . . . . . . 8
class (ℤ
∖ {0}) |
12 | 7, 11 | cima 5593 |
. . . . . . 7
class (◡ℎ “ (ℤ ∖
{0})) |
13 | | vx |
. . . . . . . 8
setvar 𝑥 |
14 | 13 | cv 1541 |
. . . . . . 7
class 𝑥 |
15 | 12, 14 | wss 3892 |
. . . . . 6
wff (◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥 |
16 | | cuz 12581 |
. . . . . . 7
class
ℤ≥ |
17 | 16 | crn 5591 |
. . . . . 6
class ran
ℤ≥ |
18 | 15, 13, 17 | wrex 3067 |
. . . . 5
wff
∃𝑥 ∈ ran
ℤ≥(◡ℎ “ (ℤ ∖ {0}))
⊆ 𝑥 |
19 | 2 | cv 1541 |
. . . . . . . 8
class 𝑝 |
20 | | c1 10873 |
. . . . . . . 8
class
1 |
21 | | cmin 11205 |
. . . . . . . 8
class
− |
22 | 19, 20, 21 | co 7271 |
. . . . . . 7
class (𝑝 − 1) |
23 | | cfz 13238 |
. . . . . . 7
class
... |
24 | 9, 22, 23 | co 7271 |
. . . . . 6
class
(0...(𝑝 −
1)) |
25 | | cmap 8598 |
. . . . . 6
class
↑m |
26 | 8, 24, 25 | co 7271 |
. . . . 5
class (ℤ
↑m (0...(𝑝
− 1))) |
27 | 18, 5, 26 | crab 3070 |
. . . 4
class {ℎ ∈ (ℤ
↑m (0...(𝑝
− 1))) ∣ ∃𝑥 ∈ ran ℤ≥(◡ℎ “ (ℤ ∖ {0})) ⊆ 𝑥} |
28 | | cnx 16892 |
. . . . . . . . 9
class
ndx |
29 | | cbs 16910 |
. . . . . . . . 9
class
Base |
30 | 28, 29 | cfv 6432 |
. . . . . . . 8
class
(Base‘ndx) |
31 | 4 | cv 1541 |
. . . . . . . 8
class 𝑏 |
32 | 30, 31 | cop 4573 |
. . . . . . 7
class
〈(Base‘ndx), 𝑏〉 |
33 | | cplusg 16960 |
. . . . . . . . 9
class
+g |
34 | 28, 33 | cfv 6432 |
. . . . . . . 8
class
(+g‘ndx) |
35 | | vf |
. . . . . . . . 9
setvar 𝑓 |
36 | | vg |
. . . . . . . . 9
setvar 𝑔 |
37 | 35 | cv 1541 |
. . . . . . . . . . 11
class 𝑓 |
38 | 36 | cv 1541 |
. . . . . . . . . . 11
class 𝑔 |
39 | | caddc 10875 |
. . . . . . . . . . . 12
class
+ |
40 | 39 | cof 7525 |
. . . . . . . . . . 11
class
∘f + |
41 | 37, 38, 40 | co 7271 |
. . . . . . . . . 10
class (𝑓 ∘f + 𝑔) |
42 | | crqp 33605 |
. . . . . . . . . . 11
class
/Qp |
43 | 19, 42 | cfv 6432 |
. . . . . . . . . 10
class
(/Qp‘𝑝) |
44 | 41, 43 | cfv 6432 |
. . . . . . . . 9
class
((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)) |
45 | 35, 36, 31, 31, 44 | cmpo 7273 |
. . . . . . . 8
class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔))) |
46 | 34, 45 | cop 4573 |
. . . . . . 7
class
〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉 |
47 | | cmulr 16961 |
. . . . . . . . 9
class
.r |
48 | 28, 47 | cfv 6432 |
. . . . . . . 8
class
(.r‘ndx) |
49 | | vn |
. . . . . . . . . . 11
setvar 𝑛 |
50 | | vk |
. . . . . . . . . . . . . . 15
setvar 𝑘 |
51 | 50 | cv 1541 |
. . . . . . . . . . . . . 14
class 𝑘 |
52 | 51, 37 | cfv 6432 |
. . . . . . . . . . . . 13
class (𝑓‘𝑘) |
53 | 49 | cv 1541 |
. . . . . . . . . . . . . . 15
class 𝑛 |
54 | 53, 51, 21 | co 7271 |
. . . . . . . . . . . . . 14
class (𝑛 − 𝑘) |
55 | 54, 38 | cfv 6432 |
. . . . . . . . . . . . 13
class (𝑔‘(𝑛 − 𝑘)) |
56 | | cmul 10877 |
. . . . . . . . . . . . 13
class
· |
57 | 52, 55, 56 | co 7271 |
. . . . . . . . . . . 12
class ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))) |
58 | 8, 57, 50 | csu 15395 |
. . . . . . . . . . 11
class
Σ𝑘 ∈
ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))) |
59 | 49, 8, 58 | cmpt 5162 |
. . . . . . . . . 10
class (𝑛 ∈ ℤ ↦
Σ𝑘 ∈ ℤ
((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))) |
60 | 59, 43 | cfv 6432 |
. . . . . . . . 9
class
((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))) |
61 | 35, 36, 31, 31, 60 | cmpo 7273 |
. . . . . . . 8
class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘)))))) |
62 | 48, 61 | cop 4573 |
. . . . . . 7
class
〈(.r‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉 |
63 | 32, 46, 62 | ctp 4571 |
. . . . . 6
class
{〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉} |
64 | | cple 16967 |
. . . . . . . . 9
class
le |
65 | 28, 64 | cfv 6432 |
. . . . . . . 8
class
(le‘ndx) |
66 | 37, 38 | cpr 4569 |
. . . . . . . . . . 11
class {𝑓, 𝑔} |
67 | 66, 31 | wss 3892 |
. . . . . . . . . 10
wff {𝑓, 𝑔} ⊆ 𝑏 |
68 | 51 | cneg 11206 |
. . . . . . . . . . . . . 14
class -𝑘 |
69 | 68, 37 | cfv 6432 |
. . . . . . . . . . . . 13
class (𝑓‘-𝑘) |
70 | 19, 20, 39 | co 7271 |
. . . . . . . . . . . . . 14
class (𝑝 + 1) |
71 | | cexp 13780 |
. . . . . . . . . . . . . 14
class
↑ |
72 | 70, 68, 71 | co 7271 |
. . . . . . . . . . . . 13
class ((𝑝 + 1)↑-𝑘) |
73 | 69, 72, 56 | co 7271 |
. . . . . . . . . . . 12
class ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) |
74 | 8, 73, 50 | csu 15395 |
. . . . . . . . . . 11
class
Σ𝑘 ∈
ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) |
75 | 68, 38 | cfv 6432 |
. . . . . . . . . . . . 13
class (𝑔‘-𝑘) |
76 | 75, 72, 56 | co 7271 |
. . . . . . . . . . . 12
class ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)) |
77 | 8, 76, 50 | csu 15395 |
. . . . . . . . . . 11
class
Σ𝑘 ∈
ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)) |
78 | | clt 11010 |
. . . . . . . . . . 11
class
< |
79 | 74, 77, 78 | wbr 5079 |
. . . . . . . . . 10
wff
Σ𝑘 ∈
ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)) |
80 | 67, 79 | wa 396 |
. . . . . . . . 9
wff ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘))) |
81 | 80, 35, 36 | copab 5141 |
. . . . . . . 8
class
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))} |
82 | 65, 81 | cop 4573 |
. . . . . . 7
class
〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉 |
83 | 82 | csn 4567 |
. . . . . 6
class
{〈(le‘ndx), {〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉} |
84 | 63, 83 | cun 3890 |
. . . . 5
class
({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉} ∪ {〈(le‘ndx),
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉}) |
85 | 8, 10 | cxp 5588 |
. . . . . . . 8
class (ℤ
× {0}) |
86 | 37, 85 | wceq 1542 |
. . . . . . 7
wff 𝑓 = (ℤ ×
{0}) |
87 | 37 | ccnv 5589 |
. . . . . . . . . . 11
class ◡𝑓 |
88 | 87, 11 | cima 5593 |
. . . . . . . . . 10
class (◡𝑓 “ (ℤ ∖
{0})) |
89 | | cr 10871 |
. . . . . . . . . 10
class
ℝ |
90 | 88, 89, 78 | cinf 9178 |
. . . . . . . . 9
class
inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< ) |
91 | 90 | cneg 11206 |
. . . . . . . 8
class
-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< ) |
92 | 19, 91, 71 | co 7271 |
. . . . . . 7
class (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< )) |
93 | 86, 9, 92 | cif 4465 |
. . . . . 6
class if(𝑓 = (ℤ × {0}), 0,
(𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< ))) |
94 | 35, 31, 93 | cmpt 5162 |
. . . . 5
class (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< )))) |
95 | | ctng 23732 |
. . . . 5
class
toNrmGrp |
96 | 84, 94, 95 | co 7271 |
. . . 4
class
(({〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉} ∪ {〈(le‘ndx),
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< ))))) |
97 | 4, 27, 96 | csb 3837 |
. . 3
class
⦋{ℎ
∈ (ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran
ℤ≥(◡ℎ “ (ℤ ∖ {0}))
⊆ 𝑥} / 𝑏⦌(({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉} ∪ {〈(le‘ndx),
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< ))))) |
98 | 2, 3, 97 | cmpt 5162 |
. 2
class (𝑝 ∈ ℙ ↦
⦋{ℎ ∈
(ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran
ℤ≥(◡ℎ “ (ℤ ∖ {0}))
⊆ 𝑥} / 𝑏⦌(({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉} ∪ {〈(le‘ndx),
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< )))))) |
99 | 1, 98 | wceq 1542 |
1
wff Qp = (𝑝 ∈ ℙ ↦
⦋{ℎ ∈
(ℤ ↑m (0...(𝑝 − 1))) ∣ ∃𝑥 ∈ ran
ℤ≥(◡ℎ “ (ℤ ∖ {0}))
⊆ 𝑥} / 𝑏⦌(({〈(Base‘ndx),
𝑏〉,
〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑓 ∘f + 𝑔)))〉, 〈(.r‘ndx),
(𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ ((/Qp‘𝑝)‘(𝑛 ∈ ℤ ↦ Σ𝑘 ∈ ℤ ((𝑓‘𝑘) · (𝑔‘(𝑛 − 𝑘))))))〉} ∪ {〈(le‘ndx),
{〈𝑓, 𝑔〉 ∣ ({𝑓, 𝑔} ⊆ 𝑏 ∧ Σ𝑘 ∈ ℤ ((𝑓‘-𝑘) · ((𝑝 + 1)↑-𝑘)) < Σ𝑘 ∈ ℤ ((𝑔‘-𝑘) · ((𝑝 + 1)↑-𝑘)))}〉}) toNrmGrp (𝑓 ∈ 𝑏 ↦ if(𝑓 = (ℤ × {0}), 0, (𝑝↑-inf((◡𝑓 “ (ℤ ∖ {0})), ℝ,
< )))))) |