Theorem: neg_logDeriv_ζ₁_eq (EulerProducts/PNT.lean)

State before:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -deriv ζ₁ z / ζ₁ z = -deriv ζ z / ζ z - 1 / (z - 1)
Tactic:
rw [ζ₁_apply_of_ne_one hz₁, deriv_ζ₁_apply_of_ne_one hz₁]
State after:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -(deriv ζ z * (z - 1) + ζ z) / (ζ z * (z - 1)) = -deriv ζ z / ζ z - 1 / (z - 1)

State before:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -(deriv ζ z * (z - 1) + ζ z) / (ζ z * (z - 1)) = -deriv ζ z / ζ z - 1 / (z - 1)
Tactic:
field_simp [sub_ne_zero.mpr hz₁]
State after:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -ζ z + -(deriv ζ z * (z - 1)) = -(deriv ζ z * (z - 1)) - ζ z

State before:
z : ℂ
hz₁ : z ≠ 1
hz₂ : ζ z ≠ 0
⊢ -ζ z + -(deriv ζ z * (z - 1)) = -(deriv ζ z * (z - 1)) - ζ z
Tactic:
ring
State after:
no goals