---

Step * 2 of Lemma mul-imax


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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mkleeneopen{}(n  *  b)  \mleq{}  (n  *  a)\mkleeneclose{}\mcdot{}  THEN  EAuto  1)

---

Home Index