Theorem: HasDerivAt_cpow_over_var (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z / z) (↑N ^ z / z ^ 2 - ↑(↑N).log * ↑N ^ z / z) z
Tactic:
simp_rw [div_eq_mul_inv]
State after:
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z * z⁻¹) (↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹) z

State before:
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z * z⁻¹) (↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹) z
Tactic:
convert HasDerivAt.mul (c := fun z ↦ - (N : ℂ) ^ z) (d := fun z ↦ z⁻¹) (c' := - (N : ℂ) ^ z * Real.log N)
  (d' := - (z ^ 2)⁻¹) ?_ ?_ using 1
State after:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹ = -↑N ^ z * ↑(↑N).log * z⁻¹ + -↑N ^ z * -(z ^ 2)⁻¹

case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-↑N ^ z * ↑(↑N).log) z

case convert_3
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => z⁻¹) (-(z ^ 2)⁻¹) z

State before:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - ↑(↑N).log * ↑N ^ z * z⁻¹ = -↑N ^ z * ↑(↑N).log * z⁻¹ + -↑N ^ z * -(z ^ 2)⁻¹
Tactic:
simp only [natCast_log, neg_mul, cpow_ofNat, mul_neg, neg_neg]
State after:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - (↑N).log * ↑N ^ z * z⁻¹ = -(↑N ^ z * (↑N).log * z⁻¹) + ↑N ^ z * (z ^ 2)⁻¹

State before:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (z ^ 2)⁻¹ - (↑N).log * ↑N ^ z * z⁻¹ = -(↑N ^ z * (↑N).log * z⁻¹) + ↑N ^ z * (z ^ 2)⁻¹
Tactic:
ring_nf
State after:
no goals

State before:
case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-↑N ^ z * ↑(↑N).log) z
Tactic:
simp only [natCast_log, neg_mul]
State after:
case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-(↑N ^ z * (↑N).log)) z

State before:
case convert_2
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => -↑N ^ z) (-(↑N ^ z * (↑N).log)) z
Tactic:
apply HasDerivAt.neg
State after:
case convert_2.h
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun x => ↑N ^ x) (↑N ^ z * (↑N).log) z

State before:
case convert_2.h
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun x => ↑N ^ x) (↑N ^ z * (↑N).log) z
Tactic:
convert HasDerivAt.const_cpow (c := (N : ℂ)) (f := id) (f' := 1) (x := z) (hasDerivAt_id z)
  (by simp [z_ne_zero]) using 1
State after:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (↑N).log = ↑N ^ id z * (↑N).log * 1

State before:
case h.e'_7
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ^ z * (↑N).log = ↑N ^ id z * (↑N).log * 1
Tactic:
simp only [id_eq, mul_one]
State after:
no goals

State before:
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ ↑N ≠ 0 ∨ id z ≠ 0
Tactic:
simp [z_ne_zero]
State after:
no goals

State before:
case convert_3
N : ℕ
z : ℂ
z_ne_zero : z ≠ 0
⊢ HasDerivAt (fun z => z⁻¹) (-(z ^ 2)⁻¹) z
Tactic:
exact hasDerivAt_inv z_ne_zero
State after:
no goals