Theorem isprimroot 42532

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 42531	. . . . . 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 771	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → 𝑟 = 𝑅)
4	3	fveq2d 6844	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → (Base‘𝑟) = (Base‘𝑅))
5		simplrl 777	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑟 = 𝑅)
6	5	fveq2d 6844	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (.g‘𝑟) = (.g‘𝑅))
7		simplrr 778	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑘 = 𝐾)
8		eqidd 2737	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → 𝑥 = 𝑥)
9	6, 7, 8	oveq123d 7388	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑘(.g‘𝑟)𝑥) = (𝐾(.g‘𝑅)𝑥))
10	5	fveq2d 6844	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (0g‘𝑟) = (0g‘𝑅))
11	9, 10	eqeq12d 2752	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ↔ (𝐾(.g‘𝑅)𝑥) = (0g‘𝑅)))
12	3	fveq2d 6844	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → (.g‘𝑟) = (.g‘𝑅))
13	12	oveqdr 7395	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑙(.g‘𝑟)𝑥) = (𝑙(.g‘𝑅)𝑥))
14	13, 10	eqeq12d 2752	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) ↔ (𝑙(.g‘𝑅)𝑥) = (0g‘𝑅)))
15	7	breq1d 5095	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (𝑘 ∥ 𝑙 ↔ 𝐾 ∥ 𝑙))
16	14, 15	imbi12d 344	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
17	16	ralbidv 3160	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
18	11, 17	anbi12d 633	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) ∧ 𝑥 ∈ 𝑏) → (((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙)) ↔ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
19	18	rabbidva 3395	. . . . . 6 ⊢ ((𝜑 ∧ (𝑟 = 𝑅 ∧ 𝑘 = 𝐾)) → {𝑥 ∈ 𝑏 ∣ ((𝑘(.g‘𝑟)𝑥) = (0g‘𝑟) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑟)𝑥) = (0g‘𝑟) → 𝑘 ∥ 𝑙))} = {𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
20	4, 19	csbeq12dv 3846	. . . . 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 2736	. . . . . . 7 ⊢ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))}
24		fvexd 6855	. . . . . . 7 ⊢ (𝜑 → (Base‘𝑅) ∈ V)
25	23, 24	rabexd 5281	. . . . . 6 ⊢ (𝜑 → {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V)
26		simpr 484	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑏 = (Base‘𝑅)) → 𝑏 = (Base‘𝑅))
27	26	rabeqdv 3404	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑏 = (Base‘𝑅)) → {𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
28	24, 27	csbied 3873	. . . . . . 7 ⊢ (𝜑 → ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
29	28	eleq1d 2821	. . . . . 6 ⊢ (𝜑 → (⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V ↔ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V))
30	25, 29	mpbird 257	. . . . 5 ⊢ (𝜑 → ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ∈ V)
31	2, 20, 21, 22, 30	ovmpod 7519	. . . 4 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = ⦋(Base‘𝑅) / 𝑏⦌{𝑥 ∈ 𝑏 ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
32	31, 28	eqtrd 2771	. . 3 ⊢ (𝜑 → (𝑅 PrimRoots 𝐾) = {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))})
33	32	eleq2d 2822	. 2 ⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ 𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))}))
34		oveq2 7375	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (𝐾(.g‘𝑅)𝑥) = (𝐾(.g‘𝑅)𝑀))
35	34	eqeq1d 2738	. . . . . 6 ⊢ (𝑥 = 𝑀 → ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ↔ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅)))
36		oveq2 7375	. . . . . . . . 9 ⊢ (𝑥 = 𝑀 → (𝑙(.g‘𝑅)𝑥) = (𝑙(.g‘𝑅)𝑀))
37	36	eqeq1d 2738	. . . . . . . 8 ⊢ (𝑥 = 𝑀 → ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) ↔ (𝑙(.g‘𝑅)𝑀) = (0g‘𝑅)))
38	37	imbi1d 341	. . . . . . 7 ⊢ (𝑥 = 𝑀 → (((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
39	38	ralbidv 3160	. . . . . 6 ⊢ (𝑥 = 𝑀 → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
40	35, 39	anbi12d 633	. . . . 5 ⊢ (𝑥 = 𝑀 → (((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
41	40	elrab 3634	. . . 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 1095	. . . . . 6 ⊢ ((𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ (𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
44	43	bicomi 224	. . . . 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 262	. . . . 5 ⊢ (𝜑 → (𝑀 ∈ (Base‘𝑅) ↔ 𝑀 ∈ (Base‘𝑅)))
47		isprimroot.3	. . . . . . . . 9 ⊢ ↑ = (.g‘𝑅)
48	47	eqcomi 2745	. . . . . . . 8 ⊢ (.g‘𝑅) = ↑
49	48	a1i 11	. . . . . . 7 ⊢ (𝜑 → (.g‘𝑅) = ↑ )
50	49	oveqd 7384	. . . . . 6 ⊢ (𝜑 → (𝐾(.g‘𝑅)𝑀) = (𝐾 ↑ 𝑀))
51	50	eqeq1d 2738	. . . . 5 ⊢ (𝜑 → ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ↔ (𝐾 ↑ 𝑀) = (0g‘𝑅)))
52	49	oveqd 7384	. . . . . . . 8 ⊢ (𝜑 → (𝑙(.g‘𝑅)𝑀) = (𝑙 ↑ 𝑀))
53	52	eqeq1d 2738	. . . . . . 7 ⊢ (𝜑 → ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) ↔ (𝑙 ↑ 𝑀) = (0g‘𝑅)))
54	53	imbi1d 341	. . . . . 6 ⊢ (𝜑 → (((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
55	54	ralbidv 3160	. . . . 5 ⊢ (𝜑 → (∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙) ↔ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)))
56	46, 51, 55	3anbi123d 1439	. . . 4 ⊢ (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ (𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙)) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
57	45, 56	bitrd 279	. . 3 ⊢ (𝜑 → ((𝑀 ∈ (Base‘𝑅) ∧ ((𝐾(.g‘𝑅)𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
58	42, 57	bitrd 279	. 2 ⊢ (𝜑 → (𝑀 ∈ {𝑥 ∈ (Base‘𝑅) ∣ ((𝐾(.g‘𝑅)𝑥) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘𝑅)𝑥) = (0g‘𝑅) → 𝐾 ∥ 𝑙))} ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))
59	33, 58	bitrd 279	1 ⊢ (𝜑 → (𝑀 ∈ (𝑅 PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘𝑅) ∧ (𝐾 ↑ 𝑀) = (0g‘𝑅) ∧ ∀𝑙 ∈ ℕ0 ((𝑙 ↑ 𝑀) = (0g‘𝑅) → 𝐾 ∥ 𝑙))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3051  {crab 3389  Vcvv 3429  ⦋csb 3837   class class class wbr 5085  ‘cfv 6498  (class class class)co 7367   ∈ cmpo 7369  ℕ₀cn0 12437   ∥ cdvds 16221  Basecbs 17179  0_gc0g 17402  ._gcmg 19043  CMndccmn 19755   PrimRoots cprimroots 42530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-primroots 42531

This theorem is referenced by:  isprimroot2  42533  primrootsunit1  42536  primrootscoprmpow  42538  primrootscoprbij  42541  primrootlekpowne0  42544  primrootspoweq0  42545  aks6d1c1p2  42548  aks6d1c1p3  42549  aks6d1c1p4  42550  aks6d1c1p5  42551  aks6d1c1p7  42552  aks6d1c1p6  42553  aks6d1c1p8  42554  aks6d1c2lem3  42565  aks6d1c2lem4  42566  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6lem5  42616  aks5lem2  42626  aks5lem3a  42628