Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
primrootspoweq0.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
primrootspoweq0.3 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )
primrootspoweq0.4 ⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
primrootspoweq0.5 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion primrootspoweq0 ( 𝜑 → ( ( 𝑁 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ 𝐾 ∥ 𝑁 ) )

Proof

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