---

Step * 1 1 of Lemma sqeq-copath5


1. n : Base
2. m : Base
3. (((m + 1) + (-n)) + (-1))↓
4. (m + 1) + (-n) ∈ ℤ
5. -1 ∈ ℤ
6. ((m + 1) + (-n))↓
7. m + 1 ∈ ℤ
8. -n ∈ ℤ
9. (m + 1)↓
10. m ∈ ℤ
11. 1 ∈ ℤ
12. (-n)↓
13. n ∈ ℤ
⊢ ((m + 1) + (-n)) + (-1) ≤ (m + (-(n + (-1)))) + (-1)
BY
{ (Subst ⌜(((m + 1) + (-n)) + (-1)) = ((m + (-(n + (-1)))) + (-1)) ∈ ℤ⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  Base
2.  m  :  Base
3.  (((m  +  1)  +  (-n))  +  (-1))\mdownarrow{}
4.  (m  +  1)  +  (-n)  \mmember{}  \mBbbZ{}
5.  -1  \mmember{}  \mBbbZ{}
6.  ((m  +  1)  +  (-n))\mdownarrow{}
7.  m  +  1  \mmember{}  \mBbbZ{}
8.  -n  \mmember{}  \mBbbZ{}
9.  (m  +  1)\mdownarrow{}
10.  m  \mmember{}  \mBbbZ{}
11.  1  \mmember{}  \mBbbZ{}
12.  (-n)\mdownarrow{}
13.  n  \mmember{}  \mBbbZ{}
\mvdash{}  ((m  +  1)  +  (-n))  +  (-1)  \mleq{}  (m  +  (-(n  +  (-1))))  +  (-1)


By

---

Latex:
(Subst  \mkleeneopen{}(((m  +  1)  +  (-n))  +  (-1))  =  ((m  +  (-(n  +  (-1))))  +  (-1))\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index