---

Step * of Lemma rabs-difference-lower-bound

No Annotations
∀x,y,z:ℝ.  (z < |x - y| ⇐⇒ ((z + y) < x) ∨ ((z + x) < y))
BY
{ ((UnivCD THENA Auto) THEN (RWO "rabs-as-rmax" 0 THENM RWO "rmax_strict_ub<" 0) THEN Auto THEN ParallelLast) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. z < (x - y)
⊢ (z + y) < x

2
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. z < -(x - y)
⊢ (z + x) < y

3
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. (z + y) < x
⊢ z < (x - y)

4
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. (z + x) < y
⊢ z < -(x - y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}x,y,z:\mBbbR{}.    (z  <  |x  -  y|  \mLeftarrow{}{}\mRightarrow{}  ((z  +  y)  <  x)  \mvee{}  ((z  +  x)  <  y))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "rabs-as-rmax"  0  THENM  RWO  "rmax\_strict\_ub<"  0)
  THEN  Auto
  THEN  ParallelLast)

---

Home Index