---

Step * 2 1 2 1 1 1 of Lemma div_unique3


1. x : ℤ
2. y : ℤ
3. z : ℤ
4. (0 < x ⇒ (0 ≤ y)) ∧ (0 < y ⇒ (0 ≤ x))
5. x = 0 ∈ ℤ
⊢ |x| < z ⇒ |y| < z ⇒ |x - y| < z
BY
{ TACTIC:(HypSubst' (-1) 0 THEN Subst' |0 - y| ~ |y| 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}
2.  y  :  \mBbbZ{}
3.  z  :  \mBbbZ{}
4.  (0  <  x  {}\mRightarrow{}  (0  \mleq{}  y))  \mwedge{}  (0  <  y  {}\mRightarrow{}  (0  \mleq{}  x))
5.  x  =  0
\mvdash{}  |x|  <  z  {}\mRightarrow{}  |y|  <  z  {}\mRightarrow{}  |x  -  y|  <  z


By

---

Latex:
TACTIC:(HypSubst'  (-1)  0  THEN  Subst'  |0  -  y|  \msim{}  |y|  0  THEN  Auto)

---

Home Index