MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-odz Structured version   Visualization version   GIF version

Definition df-odz 16734
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
StepHypRef Expression
1 codz 16732 . 2 class od
2 vn . . 3 setvar 𝑛
3 cn 12243 . . 3 class
4 vx . . . 4 setvar 𝑥
54cv 1533 . . . . . . 7 class 𝑥
62cv 1533 . . . . . . 7 class 𝑛
7 cgcd 16469 . . . . . . 7 class gcd
85, 6, 7co 7420 . . . . . 6 class (𝑥 gcd 𝑛)
9 c1 11140 . . . . . 6 class 1
108, 9wceq 1534 . . . . 5 wff (𝑥 gcd 𝑛) = 1
11 cz 12589 . . . . 5 class
1210, 4, 11crab 3429 . . . 4 class {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1}
13 vm . . . . . . . . . 10 setvar 𝑚
1413cv 1533 . . . . . . . . 9 class 𝑚
15 cexp 14059 . . . . . . . . 9 class
165, 14, 15co 7420 . . . . . . . 8 class (𝑥𝑚)
17 cmin 11475 . . . . . . . 8 class
1816, 9, 17co 7420 . . . . . . 7 class ((𝑥𝑚) − 1)
19 cdvds 16231 . . . . . . 7 class
206, 18, 19wbr 5148 . . . . . 6 wff 𝑛 ∥ ((𝑥𝑚) − 1)
2120, 13, 3crab 3429 . . . . 5 class {𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥𝑚) − 1)}
22 cr 11138 . . . . 5 class
23 clt 11279 . . . . 5 class <
2421, 22, 23cinf 9465 . . . 4 class inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥𝑚) − 1)}, ℝ, < )
254, 12, 24cmpt 5231 . . 3 class (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥𝑚) − 1)}, ℝ, < ))
262, 3, 25cmpt 5231 . 2 class (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥𝑚) − 1)}, ℝ, < )))
271, 26wceq 1534 1 wff od = (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥𝑚) − 1)}, ℝ, < )))
Colors of variables: wff setvar class
This definition is referenced by:  odzval  16760
  Copyright terms: Public domain W3C validator