---

Step * 1 2 2 2 2 2 1 1 1 of Lemma rmul-is-negative1


1. n : ℕ+
2. N : {4...}
3. z : {-16..17-}
⊢ (z ÷ 2 * (2 * N) * n ÷ 2 * N) + 4 < 2 * n * 0 ⇒ False
BY
{ Auto }

1
1. n : ℕ+
2. N : {4...}
3. z : {-16..17-}
4. (z ÷ 2 * (2 * N) * n ÷ 2 * N) + 4 < 2 * n * 0
⊢ False

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  N  :  \{4...\}
3.  z  :  \{-16..17\msupminus{}\}
\mvdash{}  (z  \mdiv{}  2  *  (2  *  N)  *  n  \mdiv{}  2  *  N)  +  4  <  2  *  n  *  0  {}\mRightarrow{}  False


By

---

Latex:
Auto

---

Home Index