---

Step * of Lemma rminus_functionality

∀[x,y:ℝ].  -(x) = -(y) supposing x = y
BY
{ (Auto THEN RepeatFor 2 (ParallelLast) THEN (RWO "absval_sym" 0 THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. ∀n:ℕ+. (|(x n) - y n| ≤ 4)
4. n : ℕ+
5. |(x n) - y n| ≤ 4
⊢ |-((-(x) n) - -(y) n)| ≤ 4

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    -(x)  =  -(y)  supposing  x  =  y


By

---

Latex:
(Auto  THEN  RepeatFor  2  (ParallelLast)  THEN  (RWO  "absval\_sym"  0  THENA  Auto))

---

Home Index