Metamath Proof Explorer

Theorem odzval

Description: Value of the order function. This is a function of functions; the inner argument selects the base (i.e., mod N for some N , often prime) and the outer argument selects the integer or equivalence class (if you want to think about it that way) from the integers mod N . In order to ensure the supremum is well-defined, we only define the expression when A and N are coprime. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by AV, 26-Sep-2020)

Ref Expression
Assertion odzval 
|- ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( m = N -> ( x gcd m ) = ( x gcd N ) )
2 1 eqeq1d 
 |-  ( m = N -> ( ( x gcd m ) = 1 <-> ( x gcd N ) = 1 ) )
3 2 rabbidv 
 |-  ( m = N -> { x e. ZZ | ( x gcd m ) = 1 } = { x e. ZZ | ( x gcd N ) = 1 } )
4 oveq1 
 |-  ( n = x -> ( n gcd N ) = ( x gcd N ) )
5 4 eqeq1d 
 |-  ( n = x -> ( ( n gcd N ) = 1 <-> ( x gcd N ) = 1 ) )
6 5 cbvrabv 
 |-  { n e. ZZ | ( n gcd N ) = 1 } = { x e. ZZ | ( x gcd N ) = 1 }
7 3 6 eqtr4di 
 |-  ( m = N -> { x e. ZZ | ( x gcd m ) = 1 } = { n e. ZZ | ( n gcd N ) = 1 } )
8 breq1 
 |-  ( m = N -> ( m || ( ( x ^ n ) - 1 ) <-> N || ( ( x ^ n ) - 1 ) ) )
9 8 rabbidv 
 |-  ( m = N -> { n e. NN | m || ( ( x ^ n ) - 1 ) } = { n e. NN | N || ( ( x ^ n ) - 1 ) } )
10 9 infeq1d 
 |-  ( m = N -> inf ( { n e. NN | m || ( ( x ^ n ) - 1 ) } , RR , < ) = inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) )
11 7 10 mpteq12dv 
 |-  ( m = N -> ( x e. { x e. ZZ | ( x gcd m ) = 1 } |-> inf ( { n e. NN | m || ( ( x ^ n ) - 1 ) } , RR , < ) ) = ( x e. { n e. ZZ | ( n gcd N ) = 1 } |-> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) ) )
12 df-odz 
 |-  odZ = ( m e. NN |-> ( x e. { x e. ZZ | ( x gcd m ) = 1 } |-> inf ( { n e. NN | m || ( ( x ^ n ) - 1 ) } , RR , < ) ) )
13 zex 
 |-  ZZ e. _V
14 13 mptrabex 
 |-  ( x e. { n e. ZZ | ( n gcd N ) = 1 } |-> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) ) e. _V
15 11 12 14 fvmpt 
 |-  ( N e. NN -> ( odZ ` N ) = ( x e. { n e. ZZ | ( n gcd N ) = 1 } |-> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) ) )
16 15 fveq1d 
 |-  ( N e. NN -> ( ( odZ ` N ) ` A ) = ( ( x e. { n e. ZZ | ( n gcd N ) = 1 } |-> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) ) ` A ) )
17 oveq1 
 |-  ( n = A -> ( n gcd N ) = ( A gcd N ) )
18 17 eqeq1d 
 |-  ( n = A -> ( ( n gcd N ) = 1 <-> ( A gcd N ) = 1 ) )
19 18 elrab 
 |-  ( A e. { n e. ZZ | ( n gcd N ) = 1 } <-> ( A e. ZZ /\ ( A gcd N ) = 1 ) )
20 oveq1 
 |-  ( x = A -> ( x ^ n ) = ( A ^ n ) )
21 20 oveq1d 
 |-  ( x = A -> ( ( x ^ n ) - 1 ) = ( ( A ^ n ) - 1 ) )
22 21 breq2d 
 |-  ( x = A -> ( N || ( ( x ^ n ) - 1 ) <-> N || ( ( A ^ n ) - 1 ) ) )
23 22 rabbidv 
 |-  ( x = A -> { n e. NN | N || ( ( x ^ n ) - 1 ) } = { n e. NN | N || ( ( A ^ n ) - 1 ) } )
24 23 infeq1d 
 |-  ( x = A -> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )
25 eqid 
 |-  ( x e. { n e. ZZ | ( n gcd N ) = 1 } |-> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) ) = ( x e. { n e. ZZ | ( n gcd N ) = 1 } |-> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) )
26 ltso 
 |-  < Or RR
27 26 infex 
 |-  inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) e. _V
28 24 25 27 fvmpt 
 |-  ( A e. { n e. ZZ | ( n gcd N ) = 1 } -> ( ( x e. { n e. ZZ | ( n gcd N ) = 1 } |-> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )
29 19 28 sylbir 
 |-  ( ( A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( x e. { n e. ZZ | ( n gcd N ) = 1 } |-> inf ( { n e. NN | N || ( ( x ^ n ) - 1 ) } , RR , < ) ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )
30 16 29 sylan9eq 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ ( A gcd N ) = 1 ) ) -> ( ( odZ ` N ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )
31 30 3impb 
 |-  ( ( N e. NN /\ A e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( odZ ` N ) ` A ) = inf ( { n e. NN | N || ( ( A ^ n ) - 1 ) } , RR , < ) )