[STATEMENT]
lemma d_sinpoly_cospoly:
    "(sinpoly (Suc n) has_field_derivative cospoly n x) (at x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x)
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (sinpoly (Suc 0) has_real_derivative cospoly 0 x) (at x)
 2. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:


goal (2 subgoals):
 1. (sinpoly (Suc 0) has_real_derivative cospoly 0 x) (at x)
 2. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinpoly (Suc 0) has_real_derivative cospoly 0 x) (at x)
[PROOF STEP]
by (simp add: sinpoly_def cospoly_def)
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc 0) has_real_derivative cospoly 0 x) (at x)

goal (1 subgoal):
 1. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc n) has_real_derivative cospoly n x) (at x)

goal (1 subgoal):
 1. \<And>n. (sinpoly (Suc n) has_real_derivative cospoly n x) (at x) \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
proof (cases "n=0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
 2. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
 2. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
by (simp add: sinpoly_def sin_coeff_def cospoly_def)
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 0

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> 0
[PROOF STEP]
have xn: "x ^ (n - Suc 0) * x = x ^ n"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> 0

goal (1 subgoal):
 1. x ^ (n - Suc 0) * x = x ^ n
[PROOF STEP]
by (metis Suc_pred mult.commute not_gr0 power_Suc)
[PROOF STATE]
proof (state)
this:
x ^ (n - Suc 0) * x = x ^ n

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
using Suc False
[PROOF STATE]
proof (prove)
using this:
(sinpoly (Suc n) has_real_derivative cospoly n x) (at x)
n \<noteq> 0

goal (1 subgoal):
 1. (sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)
[PROOF STEP]
apply (simp add: sinpoly_Suc [of "Suc n"] cospoly_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sinpoly (Suc n) has_real_derivative (\<Sum>k<n. cos_coeff k * x ^ k)) (at x); 0 < n\<rbrakk> \<Longrightarrow> ((\<lambda>a. sinpoly (Suc n) a + sin_coeff (Suc n) * (a * a ^ n)) has_real_derivative (\<Sum>k<n. cos_coeff k * x ^ k) + cos_coeff n * x ^ n) (at x)
[PROOF STEP]
apply (intro derivative_eq_intros | simp)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sinpoly (Suc n) has_real_derivative (\<Sum>k<n. cos_coeff k * x ^ k)) (at x); 0 < n\<rbrakk> \<Longrightarrow> (x ^ n + real n * x ^ (n - Suc 0) * x) * sin_coeff (Suc n) = cos_coeff n * x ^ n
[PROOF STEP]
apply (simp add: xn mult.assoc sin_coeff_def cos_coeff_def divide_simps del: fact_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(sinpoly (Suc n) has_real_derivative (\<Sum>k<n. (if even k then (- 1) ^ (k div 2) / fact k else 0) * x ^ k)) (at x); 0 < n\<rbrakk> \<Longrightarrow> even n \<longrightarrow> (x ^ n + real n * x ^ n) * fact n = x ^ n * fact (Suc n)
[PROOF STEP]
apply (simp add: algebra_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(sinpoly (Suc (Suc n)) has_real_derivative cospoly (Suc n) x) (at x)

goal:
No subgoals!
[PROOF STEP]
qed