---

Step * 1 of Lemma modulus-equal


1. x : ℤ
2. y : ℤ
3. m : ℕ+
⊢ (x mod m) = (y mod m) ∈ ℤ ⇐⇒ m | (x - y)
BY
{ (((InstLemma `mod_bounds` [⌜x⌝; ⌜m⌝])⋅ THENA Auto)
   THEN ((InstLemma `mod_bounds` [⌜y⌝; ⌜m⌝])⋅ THENA Auto)
   THEN ((InstLemma `div_floor_mod_sum` [⌜x⌝; ⌜m⌝])⋅ THENA Auto)
   THEN ((InstLemma `div_floor_mod_sum` [⌜y⌝; ⌜m⌝])⋅ THENA Auto)) }

1
1. x : ℤ
2. y : ℤ
3. m : ℕ+
4. (0 ≤ (x mod m)) ∧ x mod m < m
5. (0 ≤ (y mod m)) ∧ y mod m < m
6. x = (((x ÷↓ m) * m) + (x mod m)) ∈ ℤ
7. y = (((y ÷↓ m) * m) + (y mod m)) ∈ ℤ
⊢ (x mod m) = (y mod m) ∈ ℤ ⇐⇒ m | (x - y)

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  (x  mod  m)  =  (y  mod  m)  \mLeftarrow{}{}\mRightarrow{}  m  |  (x  -  y)


By

---

Latex:
(((InstLemma  `mod\_bounds`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `mod\_bounds`  [\mkleeneopen{}y\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `div\_floor\_mod\_sum`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `div\_floor\_mod\_sum`  [\mkleeneopen{}y\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index