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

Definition df-odz 14143
 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 14141 . 2
2 vn . . 3
3 cn 10525 . . 3
4 vx . . . 4
54cv 1373 . . . . . . 7
62cv 1373 . . . . . . 7
7 cgcd 13992 . . . . . . 7
85, 6, 7co 6275 . . . . . 6
9 c1 9482 . . . . . 6
108, 9wceq 1374 . . . . 5
11 cz 10853 . . . . 5
1210, 4, 11crab 2811 . . . 4
13 vm . . . . . . . . . 10
1413cv 1373 . . . . . . . . 9
15 cexp 12122 . . . . . . . . 9
165, 14, 15co 6275 . . . . . . . 8
17 cmin 9794 . . . . . . . 8
1816, 9, 17co 6275 . . . . . . 7
19 cdivides 13836 . . . . . . 7
206, 18, 19wbr 4440 . . . . . 6
2120, 13, 3crab 2811 . . . . 5
22 cr 9480 . . . . 5
23 clt 9617 . . . . . 6
2423ccnv 4991 . . . . 5
2521, 22, 24csup 7889 . . . 4
264, 12, 25cmpt 4498 . . 3
272, 3, 26cmpt 4498 . 2
281, 27wceq 1374 1
 Colors of variables: wff setvar class This definition is referenced by:  odzval  14166
 Copyright terms: Public domain W3C validator