Description: Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by Stefan O'Rear, 4-Sep-2015) (Revised by AV, 26-Sep-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-gex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cgex | |
|
1 | vg | |
|
2 | cvv | |
|
3 | vn | |
|
4 | cn | |
|
5 | vx | |
|
6 | cbs | |
|
7 | 1 | cv | |
8 | 7 6 | cfv | |
9 | 3 | cv | |
10 | cmg | |
|
11 | 7 10 | cfv | |
12 | 5 | cv | |
13 | 9 12 11 | co | |
14 | c0g | |
|
15 | 7 14 | cfv | |
16 | 13 15 | wceq | |
17 | 16 5 8 | wral | |
18 | 17 3 4 | crab | |
19 | vi | |
|
20 | 19 | cv | |
21 | c0 | |
|
22 | 20 21 | wceq | |
23 | cc0 | |
|
24 | cr | |
|
25 | clt | |
|
26 | 20 24 25 | cinf | |
27 | 22 23 26 | cif | |
28 | 19 18 27 | csb | |
29 | 1 2 28 | cmpt | |
30 | 0 29 | wceq | |