Definition df-odz 12843

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	|- odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )

Distinct variable group:   m, n, x

Detailed syntax breakdown of Definition df-odz

Step	Hyp	Ref	Expression
1		codz 12841	. 2 class odZ
2		vn	. . 3 setvar n
3		cn 9186	. . 3 class NN
4		vx	. . . 4 setvar x
5	4	cv 1397	. . . . . . 7 class x
6	2	cv 1397	. . . . . . 7 class n
7		cgcd 12585	. . . . . . 7 class gcd
8	5, 6, 7	co 6028	. . . . . 6 class ( x gcd n )
9		c1 8076	. . . . . 6 class 1
10	8, 9	wceq 1398	. . . . 5 wff ( x gcd n ) = 1
11		cz 9522	. . . . 5 class ZZ
12	10, 4, 11	crab 2515	. . . 4 class { x e. ZZ | ( x gcd n ) = 1 }
13		vm	. . . . . . . . . 10 setvar m
14	13	cv 1397	. . . . . . . . 9 class m
15		cexp 10844	. . . . . . . . 9 class ^
16	5, 14, 15	co 6028	. . . . . . . 8 class ( x ^ m )
17		cmin 8393	. . . . . . . 8 class -
18	16, 9, 17	co 6028	. . . . . . 7 class ( ( x ^ m ) - 1 )
19		cdvds 12409	. . . . . . 7 class ||
20	6, 18, 19	wbr 4093	. . . . . 6 wff n || ( ( x ^ m ) - 1 )
21	20, 13, 3	crab 2515	. . . . 5 class { m e. NN | n || ( ( x ^ m ) - 1 ) }
22		cr 8074	. . . . 5 class RR
23		clt 8257	. . . . 5 class <
24	21, 22, 23	cinf 7225	. . . 4 class inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < )
25	4, 12, 24	cmpt 4155	. . 3 class ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) )
26	2, 3, 25	cmpt 4155	. 2 class ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )
27	1, 26	wceq 1398	1 wff odZ = ( n e. NN |-> ( x e. { x e. ZZ | ( x gcd n ) = 1 } |-> inf ( { m e. NN | n || ( ( x ^ m ) - 1 ) } , RR , < ) ) )

This definition is referenced by:  odzval  12875