---

Step * of Lemma rcos-radd

∀[x,y:ℝ].  (rcos(x + y) = ((rcos(x) * rcos(y)) - rsin(x) * rsin(y)))
BY
{ (Auto
   THEN ((InstLemma `derivative_unique` 
          [⌜(-∞, ∞)⌝;⌜λ2x.rsin(x + y)⌝;⌜λ2x.rcos(x + y)⌝;⌜λ2x.(rcos(x) * rcos(y)) - rsin(x) * rsin(y)⌝]⋅
          THENA Auto
          )
        THENM (D -1 With ⌜x⌝  THEN Auto)
        )
   ) }

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

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

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (rcos(x  +  y)  =  ((rcos(x)  *  rcos(y))  -  rsin(x)  *  rsin(y)))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `derivative\_unique` 
                [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rsin(x  +  y)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.rcos(x  +  y)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.(rcos(x)  *  rcos(y))  -  rsin(x)  *  rsin(y)\mkleeneclose{}
                ]\mcdot{}
                THENA  Auto
                )
            THENM  (D  -1  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)
            )
  )

---

Home Index