---

Step * 1 1 1 of Lemma modulus-equal


1. x : ℤ
2. y : ℤ
3. m : ℕ+
4. a : ℤ
5. (x mod m) = a ∈ ℤ
6. b : ℤ
7. (y mod m) = b ∈ ℤ
⊢ ((0 ≤ a) ∧ a < m)
⇒ ((0 ≤ b) ∧ b < m)
⇒ (x = (((x ÷↓ m) * m) + a) ∈ ℤ)
⇒ (y = (((y ÷↓ m) * m) + b) ∈ ℤ)
⇒ (a = b ∈ ℤ ⇐⇒ m | (x - y))
BY
{ ((UnivCD THENA Auto) THEN RepeatFor 2 (((HypSubst' (-1) 0) THEN (Thin (-1))))) }

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

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  m  :  \mBbbN{}\msupplus{}
4.  a  :  \mBbbZ{}
5.  (x  mod  m)  =  a
6.  b  :  \mBbbZ{}
7.  (y  mod  m)  =  b
\mvdash{}  ((0  \mleq{}  a)  \mwedge{}  a  <  m)
{}\mRightarrow{}  ((0  \mleq{}  b)  \mwedge{}  b  <  m)
{}\mRightarrow{}  (x  =  (((x  \mdiv{}\mdownarrow{}  m)  *  m)  +  a))
{}\mRightarrow{}  (y  =  (((y  \mdiv{}\mdownarrow{}  m)  *  m)  +  b))
{}\mRightarrow{}  (a  =  b  \mLeftarrow{}{}\mRightarrow{}  m  |  (x  -  y))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepeatFor  2  (((HypSubst'  (-1)  0)  THEN  (Thin  (-1)))))

---

Home Index