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

Definition df-odz 12833
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 12831 . 2  class  od Z
2 vn . . 3  set  n
3 cn 9746 . . 3  class  NN
4 vx . . . 4  set  x
54cv 1622 . . . . . . 7  class  x
62cv 1622 . . . . . . 7  class  n
7 cgcd 12685 . . . . . . 7  class  gcd
85, 6, 7co 5858 . . . . . 6  class  ( x  gcd  n )
9 c1 8738 . . . . . 6  class  1
108, 9wceq 1623 . . . . 5  wff  ( x  gcd  n )  =  1
11 cz 10024 . . . . 5  class  ZZ
1210, 4, 11crab 2547 . . . 4  class  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }
13 vm . . . . . . . . . 10  set  m
1413cv 1622 . . . . . . . . 9  class  m
15 cexp 11104 . . . . . . . . 9  class  ^
165, 14, 15co 5858 . . . . . . . 8  class  ( x ^ m )
17 cmin 9037 . . . . . . . 8  class  -
1816, 9, 17co 5858 . . . . . . 7  class  ( ( x ^ m )  -  1 )
19 cdivides 12531 . . . . . . 7  class  ||
206, 18, 19wbr 4023 . . . . . 6  wff  n  ||  ( ( x ^
m )  -  1 )
2120, 13, 3crab 2547 . . . . 5  class  { m  e.  NN  |  n  ||  ( ( x ^
m )  -  1 ) }
22 cr 8736 . . . . 5  class  RR
23 clt 8867 . . . . . 6  class  <
2423ccnv 4688 . . . . 5  class  `'  <
2521, 22, 24csup 7193 . . . 4  class  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  )
264, 12, 25cmpt 4077 . . 3  class  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |->  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  ) )
272, 3, 26cmpt 4077 . 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 1623 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  12856
  Copyright terms: Public domain W3C validator