---

Step * 1 of Lemma add_reduce_eqmod


1. m : ℤ
2. x : ℤ
3. y : ℤ
4. (x + y) ≡ x mod m
⊢ y ≡ 0 mod m
BY
{ (Assert ⌜(-x) ≡ (-x) mod m⌝⋅ THENA (RelRST THEN Auto)) }

1
1. m : ℤ
2. x : ℤ
3. y : ℤ
4. (x + y) ≡ x mod m
5. (-x) ≡ (-x) mod m
⊢ y ≡ 0 mod m

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  x  :  \mBbbZ{}
3.  y  :  \mBbbZ{}
4.  (x  +  y)  \mequiv{}  x  mod  m
\mvdash{}  y  \mequiv{}  0  mod  m


By

---

Latex:
(Assert  \mkleeneopen{}(-x)  \mequiv{}  (-x)  mod  m\mkleeneclose{}\mcdot{}  THENA  (RelRST  THEN  Auto))

---

Home Index