[STATEMENT]
lemma fds_abs_summable_zeta: 
  "(s :: 'a :: {banach, nat_power_normed_field}) \<bullet> 1 > 1 \<Longrightarrow> fds_abs_converges fds_zeta s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < s \<bullet> (1::'a) \<Longrightarrow> fds_abs_converges fds_zeta s
[PROOF STEP]
by simp