Step
*
1
1
1
2
2
1
1
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 ∈ ℤ)
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 )
14. infinite-deriv-seq((-∞, ∞);i,x.if (i rem 4 =z 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (i rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =z 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi )
⊢ rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))
BY
{ (((InstLemma `equal-functions-by-Taylor` [⌜λ2i 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 ⌝;⌜λ2i x.if (i rem 4 =z 0)
then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (i rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =z 2)
then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi ⌝]⋅
THENM (Reduce -1 THEN Auto)
)
THEN Try (Trivial)
)
THENW Auto
) }
1
.....antecedent.....
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 )
14. infinite-deriv-seq((-∞, ∞);i,x.if (i rem 4 =z 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (i rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =z 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi )
⊢ ∀k:ℕ. ∀x,y@0:ℝ.
((x = y@0)
⇒ (if (k rem 4 =z 0) then rsin(x + y)
if (k rem 4 =z 1) then rcos(x + y)
if (k rem 4 =z 2) then -(rsin(x + y))
else -(rcos(x + y))
fi
= if (k rem 4 =z 0) then rsin(y@0 + y)
if (k rem 4 =z 1) then rcos(y@0 + y)
if (k rem 4 =z 2) then -(rsin(y@0 + y))
else -(rcos(y@0 + y))
fi ))
2
.....antecedent.....
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 )
14. infinite-deriv-seq((-∞, ∞);i,x.if (i rem 4 =z 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (i rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =z 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi )
⊢ ∀k:ℕ. ∀x,y@0:ℝ.
((x = y@0)
⇒ (if (k rem 4 =z 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (k rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (k rem 4 =z 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi
= if (k rem 4 =z 0) then (rsin(y@0) * rcos(y)) + (rcos(y@0) * rsin(y))
if (k rem 4 =z 1) then (rcos(y@0) * rcos(y)) + (-(rsin(y@0)) * rsin(y))
if (k rem 4 =z 2) then (-(rsin(y@0)) * rcos(y)) + (-(rcos(y@0)) * rsin(y))
else (-(rcos(y@0)) * rcos(y)) + (-(-(rsin(y@0))) * rsin(y))
fi ))
3
.....antecedent.....
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 )
14. infinite-deriv-seq((-∞, ∞);i,x.if (i rem 4 =z 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (i rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =z 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi )
⊢ ∀m:ℕ
∃c:ℝ
∃N:ℕ
∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .
(|if (k rem 4 =z 0) then rsin(x + y)
if (k rem 4 =z 1) then rcos(x + y)
if (k rem 4 =z 2) then -(rsin(x + y))
else -(rcos(x + y))
fi | ≤ c)
4
.....antecedent.....
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 )
14. infinite-deriv-seq((-∞, ∞);i,x.if (i rem 4 =z 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (i rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =z 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi )
⊢ ∀m:ℕ
∃c:ℝ
∃N:ℕ
∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .
(|if (k rem 4 =z 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (k rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (k rem 4 =z 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi | ≤ c)
5
.....antecedent.....
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 )
14. infinite-deriv-seq((-∞, ∞);i,x.if (i rem 4 =z 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (i rem 4 =z 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =z 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi )
⊢ ∀n:ℕ
(if (n rem 4 =z 0) then rsin(r0 + y)
if (n rem 4 =z 1) then rcos(r0 + y)
if (n rem 4 =z 2) then -(rsin(r0 + y))
else -(rcos(r0 + y))
fi
= if (n rem 4 =z 0) then (rsin(r0) * rcos(y)) + (rcos(r0) * rsin(y))
if (n rem 4 =z 1) then (rcos(r0) * rcos(y)) + (-(rsin(r0)) * rsin(y))
if (n rem 4 =z 2) then (-(rsin(r0)) * rcos(y)) + (-(rcos(r0)) * rsin(y))
else (-(rcos(r0)) * rcos(y)) + (-(-(rsin(r0))) * rsin(y))
fi )
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 )
13. 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 )
14. infinite-deriv-seq((-\minfty{}, \minfty{});i,x.if (i rem 4 =\msubz{} 0) then (rsin(x) * rcos(y)) + (rcos(x) * rsin(y))
if (i rem 4 =\msubz{} 1) then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =\msubz{} 2) then (-(rsin(x)) * rcos(y)) + (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y)) + (-(-(rsin(x))) * rsin(y))
fi )
\mvdash{} rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y)))
By
Latex:
(((InstLemma `equal-functions-by-Taylor` [\mkleeneopen{}\mlambda{}\msubtwo{}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 \mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i x.if (i rem 4 =\msubz{} 0)
then (rsin(x) * rcos(y))
+ (rcos(x) * rsin(y))
if (i rem 4 =\msubz{} 1)
then (rcos(x) * rcos(y)) + (-(rsin(x)) * rsin(y))
if (i rem 4 =\msubz{} 2)
then (-(rsin(x)) * rcos(y))
+ (-(rcos(x)) * rsin(y))
else (-(rcos(x)) * rcos(y))
+ (-(-(rsin(x))) * rsin(y))
fi \mkleeneclose{}]\mcdot{}
THENM (Reduce -1 THEN Auto)
)
THEN Try (Trivial)
)
THENW Auto
)
Home
Index