Detailed syntax breakdown of Definition df-gfoo
Step | Hyp | Ref
| Expression |
1 | | cgfo 31540 |
. 2
GF∞ |
2 | | vp |
. . 3
|
3 | | cprime 15385 |
. . 3
|
4 | | vr |
. . . 4
|
5 | 2 | cv 1482 |
. . . . 5
|
6 | | czn 19851 |
. . . . 5
ℤ/nℤ |
7 | 5, 6 | cfv 5888 |
. . . 4
ℤ/nℤ |
8 | 4 | cv 1482 |
. . . . 5
|
9 | | vn |
. . . . . 6
|
10 | | cn 11020 |
. . . . . 6
|
11 | | vs |
. . . . . . . 8
|
12 | | cpl1 19547 |
. . . . . . . . 9
Poly1 |
13 | 8, 12 | cfv 5888 |
. . . . . . . 8
Poly1 |
14 | | vx |
. . . . . . . . 9
|
15 | | cv1 19546 |
. . . . . . . . . 10
var1 |
16 | 8, 15 | cfv 5888 |
. . . . . . . . 9
var1 |
17 | 9 | cv 1482 |
. . . . . . . . . . . 12
|
18 | | cexp 12860 |
. . . . . . . . . . . 12
|
19 | 5, 17, 18 | co 6650 |
. . . . . . . . . . 11
|
20 | 14 | cv 1482 |
. . . . . . . . . . 11
|
21 | 11 | cv 1482 |
. . . . . . . . . . . . 13
|
22 | | cmgp 18489 |
. . . . . . . . . . . . 13
mulGrp |
23 | 21, 22 | cfv 5888 |
. . . . . . . . . . . 12
mulGrp |
24 | | cmg 17540 |
. . . . . . . . . . . 12
.g |
25 | 23, 24 | cfv 5888 |
. . . . . . . . . . 11
.gmulGrp |
26 | 19, 20, 25 | co 6650 |
. . . . . . . . . 10
.gmulGrp |
27 | | csg 17424 |
. . . . . . . . . . 11
|
28 | 21, 27 | cfv 5888 |
. . . . . . . . . 10
|
29 | 26, 20, 28 | co 6650 |
. . . . . . . . 9
.gmulGrp |
30 | 14, 16, 29 | csb 3533 |
. . . . . . . 8
var1 .gmulGrp |
31 | 11, 13, 30 | csb 3533 |
. . . . . . 7
Poly1 var1 .gmulGrp |
32 | 31 | csn 4177 |
. . . . . 6
Poly1 var1 .gmulGrp |
33 | 9, 10, 32 | cmpt 4729 |
. . . . 5
Poly1 var1 .gmulGrp |
34 | | cpsl 31529 |
. . . . 5
polySplitLim |
35 | 8, 33, 34 | co 6650 |
. . . 4
polySplitLim
Poly1 var1 .gmulGrp |
36 | 4, 7, 35 | csb 3533 |
. . 3
ℤ/nℤ
polySplitLim Poly1 var1 .gmulGrp |
37 | 2, 3, 36 | cmpt 4729 |
. 2
ℤ/nℤ
polySplitLim Poly1 var1 .gmulGrp |
38 | 1, 37 | wceq 1483 |
1
GF∞
ℤ/nℤ polySplitLim
Poly1 var1 .gmulGrp |