[STATEMENT]
lemma show7:
  fixes d::"nat\<Rightarrow>real" and a b::"nat\<Rightarrow>int " and q p::int
  assumes "q \<ge>1" and "p \<ge> 1" and a: "\<forall>n. a n \<ge> 1" and "\<forall>n. b n \<ge> 1"
    and assumerational:"(\<lambda> n. b (n+1) / a (n+1) ) sums (p/q)"
  shows "q*((\<Prod>j=1..n. of_int( a j)))*( suminf (\<lambda> (j::nat). (b (j+n+1)/ a (j+n+1 )))) \<ge> 1 "
    (is "?L \<ge> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
define LL where "LL=?L"
[PROOF STATE]
proof (state)
this:
LL = real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))

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

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

goal (1 subgoal):
 1. 1 \<le> real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
have "?L > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
have "aa > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < aa
[PROOF STEP]
unfolding aa_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. 1 \<le> a n

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

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

goal (1 subgoal):
 1. 0 < real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
have "(\<Sum>j. ff (j + n)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Sum>j. ff (j + n))
[PROOF STEP]
proof (rule suminf_pos)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. summable (\<lambda>j. ff (j + n))
 2. \<And>na. 0 < ff (na + n)
[PROOF STEP]
have "summable ff"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable ff
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>i. real_of_int (b (i + 1)) / real_of_int (a (i + 1)))
[PROOF STEP]
using assumerational
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)

goal (1 subgoal):
 1. summable (\<lambda>i. real_of_int (b (i + 1)) / real_of_int (a (i + 1)))
[PROOF STEP]
using summable_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)
summable ?f = (\<exists>s. ?f sums s)

goal (1 subgoal):
 1. summable (\<lambda>i. real_of_int (b (i + 1)) / real_of_int (a (i + 1)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
summable ff

goal (2 subgoals):
 1. summable (\<lambda>j. ff (j + n))
 2. \<And>na. 0 < ff (na + n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
summable ff
[PROOF STEP]
show " summable (\<lambda>j. ff (j + n))"
[PROOF STATE]
proof (prove)
using this:
summable ff

goal (1 subgoal):
 1. summable (\<lambda>j. ff (j + n))
[PROOF STEP]
using summable_iff_shift[of ff n]
[PROOF STATE]
proof (prove)
using this:
summable ff
summable (\<lambda>na. ff (na + n)) = summable ff

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

goal (1 subgoal):
 1. \<And>na. 0 < ff (na + n)
[PROOF STEP]
show "\<And>i. 0 < ff (i + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. 0 < ff (i + n)
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. 0 < real_of_int (b (i + n + 1)) / real_of_int (a (i + n + 1))
[PROOF STEP]
using a assms(4) int_one_le_iff_zero_less
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 1 \<le> a n
\<forall>n. 1 \<le> b n
(1 \<le> ?z) = (0 < ?z)

goal (1 subgoal):
 1. \<And>i. 0 < real_of_int (b (i + n + 1)) / real_of_int (a (i + n + 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < ff (?i + n)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < (\<Sum>j. ff (j + n))

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

goal (1 subgoal):
 1. 0 < real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
unfolding aa_def ff_def
[PROOF STATE]
proof (prove)
using this:
0 < (\<Prod>j = 1..n. real_of_int (a j))
0 < (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))

goal (1 subgoal):
 1. 0 < real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
using \<open>q\<ge>1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < (\<Prod>j = 1..n. real_of_int (a j))
0 < (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
1 \<le> q

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))

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

goal (1 subgoal):
 1. 1 \<le> real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
have "?L \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>
[PROOF STEP]
have "?L = aa *(p -q* ( \<Sum>j=1..n. b j / a j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = (\<Prod>j = 1..n. real_of_int (a j)) * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))
[PROOF STEP]
using a assms assumerational int_one_le_iff_zero_less showpre7
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 1 \<le> a n
1 \<le> q
1 \<le> p
\<forall>n. 1 \<le> a n
\<forall>n. 1 \<le> b n
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)
(1 \<le> ?z) = (0 < ?z)
\<lbrakk>0 < ?q; 0 < ?p; \<forall>n. 0 < ?a n; \<forall>n. 0 < ?b n; (\<lambda>n. real_of_int (?b (n + 1)) / real_of_int (?a (n + 1))) sums (real_of_int ?p / real_of_int ?q)\<rbrakk> \<Longrightarrow> real_of_int (?q * (\<Prod>j = 1..?n. of_int (?a j))) * (\<Sum>j. real_of_int (?b (j + ?n + 1)) / real_of_int (?a (j + ?n + 1))) = (\<Prod>j = 1..?n. real_of_int (?a j)) * (real_of_int ?p - real_of_int ?q * (\<Sum>j = 1..?n. real_of_int (?b j) / real_of_int (?a j)))

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

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) = aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j)))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>
[PROOF STEP]
have "... = aa * p - q * (\<Sum>j=1..n. aa * b j / a j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j))) = aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j))
[PROOF STEP]
by (auto simp add:algebra_simps sum_distrib_left)
[PROOF STATE]
proof (state)
this:
aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j))) = aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aa * (real_of_int p - real_of_int q * (\<Sum>j = 1..n. real_of_int (b j) / real_of_int (a j))) = aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>
[PROOF STEP]
have "... = prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))
[PROOF STEP]
have "(\<Sum>j=1..n. aa * b j / a j) = (\<Sum>j=1..n. b j * prod a ({1..n} - {j}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))
[PROOF STEP]
unfolding of_int_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = (\<Sum>x = 1..n. real_of_int (b x * prod a ({1..n} - {x})))
[PROOF STEP]
proof (rule sum.cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {1..n} = {1..n}
 2. \<And>x. x \<in> {1..n} \<Longrightarrow> aa * real_of_int (b x) / real_of_int (a x) = real_of_int (b x * prod a ({1..n} - {x}))
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {1..n} = {1..n}
 2. \<And>x. x \<in> {1..n} \<Longrightarrow> aa * real_of_int (b x) / real_of_int (a x) = real_of_int (b x * prod a ({1..n} - {x}))
[PROOF STEP]
assume "j \<in> {1..n}"
[PROOF STATE]
proof (state)
this:
j \<in> {1..n}

goal (2 subgoals):
 1. {1..n} = {1..n}
 2. \<And>x. x \<in> {1..n} \<Longrightarrow> aa * real_of_int (b x) / real_of_int (a x) = real_of_int (b x * prod a ({1..n} - {x}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j \<in> {1..n}
[PROOF STEP]
have "(\<Prod>i = 1..n. real_of_int (a i)) = a j * (\<Prod>i\<in>{1..n} - {j}. real_of_int (a i))"
[PROOF STATE]
proof (prove)
using this:
j \<in> {1..n}

goal (1 subgoal):
 1. (\<Prod>i = 1..n. real_of_int (a i)) = real_of_int (a j) * (\<Prod>i\<in>{1..n} - {j}. real_of_int (a i))
[PROOF STEP]
by (meson finite_atLeastAtMost prod.remove)
[PROOF STATE]
proof (state)
this:
(\<Prod>i = 1..n. real_of_int (a i)) = real_of_int (a j) * (\<Prod>i\<in>{1..n} - {j}. real_of_int (a i))

goal (2 subgoals):
 1. {1..n} = {1..n}
 2. \<And>x. x \<in> {1..n} \<Longrightarrow> aa * real_of_int (b x) / real_of_int (a x) = real_of_int (b x * prod a ({1..n} - {x}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>i = 1..n. real_of_int (a i)) = real_of_int (a j) * (\<Prod>i\<in>{1..n} - {j}. real_of_int (a i))
[PROOF STEP]
have "aa / real_of_int (a j) = prod a ({1..n} - {j})"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>i = 1..n. real_of_int (a i)) = real_of_int (a j) * (\<Prod>i\<in>{1..n} - {j}. real_of_int (a i))

goal (1 subgoal):
 1. aa / real_of_int (a j) = real_of_int (prod a ({1..n} - {j}))
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
using this:
(\<Prod>i = 1..n. real_of_int (a i)) = real_of_int (a j) * (\<Prod>i\<in>{1..n} - {j}. real_of_int (a i))

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) / real_of_int (a j) = real_of_int (prod a ({1..n} - {j}))
[PROOF STEP]
using a[rule_format,of j]
[PROOF STATE]
proof (prove)
using this:
(\<Prod>i = 1..n. real_of_int (a i)) = real_of_int (a j) * (\<Prod>i\<in>{1..n} - {j}. real_of_int (a i))
1 \<le> a j

goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) / real_of_int (a j) = real_of_int (prod a ({1..n} - {j}))
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
aa / real_of_int (a j) = real_of_int (prod a ({1..n} - {j}))

goal (2 subgoals):
 1. {1..n} = {1..n}
 2. \<And>x. x \<in> {1..n} \<Longrightarrow> aa * real_of_int (b x) / real_of_int (a x) = real_of_int (b x * prod a ({1..n} - {x}))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
aa / real_of_int (a j) = real_of_int (prod a ({1..n} - {j}))
[PROOF STEP]
show "aa * b j / a j = b j * prod a ({1..n} - {j})"
[PROOF STATE]
proof (prove)
using this:
aa / real_of_int (a j) = real_of_int (prod a ({1..n} - {j}))

goal (1 subgoal):
 1. aa * real_of_int (b j) / real_of_int (a j) = real_of_int (b j * prod a ({1..n} - {j}))
[PROOF STEP]
by (metis mult.commute of_int_mult times_divide_eq_right)
[PROOF STATE]
proof (state)
this:
aa * real_of_int (b j) / real_of_int (a j) = real_of_int (b j * prod a ({1..n} - {j}))

goal (1 subgoal):
 1. {1..n} = {1..n}
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))

goal (1 subgoal):
 1. aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))

goal (1 subgoal):
 1. aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))
[PROOF STEP]
have "aa * p = (\<Prod>j = 1..n.  (a j)) *  p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aa * real_of_int p = real_of_int (prod a {1..n} * p)
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j = 1..n. real_of_int (a j)) * real_of_int p = real_of_int (prod a {1..n} * p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
aa * real_of_int p = real_of_int (prod a {1..n} * p)

goal (1 subgoal):
 1. aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))
aa * real_of_int p = real_of_int (prod a {1..n} * p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))
aa * real_of_int p = real_of_int (prod a {1..n} * p)

goal (1 subgoal):
 1. aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
aa * real_of_int p - real_of_int q * (\<Sum>j = 1..n. aa * real_of_int (b j) / real_of_int (a j)) = real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j})))

goal (1 subgoal):
 1. real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>
[PROOF STEP]
have "... \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))) \<in> \<int>
[PROOF STEP]
using Ints_of_int
[PROOF STATE]
proof (prove)
using this:
of_int ?z \<in> \<int>

goal (1 subgoal):
 1. real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))) \<in> \<int>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
real_of_int (prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))) \<in> \<int>

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1))) \<in> \<int>

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

goal (1 subgoal):
 1. 1 \<le> real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))
[PROOF STEP]
apply (fold LL_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < LL; LL \<in> \<int>\<rbrakk> \<Longrightarrow> 1 \<le> LL
[PROOF STEP]
by (metis Ints_cases int_one_le_iff_zero_less not_less of_int_0_less_iff of_int_less_1_iff)
[PROOF STATE]
proof (state)
this:
1 \<le> real_of_int (q * (\<Prod>j = 1..n. of_int (a j))) * (\<Sum>j. real_of_int (b (j + n + 1)) / real_of_int (a (j + n + 1)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma show8:
  fixes d ::"nat\<Rightarrow>real " and a :: "nat\<Rightarrow>int" and s k::nat
  assumes "A > 1" and d: "\<forall>n. d n> 1"  and a:"\<forall>n. a n>0" and "s>0"
    and "convergent_prod d"
    and assu2: "\<forall>n \<ge> s. A / of_int (a n) powr (1 / of_int (2^n)) > (\<Prod>j. d (n + j))"
  shows "\<forall>n\<ge>s. (\<Prod>j. d (j+n)) < A / (MAX j\<in>{s..n}. of_int (a j) powr (1 / of_int (2 ^ j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<ge>s. (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
proof (intro strip)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. s \<le> n \<Longrightarrow> (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. s \<le> n \<Longrightarrow> (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
assume "s \<le> n"
[PROOF STATE]
proof (state)
this:
s \<le> n

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

goal (1 subgoal):
 1. \<And>n. s \<le> n \<Longrightarrow> (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
define ff where "ff \<equiv> (\<lambda>(j::nat). (real_of_int (a j)) powr(1 /of_int (2^j)))"
[PROOF STATE]
proof (state)
this:
ff \<equiv> \<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))

goal (1 subgoal):
 1. \<And>n. s \<le> n \<Longrightarrow> (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
have "sp i \<ge> sp n" when "i\<le>n" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sp n \<le> sp i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sp n \<le> sp i
[PROOF STEP]
have "(\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))
[PROOF STEP]
proof (rule prodinf_split_initial_segment)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. convergent_prod (\<lambda>j. d (j + i))
 2. \<And>ia. ia < n - i \<Longrightarrow> d (ia + i) \<noteq> 0
[PROOF STEP]
show "convergent_prod (\<lambda>j. d (j + i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent_prod (\<lambda>j. d (j + i))
[PROOF STEP]
using \<open>convergent_prod d\<close> convergent_prod_iff_shift[of d i]
[PROOF STATE]
proof (prove)
using this:
convergent_prod d
convergent_prod (\<lambda>ia. d (ia + i)) = convergent_prod d

goal (1 subgoal):
 1. convergent_prod (\<lambda>j. d (j + i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
convergent_prod (\<lambda>j. d (j + i))

goal (1 subgoal):
 1. \<And>ia. ia < n - i \<Longrightarrow> d (ia + i) \<noteq> 0
[PROOF STEP]
show "\<And>j. j < n - i \<Longrightarrow> d (j + i) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. j < n - i \<Longrightarrow> d (j + i) \<noteq> 0
[PROOF STEP]
by (metis d not_one_less_zero)
[PROOF STATE]
proof (state)
this:
?j < n - i \<Longrightarrow> d (?j + i) \<noteq> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))

goal (1 subgoal):
 1. sp n \<le> sp i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))
[PROOF STEP]
have "sp i = sp n * (\<Prod>j<n - i. d (i + j))"
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))

goal (1 subgoal):
 1. sp i = sp n * (\<Prod>j<n - i. d (i + j))
[PROOF STEP]
unfolding sp_def
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))

goal (1 subgoal):
 1. (\<Prod>j. d (j + i)) = (\<Prod>j. d (j + n)) * (\<Prod>j<n - i. d (i + j))
[PROOF STEP]
using \<open>n\<ge>i\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))
i \<le> n

goal (1 subgoal):
 1. (\<Prod>j. d (j + i)) = (\<Prod>j. d (j + n)) * (\<Prod>j<n - i. d (i + j))
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
sp i = sp n * (\<Prod>j<n - i. d (i + j))

goal (1 subgoal):
 1. sp n \<le> sp i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sp i = sp n * (\<Prod>j<n - i. d (i + j))

goal (1 subgoal):
 1. sp n \<le> sp i
[PROOF STEP]
have "sp i>1" "sp n>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < sp i &&& 1 < sp n
[PROOF STEP]
unfolding sp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < (\<Prod>j. d (j + i)) &&& 1 < (\<Prod>j. d (j + n))
[PROOF STEP]
using convergent_prod_iff_shift \<open>convergent_prod d\<close> d
[PROOF STATE]
proof (prove)
using this:
convergent_prod (\<lambda>i. ?f (i + ?n)) = convergent_prod ?f
convergent_prod d
\<forall>n. 1 < d n

goal (1 subgoal):
 1. 1 < (\<Prod>j. d (j + i)) &&& 1 < (\<Prod>j. d (j + n))
[PROOF STEP]
by (auto intro!:less_1_prodinf)
[PROOF STATE]
proof (state)
this:
1 < sp i
1 < sp n

goal (1 subgoal):
 1. sp n \<le> sp i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 < sp i
1 < sp n

goal (1 subgoal):
 1. sp n \<le> sp i
[PROOF STEP]
have "(\<Prod>j<n - i. d (i + j)) \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> (\<Prod>j<n - i. d (i + j))
[PROOF STEP]
using d less_imp_le
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 1 < d n
?x < ?y \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. 1 \<le> (\<Prod>j<n - i. d (i + j))
[PROOF STEP]
by (auto intro: prod_ge_1)
[PROOF STATE]
proof (state)
this:
1 \<le> (\<Prod>j<n - i. d (i + j))

goal (1 subgoal):
 1. sp n \<le> sp i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sp i = sp n * (\<Prod>j<n - i. d (i + j))
1 < sp i
1 < sp n
1 \<le> (\<Prod>j<n - i. d (i + j))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sp i = sp n * (\<Prod>j<n - i. d (i + j))
1 < sp i
1 < sp n
1 \<le> (\<Prod>j<n - i. d (i + j))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i \<le> n \<Longrightarrow> sp n \<le> sp ?i

goal (1 subgoal):
 1. \<And>n. s \<le> n \<Longrightarrow> (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i \<le> n \<Longrightarrow> sp n \<le> sp ?i

goal (1 subgoal):
 1. \<And>n. s \<le> n \<Longrightarrow> (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
have "\<forall>j\<ge>s. A / ff j > sp j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<ge>s. sp j < A / ff j
[PROOF STEP]
unfolding ff_def sp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<ge>s. (\<Prod>ja. d (ja + j)) < A / real_of_int (a j) powr (1 / real_of_int (2 ^ j))
[PROOF STEP]
using assu2
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>s. (\<Prod>j. d (n + j)) < A / real_of_int (a n) powr (1 / real_of_int (2 ^ n))

goal (1 subgoal):
 1. \<forall>j\<ge>s. (\<Prod>ja. d (ja + j)) < A / real_of_int (a j) powr (1 / real_of_int (2 ^ j))
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
\<forall>j\<ge>s. sp j < A / ff j

goal (1 subgoal):
 1. \<And>n. s \<le> n \<Longrightarrow> (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?i \<le> n \<Longrightarrow> sp n \<le> sp ?i
\<forall>j\<ge>s. sp j < A / ff j
[PROOF STEP]
have "\<forall>j. s\<le>j \<and> j\<le>n \<longrightarrow> A / ff j > sp n"
[PROOF STATE]
proof (prove)
using this:
?i \<le> n \<Longrightarrow> sp n \<le> sp ?i
\<forall>j\<ge>s. sp j < A / ff j

goal (1 subgoal):
 1. \<forall>j. s \<le> j \<and> j \<le> n \<longrightarrow> sp n < A / ff j
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>j. s \<le> j \<and> j \<le> n \<longrightarrow> sp n < A / ff j

goal (1 subgoal):
 1. \<And>n. s \<le> n \<Longrightarrow> (\<Prod>j. d (j + n)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>j. s \<le> j \<and> j \<le> n \<longrightarrow> sp n < A / ff j
[PROOF STEP]
show "sp n< A / Max (ff ` {s..n})"
[PROOF STATE]
proof (prove)
using this:
\<forall>j. s \<le> j \<and> j \<le> n \<longrightarrow> sp n < A / ff j

goal (1 subgoal):
 1. sp n < A / Max (ff ` {s..n})
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) Max_in \<open>n\<ge>s\<close> atLeastAtMost_iff empty_iff
        finite_atLeastAtMost finite_imageI imageE image_is_empty order_refl)
[PROOF STATE]
proof (state)
this:
sp n < A / Max (ff ` {s..n})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma auxiliary1_9:
  fixes d ::"nat\<Rightarrow>real" and a::"nat\<Rightarrow>int " and s m::nat
  assumes d: "\<forall>n. d n> 1"  and a: "\<forall>n. a n>0" and "s>0" and "n \<ge> m" and " m \<ge> s"
    and auxifalse_assu: "\<forall>n\<ge>m. (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) <
              (d (n+1))* (Max ((\<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} ))"
  shows "(of_int (a (n+1))) powr(1 /of_int (2^(n+1))) <
    (\<Prod>j=(m+1)..(n+1). d j) * (Max ((\<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..m}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {m + 1..n + 1} * (MAX j\<in>{s..m}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {m + 1..n + 1} * (MAX j\<in>{s..m}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
define ff where "ff \<equiv> \<lambda>j. real_of_int (a j) powr (1 / of_int (2^j))"
[PROOF STATE]
proof (state)
this:
ff \<equiv> \<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))

goal (1 subgoal):
 1. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {m + 1..n + 1} * (MAX j\<in>{s..m}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
have [simp]:"ff j > 0" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < ff j
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < real_of_int (a j) powr (1 / real_of_int (2 ^ j))
[PROOF STEP]
by (metis a less_numeral_extra(3) of_int_0_less_iff powr_gt_zero)
[PROOF STATE]
proof (state)
this:
0 < ff ?j

goal (1 subgoal):
 1. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {m + 1..n + 1} * (MAX j\<in>{s..m}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
have ff_asm:"ff (n+1) < d (n+1) * Max (ff ` {s..n})" when "n\<ge>m" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ff (n + 1) < d (n + 1) * Max (ff ` {s..n})
[PROOF STEP]
using auxifalse_assu that
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>m. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
m \<le> n

goal (1 subgoal):
 1. ff (n + 1) < d (n + 1) * Max (ff ` {s..n})
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>m. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
m \<le> n

goal (1 subgoal):
 1. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < d (n + 1) * (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m \<le> ?n \<Longrightarrow> ff (?n + 1) < d (?n + 1) * Max (ff ` {s..?n})

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

goal (1 subgoal):
 1. Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})
[PROOF STEP]
proof(induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m \<le> 0 \<Longrightarrow> Max (ff ` {s..0}) \<le> prod d {m + 1..0} * Max (ff ` {s..m})
 2. \<And>n. \<lbrakk>m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m}); m \<le> Suc n\<rbrakk> \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
m \<le> 0

goal (2 subgoals):
 1. m \<le> 0 \<Longrightarrow> Max (ff ` {s..0}) \<le> prod d {m + 1..0} * Max (ff ` {s..m})
 2. \<And>n. \<lbrakk>m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m}); m \<le> Suc n\<rbrakk> \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<le> 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m \<le> 0

goal (1 subgoal):
 1. Max (ff ` {s..0}) \<le> prod d {m + 1..0} * Max (ff ` {s..m})
[PROOF STEP]
using \<open>m\<ge>s\<close>
[PROOF STATE]
proof (prove)
using this:
m \<le> 0
s \<le> m

goal (1 subgoal):
 1. Max (ff ` {s..0}) \<le> prod d {m + 1..0} * Max (ff ` {s..m})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..0}) \<le> prod d {m + 1..0} * Max (ff ` {s..m})

goal (1 subgoal):
 1. \<And>n. \<lbrakk>m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m}); m \<le> Suc n\<rbrakk> \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m}); m \<le> Suc n\<rbrakk> \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})
m \<le> Suc n

goal (1 subgoal):
 1. \<And>n. \<lbrakk>m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m}); m \<le> Suc n\<rbrakk> \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have ?case when "m=Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
m = Suc n

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m = Suc n \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})

goal (1 subgoal):
 1. \<And>n. \<lbrakk>m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m}); m \<le> Suc n\<rbrakk> \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m = Suc n \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})

goal (1 subgoal):
 1. \<And>n. \<lbrakk>m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m}); m \<le> Suc n\<rbrakk> \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have ?case when "m\<noteq>Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have "m \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> n
[PROOF STEP]
using that Suc(2)
[PROOF STATE]
proof (prove)
using this:
m \<noteq> Suc n
m \<le> Suc n

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

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<le> n
[PROOF STEP]
have IH: "Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})"
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})
[PROOF STEP]
using Suc(1)
[PROOF STATE]
proof (prove)
using this:
m \<le> n
m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})

goal (1 subgoal):
 1. Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have "Max (ff ` {s..Suc n}) = Max (ff ` {s..n} \<union> {ff (Suc n)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) = Max (ff ` {s..n} \<union> {ff (Suc n)})
[PROOF STEP]
using Suc.prems assms(5) atLeastAtMostSuc_conv
[PROOF STATE]
proof (prove)
using this:
m \<le> Suc n
s \<le> m
?m \<le> Suc ?n \<Longrightarrow> {?m..Suc ?n} = insert (Suc ?n) {?m..?n}

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

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..Suc n}) = Max (ff ` {s..n} \<union> {ff (Suc n)})

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have "... = max (Max (ff ` {s..n})) (ff (Suc n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (ff ` {s..n} \<union> {ff (Suc n)}) = max (Max (ff ` {s..n})) (ff (Suc n))
[PROOF STEP]
using Suc.prems assms(5) max_def sup_assoc that
[PROOF STATE]
proof (prove)
using this:
m \<le> Suc n
s \<le> m
max ?a ?b = (if ?a \<le> ?b then ?b else ?a)
sup (sup ?x ?y) ?z = sup ?x (sup ?y ?z)
m \<noteq> Suc n

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

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..n} \<union> {ff (Suc n)}) = max (Max (ff ` {s..n})) (ff (Suc n))

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have "... \<le> max (Max (ff ` {s..n})) (d (n+1) * Max (ff ` {s..n}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (Max (ff ` {s..n})) (ff (Suc n)) \<le> max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n}))
[PROOF STEP]
using \<open>m \<le> n\<close> ff_asm
[PROOF STATE]
proof (prove)
using this:
m \<le> n
m \<le> ?n \<Longrightarrow> ff (?n + 1) < d (?n + 1) * Max (ff ` {s..?n})

goal (1 subgoal):
 1. max (Max (ff ` {s..n})) (ff (Suc n)) \<le> max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n}))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
max (Max (ff ` {s..n})) (ff (Suc n)) \<le> max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n}))

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (Max (ff ` {s..n})) (ff (Suc n)) \<le> max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n}))

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have "... \<le> Max (ff ` {s..n}) * max 1 (d (n+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n})) \<le> Max (ff ` {s..n}) * max 1 (d (n + 1))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n})) \<le> Max (ff ` {s..n}) * max 1 (d (n + 1))
[PROOF STEP]
have "Max (ff ` {s..n}) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Max (ff ` {s..n})
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) Max_in \<open>\<And>j. 0 < ff j\<close> \<open>m \<le> n\<close> assms(5)
              atLeastAtMost_iff empty_iff finite_atLeastAtMost finite_imageI imageE
              image_is_empty less_eq_real_def)
[PROOF STATE]
proof (state)
this:
0 \<le> Max (ff ` {s..n})

goal (1 subgoal):
 1. max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n})) \<le> Max (ff ` {s..n}) * max 1 (d (n + 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> Max (ff ` {s..n})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> Max (ff ` {s..n})

goal (1 subgoal):
 1. max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n})) \<le> Max (ff ` {s..n}) * max 1 (d (n + 1))
[PROOF STEP]
using max_mult_distrib_right
[PROOF STATE]
proof (prove)
using this:
0 \<le> Max (ff ` {s..n})
max ?x ?y * ?p = (if (0::?'a) \<le> ?p then max (?x * ?p) (?y * ?p) else min (?x * ?p) (?y * ?p))

goal (1 subgoal):
 1. max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n})) \<le> Max (ff ` {s..n}) * max 1 (d (n + 1))
[PROOF STEP]
by (simp add: max_mult_distrib_right mult.commute)
[PROOF STATE]
proof (state)
this:
max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n})) \<le> Max (ff ` {s..n}) * max 1 (d (n + 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n})) \<le> Max (ff ` {s..n}) * max 1 (d (n + 1))

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (Max (ff ` {s..n})) (d (n + 1) * Max (ff ` {s..n})) \<le> Max (ff ` {s..n}) * max 1 (d (n + 1))

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have "... = Max (ff ` {s..n}) * d (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (ff ` {s..n}) * max 1 (d (n + 1)) = Max (ff ` {s..n}) * d (n + 1)
[PROOF STEP]
by (metis d max.commute max.strict_order_iff)
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..n}) * max 1 (d (n + 1)) = Max (ff ` {s..n}) * d (n + 1)

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..n}) * max 1 (d (n + 1)) = Max (ff ` {s..n}) * d (n + 1)

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have "... \<le>  prod d {m + 1..n} * Max (ff ` {s..m}) * d (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (ff ` {s..n}) * d (n + 1) \<le> prod d {m + 1..n} * Max (ff ` {s..m}) * d (n + 1)
[PROOF STEP]
using IH d[rule_format, of "n+1"]
[PROOF STATE]
proof (prove)
using this:
Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})
1 < d (n + 1)

goal (1 subgoal):
 1. Max (ff ` {s..n}) * d (n + 1) \<le> prod d {m + 1..n} * Max (ff ` {s..m}) * d (n + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..n}) * d (n + 1) \<le> prod d {m + 1..n} * Max (ff ` {s..m}) * d (n + 1)

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..n}) * d (n + 1) \<le> prod d {m + 1..n} * Max (ff ` {s..m}) * d (n + 1)

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
have "... = prod d {m + 1..n+1} * Max (ff ` {s..m})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod d {m + 1..n} * Max (ff ` {s..m}) * d (n + 1) = prod d {m + 1..n + 1} * Max (ff ` {s..m})
[PROOF STEP]
using \<open>n\<ge>m\<close>
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. prod d {m + 1..n} * Max (ff ` {s..m}) * d (n + 1) = prod d {m + 1..n + 1} * Max (ff ` {s..m})
[PROOF STEP]
by (simp add:prod.nat_ivl_Suc' algebra_simps)
[PROOF STATE]
proof (state)
this:
prod d {m + 1..n} * Max (ff ` {s..m}) * d (n + 1) = prod d {m + 1..n + 1} * Max (ff ` {s..m})

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Max (ff ` {s..Suc n}) \<le> prod d {m + 1..n + 1} * Max (ff ` {s..m})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Max (ff ` {s..Suc n}) \<le> prod d {m + 1..n + 1} * Max (ff ` {s..m})

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m \<noteq> Suc n \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})

goal (1 subgoal):
 1. \<And>n. \<lbrakk>m \<le> n \<Longrightarrow> Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m}); m \<le> Suc n\<rbrakk> \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m = Suc n \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
m \<noteq> Suc n \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
m = Suc n \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
m \<noteq> Suc n \<Longrightarrow> Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})

goal (1 subgoal):
 1. Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..Suc n}) \<le> prod d {m + 1..Suc n} * Max (ff ` {s..m})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})

goal (1 subgoal):
 1. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {m + 1..n + 1} * (MAX j\<in>{s..m}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})
[PROOF STEP]
have "d (n+1) * Max (ff ` {s..n} ) \<le> (\<Prod>j=(m+1)..(n+1). d j)* (Max (ff ` {s..m}))"
[PROOF STATE]
proof (prove)
using this:
Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})

goal (1 subgoal):
 1. d (n + 1) * Max (ff ` {s..n}) \<le> prod d {m + 1..n + 1} * Max (ff ` {s..m})
[PROOF STEP]
using \<open>m\<le>n\<close> d[rule_format,of "Suc n"]
[PROOF STATE]
proof (prove)
using this:
Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})
m \<le> n
1 < d (Suc n)

goal (1 subgoal):
 1. d (n + 1) * Max (ff ` {s..n}) \<le> prod d {m + 1..n + 1} * Max (ff ` {s..m})
[PROOF STEP]
by (simp add:prod.nat_ivl_Suc')
[PROOF STATE]
proof (state)
this:
d (n + 1) * Max (ff ` {s..n}) \<le> prod d {m + 1..n + 1} * Max (ff ` {s..m})

goal (1 subgoal):
 1. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {m + 1..n + 1} * (MAX j\<in>{s..m}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
d (n + 1) * Max (ff ` {s..n}) \<le> prod d {m + 1..n + 1} * Max (ff ` {s..m})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
d (n + 1) * Max (ff ` {s..n}) \<le> prod d {m + 1..n + 1} * Max (ff ` {s..m})

goal (1 subgoal):
 1. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {m + 1..n + 1} * (MAX j\<in>{s..m}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
using ff_asm[of n] \<open>s\<le>m\<close> \<open>m\<le>n\<close>
[PROOF STATE]
proof (prove)
using this:
d (n + 1) * Max (ff ` {s..n}) \<le> prod d {m + 1..n + 1} * Max (ff ` {s..m})
m \<le> n \<Longrightarrow> ff (n + 1) < d (n + 1) * Max (ff ` {s..n})
s \<le> m
m \<le> n

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma show9:
  fixes d ::"nat\<Rightarrow>real " and a :: "nat\<Rightarrow>int " and s ::nat and A::real
  assumes   "A > 1" and  d: "\<forall>n. d n> 1"  and a: "\<forall>n. a n>0" and "s>0"
    and assu1: "(( \<lambda> n. (of_int (a n)) powr(1 /of_int (2^n)))\<longlongrightarrow> A) sequentially "
    and "convergent_prod d"
    and 8: "\<forall>n\<ge>s. prodinf (\<lambda>j. d( n+j))
                  < A/(Max ((\<lambda>(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n})) "
  shows "\<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} )))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m\<ge>s. \<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]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
define ff where "ff \<equiv> (\<lambda>j. real_of_int (a j) powr (1 / of_int (2^j)))"
[PROOF STATE]
proof (state)
this:
ff \<equiv> \<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
assume assumptioncontra: " \<not> (\<forall>m \<ge>s. \<exists>n\<ge>m. ff(n+1) \<ge> d(n+1) * Max (ff  ` {s..n}))"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>m\<ge>s. \<exists>n\<ge>m. d (n + 1) * Max (ff ` {s..n}) \<le> ff (n + 1))

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>m\<ge>s. \<exists>n\<ge>m. d (n + 1) * Max (ff ` {s..n}) \<le> ff (n + 1))
[PROOF STEP]
obtain t where "t\<ge>s" and
    ttt: "\<forall>n\<ge>t. ff (n+1) < d (n+1) * Max (ff ` {s..n})"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>m\<ge>s. \<exists>n\<ge>m. d (n + 1) * Max (ff ` {s..n}) \<le> ff (n + 1))

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>s \<le> t; \<forall>n\<ge>t. ff (n + 1) < d (n + 1) * Max (ff ` {s..n})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
s \<le> t
\<forall>n\<ge>t. ff (n + 1) < d (n + 1) * Max (ff ` {s..n})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
define B where "B \<equiv> \<Prod>j. d (t + 1 + j)"
[PROOF STATE]
proof (state)
this:
B \<equiv> \<Prod>j. d (t + 1 + j)

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
have "B>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < B
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Prod>j. d (t + 1 + j))
[PROOF STEP]
proof (rule less_0_prodinf)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. convergent_prod (\<lambda>j. d (t + 1 + j))
 2. \<And>i. 0 < d (t + 1 + i)
[PROOF STEP]
show "convergent_prod (\<lambda>j. d (t + 1 + j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent_prod (\<lambda>j. d (t + 1 + j))
[PROOF STEP]
using convergent_prod_iff_shift[of d "t+1"] \<open>convergent_prod d\<close>
[PROOF STATE]
proof (prove)
using this:
convergent_prod (\<lambda>i. d (i + (t + 1))) = convergent_prod d
convergent_prod d

goal (1 subgoal):
 1. convergent_prod (\<lambda>j. d (t + 1 + j))
[PROOF STEP]
by (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
convergent_prod (\<lambda>j. d (t + 1 + j))

goal (1 subgoal):
 1. \<And>i. 0 < d (t + 1 + i)
[PROOF STEP]
show "\<And>i. 0 < d (t + 1 + i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. 0 < d (t + 1 + i)
[PROOF STEP]
using d le_less_trans zero_le_one
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 1 < d n
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z
(0::?'a) \<le> (1::?'a)

goal (1 subgoal):
 1. \<And>i. 0 < d (t + 1 + i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 < d (t + 1 + ?i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < B

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
have "A \<le> B * Max ( ff ` {s..t})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<le> B * Max (ff ` {s..t})
[PROOF STEP]
proof (rule tendsto_le[of sequentially "\<lambda>n. (\<Prod>j=(t+1)..(n+1). d j) * Max ( ff ` {s..t})" _
        "\<lambda>n. ff (n+1)"])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. sequentially \<noteq> bot
 2. (\<lambda>n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \<longlonglongrightarrow> B * Max (ff ` {s..t})
 3. (\<lambda>n. ff (n + 1)) \<longlonglongrightarrow> A
 4. \<forall>\<^sub>F x in sequentially. ff (x + 1) \<le> prod d {t + 1..x + 1} * Max (ff ` {s..t})
[PROOF STEP]
show "(\<lambda>n. ff (n + 1)) \<longlonglongrightarrow> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ff (n + 1)) \<longlonglongrightarrow> A
[PROOF STEP]
using assu1[folded ff_def] LIMSEQ_ignore_initial_segment
[PROOF STATE]
proof (prove)
using this:
ff \<longlonglongrightarrow> A
?f \<longlonglongrightarrow> ?a \<Longrightarrow> (\<lambda>n. ?f (n + ?k)) \<longlonglongrightarrow> ?a

goal (1 subgoal):
 1. (\<lambda>n. ff (n + 1)) \<longlonglongrightarrow> A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ff (n + 1)) \<longlonglongrightarrow> A

goal (3 subgoals):
 1. sequentially \<noteq> bot
 2. (\<lambda>n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \<longlonglongrightarrow> B * Max (ff ` {s..t})
 3. \<forall>\<^sub>F x in sequentially. ff (x + 1) \<le> prod d {t + 1..x + 1} * Max (ff ` {s..t})
[PROOF STEP]
have "(\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B
[PROOF STEP]
have "convergent_prod (\<lambda>j. d (t + 1 + j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent_prod (\<lambda>j. d (t + 1 + j))
[PROOF STEP]
using \<open>convergent_prod d\<close> convergent_prod_iff_shift[of d "t+1"]
[PROOF STATE]
proof (prove)
using this:
convergent_prod d
convergent_prod (\<lambda>i. d (i + (t + 1))) = convergent_prod d

goal (1 subgoal):
 1. convergent_prod (\<lambda>j. d (t + 1 + j))
[PROOF STEP]
by (simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
convergent_prod (\<lambda>j. d (t + 1 + j))

goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
convergent_prod (\<lambda>j. d (t + 1 + j))
[PROOF STEP]
have "(\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B"
[PROOF STATE]
proof (prove)
using this:
convergent_prod (\<lambda>j. d (t + 1 + j))

goal (1 subgoal):
 1. (\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B
[PROOF STEP]
using B_def convergent_prod_LIMSEQ
[PROOF STATE]
proof (prove)
using this:
convergent_prod (\<lambda>j. d (t + 1 + j))
B \<equiv> \<Prod>j. d (t + 1 + j)
convergent_prod ?f \<Longrightarrow> (\<lambda>n. prod ?f {..n}) \<longlonglongrightarrow> prodinf ?f

goal (1 subgoal):
 1. (\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B

goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B
[PROOF STEP]
have "(\<lambda>n. \<Prod>i\<in>{0..n}. d (i+(t + 1))) \<longlonglongrightarrow> B"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B

goal (1 subgoal):
 1. (\<lambda>n. \<Prod>i = 0..n. d (i + (t + 1))) \<longlonglongrightarrow> B
[PROOF STEP]
using atLeast0AtMost
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B
{0..?n} = {..?n}

goal (1 subgoal):
 1. (\<lambda>n. \<Prod>i = 0..n. d (i + (t + 1))) \<longlonglongrightarrow> B
[PROOF STEP]
by (auto simp:algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Prod>i = 0..n. d (i + (t + 1))) \<longlonglongrightarrow> B

goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<Prod>i = 0..n. d (i + (t + 1))) \<longlonglongrightarrow> B
[PROOF STEP]
have "(\<lambda>n. prod d {(t + 1)..n + (t + 1)}) \<longlonglongrightarrow> B"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<Prod>i = 0..n. d (i + (t + 1))) \<longlonglongrightarrow> B

goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + (t + 1)}) \<longlonglongrightarrow> B
[PROOF STEP]
apply (subst (asm) prod.shift_bounds_cl_nat_ivl[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. prod d {0 + (t + 1)..n + (t + 1)}) \<longlonglongrightarrow> B \<Longrightarrow> (\<lambda>n. prod d {t + 1..n + (t + 1)}) \<longlonglongrightarrow> B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. prod d {t + 1..n + (t + 1)}) \<longlonglongrightarrow> B

goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B
[PROOF STEP]
from seq_offset_neg[OF this,of "t"]
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>i. prod d {t + 1..i - t + (t + 1)}) \<longlonglongrightarrow> B
[PROOF STEP]
show "(\<lambda>n. prod d {t + 1..n+1}) \<longlonglongrightarrow> B"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>i. prod d {t + 1..i - t + (t + 1)}) \<longlonglongrightarrow> B

goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B
[PROOF STEP]
apply (elim Lim_transform)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. prod d {t + 1..x + 1} - prod d {t + 1..x - t + (t + 1)}) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule LIMSEQ_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. norm (prod d {t + 1..n + 1} - prod d {t + 1..n - t + (t + 1)} - 0) < r
[PROOF STEP]
apply (rule exI[where x="t+1"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. 0 < r \<Longrightarrow> \<forall>n\<ge>t + 1. norm (prod d {t + 1..n + 1} - prod d {t + 1..n - t + (t + 1)} - 0) < r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B

goal (3 subgoals):
 1. sequentially \<noteq> bot
 2. (\<lambda>n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \<longlonglongrightarrow> B * Max (ff ` {s..t})
 3. \<forall>\<^sub>F x in sequentially. ff (x + 1) \<le> prod d {t + 1..x + 1} * Max (ff ` {s..t})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B
[PROOF STEP]
show "(\<lambda>n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \<longlonglongrightarrow> B * Max (ff ` {s..t})"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B

goal (1 subgoal):
 1. (\<lambda>n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \<longlonglongrightarrow> B * Max (ff ` {s..t})
[PROOF STEP]
by (auto intro:tendsto_eq_intros)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \<longlonglongrightarrow> B * Max (ff ` {s..t})

goal (2 subgoals):
 1. sequentially \<noteq> bot
 2. \<forall>\<^sub>F x in sequentially. ff (x + 1) \<le> prod d {t + 1..x + 1} * Max (ff ` {s..t})
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. (ff (n+1)) < (\<Prod>j=(t+1)..(n+1). d j) * (Max ( ff ` {s..t}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. ff (n + 1) < prod d {t + 1..n + 1} * Max (ff ` {s..t})
[PROOF STEP]
unfolding eventually_sequentially ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {t + 1..n + 1} * (MAX j\<in>{s..t}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
using auxiliary1_9[OF d a \<open>s>0\<close> _ \<open>t\<ge>s\<close> ttt[unfolded ff_def]]
[PROOF STATE]
proof (prove)
using this:
t \<le> ?n \<Longrightarrow> real_of_int (a (?n + 1)) powr (1 / real_of_int (2 ^ (?n + 1))) < prod d {t + 1..?n + 1} * (MAX j\<in>{s..t}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1))) < prod d {t + 1..n + 1} * (MAX j\<in>{s..t}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. ff (n + 1) < prod d {t + 1..n + 1} * Max (ff ` {s..t})

goal (2 subgoals):
 1. sequentially \<noteq> bot
 2. \<forall>\<^sub>F x in sequentially. ff (x + 1) \<le> prod d {t + 1..x + 1} * Max (ff ` {s..t})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. ff (n + 1) < prod d {t + 1..n + 1} * Max (ff ` {s..t})
[PROOF STEP]
show "\<forall>\<^sub>F n in sequentially. (ff (n+1)) \<le> (\<Prod>j=(t+1)..(n+1). d j) * (Max ( ff ` {s..t}))"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. ff (n + 1) < prod d {t + 1..n + 1} * Max (ff ` {s..t})

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. ff (n + 1) \<le> prod d {t + 1..n + 1} * Max (ff ` {s..t})
[PROOF STEP]
by (eventually_elim,simp)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. ff (n + 1) \<le> prod d {t + 1..n + 1} * Max (ff ` {s..t})

goal (1 subgoal):
 1. sequentially \<noteq> bot
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
A \<le> B * Max (ff ` {s..t})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A \<le> B * Max (ff ` {s..t})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
have "... \<le> B * Max ( ff ` {s..t+1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B * Max (ff ` {s..t}) \<le> B * Max (ff ` {s..t + 1})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B * Max (ff ` {s..t}) \<le> B * Max (ff ` {s..t + 1})
[PROOF STEP]
have "Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})
[PROOF STEP]
using \<open>t\<ge>s\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> t

goal (1 subgoal):
 1. Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})
[PROOF STEP]
by (auto intro: Max_mono)
[PROOF STATE]
proof (state)
this:
Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. B * Max (ff ` {s..t}) \<le> B * Max (ff ` {s..t + 1})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. B * Max (ff ` {s..t}) \<le> B * Max (ff ` {s..t + 1})
[PROOF STEP]
using \<open>B>0\<close>
[PROOF STATE]
proof (prove)
using this:
Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})
0 < B

goal (1 subgoal):
 1. B * Max (ff ` {s..t}) \<le> B * Max (ff ` {s..t + 1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B * Max (ff ` {s..t}) \<le> B * Max (ff ` {s..t + 1})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
B * Max (ff ` {s..t}) \<le> B * Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A \<le> B * Max (ff ` {s..t + 1})
[PROOF STEP]
have "A \<le> B * Max (ff ` {s..t + 1})"
[PROOF STATE]
proof (prove)
using this:
A \<le> B * Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. A \<le> B * Max (ff ` {s..t + 1})
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
using this:
A \<le> (\<Prod>j. d (t + 1 + j)) * Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. A \<le> (\<Prod>j. d (t + 1 + j)) * Max (ff ` {s..t + 1})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A \<le> B * Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A \<le> B * Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
have "B < A / Max (ff ` {s..t + 1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B < A / Max (ff ` {s..t + 1})
[PROOF STEP]
using 8[rule_format, of "t+1",folded ff_def B_def] \<open>s\<le>t\<close>
[PROOF STATE]
proof (prove)
using this:
s \<le> t + 1 \<Longrightarrow> B < A / Max (ff ` {s..t + 1})
s \<le> t

goal (1 subgoal):
 1. B < A / Max (ff ` {s..t + 1})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B < A / Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
B < A / Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
have "Max (ff ` {s..t+1})>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < Max (ff ` {s..t + 1})
[PROOF STEP]
using \<open>A \<le> B * Max (ff ` {s..t + 1})\<close> \<open>B>0\<close> \<open>A>1\<close> zero_less_mult_pos [of B "Max (ff ` {s..Suc t})"]
[PROOF STATE]
proof (prove)
using this:
A \<le> B * Max (ff ` {s..t + 1})
0 < B
1 < A
\<lbrakk>0 < B * Max (ff ` {s..Suc t}); 0 < B\<rbrakk> \<Longrightarrow> 0 < Max (ff ` {s..Suc t})

goal (1 subgoal):
 1. 0 < Max (ff ` {s..t + 1})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 < Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>s. \<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)))) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A \<le> B * Max (ff ` {s..t + 1})
B < A / Max (ff ` {s..t + 1})
0 < Max (ff ` {s..t + 1})
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
A \<le> B * Max (ff ` {s..t + 1})
B < A / Max (ff ` {s..t + 1})
0 < Max (ff ` {s..t + 1})

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed