Metamath Proof Explorer

Definition df-primroots

Description: A r -th primitive root is a root of unity such that the exponent divides r . (Contributed by metakunt, 25-Apr-2025)

Ref Expression
Assertion df-primroots 
|- PrimRoots = ( r e. CMnd , k e. NN0 |-> [_ ( Base ` r ) / b ]_ { a e. b | ( ( k ( .g ` r ) a ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) a ) = ( 0g ` r ) -> k || l ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprimroots 
 |-  PrimRoots
1 vr 
 |-  r
2 ccmn 
 |-  CMnd
3 vk 
 |-  k
4 cn0 
 |-  NN0
5 cbs 
 |-  Base
6 1 cv 
 |-  r
7 6 5 cfv 
 |-  ( Base ` r )
8 vb 
 |-  b
9 va 
 |-  a
10 8 cv 
 |-  b
11 3 cv 
 |-  k
12 cmg 
 |-  .g
13 6 12 cfv 
 |-  ( .g ` r )
14 9 cv 
 |-  a
15 11 14 13 co 
 |-  ( k ( .g ` r ) a )
16 c0g 
 |-  0g
17 6 16 cfv 
 |-  ( 0g ` r )
18 15 17 wceq 
 |-  ( k ( .g ` r ) a ) = ( 0g ` r )
19 vl 
 |-  l
20 19 cv 
 |-  l
21 20 14 13 co 
 |-  ( l ( .g ` r ) a )
22 21 17 wceq 
 |-  ( l ( .g ` r ) a ) = ( 0g ` r )
23 cdvds 
 |-  ||
24 11 20 23 wbr 
 |-  k || l
25 22 24 wi 
 |-  ( ( l ( .g ` r ) a ) = ( 0g ` r ) -> k || l )
26 25 19 4 wral 
 |-  A. l e. NN0 ( ( l ( .g ` r ) a ) = ( 0g ` r ) -> k || l )
27 18 26 wa 
 |-  ( ( k ( .g ` r ) a ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) a ) = ( 0g ` r ) -> k || l ) )
28 27 9 10 crab 
 |-  { a e. b | ( ( k ( .g ` r ) a ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) a ) = ( 0g ` r ) -> k || l ) ) }
29 8 7 28 csb 
 |-  [_ ( Base ` r ) / b ]_ { a e. b | ( ( k ( .g ` r ) a ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) a ) = ( 0g ` r ) -> k || l ) ) }
30 1 3 2 4 29 cmpo 
 |-  ( r e. CMnd , k e. NN0 |-> [_ ( Base ` r ) / b ]_ { a e. b | ( ( k ( .g ` r ) a ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) a ) = ( 0g ` r ) -> k || l ) ) } )
31 0 30 wceq 
 |-  PrimRoots = ( r e. CMnd , k e. NN0 |-> [_ ( Base ` r ) / b ]_ { a e. b | ( ( k ( .g ` r ) a ) = ( 0g ` r ) /\ A. l e. NN0 ( ( l ( .g ` r ) a ) = ( 0g ` r ) -> k || l ) ) } )