Definition df-odz

Description: Define the order function on the class of integers mod N. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by AV, 26-Sep-2020)

	Ref	Expression
Assertion	df-odz	⊢ odℤ = ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 } ↦ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		codz	⊢ odℤ
1		vn	⊢ 𝑛
2		cn	⊢ ℕ
3		vx	⊢ 𝑥
4		cz	⊢ ℤ
5	3	cv	⊢ 𝑥
6		cgcd	⊢ gcd
7	1	cv	⊢ 𝑛
8	5 7 6	co	⊢ ( 𝑥 gcd 𝑛 )
9		c1	⊢ 1
10	8 9	wceq	⊢ ( 𝑥 gcd 𝑛 ) = 1
11	10 3 4	crab	⊢ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 }
12		vm	⊢ 𝑚
13		cdvds	⊢ ∥
14		cexp	⊢ ↑
15	12	cv	⊢ 𝑚
16	5 15 14	co	⊢ ( 𝑥 ↑ 𝑚 )
17		cmin	⊢ −
18	16 9 17	co	⊢ ( ( 𝑥 ↑ 𝑚 ) − 1 )
19	7 18 13	wbr	⊢ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 )
20	19 12 2	crab	⊢ { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) }
21		cr	⊢ ℝ
22		clt	⊢ <
23	20 21 22	cinf	⊢ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < )
24	3 11 23	cmpt	⊢ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 } ↦ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < ) )
25	1 2 24	cmpt	⊢ ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 } ↦ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < ) ) )
26	0 25	wceq	⊢ odℤ = ( 𝑛 ∈ ℕ ↦ ( 𝑥 ∈ { 𝑥 ∈ ℤ ∣ ( 𝑥 gcd 𝑛 ) = 1 } ↦ inf ( { 𝑚 ∈ ℕ ∣ 𝑛 ∥ ( ( 𝑥 ↑ 𝑚 ) − 1 ) } , ℝ , < ) ) )