This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) = inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑚 = 𝑁 → ( 𝑥 gcd 𝑚 ) = ( 𝑥 gcd 𝑁 ) )
2 1 eqeq1d ⊢ ( 𝑚 = 𝑁 → ( ( 𝑥 gcd 𝑚 ) = 1 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
3 2 rabbidv ⊢ ( 𝑚 = 𝑁 → { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑚 ) = 1 } = { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑁 ) = 1 } )
4 oveq1 ⊢ ( 𝑛 = 𝑥 → ( 𝑛 gcd 𝑁 ) = ( 𝑥 gcd 𝑁 ) )
5 4 eqeq1d ⊢ ( 𝑛 = 𝑥 → ( ( 𝑛 gcd 𝑁 ) = 1 ↔ ( 𝑥 gcd 𝑁 ) = 1 ) )
6 5 cbvrabv ⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } = { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑁 ) = 1 }
7 3 6 eqtr4di ⊢ ( 𝑚 = 𝑁 → { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑚 ) = 1 } = { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } )
8 breq1 ⊢ ( 𝑚 = 𝑁 → ( 𝑚 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) ↔ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) ) )
9 8 rabbidv ⊢ ( 𝑚 = 𝑁 → { 𝑛 ∈ ℕ ∣ 𝑚 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } = { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } )
10 9 infeq1d ⊢ ( 𝑚 = 𝑁 → inf ( { 𝑛 ∈ ℕ ∣ 𝑚 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )
11 7 10 mpteq12dv ⊢ ( 𝑚 = 𝑁 → ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑚 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑚 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) = ( 𝑥 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) )
12 df-odz ⊢ odℤ = ( 𝑚 ∈ ℕ ↦ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑚 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑚 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) )
13 zex ⊢ ℤ ∈ V
14 13 mptrabex ⊢ ( 𝑥 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) ∈ V
15 11 12 14 fvmpt ⊢ ( 𝑁 ∈ ℕ → ( odℤ ‘ 𝑁 ) = ( 𝑥 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) )
16 15 fveq1d ⊢ ( 𝑁 ∈ ℕ → ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) = ( ( 𝑥 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) ‘ 𝐴 ) )
17 oveq1 ⊢ ( 𝑛 = 𝐴 → ( 𝑛 gcd 𝑁 ) = ( 𝐴 gcd 𝑁 ) )
18 17 eqeq1d ⊢ ( 𝑛 = 𝐴 → ( ( 𝑛 gcd 𝑁 ) = 1 ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
19 18 elrab ⊢ ( 𝐴 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↔ ( 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) )
20 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ↑ 𝑛 ) = ( 𝐴 ↑ 𝑛 ) )
21 20 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ↑ 𝑛 ) − 1 ) = ( ( 𝐴 ↑ 𝑛 ) − 1 ) )
22 21 breq2d ⊢ ( 𝑥 = 𝐴 → ( 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) ↔ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) ) )
23 22 rabbidv ⊢ ( 𝑥 = 𝐴 → { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } = { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } )
24 23 infeq1d ⊢ ( 𝑥 = 𝐴 → inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )
25 eqid ⊢ ( 𝑥 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) = ( 𝑥 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )
26 ltso ⊢ < Or ℝ
27 26 infex ⊢ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ∈ V
28 24 25 27 fvmpt ⊢ ( 𝐴 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } → ( ( 𝑥 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) ‘ 𝐴 ) = inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )
29 19 28 sylbir ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝑥 ∈ { 𝑛 ∈ ℤ ∣ ( 𝑛 gcd 𝑁 ) = 1 } ↦ inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝑥 ↑ 𝑛 ) − 1 ) } , ℝ , < ) ) ‘ 𝐴 ) = inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )
30 16 29 sylan9eq ⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) ) → ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) = inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )
31 30 3impb ⊢ ( ( 𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( odℤ ‘ 𝑁 ) ‘ 𝐴 ) = inf ( { 𝑛 ∈ ℕ ∣ 𝑁 ∥ ( ( 𝐴 ↑ 𝑛 ) − 1 ) } , ℝ , < ) )