[GOAL]
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) (cos z)
[PROOFSTEP]
rw [Complex.cos, Complex.exp_eq_exp_ℂ]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
have := ((expSeries_div_hasSum_exp ℂ (z * Complex.I)).add (expSeries_div_hasSum_exp ℂ (-z * Complex.I))).div_const 2
[GOAL]
z : ℂ
this :
  HasSum (fun i => ((z * I) ^ i / ↑i ! + (-z * I) ^ i / ↑i !) / 2) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
[GOAL]
z : ℂ
this :
  HasSum ((fun i => ((z * I) ^ i / ↑i ! + (-z * I) ^ i / ↑i !) / 2) ∘ ↑(Nat.divModEquiv 2).symm)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (x.fst * 2 + ↑x.snd) / ↑(x.fst * 2 + ↑x.snd)! +
          (-z * I) ^ (x.fst * 2 + ↑x.snd) / ↑(x.fst * 2 + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
simp_rw [← mul_comm 2 _] at this 
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
[PROOFSTEP]
refine' this.prod_fiberwise fun k => _
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
k : ℕ
⊢ HasSum
    (fun c =>
      ((z * I) ^ (2 * (k, c).fst + ↑(k, c).snd) / ↑(2 * (k, c).fst + ↑(k, c).snd)! +
          (-z * I) ^ (2 * (k, c).fst + ↑(k, c).snd) / ↑(2 * (k, c).fst + ↑(k, c).snd)!) /
        2)
    ((z * I) ^ (2 * k) / ↑(2 * k)!)
[PROOFSTEP]
dsimp only
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
k : ℕ
⊢ HasSum (fun c => ((z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)! + (-z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)!) / 2)
    ((z * I) ^ (2 * k) / ↑(2 * k)!)
[PROOFSTEP]
convert hasSum_fintype (_ : Fin 2 → ℂ) using 1
[GOAL]
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    Finset.sum Finset.univ fun b =>
      ((z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)! + (-z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)!) / 2
[PROOFSTEP]
rw [Fin.sum_univ_two]
[GOAL]
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! +
          (-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) /
        2)
    ((_root_.exp ℂ (z * I) + _root_.exp ℂ (-z * I)) / 2)
k : ℕ
⊢ (z * I) ^ (2 * k) / ↑(2 * k)! =
    ((z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)! + (-z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)!) / 2 +
      ((z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)! + (-z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)!) / 2
[PROOFSTEP]
simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ', pow_mul, mul_pow, neg_sq, ← two_mul, neg_mul, mul_neg, neg_div,
  add_right_neg, zero_div, add_zero, mul_div_cancel_left _ (two_ne_zero : (2 : ℂ) ≠ 0)]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) (sin z)
[PROOFSTEP]
rw [Complex.sin, Complex.exp_eq_exp_ℂ]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
have :=
  (((expSeries_div_hasSum_exp ℂ (-z * Complex.I)).sub (expSeries_div_hasSum_exp ℂ (z * Complex.I))).mul_right
        Complex.I).div_const
    2
[GOAL]
z : ℂ
this :
  HasSum (fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
replace := (Nat.divModEquiv 2).symm.hasSum_iff.mpr this
[GOAL]
z : ℂ
this :
  HasSum ((fun i => ((-z * I) ^ i / ↑i ! - (z * I) ^ i / ↑i !) * I / 2) ∘ ↑(Nat.divModEquiv 2).symm)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
dsimp [Function.comp] at this 
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (x.fst * 2 + ↑x.snd) / ↑(x.fst * 2 + ↑x.snd)! -
            (z * I) ^ (x.fst * 2 + ↑x.snd) / ↑(x.fst * 2 + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
simp_rw [← mul_comm 2 _] at this 
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
⊢ HasSum (fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I) ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
[PROOFSTEP]
refine' this.prod_fiberwise fun k => _
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
k : ℕ
⊢ HasSum
    (fun c =>
      ((-z * I) ^ (2 * (k, c).fst + ↑(k, c).snd) / ↑(2 * (k, c).fst + ↑(k, c).snd)! -
            (z * I) ^ (2 * (k, c).fst + ↑(k, c).snd) / ↑(2 * (k, c).fst + ↑(k, c).snd)!) *
          I /
        2)
    ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I)
[PROOFSTEP]
dsimp only
[GOAL]
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
k : ℕ
⊢ HasSum (fun c => ((-z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)! - (z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)!) * I / 2)
    ((z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I)
[PROOFSTEP]
convert hasSum_fintype (_ : Fin 2 → ℂ) using 1
[GOAL]
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
k : ℕ
⊢ (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I =
    Finset.sum Finset.univ fun b =>
      ((-z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)! - (z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)!) * I / 2
[PROOFSTEP]
rw [Fin.sum_univ_two]
[GOAL]
case h.e'_6
z : ℂ
this :
  HasSum
    (fun x =>
      ((-z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)! -
            (z * I) ^ (2 * x.fst + ↑x.snd) / ↑(2 * x.fst + ↑x.snd)!) *
          I /
        2)
    ((_root_.exp ℂ (-z * I) - _root_.exp ℂ (z * I)) * I / 2)
k : ℕ
⊢ (z * I) ^ (2 * k + 1) / ↑(2 * k + 1)! / I =
    ((-z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)! - (z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)!) * I / 2 +
      ((-z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)! - (z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)!) * I / 2
[PROOFSTEP]
simp_rw [Fin.val_zero, Fin.val_one, add_zero, pow_succ', pow_mul, mul_pow, neg_sq, sub_self, zero_mul, zero_div,
  zero_add, neg_mul, mul_neg, neg_div, ← neg_add', ← two_mul, neg_mul, neg_div, mul_assoc,
  mul_div_cancel_left _ (two_ne_zero : (2 : ℂ) ≠ 0), Complex.div_I]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (cos z)
[PROOFSTEP]
convert Complex.hasSum_cos' z using 1
[GOAL]
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) = fun n => (z * I) ^ (2 * n) / ↑(2 * n)!
[PROOFSTEP]
simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]
[GOAL]
z : ℂ
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) (sin z)
[PROOFSTEP]
convert Complex.hasSum_sin' z using 1
[GOAL]
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)!) = fun n => (z * I) ^ (2 * n + 1) / ↑(2 * n + 1)! / I
[PROOFSTEP]
simp_rw [mul_pow, pow_succ', pow_mul, Complex.I_sq, ← mul_assoc, mul_div_assoc, div_right_comm,
  div_self Complex.I_ne_zero, mul_comm _ ((-1 : ℂ) ^ _), mul_one_div, mul_div_assoc, mul_assoc]
[GOAL]
r : ℝ
⊢ HasSum (fun n => (-1) ^ n * r ^ (2 * n) / ↑(2 * n)!) (cos r)
[PROOFSTEP]
exact_mod_cast Complex.hasSum_cos r
[GOAL]
r : ℝ
⊢ HasSum (fun n => (-1) ^ n * r ^ (2 * n + 1) / ↑(2 * n + 1)!) (sin r)
[PROOFSTEP]
exact_mod_cast Complex.hasSum_sin r
