---

Step * of Lemma rneq-radd

∀x,y,a,b:ℝ.  (x + y ≠ a + b ⇒ (x ≠ a ∨ y ≠ b))
BY
{ (RWO "rneq-iff-rabs" 0 THEN Auto) }

1
1. x : ℝ
2. y : ℝ
3. a : ℝ
4. b : ℝ
5. r0 < |(x + y) - a + b|
⊢ (r0 < |x - a|) ∨ (r0 < |y - b|)

---

Latex:

---

Latex:
\mforall{}x,y,a,b:\mBbbR{}.    (x  +  y  \mneq{}  a  +  b  {}\mRightarrow{}  (x  \mneq{}  a  \mvee{}  y  \mneq{}  b))


By

---

Latex:
(RWO  "rneq-iff-rabs"  0  THEN  Auto)

---

Home Index