Theorem isprimroot2

Description: Alternative way of creating primitive roots. (Contributed by metakunt, 14-Jul-2025)

	Ref	Expression
Hypotheses	isprimroot2.1	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
	isprimroot2.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	isprimroot2.3	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ 𝑅 ) )
	isprimroot2.4	⊢ ( 𝜑 → ( ( od ‘ 𝑅 ) ‘ 𝑀 ) = 𝐾 )
Assertion	isprimroot2	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		isprimroot2.1	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
2		isprimroot2.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3		isprimroot2.3	⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ 𝑅 ) )
4		isprimroot2.4	⊢ ( 𝜑 → ( ( od ‘ 𝑅 ) ‘ 𝑀 ) = 𝐾 )
5	4	eqcomd	⊢ ( 𝜑 → 𝐾 = ( ( od ‘ 𝑅 ) ‘ 𝑀 ) )
6	5	oveq1d	⊢ ( 𝜑 → ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( ( ( od ‘ 𝑅 ) ‘ 𝑀 ) ( .g ‘ 𝑅 ) 𝑀 ) )
7		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
8		eqid	⊢ ( od ‘ 𝑅 ) = ( od ‘ 𝑅 )
9		eqid	⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
10		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
11	7 8 9 10	odid	⊢ ( 𝑀 ∈ ( Base ‘ 𝑅 ) → ( ( ( od ‘ 𝑅 ) ‘ 𝑀 ) ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) )
12	3 11	syl	⊢ ( 𝜑 → ( ( ( od ‘ 𝑅 ) ‘ 𝑀 ) ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) )
13	6 12	eqtrd	⊢ ( 𝜑 → ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) )
14	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) ∧ ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → ( ( od ‘ 𝑅 ) ‘ 𝑀 ) = 𝐾 )
15	14	eqcomd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) ∧ ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → 𝐾 = ( ( od ‘ 𝑅 ) ‘ 𝑀 ) )
16	1	cmnmndd	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) → 𝑅 ∈ Mnd )
18	3	adantr	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) → 𝑀 ∈ ( Base ‘ 𝑅 ) )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) → 𝑙 ∈ ℕ0 )
20	7 8 9 10	oddvdsnn0	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ 𝑙 ∈ ℕ0 ) → ( ( ( od ‘ 𝑅 ) ‘ 𝑀 ) ∥ 𝑙 ↔ ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) )
21	17 18 19 20	syl3anc	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) → ( ( ( od ‘ 𝑅 ) ‘ 𝑀 ) ∥ 𝑙 ↔ ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) )
22	21	bicomd	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ↔ ( ( od ‘ 𝑅 ) ‘ 𝑀 ) ∥ 𝑙 ) )
23	22	biimpd	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → ( ( od ‘ 𝑅 ) ‘ 𝑀 ) ∥ 𝑙 ) )
24	23	imp	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) ∧ ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → ( ( od ‘ 𝑅 ) ‘ 𝑀 ) ∥ 𝑙 )
25	15 24	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) ∧ ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → 𝐾 ∥ 𝑙 )
26	25	ex	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℕ0 ) → ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) )
27	26	ralrimiva	⊢ ( 𝜑 → ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) )
28	3 13 27	3jca	⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
29	2	nnnn0d	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
30	1 29 9	isprimroot	⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
31	28 30	mpbird	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )