---

Step * 1 of Lemma sinh-radd


1. x : ℝ
2. y : ℝ
⊢ (expr(x + y) + -(expr(-(x + y)))) = (-(expr(-(x)) * expr(-(y))) + (expr(x) * expr(y)))
BY
{ ((RWO "expr-req" 0 THENA Auto) THEN (Assert -(x + y) = (-(x) + -(y)) BY Auto) THEN RWW "-1 rexp-radd" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
\mvdash{}  (expr(x  +  y)  +  -(expr(-(x  +  y))))  =  (-(expr(-(x))  *  expr(-(y)))  +  (expr(x)  *  expr(y)))


By

---

Latex:
((RWO  "expr-req"  0  THENA  Auto)
  THEN  (Assert  -(x  +  y)  =  (-(x)  +  -(y))  BY
                          Auto)
  THEN  RWW  "-1  rexp-radd"  0
  THEN  Auto)

---

Home Index