---

Step * 2 1 2 1 1 2 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:(Decide ⌜y = 0 ∈ ℤ⌝⋅ THENA Auto) }

1
1. x : ℤ
2. y : ℤ
3. z : ℤ
4. (0 < x ⇒ (0 ≤ y)) ∧ (0 < y ⇒ (0 ≤ x))
5. ¬(x = 0 ∈ ℤ)
6. y = 0 ∈ ℤ
⊢ |x| < z ⇒ |y| < z ⇒ |x - y| < z

2
1. x : ℤ
2. y : ℤ
3. z : ℤ
4. (0 < x ⇒ (0 ≤ y)) ∧ (0 < y ⇒ (0 ≤ x))
5. ¬(x = 0 ∈ ℤ)
6. ¬(y = 0 ∈ ℤ)
⊢ |x| < z ⇒ |y| < z ⇒ |x - y| < z

---

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.  \mneg{}(x  =  0)
\mvdash{}  |x|  <  z  {}\mRightarrow{}  |y|  <  z  {}\mRightarrow{}  |x  -  y|  <  z


By

---

Latex:
TACTIC:(Decide  \mkleeneopen{}y  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index