isprimroot2

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

	Ref	Expression
Hypotheses	isprimroot2.1	$⊢ φ \to R \in CMnd$
	isprimroot2.2	$⊢ φ \to K \in ℕ$
	isprimroot2.3	$⊢ φ \to M \in {Base}_{R}$
	isprimroot2.4	$⊢ φ \to od (R) (M) = K$
Assertion	isprimroot2	$⊢ φ \to M \in (R PrimRoots K)$

Proof

Step	Hyp	Ref	Expression
1		isprimroot2.1	$⊢ φ \to R \in CMnd$
2		isprimroot2.2	$⊢ φ \to K \in ℕ$
3		isprimroot2.3	$⊢ φ \to M \in {Base}_{R}$
4		isprimroot2.4	$⊢ φ \to od (R) (M) = K$
5	4	eqcomd	$⊢ φ \to K = od (R) (M)$
6	5	oveq1d	$⊢ φ \to K \cdot_{R} M = od (R) (M) \cdot_{R} M$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8		eqid	$⊢ od (R) = od (R)$
9		eqid	$⊢ \cdot_{R} = \cdot_{R}$
10		eqid	$⊢ 0_{R} = 0_{R}$
11	7 8 9 10	odid	$⊢ M \in {Base}_{R} \to od (R) (M) \cdot_{R} M = 0_{R}$
12	3 11	syl	$⊢ φ \to od (R) (M) \cdot_{R} M = 0_{R}$
13	6 12	eqtrd	$⊢ φ \to K \cdot_{R} M = 0_{R}$
14	4	ad2antrr	$⊢ ((φ \land l \in ℕ_{0}) \land l \cdot_{R} M = 0_{R}) \to od (R) (M) = K$
15	14	eqcomd	$⊢ ((φ \land l \in ℕ_{0}) \land l \cdot_{R} M = 0_{R}) \to K = od (R) (M)$
16	1	cmnmndd	$⊢ φ \to R \in Mnd$
17	16	adantr	$⊢ (φ \land l \in ℕ_{0}) \to R \in Mnd$
18	3	adantr	$⊢ (φ \land l \in ℕ_{0}) \to M \in {Base}_{R}$
19		simpr	$⊢ (φ \land l \in ℕ_{0}) \to l \in ℕ_{0}$
20	7 8 9 10	oddvdsnn0	$⊢ (R \in Mnd \land M \in {Base}_{R} \land l \in ℕ_{0}) \to (od (R) (M) ∥ l \leftrightarrow l \cdot_{R} M = 0_{R})$
21	17 18 19 20	syl3anc	$⊢ (φ \land l \in ℕ_{0}) \to (od (R) (M) ∥ l \leftrightarrow l \cdot_{R} M = 0_{R})$
22	21	bicomd	$⊢ (φ \land l \in ℕ_{0}) \to (l \cdot_{R} M = 0_{R} \leftrightarrow od (R) (M) ∥ l)$
23	22	biimpd	$⊢ (φ \land l \in ℕ_{0}) \to (l \cdot_{R} M = 0_{R} \to od (R) (M) ∥ l)$
24	23	imp	$⊢ ((φ \land l \in ℕ_{0}) \land l \cdot_{R} M = 0_{R}) \to od (R) (M) ∥ l$
25	15 24	eqbrtrd	$⊢ ((φ \land l \in ℕ_{0}) \land l \cdot_{R} M = 0_{R}) \to K ∥ l$
26	25	ex	$⊢ (φ \land l \in ℕ_{0}) \to (l \cdot_{R} M = 0_{R} \to K ∥ l)$
27	26	ralrimiva	$⊢ φ \to \forall l \in ℕ_{0} (l \cdot_{R} M = 0_{R} \to K ∥ l)$
28	3 13 27	3jca	$⊢ φ \to (M \in {Base}_{R} \land K \cdot_{R} M = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} M = 0_{R} \to K ∥ l))$
29	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
30	1 29 9	isprimroot	$⊢ φ \to (M \in (R PrimRoots K) \leftrightarrow (M \in {Base}_{R} \land K \cdot_{R} M = 0_{R} \land \forall l \in ℕ_{0} (l \cdot_{R} M = 0_{R} \to K ∥ l)))$
31	28 30	mpbird	$⊢ φ \to M \in (R PrimRoots K)$

Metamath Proof Explorer

Theorem isprimroot2

Proof