[STATEMENT]
lemma imp_ab_rational:
  assumes "\<exists> (B::int)>0. \<exists> c::nat\<Rightarrow> int.
              (\<forall>\<^sub>F n in sequentially. B*b n = c n * a n - c(n+1) \<and> \<bar>c(n+1)\<bar><a n/2)"
  shows "(\<Sum>n. (b n / (\<Prod>i \<le> n. a i))) \<in> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
obtain B::int and c::"nat\<Rightarrow>int" and N::nat where "B>0" and
    large_n:"\<forall>n\<ge>N. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < a n / 2
                      \<and> a n\<ge>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B N c. \<lbrakk>0 < B; \<forall>n\<ge>N. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2 \<and> 2 \<le> a n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>B N c. \<lbrakk>0 < B; \<forall>n\<ge>N. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2 \<and> 2 \<le> a n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain B c where "B>0" and event1:"\<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1)
              \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B c. \<lbrakk>0 < B; \<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<exists>B>0. \<exists>c. \<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2

goal (1 subgoal):
 1. (\<And>B c. \<lbrakk>0 < B; \<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < B
\<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2

goal (1 subgoal):
 1. (\<And>B N c. \<lbrakk>0 < B; \<forall>n\<ge>N. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2 \<and> 2 \<le> a n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from eventually_conj[OF event1 a_large,unfolded eventually_at_top_linorder]
[PROOF STATE]
proof (chain)
picking this:
\<exists>N. \<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 1 < a n
[PROOF STEP]
obtain N where "\<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1)
                        \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 2 \<le> a n"
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 1 < a n

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 2 \<le> a n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 2 \<le> a n

goal (1 subgoal):
 1. (\<And>B N c. \<lbrakk>0 < B; \<forall>n\<ge>N. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2 \<and> 2 \<le> a n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 2 \<le> a n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 2 \<le> a n

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of B N c] \<open>B>0\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 2 \<le> a n
\<lbrakk>0 < B; \<forall>n\<ge>N. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2 \<and> 2 \<le> a n\<rbrakk> \<Longrightarrow> thesis
0 < B

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < B
\<forall>n\<ge>N. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2 \<and> 2 \<le> a n

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
define f where "f=(\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
define S where "S = (\<Sum>n. f n)"
[PROOF STATE]
proof (state)
this:
S = (\<Sum>n. f n)

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
have "summable f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable f
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
by (rule aux_series_summable)
[PROOF STATE]
proof (state)
this:
summable f

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
define C where "C=B*prod a {..<N} * (\<Sum>n<N. f n)"
[PROOF STATE]
proof (state)
this:
C = real_of_int (B * prod a {..<N}) * sum f {..<N}

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
have "B*prod a {..<N} * S = C + real_of_int (c N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
define h1 where "h1 \<equiv> (\<lambda>n. (c (n+N) * a (n+N)) / prod a {N..n+N})"
[PROOF STATE]
proof (state)
this:
h1 \<equiv> \<lambda>n. real_of_int (c (n + N) * a (n + N)) / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
define h2 where "h2 \<equiv> (\<lambda>n. c (n+N+1) / prod a {N..n+N})"
[PROOF STATE]
proof (state)
this:
h2 \<equiv> \<lambda>n. real_of_int (c (n + N + 1)) / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
have f_h12: "B * prod a {..<N}*f (n+N) = h1 n - h2 n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
define g1 where "g1 \<equiv> (\<lambda>n. B * b (n+N))"
[PROOF STATE]
proof (state)
this:
g1 \<equiv> \<lambda>n. B * b (n + N)

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
define g2 where "g2 \<equiv> (\<lambda>n. prod a {..<N} / prod a {..n + N})"
[PROOF STATE]
proof (state)
this:
g2 \<equiv> \<lambda>n. real_of_int (prod a {..<N}) / real_of_int (prod a {..n + N})

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
have "B * prod a {..<N}*f (n+N) = (g1 n * g2 n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = real_of_int (g1 n) * g2 n
[PROOF STEP]
unfolding f_def g1_def g2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (real_of_int (b (n + N)) / real_of_int (prod a {..n + N})) = real_of_int (B * b (n + N)) * (real_of_int (prod a {..<N}) / real_of_int (prod a {..n + N}))
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * f (n + N) = real_of_int (g1 n) * g2 n

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * f (n + N) = real_of_int (g1 n) * g2 n

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
have "g1 n = c (n+N) * a (n+N) - c (n+N+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g1 n = c (n + N) * a (n + N) - c (n + N + 1)
[PROOF STEP]
using large_n[rule_format,of "n+N"]
[PROOF STATE]
proof (prove)
using this:
N \<le> n + N \<Longrightarrow> B * b (n + N) = c (n + N) * a (n + N) - c (n + N + 1) \<and> real_of_int \<bar>c (n + N + 1)\<bar> < real_of_int (a (n + N)) / 2 \<and> 2 \<le> a (n + N)

goal (1 subgoal):
 1. g1 n = c (n + N) * a (n + N) - c (n + N + 1)
[PROOF STEP]
unfolding g1_def
[PROOF STATE]
proof (prove)
using this:
N \<le> n + N \<Longrightarrow> B * b (n + N) = c (n + N) * a (n + N) - c (n + N + 1) \<and> real_of_int \<bar>c (n + N + 1)\<bar> < real_of_int (a (n + N)) / 2 \<and> 2 \<le> a (n + N)

goal (1 subgoal):
 1. B * b (n + N) = c (n + N) * a (n + N) - c (n + N + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g1 n = c (n + N) * a (n + N) - c (n + N + 1)

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
g1 n = c (n + N) * a (n + N) - c (n + N + 1)

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
have "g2 n = (1/prod a {N..n+N})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g2 n = 1 / real_of_int (prod a {N..n + N})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g2 n = 1 / real_of_int (prod a {N..n + N})
[PROOF STEP]
have "prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}
[PROOF STEP]
apply (rule prod.union_disjoint[of "{..<N}" "{N..n+N}" a])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {..<N}
 2. finite {N..n + N}
 3. {..<N} \<inter> {N..n + N} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}

goal (1 subgoal):
 1. g2 n = 1 / real_of_int (prod a {N..n + N})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}

goal (1 subgoal):
 1. g2 n = 1 / real_of_int (prod a {N..n + N})
[PROOF STEP]
have "prod a ({..<N} \<union> {N..n + N}) = prod a {..n+N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod a ({..<N} \<union> {N..n + N}) = prod a {..n + N}
[PROOF STEP]
by (simp add: ivl_disj_un_one(4))
[PROOF STATE]
proof (state)
this:
prod a ({..<N} \<union> {N..n + N}) = prod a {..n + N}

goal (1 subgoal):
 1. g2 n = 1 / real_of_int (prod a {N..n + N})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}
prod a ({..<N} \<union> {N..n + N}) = prod a {..n + N}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}
prod a ({..<N} \<union> {N..n + N}) = prod a {..n + N}

goal (1 subgoal):
 1. g2 n = 1 / real_of_int (prod a {N..n + N})
[PROOF STEP]
unfolding g2_def
[PROOF STATE]
proof (prove)
using this:
prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}
prod a ({..<N} \<union> {N..n + N}) = prod a {..n + N}

goal (1 subgoal):
 1. real_of_int (prod a {..<N}) / real_of_int (prod a {..n + N}) = 1 / real_of_int (prod a {N..n + N})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prod a {..n + N} = prod a {..<N} * prod a {N..n + N}; prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}\<rbrakk> \<Longrightarrow> (\<exists>aa\<in>{..<N}. a aa = 0) \<longrightarrow> (\<exists>aa\<in>{N..n + N}. a aa = 0)
[PROOF STEP]
using a_pos
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. \<lbrakk>prod a {..n + N} = prod a {..<N} * prod a {N..n + N}; prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}\<rbrakk> \<Longrightarrow> (\<exists>aa\<in>{..<N}. a aa = 0) \<longrightarrow> (\<exists>aa\<in>{N..n + N}. a aa = 0)
[PROOF STEP]
by (metis less_irrefl)
[PROOF STATE]
proof (state)
this:
g2 n = 1 / real_of_int (prod a {N..n + N})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g2 n = 1 / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real_of_int (B * prod a {..<N}) * f (n + N) = real_of_int (g1 n) * g2 n
g1 n = c (n + N) * a (n + N) - c (n + N + 1)
g2 n = 1 / real_of_int (prod a {N..n + N})
[PROOF STEP]
have "B*prod a {..<N}*f (n+N) = (c (n+N) * a (n+N) - c (n+N+1)) / prod a {N..n+N}"
[PROOF STATE]
proof (prove)
using this:
real_of_int (B * prod a {..<N}) * f (n + N) = real_of_int (g1 n) * g2 n
g1 n = c (n + N) * a (n + N) - c (n + N + 1)
g2 n = 1 / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = real_of_int (c (n + N) * a (n + N) - c (n + N + 1)) / real_of_int (prod a {N..n + N})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * f (n + N) = real_of_int (c (n + N) * a (n + N) - c (n + N + 1)) / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * f (n + N) = real_of_int (c (n + N) * a (n + N) - c (n + N + 1)) / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
have "... = h1 n - h2 n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (n + N) * a (n + N) - c (n + N + 1)) / real_of_int (prod a {N..n + N}) = h1 n - h2 n
[PROOF STEP]
unfolding h1_def h2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (n + N) * a (n + N) - c (n + N + 1)) / real_of_int (prod a {N..n + N}) = real_of_int (c (n + N) * a (n + N)) / real_of_int (prod a {N..n + N}) - real_of_int (c (n + N + 1)) / real_of_int (prod a {N..n + N})
[PROOF STEP]
by (auto simp:algebra_simps diff_divide_distrib)
[PROOF STATE]
proof (state)
this:
real_of_int (c (n + N) * a (n + N) - c (n + N + 1)) / real_of_int (prod a {N..n + N}) = h1 n - h2 n

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * f (n + N) = h1 n - h2 n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * f (?n + N) = h1 ?n - h2 ?n

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
have "B*prod a {..<N} * S = B*prod a {..<N} * ((\<Sum>n<N. f n) + (\<Sum>n. f (n+N)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N)))
[PROOF STEP]
using suminf_split_initial_segment[OF \<open>summable f\<close>,of N]
[PROOF STATE]
proof (prove)
using this:
suminf f = (\<Sum>n. f (n + N)) + sum f {..<N}

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N)))
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
using this:
suminf f = (\<Sum>n. f (n + N)) + sum f {..<N}

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * suminf f = real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N)))
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * S = real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N)))

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * S = real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N)))

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
have "... = C + B*prod a {..<N}*(\<Sum>n. f (n+N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N))) = C + real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N))
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N))) = real_of_int (B * prod a {..<N}) * sum f {..<N} + real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N))
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N))) = C + real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N))

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * (sum f {..<N} + (\<Sum>n. f (n + N))) = C + real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N))

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
have "... = C + (\<Sum>n. h1 n - h2 n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C + real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N)) = C + (\<Sum>n. h1 n - h2 n)
[PROOF STEP]
apply (subst suminf_mult[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. summable (\<lambda>n. f (n + N))
 2. C + (\<Sum>n. real_of_int (B * prod a {..<N}) * f (n + N)) = C + (\<Sum>n. h1 n - h2 n)
[PROOF STEP]
using \<open>summable f\<close> f_h12
[PROOF STATE]
proof (prove)
using this:
summable f
real_of_int (B * prod a {..<N}) * f (?n + N) = h1 ?n - h2 ?n

goal (2 subgoals):
 1. summable (\<lambda>n. f (n + N))
 2. C + (\<Sum>n. real_of_int (B * prod a {..<N}) * f (n + N)) = C + (\<Sum>n. h1 n - h2 n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C + real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N)) = C + (\<Sum>n. h1 n - h2 n)

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C + real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N)) = C + (\<Sum>n. h1 n - h2 n)

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
have "... = C + h1 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
have "(\<lambda>n. \<Sum>i\<le>n. h1 i - h2 i) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<Sum>i\<le>n. h1 i - h2 i) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)
[PROOF STEP]
proof (rule summable_LIMSEQ')
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>i. h1 i - h2 i)
[PROOF STEP]
have "(\<lambda>i. h1 i - h2 i) = (\<lambda>i.  real_of_int (B * prod a {..<N}) * f (i + N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. h1 i - h2 i) = (\<lambda>i. real_of_int (B * prod a {..<N}) * f (i + N))
[PROOF STEP]
using f_h12
[PROOF STATE]
proof (prove)
using this:
real_of_int (B * prod a {..<N}) * f (?n + N) = h1 ?n - h2 ?n

goal (1 subgoal):
 1. (\<lambda>i. h1 i - h2 i) = (\<lambda>i. real_of_int (B * prod a {..<N}) * f (i + N))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>i. h1 i - h2 i) = (\<lambda>i. real_of_int (B * prod a {..<N}) * f (i + N))

goal (1 subgoal):
 1. summable (\<lambda>i. h1 i - h2 i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>i. h1 i - h2 i) = (\<lambda>i. real_of_int (B * prod a {..<N}) * f (i + N))
[PROOF STEP]
show "summable (\<lambda>i. h1 i - h2 i)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>i. h1 i - h2 i) = (\<lambda>i. real_of_int (B * prod a {..<N}) * f (i + N))

goal (1 subgoal):
 1. summable (\<lambda>i. h1 i - h2 i)
[PROOF STEP]
using \<open>summable f\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>i. h1 i - h2 i) = (\<lambda>i. real_of_int (B * prod a {..<N}) * f (i + N))
summable f

goal (1 subgoal):
 1. summable (\<lambda>i. h1 i - h2 i)
[PROOF STEP]
by (simp add: summable_mult)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>i. h1 i - h2 i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>i\<le>n. h1 i - h2 i) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>i\<le>n. h1 i - h2 i) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
have "(\<Sum>i\<le>n. h1 i - h2 i)  = h1 0 - h2 n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>i\<le>0. h1 i - h2 i) = h1 0 - h2 0
 2. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<Sum>i\<le>0. h1 i - h2 i) = h1 0 - h2 0
 2. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>0. h1 i - h2 i) = h1 0 - h2 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>0. h1 i - h2 i) = h1 0 - h2 0

goal (1 subgoal):
 1. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n

goal (1 subgoal):
 1. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
have "(\<Sum>i\<le>Suc n. h1 i - h2 i) = (\<Sum>i\<le>n. h1 i - h2 i) + h1 (n+1) - h2 (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>Suc n. h1 i - h2 i) = (\<Sum>i\<le>n. h1 i - h2 i) + h1 (n + 1) - h2 (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>Suc n. h1 i - h2 i) = (\<Sum>i\<le>n. h1 i - h2 i) + h1 (n + 1) - h2 (n + 1)

goal (1 subgoal):
 1. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>Suc n. h1 i - h2 i) = (\<Sum>i\<le>n. h1 i - h2 i) + h1 (n + 1) - h2 (n + 1)

goal (1 subgoal):
 1. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
have "... =  h1 0 - h2 n + h1 (n+1) - h2 (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>n. h1 i - h2 i) + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 n + h1 (n + 1) - h2 (n + 1)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n

goal (1 subgoal):
 1. (\<Sum>i\<le>n. h1 i - h2 i) + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 n + h1 (n + 1) - h2 (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>n. h1 i - h2 i) + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 n + h1 (n + 1) - h2 (n + 1)

goal (1 subgoal):
 1. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>n. h1 i - h2 i) + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 n + h1 (n + 1) - h2 (n + 1)

goal (1 subgoal):
 1. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
have "... = h1 0 - h2 (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h1 0 - h2 n + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 (n + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h1 0 - h2 n + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 (n + 1)
[PROOF STEP]
have "h2 n = h1 (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h2 n = h1 (n + 1)
[PROOF STEP]
unfolding h2_def h1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (n + N + 1)) / real_of_int (prod a {N..n + N}) = real_of_int (c (n + 1 + N) * a (n + 1 + N)) / real_of_int (prod a {N..n + 1 + N})
[PROOF STEP]
apply (auto simp:prod.nat_ivl_Suc')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a (Suc (n + N)) = 0; \<forall>aa\<in>{N..n + N}. a aa \<noteq> 0\<rbrakk> \<Longrightarrow> c (Suc (n + N)) = 0
[PROOF STEP]
using a_pos
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. \<lbrakk>a (Suc (n + N)) = 0; \<forall>aa\<in>{N..n + N}. a aa \<noteq> 0\<rbrakk> \<Longrightarrow> c (Suc (n + N)) = 0
[PROOF STEP]
by (metis less_numeral_extra(3))
[PROOF STATE]
proof (state)
this:
h2 n = h1 (n + 1)

goal (1 subgoal):
 1. h1 0 - h2 n + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 (n + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
h2 n = h1 (n + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
h2 n = h1 (n + 1)

goal (1 subgoal):
 1. h1 0 - h2 n + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h1 0 - h2 n + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 (n + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
h1 0 - h2 n + h1 (n + 1) - h2 (n + 1) = h1 0 - h2 (n + 1)

goal (1 subgoal):
 1. \<And>n. (\<Sum>i\<le>n. h1 i - h2 i) = h1 0 - h2 n \<Longrightarrow> (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (n + 1)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (n + 1)

goal (1 subgoal):
 1. (\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>Suc n. h1 i - h2 i) = h1 0 - h2 (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>?n. h1 i - h2 i) = h1 0 - h2 ?n

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<Sum>i\<le>n. h1 i - h2 i) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)
(\<Sum>i\<le>?n. h1 i - h2 i) = h1 0 - h2 ?n
[PROOF STEP]
have "(\<lambda>n. h1 0 - h2 n) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<Sum>i\<le>n. h1 i - h2 i) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)
(\<Sum>i\<le>?n. h1 i - h2 i) = h1 0 - h2 ?n

goal (1 subgoal):
 1. (\<lambda>n. h1 0 - h2 n) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. h1 0 - h2 n) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. h1 0 - h2 n) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)
[PROOF STEP]
have "h2 \<longlonglongrightarrow> (h1 0 -  (\<Sum>i. h1 i - h2 i))"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. h1 0 - h2 n) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)

goal (1 subgoal):
 1. h2 \<longlonglongrightarrow> h1 0 - (\<Sum>i. h1 i - h2 i)
[PROOF STEP]
apply (elim metric_tendsto_imp_tendsto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. dist (h2 x) (h1 0 - (\<Sum>i. h1 i - h2 i)) \<le> dist (h1 0 - h2 x) (\<Sum>i. h1 i - h2 i)
[PROOF STEP]
by (auto intro!:eventuallyI simp add:dist_real_def)
[PROOF STATE]
proof (state)
this:
h2 \<longlonglongrightarrow> h1 0 - (\<Sum>i. h1 i - h2 i)

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
h2 \<longlonglongrightarrow> h1 0 - (\<Sum>i. h1 i - h2 i)

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
have "h2 \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h2 \<longlonglongrightarrow> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. h2 \<longlonglongrightarrow> 0
[PROOF STEP]
have h2_n:"\<bar>h2 n\<bar> < (1 / 2)^(n+1)" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
have "\<bar>h2 n\<bar> = \<bar>c (n + N + 1)\<bar> / prod a {N..n + N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>h2 n\<bar> = real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N})
[PROOF STEP]
unfolding h2_def abs_divide
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int (c (n + N + 1))\<bar> / \<bar>real_of_int (prod a {N..n + N})\<bar> = real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N})
[PROOF STEP]
using a_pos
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. \<bar>real_of_int (c (n + N + 1))\<bar> / \<bar>real_of_int (prod a {N..n + N})\<bar> = real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N})
[PROOF STEP]
by (simp add: abs_of_pos prod_pos)
[PROOF STATE]
proof (state)
this:
\<bar>h2 n\<bar> = real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>h2 n\<bar> = real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
have "... < (a (N+n) / 2) / prod a {N..n + N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N}) < real_of_int (a (N + n)) / 2 / real_of_int (prod a {N..n + N})
[PROOF STEP]
unfolding h2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N}) < real_of_int (a (N + n)) / 2 / real_of_int (prod a {N..n + N})
[PROOF STEP]
apply (rule divide_strict_right_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. real_of_int \<bar>c (n + N + 1)\<bar> < real_of_int (a (N + n)) / 2
 2. 0 < real_of_int (prod a {N..n + N})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int \<bar>c (n + N + 1)\<bar> < real_of_int (a (N + n)) / 2
[PROOF STEP]
using large_n[rule_format,of "N+n"]
[PROOF STATE]
proof (prove)
using this:
N \<le> N + n \<Longrightarrow> B * b (N + n) = c (N + n) * a (N + n) - c (N + n + 1) \<and> real_of_int \<bar>c (N + n + 1)\<bar> < real_of_int (a (N + n)) / 2 \<and> 2 \<le> a (N + n)

goal (1 subgoal):
 1. real_of_int \<bar>c (n + N + 1)\<bar> < real_of_int (a (N + n)) / 2
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < real_of_int (prod a {N..n + N})
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < real_of_int (prod a {N..n + N})
[PROOF STEP]
using a_pos
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. 0 < real_of_int (prod a {N..n + N})
[PROOF STEP]
by (simp add: prod_pos)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N}) < real_of_int (a (N + n)) / 2 / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>c (n + N + 1)\<bar> / real_of_int (prod a {N..n + N}) < real_of_int (a (N + n)) / 2 / real_of_int (prod a {N..n + N})

goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
have "... = 1 / (2*prod a {N..<n + N})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a (N + n)) / 2 / real_of_int (prod a {N..n + N}) = 1 / real_of_int (2 * prod a {N..<n + N})
[PROOF STEP]
apply (subst ivl_disj_un(6)[of N "n+N",symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. N \<le> n + N
 2. real_of_int (a (N + n)) / 2 / real_of_int (prod a ({N..<n + N} \<union> {n + N})) = 1 / real_of_int (2 * prod a {N..<n + N})
[PROOF STEP]
using a_pos[rule_format,of "N+n"]
[PROOF STATE]
proof (prove)
using this:
0 < a (N + n)

goal (2 subgoals):
 1. N \<le> n + N
 2. real_of_int (a (N + n)) / 2 / real_of_int (prod a ({N..<n + N} \<union> {n + N})) = 1 / real_of_int (2 * prod a {N..<n + N})
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (a (N + n)) / 2 / real_of_int (prod a {N..n + N}) = 1 / real_of_int (2 * prod a {N..<n + N})

goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (a (N + n)) / 2 / real_of_int (prod a {N..n + N}) = 1 / real_of_int (2 * prod a {N..<n + N})

goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
have "... \<le> (1/2)^(n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 / real_of_int (2 * prod a {N..<0 + N}) \<le> (1 / 2) ^ (0 + 1)
 2. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. 1 / real_of_int (2 * prod a {N..<0 + N}) \<le> (1 / 2) ^ (0 + 1)
 2. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real_of_int (2 * prod a {N..<0 + N}) \<le> (1 / 2) ^ (0 + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 / real_of_int (2 * prod a {N..<0 + N}) \<le> (1 / 2) ^ (0 + 1)

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1)

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
define P where "P=1 / real_of_int (2 * prod a {N..<n + N})"
[PROOF STATE]
proof (state)
this:
P = 1 / real_of_int (2 * prod a {N..<n + N})

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
have "1 / real_of_int (2 * prod a {N..<Suc n + N}) = P / a (n+N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real_of_int (2 * prod a {N..<Suc n + N}) = P / real_of_int (a (n + N))
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real_of_int (2 * prod a {N..<Suc n + N}) = 1 / real_of_int (2 * prod a {N..<n + N}) / real_of_int (a (n + N))
[PROOF STEP]
by (auto simp add: prod.atLeastLessThan_Suc)
[PROOF STATE]
proof (state)
this:
1 / real_of_int (2 * prod a {N..<Suc n + N}) = P / real_of_int (a (n + N))

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 / real_of_int (2 * prod a {N..<Suc n + N}) = P / real_of_int (a (n + N))

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
have "... \<le>  ( (1 / 2) ^ (n + 1) ) / a (n+N) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P / real_of_int (a (n + N)) \<le> (1 / 2) ^ (n + 1) / real_of_int (a (n + N))
[PROOF STEP]
apply (rule divide_right_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. P \<le> (1 / 2) ^ (n + 1)
 2. 0 \<le> real_of_int (a (n + N))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<le> (1 / 2) ^ (n + 1)
[PROOF STEP]
unfolding P_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1)

goal (1 subgoal):
 1. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> real_of_int (a (n + N))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> real_of_int (a (n + N))
[PROOF STEP]
by (simp add: a_pos less_imp_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
P / real_of_int (a (n + N)) \<le> (1 / 2) ^ (n + 1) / real_of_int (a (n + N))

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P / real_of_int (a (n + N)) \<le> (1 / 2) ^ (n + 1) / real_of_int (a (n + N))

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
have "... \<le> ( (1 / 2) ^ (n + 1) ) / 2 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 / 2) ^ (n + 1) / real_of_int (a (n + N)) \<le> (1 / 2) ^ (n + 1) / 2
[PROOF STEP]
apply (rule divide_left_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. 2 \<le> real_of_int (a (n + N))
 2. 0 \<le> (1 / 2) ^ (n + 1)
 3. 0 < real_of_int (a (n + N)) * 2
[PROOF STEP]
using large_n[rule_format,of "n+N",simplified]
[PROOF STATE]
proof (prove)
using this:
B * b (n + N) = c (n + N) * a (n + N) - c (Suc (n + N)) \<and> \<bar>real_of_int (c (Suc (n + N)))\<bar> * 2 < real_of_int (a (n + N)) \<and> 2 \<le> a (n + N)

goal (3 subgoals):
 1. 2 \<le> real_of_int (a (n + N))
 2. 0 \<le> (1 / 2) ^ (n + 1)
 3. 0 < real_of_int (a (n + N)) * 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 / 2) ^ (n + 1) / real_of_int (a (n + N)) \<le> (1 / 2) ^ (n + 1) / 2

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1 / 2) ^ (n + 1) / real_of_int (a (n + N)) \<le> (1 / 2) ^ (n + 1) / 2

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
have "... = (1 / 2) ^ (n + 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 / 2) ^ (n + 1) / 2 = (1 / 2) ^ (n + 2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1 / 2) ^ (n + 1) / 2 = (1 / 2) ^ (n + 2)

goal (1 subgoal):
 1. \<And>n. 1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1) \<Longrightarrow> 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (n + 2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (n + 2)

goal (1 subgoal):
 1. 1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 / real_of_int (2 * prod a {N..<Suc n + N}) \<le> (1 / 2) ^ (Suc n + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 / real_of_int (2 * prod a {N..<n + N}) \<le> (1 / 2) ^ (n + 1)

goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)

goal (1 subgoal):
 1. \<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>h2 n\<bar> < (1 / 2) ^ (n + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>h2 ?n\<bar> < (1 / 2) ^ (?n + 1)

goal (1 subgoal):
 1. h2 \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. (1 / 2)^(n+1)) \<longlonglongrightarrow> (0::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. (1 / 2) ^ (n + 1)) \<longlonglongrightarrow> 0
[PROOF STEP]
using tendsto_mult_right_zero[OF LIMSEQ_abs_realpow_zero2[of "1/2",simplified],of "1/2"]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. 1 / 2 * (1 / 2) ^ x) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. (1 / 2) ^ (n + 1)) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (1 / 2) ^ (n + 1)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. h2 \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (1 / 2) ^ (n + 1)) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (1 / 2) ^ (n + 1)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. h2 \<longlonglongrightarrow> 0
[PROOF STEP]
apply (elim Lim_null_comparison[rotated])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. norm (h2 x) \<le> (1 / 2) ^ (x + 1)
[PROOF STEP]
using h2_n less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
\<bar>h2 ?n\<bar> < (1 / 2) ^ (?n + 1)
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. norm (h2 x) \<le> (1 / 2) ^ (x + 1)
[PROOF STEP]
by (auto intro!:eventuallyI)
[PROOF STATE]
proof (state)
this:
h2 \<longlonglongrightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
h2 \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
h2 \<longlonglongrightarrow> h1 0 - (\<Sum>i. h1 i - h2 i)
h2 \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<Sum>i. h1 i - h2 i) = h1 0"
[PROOF STATE]
proof (prove)
using this:
h2 \<longlonglongrightarrow> h1 0 - (\<Sum>i. h1 i - h2 i)
h2 \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<Sum>i. h1 i - h2 i) = h1 0
[PROOF STEP]
using LIMSEQ_unique
[PROOF STATE]
proof (prove)
using this:
h2 \<longlonglongrightarrow> h1 0 - (\<Sum>i. h1 i - h2 i)
h2 \<longlonglongrightarrow> 0
\<lbrakk>?X \<longlonglongrightarrow> ?a; ?X \<longlonglongrightarrow> ?b\<rbrakk> \<Longrightarrow> ?a = ?b

goal (1 subgoal):
 1. (\<Sum>i. h1 i - h2 i) = h1 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<Sum>i. h1 i - h2 i) = h1 0

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i. h1 i - h2 i) = h1 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i. h1 i - h2 i) = h1 0

goal (1 subgoal):
 1. C + (\<Sum>n. h1 n - h2 n) = C + h1 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C + (\<Sum>n. h1 n - h2 n) = C + h1 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
C + (\<Sum>n. h1 n - h2 n) = C + h1 0

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C + (\<Sum>n. h1 n - h2 n) = C + h1 0

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
have "... = C + c N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C + h1 0 = C + real_of_int (c N)
[PROOF STEP]
unfolding h1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C + real_of_int (c (0 + N) * a (0 + N)) / real_of_int (prod a {N..0 + N}) = C + real_of_int (c N)
[PROOF STEP]
using a_pos
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. C + real_of_int (c (0 + N) * a (0 + N)) / real_of_int (prod a {N..0 + N}) = C + real_of_int (c N)
[PROOF STEP]
by auto (metis less_irrefl)
[PROOF STATE]
proof (state)
this:
C + h1 0 = C + real_of_int (c N)

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)
[PROOF STEP]
have "S = (C + real_of_int (c N)) / (B*prod a {..<N})"
[PROOF STATE]
proof (prove)
using this:
real_of_int (B * prod a {..<N}) * S = C + real_of_int (c N)

goal (1 subgoal):
 1. S = (C + real_of_int (c N)) / real_of_int (B * prod a {..<N})
[PROOF STEP]
by (metis \<open>0 < B\<close> a_pos less_irrefl mult.commute mult_pos_pos
        nonzero_mult_div_cancel_right of_int_eq_0_iff prod_pos)
[PROOF STATE]
proof (state)
this:
S = (C + real_of_int (c N)) / real_of_int (B * prod a {..<N})

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S = (C + real_of_int (c N)) / real_of_int (B * prod a {..<N})

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
have "... \<in> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C + real_of_int (c N)) / real_of_int (B * prod a {..<N}) \<in> \<rat>
[PROOF STEP]
unfolding C_def f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real_of_int (B * prod a {..<N}) * (\<Sum>n<N. real_of_int (b n) / real_of_int (prod a {..n})) + real_of_int (c N)) / real_of_int (B * prod a {..<N}) \<in> \<rat>
[PROOF STEP]
by (intro Rats_divide Rats_add Rats_mult Rats_of_int Rats_sum)
[PROOF STATE]
proof (state)
this:
(C + real_of_int (c N)) / real_of_int (B * prod a {..<N}) \<in> \<rat>

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
S = (C + real_of_int (c N)) / real_of_int (B * prod a {..<N})
(C + real_of_int (c N)) / real_of_int (B * prod a {..<N}) \<in> \<rat>
[PROOF STEP]
show "S \<in> \<rat>"
[PROOF STATE]
proof (prove)
using this:
S = (C + real_of_int (c N)) / real_of_int (B * prod a {..<N})
(C + real_of_int (c N)) / real_of_int (B * prod a {..<N}) \<in> \<rat>

goal (1 subgoal):
 1. S \<in> \<rat>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<in> \<rat>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem theorem_2_1_Erdos_Straus :
  "(\<Sum>n. (b n / (\<Prod>i \<le> n. a i))) \<in> \<rat> \<longleftrightarrow> (\<exists> (B::int)>0. \<exists> c::nat\<Rightarrow> int.
            (\<forall>\<^sub>F n in sequentially. B*b n = c n * a n - c(n+1) \<and> \<bar>c(n+1)\<bar><a n/2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>) = (\<exists>B>0. \<exists>c. \<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2)
[PROOF STEP]
using ab_rationality_imp imp_ab_rational
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat> \<Longrightarrow> \<exists>B>0. \<exists>c. (\<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0
\<exists>B>0. \<exists>c. \<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2 \<Longrightarrow> (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>

goal (1 subgoal):
 1. ((\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>) = (\<exists>B>0. \<exists>c. \<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2)
[PROOF STEP]
by auto


[STATEMENT]
lemma nth_prime_nonzero[simp]:"nth_prime n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_prime n \<noteq> 0
[PROOF STEP]
by (simp add: prime_gt_0_nat prime_nth_prime)


[STATEMENT]
lemma nth_prime_gt_zero[simp]:"nth_prime n >0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < nth_prime n
[PROOF STEP]
by (simp add: prime_gt_0_nat prime_nth_prime)


[STATEMENT]
lemma ratio_of_consecutive_primes:
  "(\<lambda>n. nth_prime (n+1)/nth_prime n) \<longlonglongrightarrow>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
define f where "f=(\<lambda>x. real (nth_prime (Suc x)) /real (nth_prime x))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>x. real (nth_prime (Suc x)) / real (nth_prime x))

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
define g where "g=(\<lambda>x. (real x * ln (real x))
                              / (real (Suc x) * ln (real (Suc x))))"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>x. real x * ln (real x) / (real (Suc x) * ln (real (Suc x))))

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
have p_n:"(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
using nth_prime_asymptotics[unfolded asymp_equiv_def,simplified]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
have p_sn:"(\<lambda>n. real (nth_prime (Suc n))
                        / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (Suc n)) / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1
[PROOF STEP]
using nth_prime_asymptotics[unfolded asymp_equiv_def,simplified
        ,THEN LIMSEQ_Suc]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real (nth_prime (Suc n)) / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (Suc n)) / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real (nth_prime (Suc n)) / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
(\<lambda>n. real (nth_prime (Suc n)) / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1
[PROOF STEP]
have "(\<lambda>x. f x * g x) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
(\<lambda>n. real (nth_prime (Suc n)) / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<longlonglongrightarrow> 1
[PROOF STEP]
using tendsto_divide[OF p_sn p_n]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
(\<lambda>n. real (nth_prime (Suc n)) / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1
1 \<noteq> 0 \<Longrightarrow> (\<lambda>x. real (nth_prime (Suc x)) / (real (Suc x) * ln (real (Suc x))) / (real (nth_prime x) / (real x * ln (real x)))) \<longlonglongrightarrow> 1 / 1

goal (1 subgoal):
 1. (\<lambda>x. f x * g x) \<longlonglongrightarrow> 1
[PROOF STEP]
unfolding f_def g_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
(\<lambda>n. real (nth_prime (Suc n)) / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1
1 \<noteq> 0 \<Longrightarrow> (\<lambda>x. real (nth_prime (Suc x)) / (real (Suc x) * ln (real (Suc x))) / (real (nth_prime x) / (real x * ln (real x)))) \<longlonglongrightarrow> 1 / 1

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (Suc x)) / real (nth_prime x) * (real x * ln (real x) / (real (Suc x) * ln (real (Suc x))))) \<longlonglongrightarrow> 1
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * g x) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
have "g \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<longlonglongrightarrow> 1
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real x * ln (real x) / (real (Suc x) * ln (real (Suc x)))) \<longlonglongrightarrow> 1
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
g \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. f x * g x) \<longlonglongrightarrow> 1
g \<longlonglongrightarrow> 1
[PROOF STEP]
have "(\<lambda>x. if g x = 0 then 0 else f x) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. f x * g x) \<longlonglongrightarrow> 1
g \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>x. if g x = 0 then 0 else f x) \<longlonglongrightarrow> 1
[PROOF STEP]
apply (drule_tac tendsto_divide[OF _ \<open>g \<longlonglongrightarrow> 1\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. g \<longlonglongrightarrow> 1 \<Longrightarrow> 1 \<noteq> 0
 2. \<lbrakk>g \<longlonglongrightarrow> 1; (\<lambda>x. f x * g x / g x) \<longlonglongrightarrow> 1 / 1\<rbrakk> \<Longrightarrow> (\<lambda>x. if g x = 0 then 0 else f x) \<longlonglongrightarrow> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. if g x = 0 then 0 else f x) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. if g x = 0 then 0 else f x) \<longlonglongrightarrow> 1
[PROOF STEP]
have "f \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. if g x = 0 then 0 else f x) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. f \<longlonglongrightarrow> 1
[PROOF STEP]
proof (elim filterlim_mono_eventually)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. nhds 1 \<le> nhds 1
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. (if g x = 0 then 0 else f x) = f x
[PROOF STEP]
have "\<forall>\<^sub>F x in sequentially. (if g (x+3) = 0 then 0
                else f (x+3)) = f (x+3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. (if g (x + 3) = 0 then 0 else f (x + 3)) = f (x + 3)
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. (if real (x + 3) * ln (real (x + 3)) / (real (Suc (x + 3)) * ln (real (Suc (x + 3)))) = 0 then 0 else f (x + 3)) = f (x + 3)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. (if g (x + 3) = 0 then 0 else f (x + 3)) = f (x + 3)

goal (3 subgoals):
 1. nhds 1 \<le> nhds 1
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. (if g x = 0 then 0 else f x) = f x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in sequentially. (if g (x + 3) = 0 then 0 else f (x + 3)) = f (x + 3)
[PROOF STEP]
show "\<forall>\<^sub>F x in sequentially. (if g x = 0 then 0 else f x) = f x"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. (if g (x + 3) = 0 then 0 else f (x + 3)) = f (x + 3)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. (if g x = 0 then 0 else f x) = f x
[PROOF STEP]
apply (subst (asm) eventually_sequentially_seg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F a in sequentially. (if g a = 0 then 0 else f a) = f a \<Longrightarrow> \<forall>\<^sub>F x in sequentially. (if g x = 0 then 0 else f x) = f x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. (if g x = 0 then 0 else f x) = f x

goal (2 subgoals):
 1. nhds 1 \<le> nhds 1
 2. sequentially \<le> sequentially
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
f \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<longlonglongrightarrow> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real (nth_prime (Suc x)) / real (nth_prime x)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real (nth_prime (n + 1)) / real (nth_prime n)) \<longlonglongrightarrow> 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_prime_double_sqrt_less:
  assumes "\<epsilon> > 0"
  shows "\<forall>\<^sub>F n in sequentially. (nth_prime (2*n) - nth_prime n)
            / sqrt (nth_prime n) < n powr (1/2+\<epsilon>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
define pp ll where
    "pp=(\<lambda>n. (nth_prime (2*n) - nth_prime n) / sqrt (nth_prime n))" and
    "ll=(\<lambda>x::nat. x * ln x)"
[PROOF STATE]
proof (state)
this:
pp = (\<lambda>n. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)))
ll = (\<lambda>x. real x * ln (real x))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
have pp_pos:"pp (n+1) > 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < pp (n + 1)
[PROOF STEP]
unfolding pp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < real (nth_prime (2 * (n + 1)) - nth_prime (n + 1)) / sqrt (real (nth_prime (n + 1)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < pp (?n + 1)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
have "(\<lambda>x. nth_prime (2 * x)) \<sim>[sequentially] (\<lambda>x. (2 * x) * ln (2 * x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real (2 * x)))
[PROOF STEP]
using nth_prime_asymptotics[THEN asymp_equiv_compose
        ,of "(*) 2" sequentially,unfolded comp_def]
[PROOF STATE]
proof (prove)
using this:
filterlim ((*) 2) sequentially sequentially \<Longrightarrow> (\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real (2 * x)))

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real (2 * x)))
[PROOF STEP]
using mult_nat_left_at_top pos2
[PROOF STATE]
proof (prove)
using this:
filterlim ((*) 2) sequentially sequentially \<Longrightarrow> (\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real (2 * x)))
0 < ?c \<Longrightarrow> filterlim ((*) ?c) sequentially sequentially
0 < 2

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real (2 * x)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real (2 * x)))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real (2 * x)))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
have "... \<sim>[sequentially] (\<lambda>x. 2 *x * ln x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real (2 * x) * ln (real (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real x))
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (2 * x) * ln (real (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real x))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>c d. c \<sim>[sequentially] d \<Longrightarrow> c \<sim>[sequentially] d) \<Longrightarrow> (\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>a. real (2 * a) * ln (real a))
[PROOF STEP]
have "(\<lambda>x. nth_prime (2 * x)) \<sim>[sequentially] (\<lambda>x. 2 *x * ln x)"
[PROOF STATE]
proof (prove)
using this:
(\<And>c d. c \<sim>[sequentially] d \<Longrightarrow> c \<sim>[sequentially] d) \<Longrightarrow> (\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>a. real (2 * a) * ln (real a))

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime (2 * x))) \<sim>[sequentially] (\<lambda>x. real (2 * x) * ln (real x))

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
from this[unfolded asymp_equiv_def, THEN tendsto_mult_left,of 2]
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. 2 * (if real (nth_prime (2 * x)) = 0 \<and> real (2 * x) * ln (real x) = 0 then 1 else real (nth_prime (2 * x)) / (real (2 * x) * ln (real x)))) \<longlonglongrightarrow> 2 * 1
[PROOF STEP]
have "(\<lambda>x. nth_prime (2 * x) / (x * ln x)) \<longlonglongrightarrow> 2"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. 2 * (if real (nth_prime (2 * x)) = 0 \<and> real (2 * x) * ln (real x) = 0 then 1 else real (nth_prime (2 * x)) / (real (2 * x) * ln (real x)))) \<longlonglongrightarrow> 2 * 1

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x))) \<longlonglongrightarrow> 2
[PROOF STEP]
unfolding asymp_equiv_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. 2 * (if real (nth_prime (2 * x)) = 0 \<and> real (2 * x) * ln (real x) = 0 then 1 else real (nth_prime (2 * x)) / (real (2 * x) * ln (real x)))) \<longlonglongrightarrow> 2 * 1

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x))) \<longlonglongrightarrow> 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x))) \<longlonglongrightarrow> 2

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x))) \<longlonglongrightarrow> 2

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
have *:"(\<lambda>x. nth_prime x / (x * ln x)) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
using nth_prime_asymptotics
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real (nth_prime n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
unfolding asymp_equiv_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. if real (nth_prime x) = 0 \<and> real x * ln (real x) = 0 then 1 else real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x))) \<longlonglongrightarrow> 2
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
have "(\<lambda>x. (nth_prime (2 * x) - nth_prime x) / ll x) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x))) \<longlonglongrightarrow> 2
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / ll x) \<longlonglongrightarrow> 1
[PROOF STEP]
unfolding ll_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x))) \<longlonglongrightarrow> 2
(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x))) \<longlonglongrightarrow> 2; (\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1\<rbrakk> \<Longrightarrow> (\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
apply (drule (1) tendsto_diff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1; (\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x)) - real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 2 - 1\<rbrakk> \<Longrightarrow> (\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
apply (subst of_nat_diff,simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1; (\<lambda>x. real (nth_prime (2 * x)) / (real x * ln (real x)) - real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 2 - 1\<rbrakk> \<Longrightarrow> (\<lambda>x. (real (nth_prime (2 * x)) - real (nth_prime x)) / (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
by (subst diff_divide_distrib,simp)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / ll x) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / ll x) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
have "(\<lambda>x. sqrt (nth_prime x) / sqrt (ll x)) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sqrt (real (nth_prime x)) / sqrt (ll x)) \<longlonglongrightarrow> 1
[PROOF STEP]
unfolding ll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sqrt (real (nth_prime x)) / sqrt (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
using tendsto_real_sqrt[OF *]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. sqrt (real (nth_prime x) / (real x * ln (real x)))) \<longlonglongrightarrow> sqrt 1

goal (1 subgoal):
 1. (\<lambda>x. sqrt (real (nth_prime x)) / sqrt (real x * ln (real x))) \<longlonglongrightarrow> 1
[PROOF STEP]
by (auto simp: real_sqrt_divide)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. sqrt (real (nth_prime x)) / sqrt (ll x)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / ll x) \<longlonglongrightarrow> 1
(\<lambda>x. sqrt (real (nth_prime x)) / sqrt (ll x)) \<longlonglongrightarrow> 1
[PROOF STEP]
have "(\<lambda>x. pp x * (sqrt (ll x) / (ll x))) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / ll x) \<longlonglongrightarrow> 1
(\<lambda>x. sqrt (real (nth_prime x)) / sqrt (ll x)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>x. pp x * (sqrt (ll x) / ll x)) \<longlonglongrightarrow> 1
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / ll x) \<longlonglongrightarrow> 1; (\<lambda>x. sqrt (real (nth_prime x)) / sqrt (ll x)) \<longlonglongrightarrow> 1\<rbrakk> \<Longrightarrow> (\<lambda>x. pp x * (sqrt (ll x) / ll x)) \<longlonglongrightarrow> 1
[PROOF STEP]
apply (drule (1) tendsto_divide,simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. sqrt (real (nth_prime x)) / sqrt (ll x)) \<longlonglongrightarrow> 1; (\<lambda>x. real (nth_prime (2 * x) - nth_prime x) / ll x / (sqrt (real (nth_prime x)) / sqrt (ll x))) \<longlonglongrightarrow> 1 / 1\<rbrakk> \<Longrightarrow> (\<lambda>x. pp x * (sqrt (ll x) / ll x)) \<longlonglongrightarrow> 1
[PROOF STEP]
by (auto simp:field_simps of_nat_diff pp_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pp x * (sqrt (ll x) / ll x)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pp x * (sqrt (ll x) / ll x)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
have "\<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1/sqrt (ll x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1 / sqrt (ll x)
[PROOF STEP]
apply (subst eventually_sequentially_Suc[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F i in sequentially. sqrt (ll (Suc i)) / ll (Suc i) = 1 / sqrt (ll (Suc i))
[PROOF STEP]
by (auto intro!:eventuallyI simp:ll_def divide_simps)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1 / sqrt (ll x)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. pp x * (sqrt (ll x) / ll x)) \<longlonglongrightarrow> 1
\<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1 / sqrt (ll x)
[PROOF STEP]
have "(\<lambda>x. pp x / sqrt (ll x)) \<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. pp x * (sqrt (ll x) / ll x)) \<longlonglongrightarrow> 1
\<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1 / sqrt (ll x)

goal (1 subgoal):
 1. (\<lambda>x. pp x / sqrt (ll x)) \<longlonglongrightarrow> 1
[PROOF STEP]
apply (elim filterlim_mono_eventually)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1 / sqrt (ll x) \<Longrightarrow> nhds 1 \<le> nhds 1
 2. \<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1 / sqrt (ll x) \<Longrightarrow> sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1 / sqrt (ll x) \<Longrightarrow> \<forall>\<^sub>F x in sequentially. pp x * (sqrt (ll x) / ll x) = pp x / sqrt (ll x)
[PROOF STEP]
by (auto elim!:eventually_mono) (metis mult.right_neutral times_divide_eq_right)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pp x / sqrt (ll x)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pp x / sqrt (ll x)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
have "(\<lambda>x. sqrt (ll x) / x powr (1/2+\<epsilon>)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sqrt (ll x) / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0
[PROOF STEP]
unfolding ll_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sqrt (real x * ln (real x)) / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0
[PROOF STEP]
using \<open>\<epsilon>>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon>

goal (1 subgoal):
 1. (\<lambda>x. sqrt (real x * ln (real x)) / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0
[PROOF STEP]
by real_asymp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. sqrt (ll x) / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. pp x / sqrt (ll x)) \<longlonglongrightarrow> 1
(\<lambda>x. sqrt (ll x) / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>x. pp x / x powr (1/2+\<epsilon>) *
                      (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. pp x / sqrt (ll x)) \<longlonglongrightarrow> 1
(\<lambda>x. sqrt (ll x) / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>) * (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. pp x / sqrt (ll x)) \<longlonglongrightarrow> 1; (\<lambda>x. sqrt (ll x) / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>) * (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (drule (1) tendsto_mult)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. sqrt (ll x) / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0; (\<lambda>x. pp x / sqrt (ll x) * (sqrt (ll x) / real x powr (1 / 2 + \<epsilon>))) \<longlonglongrightarrow> 1 * 0\<rbrakk> \<Longrightarrow> (\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>) * (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0
[PROOF STEP]
by (auto elim:filterlim_mono_eventually)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>) * (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>) * (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
have "\<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1
[PROOF STEP]
apply (subst eventually_sequentially_Suc[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F i in sequentially. sqrt (ll (Suc i)) / sqrt (ll (Suc i)) = 1
[PROOF STEP]
by (auto intro!:eventuallyI simp:ll_def )
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>) * (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0
\<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1
[PROOF STEP]
have "(\<lambda>x. pp x / x powr (1/2+\<epsilon>)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>) * (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0
\<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1

goal (1 subgoal):
 1. (\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (elim filterlim_mono_eventually)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1 \<Longrightarrow> nhds 0 \<le> nhds 0
 2. \<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1 \<Longrightarrow> sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1 \<Longrightarrow> \<forall>\<^sub>F x in sequentially. pp x / real x powr (1 / 2 + \<epsilon>) * (sqrt (ll x) / sqrt (ll x)) = pp x / real x powr (1 / 2 + \<epsilon>)
[PROOF STEP]
by (auto elim:eventually_mono)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. pp x / real x powr (1 / 2 + \<epsilon>)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real (nth_prime (2 * n) - nth_prime n) / sqrt (real (nth_prime n)) < real n powr (1 / 2 + \<epsilon>)
[PROOF STEP]
from tendstoD[OF this, of 1,simplified]
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in sequentially. \<bar>pp x\<bar> / real x powr (1 / 2 + \<epsilon>) < 1
[PROOF STEP]
show "\<forall>\<^sub>F x in sequentially. pp x < x powr (1 / 2 + \<epsilon>)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. \<bar>pp x\<bar> / real x powr (1 / 2 + \<epsilon>) < 1

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. pp x < real x powr (1 / 2 + \<epsilon>)
[PROOF STEP]
apply (elim eventually_mono_sequentially[of _ 1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<bar>pp (x + 1)\<bar> / real (x + 1) powr (1 / 2 + \<epsilon>) < 1 \<Longrightarrow> pp (x + 1) < real (x + 1) powr (1 / 2 + \<epsilon>)
[PROOF STEP]
using pp_pos
[PROOF STATE]
proof (prove)
using this:
0 < pp (?n + 1)

goal (1 subgoal):
 1. \<And>x. \<bar>pp (x + 1)\<bar> / real (x + 1) powr (1 / 2 + \<epsilon>) < 1 \<Longrightarrow> pp (x + 1) < real (x + 1) powr (1 / 2 + \<epsilon>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. pp x < real x powr (1 / 2 + \<epsilon>)

goal:
No subgoals!
[PROOF STEP]
qed