---

Step * 1 1 1 2 2 of Lemma rsin-radd


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 (-∞, ∞)
7. d((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))/dx = λx.(rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y)) on (-∞, ∞)
8. d((rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y)))/dx = λx.(-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y)) on (-∞, ∞)
9. d((-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y)))/dx = λx.(-(rcos(x)) * rcos(y))
+ (-(-(rsin(x))) * rsin(y)) on (-∞, ∞)
10. d((-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y)))/dx = λx.(rsin(x) * rcos(y)) + (rcos(x) * rsin(y)) on (-∞, ∞)
11. (rsin(r0 + y) = ((rsin(r0) * rcos(y)) + (rcos(r0) * rsin(y))))
∧ (rcos(r0 + y) = ((rcos(r0) * rcos(y)) + (-(rsin(r0)) * rsin(y))))
∧ (-(rsin(r0 + y)) = ((-(rsin(r0)) * rcos(y)) + (-(rcos(r0)) * rsin(y))))
∧ (-(rcos(r0 + y)) = ((-(rcos(r0)) * rcos(y)) + (-(-(rsin(r0))) * rsin(y))))
12. ∀i:ℕ+. ((i rem 4) = if (i - 1 rem 4 =z 3) then 0 else 1 + (i - 1 rem 4) fi  ∈ ℤ)
⊢ rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))
BY
{ (Assert infinite-deriv-seq((-∞, ∞);i,x.if (i rem 4 =z 0) then rsin(x + y)
         if (i rem 4 =z 1) then rcos(x + y)
         if (i rem 4 =z 2) then -(rsin(x + y))
         else -(rcos(x + y))
         fi ) BY
         (((D 0 THENA Auto) THEN (Subst' i + 1 rem 4 ~ if (i rem 4 =z 3) then 0 else 1 + (i rem 4) fi  0 THENA Auto))
          THEN (InstLemma `rem_bounds_1` [⌜i⌝;⌜4⌝]⋅ THENA Auto)
          THEN (GenConcl ⌜(i rem 4) = k ∈ ℕ4⌝⋅ THENA Auto)
          THEN IntSegCases(-2)
          THEN Reduce 0
          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 (-∞, ∞)
7. d((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))/dx = λx.(rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y)) on (-∞, ∞)
8. d((rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y)))/dx = λx.(-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y)) on (-∞, ∞)
9. d((-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y)))/dx = λx.(-(rcos(x)) * rcos(y))
+ (-(-(rsin(x))) * rsin(y)) on (-∞, ∞)
10. d((-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y)))/dx = λx.(rsin(x) * rcos(y)) + (rcos(x) * rsin(y)) on (-∞, ∞)
11. (rsin(r0 + y) = ((rsin(r0) * rcos(y)) + (rcos(r0) * rsin(y))))
∧ (rcos(r0 + y) = ((rcos(r0) * rcos(y)) + (-(rsin(r0)) * rsin(y))))
∧ (-(rsin(r0 + y)) = ((-(rsin(r0)) * rcos(y)) + (-(rcos(r0)) * rsin(y))))
∧ (-(rcos(r0 + y)) = ((-(rcos(r0)) * rcos(y)) + (-(-(rsin(r0))) * rsin(y))))
12. ∀i:ℕ+. ((i rem 4) = if (i - 1 rem 4 =z 3) then 0 else 1 + (i - 1 rem 4) fi  ∈ ℤ)
13. infinite-deriv-seq((-∞, ∞);i,x.if (i rem 4 =z 0) then rsin(x + y)
if (i rem 4 =z 1) then rcos(x + y)
if (i rem 4 =z 2) then -(rsin(x + y))
else -(rcos(x + y))
fi )
⊢ rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  y  :  \mBbbR{}
3.  d(rsin(x  +  y))/dx  =  \mlambda{}x.rcos(x  +  y)  on  (-\minfty{},  \minfty{})
4.  d(rcos(x  +  y))/dx  =  \mlambda{}x.-(rsin(x  +  y))  on  (-\minfty{},  \minfty{})
5.  d(-(rsin(x  +  y)))/dx  =  \mlambda{}x.-(rcos(x  +  y))  on  (-\minfty{},  \minfty{})
6.  d(-(rcos(x  +  y)))/dx  =  \mlambda{}x.rsin(x  +  y)  on  (-\minfty{},  \minfty{})
7.  d((rsin(x)  *  rcos(y))  +  (rcos(x)  *  rsin(y)))/dx  =  \mlambda{}x.(rcos(x)  *  rcos(y))
+  (-(rsin(x))  *  rsin(y))  on  (-\minfty{},  \minfty{})
8.  d((rcos(x)  *  rcos(y))  +  (-(rsin(x))  *  rsin(y)))/dx  =  \mlambda{}x.(-(rsin(x))  *  rcos(y))
+  (-(rcos(x))  *  rsin(y))  on  (-\minfty{},  \minfty{})
9.  d((-(rsin(x))  *  rcos(y))  +  (-(rcos(x))  *  rsin(y)))/dx  =  \mlambda{}x.(-(rcos(x))  *  rcos(y))
+  (-(-(rsin(x)))  *  rsin(y))  on  (-\minfty{},  \minfty{})
10.  d((-(rcos(x))  *  rcos(y))  +  (-(-(rsin(x)))  *  rsin(y)))/dx  =  \mlambda{}x.(rsin(x)  *  rcos(y))
+  (rcos(x)  *  rsin(y))  on  (-\minfty{},  \minfty{})
11.  (rsin(r0  +  y)  =  ((rsin(r0)  *  rcos(y))  +  (rcos(r0)  *  rsin(y))))
\mwedge{}  (rcos(r0  +  y)  =  ((rcos(r0)  *  rcos(y))  +  (-(rsin(r0))  *  rsin(y))))
\mwedge{}  (-(rsin(r0  +  y))  =  ((-(rsin(r0))  *  rcos(y))  +  (-(rcos(r0))  *  rsin(y))))
\mwedge{}  (-(rcos(r0  +  y))  =  ((-(rcos(r0))  *  rcos(y))  +  (-(-(rsin(r0)))  *  rsin(y))))
12.  \mforall{}i:\mBbbN{}\msupplus{}.  ((i  rem  4)  =  if  (i  -  1  rem  4  =\msubz{}  3)  then  0  else  1  +  (i  -  1  rem  4)  fi  )
\mvdash{}  rsin(x  +  y)  =  ((rsin(x)  *  rcos(y))  +  (rcos(x)  *  rsin(y)))


By

---

Latex:
(Assert  infinite-deriv-seq((-\minfty{},  \minfty{});i,x.if  (i  rem  4  =\msubz{}  0)  then  rsin(x  +  y)
              if  (i  rem  4  =\msubz{}  1)  then  rcos(x  +  y)
              if  (i  rem  4  =\msubz{}  2)  then  -(rsin(x  +  y))
              else  -(rcos(x  +  y))
              fi  )  BY
              (((D  0  THENA  Auto)
                  THEN  (Subst'  i  +  1  rem  4  \msim{}  if  (i  rem  4  =\msubz{}  3)  then  0  else  1  +  (i  rem  4)  fi    0  THENA  Auto)
                  )
                THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}4\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (GenConcl  \mkleeneopen{}(i  rem  4)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  IntSegCases(-2)
                THEN  Reduce  0
                THEN  Auto))

---

Home Index