Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  primrootspoweq0 Structured version   Visualization version   GIF version

Theorem primrootspoweq0 42088
Description: The power of a 𝑅-th primitive root is zero if and only if it divides 𝑅. (Contributed by metakunt, 15-May-2025.)
Hypotheses
Ref Expression
primrootspoweq0.1 (𝜑𝑅 ∈ CMnd)
primrootspoweq0.2 (𝜑𝐾 ∈ ℕ)
primrootspoweq0.3 (𝜑𝑀 ∈ (𝑅 PrimRoots 𝐾))
primrootspoweq0.4 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g𝑅)𝑎) = (0g𝑅)}
primrootspoweq0.5 (𝜑𝑁 ∈ ℤ)
Assertion
Ref Expression
primrootspoweq0 (𝜑 → ((𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) ↔ 𝐾𝑁))
Distinct variable group:   𝑅,𝑎,𝑖
Allowed substitution hints:   𝜑(𝑖,𝑎)   𝑈(𝑖,𝑎)   𝐾(𝑖,𝑎)   𝑀(𝑖,𝑎)   𝑁(𝑖,𝑎)

Proof of Theorem primrootspoweq0
Dummy variables 𝑙 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simplr 769 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝑁 = ((𝑥 · 𝐾) + 𝑦))
21oveq1d 7446 . . . . . . . 8 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (((𝑥 · 𝐾) + 𝑦)(.g‘(𝑅s 𝑈))𝑀))
3 primrootspoweq0.1 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ CMnd)
4 primrootspoweq0.2 . . . . . . . . . . . . . 14 (𝜑𝐾 ∈ ℕ)
5 primrootspoweq0.4 . . . . . . . . . . . . . 14 𝑈 = {𝑎 ∈ (Base‘𝑅) ∣ ∃𝑖 ∈ (Base‘𝑅)(𝑖(+g𝑅)𝑎) = (0g𝑅)}
63, 4, 5primrootsunit 42080 . . . . . . . . . . . . 13 (𝜑 → ((𝑅 PrimRoots 𝐾) = ((𝑅s 𝑈) PrimRoots 𝐾) ∧ (𝑅s 𝑈) ∈ Abel))
76simprd 495 . . . . . . . . . . . 12 (𝜑 → (𝑅s 𝑈) ∈ Abel)
87ad4antr 732 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑅s 𝑈) ∈ Abel)
98ablgrpd 19819 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑅s 𝑈) ∈ Grp)
10 simp-4r 784 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝑥 ∈ ℤ)
114nnzd 12638 . . . . . . . . . . . . 13 (𝜑𝐾 ∈ ℤ)
1211ad4antr 732 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝐾 ∈ ℤ)
1310, 12zmulcld 12726 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑥 · 𝐾) ∈ ℤ)
14 simpllr 776 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝑦 ∈ (0...(𝐾 − 1)))
1514elfzelzd 13562 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝑦 ∈ ℤ)
16 primrootspoweq0.3 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ (𝑅 PrimRoots 𝐾))
176simpld 494 . . . . . . . . . . . . . . 15 (𝜑 → (𝑅 PrimRoots 𝐾) = ((𝑅s 𝑈) PrimRoots 𝐾))
1816, 17eleqtrd 2841 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ((𝑅s 𝑈) PrimRoots 𝐾))
19 ablcmn 19820 . . . . . . . . . . . . . . . . 17 ((𝑅s 𝑈) ∈ Abel → (𝑅s 𝑈) ∈ CMnd)
207, 19syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑅s 𝑈) ∈ CMnd)
214nnnn0d 12585 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ ℕ0)
22 eqid 2735 . . . . . . . . . . . . . . . 16 (.g‘(𝑅s 𝑈)) = (.g‘(𝑅s 𝑈))
2320, 21, 22isprimroot 42075 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀 ∈ ((𝑅s 𝑈) PrimRoots 𝐾) ↔ (𝑀 ∈ (Base‘(𝑅s 𝑈)) ∧ (𝐾(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) → 𝐾𝑙))))
2423biimpd 229 . . . . . . . . . . . . . 14 (𝜑 → (𝑀 ∈ ((𝑅s 𝑈) PrimRoots 𝐾) → (𝑀 ∈ (Base‘(𝑅s 𝑈)) ∧ (𝐾(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) → 𝐾𝑙))))
2518, 24mpd 15 . . . . . . . . . . . . 13 (𝜑 → (𝑀 ∈ (Base‘(𝑅s 𝑈)) ∧ (𝐾(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) ∧ ∀𝑙 ∈ ℕ0 ((𝑙(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) → 𝐾𝑙)))
2625simp1d 1141 . . . . . . . . . . . 12 (𝜑𝑀 ∈ (Base‘(𝑅s 𝑈)))
2726ad4antr 732 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝑀 ∈ (Base‘(𝑅s 𝑈)))
2813, 15, 273jca 1127 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → ((𝑥 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅s 𝑈))))
29 eqid 2735 . . . . . . . . . . 11 (Base‘(𝑅s 𝑈)) = (Base‘(𝑅s 𝑈))
30 eqid 2735 . . . . . . . . . . 11 (+g‘(𝑅s 𝑈)) = (+g‘(𝑅s 𝑈))
3129, 22, 30mulgdir 19137 . . . . . . . . . 10 (((𝑅s 𝑈) ∈ Grp ∧ ((𝑥 · 𝐾) ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅s 𝑈)))) → (((𝑥 · 𝐾) + 𝑦)(.g‘(𝑅s 𝑈))𝑀) = (((𝑥 · 𝐾)(.g‘(𝑅s 𝑈))𝑀)(+g‘(𝑅s 𝑈))(𝑦(.g‘(𝑅s 𝑈))𝑀)))
329, 28, 31syl2anc 584 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (((𝑥 · 𝐾) + 𝑦)(.g‘(𝑅s 𝑈))𝑀) = (((𝑥 · 𝐾)(.g‘(𝑅s 𝑈))𝑀)(+g‘(𝑅s 𝑈))(𝑦(.g‘(𝑅s 𝑈))𝑀)))
3310, 12, 273jca 1127 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑥 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅s 𝑈))))
3429, 22mulgass 19142 . . . . . . . . . . . . 13 (((𝑅s 𝑈) ∈ Grp ∧ (𝑥 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅s 𝑈)))) → ((𝑥 · 𝐾)(.g‘(𝑅s 𝑈))𝑀) = (𝑥(.g‘(𝑅s 𝑈))(𝐾(.g‘(𝑅s 𝑈))𝑀)))
359, 33, 34syl2anc 584 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → ((𝑥 · 𝐾)(.g‘(𝑅s 𝑈))𝑀) = (𝑥(.g‘(𝑅s 𝑈))(𝐾(.g‘(𝑅s 𝑈))𝑀)))
3625simp2d 1142 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
3736ad4antr 732 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝐾(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
3837oveq2d 7447 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑥(.g‘(𝑅s 𝑈))(𝐾(.g‘(𝑅s 𝑈))𝑀)) = (𝑥(.g‘(𝑅s 𝑈))(0g‘(𝑅s 𝑈))))
39 eqid 2735 . . . . . . . . . . . . . . 15 (0g‘(𝑅s 𝑈)) = (0g‘(𝑅s 𝑈))
4029, 22, 39mulgz 19133 . . . . . . . . . . . . . 14 (((𝑅s 𝑈) ∈ Grp ∧ 𝑥 ∈ ℤ) → (𝑥(.g‘(𝑅s 𝑈))(0g‘(𝑅s 𝑈))) = (0g‘(𝑅s 𝑈)))
419, 10, 40syl2anc 584 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑥(.g‘(𝑅s 𝑈))(0g‘(𝑅s 𝑈))) = (0g‘(𝑅s 𝑈)))
4238, 41eqtrd 2775 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑥(.g‘(𝑅s 𝑈))(𝐾(.g‘(𝑅s 𝑈))𝑀)) = (0g‘(𝑅s 𝑈)))
4335, 42eqtrd 2775 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → ((𝑥 · 𝐾)(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
4443oveq1d 7446 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (((𝑥 · 𝐾)(.g‘(𝑅s 𝑈))𝑀)(+g‘(𝑅s 𝑈))(𝑦(.g‘(𝑅s 𝑈))𝑀)) = ((0g‘(𝑅s 𝑈))(+g‘(𝑅s 𝑈))(𝑦(.g‘(𝑅s 𝑈))𝑀)))
4529, 22, 9, 15, 27mulgcld 19127 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑦(.g‘(𝑅s 𝑈))𝑀) ∈ (Base‘(𝑅s 𝑈)))
4629, 30, 39, 9, 45grplidd 19000 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → ((0g‘(𝑅s 𝑈))(+g‘(𝑅s 𝑈))(𝑦(.g‘(𝑅s 𝑈))𝑀)) = (𝑦(.g‘(𝑅s 𝑈))𝑀))
4744, 46eqtrd 2775 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (((𝑥 · 𝐾)(.g‘(𝑅s 𝑈))𝑀)(+g‘(𝑅s 𝑈))(𝑦(.g‘(𝑅s 𝑈))𝑀)) = (𝑦(.g‘(𝑅s 𝑈))𝑀))
4832, 47eqtrd 2775 . . . . . . . 8 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (((𝑥 · 𝐾) + 𝑦)(.g‘(𝑅s 𝑈))𝑀) = (𝑦(.g‘(𝑅s 𝑈))𝑀))
492, 48eqtrd 2775 . . . . . . 7 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (𝑦(.g‘(𝑅s 𝑈))𝑀))
508, 19syl 17 . . . . . . . 8 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑅s 𝑈) ∈ CMnd)
514ad4antr 732 . . . . . . . 8 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝐾 ∈ ℕ)
5216ad4antr 732 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝑀 ∈ (𝑅 PrimRoots 𝐾))
5317ad4antr 732 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑅 PrimRoots 𝐾) = ((𝑅s 𝑈) PrimRoots 𝐾))
5452, 53eleqtrd 2841 . . . . . . . 8 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝑀 ∈ ((𝑅s 𝑈) PrimRoots 𝐾))
55 1cnd 11254 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℂ)
5655addlidd 11460 . . . . . . . . . . . . . . . 16 (𝜑 → (0 + 1) = 1)
574nnge1d 12312 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ≤ 𝐾)
5856, 57eqbrtrd 5170 . . . . . . . . . . . . . . 15 (𝜑 → (0 + 1) ≤ 𝐾)
59 0red 11262 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℝ)
60 1red 11260 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℝ)
614nnred 12279 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ ℝ)
62 leaddsub 11737 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐾 ∈ ℝ) → ((0 + 1) ≤ 𝐾 ↔ 0 ≤ (𝐾 − 1)))
6359, 60, 61, 62syl3anc 1370 . . . . . . . . . . . . . . 15 (𝜑 → ((0 + 1) ≤ 𝐾 ↔ 0 ≤ (𝐾 − 1)))
6458, 63mpbid 232 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ (𝐾 − 1))
65 0zd 12623 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ℤ)
66 1zzd 12646 . . . . . . . . . . . . . . . 16 (𝜑 → 1 ∈ ℤ)
6711, 66zsubcld 12725 . . . . . . . . . . . . . . 15 (𝜑 → (𝐾 − 1) ∈ ℤ)
68 eluz 12890 . . . . . . . . . . . . . . 15 ((0 ∈ ℤ ∧ (𝐾 − 1) ∈ ℤ) → ((𝐾 − 1) ∈ (ℤ‘0) ↔ 0 ≤ (𝐾 − 1)))
6965, 67, 68syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → ((𝐾 − 1) ∈ (ℤ‘0) ↔ 0 ≤ (𝐾 − 1)))
7064, 69mpbird 257 . . . . . . . . . . . . 13 (𝜑 → (𝐾 − 1) ∈ (ℤ‘0))
71 elfzp12 13640 . . . . . . . . . . . . 13 ((𝐾 − 1) ∈ (ℤ‘0) → (𝑦 ∈ (0...(𝐾 − 1)) ↔ (𝑦 = 0 ∨ 𝑦 ∈ ((0 + 1)...(𝐾 − 1)))))
7270, 71syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑦 ∈ (0...(𝐾 − 1)) ↔ (𝑦 = 0 ∨ 𝑦 ∈ ((0 + 1)...(𝐾 − 1)))))
7372ad4antr 732 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑦 ∈ (0...(𝐾 − 1)) ↔ (𝑦 = 0 ∨ 𝑦 ∈ ((0 + 1)...(𝐾 − 1)))))
7473biimpd 229 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑦 ∈ (0...(𝐾 − 1)) → (𝑦 = 0 ∨ 𝑦 ∈ ((0 + 1)...(𝐾 − 1)))))
7514, 74mpd 15 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑦 = 0 ∨ 𝑦 ∈ ((0 + 1)...(𝐾 − 1))))
76 simp-5r 786 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝑥 ∈ ℤ)
7751adantr 480 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝐾 ∈ ℕ)
7877nnzd 12638 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝐾 ∈ ℤ)
79 dvdsmul2 16313 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℤ ∧ 𝐾 ∈ ℤ) → 𝐾 ∥ (𝑥 · 𝐾))
8076, 78, 79syl2anc 584 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝐾 ∥ (𝑥 · 𝐾))
8176zcnd 12721 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝑥 ∈ ℂ)
8277nncnd 12280 . . . . . . . . . . . . . . . . . 18 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝐾 ∈ ℂ)
8381, 82mulcld 11279 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → (𝑥 · 𝐾) ∈ ℂ)
8483addridd 11459 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → ((𝑥 · 𝐾) + 0) = (𝑥 · 𝐾))
8584eqcomd 2741 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → (𝑥 · 𝐾) = ((𝑥 · 𝐾) + 0))
86 simpr 484 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝑦 = 0)
8786eqcomd 2741 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 0 = 𝑦)
8887oveq2d 7447 . . . . . . . . . . . . . . 15 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → ((𝑥 · 𝐾) + 0) = ((𝑥 · 𝐾) + 𝑦))
8985, 88eqtrd 2775 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → (𝑥 · 𝐾) = ((𝑥 · 𝐾) + 𝑦))
9080, 89breqtrd 5174 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝐾 ∥ ((𝑥 · 𝐾) + 𝑦))
911adantr 480 . . . . . . . . . . . . . 14 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝑁 = ((𝑥 · 𝐾) + 𝑦))
9291eqcomd 2741 . . . . . . . . . . . . 13 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → ((𝑥 · 𝐾) + 𝑦) = 𝑁)
9390, 92breqtrd 5174 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝐾𝑁)
94 simplr 769 . . . . . . . . . . . 12 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → ¬ 𝐾𝑁)
9593, 94pm2.21dd 195 . . . . . . . . . . 11 ((((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) ∧ 𝑦 = 0) → 𝑦 ∈ (1...(𝐾 − 1)))
9695ex 412 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑦 = 0 → 𝑦 ∈ (1...(𝐾 − 1))))
97 1cnd 11254 . . . . . . . . . . . . . 14 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 1 ∈ ℂ)
9897addlidd 11460 . . . . . . . . . . . . 13 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (0 + 1) = 1)
9998oveq1d 7446 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → ((0 + 1)...(𝐾 − 1)) = (1...(𝐾 − 1)))
100 ssidd 4019 . . . . . . . . . . . 12 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (1...(𝐾 − 1)) ⊆ (1...(𝐾 − 1)))
10199, 100eqsstrd 4034 . . . . . . . . . . 11 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → ((0 + 1)...(𝐾 − 1)) ⊆ (1...(𝐾 − 1)))
102101sseld 3994 . . . . . . . . . 10 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑦 ∈ ((0 + 1)...(𝐾 − 1)) → 𝑦 ∈ (1...(𝐾 − 1))))
10396, 102jaod 859 . . . . . . . . 9 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → ((𝑦 = 0 ∨ 𝑦 ∈ ((0 + 1)...(𝐾 − 1))) → 𝑦 ∈ (1...(𝐾 − 1))))
10475, 103mpd 15 . . . . . . . 8 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → 𝑦 ∈ (1...(𝐾 − 1)))
10550, 51, 54, 104primrootlekpowne0 42087 . . . . . . 7 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑦(.g‘(𝑅s 𝑈))𝑀) ≠ (0g‘(𝑅s 𝑈)))
10649, 105eqnetrd 3006 . . . . . 6 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → (𝑁(.g‘(𝑅s 𝑈))𝑀) ≠ (0g‘(𝑅s 𝑈)))
107106neneqd 2943 . . . . 5 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ ¬ 𝐾𝑁) → ¬ (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
108107ex 412 . . . 4 ((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) → (¬ 𝐾𝑁 → ¬ (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈))))
109108con4d 115 . . 3 ((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) → ((𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) → 𝐾𝑁))
110 simp-4l 783 . . . . . 6 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ 𝐾𝑁) → 𝜑)
111 simpr 484 . . . . . 6 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ 𝐾𝑁) → 𝐾𝑁)
112110, 111jca 511 . . . . 5 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ 𝐾𝑁) → (𝜑𝐾𝑁))
113 primrootspoweq0.5 . . . . . . . . 9 (𝜑𝑁 ∈ ℤ)
114 divides 16289 . . . . . . . . 9 ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾𝑁 ↔ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁))
11511, 113, 114syl2anc 584 . . . . . . . 8 (𝜑 → (𝐾𝑁 ↔ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁))
116115biimpd 229 . . . . . . 7 (𝜑 → (𝐾𝑁 → ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁))
117116imp 406 . . . . . 6 ((𝜑𝐾𝑁) → ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁)
118 simpr 484 . . . . . . . . . . . 12 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑦 · 𝐾) = 𝑁)
119118eqcomd 2741 . . . . . . . . . . 11 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → 𝑁 = (𝑦 · 𝐾))
120119oveq1d 7446 . . . . . . . . . 10 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑁(.g‘(𝑅s 𝑈))𝑀) = ((𝑦 · 𝐾)(.g‘(𝑅s 𝑈))𝑀))
1217ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑅s 𝑈) ∈ Abel)
122 ablgrp 19818 . . . . . . . . . . . . 13 ((𝑅s 𝑈) ∈ Abel → (𝑅s 𝑈) ∈ Grp)
123121, 122syl 17 . . . . . . . . . . . 12 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑅s 𝑈) ∈ Grp)
124 simplr 769 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → 𝑦 ∈ ℤ)
12511ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → 𝐾 ∈ ℤ)
12626ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → 𝑀 ∈ (Base‘(𝑅s 𝑈)))
127124, 125, 1263jca 1127 . . . . . . . . . . . 12 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅s 𝑈))))
12829, 22mulgass 19142 . . . . . . . . . . . 12 (((𝑅s 𝑈) ∈ Grp ∧ (𝑦 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ (Base‘(𝑅s 𝑈)))) → ((𝑦 · 𝐾)(.g‘(𝑅s 𝑈))𝑀) = (𝑦(.g‘(𝑅s 𝑈))(𝐾(.g‘(𝑅s 𝑈))𝑀)))
129123, 127, 128syl2anc 584 . . . . . . . . . . 11 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → ((𝑦 · 𝐾)(.g‘(𝑅s 𝑈))𝑀) = (𝑦(.g‘(𝑅s 𝑈))(𝐾(.g‘(𝑅s 𝑈))𝑀)))
13036ad3antrrr 730 . . . . . . . . . . . . 13 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝐾(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
131130oveq2d 7447 . . . . . . . . . . . 12 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑦(.g‘(𝑅s 𝑈))(𝐾(.g‘(𝑅s 𝑈))𝑀)) = (𝑦(.g‘(𝑅s 𝑈))(0g‘(𝑅s 𝑈))))
13229, 22, 39mulgz 19133 . . . . . . . . . . . . 13 (((𝑅s 𝑈) ∈ Grp ∧ 𝑦 ∈ ℤ) → (𝑦(.g‘(𝑅s 𝑈))(0g‘(𝑅s 𝑈))) = (0g‘(𝑅s 𝑈)))
133123, 124, 132syl2anc 584 . . . . . . . . . . . 12 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑦(.g‘(𝑅s 𝑈))(0g‘(𝑅s 𝑈))) = (0g‘(𝑅s 𝑈)))
134131, 133eqtrd 2775 . . . . . . . . . . 11 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑦(.g‘(𝑅s 𝑈))(𝐾(.g‘(𝑅s 𝑈))𝑀)) = (0g‘(𝑅s 𝑈)))
135129, 134eqtrd 2775 . . . . . . . . . 10 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → ((𝑦 · 𝐾)(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
136120, 135eqtrd 2775 . . . . . . . . 9 ((((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 𝐾) = 𝑁) → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
137 nfv 1912 . . . . . . . . . . . 12 𝑦(𝑥 · 𝐾) = 𝑁
138 nfv 1912 . . . . . . . . . . . 12 𝑥(𝑦 · 𝐾) = 𝑁
139 oveq1 7438 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 · 𝐾) = (𝑦 · 𝐾))
140139eqeq1d 2737 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝑥 · 𝐾) = 𝑁 ↔ (𝑦 · 𝐾) = 𝑁))
141137, 138, 140cbvrexw 3305 . . . . . . . . . . 11 (∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁 ↔ ∃𝑦 ∈ ℤ (𝑦 · 𝐾) = 𝑁)
142141biimpi 216 . . . . . . . . . 10 (∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁 → ∃𝑦 ∈ ℤ (𝑦 · 𝐾) = 𝑁)
143142adantl 481 . . . . . . . . 9 ((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) → ∃𝑦 ∈ ℤ (𝑦 · 𝐾) = 𝑁)
144136, 143r19.29a 3160 . . . . . . . 8 ((𝜑 ∧ ∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁) → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
145144ex 412 . . . . . . 7 (𝜑 → (∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁 → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈))))
146145adantr 480 . . . . . 6 ((𝜑𝐾𝑁) → (∃𝑥 ∈ ℤ (𝑥 · 𝐾) = 𝑁 → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈))))
147117, 146mpd 15 . . . . 5 ((𝜑𝐾𝑁) → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
148112, 147syl 17 . . . 4 (((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) ∧ 𝐾𝑁) → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)))
149148ex 412 . . 3 ((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) → (𝐾𝑁 → (𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈))))
150109, 149impbid 212 . 2 ((((𝜑𝑥 ∈ ℤ) ∧ 𝑦 ∈ (0...(𝐾 − 1))) ∧ 𝑁 = ((𝑥 · 𝐾) + 𝑦)) → ((𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) ↔ 𝐾𝑁))
151113, 4remexz 42086 . 2 (𝜑 → ∃𝑥 ∈ ℤ ∃𝑦 ∈ (0...(𝐾 − 1))𝑁 = ((𝑥 · 𝐾) + 𝑦))
152150, 151r19.29vva 3214 1 (𝜑 → ((𝑁(.g‘(𝑅s 𝑈))𝑀) = (0g‘(𝑅s 𝑈)) ↔ 𝐾𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wcel 2106  wral 3059  wrex 3068  {crab 3433   class class class wbr 5148  cfv 6563  (class class class)co 7431  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158  cle 11294  cmin 11490  cn 12264  0cn0 12524  cz 12611  cuz 12876  ...cfz 13544  cdvds 16287  Basecbs 17245  s cress 17274  +gcplusg 17298  0gc0g 17486  Grpcgrp 18964  .gcmg 19098  CMndccmn 19813  Abelcabl 19814   PrimRoots cprimroots 42073
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-sup 9480  df-inf 9481  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-n0 12525  df-z 12612  df-uz 12877  df-rp 13033  df-ico 13390  df-fz 13545  df-fzo 13692  df-fl 13829  df-mod 13907  df-seq 14040  df-dvds 16288  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-0g 17488  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-submnd 18810  df-grp 18967  df-minusg 18968  df-mulg 19099  df-cmn 19815  df-abl 19816  df-primroots 42074
This theorem is referenced by:  aks6d1c6isolem3  42158
  Copyright terms: Public domain W3C validator