[STATEMENT]
lemma uniformly_summable_deriv_ln_Gamma:
  assumes z: "(z :: 'a :: {real_normed_field,banach}) \<noteq> 0" and d: "d > 0" "d \<le> norm z/2"
  shows "uniformly_convergent_on (ball z d)
            (\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))"
           (is "uniformly_convergent_on _ (\<lambda>k z. \<Sum>i<k. ?f i z)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse (of_nat (Suc i)) - inverse (z + of_nat (Suc i)))
[PROOF STEP]
proof (rule Weierstrass_m_test'_ev)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
assume t: "t \<in> ball z d"
[PROOF STATE]
proof (state)
this:
t \<in> ball z d

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
have "norm z = norm (t + (z - t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm z = norm (t + (z - t))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm z = norm (t + (z - t))

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
have "norm (t + (z - t)) \<le> norm t + norm (z - t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (t + (z - t)) \<le> norm t + norm (z - t)
[PROOF STEP]
by (rule norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (t + (z - t)) \<le> norm t + norm (z - t)

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (t + (z - t)) \<le> norm t + norm (z - t)

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
from t d
[PROOF STATE]
proof (chain)
picking this:
t \<in> ball z d
0 < d
d \<le> norm z / 2
[PROOF STEP]
have "norm (z - t) < norm z / 2"
[PROOF STATE]
proof (prove)
using this:
t \<in> ball z d
0 < d
d \<le> norm z / 2

goal (1 subgoal):
 1. norm (z - t) < norm z / 2
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
norm (z - t) < norm z / 2

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x < y \<Longrightarrow> norm t + x < norm t + y) \<Longrightarrow> norm (t + (z - t)) < norm t + norm z / 2
[PROOF STEP]
have A: "norm t > norm z / 2"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x < y \<Longrightarrow> norm t + x < norm t + y) \<Longrightarrow> norm (t + (z - t)) < norm t + norm z / 2

goal (1 subgoal):
 1. norm z / 2 < norm t
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x < y \<Longrightarrow> norm t + x < norm t + y) \<Longrightarrow> norm (t + (z - t)) < norm t + norm z / 2
z \<noteq> (0::'a)

goal (1 subgoal):
 1. norm z / 2 < norm t
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
norm z / 2 < norm t

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
have "norm t = norm (z + (t - z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm t = norm (z + (t - z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm t = norm (z + (t - z))

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm t = norm (z + (t - z))

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
have "\<dots> \<le> norm z + norm (t - z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (z + (t - z)) \<le> norm z + norm (t - z)
[PROOF STEP]
by (rule norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (z + (t - z)) \<le> norm z + norm (t - z)

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (z + (t - z)) \<le> norm z + norm (t - z)

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
from t d
[PROOF STATE]
proof (chain)
picking this:
t \<in> ball z d
0 < d
d \<le> norm z / 2
[PROOF STEP]
have "norm (t - z) \<le> norm z / 2"
[PROOF STATE]
proof (prove)
using this:
t \<in> ball z d
0 < d
d \<le> norm z / 2

goal (1 subgoal):
 1. norm (t - z) \<le> norm z / 2
[PROOF STEP]
by (simp add: dist_norm norm_minus_commute)
[PROOF STATE]
proof (state)
this:
norm (t - z) \<le> norm z / 2

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (t - z) \<le> norm z / 2

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
from z
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> (0::'a)
[PROOF STEP]
have "\<dots> < norm z"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0::'a)

goal (1 subgoal):
 1. norm z / 2 < norm z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm z / 2 < norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> norm z + x \<le> norm z + y; \<And>x y. x < y \<Longrightarrow> norm z + x < norm z + y\<rbrakk> \<Longrightarrow> norm t < norm z + norm z
[PROOF STEP]
have B: "norm t < 2 * norm z"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> norm z + x \<le> norm z + y; \<And>x y. x < y \<Longrightarrow> norm z + x < norm z + y\<rbrakk> \<Longrightarrow> norm t < norm z + norm z

goal (1 subgoal):
 1. norm t < 2 * norm z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm t < 2 * norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
note A B
[PROOF STATE]
proof (state)
this:
norm z / 2 < norm t
norm t < 2 * norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?t2 \<in> ball z d \<Longrightarrow> norm z / 2 < norm ?t2
?t2 \<in> ball z d \<Longrightarrow> norm ?t2 < 2 * norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
note ball = this
[PROOF STATE]
proof (state)
this:
?t2 \<in> ball z d \<Longrightarrow> norm z / 2 < norm ?t2
?t2 \<in> ball z d \<Longrightarrow> norm ?t2 < 2 * norm z

goal (2 subgoals):
 1. \<forall>\<^sub>F k in sequentially. \<forall>z\<in>ball z d. norm (inverse (of_nat (Suc k)) - inverse (z + of_nat (Suc k))) \<le> ?M k
 2. summable ?M
[PROOF STEP]
show "eventually (\<lambda>n. \<forall>t\<in>ball z d. norm (?f n t) \<le> 4 * norm z * inverse (of_nat (Suc n)^2)) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<forall>t\<in>ball z d. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
using eventually_gt_at_top
[PROOF STATE]
proof (prove)
using this:
eventually ((<) ?c) at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. \<forall>t\<in>ball z d. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
apply eventually_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. ?c1 < n \<Longrightarrow> \<forall>t\<in>ball z d. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
fix t :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
assume t: "t \<in> ball z d"
[PROOF STATE]
proof (state)
this:
t \<in> ball z d

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
from z ball[OF t]
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> (0::'a)
norm z / 2 < norm t
norm t < 2 * norm z
[PROOF STEP]
have t_nz: "t \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0::'a)
norm z / 2 < norm t
norm t < 2 * norm z

goal (1 subgoal):
 1. t \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
assume n: "n > nat \<lceil>4 * norm z\<rceil>"
[PROOF STATE]
proof (state)
this:
nat \<lceil>4 * norm z\<rceil> < n

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
from ball[OF t] t_nz
[PROOF STATE]
proof (chain)
picking this:
norm z / 2 < norm t
norm t < 2 * norm z
t \<noteq> (0::'a)
[PROOF STEP]
have "4 * norm z > 2 * norm t"
[PROOF STATE]
proof (prove)
using this:
norm z / 2 < norm t
norm t < 2 * norm z
t \<noteq> (0::'a)

goal (1 subgoal):
 1. 2 * norm t < 4 * norm z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * norm t < 4 * norm z

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 * norm t < 4 * norm z

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
from n
[PROOF STATE]
proof (chain)
picking this:
nat \<lceil>4 * norm z\<rceil> < n
[PROOF STEP]
have "\<dots>  < of_nat n"
[PROOF STATE]
proof (prove)
using this:
nat \<lceil>4 * norm z\<rceil> < n

goal (1 subgoal):
 1. 4 * norm z < real n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
4 * norm z < real n

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
2 * norm t < real n
[PROOF STEP]
have n: "of_nat n > 2 * norm t"
[PROOF STATE]
proof (prove)
using this:
2 * norm t < real n

goal (1 subgoal):
 1. 2 * norm t < real n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
2 * norm t < real n

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
hence "of_nat n > norm t"
[PROOF STATE]
proof (prove)
using this:
2 * norm t < real n

goal (1 subgoal):
 1. norm t < real n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm t < real n

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
hence t': "t \<noteq> -of_nat (Suc n)"
[PROOF STATE]
proof (prove)
using this:
norm t < real n

goal (1 subgoal):
 1. t \<noteq> - of_nat (Suc n)
[PROOF STEP]
by (intro notI) (simp del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
t \<noteq> - of_nat (Suc n)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
with t_nz
[PROOF STATE]
proof (chain)
picking this:
t \<noteq> (0::'a)
t \<noteq> - of_nat (Suc n)
[PROOF STEP]
have "?f n t = 1 / (of_nat (Suc n) * (1 + of_nat (Suc n)/t))"
[PROOF STATE]
proof (prove)
using this:
t \<noteq> (0::'a)
t \<noteq> - of_nat (Suc n)

goal (1 subgoal):
 1. inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n)) = (1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))
[PROOF STEP]
by (simp add: field_split_simps eq_neg_iff_add_eq_0 del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n)) = (1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n)) = (1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
have "norm \<dots> = inverse (of_nat (Suc n)) * inverse (norm (of_nat (Suc n)/t + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm ((1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))) = inverse (real (Suc n)) * inverse (norm (of_nat (Suc n) / t + (1::'a)))
[PROOF STEP]
by (simp add: norm_divide norm_mult field_split_simps del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
norm ((1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))) = inverse (real (Suc n)) * inverse (norm (of_nat (Suc n) / t + (1::'a)))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm ((1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))) = inverse (real (Suc n)) * inverse (norm (of_nat (Suc n) / t + (1::'a)))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
norm ((1::'a) / (of_nat (Suc n) * ((1::'a) + of_nat (Suc n) / t))) = inverse (real (Suc n)) * inverse (norm (of_nat (Suc n) / t + (1::'a)))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
from z t_nz ball[OF t]
[PROOF STATE]
proof (chain)
picking this:
z \<noteq> (0::'a)
t \<noteq> (0::'a)
norm z / 2 < norm t
norm t < 2 * norm z
[PROOF STEP]
have "of_nat (Suc n) / (4 * norm z) \<le> of_nat (Suc n) / (2 * norm t)"
[PROOF STATE]
proof (prove)
using this:
z \<noteq> (0::'a)
t \<noteq> (0::'a)
norm z / 2 < norm t
norm t < 2 * norm z

goal (1 subgoal):
 1. real (Suc n) / (4 * norm z) \<le> real (Suc n) / (2 * norm t)
[PROOF STEP]
by (intro divide_left_mono mult_pos_pos) simp_all
[PROOF STATE]
proof (state)
this:
real (Suc n) / (4 * norm z) \<le> real (Suc n) / (2 * norm t)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (Suc n) / (4 * norm z) \<le> real (Suc n) / (2 * norm t)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
have "\<dots> < norm (of_nat (Suc n) / t) - norm (1 :: 'a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Suc n) / (2 * norm t) < norm (of_nat (Suc n) / t) - norm (1::'a)
[PROOF STEP]
using t_nz n
[PROOF STATE]
proof (prove)
using this:
t \<noteq> (0::'a)
2 * norm t < real n

goal (1 subgoal):
 1. real (Suc n) / (2 * norm t) < norm (of_nat (Suc n) / t) - norm (1::'a)
[PROOF STEP]
by (simp add: field_simps norm_divide del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
real (Suc n) / (2 * norm t) < norm (of_nat (Suc n) / t) - norm (1::'a)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (Suc n) / (2 * norm t) < norm (of_nat (Suc n) / t) - norm (1::'a)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
have "\<dots> \<le> norm (of_nat (Suc n)/t + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (of_nat (Suc n) / t) - norm (1::'a) \<le> norm (of_nat (Suc n) / t + (1::'a))
[PROOF STEP]
by (rule norm_diff_ineq)
[PROOF STATE]
proof (state)
this:
norm (of_nat (Suc n) / t) - norm (1::'a) \<le> norm (of_nat (Suc n) / t + (1::'a))

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (Suc n) / (4 * norm z) < norm (of_nat (Suc n) / t + (1::'a))
[PROOF STEP]
have "inverse (norm (of_nat (Suc n)/t + 1)) \<le> 4 * norm z / of_nat (Suc n)"
[PROOF STATE]
proof (prove)
using this:
real (Suc n) / (4 * norm z) < norm (of_nat (Suc n) / t + (1::'a))

goal (1 subgoal):
 1. inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
real (Suc n) / (4 * norm z) < norm (of_nat (Suc n) / t + (1::'a))
z \<noteq> (0::'a)

goal (1 subgoal):
 1. inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)
[PROOF STEP]
by (simp add: field_split_simps norm_divide mult_ac del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse (norm (of_nat (Suc n) / t + (1::'a))) \<le> 4 * norm z / real (Suc n)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
have "inverse (real_of_nat (Suc n)) * (4 * norm z / real_of_nat (Suc n)) =
                 4 * norm z * inverse (of_nat (Suc n)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (real (Suc n)) * (4 * norm z / real (Suc n)) = 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
by (simp add: field_split_simps power2_eq_square del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
inverse (real (Suc n)) * (4 * norm z / real (Suc n)) = 4 * norm z * inverse ((real (Suc n))\<^sup>2)

goal (1 subgoal):
 1. \<And>n t. \<lbrakk>?c1 < n; t \<in> ball z d\<rbrakk> \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> inverse (real (Suc n)) * x \<le> inverse (real (Suc n)) * y) \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
show "norm (?f n t) \<le> 4 * norm z * inverse (of_nat (Suc n)^2)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> inverse (real (Suc n)) * x \<le> inverse (real (Suc n)) * y) \<Longrightarrow> norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)

goal (1 subgoal):
 1. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)
[PROOF STEP]
by (simp del: of_nat_Suc)
[PROOF STATE]
proof (state)
this:
norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. \<forall>t\<in>ball z d. norm (inverse (of_nat (Suc n)) - inverse (t + of_nat (Suc n))) \<le> 4 * norm z * inverse ((real (Suc n))\<^sup>2)

goal (1 subgoal):
 1. summable (\<lambda>n. 4 * norm z * inverse ((real (Suc n))\<^sup>2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>n. 4 * norm z * inverse ((real (Suc n))\<^sup>2))
[PROOF STEP]
show "summable (\<lambda>n. 4 * norm z * inverse ((of_nat (Suc n))^2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. 4 * norm z * inverse ((real (Suc n))\<^sup>2))
[PROOF STEP]
by (subst summable_Suc_iff) (simp add: summable_mult inverse_power_summable)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. 4 * norm z * inverse ((real (Suc n))\<^sup>2))

goal:
No subgoals!
[PROOF STEP]
qed