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 = ( 𝑟 ∈ CMnd , 𝑘 ∈ ℕ0 ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑎 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cprimroots	⊢ PrimRoots
1		vr	⊢ 𝑟
2		ccmn	⊢ CMnd
3		vk	⊢ 𝑘
4		cn0	⊢ ℕ0
5		cbs	⊢ Base
6	1	cv	⊢ 𝑟
7	6 5	cfv	⊢ ( Base ‘ 𝑟 )
8		vb	⊢ 𝑏
9		va	⊢ 𝑎
10	8	cv	⊢ 𝑏
11	3	cv	⊢ 𝑘
12		cmg	⊢ .g
13	6 12	cfv	⊢ ( .g ‘ 𝑟 )
14	9	cv	⊢ 𝑎
15	11 14 13	co	⊢ ( 𝑘 ( .g ‘ 𝑟 ) 𝑎 )
16		c0g	⊢ 0g
17	6 16	cfv	⊢ ( 0g ‘ 𝑟 )
18	15 17	wceq	⊢ ( 𝑘 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 )
19		vl	⊢ 𝑙
20	19	cv	⊢ 𝑙
21	20 14 13	co	⊢ ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 )
22	21 17	wceq	⊢ ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 )
23		cdvds	⊢ ∥
24	11 20 23	wbr	⊢ 𝑘 ∥ 𝑙
25	22 24	wi	⊢ ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 )
26	25 19 4	wral	⊢ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 )
27	18 26	wa	⊢ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) )
28	27 9 10	crab	⊢ { 𝑎 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) }
29	8 7 28	csb	⊢ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑎 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) }
30	1 3 2 4 29	cmpo	⊢ ( 𝑟 ∈ CMnd , 𝑘 ∈ ℕ0 ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑎 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) } )
31	0 30	wceq	⊢ PrimRoots = ( 𝑟 ∈ CMnd , 𝑘 ∈ ℕ0 ↦ ⦋ ( Base ‘ 𝑟 ) / 𝑏 ⦌ { 𝑎 ∈ 𝑏 ∣ ( ( 𝑘 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑟 ) 𝑎 ) = ( 0g ‘ 𝑟 ) → 𝑘 ∥ 𝑙 ) ) } )