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 ) } , ℝ , < ) )