primrootspoweq0

Description: The power of a R -th primitive root is zero if and only if it divides R . (Contributed by metakunt, 15-May-2025)

	Ref	Expression
Hypotheses	primrootspoweq0.1	$⊢ φ \to R \in CMnd$
	primrootspoweq0.2	$⊢ φ \to K \in ℕ$
	primrootspoweq0.3	$⊢ φ \to M \in (R PrimRoots K)$
	primrootspoweq0.4	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
	primrootspoweq0.5	$⊢ φ \to N \in ℤ$
Assertion	primrootspoweq0	$⊢ φ \to (N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \leftrightarrow K ∥ N)$

Proof

Step	Hyp	Ref	Expression
1		primrootspoweq0.1	$⊢ φ \to R \in CMnd$
2		primrootspoweq0.2	$⊢ φ \to K \in ℕ$
3		primrootspoweq0.3	$⊢ φ \to M \in (R PrimRoots K)$
4		primrootspoweq0.4	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
5		primrootspoweq0.5	$⊢ φ \to N \in ℤ$
6		simplr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to N = x K + y$
7	6	oveq1d	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to N \cdot_{(R ↾_{𝑠} U)} M = (x K + y) \cdot_{(R ↾_{𝑠} U)} M$
8	1 2 4	primrootsunit	$⊢ φ \to (R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K \land R ↾_{𝑠} U \in Abel)$
9	8	simprd	$⊢ φ \to R ↾_{𝑠} U \in Abel$
10	9	ad4antr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to R ↾_{𝑠} U \in Abel$
11	10	ablgrpd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to R ↾_{𝑠} U \in Grp$
12		simp-4r	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to x \in ℤ$
13	2	nnzd	$⊢ φ \to K \in ℤ$
14	13	ad4antr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to K \in ℤ$
15	12 14	zmulcld	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to x K \in ℤ$
16		simpllr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to y \in (0 \dots K - 1)$
17	16	elfzelzd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to y \in ℤ$
18	8	simpld	$⊢ φ \to R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K$
19	3 18	eleqtrd	$⊢ φ \to M \in ((R ↾_{𝑠} U) PrimRoots K)$
20		ablcmn	$⊢ R ↾_{𝑠} U \in Abel \to R ↾_{𝑠} U \in CMnd$
21	9 20	syl	$⊢ φ \to R ↾_{𝑠} U \in CMnd$
22	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
23		eqid	$⊢ \cdot_{(R ↾_{𝑠} U)} = \cdot_{(R ↾_{𝑠} U)}$
24	21 22 23	isprimroot	$⊢ φ \to (M \in ((R ↾_{𝑠} U) PrimRoots K) \leftrightarrow (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
25	24	biimpd	$⊢ φ \to (M \in ((R ↾_{𝑠} U) PrimRoots K) \to (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l)))$
26	19 25	mpd	$⊢ φ \to (M \in {Base}_{(R ↾_{𝑠} U)} \land K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \land \forall l \in ℕ_{0} (l \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ l))$
27	26	simp1d	$⊢ φ \to M \in {Base}_{(R ↾_{𝑠} U)}$
28	27	ad4antr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to M \in {Base}_{(R ↾_{𝑠} U)}$
29	15 17 28	3jca	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (x K \in ℤ \land y \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
30		eqid	$⊢ {Base}_{(R ↾_{𝑠} U)} = {Base}_{(R ↾_{𝑠} U)}$
31		eqid	$⊢ +_{(R ↾_{𝑠} U)} = +_{(R ↾_{𝑠} U)}$
32	30 23 31	mulgdir	$⊢ (R ↾_{𝑠} U \in Grp \land (x K \in ℤ \land y \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to (x K + y) \cdot_{(R ↾_{𝑠} U)} M = (x K \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (y \cdot_{(R ↾_{𝑠} U)} M)$
33	11 29 32	syl2anc	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (x K + y) \cdot_{(R ↾_{𝑠} U)} M = (x K \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (y \cdot_{(R ↾_{𝑠} U)} M)$
34	12 14 28	3jca	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (x \in ℤ \land K \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
35	30 23	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (x \in ℤ \land K \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to x K \cdot_{(R ↾_{𝑠} U)} M = x \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M)$
36	11 34 35	syl2anc	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to x K \cdot_{(R ↾_{𝑠} U)} M = x \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M)$
37	26	simp2d	$⊢ φ \to K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
38	37	ad4antr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
39	38	oveq2d	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to x \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M) = x \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
40		eqid	$⊢ 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
41	30 23 40	mulgz	$⊢ (R ↾_{𝑠} U \in Grp \land x \in ℤ) \to x \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
42	11 12 41	syl2anc	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to x \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
43	39 42	eqtrd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to x \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)}$
44	36 43	eqtrd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to x K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
45	44	oveq1d	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (x K \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (y \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)} +_{(R ↾_{𝑠} U)} (y \cdot_{(R ↾_{𝑠} U)} M)$
46	30 23 11 17 28	mulgcld	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to y \cdot_{(R ↾_{𝑠} U)} M \in {Base}_{(R ↾_{𝑠} U)}$
47	30 31 40 11 46	grplidd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to 0_{(R ↾_{𝑠} U)} +_{(R ↾_{𝑠} U)} (y \cdot_{(R ↾_{𝑠} U)} M) = y \cdot_{(R ↾_{𝑠} U)} M$
48	45 47	eqtrd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (x K \cdot_{(R ↾_{𝑠} U)} M) +_{(R ↾_{𝑠} U)} (y \cdot_{(R ↾_{𝑠} U)} M) = y \cdot_{(R ↾_{𝑠} U)} M$
49	33 48	eqtrd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (x K + y) \cdot_{(R ↾_{𝑠} U)} M = y \cdot_{(R ↾_{𝑠} U)} M$
50	7 49	eqtrd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to N \cdot_{(R ↾_{𝑠} U)} M = y \cdot_{(R ↾_{𝑠} U)} M$
51	10 20	syl	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to R ↾_{𝑠} U \in CMnd$
52	2	ad4antr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to K \in ℕ$
53	3	ad4antr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to M \in (R PrimRoots K)$
54	18	ad4antr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to R PrimRoots K = (R ↾_{𝑠} U) PrimRoots K$
55	53 54	eleqtrd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to M \in ((R ↾_{𝑠} U) PrimRoots K)$
56		1cnd	$⊢ φ \to 1 \in ℂ$
57	56	addlidd	$⊢ φ \to 0 + 1 = 1$
58	2	nnge1d	$⊢ φ \to 1 \leq K$
59	57 58	eqbrtrd	$⊢ φ \to 0 + 1 \leq K$
60		0red	$⊢ φ \to 0 \in ℝ$
61		1red	$⊢ φ \to 1 \in ℝ$
62	2	nnred	$⊢ φ \to K \in ℝ$
63		leaddsub	$⊢ (0 \in ℝ \land 1 \in ℝ \land K \in ℝ) \to (0 + 1 \leq K \leftrightarrow 0 \leq K - 1)$
64	60 61 62 63	syl3anc	$⊢ φ \to (0 + 1 \leq K \leftrightarrow 0 \leq K - 1)$
65	59 64	mpbid	$⊢ φ \to 0 \leq K - 1$
66		0zd	$⊢ φ \to 0 \in ℤ$
67		1zzd	$⊢ φ \to 1 \in ℤ$
68	13 67	zsubcld	$⊢ φ \to K - 1 \in ℤ$
69		eluz	$⊢ (0 \in ℤ \land K - 1 \in ℤ) \to (K - 1 \in ℤ_{\geq 0} \leftrightarrow 0 \leq K - 1)$
70	66 68 69	syl2anc	$⊢ φ \to (K - 1 \in ℤ_{\geq 0} \leftrightarrow 0 \leq K - 1)$
71	65 70	mpbird	$⊢ φ \to K - 1 \in ℤ_{\geq 0}$
72		elfzp12	$⊢ K - 1 \in ℤ_{\geq 0} \to (y \in (0 \dots K - 1) \leftrightarrow (y = 0 \lor y \in (0 + 1 \dots K - 1)))$
73	71 72	syl	$⊢ φ \to (y \in (0 \dots K - 1) \leftrightarrow (y = 0 \lor y \in (0 + 1 \dots K - 1)))$
74	73	ad4antr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (y \in (0 \dots K - 1) \leftrightarrow (y = 0 \lor y \in (0 + 1 \dots K - 1)))$
75	74	biimpd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (y \in (0 \dots K - 1) \to (y = 0 \lor y \in (0 + 1 \dots K - 1)))$
76	16 75	mpd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (y = 0 \lor y \in (0 + 1 \dots K - 1))$
77		simp-5r	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to x \in ℤ$
78	52	adantr	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to K \in ℕ$
79	78	nnzd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to K \in ℤ$
80		dvdsmul2	$⊢ (x \in ℤ \land K \in ℤ) \to K ∥ x K$
81	77 79 80	syl2anc	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to K ∥ x K$
82	77	zcnd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to x \in ℂ$
83	78	nncnd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to K \in ℂ$
84	82 83	mulcld	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to x K \in ℂ$
85	84	addridd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to x K + 0 = x K$
86	85	eqcomd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to x K = x K + 0$
87		simpr	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to y = 0$
88	87	eqcomd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to 0 = y$
89	88	oveq2d	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to x K + 0 = x K + y$
90	86 89	eqtrd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to x K = x K + y$
91	81 90	breqtrd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to K ∥ (x K + y)$
92	6	adantr	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to N = x K + y$
93	92	eqcomd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to x K + y = N$
94	91 93	breqtrd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to K ∥ N$
95		simplr	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to \neg K ∥ N$
96	94 95	pm2.21dd	$⊢ (((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \land y = 0) \to y \in (1 \dots K - 1)$
97	96	ex	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (y = 0 \to y \in (1 \dots K - 1))$
98		1cnd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to 1 \in ℂ$
99	98	addlidd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to 0 + 1 = 1$
100	99	oveq1d	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (0 + 1 \dots K - 1) = (1 \dots K - 1)$
101		ssidd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (1 \dots K - 1) \subseteq (1 \dots K - 1)$
102	100 101	eqsstrd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (0 + 1 \dots K - 1) \subseteq (1 \dots K - 1)$
103	102	sseld	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to (y \in (0 + 1 \dots K - 1) \to y \in (1 \dots K - 1))$
104	97 103	jaod	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to ((y = 0 \lor y \in (0 + 1 \dots K - 1)) \to y \in (1 \dots K - 1))$
105	76 104	mpd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to y \in (1 \dots K - 1)$
106	51 52 55 105	primrootlekpowne0	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to y \cdot_{(R ↾_{𝑠} U)} M \neq 0_{(R ↾_{𝑠} U)}$
107	50 106	eqnetrd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to N \cdot_{(R ↾_{𝑠} U)} M \neq 0_{(R ↾_{𝑠} U)}$
108	107	neneqd	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land \neg K ∥ N) \to \neg N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
109	108	ex	$⊢ (((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \to (\neg K ∥ N \to \neg N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)})$
110	109	con4d	$⊢ (((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \to (N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \to K ∥ N)$
111		simp-4l	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land K ∥ N) \to φ$
112		simpr	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land K ∥ N) \to K ∥ N$
113	111 112	jca	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land K ∥ N) \to (φ \land K ∥ N)$
114		divides	$⊢ (K \in ℤ \land N \in ℤ) \to (K ∥ N \leftrightarrow \exists x \in ℤ x K = N)$
115	13 5 114	syl2anc	$⊢ φ \to (K ∥ N \leftrightarrow \exists x \in ℤ x K = N)$
116	115	biimpd	$⊢ φ \to (K ∥ N \to \exists x \in ℤ x K = N)$
117	116	imp	$⊢ (φ \land K ∥ N) \to \exists x \in ℤ x K = N$
118		simpr	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to y K = N$
119	118	eqcomd	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to N = y K$
120	119	oveq1d	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to N \cdot_{(R ↾_{𝑠} U)} M = y K \cdot_{(R ↾_{𝑠} U)} M$
121	9	ad3antrrr	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to R ↾_{𝑠} U \in Abel$
122		ablgrp	$⊢ R ↾_{𝑠} U \in Abel \to R ↾_{𝑠} U \in Grp$
123	121 122	syl	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to R ↾_{𝑠} U \in Grp$
124		simplr	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to y \in ℤ$
125	13	ad3antrrr	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to K \in ℤ$
126	27	ad3antrrr	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to M \in {Base}_{(R ↾_{𝑠} U)}$
127	124 125 126	3jca	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to (y \in ℤ \land K \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})$
128	30 23	mulgass	$⊢ (R ↾_{𝑠} U \in Grp \land (y \in ℤ \land K \in ℤ \land M \in {Base}_{(R ↾_{𝑠} U)})) \to y K \cdot_{(R ↾_{𝑠} U)} M = y \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M)$
129	123 127 128	syl2anc	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to y K \cdot_{(R ↾_{𝑠} U)} M = y \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M)$
130	37	ad3antrrr	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
131	130	oveq2d	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to y \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M) = y \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)}$
132	30 23 40	mulgz	$⊢ (R ↾_{𝑠} U \in Grp \land y \in ℤ) \to y \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
133	123 124 132	syl2anc	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to y \cdot_{(R ↾_{𝑠} U)} 0_{(R ↾_{𝑠} U)} = 0_{(R ↾_{𝑠} U)}$
134	131 133	eqtrd	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to y \cdot_{(R ↾_{𝑠} U)} (K \cdot_{(R ↾_{𝑠} U)} M) = 0_{(R ↾_{𝑠} U)}$
135	129 134	eqtrd	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to y K \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
136	120 135	eqtrd	$⊢ (((φ \land \exists x \in ℤ x K = N) \land y \in ℤ) \land y K = N) \to N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
137		nfv	$⊢ Ⅎ y x K = N$
138		nfv	$⊢ Ⅎ x y K = N$
139		oveq1	$⊢ x = y \to x K = y K$
140	139	eqeq1d	$⊢ x = y \to (x K = N \leftrightarrow y K = N)$
141	137 138 140	cbvrexw	$⊢ \exists x \in ℤ x K = N \leftrightarrow \exists y \in ℤ y K = N$
142	141	biimpi	$⊢ \exists x \in ℤ x K = N \to \exists y \in ℤ y K = N$
143	142	adantl	$⊢ (φ \land \exists x \in ℤ x K = N) \to \exists y \in ℤ y K = N$
144	136 143	r19.29a	$⊢ (φ \land \exists x \in ℤ x K = N) \to N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
145	144	ex	$⊢ φ \to (\exists x \in ℤ x K = N \to N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)})$
146	145	adantr	$⊢ (φ \land K ∥ N) \to (\exists x \in ℤ x K = N \to N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)})$
147	117 146	mpd	$⊢ (φ \land K ∥ N) \to N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
148	113 147	syl	$⊢ ((((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \land K ∥ N) \to N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)}$
149	148	ex	$⊢ (((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \to (K ∥ N \to N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)})$
150	110 149	impbid	$⊢ (((φ \land x \in ℤ) \land y \in (0 \dots K - 1)) \land N = x K + y) \to (N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \leftrightarrow K ∥ N)$
151	5 2	remexz	$⊢ φ \to \exists x \in ℤ \exists y \in (0 \dots K - 1) N = x K + y$
152	150 151	r19.29vva	$⊢ φ \to (N \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \leftrightarrow K ∥ N)$

Metamath Proof Explorer

Theorem primrootspoweq0

Proof