[STATEMENT]
lemma ab_rationality_imp:
  assumes ab_rational:"(\<Sum>n. (b n / (\<Prod>i \<le> n. a i))) \<in> \<rat>"
  shows "\<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)
            \<and> (\<lambda>n. c (Suc n) / a n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<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
[PROOF STEP]
have [simp]:"a n \<noteq> 0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a n \<noteq> 0
[PROOF STEP]
using a_pos
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. a n \<noteq> 0
[PROOF STEP]
by (metis less_numeral_extra(3))
[PROOF STATE]
proof (state)
this:
a ?n \<noteq> 0

goal (1 subgoal):
 1. \<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
[PROOF STEP]
obtain A::int and B::int where
    AB_eq:"(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = A / B" and "B>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_int A / real_of_int B; 0 < B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_int A / real_of_int B; 0 < B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain q::rat where "(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ab_rational
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) \<in> \<rat>

goal (1 subgoal):
 1. (\<And>q. (\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Rats_cases) simp
[PROOF STATE]
proof (state)
this:
(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_int A / real_of_int B; 0 < B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_int A / real_of_int B; 0 < B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain A::int and B::int where "q = Rat.Fract A B" "B > 0" "coprime A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>q = Rat.Fract A B; 0 < B; coprime A B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Rat_cases) auto
[PROOF STATE]
proof (state)
this:
q = Rat.Fract A B
0 < B
coprime A B

goal (1 subgoal):
 1. (\<And>A B. \<lbrakk>(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_int A / real_of_int B; 0 < B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q
q = Rat.Fract A B
0 < B
coprime A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q
q = Rat.Fract A B
0 < B
coprime A B

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto intro!: that[of A B] simp:of_rat_rat)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_int A / real_of_int B
0 < B

goal (1 subgoal):
 1. \<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
[PROOF STEP]
define f where "f \<equiv> (\<lambda>n. b n / real_of_int (prod a {..n}))"
[PROOF STATE]
proof (state)
this:
f \<equiv> \<lambda>n. real_of_int (b n) / real_of_int (prod a {..n})

goal (1 subgoal):
 1. \<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
[PROOF STEP]
define R where "R \<equiv> (\<lambda>N. (\<Sum>n. B*b (n+N+1) / prod a {N..n+N+1}))"
[PROOF STATE]
proof (state)
this:
R \<equiv> \<lambda>N. \<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})

goal (1 subgoal):
 1. \<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
[PROOF STEP]
have all_e_ubound:"\<forall>e>0. \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>B*b (n+M+1) / prod a {M..n+M+1}\<bar> < e/4 * 1/2^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e>0. \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
fix e::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
assume "e>0"
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
obtain N where N_a2: "\<forall>n \<ge> N. a n \<ge> 2"
      and N_ba: "\<forall>n \<ge> N. \<bar>b n\<bar> / (a (n-1) * a n)  < e/(4*B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>n\<ge>N. 2 \<le> a n; \<forall>n\<ge>N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>n\<ge>N. 2 \<le> a n; \<forall>n\<ge>N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. \<bar>b n\<bar> / (a (n - 1) * a n) < e/(4*B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)
[PROOF STEP]
using order_topology_class.order_tendstoD[OF ab_tendsto,of "e/(4*B)"] \<open>B>0\<close> \<open>e>0\<close>
[PROOF STATE]
proof (prove)
using this:
e / real_of_int (4 * B) < 0 \<Longrightarrow> \<forall>\<^sub>F x in sequentially. e / real_of_int (4 * B) < real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x)
0 < e / real_of_int (4 * B) \<Longrightarrow> \<forall>\<^sub>F x in sequentially. real_of_int \<bar>b x\<bar> / real_of_int (a (x - 1) * a x) < e / real_of_int (4 * B)
0 < B
0 < e

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>n\<ge>N. 2 \<le> a n; \<forall>n\<ge>N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>n\<ge>N. 2 \<le> a n; \<forall>n\<ge>N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. a n \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 2 \<le> a n
[PROOF STEP]
using a_large
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. 1 < a n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. 2 \<le> a n
[PROOF STEP]
by (auto elim: eventually_mono)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. 2 \<le> a n

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>n\<ge>N. 2 \<le> a n; \<forall>n\<ge>N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)
\<forall>\<^sub>F n in sequentially. 2 \<le> a n
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. \<bar>b n\<bar> / (a (n - 1) * a n) < e/(4*B) \<and> a n \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)
\<forall>\<^sub>F n in sequentially. 2 \<le> a n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B) \<and> 2 \<le> a n
[PROOF STEP]
by eventually_elim auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B) \<and> 2 \<le> a n

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

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B) \<and> 2 \<le> a n

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B) \<and> 2 \<le> a n
\<lbrakk>\<forall>n\<ge>?N. 2 \<le> a n; \<forall>n\<ge>?N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)\<rbrakk> \<Longrightarrow> thesis

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:
\<forall>n\<ge>N. 2 \<le> a n
\<forall>n\<ge>N. real_of_int \<bar>b n\<bar> / real_of_int (a (n - 1) * a n) < e / real_of_int (4 * B)

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
have geq_N_bound:"\<bar>B*b (n+M+1) / prod a {M..n+M+1}\<bar> < e/4 * 1/2^n" when "M\<ge>N" for n M
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
define D where "D = B*b (n+M+1)/ (a (n+M) * a (n+M+1))"
[PROOF STATE]
proof (state)
this:
D = real_of_int (B * b (n + M + 1)) / real_of_int (a (n + M) * a (n + M + 1))

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
have "\<bar>B*b (n+M+1) / prod a {M..n+M+1}\<bar> = \<bar>D / prod a {M..<n+M}\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> = \<bar>D / real_of_int (prod a {M..<n + M})\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> = \<bar>D / real_of_int (prod a {M..<n + M})\<bar>
[PROOF STEP]
have "{M..n+M+1} = {M..<n+M} \<union> {n+M,n+M+1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {M..n + M + 1} = {M..<n + M} \<union> {n + M, n + M + 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{M..n + M + 1} = {M..<n + M} \<union> {n + M, n + M + 1}

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> = \<bar>D / real_of_int (prod a {M..<n + M})\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{M..n + M + 1} = {M..<n + M} \<union> {n + M, n + M + 1}
[PROOF STEP]
have "prod a {M..n+M+1} = a (n+M) * a (n+M+1)* prod a {M..<n+M}"
[PROOF STATE]
proof (prove)
using this:
{M..n + M + 1} = {M..<n + M} \<union> {n + M, n + M + 1}

goal (1 subgoal):
 1. prod a {M..n + M + 1} = a (n + M) * a (n + M + 1) * prod a {M..<n + M}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prod a {M..n + M + 1} = a (n + M) * a (n + M + 1) * prod a {M..<n + M}

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> = \<bar>D / real_of_int (prod a {M..<n + M})\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
prod a {M..n + M + 1} = a (n + M) * a (n + M + 1) * prod a {M..<n + M}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod a {M..n + M + 1} = a (n + M) * a (n + M + 1) * prod a {M..<n + M}

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> = \<bar>D / real_of_int (prod a {M..<n + M})\<bar>
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
using this:
prod a {M..n + M + 1} = a (n + M) * a (n + M + 1) * prod a {M..<n + M}

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> = \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (a (n + M) * a (n + M + 1)) / real_of_int (prod a {M..<n + M})\<bar>
[PROOF STEP]
by (simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> = \<bar>D / real_of_int (prod a {M..<n + M})\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> = \<bar>D / real_of_int (prod a {M..<n + M})\<bar>

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

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
have "... <  \<bar>e/4 * (1/prod a {M..<n+M})\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>D / real_of_int (prod a {M..<n + M})\<bar> < \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>D / real_of_int (prod a {M..<n + M})\<bar> < \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar>
[PROOF STEP]
have "\<bar>D\<bar> < e/4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>D\<bar> < e / 4
[PROOF STEP]
unfolding D_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (a (n + M) * a (n + M + 1))\<bar> < e / 4
[PROOF STEP]
using N_ba[rule_format, of "n+M+1"] \<open>B>0\<close> \<open>M \<ge> N\<close> \<open>e>0\<close> a_pos
[PROOF STATE]
proof (prove)
using this:
N \<le> n + M + 1 \<Longrightarrow> real_of_int \<bar>b (n + M + 1)\<bar> / real_of_int (a (n + M + 1 - 1) * a (n + M + 1)) < e / real_of_int (4 * B)
0 < B
N \<le> M
0 < e
\<forall>n. 0 < a n

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (a (n + M) * a (n + M + 1))\<bar> < e / 4
[PROOF STEP]
by (auto simp:field_simps abs_mult abs_of_pos)
[PROOF STATE]
proof (state)
this:
\<bar>D\<bar> < e / 4

goal (1 subgoal):
 1. \<bar>D / real_of_int (prod a {M..<n + M})\<bar> < \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar>
[PROOF STEP]
from mult_strict_right_mono[OF this,of "1/prod a {M..<n+M}"] a_pos \<open>e>0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 < 1 / real_of_int (prod a {M..<n + M}) \<Longrightarrow> \<bar>D\<bar> * (1 / real_of_int (prod a {M..<n + M})) < e / 4 * (1 / real_of_int (prod a {M..<n + M}))
\<forall>n. 0 < a n
0 < e
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < 1 / real_of_int (prod a {M..<n + M}) \<Longrightarrow> \<bar>D\<bar> * (1 / real_of_int (prod a {M..<n + M})) < e / 4 * (1 / real_of_int (prod a {M..<n + M}))
\<forall>n. 0 < a n
0 < e

goal (1 subgoal):
 1. \<bar>D / real_of_int (prod a {M..<n + M})\<bar> < \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar>
[PROOF STEP]
apply (auto simp:abs_prod abs_mult prod_pos)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<bar>D\<bar> / (\<Prod>x = M..<n + M. real_of_int (a x)) < e / (4 * (\<Prod>x = M..<n + M. real_of_int (a x))); \<forall>n. 0 < a n; 0 < e\<rbrakk> \<Longrightarrow> \<bar>D\<bar> / (\<Prod>x = M..<n + M. \<bar>real_of_int (a x)\<bar>) < e / (4 * (\<Prod>x = M..<n + M. \<bar>real_of_int (a x)\<bar>))
[PROOF STEP]
by (subst (2) abs_of_pos,auto)+
[PROOF STATE]
proof (state)
this:
\<bar>D / real_of_int (prod a {M..<n + M})\<bar> < \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>D / real_of_int (prod a {M..<n + M})\<bar> < \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar>

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>D / real_of_int (prod a {M..<n + M})\<bar> < \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar>

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

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

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

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

goal (1 subgoal):
 1. 2 ^ Suc n \<le> prod a {M..<Suc n + M}
[PROOF STEP]
using \<open>M\<ge>N\<close>
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> prod a {M..<n + M}
N \<le> M

goal (1 subgoal):
 1. 2 ^ Suc n \<le> prod a {M..<Suc n + M}
[PROOF STEP]
by (simp add: N_a2 mult.commute mult_mono' prod.atLeastLessThan_Suc)
[PROOF STATE]
proof (state)
this:
2 ^ Suc n \<le> prod a {M..<Suc n + M}

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

goal (1 subgoal):
 1. \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar> \<le> e / 4 * 1 / 2 ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ n \<le> prod a {M..<n + M}
[PROOF STEP]
have "real_of_int (prod a {M..<n+M}) \<ge> 2^n"
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> prod a {M..<n + M}

goal (1 subgoal):
 1. 2 ^ n \<le> real_of_int (prod a {M..<n + M})
[PROOF STEP]
using numeral_power_le_of_int_cancel_iff
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> prod a {M..<n + M}
(numeral ?x ^ ?n \<le> of_int ?a) = (numeral ?x ^ ?n \<le> ?a)

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

goal (1 subgoal):
 1. \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar> \<le> e / 4 * 1 / 2 ^ n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ n \<le> real_of_int (prod a {M..<n + M})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> real_of_int (prod a {M..<n + M})

goal (1 subgoal):
 1. \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar> \<le> e / 4 * 1 / 2 ^ n
[PROOF STEP]
using \<open>e>0\<close>
[PROOF STATE]
proof (prove)
using this:
2 ^ n \<le> real_of_int (prod a {M..<n + M})
0 < e

goal (1 subgoal):
 1. \<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar> \<le> e / 4 * 1 / 2 ^ n
[PROOF STEP]
by (auto simp add:divide_simps)
[PROOF STATE]
proof (state)
this:
\<bar>e / 4 * (1 / real_of_int (prod a {M..<n + M}))\<bar> \<le> e / 4 * 1 / 2 ^ n

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

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n

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

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
show "\<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1))
                / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
apply (rule eventually_sequentiallyI[of N])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. N \<le> x \<Longrightarrow> \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
using geq_N_bound
[PROOF STATE]
proof (prove)
using this:
N \<le> ?M \<Longrightarrow> \<bar>real_of_int (B * b (?n + ?M + 1)) / real_of_int (prod a {?M..?n + ?M + 1})\<bar> < e / 4 * 1 / 2 ^ ?n

goal (1 subgoal):
 1. \<And>x. N \<le> x \<Longrightarrow> \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>e>0. \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n

goal (1 subgoal):
 1. \<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
[PROOF STEP]
have R_tendsto_0:"R \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<longlonglongrightarrow> 0
[PROOF STEP]
proof (rule tendstoI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in sequentially. dist (R x) 0 < e
[PROOF STEP]
fix e::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in sequentially. dist (R x) 0 < e
[PROOF STEP]
assume "e>0"
[PROOF STATE]
proof (state)
this:
0 < e

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F x in sequentially. dist (R x) 0 < e
[PROOF STEP]
show "\<forall>\<^sub>F x in sequentially. dist (R x) 0 < e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. dist (R x) 0 < e
[PROOF STEP]
using all_e_ubound[rule_format,OF \<open>e>0\<close>]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. dist (R x) 0 < e
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
case (elim M)
[PROOF STATE]
proof (state)
this:
\<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
define g where "g = (\<lambda>n. B*b (n+M+1) / prod a {M..n+M+1})"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>n. real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1}))

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
have g_lt:"\<bar>g n\<bar> < e/4 * 1/2^n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>g n\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
using elim
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n

goal (1 subgoal):
 1. \<bar>g n\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>g ?n\<bar> < e / 4 * 1 / 2 ^ ?n

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
have \<section>: "summable (\<lambda>n. (e/4) * (1/2)^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. e / 4 * (1 / 2) ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. e / 4 * (1 / 2) ^ n)

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
summable (\<lambda>n. e / 4 * (1 / 2) ^ n)
[PROOF STEP]
have g_abs_summable:"summable (\<lambda>n. \<bar>g n\<bar>)"
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. e / 4 * (1 / 2) ^ n)

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>g n\<bar>)
[PROOF STEP]
apply (elim summable_comparison_test')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. ?N1 \<le> n \<Longrightarrow> norm \<bar>g n\<bar> \<le> e / 4 * (1 / 2) ^ n
[PROOF STEP]
by (metis abs_idempotent g_lt less_eq_real_def power_one_over real_norm_def times_divide_eq_right)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>g n\<bar>)

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
have "\<bar>\<Sum>n. g n\<bar> \<le> (\<Sum>n. \<bar>g n\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>\<Sum>n. g n\<bar> \<le> (\<Sum>n. \<bar>g n\<bar>)
[PROOF STEP]
by (rule summable_rabs[OF g_abs_summable])
[PROOF STATE]
proof (state)
this:
\<bar>\<Sum>n. g n\<bar> \<le> (\<Sum>n. \<bar>g n\<bar>)

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>\<Sum>n. g n\<bar> \<le> (\<Sum>n. \<bar>g n\<bar>)

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
have "... \<le>(\<Sum>n. e/4 * 1/2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. \<bar>g n\<bar>) \<le> (\<Sum>n. e / 4 * 1 / 2 ^ n)
[PROOF STEP]
proof (rule suminf_comparison)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. summable (\<lambda>n. e / 4 * 1 / 2 ^ n)
 2. \<And>n. norm \<bar>g n\<bar> \<le> e / 4 * 1 / 2 ^ n
[PROOF STEP]
show "summable (\<lambda>n. e/4 * 1/2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. e / 4 * 1 / 2 ^ n)
[PROOF STEP]
using \<section>
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. e / 4 * (1 / 2) ^ n)

goal (1 subgoal):
 1. summable (\<lambda>n. e / 4 * 1 / 2 ^ n)
[PROOF STEP]
unfolding power_divide
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. e / 4 * (1 ^ n / 2 ^ n))

goal (1 subgoal):
 1. summable (\<lambda>n. e / 4 * 1 / 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. e / 4 * 1 / 2 ^ n)

goal (1 subgoal):
 1. \<And>n. norm \<bar>g n\<bar> \<le> e / 4 * 1 / 2 ^ n
[PROOF STEP]
show "\<And>n. norm \<bar>g n\<bar> \<le> e / 4 * 1 / 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. norm \<bar>g n\<bar> \<le> e / 4 * 1 / 2 ^ n
[PROOF STEP]
using g_lt less_eq_real_def
[PROOF STATE]
proof (prove)
using this:
\<bar>g ?n\<bar> < e / 4 * 1 / 2 ^ ?n
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)

goal (1 subgoal):
 1. \<And>n. norm \<bar>g n\<bar> \<le> e / 4 * 1 / 2 ^ n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
norm \<bar>g ?n\<bar> \<le> e / 4 * 1 / 2 ^ ?n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<bar>g n\<bar>) \<le> (\<Sum>n. e / 4 * 1 / 2 ^ n)

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. \<bar>g n\<bar>) \<le> (\<Sum>n. e / 4 * 1 / 2 ^ n)

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
have "... = (e/4) * (\<Sum>n. (1/2)^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. e / 4 * 1 / 2 ^ n) = e / 4 * (\<Sum>n. (1 / 2) ^ n)
[PROOF STEP]
apply (subst suminf_mult[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. summable ((^) (1 / 2))
 2. (\<Sum>n. e / 4 * 1 / 2 ^ n) = (\<Sum>n. e / 4 * (1 / 2) ^ n)
[PROOF STEP]
by (auto simp: algebra_simps power_divide)
[PROOF STATE]
proof (state)
this:
(\<Sum>n. e / 4 * 1 / 2 ^ n) = e / 4 * (\<Sum>n. (1 / 2) ^ n)

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. e / 4 * 1 / 2 ^ n) = e / 4 * (\<Sum>n. (1 / 2) ^ n)

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
have "... = e/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e / 4 * (\<Sum>n. (1 / 2) ^ n) = e / 2
[PROOF STEP]
by (simp add:suminf_geometric[of "1/2"])
[PROOF STATE]
proof (state)
this:
e / 4 * (\<Sum>n. (1 / 2) ^ n) = e / 2

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<bar>\<Sum>n. g n\<bar> \<le> e / 2
[PROOF STEP]
have "\<bar>\<Sum>n. g n\<bar> \<le> e / 2"
[PROOF STATE]
proof (prove)
using this:
\<bar>\<Sum>n. g n\<bar> \<le> e / 2

goal (1 subgoal):
 1. \<bar>\<Sum>n. g n\<bar> \<le> e / 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>\<Sum>n. g n\<bar> \<le> e / 2

goal (1 subgoal):
 1. \<And>x. \<forall>n. \<bar>real_of_int (B * b (n + x + 1)) / real_of_int (prod a {x..n + x + 1})\<bar> < e / 4 * 1 / 2 ^ n \<Longrightarrow> dist (R x) 0 < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<bar>\<Sum>n. g n\<bar> \<le> e / 2
[PROOF STEP]
show "dist (R M) 0 < e"
[PROOF STATE]
proof (prove)
using this:
\<bar>\<Sum>n. g n\<bar> \<le> e / 2

goal (1 subgoal):
 1. dist (R M) 0 < e
[PROOF STEP]
unfolding R_def g_def
[PROOF STATE]
proof (prove)
using this:
\<bar>\<Sum>n. real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> \<le> e / 2

goal (1 subgoal):
 1. dist (\<Sum>n. real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})) 0 < e
[PROOF STEP]
using \<open>e>0\<close>
[PROOF STATE]
proof (prove)
using this:
\<bar>\<Sum>n. real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> \<le> e / 2
0 < e

goal (1 subgoal):
 1. dist (\<Sum>n. real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})) 0 < e
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dist (R M) 0 < e

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. dist (R x) 0 < e

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

goal (1 subgoal):
 1. \<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
[PROOF STEP]
obtain N where R_N_bound:"\<forall>M \<ge> N. \<bar>R M\<bar> \<le>  1 / 4"
    and N_geometric:"\<forall>M\<ge>N. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>M\<ge>N. \<bar>R M\<bar> \<le> 1 / 4; \<forall>M\<ge>N. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>M\<ge>N. \<bar>R M\<bar> \<le> 1 / 4; \<forall>M\<ge>N. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain N1 where N1:"\<forall>M \<ge> N1. \<bar>R M\<bar> \<le>  1 / 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N1. \<forall>M\<ge>N1. \<bar>R M\<bar> \<le> 1 / 4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using metric_LIMSEQ_D[OF R_tendsto_0,of "1/4"] all_e_ubound[rule_format,of 4,unfolded eventually_sequentially]
[PROOF STATE]
proof (prove)
using this:
0 < 1 / 4 \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (R n) 0 < 1 / 4
0 < 4 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>na. \<bar>real_of_int (B * b (na + n + 1)) / real_of_int (prod a {n..na + n + 1})\<bar> < 4 / 4 * 1 / 2 ^ na

goal (1 subgoal):
 1. (\<And>N1. \<forall>M\<ge>N1. \<bar>R M\<bar> \<le> 1 / 4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp:less_eq_real_def)
[PROOF STATE]
proof (state)
this:
\<forall>M\<ge>N1. \<bar>R M\<bar> \<le> 1 / 4

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>M\<ge>N. \<bar>R M\<bar> \<le> 1 / 4; \<forall>M\<ge>N. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain N2 where N2:"\<forall>M\<ge>N2. \<forall>n. \<bar>real_of_int (B * b (n + M + 1))
                          / (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N2. \<forall>M\<ge>N2. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using all_e_ubound[rule_format,of 4,unfolded eventually_sequentially]
[PROOF STATE]
proof (prove)
using this:
0 < 4 \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>na. \<bar>real_of_int (B * b (na + n + 1)) / real_of_int (prod a {n..na + n + 1})\<bar> < 4 / 4 * 1 / 2 ^ na

goal (1 subgoal):
 1. (\<And>N2. \<forall>M\<ge>N2. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp:less_eq_real_def)
[PROOF STATE]
proof (state)
this:
\<forall>M\<ge>N2. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>M\<ge>N. \<bar>R M\<bar> \<le> 1 / 4; \<forall>M\<ge>N. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define N where "N=max N1 N2"
[PROOF STATE]
proof (state)
this:
N = max N1 N2

goal (1 subgoal):
 1. (\<And>N. \<lbrakk>\<forall>M\<ge>N. \<bar>R M\<bar> \<le> 1 / 4; \<forall>M\<ge>N. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of N] N1 N2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>M\<ge>N. \<bar>R M\<bar> \<le> 1 / 4; \<forall>M\<ge>N. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n\<rbrakk> \<Longrightarrow> thesis
\<forall>M\<ge>N1. \<bar>R M\<bar> \<le> 1 / 4
\<forall>M\<ge>N2. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>M\<ge>max N1 N2. \<bar>R M\<bar> \<le> 1 / 4; \<forall>M\<ge>max N1 N2. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n\<rbrakk> \<Longrightarrow> thesis
\<forall>M\<ge>N1. \<bar>R M\<bar> \<le> 1 / 4
\<forall>M\<ge>N2. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n

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

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

goal (1 subgoal):
 1. \<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
[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. \<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
[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]
using aux_series_summable
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))

goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
summable f

goal (1 subgoal):
 1. \<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
[PROOF STEP]
have "A * prod a {..<N} = C + B * b N / a N  + R N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (A * prod a {..<N}) = C + real_of_int (B * b N) / real_of_int (a N) + R N
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (A * prod a {..<N}) = C + real_of_int (B * b N) / real_of_int (a N) + R N
[PROOF STEP]
have "A * prod a {..<N} = B * prod a {..<N} * (\<Sum>n. f n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (A * prod a {..<N}) = real_of_int (B * prod a {..<N}) * (\<Sum>n. f n)
[PROOF STEP]
unfolding AB_eq f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (A * prod a {..<N}) = real_of_int (B * prod a {..<N}) * (real_of_int A / real_of_int B)
[PROOF STEP]
using \<open>B>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < B

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

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

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

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

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

goal (1 subgoal):
 1. real_of_int (A * prod a {..<N}) = C + real_of_int (B * b N) / real_of_int (a N) + R N
[PROOF STEP]
have "... = B * prod a {..<N} * ((\<Sum>n<N. f n) + f N + (\<Sum>n. f (n+N+1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (sum f {..<N + 1} + (\<Sum>n. f (n + N + 1))) = real_of_int (B * prod a {..<N}) * (sum f {..<N} + f N + (\<Sum>n. f (n + N + 1)))
[PROOF STEP]
using sum.atLeast0_lessThan_Suc
[PROOF STATE]
proof (prove)
using this:
sum ?g {0..<Suc ?n} = sum ?g {0..<?n} + ?g ?n

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

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

goal (1 subgoal):
 1. real_of_int (A * prod a {..<N}) = C + real_of_int (B * b N) / real_of_int (a N) + R N
[PROOF STEP]
have "... = C + B * b N / a N + (\<Sum>n. B*b (n+N+1) / prod a {N..n+N+1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (sum f {..<N} + f N + (\<Sum>n. f (n + N + 1))) = C + real_of_int (B * b N) / real_of_int (a N) + (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (sum f {..<N} + f N + (\<Sum>n. f (n + N + 1))) = C + real_of_int (B * b N) / real_of_int (a N) + (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
have "B * prod a {..<N} * f N = B * b N / a N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f N = real_of_int (B * b N) / real_of_int (a N)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f N = real_of_int (B * b N) / real_of_int (a N)
[PROOF STEP]
have "{..N} =  {..<N} \<union> {N}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..N} = {..<N} \<union> {N}
[PROOF STEP]
using ivl_disj_un_singleton(2)
[PROOF STATE]
proof (prove)
using this:
{..<?u} \<union> {?u} = {..?u}

goal (1 subgoal):
 1. {..N} = {..<N} \<union> {N}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{..N} = {..<N} \<union> {N}

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

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * f N = real_of_int (B * b N) / real_of_int (a N)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
{..N} = {..<N} \<union> {N}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * f N = real_of_int (B * b N) / real_of_int (a N)

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

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (sum f {..<N} + f N + (\<Sum>n. f (n + N + 1))) = C + real_of_int (B * b N) / real_of_int (a N) + (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
have "B * prod a {..<N} * (\<Sum>n. f (n+N+1)) = (\<Sum>n. B*b (n+N+1) / prod a {N..n+N+1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N + 1)) = (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N + 1)) = (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
have "summable (\<lambda>n. f (n + N + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. f (n + N + 1))
[PROOF STEP]
using \<open>summable f\<close> summable_iff_shift[of f "N+1"]
[PROOF STATE]
proof (prove)
using this:
summable f
summable (\<lambda>n. f (n + (N + 1))) = summable f

goal (1 subgoal):
 1. summable (\<lambda>n. f (n + N + 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. f (n + N + 1))

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

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N + 1)) = (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
have "prod a {..<N} * f (n + N + 1) = b (n + N + 1) / prod a {N..n + N + 1}" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (prod a {..<N}) * f (n + N + 1) = real_of_int (b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (prod a {..<N}) * f (n + N + 1) = real_of_int (b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})
[PROOF STEP]
have "{..n + N + 1} = {..<N} \<union> {N..n + N + 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..n + N + 1} = {..<N} \<union> {N..n + N + 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{..n + N + 1} = {..<N} \<union> {N..n + N + 1}

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

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

goal (1 subgoal):
 1. real_of_int (prod a {..<N}) * (real_of_int (b (n + N + 1)) / real_of_int (prod a {..n + N + 1})) = real_of_int (b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..Suc (n + N)} = {..<N} \<union> {N..Suc (n + N)} \<Longrightarrow> (\<Prod>x<N. real_of_int (a x)) * real_of_int (b (Suc (n + N))) / (\<Prod>x\<in>{..<N} \<union> {N..Suc (n + N)}. real_of_int (a x)) = real_of_int (b (Suc (n + N))) / ((\<Prod>x = N..n + N. real_of_int (a x)) * real_of_int (a (Suc (n + N))))
[PROOF STEP]
apply (subst prod.union_disjoint)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {..Suc (n + N)} = {..<N} \<union> {N..Suc (n + N)} \<Longrightarrow> finite {..<N}
 2. {..Suc (n + N)} = {..<N} \<union> {N..Suc (n + N)} \<Longrightarrow> finite {N..Suc (n + N)}
 3. {..Suc (n + N)} = {..<N} \<union> {N..Suc (n + N)} \<Longrightarrow> {..<N} \<inter> {N..Suc (n + N)} = {}
 4. {..Suc (n + N)} = {..<N} \<union> {N..Suc (n + N)} \<Longrightarrow> (\<Prod>x<N. real_of_int (a x)) * real_of_int (b (Suc (n + N))) / ((\<Prod>x<N. real_of_int (a x)) * (\<Prod>x = N..Suc (n + N). real_of_int (a x))) = real_of_int (b (Suc (n + N))) / ((\<Prod>x = N..n + N. real_of_int (a x)) * real_of_int (a (Suc (n + N))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int (prod a {..<N}) * f (n + N + 1) = real_of_int (b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})

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

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

goal (1 subgoal):
 1. real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N + 1)) = (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
apply (subst suminf_mult[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>summable (\<lambda>n. f (n + N + 1)); \<And>n. real_of_int (prod a {..<N}) * f (n + N + 1) = real_of_int (b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})\<rbrakk> \<Longrightarrow> summable (\<lambda>n. f (n + N + 1))
 2. \<lbrakk>summable (\<lambda>n. f (n + N + 1)); \<And>n. real_of_int (prod a {..<N}) * f (n + N + 1) = real_of_int (b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})\<rbrakk> \<Longrightarrow> (\<Sum>n. real_of_int (B * prod a {..<N}) * f (n + N + 1)) = (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
by (auto simp add: mult.commute mult.left_commute)
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N + 1)) = (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * (\<Sum>n. f (n + N + 1)) = (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (B * prod a {..<N}) * (sum f {..<N} + f N + (\<Sum>n. f (n + N + 1))) = C + real_of_int (B * b N) / real_of_int (a N) + (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))

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

goal (1 subgoal):
 1. real_of_int (A * prod a {..<N}) = C + real_of_int (B * b N) / real_of_int (a N) + R N
[PROOF STEP]
have "... = C +B * b N / a N  + R N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C + real_of_int (B * b N) / real_of_int (a N) + (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})) = C + real_of_int (B * b N) / real_of_int (a N) + R N
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C + real_of_int (B * b N) / real_of_int (a N) + (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})) = C + real_of_int (B * b N) / real_of_int (a N) + (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C + real_of_int (B * b N) / real_of_int (a N) + (\<Sum>n. real_of_int (B * b (n + N + 1)) / real_of_int (prod a {N..n + N + 1})) = C + real_of_int (B * b N) / real_of_int (a N) + R N

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

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

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

goal (1 subgoal):
 1. \<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
[PROOF STEP]
have R_bound:"\<bar>R M\<bar> \<le> 1 / 4" and R_Suc:"R (Suc M) = a M * R M - B * b (Suc M) / a (Suc M)"
    when "M \<ge> N" for M
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>R M\<bar> \<le> 1 / 4 &&& R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<bar>R M\<bar> \<le> 1 / 4
 2. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
define g where "g = (\<lambda>n. B*b (n+M+1) / prod a {M..n+M+1})"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>n. real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1}))

goal (2 subgoals):
 1. \<bar>R M\<bar> \<le> 1 / 4
 2. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
have g_abs_summable:"summable (\<lambda>n. \<bar>g n\<bar>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>g n\<bar>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>g n\<bar>)
[PROOF STEP]
have "summable (\<lambda>n. (1/2::real) ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable ((^) (1 / 2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
summable ((^) (1 / 2))

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>g n\<bar>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
summable ((^) (1 / 2))

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>g n\<bar>)
[PROOF STEP]
have "\<bar>g n\<bar> < 1/2^n" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>g n\<bar> < 1 / 2 ^ n
[PROOF STEP]
using N_geometric[rule_format,OF that]
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int (B * b (?n + M + 1)) / real_of_int (prod a {M..?n + M + 1})\<bar> < 1 / 2 ^ ?n

goal (1 subgoal):
 1. \<bar>g n\<bar> < 1 / 2 ^ n
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int (B * b (?n + M + 1)) / real_of_int (prod a {M..?n + M + 1})\<bar> < 1 / 2 ^ ?n

goal (1 subgoal):
 1. \<bar>real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>g ?n\<bar> < 1 / 2 ^ ?n

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

goal (1 subgoal):
 1. summable (\<lambda>n. \<bar>g n\<bar>)
[PROOF STEP]
apply (elim summable_comparison_test')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<And>n. \<bar>g n\<bar> < 1 / 2 ^ n; ?N3 \<le> n\<rbrakk> \<Longrightarrow> norm \<bar>g n\<bar> \<le> (1 / 2) ^ n
[PROOF STEP]
by (simp add: less_eq_real_def power_one_over)
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>g n\<bar>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
summable (\<lambda>n. \<bar>g n\<bar>)

goal (2 subgoals):
 1. \<bar>R M\<bar> \<le> 1 / 4
 2. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
show "\<bar>R M\<bar> \<le> 1 / 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>R M\<bar> \<le> 1 / 4
[PROOF STEP]
using R_N_bound[rule_format,OF that]
[PROOF STATE]
proof (prove)
using this:
\<bar>R M\<bar> \<le> 1 / 4

goal (1 subgoal):
 1. \<bar>R M\<bar> \<le> 1 / 4
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>R M\<bar> \<le> 1 / 4

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
have "R M = (\<Sum>n. g n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R M = (\<Sum>n. g n)
[PROOF STEP]
unfolding R_def g_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1})) = (\<Sum>n. real_of_int (B * b (n + M + 1)) / real_of_int (prod a {M..n + M + 1}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
R M = (\<Sum>n. g n)

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R M = (\<Sum>n. g n)

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
have "... = g 0 + (\<Sum>n. g (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. g n) = g 0 + (\<Sum>n. g (Suc n))
[PROOF STEP]
apply (subst suminf_split_head)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. summable g
 2. suminf g = g 0 + (suminf g - g 0)
[PROOF STEP]
using summable_rabs_cancel[OF g_abs_summable]
[PROOF STATE]
proof (prove)
using this:
summable g

goal (2 subgoals):
 1. summable g
 2. suminf g = g 0 + (suminf g - g 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n. g n) = g 0 + (\<Sum>n. g (Suc n))

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n. g n) = g 0 + (\<Sum>n. g (Suc n))

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
have "... = g 0 + 1/a M * (\<Sum>n. a M * g (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g 0 + (\<Sum>n. g (Suc n)) = g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n))
[PROOF STEP]
apply (subst suminf_mult)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. summable (\<lambda>n. g (Suc n))
 2. g 0 + (\<Sum>n. g (Suc n)) = g 0 + 1 / real_of_int (a M) * (real_of_int (a M) * (\<Sum>n. g (Suc n)))
[PROOF STEP]
by (auto simp add: g_abs_summable summable_Suc_iff summable_rabs_cancel)
[PROOF STATE]
proof (state)
this:
g 0 + (\<Sum>n. g (Suc n)) = g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n))

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
g 0 + (\<Sum>n. g (Suc n)) = g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n))

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
have "... = g 0 + 1/a M * R (Suc M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n)) = g 0 + 1 / real_of_int (a M) * R (Suc M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n)) = g 0 + 1 / real_of_int (a M) * R (Suc M)
[PROOF STEP]
have "a M * g (Suc n) = B * b (n + M + 2) / prod a {Suc M..n + M + 2}" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a M) * g (Suc n) = real_of_int (B * b (n + M + 2)) / real_of_int (prod a {Suc M..n + M + 2})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (a M) * g (Suc n) = real_of_int (B * b (n + M + 2)) / real_of_int (prod a {Suc M..n + M + 2})
[PROOF STEP]
have "{M..Suc (Suc (M + n))} = {M} \<union> {Suc M..Suc (Suc (M + n))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {M..Suc (Suc (M + n))} = {M} \<union> {Suc M..Suc (Suc (M + n))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{M..Suc (Suc (M + n))} = {M} \<union> {Suc M..Suc (Suc (M + n))}

goal (1 subgoal):
 1. real_of_int (a M) * g (Suc n) = real_of_int (B * b (n + M + 2)) / real_of_int (prod a {Suc M..n + M + 2})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{M..Suc (Suc (M + n))} = {M} \<union> {Suc M..Suc (Suc (M + n))}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{M..Suc (Suc (M + n))} = {M} \<union> {Suc M..Suc (Suc (M + n))}

goal (1 subgoal):
 1. real_of_int (a M) * g (Suc n) = real_of_int (B * b (n + M + 2)) / real_of_int (prod a {Suc M..n + M + 2})
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
{M..Suc (Suc (M + n))} = {M} \<union> {Suc M..Suc (Suc (M + n))}

goal (1 subgoal):
 1. real_of_int (a M) * (real_of_int (B * b (Suc n + M + 1)) / real_of_int (prod a {M..Suc n + M + 1})) = real_of_int (B * b (n + M + 2)) / real_of_int (prod a {Suc M..n + M + 2})
[PROOF STEP]
using \<open>B>0\<close>
[PROOF STATE]
proof (prove)
using this:
{M..Suc (Suc (M + n))} = {M} \<union> {Suc M..Suc (Suc (M + n))}
0 < B

goal (1 subgoal):
 1. real_of_int (a M) * (real_of_int (B * b (Suc n + M + 1)) / real_of_int (prod a {M..Suc n + M + 1})) = real_of_int (B * b (n + M + 2)) / real_of_int (prod a {Suc M..n + M + 2})
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (a M) * g (Suc n) = real_of_int (B * b (n + M + 2)) / real_of_int (prod a {Suc M..n + M + 2})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (a M) * g (Suc ?n) = real_of_int (B * b (?n + M + 2)) / real_of_int (prod a {Suc M..?n + M + 2})

goal (1 subgoal):
 1. g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n)) = g 0 + 1 / real_of_int (a M) * R (Suc M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int (a M) * g (Suc ?n) = real_of_int (B * b (?n + M + 2)) / real_of_int (prod a {Suc M..?n + M + 2})
[PROOF STEP]
have "(\<Sum>n. a M * g (Suc n)) = R (Suc M)"
[PROOF STATE]
proof (prove)
using this:
real_of_int (a M) * g (Suc ?n) = real_of_int (B * b (?n + M + 2)) / real_of_int (prod a {Suc M..?n + M + 2})

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (a M) * g (Suc n)) = R (Suc M)
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
real_of_int (a M) * g (Suc ?n) = real_of_int (B * b (?n + M + 2)) / real_of_int (prod a {Suc M..?n + M + 2})

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (a M) * g (Suc n)) = (\<Sum>n. real_of_int (B * b (n + Suc M + 1)) / real_of_int (prod a {Suc M..n + Suc M + 1}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n. real_of_int (a M) * g (Suc n)) = R (Suc M)

goal (1 subgoal):
 1. g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n)) = g 0 + 1 / real_of_int (a M) * R (Suc M)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n. real_of_int (a M) * g (Suc n)) = R (Suc M)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. real_of_int (a M) * g (Suc n)) = R (Suc M)

goal (1 subgoal):
 1. g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n)) = g 0 + 1 / real_of_int (a M) * R (Suc M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n)) = g 0 + 1 / real_of_int (a M) * R (Suc M)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g 0 + 1 / real_of_int (a M) * (\<Sum>n. real_of_int (a M) * g (Suc n)) = g 0 + 1 / real_of_int (a M) * R (Suc M)

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
R M = g 0 + 1 / real_of_int (a M) * R (Suc M)
[PROOF STEP]
have "R M = g 0 + 1 / a M * R (Suc M)"
[PROOF STATE]
proof (prove)
using this:
R M = g 0 + 1 / real_of_int (a M) * R (Suc M)

goal (1 subgoal):
 1. R M = g 0 + 1 / real_of_int (a M) * R (Suc M)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
R M = g 0 + 1 / real_of_int (a M) * R (Suc M)

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R M = g 0 + 1 / real_of_int (a M) * R (Suc M)
[PROOF STEP]
have "R (Suc M) = a M * R M - g 0 * a M"
[PROOF STATE]
proof (prove)
using this:
R M = g 0 + 1 / real_of_int (a M) * R (Suc M)

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - g 0 * real_of_int (a M)
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
R (Suc M) = real_of_int (a M) * R M - g 0 * real_of_int (a M)

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R (Suc M) = real_of_int (a M) * R M - g 0 * real_of_int (a M)

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
have "{M..Suc M} = {M,Suc M}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {M..Suc M} = {M, Suc M}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{M..Suc M} = {M, Suc M}

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R (Suc M) = real_of_int (a M) * R M - g 0 * real_of_int (a M)
{M..Suc M} = {M, Suc M}
[PROOF STEP]
show "R (Suc M) = a M * R M - B * b (Suc M) / a (Suc M)"
[PROOF STATE]
proof (prove)
using this:
R (Suc M) = real_of_int (a M) * R M - g 0 * real_of_int (a M)
{M..Suc M} = {M, Suc M}

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
unfolding g_def
[PROOF STATE]
proof (prove)
using this:
R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (0 + M + 1)) / real_of_int (prod a {M..0 + M + 1}) * real_of_int (a M)
{M..Suc M} = {M, Suc M}

goal (1 subgoal):
 1. R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R (Suc M) = real_of_int (a M) * R M - real_of_int (B * b (Suc M)) / real_of_int (a (Suc M))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N \<le> ?M \<Longrightarrow> \<bar>R ?M\<bar> \<le> 1 / 4
N \<le> ?M \<Longrightarrow> R (Suc ?M) = real_of_int (a ?M) * R ?M - real_of_int (B * b (Suc ?M)) / real_of_int (a (Suc ?M))

goal (1 subgoal):
 1. \<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
[PROOF STEP]
define c where "c = (\<lambda>n. if n\<ge>N then get_c a b B N (n-N) else undefined)"
[PROOF STATE]
proof (state)
this:
c = (\<lambda>n. if N \<le> n then get_c a b B N (n - N) else undefined)

goal (1 subgoal):
 1. \<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
[PROOF STEP]
have c_rec:"c (n+1) = c n * a n -  B * b n" when "n \<ge> N" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c (n + 1) = c n * a n - B * b n
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if N \<le> n + 1 then get_c a b B N (n + 1 - N) else undefined) = (if N \<le> n then get_c a b B N (n - N) else undefined) * a n - B * b n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
N \<le> n

goal (1 subgoal):
 1. (if N \<le> n + 1 then get_c a b B N (n + 1 - N) else undefined) = (if N \<le> n then get_c a b B N (n - N) else undefined) * a n - B * b n
[PROOF STEP]
by (auto simp:Suc_diff_le)
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> c (?n + 1) = c ?n * a ?n - B * b ?n

goal (1 subgoal):
 1. \<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
[PROOF STEP]
have c_R:"c (Suc n) / a n = R n" when "n \<ge> N" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (Suc n)) / real_of_int (a n) = R n
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
N \<le> n

goal (1 subgoal):
 1. real_of_int (c (Suc n)) / real_of_int (a n) = R n
[PROOF STEP]
proof (induct rule:nat_induct_at_least)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
have "\<bar> c (N+1) / a N \<bar> \<le> 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
[PROOF STEP]
have "c N = round (B * b N / a N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c N = round (real_of_int (B * b N) / real_of_int (a N))
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if N \<le> N then get_c a b B N (N - N) else undefined) = round (real_of_int (B * b N) / real_of_int (a N))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c N = round (real_of_int (B * b N) / real_of_int (a N))

goal (1 subgoal):
 1. \<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c N = round (real_of_int (B * b N) / real_of_int (a N))

goal (1 subgoal):
 1. \<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
[PROOF STEP]
have "c (N+1) / a N = c N - B * b N / a N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)
[PROOF STEP]
using a_pos[rule_format,of N]
[PROOF STATE]
proof (prove)
using this:
0 < a N

goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)
[PROOF STEP]
by (auto simp add:c_rec[of N,simplified] divide_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)

goal (1 subgoal):
 1. \<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c N = round (real_of_int (B * b N) / real_of_int (a N))
real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c N = round (real_of_int (B * b N) / real_of_int (a N))
real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)

goal (1 subgoal):
 1. \<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
[PROOF STEP]
using of_int_round_abs_le
[PROOF STATE]
proof (prove)
using this:
c N = round (real_of_int (B * b N) / real_of_int (a N))
real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)
\<bar>of_int (round ?x) - ?x\<bar> \<le> (1::?'a) / (2::?'a)

goal (1 subgoal):
 1. \<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2

goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2

goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
have "\<bar>R N\<bar> \<le> 1 / 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>R N\<bar> \<le> 1 / 4
[PROOF STEP]
using R_bound[of N]
[PROOF STATE]
proof (prove)
using this:
N \<le> N \<Longrightarrow> \<bar>R N\<bar> \<le> 1 / 4

goal (1 subgoal):
 1. \<bar>R N\<bar> \<le> 1 / 4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>R N\<bar> \<le> 1 / 4

goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
\<bar>R N\<bar> \<le> 1 / 4
[PROOF STEP]
have "\<bar>c (N+1) / a N - R N \<bar> < 1"
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N)\<bar> \<le> 1 / 2
\<bar>R N\<bar> \<le> 1 / 4

goal (1 subgoal):
 1. \<bar>real_of_int (c (N + 1)) / real_of_int (a N) - R N\<bar> < 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N) - R N\<bar> < 1

goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N) - R N\<bar> < 1

goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
have "c (N+1) / a N - R N \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>
[PROOF STEP]
have "c (N+1) / a N = c N - B * b N / a N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)
[PROOF STEP]
using a_pos[rule_format,of N]
[PROOF STATE]
proof (prove)
using this:
0 < a N

goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)
[PROOF STEP]
by (auto simp add:c_rec[of N,simplified] divide_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)

goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)

goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>
[PROOF STEP]
have " B * b N / a N + R N \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>
[PROOF STEP]
have "C = B * (\<Sum>n<N. prod a {..<N} * (b n / prod a {..n}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C = real_of_int B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n})))
[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 B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n})))
[PROOF STEP]
by (simp add:sum_distrib_left algebra_simps)
[PROOF STATE]
proof (state)
this:
C = real_of_int B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n})))

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

goal (1 subgoal):
 1. real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>
[PROOF STEP]
have "... = B * (\<Sum>n<N. prod a {n<..<N} * b n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n}))) = real_of_int (B * (\<Sum>n<N. prod a {n<..<N} * b n))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n}))) = real_of_int (B * (\<Sum>n<N. prod a {n<..<N} * b n))
[PROOF STEP]
have "{..<N} = {n<..<N} \<union> {..n}" if "n<N" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {..<N} = {n<..<N} \<union> {..n}
[PROOF STEP]
by (simp add: ivl_disj_un_one(1) sup_commute that)
[PROOF STATE]
proof (state)
this:
?n < N \<Longrightarrow> {..<N} = {?n<..<N} \<union> {..?n}

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

goal (1 subgoal):
 1. real_of_int B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n}))) = real_of_int (B * (\<Sum>n<N. prod a {n<..<N} * b n))
[PROOF STEP]
using \<open>B>0\<close>
[PROOF STATE]
proof (prove)
using this:
?n < N \<Longrightarrow> {..<N} = {?n<..<N} \<union> {..?n}
0 < B

goal (1 subgoal):
 1. real_of_int B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n}))) = real_of_int (B * (\<Sum>n<N. prod a {n<..<N} * b n))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. n < N \<Longrightarrow> {..<N} = {n<..<N} \<union> {..n}; 0 < B\<rbrakk> \<Longrightarrow> (\<Sum>n<N. (\<Prod>x\<in>{n<..<N} \<union> {..n}. real_of_int (a x)) * real_of_int (b n) / (\<Prod>x\<le>n. real_of_int (a x))) = (\<Sum>x<N. (\<Prod>x\<in>{x<..<N}. real_of_int (a x)) * real_of_int (b x))
[PROOF STEP]
apply (subst prod.union_disjoint)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>na. \<lbrakk>\<And>n. n < N \<Longrightarrow> {..<N} = {n<..<N} \<union> {..n}; 0 < B\<rbrakk> \<Longrightarrow> finite {na<..<N}
 2. \<And>na. \<lbrakk>\<And>n. n < N \<Longrightarrow> {..<N} = {n<..<N} \<union> {..n}; 0 < B\<rbrakk> \<Longrightarrow> finite {..na}
 3. \<And>na. \<lbrakk>\<And>n. n < N \<Longrightarrow> {..<N} = {n<..<N} \<union> {..n}; 0 < B\<rbrakk> \<Longrightarrow> {na<..<N} \<inter> {..na} = {}
 4. \<lbrakk>\<And>n. n < N \<Longrightarrow> {..<N} = {n<..<N} \<union> {..n}; 0 < B\<rbrakk> \<Longrightarrow> (\<Sum>n<N. (\<Prod>x\<in>{n<..<N}. real_of_int (a x)) * (\<Prod>x\<le>n. real_of_int (a x)) * real_of_int (b n) / (\<Prod>x\<le>n. real_of_int (a x))) = (\<Sum>x<N. (\<Prod>x\<in>{x<..<N}. real_of_int (a x)) * real_of_int (b x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n}))) = real_of_int (B * (\<Sum>n<N. prod a {n<..<N} * b n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int B * (\<Sum>n<N. real_of_int (prod a {..<N}) * (real_of_int (b n) / real_of_int (prod a {..n}))) = real_of_int (B * (\<Sum>n<N. prod a {n<..<N} * b n))

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

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

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

goal (1 subgoal):
 1. C \<in> \<int>
[PROOF STEP]
using Ints_of_int
[PROOF STATE]
proof (prove)
using this:
C = real_of_int (B * (\<Sum>n<N. prod a {n<..<N} * b n))
of_int ?z \<in> \<int>

goal (1 subgoal):
 1. C \<in> \<int>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C \<in> \<int>

goal (1 subgoal):
 1. real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C \<in> \<int>

goal (1 subgoal):
 1. real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>
[PROOF STEP]
note \<open>A * prod a {..<N} = C + B * b N / a N  + R N\<close>
[PROOF STATE]
proof (state)
this:
real_of_int (A * prod a {..<N}) = C + real_of_int (B * b N) / real_of_int (a N) + R N

goal (1 subgoal):
 1. real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C \<in> \<int>
real_of_int (A * prod a {..<N}) = C + real_of_int (B * b N) / real_of_int (a N) + R N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<in> \<int>
real_of_int (A * prod a {..<N}) = C + real_of_int (B * b N) / real_of_int (a N) + R N

goal (1 subgoal):
 1. real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>
[PROOF STEP]
by (metis Ints_diff Ints_of_int add.assoc add_diff_cancel_left')
[PROOF STATE]
proof (state)
this:
real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>

goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)
real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int (c (N + 1)) / real_of_int (a N) = real_of_int (c N) - real_of_int (B * b N) / real_of_int (a N)
real_of_int (B * b N) / real_of_int (a N) + R N \<in> \<int>

goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>
[PROOF STEP]
by (simp add: diff_diff_add)
[PROOF STATE]
proof (state)
this:
real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>

goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N) - R N\<bar> < 1
real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>
[PROOF STEP]
have "c (N+1) / a N - R N = 0"
[PROOF STATE]
proof (prove)
using this:
\<bar>real_of_int (c (N + 1)) / real_of_int (a N) - R N\<bar> < 1
real_of_int (c (N + 1)) / real_of_int (a N) - R N \<in> \<int>

goal (1 subgoal):
 1. real_of_int (c (N + 1)) / real_of_int (a N) - R N = 0
[PROOF STEP]
by (metis Ints_cases less_irrefl of_int_0 of_int_lessD)
[PROOF STATE]
proof (state)
this:
real_of_int (c (N + 1)) / real_of_int (a N) - R N = 0

goal (2 subgoals):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
 2. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int (c (N + 1)) / real_of_int (a N) - R N = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
real_of_int (c (N + 1)) / real_of_int (a N) - R N = 0

goal (1 subgoal):
 1. real_of_int (c (Suc N)) / real_of_int (a N) = R N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of_int (c (Suc N)) / real_of_int (a N) = R N

goal (1 subgoal):
 1. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
N \<le> n
real_of_int (c (Suc n)) / real_of_int (a n) = R n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
have "c (Suc (Suc n)) / a (Suc n) = c (Suc n) - B * b (Suc n) / a (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))
[PROOF STEP]
apply (subst c_rec[of "Suc n",simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. N \<le> Suc n
 2. real_of_int (c (Suc n) * a (Suc n) - B * b (Suc n)) / real_of_int (a (Suc n)) = real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))
[PROOF STEP]
using \<open>N \<le> n\<close>
[PROOF STATE]
proof (prove)
using this:
N \<le> n

goal (2 subgoals):
 1. N \<le> Suc n
 2. real_of_int (c (Suc n) * a (Suc n) - B * b (Suc n)) / real_of_int (a (Suc n)) = real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))
[PROOF STEP]
by (auto simp add: divide_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
have "... = a n * R n - B * b (Suc n) / a (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n)) = real_of_int (a n) * R n - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
N \<le> n
real_of_int (c (Suc n)) / real_of_int (a n) = R n

goal (1 subgoal):
 1. real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n)) = real_of_int (a n) * R n - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))
[PROOF STEP]
by (auto simp: divide_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n)) = real_of_int (a n) * R n - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (c (Suc n)) - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n)) = real_of_int (a n) * R n - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))

goal (1 subgoal):
 1. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
have "... = R (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a n) * R n - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
using R_Suc[OF \<open>N \<le> n\<close>]
[PROOF STATE]
proof (prove)
using this:
R (Suc n) = real_of_int (a n) * R n - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n))

goal (1 subgoal):
 1. real_of_int (a n) * R n - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of_int (a n) * R n - real_of_int (B * b (Suc n)) / real_of_int (a (Suc n)) = R (Suc n)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>N \<le> n; real_of_int (c (Suc n)) / real_of_int (a n) = R n\<rbrakk> \<Longrightarrow> real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)

goal (1 subgoal):
 1. real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real_of_int (c (Suc (Suc n))) / real_of_int (a (Suc n)) = R (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> real_of_int (c (Suc ?n)) / real_of_int (a ?n) = R ?n

goal (1 subgoal):
 1. \<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
[PROOF STEP]
have ca_tendsto_zero:"(\<lambda>n. c (Suc n) / a n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0
[PROOF STEP]
using R_tendsto_0
[PROOF STATE]
proof (prove)
using this:
R \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (elim filterlim_mono_eventually)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. R x = real_of_int (c (Suc x)) / real_of_int (a x)
[PROOF STEP]
using c_R
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n \<Longrightarrow> real_of_int (c (Suc ?n)) / real_of_int (a ?n) = R ?n

goal (3 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. R x = real_of_int (c (Suc x)) / real_of_int (a x)
[PROOF STEP]
by (auto intro!:eventually_sequentiallyI[of N])
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<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
[PROOF STEP]
have ca_bound:"\<bar>c (n + 1)\<bar> < a n / 2" when "n \<ge> N" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
have "\<bar>c (Suc n)\<bar> / a n  = \<bar>c (Suc n) / a n\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) = \<bar>real_of_int (c (Suc n)) / real_of_int (a n)\<bar>
[PROOF STEP]
using a_pos[rule_format,of n]
[PROOF STATE]
proof (prove)
using this:
0 < a n

goal (1 subgoal):
 1. real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) = \<bar>real_of_int (c (Suc n)) / real_of_int (a n)\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) = \<bar>real_of_int (c (Suc n)) / real_of_int (a n)\<bar>

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

goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
have "... = \<bar>R n\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>real_of_int (c (Suc n)) / real_of_int (a n)\<bar> = \<bar>R n\<bar>
[PROOF STEP]
using c_R[OF that]
[PROOF STATE]
proof (prove)
using this:
real_of_int (c (Suc n)) / real_of_int (a n) = R n

goal (1 subgoal):
 1. \<bar>real_of_int (c (Suc n)) / real_of_int (a n)\<bar> = \<bar>R n\<bar>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (c (Suc n)) / real_of_int (a n)\<bar> = \<bar>R n\<bar>

goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>real_of_int (c (Suc n)) / real_of_int (a n)\<bar> = \<bar>R n\<bar>

goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
have "... < 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>R n\<bar> < 1 / 2
[PROOF STEP]
using R_bound[OF that]
[PROOF STATE]
proof (prove)
using this:
\<bar>R n\<bar> \<le> 1 / 4

goal (1 subgoal):
 1. \<bar>R n\<bar> < 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<bar>R n\<bar> < 1 / 2

goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) < 1 / 2
[PROOF STEP]
have "\<bar>c (Suc n)\<bar> / a n < 1/2"
[PROOF STATE]
proof (prove)
using this:
real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) < 1 / 2

goal (1 subgoal):
 1. real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) < 1 / 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) < 1 / 2

goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) < 1 / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) < 1 / 2

goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
using a_pos[rule_format,of n]
[PROOF STATE]
proof (prove)
using this:
real_of_int \<bar>c (Suc n)\<bar> / real_of_int (a n) < 1 / 2
0 < a n

goal (1 subgoal):
 1. real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> real_of_int \<bar>c (?n + 1)\<bar> < real_of_int (a ?n) / 2

goal (1 subgoal):
 1. \<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
[PROOF STEP]
(* (* the following part corresponds to (2.7) (2.8) in the original paper, but turns out to be
        not necessary. *)
  have c_round:"c n = round (B * b n / a n)" when "n \<ge> N" for n
  proof (cases "n=N")
    case True
    then show ?thesis unfolding c_def by simp
  next
    case False
    with \<open>n\<ge>N\<close> obtain n' where n_Suc:"n=Suc n'" and "n' \<ge> N"
      by (metis le_eq_less_or_eq lessE less_imp_le_nat)
    have "B * b n / a n = c n - R n"
    proof -
      have "R n = c n - B * b n / a n"
        using c_R[OF \<open>n'\<ge>N\<close>,symmetric,folded n_Suc] R_Suc[OF \<open>n'\<ge>N\<close>,folded n_Suc]
        by (auto simp:field_simps)
      then show ?thesis by (auto simp:field_simps)
    qed
    then have "\<bar>B * b n / a n - c n\<bar> = \<bar>R n\<bar>" by auto
    then have "\<bar>B * b n / a n - c n\<bar> < 1/2" using R_bound[OF \<open>n \<ge> N\<close>] by auto
    from round_unique'[OF this] show ?thesis by auto
  qed
  *)
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> real_of_int \<bar>c (?n + 1)\<bar> < real_of_int (a ?n) / 2

goal (1 subgoal):
 1. \<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
[PROOF STEP]
show "\<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> < a n / 2) \<and> (\<lambda>n. c (Suc n) / a n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<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
[PROOF STEP]
unfolding eventually_at_top_linorder
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B>0. \<exists>c. (\<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> (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule exI[of _ B],use \<open>B>0\<close> in simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < B \<Longrightarrow> \<exists>c. (\<exists>N. \<forall>n\<ge>N. B * b n = c n * a n - c (Suc n) \<and> \<bar>real_of_int (c (Suc n))\<bar> * 2 < real_of_int (a n)) \<and> (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (intro exI[of _c] exI[of _ N])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < B \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. B * b n = c n * a n - c (Suc n) \<and> \<bar>real_of_int (c (Suc n))\<bar> * 2 < real_of_int (a n)) \<and> (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0
[PROOF STEP]
using c_rec ca_bound ca_tendsto_zero
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n \<Longrightarrow> c (?n + 1) = c ?n * a ?n - B * b ?n
N \<le> ?n \<Longrightarrow> real_of_int \<bar>c (?n + 1)\<bar> < real_of_int (a ?n) / 2
(\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. 0 < B \<Longrightarrow> (\<exists>N. \<forall>n\<ge>N. B * b n = c n * a n - c (Suc n) \<and> \<bar>real_of_int (c (Suc n))\<bar> * 2 < real_of_int (a n)) \<and> (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
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) \<and> (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed