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 ∈ ℕ ∧ A ∈ ℤ ∧ A gcd N = 1 → odℤ ⁡ N ⁡ A = inf n ∈ ℕ | N ∥ A n − 1 ℝ <

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 ∈ ℤ | x gcd m = 1 = x ∈ ℤ | 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 ∈ ℤ | n gcd N = 1 = x ∈ ℤ | x gcd N = 1
7 3 6 eqtr4di ⊢ m = N → x ∈ ℤ | x gcd m = 1 = n ∈ ℤ | n gcd N = 1
8 breq1 ⊢ m = N → m ∥ x n − 1 ↔ N ∥ x n − 1
9 8 rabbidv ⊢ m = N → n ∈ ℕ | m ∥ x n − 1 = n ∈ ℕ | N ∥ x n − 1
10 9 infeq1d ⊢ m = N → inf n ∈ ℕ | m ∥ x n − 1 ℝ < = inf n ∈ ℕ | N ∥ x n − 1 ℝ <
11 7 10 mpteq12dv ⊢ m = N → x ∈ x ∈ ℤ | x gcd m = 1 ⟼ inf n ∈ ℕ | m ∥ x n − 1 ℝ < = x ∈ n ∈ ℤ | n gcd N = 1 ⟼ inf n ∈ ℕ | N ∥ x n − 1 ℝ <
12 df-odz ⊢ odℤ = m ∈ ℕ ⟼ x ∈ x ∈ ℤ | x gcd m = 1 ⟼ inf n ∈ ℕ | m ∥ x n − 1 ℝ <
13 zex ⊢ ℤ ∈ V
14 13 mptrabex ⊢ x ∈ n ∈ ℤ | n gcd N = 1 ⟼ inf n ∈ ℕ | N ∥ x n − 1 ℝ < ∈ V
15 11 12 14 fvmpt ⊢ N ∈ ℕ → odℤ ⁡ N = x ∈ n ∈ ℤ | n gcd N = 1 ⟼ inf n ∈ ℕ | N ∥ x n − 1 ℝ <
16 15 fveq1d ⊢ N ∈ ℕ → odℤ ⁡ N ⁡ A = x ∈ n ∈ ℤ | n gcd N = 1 ⟼ inf n ∈ ℕ | N ∥ x n − 1 ℝ < ⁡ 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 ∈ n ∈ ℤ | n gcd N = 1 ↔ A ∈ ℤ ∧ 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 ∈ ℕ | N ∥ x n − 1 = n ∈ ℕ | N ∥ A n − 1
24 23 infeq1d ⊢ x = A → inf n ∈ ℕ | N ∥ x n − 1 ℝ < = inf n ∈ ℕ | N ∥ A n − 1 ℝ <
25 eqid ⊢ x ∈ n ∈ ℤ | n gcd N = 1 ⟼ inf n ∈ ℕ | N ∥ x n − 1 ℝ < = x ∈ n ∈ ℤ | n gcd N = 1 ⟼ inf n ∈ ℕ | N ∥ x n − 1 ℝ <
26 ltso ⊢ < Or ℝ
27 26 infex ⊢ inf n ∈ ℕ | N ∥ A n − 1 ℝ < ∈ V
28 24 25 27 fvmpt ⊢ A ∈ n ∈ ℤ | n gcd N = 1 → x ∈ n ∈ ℤ | n gcd N = 1 ⟼ inf n ∈ ℕ | N ∥ x n − 1 ℝ < ⁡ A = inf n ∈ ℕ | N ∥ A n − 1 ℝ <
29 19 28 sylbir ⊢ A ∈ ℤ ∧ A gcd N = 1 → x ∈ n ∈ ℤ | n gcd N = 1 ⟼ inf n ∈ ℕ | N ∥ x n − 1 ℝ < ⁡ A = inf n ∈ ℕ | N ∥ A n − 1 ℝ <
30 16 29 sylan9eq ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ A gcd N = 1 → odℤ ⁡ N ⁡ A = inf n ∈ ℕ | N ∥ A n − 1 ℝ <
31 30 3impb ⊢ N ∈ ℕ ∧ A ∈ ℤ ∧ A gcd N = 1 → odℤ ⁡ N ⁡ A = inf n ∈ ℕ | N ∥ A n − 1 ℝ <