| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | gexcl.1 | . . . . . 6
⊢ 𝑋 = (Base‘𝐺) | 
| 2 |  | gexcl.2 | . . . . . 6
⊢ 𝐸 = (gEx‘𝐺) | 
| 3 |  | gexid.3 | . . . . . 6
⊢  · =
(.g‘𝐺) | 
| 4 |  | gexid.4 | . . . . . 6
⊢  0 =
(0g‘𝐺) | 
| 5 | 1, 2, 3, 4 | gexdvdsi 19601 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁) → (𝑁 · 𝑥) = 0 ) | 
| 6 | 5 | 3expia 1122 | . . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋) → (𝐸 ∥ 𝑁 → (𝑁 · 𝑥) = 0 )) | 
| 7 | 6 | ralrimdva 3154 | . . 3
⊢ (𝐺 ∈ Grp → (𝐸 ∥ 𝑁 → ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 )) | 
| 8 | 7 | adantr 480 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 → ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 )) | 
| 9 |  | noel 4338 | . . . . . . 7
⊢  ¬
(abs‘𝑁) ∈
∅ | 
| 10 |  | simprr 773 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
{𝑦 ∈ ℕ ∣
∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } =
∅) | 
| 11 | 10 | eleq2d 2827 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
((abs‘𝑁) ∈
{𝑦 ∈ ℕ ∣
∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } ↔ (abs‘𝑁) ∈
∅)) | 
| 12 |  | oveq1 7438 | . . . . . . . . . . . 12
⊢ (𝑦 = (abs‘𝑁) → (𝑦 · 𝑥) = ((abs‘𝑁) · 𝑥)) | 
| 13 | 12 | eqeq1d 2739 | . . . . . . . . . . 11
⊢ (𝑦 = (abs‘𝑁) → ((𝑦 · 𝑥) = 0 ↔ ((abs‘𝑁) · 𝑥) = 0 )) | 
| 14 | 13 | ralbidv 3178 | . . . . . . . . . 10
⊢ (𝑦 = (abs‘𝑁) → (∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 ↔ ∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 )) | 
| 15 | 14 | elrab 3692 | . . . . . . . . 9
⊢
((abs‘𝑁)
∈ {𝑦 ∈ ℕ
∣ ∀𝑥 ∈
𝑋 (𝑦 · 𝑥) = 0 } ↔ ((abs‘𝑁) ∈ ℕ ∧
∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 )) | 
| 16 | 11, 15 | bitr3di 286 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
((abs‘𝑁) ∈
∅ ↔ ((abs‘𝑁) ∈ ℕ ∧ ∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 ))) | 
| 17 | 16 | rbaibd 540 | . . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) ∧
∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 ) → ((abs‘𝑁) ∈ ∅ ↔
(abs‘𝑁) ∈
ℕ)) | 
| 18 | 9, 17 | mtbii 326 | . . . . . 6
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) ∧
∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 ) → ¬
(abs‘𝑁) ∈
ℕ) | 
| 19 | 18 | ex 412 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
(∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 → ¬
(abs‘𝑁) ∈
ℕ)) | 
| 20 |  | nn0abscl 15351 | . . . . . . . 8
⊢ (𝑁 ∈ ℤ →
(abs‘𝑁) ∈
ℕ0) | 
| 21 | 20 | ad2antlr 727 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
(abs‘𝑁) ∈
ℕ0) | 
| 22 |  | elnn0 12528 | . . . . . . 7
⊢
((abs‘𝑁)
∈ ℕ0 ↔ ((abs‘𝑁) ∈ ℕ ∨ (abs‘𝑁) = 0)) | 
| 23 | 21, 22 | sylib 218 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
((abs‘𝑁) ∈
ℕ ∨ (abs‘𝑁)
= 0)) | 
| 24 | 23 | ord 865 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
(¬ (abs‘𝑁) ∈
ℕ → (abs‘𝑁) = 0)) | 
| 25 | 19, 24 | syld 47 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
(∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 → (abs‘𝑁) = 0)) | 
| 26 |  | simpr 484 | . . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) ∧ (abs‘𝑁) = 𝑁) → (abs‘𝑁) = 𝑁) | 
| 27 | 26 | oveq1d 7446 | . . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) ∧ (abs‘𝑁) = 𝑁) → ((abs‘𝑁) · 𝑥) = (𝑁 · 𝑥)) | 
| 28 | 27 | eqeq1d 2739 | . . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) ∧ (abs‘𝑁) = 𝑁) → (((abs‘𝑁) · 𝑥) = 0 ↔ (𝑁 · 𝑥) = 0 )) | 
| 29 |  | oveq1 7438 | . . . . . . . . 9
⊢
((abs‘𝑁) =
-𝑁 → ((abs‘𝑁) · 𝑥) = (-𝑁 · 𝑥)) | 
| 30 | 29 | eqeq1d 2739 | . . . . . . . 8
⊢
((abs‘𝑁) =
-𝑁 →
(((abs‘𝑁) · 𝑥) = 0 ↔ (-𝑁 · 𝑥) = 0 )) | 
| 31 |  | eqid 2737 | . . . . . . . . . . . 12
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 32 | 1, 3, 31 | mulgneg 19110 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ 𝑋) → (-𝑁 · 𝑥) = ((invg‘𝐺)‘(𝑁 · 𝑥))) | 
| 33 | 32 | 3expa 1119 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → (-𝑁 · 𝑥) = ((invg‘𝐺)‘(𝑁 · 𝑥))) | 
| 34 | 4, 31 | grpinvid 19017 | . . . . . . . . . . . 12
⊢ (𝐺 ∈ Grp →
((invg‘𝐺)‘ 0 ) = 0 ) | 
| 35 | 34 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → ((invg‘𝐺)‘ 0 ) = 0 ) | 
| 36 | 35 | eqcomd 2743 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → 0 =
((invg‘𝐺)‘ 0 )) | 
| 37 | 33, 36 | eqeq12d 2753 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → ((-𝑁 · 𝑥) = 0 ↔
((invg‘𝐺)‘(𝑁 · 𝑥)) = ((invg‘𝐺)‘ 0 ))) | 
| 38 |  | simpll 767 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → 𝐺 ∈ Grp) | 
| 39 | 1, 3 | mulgcl 19109 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ 𝑋) → (𝑁 · 𝑥) ∈ 𝑋) | 
| 40 | 39 | 3expa 1119 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → (𝑁 · 𝑥) ∈ 𝑋) | 
| 41 | 1, 4 | grpidcl 18983 | . . . . . . . . . . 11
⊢ (𝐺 ∈ Grp → 0 ∈ 𝑋) | 
| 42 | 41 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → 0 ∈ 𝑋) | 
| 43 | 1, 31, 38, 40, 42 | grpinv11 19025 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → (((invg‘𝐺)‘(𝑁 · 𝑥)) = ((invg‘𝐺)‘ 0 ) ↔ (𝑁 · 𝑥) = 0 )) | 
| 44 | 37, 43 | bitrd 279 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → ((-𝑁 · 𝑥) = 0 ↔ (𝑁 · 𝑥) = 0 )) | 
| 45 | 30, 44 | sylan9bbr 510 | . . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) ∧ (abs‘𝑁) = -𝑁) → (((abs‘𝑁) · 𝑥) = 0 ↔ (𝑁 · 𝑥) = 0 )) | 
| 46 |  | zre 12617 | . . . . . . . . 9
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) | 
| 47 | 46 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → 𝑁 ∈ ℝ) | 
| 48 | 47 | absord 15454 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → ((abs‘𝑁) = 𝑁 ∨ (abs‘𝑁) = -𝑁)) | 
| 49 | 28, 45, 48 | mpjaodan 961 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝑥 ∈ 𝑋) → (((abs‘𝑁) · 𝑥) = 0 ↔ (𝑁 · 𝑥) = 0 )) | 
| 50 | 49 | ralbidva 3176 | . . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) →
(∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 ↔ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 )) | 
| 51 | 50 | adantr 480 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
(∀𝑥 ∈ 𝑋 ((abs‘𝑁) · 𝑥) = 0 ↔ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 )) | 
| 52 |  | 0dvds 16314 | . . . . . 6
⊢ (𝑁 ∈ ℤ → (0
∥ 𝑁 ↔ 𝑁 = 0)) | 
| 53 | 52 | ad2antlr 727 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) → (0
∥ 𝑁 ↔ 𝑁 = 0)) | 
| 54 |  | simprl 771 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) → 𝐸 = 0) | 
| 55 | 54 | breq1d 5153 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
(𝐸 ∥ 𝑁 ↔ 0 ∥ 𝑁)) | 
| 56 |  | zcn 12618 | . . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) | 
| 57 | 56 | ad2antlr 727 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) → 𝑁 ∈
ℂ) | 
| 58 | 57 | abs00ad 15329 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
((abs‘𝑁) = 0 ↔
𝑁 = 0)) | 
| 59 | 53, 55, 58 | 3bitr4rd 312 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
((abs‘𝑁) = 0 ↔
𝐸 ∥ 𝑁)) | 
| 60 | 25, 51, 59 | 3imtr3d 293 | . . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ (𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅)) →
(∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 → 𝐸 ∥ 𝑁)) | 
| 61 |  | elrabi 3687 | . . . 4
⊢ (𝐸 ∈ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } → 𝐸 ∈ ℕ) | 
| 62 | 46 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℝ) | 
| 63 |  | nnrp 13046 | . . . . . . . . . . . 12
⊢ (𝐸 ∈ ℕ → 𝐸 ∈
ℝ+) | 
| 64 |  | modval 13911 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝐸 ∈ ℝ+)
→ (𝑁 mod 𝐸) = (𝑁 − (𝐸 · (⌊‘(𝑁 / 𝐸))))) | 
| 65 | 62, 63, 64 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → (𝑁 mod 𝐸) = (𝑁 − (𝐸 · (⌊‘(𝑁 / 𝐸))))) | 
| 66 | 65 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → (𝑁 mod 𝐸) = (𝑁 − (𝐸 · (⌊‘(𝑁 / 𝐸))))) | 
| 67 | 66 | oveq1d 7446 | . . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → ((𝑁 mod 𝐸) · 𝑥) = ((𝑁 − (𝐸 · (⌊‘(𝑁 / 𝐸)))) · 𝑥)) | 
| 68 |  | simplll 775 | . . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → 𝐺 ∈ Grp) | 
| 69 |  | simpllr 776 | . . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → 𝑁 ∈
ℤ) | 
| 70 |  | nnz 12634 | . . . . . . . . . . . 12
⊢ (𝐸 ∈ ℕ → 𝐸 ∈
ℤ) | 
| 71 | 70 | ad2antlr 727 | . . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → 𝐸 ∈
ℤ) | 
| 72 |  | rerpdivcl 13065 | . . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝐸 ∈ ℝ+)
→ (𝑁 / 𝐸) ∈
ℝ) | 
| 73 | 62, 63, 72 | syl2an 596 | . . . . . . . . . . . . 13
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → (𝑁 / 𝐸) ∈ ℝ) | 
| 74 | 73 | flcld 13838 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) →
(⌊‘(𝑁 / 𝐸)) ∈
ℤ) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) →
(⌊‘(𝑁 / 𝐸)) ∈
ℤ) | 
| 76 | 71, 75 | zmulcld 12728 | . . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → (𝐸 · (⌊‘(𝑁 / 𝐸))) ∈ ℤ) | 
| 77 |  | simprl 771 | . . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → 𝑥 ∈ 𝑋) | 
| 78 |  | eqid 2737 | . . . . . . . . . . 11
⊢
(-g‘𝐺) = (-g‘𝐺) | 
| 79 | 1, 3, 78 | mulgsubdir 19132 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ (𝐸 · (⌊‘(𝑁 / 𝐸))) ∈ ℤ ∧ 𝑥 ∈ 𝑋)) → ((𝑁 − (𝐸 · (⌊‘(𝑁 / 𝐸)))) · 𝑥) = ((𝑁 · 𝑥)(-g‘𝐺)((𝐸 · (⌊‘(𝑁 / 𝐸))) · 𝑥))) | 
| 80 | 68, 69, 76, 77, 79 | syl13anc 1374 | . . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → ((𝑁 − (𝐸 · (⌊‘(𝑁 / 𝐸)))) · 𝑥) = ((𝑁 · 𝑥)(-g‘𝐺)((𝐸 · (⌊‘(𝑁 / 𝐸))) · 𝑥))) | 
| 81 |  | simprr 773 | . . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → (𝑁 · 𝑥) = 0 ) | 
| 82 |  | dvdsmul1 16315 | . . . . . . . . . . . . 13
⊢ ((𝐸 ∈ ℤ ∧
(⌊‘(𝑁 / 𝐸)) ∈ ℤ) → 𝐸 ∥ (𝐸 · (⌊‘(𝑁 / 𝐸)))) | 
| 83 | 71, 75, 82 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → 𝐸 ∥ (𝐸 · (⌊‘(𝑁 / 𝐸)))) | 
| 84 | 1, 2, 3, 4 | gexdvdsi 19601 | . . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐸 ∥ (𝐸 · (⌊‘(𝑁 / 𝐸)))) → ((𝐸 · (⌊‘(𝑁 / 𝐸))) · 𝑥) = 0 ) | 
| 85 | 68, 77, 83, 84 | syl3anc 1373 | . . . . . . . . . . 11
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → ((𝐸 · (⌊‘(𝑁 / 𝐸))) · 𝑥) = 0 ) | 
| 86 | 81, 85 | oveq12d 7449 | . . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → ((𝑁 · 𝑥)(-g‘𝐺)((𝐸 · (⌊‘(𝑁 / 𝐸))) · 𝑥)) = ( 0 (-g‘𝐺) 0 )) | 
| 87 |  | simpll 767 | . . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → 𝐺 ∈ Grp) | 
| 88 | 1, 4, 78 | grpsubid 19042 | . . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 0 ∈ 𝑋) → ( 0 (-g‘𝐺) 0 ) = 0 ) | 
| 89 | 87, 41, 88 | syl2anc2 585 | . . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → ( 0
(-g‘𝐺)
0 ) =
0
) | 
| 90 | 89 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → ( 0
(-g‘𝐺)
0 ) =
0
) | 
| 91 | 86, 90 | eqtrd 2777 | . . . . . . . . 9
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → ((𝑁 · 𝑥)(-g‘𝐺)((𝐸 · (⌊‘(𝑁 / 𝐸))) · 𝑥)) = 0 ) | 
| 92 | 67, 80, 91 | 3eqtrd 2781 | . . . . . . . 8
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ (𝑥 ∈ 𝑋 ∧ (𝑁 · 𝑥) = 0 )) → ((𝑁 mod 𝐸) · 𝑥) = 0 ) | 
| 93 | 92 | expr 456 | . . . . . . 7
⊢ ((((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) ∧ 𝑥 ∈ 𝑋) → ((𝑁 · 𝑥) = 0 → ((𝑁 mod 𝐸) · 𝑥) = 0 )) | 
| 94 | 93 | ralimdva 3167 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) →
(∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 → ∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 )) | 
| 95 |  | modlt 13920 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 𝐸 ∈ ℝ+)
→ (𝑁 mod 𝐸) < 𝐸) | 
| 96 | 62, 63, 95 | syl2an 596 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → (𝑁 mod 𝐸) < 𝐸) | 
| 97 |  | zmodcl 13931 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℤ ∧ 𝐸 ∈ ℕ) → (𝑁 mod 𝐸) ∈
ℕ0) | 
| 98 | 97 | adantll 714 | . . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → (𝑁 mod 𝐸) ∈
ℕ0) | 
| 99 | 98 | nn0red 12588 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → (𝑁 mod 𝐸) ∈ ℝ) | 
| 100 |  | nnre 12273 | . . . . . . . . . 10
⊢ (𝐸 ∈ ℕ → 𝐸 ∈
ℝ) | 
| 101 | 100 | adantl 481 | . . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → 𝐸 ∈
ℝ) | 
| 102 | 99, 101 | ltnled 11408 | . . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → ((𝑁 mod 𝐸) < 𝐸 ↔ ¬ 𝐸 ≤ (𝑁 mod 𝐸))) | 
| 103 | 96, 102 | mpbid 232 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → ¬
𝐸 ≤ (𝑁 mod 𝐸)) | 
| 104 | 1, 2, 3, 4 | gexlem2 19600 | . . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝑁 mod 𝐸) ∈ ℕ ∧ ∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 ) → 𝐸 ∈ (1...(𝑁 mod 𝐸))) | 
| 105 |  | elfzle2 13568 | . . . . . . . . . . . . 13
⊢ (𝐸 ∈ (1...(𝑁 mod 𝐸)) → 𝐸 ≤ (𝑁 mod 𝐸)) | 
| 106 | 104, 105 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑁 mod 𝐸) ∈ ℕ ∧ ∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 ) → 𝐸 ≤ (𝑁 mod 𝐸)) | 
| 107 | 106 | 3expia 1122 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ (𝑁 mod 𝐸) ∈ ℕ) → (∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 → 𝐸 ≤ (𝑁 mod 𝐸))) | 
| 108 | 107 | impancom 451 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 ) → ((𝑁 mod 𝐸) ∈ ℕ → 𝐸 ≤ (𝑁 mod 𝐸))) | 
| 109 | 108 | con3d 152 | . . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 ) → (¬ 𝐸 ≤ (𝑁 mod 𝐸) → ¬ (𝑁 mod 𝐸) ∈ ℕ)) | 
| 110 | 109 | ex 412 | . . . . . . . 8
⊢ (𝐺 ∈ Grp →
(∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 → (¬ 𝐸 ≤ (𝑁 mod 𝐸) → ¬ (𝑁 mod 𝐸) ∈ ℕ))) | 
| 111 | 110 | ad2antrr 726 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) →
(∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 → (¬ 𝐸 ≤ (𝑁 mod 𝐸) → ¬ (𝑁 mod 𝐸) ∈ ℕ))) | 
| 112 | 103, 111 | mpid 44 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) →
(∀𝑥 ∈ 𝑋 ((𝑁 mod 𝐸) · 𝑥) = 0 → ¬ (𝑁 mod 𝐸) ∈ ℕ)) | 
| 113 |  | elnn0 12528 | . . . . . . . 8
⊢ ((𝑁 mod 𝐸) ∈ ℕ0 ↔ ((𝑁 mod 𝐸) ∈ ℕ ∨ (𝑁 mod 𝐸) = 0)) | 
| 114 | 98, 113 | sylib 218 | . . . . . . 7
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → ((𝑁 mod 𝐸) ∈ ℕ ∨ (𝑁 mod 𝐸) = 0)) | 
| 115 | 114 | ord 865 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → (¬
(𝑁 mod 𝐸) ∈ ℕ → (𝑁 mod 𝐸) = 0)) | 
| 116 | 94, 112, 115 | 3syld 60 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) →
(∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 → (𝑁 mod 𝐸) = 0)) | 
| 117 |  | simpr 484 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → 𝐸 ∈
ℕ) | 
| 118 |  | simplr 769 | . . . . . 6
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → 𝑁 ∈
ℤ) | 
| 119 |  | dvdsval3 16294 | . . . . . 6
⊢ ((𝐸 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 ↔ (𝑁 mod 𝐸) = 0)) | 
| 120 | 117, 118,
119 | syl2anc 584 | . . . . 5
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) → (𝐸 ∥ 𝑁 ↔ (𝑁 mod 𝐸) = 0)) | 
| 121 | 116, 120 | sylibrd 259 | . . . 4
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ ℕ) →
(∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 → 𝐸 ∥ 𝑁)) | 
| 122 | 61, 121 | sylan2 593 | . . 3
⊢ (((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) ∧ 𝐸 ∈ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 }) → (∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 → 𝐸 ∥ 𝑁)) | 
| 123 |  | eqid 2737 | . . . . 5
⊢ {𝑦 ∈ ℕ ∣
∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } | 
| 124 | 1, 3, 4, 2, 123 | gexlem1 19597 | . . . 4
⊢ (𝐺 ∈ Grp → ((𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅) ∨ 𝐸 ∈ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 })) | 
| 125 | 124 | adantr 480 | . . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → ((𝐸 = 0 ∧ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } = ∅) ∨ 𝐸 ∈ {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 })) | 
| 126 | 60, 122, 125 | mpjaodan 961 | . 2
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) →
(∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 → 𝐸 ∥ 𝑁)) | 
| 127 | 8, 126 | impbid 212 | 1
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 ↔ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 )) |