---

Step * 1 2 of Lemma rmin-int


1. a : ℤ
2. b : ℤ
3. n : ℕ+
4. ¬((2 * n * a) ≤ (2 * n * b))
5. a ≤ b
⊢ (2 * n * b) = (2 * n * a) ∈ ℤ
BY
{ (Mul ⌜2 * n⌝ (-1)⋅ THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  n  :  \mBbbN{}\msupplus{}
4.  \mneg{}((2  *  n  *  a)  \mleq{}  (2  *  n  *  b))
5.  a  \mleq{}  b
\mvdash{}  (2  *  n  *  b)  =  (2  *  n  *  a)


By

---

Latex:
(Mul  \mkleeneopen{}2  *  n\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto')\mcdot{}

---

Home Index