---

Step * 1 of Lemma mul-imin


1. n : ℕ
2. a : ℤ
3. b : ℤ
4. ¬((n * a) ≤ (n * b))
5. a ≤ b
⊢ (n * a) = (n * b) ∈ ℤ
BY
{ (D (-2) THEN EAuto 1) }

---

Latex:

---

Latex:

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


By

---

Latex:
(D  (-2)  THEN  EAuto  1)

---

Home Index