---

Step * 2 1 2 1 1 2 2 of Lemma div_unique3


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
BY
{ TACTIC:((RWO "absval_unfold2" 0 THENA Auto) THEN RepeatFor 2 (AutoSplit ⋅) THEN Auto THEN AutoSplit) }

1
1. x : ℤ
2. y : ℤ
3. z : ℤ
4. ¬(x = 0 ∈ ℤ)
5. ¬(y = 0 ∈ ℤ)
6. 0 < x
7. 0 < y
8. x < z
9. y < z
10. 0 ≤ x
11. 0 ≤ y
12. 0 < x - y
⊢ x - y < z

2
1. x : ℤ
2. y : ℤ
3. ¬0 < x - y
4. z : ℤ
5. ¬(x = 0 ∈ ℤ)
6. ¬(y = 0 ∈ ℤ)
7. 0 < x
8. 0 < y
9. x < z
10. y < z
11. 0 ≤ x
12. 0 ≤ y
⊢ -(x - y) < z

3
1. x : ℤ
2. ¬0 < x
3. y : ℤ
4. ¬0 < y
5. z : ℤ
6. 0 < x ⇒ (0 ≤ y)
7. 0 < y ⇒ (0 ≤ x)
8. ¬(x = 0 ∈ ℤ)
9. ¬(y = 0 ∈ ℤ)
10. -x < z
11. -y < z
12. 0 < x - y
⊢ x - y < z

4
1. x : ℤ
2. ¬0 < x
3. y : ℤ
4. ¬0 < x - y
5. ¬0 < y
6. z : ℤ
7. 0 < x ⇒ (0 ≤ y)
8. 0 < y ⇒ (0 ≤ x)
9. ¬(x = 0 ∈ ℤ)
10. ¬(y = 0 ∈ ℤ)
11. -x < z
12. -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)
6.  \mneg{}(y  =  0)
\mvdash{}  |x|  <  z  {}\mRightarrow{}  |y|  <  z  {}\mRightarrow{}  |x  -  y|  <  z


By

---

Latex:
TACTIC:((RWO  "absval\_unfold2"  0  THENA  Auto)  THEN  RepeatFor  2  (AutoSplit  \mcdot{})  THEN  Auto  THEN  AutoSplit)

---

Home Index