Theorem primrootlekpowne0

Description: There is no smaller power of a primitive root that sends it to the neutral element. (Contributed by metakunt, 15-May-2025)

	Ref	Expression
Hypotheses	primrootlekpowne0.1	$$⊢\phi \to R\in \mathrm{CMnd}$$
	primrootlekpowne0.2	$$⊢\phi \to K\in \mathbb{N}$$
	primrootlekpowne0.3	$$⊢\phi \to M\in \left(R\mathrm{PrimRoots}K\right)$$
	primrootlekpowne0.4	$$⊢\phi \to N\in \left(1\dots K-1\right)$$
Assertion	primrootlekpowne0	$$⊢\phi \to N{\cdot }_{R}M\ne 0_R$$

Proof

Step	Hyp	Ref	Expression
1		primrootlekpowne0.1	$$⊢\phi \to R\in \mathrm{CMnd}$$
2		primrootlekpowne0.2	$$⊢\phi \to K\in \mathbb{N}$$
3		primrootlekpowne0.3	$$⊢\phi \to M\in \left(R\mathrm{PrimRoots}K\right)$$
4		primrootlekpowne0.4	$$⊢\phi \to N\in \left(1\dots K-1\right)$$
5		oveq1	$$⊢l=N\to l{\cdot }_{R}M=N{\cdot }_{R}M$$
6	5	eqeq1d	$$⊢l=N\to \left(l{\cdot }_{R}M=0_R\leftrightarrow N{\cdot }_{R}M=0_R\right)$$
7		breq2	$$⊢l=N\to \left(K\parallel l\leftrightarrow K\parallel N\right)$$
8	6 7	imbi12d	$$⊢l=N\to \left(\left(l{\cdot }_{R}M=0_R\to K\parallel l\right)\leftrightarrow \left(N{\cdot }_{R}M=0_R\to K\parallel N\right)\right)$$
9	2	nnnn0d	$$⊢\phi \to K\in {\mathbb{N}}_0$$
10		eqid	$$⊢{\cdot }_R={\cdot }_R$$
11	1 9 10	isprimroot	$$⊢\phi \to \left(M\in \left(R\mathrm{PrimRoots}K\right)\leftrightarrow \left(M\in {\mathrm{Base}}_R\wedge K{\cdot }_{R}M=0_R\wedge \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{R}M=0_R\to K\parallel l\right)\right)\right)$$
12	11	biimpd	$$⊢\phi \to \left(M\in \left(R\mathrm{PrimRoots}K\right)\to \left(M\in {\mathrm{Base}}_R\wedge K{\cdot }_{R}M=0_R\wedge \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{R}M=0_R\to K\parallel l\right)\right)\right)$$
13	3 12	mpd	$$⊢\phi \to \left(M\in {\mathrm{Base}}_R\wedge K{\cdot }_{R}M=0_R\wedge \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{R}M=0_R\to K\parallel l\right)\right)$$
14	13	simp3d	$$⊢\phi \to \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{R}M=0_R\to K\parallel l\right)$$
15	14	adantr	$$⊢\left(\phi \wedge N{\cdot }_{R}M=0_R\right)\to \forall l\in {\mathbb{N}}_0\left(l{\cdot }_{R}M=0_R\to K\parallel l\right)$$
16		elfznn	$$⊢N\in \left(1\dots K-1\right)\to N\in \mathbb{N}$$
17	4 16	syl	$$⊢\phi \to N\in \mathbb{N}$$
18	17	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
19	18	adantr	$$⊢\left(\phi \wedge N{\cdot }_{R}M=0_R\right)\to N\in {\mathbb{N}}_0$$
20	8 15 19	rspcdva	$$⊢\left(\phi \wedge N{\cdot }_{R}M=0_R\right)\to \left(N{\cdot }_{R}M=0_R\to K\parallel N\right)$$
21	20	syldbl2	$$⊢\left(\phi \wedge N{\cdot }_{R}M=0_R\right)\to K\parallel N$$
22	17	nnred	$$⊢\phi \to N\in ℝ$$
23	2	nnred	$$⊢\phi \to K\in ℝ$$
24		1red	$$⊢\phi \to 1\in ℝ$$
25	23 24	resubcld	$$⊢\phi \to K-1\in ℝ$$
26		elfzle2	$$⊢N\in \left(1\dots K-1\right)\to N\le K-1$$
27	4 26	syl	$$⊢\phi \to N\le K-1$$
28	23	ltm1d	$$⊢\phi \to K-1<K$$
29	22 25 23 27 28	lelttrd	$$⊢\phi \to N<K$$
30	22 23	ltnled	$$⊢\phi \to \left(N<K\leftrightarrow \neg K\le N\right)$$
31	29 30	mpbid	$$⊢\phi \to \neg K\le N$$
32	9	nn0zd	$$⊢\phi \to K\in \mathbb{Z}$$
33		dvdsle	$$⊢\left(K\in \mathbb{Z}\wedge N\in \mathbb{N}\right)\to \left(K\parallel N\to K\le N\right)$$
34	32 17 33	syl2anc	$$⊢\phi \to \left(K\parallel N\to K\le N\right)$$
35	34	con3d	$$⊢\phi \to \left(\neg K\le N\to \neg K\parallel N\right)$$
36	31 35	mpd	$$⊢\phi \to \neg K\parallel N$$
37	36	adantr	$$⊢\left(\phi \wedge N{\cdot }_{R}M=0_R\right)\to \neg K\parallel N$$
38	21 37	pm2.21dd	$$⊢\left(\phi \wedge N{\cdot }_{R}M=0_R\right)\to N{\cdot }_{R}M\ne 0_R$$
39		simpr	$$⊢\left(\phi \wedge N{\cdot }_{R}M\ne 0_R\right)\to N{\cdot }_{R}M\ne 0_R$$
40	38 39	pm2.61dane	$$⊢\phi \to N{\cdot }_{R}M\ne 0_R$$