---

Step * 2 of Lemma rcos-radd

.....antecedent..... 
1. x : ℝ
2. y : ℝ
⊢ d(rsin(x + y))/dx = λx.(rcos(x) * rcos(y)) - rsin(x) * rsin(y) on (-∞, ∞)
BY
{ Assert ⌜d((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))/dx = λx.(rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y)) on (-∞, ∞)⌝
⋅ }

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

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

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
\mvdash{}  d(rsin(x  +  y))/dx  =  \mlambda{}x.(rcos(x)  *  rcos(y))  -  rsin(x)  *  rsin(y)  on  (-\minfty{},  \minfty{})


By

---

Latex:
Assert  \mkleeneopen{}d((rsin(x)  *  rcos(y))  +  (rcos(x)  *  rsin(y)))/dx  =  \mlambda{}x.(rcos(x)  *  rcos(y))
                +  (-(rsin(x))  *  rsin(y))  on  (-\minfty{},  \minfty{})\mkleeneclose{}\mcdot{}

---

Home Index