MPE Home 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  |-  od Z  =  ( n  e.  NN  |->  ( x  e. 
{ x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |->  sup ( { m  e.  NN  |  n  ||  ( ( x ^
m )  -  1 ) } ,  RR ,  `'  <  ) ) )
Distinct variable group:    m, n, x

Detailed syntax breakdown of Definition df-odz
StepHypRef Expression
1 codz 13154 . 2  class  od Z
2 vn . . 3  set  n
3 cn 10002 . . 3  class  NN
4 vx . . . 4  set  x
54cv 1652 . . . . . . 7  class  x
62cv 1652 . . . . . . 7  class  n
7 cgcd 13008 . . . . . . 7  class  gcd
85, 6, 7co 6083 . . . . . 6  class  ( x  gcd  n )
9 c1 8993 . . . . . 6  class  1
108, 9wceq 1653 . . . . 5  wff  ( x  gcd  n )  =  1
11 cz 10284 . . . . 5  class  ZZ
1210, 4, 11crab 2711 . . . 4  class  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }
13 vm . . . . . . . . . 10  set  m
1413cv 1652 . . . . . . . . 9  class  m
15 cexp 11384 . . . . . . . . 9  class  ^
165, 14, 15co 6083 . . . . . . . 8  class  ( x ^ m )
17 cmin 9293 . . . . . . . 8  class  -
1816, 9, 17co 6083 . . . . . . 7  class  ( ( x ^ m )  -  1 )
19 cdivides 12854 . . . . . . 7  class  ||
206, 18, 19wbr 4214 . . . . . 6  wff  n  ||  ( ( x ^
m )  -  1 )
2120, 13, 3crab 2711 . . . . 5  class  { m  e.  NN  |  n  ||  ( ( x ^
m )  -  1 ) }
22 cr 8991 . . . . 5  class  RR
23 clt 9122 . . . . . 6  class  <
2423ccnv 4879 . . . . 5  class  `'  <
2521, 22, 24csup 7447 . . . 4  class  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  )
264, 12, 25cmpt 4268 . . 3  class  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |->  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  ) )
272, 3, 26cmpt 4268 . 2  class  ( n  e.  NN  |->  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |->  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  ) ) )
281, 27wceq 1653 1  wff  od Z  =  ( n  e.  NN  |->  ( x  e. 
{ x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |->  sup ( { m  e.  NN  |  n  ||  ( ( x ^
m )  -  1 ) } ,  RR ,  `'  <  ) ) )
Colors of variables: wff set class
This definition is referenced by:  odzval  13179
  Copyright terms: Public domain W3C validator