---

Step * 1 1 of Lemma cosh2-sinh2


1. x : ℝ
⊢ (((expr(x) + expr(-(x))/r(2)) * (expr(x) + expr(-(x))/r(2))) - (expr(x) - expr(-(x))/r(2))
* (expr(x) - expr(-(x))/r(2)))
= r1
BY
{ ((Assert r0 < r(2) BY
          Auto)
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜expr(x)⌝;⌜expr(-(x))⌝;⌜r(2)⌝]⋅
   THEN (D 0 THENA Auto)) }

1
1. x : ℝ
2. v : {y:ℝ| y = e^x} 
3. expr(x) = v ∈ {y:ℝ| y = e^x} 
4. v1 : {y:ℝ| y = e^-(x)} 
5. expr(-(x)) = v1 ∈ {y:ℝ| y = e^-(x)} 
6. v2 : ℝ
7. r(2) = v2 ∈ ℝ
8. r0 < v2
⊢ (((v + v1/v2) * (v + v1/v2)) - (v - v1/v2) * (v - v1/v2)) = r1

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  r0  <  r(2)  BY
                Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}expr(x)\mkleeneclose{};\mkleeneopen{}expr(-(x))\mkleeneclose{};\mkleeneopen{}r(2)\mkleeneclose{}]\mcdot{}
  THEN  (D  0  THENA  Auto))

---

Home Index