z : ℂ
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
z : ℂ
⊢ LSeriesSummable (↑ζ) z ↔ 1 < z.re
rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re z.re), LSeriesSummable, ←
  summable_norm_iff, ← Real.summable_one_div_nat_rpow, iff_iff_eq]
case pos
z : ℂ
h0 : z.re = 0
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re

case neg
z : ℂ
h0 : ¬z.re = 0
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
z : ℂ
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
by_cases h0 : z.re = 0
case pos
z : ℂ
h0 : z.re = 0
⊢ (Summable fun n => ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖) = Summable fun n => 1 / ↑n ^ 0
case pos
z : ℂ
h0 : z.re = 0
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
rw [h0, ← summable_nat_add_iff 1]
case pos
z : ℂ
h0 : z.re = 0
⊢ (fun n => ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖) = fun n => 1 / ↑n ^ 0
case pos
z : ℂ
h0 : z.re = 0
⊢ (Summable fun n => ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖) = Summable fun n => 1 / ↑n ^ 0
apply congr rfl
case pos.h
z : ℂ
h0 : z.re = 0
n : ℕ
⊢ ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖ = 1 / ↑n ^ 0
case pos
z : ℂ
h0 : z.re = 0
⊢ (fun n => ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖) = fun n => 1 / ↑n ^ 0
ext n
no goals
case pos.h
z : ℂ
h0 : z.re = 0
n : ℕ
⊢ ‖↑↑ζ (n + 1) / ↑(n + 1) ^ ↑0‖ = 1 / ↑n ^ 0
simp [n.succ_ne_zero]
case neg
z : ℂ
h0 : ¬z.re = 0
⊢ (fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = fun n => 1 / ↑n ^ z.re
case neg
z : ℂ
h0 : ¬z.re = 0
⊢ (Summable fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = Summable fun n => 1 / ↑n ^ z.re
apply congr rfl
case neg.h.zero
z : ℂ
h0 : ¬z.re = 0
⊢ ‖↑↑ζ Nat.zero / ↑Nat.zero ^ ↑z.re‖ = 1 / ↑Nat.zero ^ z.re

case neg.h.succ
z : ℂ
h0 : ¬z.re = 0
n✝ : ℕ
⊢ ‖↑↑ζ (succ n✝) / ↑(succ n✝) ^ ↑z.re‖ = 1 / ↑(succ n✝) ^ z.re
case neg
z : ℂ
h0 : ¬z.re = 0
⊢ (fun x => ‖↑↑ζ x / ↑x ^ ↑z.re‖) = fun n => 1 / ↑n ^ z.re
ext ⟨- | n⟩
case neg.h.succ
z : ℂ
h0 : ¬z.re = 0
n✝ : ℕ
⊢ ↑Complex.abs (↑n✝ + 1) ^ z.re = (↑n✝ + 1) ^ z.re
case neg.h.succ
z : ℂ
h0 : ¬z.re = 0
n✝ : ℕ
⊢ ‖↑↑ζ (succ n✝) / ↑(succ n✝) ^ ↑z.re‖ = 1 / ↑(succ n✝) ^ z.re
simp only [cast_zero, natCoe_apply, zeta_apply, succ_ne_zero, if_false, cast_succ, one_div,
  Complex.norm_eq_abs, map_inv₀, Complex.abs_cpow_real, inv_inj, zero_add]
no goals
case neg.h.succ
z : ℂ
h0 : ¬z.re = 0
n✝ : ℕ
⊢ ↑Complex.abs (↑n✝ + 1) ^ z.re = (↑n✝ + 1) ^ z.re
rw [← cast_one, ← cast_add, Complex.abs_of_nat, cast_add, cast_one]
no goals
case neg.h.zero
z : ℂ
h0 : ¬z.re = 0
⊢ ‖↑↑ζ Nat.zero / ↑Nat.zero ^ ↑z.re‖ = 1 / ↑Nat.zero ^ z.re
simp [h0]