Metamath Proof Explorer

Definition df-odz

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)

Ref Expression
Assertion df-odz ⊢ odℤ = n ∈ ℕ ⟼ x ∈ x ∈ ℤ | x gcd n = 1 ⟼ sup m ∈ ℕ | n ∥ x m − 1 ℝ <

Detailed syntax breakdown

Step Hyp Ref Expression
0 codz class odℤ
1 vn setvar n
2 cn class ℕ
3 vx setvar x
4 cz class ℤ
5 3 cv setvar x
6 cgcd class gcd
7 1 cv setvar n
8 5 7 6 co class x gcd n
9 c1 class 1
10 8 9 wceq wff x gcd n = 1
11 10 3 4 crab class x ∈ ℤ | x gcd n = 1
12 vm setvar m
13 cdvds class ∥
14 cexp class ^
15 12 cv setvar m
16 5 15 14 co class x m
17 cmin class −
18 16 9 17 co class x m − 1
19 7 18 13 wbr wff n ∥ x m − 1
20 19 12 2 crab class m ∈ ℕ | n ∥ x m − 1
21 cr class ℝ
22 clt class <
23 20 21 22 cinf class sup m ∈ ℕ | n ∥ x m − 1 ℝ <
24 3 11 23 cmpt class x ∈ x ∈ ℤ | x gcd n = 1 ⟼ sup m ∈ ℕ | n ∥ x m − 1 ℝ <
25 1 2 24 cmpt class n ∈ ℕ ⟼ x ∈ x ∈ ℤ | x gcd n = 1 ⟼ sup m ∈ ℕ | n ∥ x m − 1 ℝ <
26 0 25 wceq wff odℤ = n ∈ ℕ ⟼ x ∈ x ∈ ℤ | x gcd n = 1 ⟼ sup m ∈ ℕ | n ∥ x m − 1 ℝ <