z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
have der1 :
  ∀ x : ℝ,
    x ∈ uIcc 0 (π / 2) →
      HasDerivAt (fun y : ℝ => (cos y : ℂ) ^ n) (-n * sin x * (cos x : ℂ) ^ (n - 1)) x := by
  intro x _
  have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by
    simpa using (hasDerivAt_cos x).ofReal_comp
  convert HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
  ring
case h.e'_2.h.e'_5
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (fun x => Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) = fun x => ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)

case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    ↑(cos (π / 2)) ^ n * (Complex.sin (2 * z * ↑(π / 2)) / (2 * z)) -
        ↑(cos 0) ^ n * (Complex.sin (2 * z * ↑0) / (2 * z)) -
      ∫ (x : ℝ) in 0 ..π / 2, -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z))

case convert_1
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ IntervalIntegrable (fun x => -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) volume 0 (π / 2)

case convert_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ IntervalIntegrable (fun x => Complex.cos (2 * z * ↑x)) volume 0 (π / 2)
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (∫ (x : ℝ) in 0 ..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) =
    ↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)
convert (config := { sameFun := true })
  integral_mul_deriv_eq_deriv_mul der1 (fun x _ => antideriv_cos_comp_const_mul hz x) _ _ using 2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
⊢ ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
intro x _
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x
⊢ HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
have b : HasDerivAt (fun y : ℝ => (cos y : ℂ)) (-sin x) x := by
  simpa using (hasDerivAt_cos x).ofReal_comp
case h.e'_7
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x
⊢ -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) = ↑n * ↑(cos x) ^ (n - 1) * -↑(sin x)
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x
⊢ HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
convert HasDerivAt.comp x (hasDerivAt_pow _ _) b using 1
no goals
case h.e'_7
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
b : HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x
⊢ -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) = ↑n * ↑(cos x) ^ (n - 1) * -↑(sin x)
ring
no goals
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
⊢ HasDerivAt (fun y => ↑(cos y)) (-↑(sin x)) x
simpa using (hasDerivAt_cos x).ofReal_comp
case h.e'_2.h.e'_5.h
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
⊢ Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)
case h.e'_2.h.e'_5
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (fun x => Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n) = fun x => ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)
ext1 x
no goals
case h.e'_2.h.e'_5.h
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
⊢ Complex.cos (2 * z * ↑x) * ↑(cos x) ^ n = ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)
rw [mul_comm]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (∫ (x : ℝ) in 0 ..π / 2, ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1))) =
    ∫ (x : ℝ) in 0 ..π / 2, -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (↑n / (2 * z) * ∫ (x : ℝ) in 0 ..π / 2, Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    ↑(cos (π / 2)) ^ n * (Complex.sin (2 * z * ↑(π / 2)) / (2 * z)) -
        ↑(cos 0) ^ n * (Complex.sin (2 * z * ↑0) / (2 * z)) -
      ∫ (x : ℝ) in 0 ..π / 2, -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z))
rw [Complex.ofReal_zero, MulZeroClass.mul_zero, Complex.sin_zero, zero_div,
  MulZeroClass.mul_zero, sub_zero, cos_pi_div_two, Complex.ofReal_zero,
  zero_pow (by positivity : 0 < n), MulZeroClass.zero_mul, zero_sub, ← integral_neg, ←
  integral_const_mul]
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ (∫ (x : ℝ) in 0 ..π / 2, ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1))) =
    ∫ (x : ℝ) in 0 ..π / 2, -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))
refine' integral_congr fun x _ => _
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n * (Complex.sin (2 * z * ↑x) * Complex.sin ↑x * Complex.cos ↑x ^ (n - 1)) =
    ↑n * Complex.sin ↑x * Complex.cos ↑x ^ (n - 1) * Complex.sin (2 * z * ↑x)
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))
field_simp
no goals
case h.e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
x✝ : x ∈ uIcc 0 (π / 2)
⊢ ↑n * (Complex.sin (2 * z * ↑x) * Complex.sin ↑x * Complex.cos ↑x ^ (n - 1)) =
    ↑n * Complex.sin ↑x * Complex.cos ↑x ^ (n - 1) * Complex.sin (2 * z * ↑x)
ring
no goals
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ 0 < n
positivity
case convert_1.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ Continuous fun x => -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)
case convert_1
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ IntervalIntegrable (fun x => -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) volume 0 (π / 2)
apply Continuous.intervalIntegrable
no goals
case convert_1.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ Continuous fun x => -↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)
exact
  (continuous_const.mul (Complex.continuous_ofReal.comp continuous_sin)).mul
    ((Complex.continuous_ofReal.comp continuous_cos).pow (n - 1))
case convert_2.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ Continuous fun x => Complex.cos (2 * z * ↑x)
case convert_2
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ IntervalIntegrable (fun x => Complex.cos (2 * z * ↑x)) volume 0 (π / 2)
apply Continuous.intervalIntegrable
no goals
case convert_2.hu
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ (x : ℝ), x ∈ uIcc 0 (π / 2) → HasDerivAt (fun y => ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ Continuous fun x => Complex.cos (2 * z * ↑x)
exact Complex.continuous_cos.comp (continuous_const.mul Complex.continuous_ofReal)