Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-odz Unicode version

Definition df-odz 14295
 Description: Define the order function on the class of integers mod N. (Contributed by Mario Carneiro, 23-Feb-2014.)
Assertion
Ref Expression
df-odz
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-odz
StepHypRef Expression
1 codz 14293 . 2
2 vn . . 3
3 cn 10561 . . 3
4 vx . . . 4
54cv 1394 . . . . . . 7
62cv 1394 . . . . . . 7
7 cgcd 14144 . . . . . . 7
85, 6, 7co 6296 . . . . . 6
9 c1 9514 . . . . . 6
108, 9wceq 1395 . . . . 5
11 cz 10889 . . . . 5
1210, 4, 11crab 2811 . . . 4
13 vm . . . . . . . . . 10
1413cv 1394 . . . . . . . . 9
15 cexp 12166 . . . . . . . . 9
165, 14, 15co 6296 . . . . . . . 8
17 cmin 9828 . . . . . . . 8
1816, 9, 17co 6296 . . . . . . 7
19 cdvds 13986 . . . . . . 7
206, 18, 19wbr 4452 . . . . . 6
2120, 13, 3crab 2811 . . . . 5
22 cr 9512 . . . . 5
23 clt 9649 . . . . . 6
2423ccnv 5003 . . . . 5
2521, 22, 24csup 7920 . . . 4
264, 12, 25cmpt 4510 . . 3
272, 3, 26cmpt 4510 . 2
281, 27wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  odzval  14318
 Copyright terms: Public domain W3C validator