ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-odz Unicode version

Definition df-odz 12153
Description: Define the order function on the class of integers modulo N. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
Assertion
Ref Expression
df-odz  |-  odZ 
=  ( n  e.  NN  |->  ( x  e. 
{ x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |-> inf ( { 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 12151 . 2  class  odZ
2 vn . . 3  setvar  n
3 cn 8867 . . 3  class  NN
4 vx . . . 4  setvar  x
54cv 1347 . . . . . . 7  class  x
62cv 1347 . . . . . . 7  class  n
7 cgcd 11886 . . . . . . 7  class  gcd
85, 6, 7co 5851 . . . . . 6  class  ( x  gcd  n )
9 c1 7764 . . . . . 6  class  1
108, 9wceq 1348 . . . . 5  wff  ( x  gcd  n )  =  1
11 cz 9201 . . . . 5  class  ZZ
1210, 4, 11crab 2452 . . . 4  class  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }
13 vm . . . . . . . . . 10  setvar  m
1413cv 1347 . . . . . . . . 9  class  m
15 cexp 10464 . . . . . . . . 9  class  ^
165, 14, 15co 5851 . . . . . . . 8  class  ( x ^ m )
17 cmin 8079 . . . . . . . 8  class  -
1816, 9, 17co 5851 . . . . . . 7  class  ( ( x ^ m )  -  1 )
19 cdvds 11738 . . . . . . 7  class  ||
206, 18, 19wbr 3987 . . . . . 6  wff  n  ||  ( ( x ^
m )  -  1 )
2120, 13, 3crab 2452 . . . . 5  class  { m  e.  NN  |  n  ||  ( ( x ^
m )  -  1 ) }
22 cr 7762 . . . . 5  class  RR
23 clt 7943 . . . . 5  class  <
2421, 22, 23cinf 6957 . . . 4  class inf ( { m  e.  NN  |  n  ||  ( ( x ^ m )  - 
1 ) } ,  RR ,  <  )
254, 12, 24cmpt 4048 . . 3  class  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |-> inf ( { m  e.  NN  |  n  ||  ( ( x ^ m )  - 
1 ) } ,  RR ,  <  ) )
262, 3, 25cmpt 4048 . 2  class  ( n  e.  NN  |->  ( x  e.  { x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |-> inf ( { m  e.  NN  |  n  ||  ( ( x ^ m )  - 
1 ) } ,  RR ,  <  ) ) )
271, 26wceq 1348 1  wff  odZ 
=  ( n  e.  NN  |->  ( x  e. 
{ x  e.  ZZ  |  ( x  gcd  n )  =  1 }  |-> inf ( { m  e.  NN  |  n  ||  ( ( x ^
m )  -  1 ) } ,  RR ,  <  ) ) )
Colors of variables: wff set class
This definition is referenced by:  odzval  12184
  Copyright terms: Public domain W3C validator