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

Definition df-odz 13156
 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 13154 . 2
2 vn . . 3
3 cn 10002 . . 3
4 vx . . . 4
54cv 1652 . . . . . . 7
62cv 1652 . . . . . . 7
7 cgcd 13008 . . . . . . 7
85, 6, 7co 6083 . . . . . 6
9 c1 8993 . . . . . 6
108, 9wceq 1653 . . . . 5
11 cz 10284 . . . . 5
1210, 4, 11crab 2711 . . . 4
13 vm . . . . . . . . . 10
1413cv 1652 . . . . . . . . 9
15 cexp 11384 . . . . . . . . 9
165, 14, 15co 6083 . . . . . . . 8
17 cmin 9293 . . . . . . . 8
1816, 9, 17co 6083 . . . . . . 7
19 cdivides 12854 . . . . . . 7
206, 18, 19wbr 4214 . . . . . 6
2120, 13, 3crab 2711 . . . . 5
22 cr 8991 . . . . 5
23 clt 9122 . . . . . 6
2423ccnv 4879 . . . . 5
2521, 22, 24csup 7447 . . . 4
264, 12, 25cmpt 4268 . . 3
272, 3, 26cmpt 4268 . 2
281, 27wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  odzval  13179
 Copyright terms: Public domain W3C validator