Theorem isprimroot 42901

Description: The value of a primitive root. (Contributed by metakunt, 25-Apr-2025.)

Hypotheses

Ref	Expression
isprimroot.1	⊢ (𝜑 → 𝑅 ∈ CMnd)
isprimroot.2	⊢ (𝜑 → 𝐾 ∈ ℕ0)
isprimroot.3	⊢ ↑ = (.g‘𝑅)

Assertion

Ref	Expression
isprimroot	⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))

Distinct variable groups:   𝐾,𝑙   𝑀,𝑙   𝑅,𝑙   𝜑,𝑙

Allowed substitution hint:   ↑ (𝑙)

Proof of Theorem isprimroot

Dummy variables 𝑏 𝑘 𝑟 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-primroots 42900	. . . . . 6 ⊢ PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0 ↦ ⦋(Base‘𝑟) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))})
2	1	a1i 11	. . . . 5 ⊢ (𝜑 → PrimRoots = (𝑟 ∈ CMnd, 𝑘 ∈ ℕ0 ↦ ⦋(Base‘𝑟) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))}))
3		simprl 783	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → 𝑟 = 𝑅)
4	3	fveq2d 6892	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → (Base‘𝑟) = (Base‘𝑅))
5		simplrl 789	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑟 = 𝑅)
6	5	fveq2d 6892	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (.g‘𝑟) = (.g‘𝑅))
7		simplrr 790	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑘 = 𝐾)
8		eqidd 2767	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑥 = 𝑥)
9	6, 7, 8	oveq123d 7444	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑘(.g‘𝑟)𝑥) = (𝐾(.g‘𝑅)𝑥))
10	5	fveq2d 6892	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (0g‘𝑟) = (0g‘𝑅))
11	9, 10	eqeq12d 2782	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ↔ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅)))
12	3	fveq2d 6892	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → (.g‘𝑟) = (.g‘𝑅))
13	12	oveqdr 7451	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑙(.g‘𝑟)𝑥) = (𝑙(.g‘𝑅)𝑥))
14	13, 10	eqeq12d 2782	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) ↔ (𝑙(.g‘𝑅)𝑥) = (0g‘𝑅)))
15	7	breq1d 5124	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑘 ∥ 𝑙 ↔ 𝐾 ∥ 𝑙))
16	14, 15	imbi12d 347	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
17	16	ralbidv 3191	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
18	11, 17	anbi12d 644	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙)) ↔ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
19	18	rabbidva 3425	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → {𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))} = {𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
20	4, 19	csbeq12dv 3865	. . . . 5 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → ⦋(Base‘𝑟) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))} = ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
21		isprimroot.1	. . . . 5 ⊢ (𝜑 → 𝑅 ∈ CMnd)
22		isprimroot.2	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ0)
23		eqid 2766	. . . . . . 7 ⊢ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))}
24		fvexd 6903	. . . . . . 7 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
25	23, 24	rabexd 5315	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V)
26		simpr 490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 = (Base‘𝑅)) → 𝑏 = (Base‘𝑅))
27	26	rabeqdv 3434	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 = (Base‘𝑅)) → {𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
28	24, 27	csbied 3892	. . . . . . 7 ⊢ (𝜑 → ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
29	28	eleq1d 2851	. . . . . 6 ⊢ (𝜑 → (⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V ↔ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V))
30	25, 29	mpbird 260	. . . . 5 ⊢ (𝜑 → ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V)
31	2, 20, 21, 22, 30	ovmpod 7575	. . . 4 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
32	31, 28	eqtrd 2801	. . 3 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
33	32	eleq2d 2852	. 2 ⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))}))
34		oveq2 7431	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (𝐾(.g‘𝑅)𝑥) = (𝐾(.g‘𝑅)𝑀))
35	34	eqeq1d 2768	. . . . . 6 ⊢ (𝑥 = 𝑀 → ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ↔ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅)))
36		oveq2 7431	. . . . . . . . 9 ⊢ (𝑥 = 𝑀 → (𝑙(.g‘𝑅)𝑥) = (𝑙(.g‘𝑅)𝑀))
37	36	eqeq1d 2768	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) ↔ (𝑙(.g‘𝑅)𝑀) = (0g‘𝑅)))
38	37	imbi1d 344	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
39	38	ralbidv 3191	. . . . . 6 ⊢ (𝑥 = 𝑀 → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
40	35, 39	anbi12d 644	. . . . 5 ⊢ (𝑥 = 𝑀 → (((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
41	40	elrab 3653	. . . 4 ⊢ (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
42	41	a1i 11	. . 3 ⊢ (𝜑 → (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))))
43		3anass 1111	. . . . . 6 ⊢ ((𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ (𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
44	43	bicomi 227	. . . . 5 ⊢ ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
45	44	a1i 11	. . . 4 ⊢ (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
46		biidd 265	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (Base‘𝑅) ↔ 𝑀 ∈ (Base‘𝑅)))
47		isprimroot.3	. . . . . . . . 9 ⊢ ↑ = (.g‘𝑅)
48	47	eqcomi 2775	. . . . . . . 8 ⊢ (.g‘𝑅) = ↑
49	48	a1i 11	. . . . . . 7 ⊢ (𝜑 → (.g‘𝑅) = ↑ )
50	49	oveqd 7440	. . . . . 6 ⊢ (𝜑 → (𝐾(.g‘𝑅)𝑀) = (𝐾 ↑ 𝑀))
51	50	eqeq1d 2768	. . . . 5 ⊢ (𝜑 → ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ↔ (𝐾 ↑ 𝑀) = (0g‘𝑅)))
52	49	oveqd 7440	. . . . . . . 8 ⊢ (𝜑 → (𝑙(.g‘𝑅)𝑀) = (𝑙 ↑ 𝑀))
53	52	eqeq1d 2768	. . . . . . 7 ⊢ (𝜑 → ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) ↔ (𝑙 ↑ 𝑀) = (0g‘𝑅)))
54	53	imbi1d 344	. . . . . 6 ⊢ (𝜑 → (((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
55	54	ralbidv 3191	. . . . 5 ⊢ (𝜑 → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
56	46, 51, 55	3anbi123d 1464	. . . 4 ⊢ (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
57	45, 56	bitrd 282	. . 3 ⊢ (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
58	42, 57	bitrd 282	. 2 ⊢ (𝜑 → (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
59	33, 58	bitrd 282	1 ⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ∀wral 3082  {crab 3419  Vcvv 3458  ⦋csb 3856   class class class wbr 5114  ‘cfv 6543  (class class class)co 7423   ∈ cmpo 7425  ℕ₀cn0 12522   ∥ cdvds 16335  Basecbs 17294  0_gc0g 17517  ._gcmg 19164  CMndccmn 19881   PrimRoots cprimroots 42899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-primroots 42900

This theorem is used by:  isprimroot2  42902  primrootsunit1  42905  primrootscoprmpow  42907  primrootscoprbij  42910  primrootlekpowne0  42913  primrootspoweq0  42914  aks6d1c1p2  42917  aks6d1c1p3  42918  aks6d1c1p4  42919  aks6d1c1p5  42920  aks6d1c1p7  42921  aks6d1c1p6  42922  aks6d1c1p8  42923  aks6d1c2lem3  42934  aks6d1c2lem4  42935  aks6d1c6lem2  42979  aks6d1c6lem3  42980  aks6d1c6lem4  42981  aks6d1c6isolem1  42982  aks6d1c6isolem2  42983  aks6d1c6lem5  42985  aks5lem2  42995  aks5lem3a  42997