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 ∈ CMnd , k ∈ ℕ 0 ⟼ ⦋ Base r / b⦌ a ∈ b | k ⋅ r a = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r a = 0 r → k ∥ l

Detailed syntax breakdown

Step Hyp Ref Expression
0 cprimroots class PrimRoots
1 vr setvar r
2 ccmn class CMnd
3 vk setvar k
4 cn0 class ℕ 0
5 cbs class Base
6 1 cv setvar r
7 6 5 cfv class Base r
8 vb setvar b
9 va setvar a
10 8 cv setvar b
11 3 cv setvar k
12 cmg class ⋅ 𝑔
13 6 12 cfv class ⋅ r
14 9 cv setvar a
15 11 14 13 co class k ⋅ r a
16 c0g class 0 𝑔
17 6 16 cfv class 0 r
18 15 17 wceq wff k ⋅ r a = 0 r
19 vl setvar l
20 19 cv setvar l
21 20 14 13 co class l ⋅ r a
22 21 17 wceq wff l ⋅ r a = 0 r
23 cdvds class ∥
24 11 20 23 wbr wff k ∥ l
25 22 24 wi wff l ⋅ r a = 0 r → k ∥ l
26 25 19 4 wral wff ∀ l ∈ ℕ 0 l ⋅ r a = 0 r → k ∥ l
27 18 26 wa wff k ⋅ r a = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r a = 0 r → k ∥ l
28 27 9 10 crab class a ∈ b | k ⋅ r a = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r a = 0 r → k ∥ l
29 8 7 28 csb class ⦋ Base r / b⦌ a ∈ b | k ⋅ r a = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r a = 0 r → k ∥ l
30 1 3 2 4 29 cmpo class r ∈ CMnd , k ∈ ℕ 0 ⟼ ⦋ Base r / b⦌ a ∈ b | k ⋅ r a = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r a = 0 r → k ∥ l
31 0 30 wceq wff PrimRoots = r ∈ CMnd , k ∈ ℕ 0 ⟼ ⦋ Base r / b⦌ a ∈ b | k ⋅ r a = 0 r ∧ ∀ l ∈ ℕ 0 l ⋅ r a = 0 r → k ∥ l