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	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
	primrootlekpowne0.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	primrootlekpowne0.3	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )
	primrootlekpowne0.4	⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... ( 𝐾 − 1 ) ) )
Assertion	primrootlekpowne0	⊢ ( 𝜑 → ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) ≠ ( 0g ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		primrootlekpowne0.1	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
2		primrootlekpowne0.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3		primrootlekpowne0.3	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )
4		primrootlekpowne0.4	⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... ( 𝐾 − 1 ) ) )
5		oveq1	⊢ ( 𝑙 = 𝑁 → ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) )
6	5	eqeq1d	⊢ ( 𝑙 = 𝑁 → ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) )
7		breq2	⊢ ( 𝑙 = 𝑁 → ( 𝐾 ∥ 𝑙 ↔ 𝐾 ∥ 𝑁 ) )
8	6 7	imbi12d	⊢ ( 𝑙 = 𝑁 → ( ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ↔ ( ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑁 ) ) )
9	2	nnnn0d	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
10		eqid	⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
11	1 9 10	isprimroot	⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) ↔ ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
12	11	biimpd	⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) → ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) ) )
13	3 12	mpd	⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐾 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) ) )
14	13	simp3d	⊢ ( 𝜑 → ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑙 ) )
16		elfznn	⊢ ( 𝑁 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑁 ∈ ℕ )
17	4 16	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
18	17	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
19	18	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → 𝑁 ∈ ℕ0 )
20	8 15 19	rspcdva	⊢ ( ( 𝜑 ∧ ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → ( ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) → 𝐾 ∥ 𝑁 ) )
21	20	syldbl2	⊢ ( ( 𝜑 ∧ ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → 𝐾 ∥ 𝑁 )
22	17	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
23	2	nnred	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
24		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
25	23 24	resubcld	⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℝ )
26		elfzle2	⊢ ( 𝑁 ∈ ( 1 ... ( 𝐾 − 1 ) ) → 𝑁 ≤ ( 𝐾 − 1 ) )
27	4 26	syl	⊢ ( 𝜑 → 𝑁 ≤ ( 𝐾 − 1 ) )
28	23	ltm1d	⊢ ( 𝜑 → ( 𝐾 − 1 ) < 𝐾 )
29	22 25 23 27 28	lelttrd	⊢ ( 𝜑 → 𝑁 < 𝐾 )
30	22 23	ltnled	⊢ ( 𝜑 → ( 𝑁 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑁 ) )
31	29 30	mpbid	⊢ ( 𝜑 → ¬ 𝐾 ≤ 𝑁 )
32	9	nn0zd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
33		dvdsle	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝐾 ∥ 𝑁 → 𝐾 ≤ 𝑁 ) )
34	32 17 33	syl2anc	⊢ ( 𝜑 → ( 𝐾 ∥ 𝑁 → 𝐾 ≤ 𝑁 ) )
35	34	con3d	⊢ ( 𝜑 → ( ¬ 𝐾 ≤ 𝑁 → ¬ 𝐾 ∥ 𝑁 ) )
36	31 35	mpd	⊢ ( 𝜑 → ¬ 𝐾 ∥ 𝑁 )
37	36	adantr	⊢ ( ( 𝜑 ∧ ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → ¬ 𝐾 ∥ 𝑁 )
38	21 37	pm2.21dd	⊢ ( ( 𝜑 ∧ ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) = ( 0g ‘ 𝑅 ) ) → ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) ≠ ( 0g ‘ 𝑅 ) )
39		simpr	⊢ ( ( 𝜑 ∧ ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) ≠ ( 0g ‘ 𝑅 ) )
40	38 39	pm2.61dane	⊢ ( 𝜑 → ( 𝑁 ( .g ‘ 𝑅 ) 𝑀 ) ≠ ( 0g ‘ 𝑅 ) )