Proof of Theorem mulgmodid
| Step | Hyp | Ref
| Expression |
| 1 | | zre 12617 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℝ) |
| 2 | | nnrp 13046 |
. . . . . 6
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ+) |
| 3 | | modval 13911 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ+)
→ (𝑁 mod 𝑀) = (𝑁 − (𝑀 · (⌊‘(𝑁 / 𝑀))))) |
| 4 | 1, 2, 3 | syl2an 596 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑁 mod 𝑀) = (𝑁 − (𝑀 · (⌊‘(𝑁 / 𝑀))))) |
| 5 | 4 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → (𝑁 mod 𝑀) = (𝑁 − (𝑀 · (⌊‘(𝑁 / 𝑀))))) |
| 6 | 5 | oveq1d 7446 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 mod 𝑀) · 𝑋) = ((𝑁 − (𝑀 · (⌊‘(𝑁 / 𝑀)))) · 𝑋)) |
| 7 | | zcn 12618 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
| 8 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑁 ∈
ℂ) |
| 9 | | nnz 12634 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℤ) |
| 10 | 9 | adantl 481 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
ℤ) |
| 11 | | nnre 12273 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℝ) |
| 12 | | nnne0 12300 |
. . . . . . . . . . 11
⊢ (𝑀 ∈ ℕ → 𝑀 ≠ 0) |
| 13 | | redivcl 11986 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ 𝑀 ≠ 0) → (𝑁 / 𝑀) ∈ ℝ) |
| 14 | 1, 11, 12, 13 | syl3an 1161 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑁 / 𝑀) ∈ ℝ) |
| 15 | 14 | 3anidm23 1423 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑁 / 𝑀) ∈ ℝ) |
| 16 | 15 | flcld 13838 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) →
(⌊‘(𝑁 / 𝑀)) ∈
ℤ) |
| 17 | 10, 16 | zmulcld 12728 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑀 · (⌊‘(𝑁 / 𝑀))) ∈ ℤ) |
| 18 | 17 | zcnd 12723 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑀 · (⌊‘(𝑁 / 𝑀))) ∈ ℂ) |
| 19 | 8, 18 | negsubd 11626 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑁 + -(𝑀 · (⌊‘(𝑁 / 𝑀)))) = (𝑁 − (𝑀 · (⌊‘(𝑁 / 𝑀))))) |
| 20 | 19 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → (𝑁 + -(𝑀 · (⌊‘(𝑁 / 𝑀)))) = (𝑁 − (𝑀 · (⌊‘(𝑁 / 𝑀))))) |
| 21 | 20 | oveq1d 7446 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 + -(𝑀 · (⌊‘(𝑁 / 𝑀)))) · 𝑋) = ((𝑁 − (𝑀 · (⌊‘(𝑁 / 𝑀)))) · 𝑋)) |
| 22 | | simp1 1137 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → 𝐺 ∈ Grp) |
| 23 | | simpl 482 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑁 ∈
ℤ) |
| 24 | 23 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → 𝑁 ∈
ℤ) |
| 25 | 10 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → 𝑀 ∈
ℤ) |
| 26 | 16 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) →
(⌊‘(𝑁 / 𝑀)) ∈
ℤ) |
| 27 | 25, 26 | zmulcld 12728 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → (𝑀 · (⌊‘(𝑁 / 𝑀))) ∈ ℤ) |
| 28 | 27 | znegcld 12724 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → -(𝑀 · (⌊‘(𝑁 / 𝑀))) ∈ ℤ) |
| 29 | | simpl 482 |
. . . . 5
⊢ ((𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 ) → 𝑋 ∈ 𝐵) |
| 30 | 29 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → 𝑋 ∈ 𝐵) |
| 31 | | mulgmodid.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐺) |
| 32 | | mulgmodid.t |
. . . . 5
⊢ · =
(.g‘𝐺) |
| 33 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 34 | 31, 32, 33 | mulgdir 19124 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ -(𝑀 · (⌊‘(𝑁 / 𝑀))) ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑁 + -(𝑀 · (⌊‘(𝑁 / 𝑀)))) · 𝑋) = ((𝑁 · 𝑋)(+g‘𝐺)(-(𝑀 · (⌊‘(𝑁 / 𝑀))) · 𝑋))) |
| 35 | 22, 24, 28, 30, 34 | syl13anc 1374 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 + -(𝑀 · (⌊‘(𝑁 / 𝑀)))) · 𝑋) = ((𝑁 · 𝑋)(+g‘𝐺)(-(𝑀 · (⌊‘(𝑁 / 𝑀))) · 𝑋))) |
| 36 | 6, 21, 35 | 3eqtr2d 2783 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 mod 𝑀) · 𝑋) = ((𝑁 · 𝑋)(+g‘𝐺)(-(𝑀 · (⌊‘(𝑁 / 𝑀))) · 𝑋))) |
| 37 | | nncn 12274 |
. . . . . . . 8
⊢ (𝑀 ∈ ℕ → 𝑀 ∈
ℂ) |
| 38 | 37 | adantl 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → 𝑀 ∈
ℂ) |
| 39 | 16 | zcnd 12723 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) →
(⌊‘(𝑁 / 𝑀)) ∈
ℂ) |
| 40 | 38, 39 | mulneg2d 11717 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) → (𝑀 · -(⌊‘(𝑁 / 𝑀))) = -(𝑀 · (⌊‘(𝑁 / 𝑀)))) |
| 41 | 40 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → (𝑀 · -(⌊‘(𝑁 / 𝑀))) = -(𝑀 · (⌊‘(𝑁 / 𝑀)))) |
| 42 | 41 | oveq1d 7446 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑀 · -(⌊‘(𝑁 / 𝑀))) · 𝑋) = (-(𝑀 · (⌊‘(𝑁 / 𝑀))) · 𝑋)) |
| 43 | 15 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → (𝑁 / 𝑀) ∈ ℝ) |
| 44 | 43 | flcld 13838 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) →
(⌊‘(𝑁 / 𝑀)) ∈
ℤ) |
| 45 | 44 | znegcld 12724 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) →
-(⌊‘(𝑁 / 𝑀)) ∈
ℤ) |
| 46 | 31, 32 | mulgassr 19130 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
(-(⌊‘(𝑁 / 𝑀)) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · -(⌊‘(𝑁 / 𝑀))) · 𝑋) = (-(⌊‘(𝑁 / 𝑀)) · (𝑀 · 𝑋))) |
| 47 | 22, 45, 25, 30, 46 | syl13anc 1374 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑀 · -(⌊‘(𝑁 / 𝑀))) · 𝑋) = (-(⌊‘(𝑁 / 𝑀)) · (𝑀 · 𝑋))) |
| 48 | | oveq2 7439 |
. . . . . . 7
⊢ ((𝑀 · 𝑋) = 0 →
(-(⌊‘(𝑁 / 𝑀)) · (𝑀 · 𝑋)) = (-(⌊‘(𝑁 / 𝑀)) · 0 )) |
| 49 | 48 | adantl 481 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 ) →
(-(⌊‘(𝑁 / 𝑀)) · (𝑀 · 𝑋)) = (-(⌊‘(𝑁 / 𝑀)) · 0 )) |
| 50 | 49 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) →
(-(⌊‘(𝑁 / 𝑀)) · (𝑀 · 𝑋)) = (-(⌊‘(𝑁 / 𝑀)) · 0 )) |
| 51 | | mulgmodid.o |
. . . . . . 7
⊢ 0 =
(0g‘𝐺) |
| 52 | 31, 32, 51 | mulgz 19120 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧
-(⌊‘(𝑁 / 𝑀)) ∈ ℤ) →
(-(⌊‘(𝑁 / 𝑀)) · 0 ) = 0 ) |
| 53 | 22, 45, 52 | syl2anc 584 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) →
(-(⌊‘(𝑁 / 𝑀)) · 0 ) = 0 ) |
| 54 | 47, 50, 53 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑀 · -(⌊‘(𝑁 / 𝑀))) · 𝑋) = 0 ) |
| 55 | 42, 54 | eqtr3d 2779 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → (-(𝑀 · (⌊‘(𝑁 / 𝑀))) · 𝑋) = 0 ) |
| 56 | 55 | oveq2d 7447 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 · 𝑋)(+g‘𝐺)(-(𝑀 · (⌊‘(𝑁 / 𝑀))) · 𝑋)) = ((𝑁 · 𝑋)(+g‘𝐺) 0 )) |
| 57 | | id 22 |
. . . 4
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Grp) |
| 58 | 31, 32 | mulgcl 19109 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵) |
| 59 | 57, 23, 29, 58 | syl3an 1161 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → (𝑁 · 𝑋) ∈ 𝐵) |
| 60 | 31, 33, 51 | grprid 18986 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ (𝑁 · 𝑋) ∈ 𝐵) → ((𝑁 · 𝑋)(+g‘𝐺) 0 ) = (𝑁 · 𝑋)) |
| 61 | 22, 59, 60 | syl2anc 584 |
. 2
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 · 𝑋)(+g‘𝐺) 0 ) = (𝑁 · 𝑋)) |
| 62 | 36, 56, 61 | 3eqtrd 2781 |
1
⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 mod 𝑀) · 𝑋) = (𝑁 · 𝑋)) |