Metamath Proof Explorer

Definition df-odz

Description: Define the order function on the class of integers mod N. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by AV, 26-Sep-2020)

Ref Expression
Assertion df-odz 
|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 codz 
 |-  odZ
1 vn 
 |-  n
2 cn 
 |-  NN
3 vx 
 |-  x
4 cz 
 |-  ZZ
5 3 cv 
 |-  x
6 cgcd 
 |-  gcd
7 1 cv 
 |-  n
8 5 7 6 co 
 |-  ( x gcd n )
9 c1 
 |-  1
10 8 9 wceq 
 |-  ( x gcd n ) = 1
11 10 3 4 crab 
 |-  { x e. ZZ | ( x gcd n ) = 1 }
12 vm 
 |-  m
13 cdvds 
 |-  ||
14 cexp 
 |-  ^
15 12 cv 
 |-  m
16 5 15 14 co 
 |-  ( x ^ m )
17 cmin 
 |-  -
18 16 9 17 co 
 |-  ( ( x ^ m ) - 1 )
19 7 18 13 wbr 
 |-  n || ( ( x ^ m ) - 1 )
20 19 12 2 crab 
 |-  { m e. NN | n || ( ( x ^ m ) - 1 ) }
21 cr 
 |-  RR
22 clt 
 |-  <
23 20 21 22 cinf 
 |-  inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < )
24 3 11 23 cmpt 
 |-  ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) )
25 1 2 24 cmpt 
 |-  ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
26 0 25 wceq 
 |-  odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )