Theorem: Summable_rpow (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
s : ℂ
s_re_gt : 1 < s.re
⊢ Summable fun n => 1 / ↑n ^ s
Tactic:
apply Summable.of_norm
State after:
case hf
s : ℂ
s_re_gt : 1 < s.re
⊢ Summable fun a => ‖1 / ↑a ^ s‖

State before:
case hf
s : ℂ
s_re_gt : 1 < s.re
⊢ Summable fun a => ‖1 / ↑a ^ s‖
Tactic:
have : s.re ≠ 0 := by linarith
State after:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖1 / ↑a ^ s‖

State before:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖1 / ↑a ^ s‖
Tactic:
simp only [one_div, norm_inv]
State after:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖↑a ^ s‖⁻¹

State before:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => ‖↑a ^ s‖⁻¹
Tactic:
simp_rw [norm_natCast_cpow_of_re_ne_zero _ this]
State after:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => (↑a ^ s.re)⁻¹

State before:
case hf
s : ℂ
s_re_gt : 1 < s.re
this : s.re ≠ 0
⊢ Summable fun a => (↑a ^ s.re)⁻¹
Tactic:
exact (Real.summable_nat_rpow_inv (p := s.re)).mpr s_re_gt
State after:
no goals

State before:
s : ℂ
s_re_gt : 1 < s.re
⊢ s.re ≠ 0
Tactic:
linarith
State after:
no goals