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∈ℤ∧AgcdN=1→odℤ⁡N⁡A=supn∈ℕ|N∥An−1ℝ<

Proof

Step Hyp Ref Expression
1 oveq2 ⊢m=N→xgcdm=xgcdN
2 1 eqeq1d ⊢m=N→xgcdm=1↔xgcdN=1
3 2 rabbidv ⊢m=N→x∈ℤ|xgcdm=1=x∈ℤ|xgcdN=1
4 oveq1 ⊢n=x→ngcdN=xgcdN
5 4 eqeq1d ⊢n=x→ngcdN=1↔xgcdN=1
6 5 cbvrabv ⊢n∈ℤ|ngcdN=1=x∈ℤ|xgcdN=1
7 3 6 eqtr4di ⊢m=N→x∈ℤ|xgcdm=1=n∈ℤ|ngcdN=1
8 breq1 ⊢m=N→m∥xn−1↔N∥xn−1
9 8 rabbidv ⊢m=N→n∈ℕ|m∥xn−1=n∈ℕ|N∥xn−1
10 9 infeq1d ⊢m=N→supn∈ℕ|m∥xn−1ℝ<=supn∈ℕ|N∥xn−1ℝ<
11 7 10 mpteq12dv ⊢m=N→x∈x∈ℤ|xgcdm=1⟼supn∈ℕ|m∥xn−1ℝ<=x∈n∈ℤ|ngcdN=1⟼supn∈ℕ|N∥xn−1ℝ<
12 df-odz ⊢odℤ=m∈ℕ⟼x∈x∈ℤ|xgcdm=1⟼supn∈ℕ|m∥xn−1ℝ<
13 zex ⊢ℤ∈V
14 13 mptrabex ⊢x∈n∈ℤ|ngcdN=1⟼supn∈ℕ|N∥xn−1ℝ<∈V
15 11 12 14 fvmpt ⊢N∈ℕ→odℤ⁡N=x∈n∈ℤ|ngcdN=1⟼supn∈ℕ|N∥xn−1ℝ<
16 15 fveq1d ⊢N∈ℕ→odℤ⁡N⁡A=x∈n∈ℤ|ngcdN=1⟼supn∈ℕ|N∥xn−1ℝ<⁡A
17 oveq1 ⊢n=A→ngcdN=AgcdN
18 17 eqeq1d ⊢n=A→ngcdN=1↔AgcdN=1
19 18 elrab ⊢A∈n∈ℤ|ngcdN=1↔A∈ℤ∧AgcdN=1
20 oveq1 ⊢x=A→xn=An
21 20 oveq1d ⊢x=A→xn−1=An−1
22 21 breq2d ⊢x=A→N∥xn−1↔N∥An−1
23 22 rabbidv ⊢x=A→n∈ℕ|N∥xn−1=n∈ℕ|N∥An−1
24 23 infeq1d ⊢x=A→supn∈ℕ|N∥xn−1ℝ<=supn∈ℕ|N∥An−1ℝ<
25 eqid ⊢x∈n∈ℤ|ngcdN=1⟼supn∈ℕ|N∥xn−1ℝ<=x∈n∈ℤ|ngcdN=1⟼supn∈ℕ|N∥xn−1ℝ<
26 ltso ⊢<Orℝ
27 26 infex ⊢supn∈ℕ|N∥An−1ℝ<∈V
28 24 25 27 fvmpt ⊢A∈n∈ℤ|ngcdN=1→x∈n∈ℤ|ngcdN=1⟼supn∈ℕ|N∥xn−1ℝ<⁡A=supn∈ℕ|N∥An−1ℝ<
29 19 28 sylbir ⊢A∈ℤ∧AgcdN=1→x∈n∈ℤ|ngcdN=1⟼supn∈ℕ|N∥xn−1ℝ<⁡A=supn∈ℕ|N∥An−1ℝ<
30 16 29 sylan9eq ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→odℤ⁡N⁡A=supn∈ℕ|N∥An−1ℝ<
31 30 3impb ⊢N∈ℕ∧A∈ℤ∧AgcdN=1→odℤ⁡N⁡A=supn∈ℕ|N∥An−1ℝ<