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	$$⊢{\mathrm{od}}_{\mathbb{Z}}=\left(n\in \mathbb{N}⟼\left(x\in \left\{x\in \mathbb{Z}|x\gcd n=1\right\}⟼sup\left(\left\{m\in \mathbb{N}|n\parallel \left(x^m-1\right)\right\},ℝ,<\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		codz	$$class{\mathrm{od}}_{\mathbb{Z}}$$
1		vn	$$setvarn$$
2		cn	$$class\mathbb{N}$$
3		vx	$$setvarx$$
4		cz	$$class\mathbb{Z}$$
5	3	cv	$$setvarx$$
6		cgcd	$$class\gcd$$
7	1	cv	$$setvarn$$
8	5 7 6	co	$$class\left(x\gcd n\right)$$
9		c1	$$class1$$
10	8 9	wceq	$$wffx\gcd n=1$$
11	10 3 4	crab	$$class\left\{x\in \mathbb{Z}|x\gcd n=1\right\}$$
12		vm	$$setvarm$$
13		cdvds	$$class\parallel$$
14		cexp	$$class^$$
15	12	cv	$$setvarm$$
16	5 15 14	co	$$class{x}^m$$
17		cmin	$$class-$$
18	16 9 17	co	$$class\left(x^m-1\right)$$
19	7 18 13	wbr	$$wffn\parallel \left(x^m-1\right)$$
20	19 12 2	crab	$$class\left\{m\in \mathbb{N}|n\parallel \left(x^m-1\right)\right\}$$
21		cr	$$classℝ$$
22		clt	$$class<$$
23	20 21 22	cinf	$$classsup\left(\left\{m\in \mathbb{N}|n\parallel \left(x^m-1\right)\right\},ℝ,<\right)$$
24	3 11 23	cmpt	$$class\left(x\in \left\{x\in \mathbb{Z}|x\gcd n=1\right\}⟼sup\left(\left\{m\in \mathbb{N}|n\parallel \left(x^m-1\right)\right\},ℝ,<\right)\right)$$
25	1 2 24	cmpt	$$class\left(n\in \mathbb{N}⟼\left(x\in \left\{x\in \mathbb{Z}|x\gcd n=1\right\}⟼sup\left(\left\{m\in \mathbb{N}|n\parallel \left(x^m-1\right)\right\},ℝ,<\right)\right)\right)$$
26	0 25	wceq	$$wff{\mathrm{od}}_{\mathbb{Z}}=\left(n\in \mathbb{N}⟼\left(x\in \left\{x\in \mathbb{Z}|x\gcd n=1\right\}⟼sup\left(\left\{m\in \mathbb{N}|n\parallel \left(x^m-1\right)\right\},ℝ,<\right)\right)\right)$$