MPE Home 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  |-  odZ 
=  ( 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 14141 . 2  class  odZ
2 vn . . 3  setvar  n
3 cn 10525 . . 3  class  NN
4 vx . . . 4  setvar  x
54cv 1373 . . . . . . 7  class  x
62cv 1373 . . . . . . 7  class  n
7 cgcd 13992 . . . . . . 7  class  gcd
85, 6, 7co 6275 . . . . . 6  class  ( x  gcd  n )
9 c1 9482 . . . . . 6  class  1
108, 9wceq 1374 . . . . 5  wff  ( x  gcd  n )  =  1
11 cz 10853 . . . . 5  class  ZZ
1210, 4, 11crab 2811 . . . 4  class  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }
13 vm . . . . . . . . . 10  setvar  m
1413cv 1373 . . . . . . . . 9  class  m
15 cexp 12122 . . . . . . . . 9  class  ^
165, 14, 15co 6275 . . . . . . . 8  class  ( x ^ m )
17 cmin 9794 . . . . . . . 8  class  -
1816, 9, 17co 6275 . . . . . . 7  class  ( ( x ^ m )  -  1 )
19 cdivides 13836 . . . . . . 7  class  ||
206, 18, 19wbr 4440 . . . . . 6  wff  n  ||  ( ( x ^
m )  -  1 )
2120, 13, 3crab 2811 . . . . 5  class  { m  e.  NN  |  n  ||  ( ( x ^
m )  -  1 ) }
22 cr 9480 . . . . 5  class  RR
23 clt 9617 . . . . . 6  class  <
2423ccnv 4991 . . . . 5  class  `'  <
2521, 22, 24csup 7889 . . . 4  class  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  )
264, 12, 25cmpt 4498 . . 3  class  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |->  sup ( { m  e.  NN  |  n  ||  ( ( x ^ m )  -  1 ) } ,  RR ,  `'  <  ) )
272, 3, 26cmpt 4498 . 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 1374 1  wff  odZ 
=  ( 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 setvar class
This definition is referenced by:  odzval  14166
  Copyright terms: Public domain W3C validator