[STATEMENT]
lemma show10:
  fixes d ::"nat\<Rightarrow>real " and  a ::"nat\<Rightarrow>int " and s::nat
  assumes d [rule_format]: "\<forall>n. d n> 1"
    and a [rule_format]: "\<forall>n. a n>0"  and " s>0"
    and 9: "\<forall>m \<ge>s. \<exists>n\<ge>m. a (n+1) powr(1 / of_int (2^(n+1))) \<ge>
          d (n+1) * (Max ((\<lambda>j. (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} ))"
  shows "\<forall>m\<ge>s. \<exists>n\<ge>m. d (n+1) powr(2^(n+1)) * (\<Prod>j=1..n. of_int( a j)) *
            (1 / (\<Prod>j=1..s-1. of_int( a j))) \<le> a (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<ge>s. \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
proof (intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
assume "s \<le> m"
[PROOF STATE]
proof (state)
this:
s \<le> m

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
from 9[rule_format,OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>n\<ge>m. d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
obtain n where "n\<ge>m" and asm_9:"( (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
          (d (n+1))* (Max ( ( \<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
[PROOF STATE]
proof (prove)
using this:
\<exists>n\<ge>m. d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>m \<le> n; d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<le> n
d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
with \<open>s\<le>m\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<le> m
m \<le> n
d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
have "s\<le>n"
[PROOF STATE]
proof (prove)
using this:
s \<le> m
m \<le> n
d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))

goal (1 subgoal):
 1. s \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<le> n

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
define M where "M \<equiv> \<lambda>s. MAX j\<in>{s..n}. a j powr (1 / real_of_int (2 ^ j))"
[PROOF STATE]
proof (state)
this:
M \<equiv> \<lambda>s. MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
have prod: "(\<Prod>j=1..n. real_of_int (a j)) * (1 / (\<Prod>j=1..s-1. of_int(a j)))
            = (\<Prod>j=s..n. of_int( a j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
define f where "f= (\<lambda>j. real_of_int( a j))"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>j. real_of_int (a j))

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
have "{Suc 0..n}= {Suc 0..s - Suc 0} \<union> {s..n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n}
[PROOF STEP]
using \<open>n\<ge>s\<close>  \<open>s >0\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> n
0 < s

goal (1 subgoal):
 1. {Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n}

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n}
[PROOF STEP]
have "(\<Prod>j=1..n. f j) = (\<Prod>j=1..s-1. f j) * (\<Prod>j=s..n. f j)"
[PROOF STATE]
proof (prove)
using this:
{Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n}

goal (1 subgoal):
 1. prod f {1..n} = prod f {1..s - 1} * prod f {s..n}
[PROOF STEP]
apply (subst prod.union_disjoint[symmetric])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. {Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n} \<Longrightarrow> finite {1..s - 1}
 2. {Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n} \<Longrightarrow> finite {s..n}
 3. {Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n} \<Longrightarrow> {1..s - 1} \<inter> {s..n} = {}
 4. {Suc 0..n} = {Suc 0..s - Suc 0} \<union> {s..n} \<Longrightarrow> prod f {1..n} = prod f ({1..s - 1} \<union> {s..n})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
prod f {1..n} = prod f {1..s - 1} * prod f {s..n}

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
prod f {1..n} = prod f {1..s - 1} * prod f {s..n}

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
have "(\<Prod>j=1..s-1. f j) > 0 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < prod f {1..s - 1}
[PROOF STEP]
by (metis a f_def of_int_0_less_iff prod_pos)
[PROOF STATE]
proof (state)
this:
0 < prod f {1..s - 1}

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < prod f {1..s - 1}
[PROOF STEP]
have "(\<Prod>j=1..s-1. f j) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
0 < prod f {1..s - 1}

goal (1 subgoal):
 1. prod f {1..s - 1} \<noteq> 0
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
prod f {1..s - 1} \<noteq> 0

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
prod f {1..n} = prod f {1..s - 1} * prod f {s..n}
prod f {1..s - 1} \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod f {1..n} = prod f {1..s - 1} * prod f {s..n}
prod f {1..s - 1} \<noteq> 0

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j = 1..n. real_of_int (a j)) = (\<Prod>j = 1..s - 1. real_of_int (a j)) * (\<Prod>j = s..n. real_of_int (a j))
(\<Prod>j = 1..s - 1. real_of_int (a j)) \<noteq> 0

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
have "d (n+1) powr 2 ^ (n+1) * (\<Prod>j = 1..n. of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. of_int (a j))) =
             d (n+1) powr 2 ^ (n+1) * (\<Prod>j = s..n. of_int (a j))"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = (\<Prod>j = s..n. real_of_int (a j))

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = s..n. real_of_int (a j))
[PROOF STEP]
by (metis mult.assoc prod)
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = s..n. real_of_int (a j))

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) = d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = s..n. real_of_int (a j))

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
have
    "... \<le> ((d (n+1))powr(2^(n+1) ) * (\<Prod>i=s..n. M s powr(2^i)) )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = s..n. real_of_int (a j)) \<le> d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i)
[PROOF STEP]
proof (rule mult_left_mono)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Prod>j = s..n. real_of_int (a j)) \<le> (\<Prod>i = s..n. M s powr 2 ^ i)
 2. 0 \<le> d (n + 1) powr 2 ^ (n + 1)
[PROOF STEP]
show "0 \<le> (d (n + 1)) powr 2 ^ (n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> d (n + 1) powr 2 ^ (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> d (n + 1) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. (\<Prod>j = s..n. real_of_int (a j)) \<le> (\<Prod>i = s..n. M s powr 2 ^ i)
[PROOF STEP]
show "(\<Prod>j = s..n. real_of_int (a j)) \<le> (\<Prod>i = s..n. M s powr 2 ^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j = s..n. real_of_int (a j)) \<le> (\<Prod>i = s..n. M s powr 2 ^ i)
[PROOF STEP]
proof (intro prod_mono conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)
 2. \<And>i. i \<in> {s..n} \<Longrightarrow> real_of_int (a i) \<le> M s powr 2 ^ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)
 2. \<And>i. i \<in> {s..n} \<Longrightarrow> real_of_int (a i) \<le> M s powr 2 ^ i
[PROOF STEP]
assume i: "i \<in> {s..n}"
[PROOF STATE]
proof (state)
this:
i \<in> {s..n}

goal (2 subgoals):
 1. \<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)
 2. \<And>i. i \<in> {s..n} \<Longrightarrow> real_of_int (a i) \<le> M s powr 2 ^ i
[PROOF STEP]
have "a i = (a i powr (1 / real_of_int (2 ^ i))) powr 2 ^ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a i) = (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i
[PROOF STEP]
unfolding powr_powr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a i) = real_of_int (a i) powr (1 / real_of_int (2 ^ i) * 2 ^ i)
[PROOF STEP]
by (simp add: a less_eq_real_def)
[PROOF STATE]
proof (state)
this:
real_of_int (a i) = (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i

goal (2 subgoals):
 1. \<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)
 2. \<And>i. i \<in> {s..n} \<Longrightarrow> real_of_int (a i) \<le> M s powr 2 ^ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (a i) = (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i

goal (2 subgoals):
 1. \<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)
 2. \<And>i. i \<in> {s..n} \<Longrightarrow> real_of_int (a i) \<le> M s powr 2 ^ i
[PROOF STEP]
have  "\<dots> \<le> M s powr(2^i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i \<le> M s powr 2 ^ i
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i \<le> (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) powr 2 ^ i
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i \<in> {s..n}

goal (1 subgoal):
 1. (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i \<le> (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) powr 2 ^ i
[PROOF STEP]
by (force intro: powr_mono2)
[PROOF STATE]
proof (state)
this:
(real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i \<le> M s powr 2 ^ i

goal (2 subgoals):
 1. \<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)
 2. \<And>i. i \<in> {s..n} \<Longrightarrow> real_of_int (a i) \<le> M s powr 2 ^ i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int (a i) \<le> M s powr 2 ^ i
[PROOF STEP]
show "a i \<le> M s powr 2 ^ i"
[PROOF STATE]
proof (prove)
using this:
real_of_int (a i) \<le> M s powr 2 ^ i

goal (1 subgoal):
 1. real_of_int (a i) \<le> M s powr 2 ^ i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real_of_int (a i) \<le> M s powr 2 ^ i

goal (1 subgoal):
 1. \<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)
[PROOF STEP]
show "\<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a i)
[PROOF STEP]
by (meson a less_imp_le of_int_0_le_iff)
[PROOF STATE]
proof (state)
this:
?i \<in> {s..n} \<Longrightarrow> 0 \<le> real_of_int (a ?i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Prod>j = s..n. real_of_int (a j)) \<le> (\<Prod>i = s..n. M s powr 2 ^ i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = s..n. real_of_int (a j)) \<le> d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i)

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = s..n. real_of_int (a j)) \<le> d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i)

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
have "... = d(n+1) powr (2^(n+1)) * M s powr (\<Sum>i=s..n. 2^i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}
[PROOF STEP]
have  "d (n+1) powr (2^(n+1)) \<ge> 1  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> d (n + 1) powr 2 ^ (n + 1)
[PROOF STEP]
by (metis Transcendental.log_one d le_powr_iff zero_le_numeral zero_le_power zero_less_one)
[PROOF STATE]
proof (state)
this:
1 \<le> d (n + 1) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> d (n + 1) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}
[PROOF STEP]
have "(\<Prod>i=s..n. M s powr(2^i)) = M s powr (\<Sum>i=s..n. 2^i ) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>i = s..n. M s powr 2 ^ i) = M s powr sum ((^) 2) {s..n}
[PROOF STEP]
using \<open>s\<le>n\<close> powrfinitesum
[PROOF STATE]
proof (prove)
using this:
s \<le> n
?s \<le> ?n \<Longrightarrow> (\<Prod>j = ?s..?n. ?a powr 2 ^ j) = ?a powr sum ((^) 2) {?s..?n}

goal (1 subgoal):
 1. (\<Prod>i = s..n. M s powr 2 ^ i) = M s powr sum ((^) 2) {s..n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Prod>i = s..n. M s powr 2 ^ i) = M s powr sum ((^) 2) {s..n}

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 \<le> d (n + 1) powr 2 ^ (n + 1)
(\<Prod>i = s..n. M s powr 2 ^ i) = M s powr sum ((^) 2) {s..n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> d (n + 1) powr 2 ^ (n + 1)
(\<Prod>i = s..n. M s powr 2 ^ i) = M s powr sum ((^) 2) {s..n}

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>i = s..n. M s powr 2 ^ i) = d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n}

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
have "... \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr(2^(n+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)
[PROOF STEP]
have "sum (power 2) {s..n} < (2::real) ^ (n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum ((^) 2) {s..n} < 2 ^ (n + 1)
[PROOF STEP]
using factt \<open>s\<le>n\<close>
[PROOF STATE]
proof (prove)
using this:
?s \<le> ?n \<Longrightarrow> sum ((^) 2) {?s..?n} < 2 ^ (?n + 1)
s \<le> n

goal (1 subgoal):
 1. sum ((^) 2) {s..n} < 2 ^ (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..n} < 2 ^ (n + 1)

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum ((^) 2) {s..n} < 2 ^ (n + 1)

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)
[PROOF STEP]
have "1 \<le> M s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
define S where "S=(\<lambda>(j::nat). ( of_int( a j) powr(1 /real_of_int (2^j)) )) ` {s..n  }"
[PROOF STATE]
proof (state)
this:
S = (\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}

goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
have "finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite S

goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite S

goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
have "S\<noteq>{}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<noteq> {}
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n} \<noteq> {}
[PROOF STEP]
using \<open>s\<le>n\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> n

goal (1 subgoal):
 1. (\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S \<noteq> {}

goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
have "\<exists>x\<in>S. x\<ge>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>S. 1 \<le> x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>S. 1 \<le> x
[PROOF STEP]
have "a s powr (1 / (2^s)) \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> real_of_int (a s) powr (1 / 2 ^ s)
[PROOF STEP]
proof (rule ge_one_powr_ge_zero)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 \<le> real_of_int (a s)
 2. 0 \<le> 1 / 2 ^ s
[PROOF STEP]
show "1 \<le> real_of_int (a s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> real_of_int (a s)
[PROOF STEP]
by (simp add: a int_one_le_iff_zero_less)
[PROOF STATE]
proof (state)
this:
1 \<le> real_of_int (a s)

goal (1 subgoal):
 1. 0 \<le> 1 / 2 ^ s
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
1 \<le> real_of_int (a s) powr (1 / 2 ^ s)

goal (1 subgoal):
 1. \<exists>x\<in>S. 1 \<le> x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> real_of_int (a s) powr (1 / 2 ^ s)

goal (1 subgoal):
 1. \<exists>x\<in>S. 1 \<le> x
[PROOF STEP]
have "of_int( a s) powr(1 /real_of_int (2^s)) \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a s) powr (1 / real_of_int (2 ^ s)) \<in> S
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a s) powr (1 / real_of_int (2 ^ s)) \<in> (\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}
[PROOF STEP]
using \<open>s\<le>n\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> n

goal (1 subgoal):
 1. real_of_int (a s) powr (1 / real_of_int (2 ^ s)) \<in> (\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int (a s) powr (1 / real_of_int (2 ^ s)) \<in> S

goal (1 subgoal):
 1. \<exists>x\<in>S. 1 \<le> x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 \<le> real_of_int (a s) powr (1 / 2 ^ s)
real_of_int (a s) powr (1 / real_of_int (2 ^ s)) \<in> S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> real_of_int (a s) powr (1 / 2 ^ s)
real_of_int (a s) powr (1 / real_of_int (2 ^ s)) \<in> S

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>S. 1 \<le> x

goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite S
S \<noteq> {}
\<exists>x\<in>S. 1 \<le> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite S
S \<noteq> {}
\<exists>x\<in>S. 1 \<le> x

goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
using Max_ge_iff[of S 1]
[PROOF STATE]
proof (prove)
using this:
finite S
S \<noteq> {}
\<exists>x\<in>S. 1 \<le> x
\<lbrakk>finite S; S \<noteq> {}\<rbrakk> \<Longrightarrow> (1 \<le> Max S) = (\<exists>a\<in>S. 1 \<le> a)

goal (1 subgoal):
 1. 1 \<le> M s
[PROOF STEP]
unfolding S_def M_def
[PROOF STATE]
proof (prove)
using this:
finite ((\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n})
(\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n} \<noteq> {}
\<exists>x\<in>(\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}. 1 \<le> x
\<lbrakk>finite ((\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}); (\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n} \<noteq> {}\<rbrakk> \<Longrightarrow> (1 \<le> (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))) = (\<exists>a\<in>(\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}. 1 \<le> a)

goal (1 subgoal):
 1. 1 \<le> (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
1 \<le> M s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 \<le> M s

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> M s

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)
[PROOF STEP]
have "0 \<le> (d (n + 1)) powr 2 ^ (n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> d (n + 1) powr 2 ^ (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> d (n + 1) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum ((^) 2) {s..n} < 2 ^ (n + 1)
1 \<le> M s
0 \<le> d (n + 1) powr 2 ^ (n + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum ((^) 2) {s..n} < 2 ^ (n + 1)
1 \<le> M s
0 \<le> d (n + 1) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)
[PROOF STEP]
by (simp add: mult_left_mono powr_mono M_def)
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * M s powr sum ((^) 2) {s..n} \<le> d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
have "... =  (d (n+1) * M s) powr(2^(n+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)
[PROOF STEP]
have "d (n + 1) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> d (n + 1)
[PROOF STEP]
using d[of "n+1"]
[PROOF STATE]
proof (prove)
using this:
1 < d (n + 1)

goal (1 subgoal):
 1. 0 \<le> d (n + 1)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
0 \<le> d (n + 1)

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> d (n + 1)

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)
[PROOF STEP]
have "M s \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> M s
[PROOF STEP]
using \<open>s\<le>n\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> n

goal (1 subgoal):
 1. 0 \<le> M s
[PROOF STEP]
by (auto simp: M_def Max_ge_iff)
[PROOF STATE]
proof (state)
this:
0 \<le> M s

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> d (n + 1)
0 \<le> M s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> d (n + 1)
0 \<le> M s

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> d (n + 1)
0 \<le> (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) powr 2 ^ (n + 1) = (d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))) powr 2 ^ (n + 1)
[PROOF STEP]
using powr_mult
[PROOF STATE]
proof (prove)
using this:
0 \<le> d (n + 1)
0 \<le> (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
\<lbrakk>0 \<le> ?x; 0 \<le> ?y\<rbrakk> \<Longrightarrow> (?x * ?y) powr ?a = ?x powr ?a * ?y powr ?a

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) powr 2 ^ (n + 1) = (d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))) powr 2 ^ (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d (n + 1) powr 2 ^ (n + 1) * M s powr 2 ^ (n + 1) = (d (n + 1) * M s) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
have "... \<le> (real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d (n + 1) * M s) powr 2 ^ (n + 1) \<le> (real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1)
[PROOF STEP]
proof (rule powr_mono2)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. 0 \<le> 2 ^ (n + 1)
 2. 0 \<le> d (n + 1) * M s
 3. d (n + 1) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
have "M s \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> M s
[PROOF STEP]
using \<open>s\<le>n\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> n

goal (1 subgoal):
 1. 0 \<le> M s
[PROOF STEP]
by (auto simp: M_def Max_ge_iff)
[PROOF STATE]
proof (state)
this:
0 \<le> M s

goal (3 subgoals):
 1. 0 \<le> 2 ^ (n + 1)
 2. 0 \<le> d (n + 1) * M s
 3. d (n + 1) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> M s

goal (3 subgoals):
 1. 0 \<le> 2 ^ (n + 1)
 2. 0 \<le> d (n + 1) * M s
 3. d (n + 1) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
have "d (n + 1) \<ge>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> d (n + 1)
[PROOF STEP]
using d[of "n+1"]
[PROOF STATE]
proof (prove)
using this:
1 < d (n + 1)

goal (1 subgoal):
 1. 0 \<le> d (n + 1)
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
0 \<le> d (n + 1)

goal (3 subgoals):
 1. 0 \<le> 2 ^ (n + 1)
 2. 0 \<le> d (n + 1) * M s
 3. d (n + 1) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> M s
0 \<le> d (n + 1)
[PROOF STEP]
show "0 \<le> (d (n + 1)) * M s"
[PROOF STATE]
proof (prove)
using this:
0 \<le> M s
0 \<le> d (n + 1)

goal (1 subgoal):
 1. 0 \<le> d (n + 1) * M s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> d (n + 1) * M s

goal (2 subgoals):
 1. 0 \<le> 2 ^ (n + 1)
 2. d (n + 1) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
show "(d (n + 1)) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (n + 1) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
using M_def asm_9
[PROOF STATE]
proof (prove)
using this:
M \<equiv> \<lambda>s. MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))
d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))

goal (1 subgoal):
 1. d (n + 1) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
d (n + 1) * M s \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))

goal (1 subgoal):
 1. 0 \<le> 2 ^ (n + 1)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(d (n + 1) * M s) powr 2 ^ (n + 1) \<le> (real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(d (n + 1) * M s) powr 2 ^ (n + 1) \<le> (real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
have "... =  (of_int (a (n+1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1) = real_of_int (a (n + 1))
[PROOF STEP]
by (simp add: a less_eq_real_def pos_add_strict powr_powr)
[PROOF STATE]
proof (state)
this:
(real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1) = real_of_int (a (n + 1))

goal (1 subgoal):
 1. \<And>m. s \<le> m \<Longrightarrow> \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
show "\<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) *
                (1 / (\<Prod>j = 1..s - 1. real_of_int (a j)))
                \<le> real_of_int (a (n + 1))"
[PROOF STATE]
proof (prove)
using this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))

goal (1 subgoal):
 1. \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
using \<open>n\<ge>m\<close> \<open>m\<ge>s\<close>
[PROOF STATE]
proof (prove)
using this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
m \<le> n
s \<le> m

goal (1 subgoal):
 1. \<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. real_of_int (a j))) \<le> real_of_int (a (n + 1))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lasttoshow:
  fixes d ::"nat\<Rightarrow>real " and a b ::"nat\<Rightarrow>int " and q::int and s::nat
  assumes d: "\<forall>n. d n> 1"
     and a:"\<forall>n. a n>0" and "s>0" and "q>0"
    and "A > 1" and b:"\<forall>n. b n>0" and 9:
    "\<forall>m\<ge>s. \<exists>n\<ge>m. ((of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
          (d (n+1))* (Max ((\<lambda>(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
    and assu3: "filterlim( \<lambda> n. (d n)^(2^n)/ b n) at_top sequentially "
    and 5: "\<forall>\<^sub>F n in sequentially. (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
  shows "\<exists>n. q*((\<Prod>j=1..n. real_of_int(a j))) * suminf (\<lambda>(j::nat). (b (j+n+1)/ a (j+n+1)))<1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
define as where "as=(\<Prod>j = 1..s - 1. real_of_int (a j))"
[PROOF STATE]
proof (state)
this:
as = (\<Prod>j = 1..s - 1. real_of_int (a j))

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
obtain n where "n\<ge>s" and n_def1:"real_of_int q * as * 2
      * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1"
    and n_def2:"d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as)
          \<le> real_of_int (a (n + 1))"
    and n_def3:"(\<Sum>j. (b (n+1 + j)) /  (a (n+1 + j))) \<le> 2 * b (n+1) / a (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have *:"(\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
using tendsto_inverse_0_at_top[OF assu3]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. inverse (d x ^ 2 ^ x / real_of_int (b x))) \<longlonglongrightarrow> 0

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

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0 \<Longrightarrow> (\<lambda>n. real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
have "d n ^ 2 ^ n = d n powr (of_nat (2 ^ n))" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d n ^ 2 ^ n = d n powr real (2 ^ n)
[PROOF STEP]
by (metis d le_less_trans powr_realpow zero_le_one)
[PROOF STATE]
proof (state)
this:
d ?n ^ 2 ^ ?n = d ?n powr real (2 ^ ?n)

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0 \<Longrightarrow> (\<lambda>n. real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d ?n ^ 2 ^ ?n = d ?n powr real (2 ^ ?n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d ?n ^ 2 ^ ?n = d ?n powr real (2 ^ ?n)

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
d ?n ^ 2 ^ ?n = d ?n powr real (2 ^ ?n)
(\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from tendsto_mult_right_zero[OF this,of "q * as * 2"]
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. real_of_int q * as * 2 * (real_of_int (b x) / d x powr 2 ^ x)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. q * as * 2 * b n / d n powr 2 ^ n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. real_of_int q * as * 2 * (real_of_int (b x) / d x powr 2 ^ x)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1
[PROOF STEP]
by (elim order_tendstoD) simp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1
                  \<and> (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n)
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1
\<forall>\<^sub>F n in sequentially. (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n)

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n)
[PROOF STEP]
by eventually_elim auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n)

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n)
[PROOF STEP]
obtain N where N_def:"\<forall>n\<ge>N. q * as * 2 * b n / d n powr 2 ^ n < 1
            \<and> (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n)

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n)

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>N. real_of_int q * as * 2 * real_of_int (b n) / d n powr 2 ^ n < 1 \<and> (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> real_of_int (2 * b n) / real_of_int (a n)

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain n where "n\<ge>s" and "n\<ge>N" and n_def:"d (n + 1) powr 2 ^ (n + 1)
                * (\<Prod>j = 1..n. of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; N \<le> n; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using show10[OF d a \<open>s>0\<close> 9,folded as_def,rule_format,of "max s N"]
[PROOF STATE]
proof (prove)
using this:
s \<le> max s N \<Longrightarrow> \<exists>n\<ge>max s N. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; N \<le> n; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<le> n
N \<le> n
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))

goal (1 subgoal):
 1. (\<And>n. \<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with N_def[rule_format, of "n+1"] that[of n]
[PROOF STATE]
proof (chain)
picking this:
N \<le> n + 1 \<Longrightarrow> real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1 \<and> (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))
\<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis
s \<le> n
N \<le> n
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N \<le> n + 1 \<Longrightarrow> real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1 \<and> (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))
\<lbrakk>s \<le> n; real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1; d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1)); (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))\<rbrakk> \<Longrightarrow> thesis
s \<le> n
N \<le> n
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))

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:
s \<le> n
real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))
(\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1))

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
define pa where "pa \<equiv> (\<Prod>j = 1..n. real_of_int (a j))"
[PROOF STATE]
proof (state)
this:
pa \<equiv> \<Prod>j = 1..n. real_of_int (a j)

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
define dn where "dn \<equiv> d (n + 1) powr 2 ^ (n + 1)"
[PROOF STATE]
proof (state)
this:
dn \<equiv> d (n + 1) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
have [simp]:"dn >0" "as > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < dn &&& 0 < as
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < dn
[PROOF STEP]
unfolding dn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < d (n + 1) powr 2 ^ (n + 1)
[PROOF STEP]
by (metis d not_le numeral_One powr_gt_zero zero_le_numeral)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < as
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < as
[PROOF STEP]
unfolding as_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Prod>j = 1..s - 1. real_of_int (a j))
[PROOF STEP]
by (simp add: a prod_pos)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 < dn
0 < as

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
have [simp]:"pa>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < pa
[PROOF STEP]
unfolding pa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Prod>j = 1..n. real_of_int (a j))
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. 0 < (\<Prod>j = 1..n. real_of_int (a j))
[PROOF STEP]
by (simp add: prod_pos)
[PROOF STATE]
proof (state)
this:
0 < pa

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
have K: "q* (\<Prod>j=1..n. real_of_int (a j)) * suminf (\<lambda> (j::nat). (b (j+n+1)/ a (j+n+1)))
              \<le>q* (\<Prod>j=1..n. real_of_int (a j)) *2* (b (n+1))/(a( n+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<le> real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1))
[PROOF STEP]
apply (fold pa_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int q * pa * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<le> real_of_int q * pa * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1))
[PROOF STEP]
using mult_left_mono[OF n_def3,of "real_of_int q * pa"]
      \<open>n\<ge>s\<close> \<open>pa>0\<close> \<open>q>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> real_of_int q * pa \<Longrightarrow> real_of_int q * pa * (\<Sum>j. real_of_int (b (n + 1 + j)) / real_of_int (a (n + 1 + j))) \<le> real_of_int q * pa * (real_of_int (2 * b (n + 1)) / real_of_int (a (n + 1)))
s \<le> n
0 < pa
0 < q

goal (1 subgoal):
 1. real_of_int q * pa * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<le> real_of_int q * pa * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1))
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<le> real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1))

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<le> real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1))

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
have KK:"... \<le> 2*q* (\<Prod>j=1..n. real_of_int (a j)) * (b(n+1))*
      ((\<Prod>j=1..s-1. real_of_int( a j))/((d (n+1))powr(2^(n+1)) * (\<Prod>j=1..n. real_of_int ( a j))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j))))
[PROOF STEP]
have " dn * pa * (1 / as) \<le> real_of_int (a (n + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dn * pa * (1 / as) \<le> real_of_int (a (n + 1))
[PROOF STEP]
using n_def2
[PROOF STATE]
proof (prove)
using this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))

goal (1 subgoal):
 1. dn * pa * (1 / as) \<le> real_of_int (a (n + 1))
[PROOF STEP]
unfolding dn_def pa_def
[PROOF STATE]
proof (prove)
using this:
d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))

goal (1 subgoal):
 1. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dn * pa * (1 / as) \<le> real_of_int (a (n + 1))

goal (1 subgoal):
 1. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dn * pa * (1 / as) \<le> real_of_int (a (n + 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dn * pa * (1 / as) \<le> real_of_int (a (n + 1))

goal (1 subgoal):
 1. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j))))
[PROOF STEP]
apply (fold pa_def dn_def as_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dn * pa * (1 / as) \<le> real_of_int (a (n + 1)) \<Longrightarrow> real_of_int q * pa * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * pa * real_of_int (b (n + 1)) * (as / (dn * pa))
[PROOF STEP]
using \<open>pa>0\<close> \<open>q>0\<close> a[rule_format, of "Suc n"] b[rule_format, of "Suc n"]
[PROOF STATE]
proof (prove)
using this:
0 < pa
0 < q
0 < a (Suc n)
0 < b (Suc n)

goal (1 subgoal):
 1. dn * pa * (1 / as) \<le> real_of_int (a (n + 1)) \<Longrightarrow> real_of_int q * pa * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * pa * real_of_int (b (n + 1)) * (as / (dn * pa))
[PROOF STEP]
by (auto simp add: field_simps)
[PROOF STATE]
proof (state)
this:
real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j))))

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / real_of_int (a (n + 1)) \<le> real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j))))

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
have KKK: "... = q * (\<Prod>j=1..(s-1). real_of_int(a j)) * 2 * b (n+1) / d (n+1) powr 2^(n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)))) = real_of_int q * (\<Prod>j = 1..s - 1. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1)
[PROOF STEP]
apply (fold as_def pa_def dn_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (2 * q) * pa * real_of_int (b (n + 1)) * (as / (dn * pa)) = real_of_int q * as * 2 * real_of_int (b (n + 1)) / dn
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pa = 0 \<longrightarrow> q = 0 \<or> as = 0 \<or> b (Suc n) = 0 \<or> dn = 0
[PROOF STEP]
using \<open>0 < pa\<close>
[PROOF STATE]
proof (prove)
using this:
0 < pa

goal (1 subgoal):
 1. pa = 0 \<longrightarrow> q = 0 \<or> as = 0 \<or> b (Suc n) = 0 \<or> dn = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)))) = real_of_int q * (\<Prod>j = 1..s - 1. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (2 * q) * (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int (b (n + 1)) * ((\<Prod>j = 1..s - 1. real_of_int (a j)) / (d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)))) = real_of_int q * (\<Prod>j = 1..s - 1. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1)

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
have KKKK: "... < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int q * (\<Prod>j = 1..s - 1. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1
[PROOF STEP]
using n_def1
[PROOF STATE]
proof (prove)
using this:
real_of_int q * as * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1

goal (1 subgoal):
 1. real_of_int q * (\<Prod>j = 1..s - 1. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1
[PROOF STEP]
unfolding as_def
[PROOF STATE]
proof (prove)
using this:
real_of_int q * (\<Prod>j = 1..s - 1. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1

goal (1 subgoal):
 1. real_of_int q * (\<Prod>j = 1..s - 1. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real_of_int q * (\<Prod>j = 1..s - 1. real_of_int (a j)) * 2 * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1

goal (1 subgoal):
 1. \<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. real_of_int q * (\<Prod>j = 1..n. real_of_int (a j)) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) < 1

goal:
No subgoals!
[PROOF STEP]
qed