Definition df-primroots 41595

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

Assertion

Ref	Expression
df-primroots	⊢ PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0 ↦ ⦋(Base‘𝑟) / 𝑏⦌{𝑎 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑎) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙))})

Distinct variable group:   𝑎,𝑏,𝑘,𝑙,𝑟

Detailed syntax breakdown of Definition df-primroots

Step	Hyp	Ref	Expression
1		cprimroots 41594	. 2 class PrimRoots
2		vr	. . 3 setvar 𝑟
3		vk	. . 3 setvar 𝑘
4		ccmn 19742	. . 3 class CMnd
5		cn0 12510	. . 3 class ℕ0
6		vb	. . . 4 setvar 𝑏
7	2	cv 1532	. . . . 5 class 𝑟
8		cbs 17187	. . . . 5 class Base
9	7, 8	cfv 6553	. . . 4 class (Base‘𝑟)
10	3	cv 1532	. . . . . . . 8 class 𝑘
11		va	. . . . . . . . 9 setvar 𝑎
12	11	cv 1532	. . . . . . . 8 class 𝑎
13		cmg 19030	. . . . . . . . 9 class .g
14	7, 13	cfv 6553	. . . . . . . 8 class (.g‘𝑟)
15	10, 12, 14	co 7426	. . . . . . 7 class (𝑘(.g‘𝑟)𝑎)
16		c0g 17428	. . . . . . . 8 class 0g
17	7, 16	cfv 6553	. . . . . . 7 class (0g‘𝑟)
18	15, 17	wceq 1533	. . . . . 6 wff (𝑘(.g‘𝑟)𝑎) = (0g‘𝑟)
19		vl	. . . . . . . . . . 11 setvar 𝑙
20	19	cv 1532	. . . . . . . . . 10 class 𝑙
21	20, 12, 14	co 7426	. . . . . . . . 9 class (𝑙(.g‘𝑟)𝑎)
22	21, 17	wceq 1533	. . . . . . . 8 wff (𝑙(.g‘𝑟)𝑎) = (0g‘𝑟)
23		cdvds 16238	. . . . . . . . 9 class ∥
24	10, 20, 23	wbr 5152	. . . . . . . 8 wff 𝑘 ∥ 𝑙
25	22, 24	wi 4	. . . . . . 7 wff ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙)
26	25, 19, 5	wral 3058	. . . . . 6 wff ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙)
27	18, 26	wa 394	. . . . 5 wff ((𝑘(.g‘𝑟)𝑎) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙))
28	6	cv 1532	. . . . 5 class 𝑏
29	27, 11, 28	crab 3430	. . . 4 class {𝑎 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑎) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙))}
30	6, 9, 29	csb 3894	. . 3 class ⦋(Base‘𝑟) / 𝑏⦌{𝑎 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑎) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙))}
31	2, 3, 4, 5, 30	cmpo 7428	. 2 class (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0 ↦ ⦋(Base‘𝑟) / 𝑏⦌{𝑎 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑎) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙))})
32	1, 31	wceq 1533	1 wff PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0 ↦ ⦋(Base‘𝑟) / 𝑏⦌{𝑎 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑎) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑎) = (0g‘𝑟) → 𝑘 ∥ 𝑙))})

This definition is referenced by:  isprimroot  41596