Definition df-odz 16942

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

Assertion

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

Distinct variable group:   𝑚,𝑛,𝑥

Detailed syntax breakdown of Definition df-odz

Step	Hyp	Ref	Expression
1		codz 16940	. 2 class odℤ
2		vn	. . 3 setvar 𝑛
3		cn 12335	. . 3 class ℕ
4		vx	. . . 4 setvar 𝑥
5	4	cv 1569	. . . . . . 7 class 𝑥
6	2	cv 1569	. . . . . . 7 class 𝑛
7		cgcd 16664	. . . . . . 7 class gcd
8	5, 6, 7	co 7420	. . . . . 6 class (𝑥 gcd 𝑛)
9		c1 11201	. . . . . 6 class 1
10	8, 9	wceq 1570	. . . . 5 wff (𝑥 gcd 𝑛) = 1
11		cz 12693	. . . . 5 class ℤ
12	10, 4, 11	crab 3413	. . . 4 class {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1}
13		vm	. . . . . . . . . 10 setvar 𝑚
14	13	cv 1569	. . . . . . . . 9 class 𝑚
15		cexp 14204	. . . . . . . . 9 class ↑
16	5, 14, 15	co 7420	. . . . . . . 8 class (𝑥↑𝑚)
17		cmin 11541	. . . . . . . 8 class −
18	16, 9, 17	co 7420	. . . . . . 7 class ((𝑥↑𝑚) − 1)
19		cdvds 16422	. . . . . . 7 class ∥
20	6, 18, 19	wbr 5103	. . . . . 6 wff 𝑛 ∥ ((𝑥↑𝑚) − 1)
21	20, 13, 3	crab 3413	. . . . 5 class {𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}
22		cr 11199	. . . . 5 class ℝ
23		clt 11343	. . . . 5 class <
24	21, 22, 23	cinf 9433	. . . 4 class inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, < )
25	4, 12, 24	cmpt 5186	. . 3 class (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, < ))
26	2, 3, 25	cmpt 5186	. 2 class (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, < )))
27	1, 26	wceq 1570	1 wff odℤ = (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, < )))

This definition is used by:  odzval  16969