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

Definition df-odz 12849
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 12847 . 2  class  od Z
2 vn . . 3  set  n
3 cn 9762 . . 3  class  NN
4 vx . . . 4  set  x
54cv 1631 . . . . . . 7  class  x
62cv 1631 . . . . . . 7  class  n
7 cgcd 12701 . . . . . . 7  class  gcd
85, 6, 7co 5874 . . . . . 6  class  ( x  gcd  n )
9 c1 8754 . . . . . 6  class  1
108, 9wceq 1632 . . . . 5  wff  ( x  gcd  n )  =  1
11 cz 10040 . . . . 5  class  ZZ
1210, 4, 11crab 2560 . . . 4  class  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }
13 vm . . . . . . . . . 10  set  m
1413cv 1631 . . . . . . . . 9  class  m
15 cexp 11120 . . . . . . . . 9  class  ^
165, 14, 15co 5874 . . . . . . . 8  class  ( x ^ m )
17 cmin 9053 . . . . . . . 8  class  -
1816, 9, 17co 5874 . . . . . . 7  class  ( ( x ^ m )  -  1 )
19 cdivides 12547 . . . . . . 7  class  ||
206, 18, 19wbr 4039 . . . . . 6  wff  n  ||  ( ( x ^
m )  -  1 )
2120, 13, 3crab 2560 . . . . 5  class  { m  e.  NN  |  n  ||  ( ( x ^
m )  -  1 ) }
22 cr 8752 . . . . 5  class  RR
23 clt 8883 . . . . . 6  class  <
2423ccnv 4704 . . . . 5  class  `'  <
2521, 22, 24csup 7209 . . . 4  class  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  )
264, 12, 25cmpt 4093 . . 3  class  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |->  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  ) )
272, 3, 26cmpt 4093 . 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 1632 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  12872
  Copyright terms: Public domain W3C validator