---

Step * 1 1 of Lemma modulus-equal


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)
BY
{ (RepeatFor 4 ((MoveToConcl (-1)))
   THEN (GenConcl ⌜(x mod m) = a ∈ ℤ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜(y mod m) = b ∈ ℤ⌝⋅ THENA Auto)) }

1
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))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  4  ((MoveToConcl  (-1)))
  THEN  (GenConcl  \mkleeneopen{}(x  mod  m)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(y  mod  m)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index