---

Step * 1 of Lemma rsin-radd


1. x : ℝ
2. y : ℝ
⊢ rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))
BY
{ ((Assert d(rsin(x + y))/dx = λx.rcos(x + y) on (-∞, ∞) BY
          (InstLemma `derivative-function-radd-const` [⌜λ2x.rsin(x)⌝;⌜⌜λ2x.rcos(x)⌝⌝]⋅
           THEN Auto
           THEN RWO  "-1" 0
           THEN Auto))
   THEN (Assert d(rcos(x + y))/dx = λx.-(rsin(x + y)) on (-∞, ∞) BY
               (InstLemma `derivative-function-radd-const` [⌜λ2x.rcos(x)⌝;⌜⌜λ2x.-(rsin(x))⌝⌝]⋅
                THEN Auto
                THEN RWO  "-1" 0
                THEN Auto))
   THEN (Assert d(-(rsin(x + y)))/dx = λx.-(rcos(x + y)) on (-∞, ∞) BY
               (ProveDerivative THEN Auto))
   THEN (Assert d(-(rcos(x + y)))/dx = λx.rsin(x + y) on (-∞, ∞) BY
               ((Assert d(-(rcos(x + y)))/dx = λx.-(-(rsin(x + y))) on (-∞, ∞) BY
                       (ProveDerivative THEN Auto))
                THEN DerivativeFunctionality (-1)
                THEN Auto))) }

1
1. x : ℝ
2. y : ℝ
3. d(rsin(x + y))/dx = λx.rcos(x + y) on (-∞, ∞)
4. d(rcos(x + y))/dx = λx.-(rsin(x + y)) on (-∞, ∞)
5. d(-(rsin(x + y)))/dx = λx.-(rcos(x + y)) on (-∞, ∞)
6. d(-(rcos(x + y)))/dx = λx.rsin(x + y) on (-∞, ∞)
⊢ rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  d(rsin(x  +  y))/dx  =  \mlambda{}x.rcos(x  +  y)  on  (-\minfty{},  \minfty{})  BY
                (InstLemma  `derivative-function-radd-const`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.rsin(x)\mkleeneclose{};\mkleeneopen{}\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{}\mkleeneclose{}]\mcdot{}
                  THEN  Auto
                  THEN  RWO    "-1"  0
                  THEN  Auto))
  THEN  (Assert  d(rcos(x  +  y))/dx  =  \mlambda{}x.-(rsin(x  +  y))  on  (-\minfty{},  \minfty{})  BY
                          (InstLemma  `derivative-function-radd-const`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x)\mkleeneclose{};\mkleeneopen{}\mkleeneopen{}\mlambda{}\msubtwo{}x.-(rsin(x))\mkleeneclose{}\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  RWO    "-1"  0
                            THEN  Auto))
  THEN  (Assert  d(-(rsin(x  +  y)))/dx  =  \mlambda{}x.-(rcos(x  +  y))  on  (-\minfty{},  \minfty{})  BY
                          (ProveDerivative  THEN  Auto))
  THEN  (Assert  d(-(rcos(x  +  y)))/dx  =  \mlambda{}x.rsin(x  +  y)  on  (-\minfty{},  \minfty{})  BY
                          ((Assert  d(-(rcos(x  +  y)))/dx  =  \mlambda{}x.-(-(rsin(x  +  y)))  on  (-\minfty{},  \minfty{})  BY
                                          (ProveDerivative  THEN  Auto))
                            THEN  DerivativeFunctionality  (-1)
                            THEN  Auto)))

---

Home Index