[STATEMENT]
lemma
  fixes d ::"nat\<Rightarrow>real " and  a b ::"nat\<Rightarrow>int " and A::real
  assumes "A > 1" and d: "\<forall>n. d n> 1" and a: "\<forall>n. a n>0" and b:"\<forall>n. b n>0"
    and assu1: "(( \<lambda> n. (of_int (a n)) powr(1 /of_int (2^n)))\<longlongrightarrow> A) sequentially "
    and assu3: "filterlim ( \<lambda> n. (d n)^(2^n)/ b n) at_top sequentially"
    and "convergent_prod d"
  shows issummable: "summable (\<lambda>j. b j / a j)"
    and show5: "\<forall>\<^sub>F n in sequentially. (\<Sum>j. (b (n + j)) / (a (n + j))) \<le> 2 * b n / a n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>j. real_of_int (b j) / real_of_int (a j)) &&& \<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)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. summable (\<lambda>j. real_of_int (b j) / real_of_int (a j))
 2. \<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)
[PROOF STEP]
define c where "c = (\<lambda>j. b j / a j)"
[PROOF STATE]
proof (state)
this:
c = (\<lambda>j. real_of_int (b j) / real_of_int (a j))

goal (2 subgoals):
 1. summable (\<lambda>j. real_of_int (b j) / real_of_int (a j))
 2. \<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)
[PROOF STEP]
have c_pos:"c j>0" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c j
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n
\<forall>n. 0 < b n

goal (1 subgoal):
 1. 0 < c j
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n
\<forall>n. 0 < b n

goal (1 subgoal):
 1. 0 < real_of_int (b j) / real_of_int (a j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < c ?j

goal (2 subgoals):
 1. summable (\<lambda>j. real_of_int (b j) / real_of_int (a j))
 2. \<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)
[PROOF STEP]
have c_ratio_tendsto:"(\<lambda>n. c (n+1) / c n ) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
define nn where "nn \<equiv> (\<lambda>n. (2::int) ^ (Suc n))"
[PROOF STATE]
proof (state)
this:
nn \<equiv> \<lambda>n. 2 ^ Suc n

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
define ff where "ff \<equiv> (\<lambda>n. (a n / a (Suc n)) powr(1 /nn n)*(d(Suc n)))"
[PROOF STATE]
proof (state)
this:
ff \<equiv> \<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n)) * d (Suc n)

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
have nn_pos:"nn n>0" and ff_pos:"ff n>0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < nn n &&& 0 < ff n
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < nn n
[PROOF STEP]
unfolding nn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ Suc n
[PROOF STEP]
by simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < ff n
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < ff n
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n)) * d (Suc n)
[PROOF STEP]
using d[rule_format, of "Suc n"] a[rule_format, of n] a[rule_format, of "Suc n"]
[PROOF STATE]
proof (prove)
using this:
1 < d (Suc n)
0 < a n
0 < a (Suc n)

goal (1 subgoal):
 1. 0 < (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n)) * d (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
0 < nn ?n
0 < ff ?n

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
have ff_tendsto:"ff \<longlonglongrightarrow> 1 / sqrt A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
have "(of_int (a n)) powr(1 / (nn n)) = sqrt(of_int (a n) powr(1 /of_int (2^n)))" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a n) powr (1 / real_of_int (nn n)) = sqrt (real_of_int (a n) powr (1 / real_of_int (2 ^ n)))
[PROOF STEP]
unfolding nn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int (a n) powr (1 / real_of_int (2 ^ Suc n)) = sqrt (real_of_int (a n) powr (1 / real_of_int (2 ^ n)))
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n

goal (1 subgoal):
 1. real_of_int (a n) powr (1 / real_of_int (2 ^ Suc n)) = sqrt (real_of_int (a n) powr (1 / real_of_int (2 ^ n)))
[PROOF STEP]
by (simp add: powr_half_sqrt [symmetric] powr_powr ac_simps)
[PROOF STATE]
proof (state)
this:
real_of_int (a ?n) powr (1 / real_of_int (nn ?n)) = sqrt (real_of_int (a ?n) powr (1 / real_of_int (2 ^ ?n)))

goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real_of_int (a ?n) powr (1 / real_of_int (nn ?n)) = sqrt (real_of_int (a ?n) powr (1 / real_of_int (2 ^ ?n)))

goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
have "(( \<lambda> n. sqrt(of_int (a n) powr(1 /of_int (2^n))))\<longlongrightarrow> sqrt A) sequentially "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. sqrt (real_of_int (a n) powr (1 / real_of_int (2 ^ n)))) \<longlonglongrightarrow> sqrt A
[PROOF STEP]
using assu1 tendsto_real_sqrt
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (a n) powr (1 / real_of_int (2 ^ n))) \<longlonglongrightarrow> A
(?f \<longlongrightarrow> ?x) ?F \<Longrightarrow> ((\<lambda>x. sqrt (?f x)) \<longlongrightarrow> sqrt ?x) ?F

goal (1 subgoal):
 1. (\<lambda>n. sqrt (real_of_int (a n) powr (1 / real_of_int (2 ^ n)))) \<longlonglongrightarrow> sqrt A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<lambda>n. sqrt (real_of_int (a n) powr (1 / real_of_int (2 ^ n)))) \<longlonglongrightarrow> sqrt A

goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real_of_int (a ?n) powr (1 / real_of_int (nn ?n)) = sqrt (real_of_int (a ?n) powr (1 / real_of_int (2 ^ ?n)))
(\<lambda>n. sqrt (real_of_int (a n) powr (1 / real_of_int (2 ^ n)))) \<longlonglongrightarrow> sqrt A
[PROOF STEP]
have "(( \<lambda> n. (of_int (a n)) powr(1 /of_int (nn n)))\<longlongrightarrow> sqrt A) sequentially "
[PROOF STATE]
proof (prove)
using this:
real_of_int (a ?n) powr (1 / real_of_int (nn ?n)) = sqrt (real_of_int (a ?n) powr (1 / real_of_int (2 ^ ?n)))
(\<lambda>n. sqrt (real_of_int (a n) powr (1 / real_of_int (2 ^ n)))) \<longlonglongrightarrow> sqrt A

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (a n) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> sqrt A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real_of_int (a n) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> sqrt A

goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
from tendsto_divide[OF this assu1[THEN LIMSEQ_ignore_initial_segment[where k=1]]]
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> 0 \<Longrightarrow> (\<lambda>x. real_of_int (a x) powr (1 / real_of_int (nn x)) / real_of_int (a (x + 1)) powr (1 / real_of_int (2 ^ (x + 1)))) \<longlonglongrightarrow> sqrt A / A
[PROOF STEP]
have "(\<lambda>n. (a n / a (Suc n)) powr(1 /nn n)) \<longlonglongrightarrow> 1/sqrt A"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> 0 \<Longrightarrow> (\<lambda>x. real_of_int (a x) powr (1 / real_of_int (nn x)) / real_of_int (a (x + 1)) powr (1 / real_of_int (2 ^ (x + 1)))) \<longlonglongrightarrow> sqrt A / A

goal (1 subgoal):
 1. (\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
using \<open>A>1\<close> a
[PROOF STATE]
proof (prove)
using this:
A \<noteq> 0 \<Longrightarrow> (\<lambda>x. real_of_int (a x) powr (1 / real_of_int (nn x)) / real_of_int (a (x + 1)) powr (1 / real_of_int (2 ^ (x + 1)))) \<longlonglongrightarrow> sqrt A / A
1 < A
\<forall>n. 0 < a n

goal (1 subgoal):
 1. (\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
unfolding nn_def
[PROOF STATE]
proof (prove)
using this:
A \<noteq> 0 \<Longrightarrow> (\<lambda>x. real_of_int (a x) powr (1 / real_of_int (2 ^ Suc x)) / real_of_int (a (x + 1)) powr (1 / real_of_int (2 ^ (x + 1)))) \<longlonglongrightarrow> sqrt A / A
1 < A
\<forall>n. 0 < a n

goal (1 subgoal):
 1. (\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (2 ^ Suc n))) \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
by (auto simp add:powr_divide less_imp_le inverse_eq_divide sqrt_divide_self_eq)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> 1 / sqrt A

goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> 1 / sqrt A

goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
have "(\<lambda>n. d (Suc n))\<longlonglongrightarrow> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. d (Suc n)) \<longlonglongrightarrow> 1
[PROOF STEP]
apply (rule convergent_prod_imp_LIMSEQ)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent_prod (\<lambda>n. d (Suc n))
[PROOF STEP]
using convergent_prod_iff_shift[of d 1] \<open>convergent_prod d\<close>
[PROOF STATE]
proof (prove)
using this:
convergent_prod (\<lambda>i. d (i + 1)) = convergent_prod d
convergent_prod d

goal (1 subgoal):
 1. convergent_prod (\<lambda>n. d (Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. d (Suc n)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> 1 / sqrt A
(\<lambda>n. d (Suc n)) \<longlonglongrightarrow> 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> 1 / sqrt A
(\<lambda>n. d (Suc n)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. ff \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n))) \<longlonglongrightarrow> 1 / sqrt A
(\<lambda>n. d (Suc n)) \<longlonglongrightarrow> 1

goal (1 subgoal):
 1. (\<lambda>n. (real_of_int (a n) / real_of_int (a (Suc n))) powr (1 / real_of_int (nn n)) * d (Suc n)) \<longlonglongrightarrow> 1 / sqrt A
[PROOF STEP]
by (auto intro:tendsto_eq_intros)
[PROOF STATE]
proof (state)
this:
ff \<longlonglongrightarrow> 1 / sqrt A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ff \<longlonglongrightarrow> 1 / sqrt A

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. (ff n) powr nn n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
define aa where "aa=(1+1/sqrt A) / 2"
[PROOF STATE]
proof (state)
this:
aa = (1 + 1 / sqrt A) / 2

goal (1 subgoal):
 1. (\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "eventually (\<lambda>n. ff n<aa) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. ff n < aa
[PROOF STEP]
apply (rule order_tendstoD[OF ff_tendsto])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / sqrt A < aa
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 / sqrt A < (1 + 1 / sqrt A) / 2
[PROOF STEP]
using \<open>A>1\<close>
[PROOF STATE]
proof (prove)
using this:
1 < A

goal (1 subgoal):
 1. 1 / sqrt A < (1 + 1 / sqrt A) / 2
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. ff n < aa

goal (1 subgoal):
 1. (\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. ff n < aa

goal (1 subgoal):
 1. (\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. aa powr nn n) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. aa powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>n. aa powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>y. aa ^ (nat \<circ> nn) y) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>y. aa ^ (nat \<circ> nn) y) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (rule tendsto_power_zero)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. filterlim (nat \<circ> nn) sequentially sequentially
 2. norm aa < 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterlim (nat \<circ> nn) sequentially sequentially
[PROOF STEP]
unfolding nn_def comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM y sequentially. nat (2 ^ Suc y) :> sequentially
[PROOF STEP]
apply (rule filterlim_subseq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono (\<lambda>y. nat (2 ^ Suc y))
[PROOF STEP]
by (auto intro:strict_monoI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm aa < 1
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm aa < 1
[PROOF STEP]
unfolding aa_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm ((1 + 1 / sqrt A) / 2) < 1
[PROOF STEP]
using \<open>A>1\<close>
[PROOF STATE]
proof (prove)
using this:
1 < A

goal (1 subgoal):
 1. norm ((1 + 1 / sqrt A) / 2) < 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>y. aa ^ (nat \<circ> nn) y) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. aa powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>y. aa ^ (nat \<circ> nn) y) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>y. aa ^ (nat \<circ> nn) y) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. aa powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
proof (elim filterlim_mono_eventually)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. aa ^ (nat \<circ> nn) x = aa powr real_of_int (nn x)
[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 < (1 + 1 / sqrt A) / 2
[PROOF STEP]
using \<open>A>1\<close>
[PROOF STATE]
proof (prove)
using this:
1 < A

goal (1 subgoal):
 1. 0 < (1 + 1 / sqrt A) / 2
[PROOF STEP]
by  (auto simp add:field_simps pos_add_strict)
[PROOF STATE]
proof (state)
this:
0 < aa

goal (3 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. aa ^ (nat \<circ> nn) x = aa powr real_of_int (nn x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < aa
[PROOF STEP]
show " \<forall>\<^sub>F x in sequentially. aa ^ (nat \<circ> nn) x = aa powr real_of_int (nn x)"
[PROOF STATE]
proof (prove)
using this:
0 < aa

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. aa ^ (nat \<circ> nn) x = aa powr real_of_int (nn x)
[PROOF STEP]
by (auto simp: powr_int order.strict_implies_order[OF nn_pos])
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. aa ^ (nat \<circ> nn) x = aa powr real_of_int (nn x)

goal (2 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. aa powr real_of_int (nn n)) \<longlonglongrightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. aa powr real_of_int (nn n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. ff n < aa
(\<lambda>n. aa powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. ff n < aa
(\<lambda>n. aa powr real_of_int (nn n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (elim metric_tendsto_imp_tendsto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. ff n < aa \<Longrightarrow> \<forall>\<^sub>F x in sequentially. dist (ff x powr real_of_int (nn x)) 0 \<le> dist (aa powr real_of_int (nn x)) 0
[PROOF STEP]
apply (auto intro!:powr_mono2 elim!:eventually_mono)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. ff x < aa \<Longrightarrow> 0 \<le> nn x
 2. \<And>x. ff x < aa \<Longrightarrow> 0 \<le> ff x
[PROOF STEP]
using nn_pos ff_pos
[PROOF STATE]
proof (prove)
using this:
0 < nn ?n
0 < ff ?n

goal (2 subgoals):
 1. \<And>x. ff x < aa \<Longrightarrow> 0 \<le> nn x
 2. \<And>x. ff x < aa \<Longrightarrow> 0 \<le> ff x
[PROOF STEP]
by (meson le_cases not_le)+
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. (d (Suc n))^(nat (nn n)) * (a n / a (Suc n))) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. ff n powr real_of_int (nn n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. d (Suc n) ^ nat (nn n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
[PROOF STEP]
proof (elim filterlim_mono_eventually)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. ff x powr real_of_int (nn x) = d (Suc x) ^ nat (nn x) * (real_of_int (a x) / real_of_int (a (Suc x)))
[PROOF STEP]
show "\<forall>\<^sub>F x in sequentially. ff x powr  (nn x) = d (Suc x) ^ nat (nn x) * (a x / a (Suc x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. ff x powr real_of_int (nn x) = d (Suc x) ^ nat (nn x) * (real_of_int (a x) / real_of_int (a (Suc x)))
[PROOF STEP]
apply (rule eventuallyI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. ff x powr real_of_int (nn x) = d (Suc x) ^ nat (nn x) * (real_of_int (a x) / real_of_int (a (Suc x)))
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ff x powr real_of_int (nn x) = d (Suc x) ^ nat (nn x) * (real_of_int (a x) / real_of_int (a (Suc x)))
[PROOF STEP]
unfolding ff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((real_of_int (a x) / real_of_int (a (Suc x))) powr (1 / real_of_int (nn x)) * d (Suc x)) powr real_of_int (nn x) = d (Suc x) ^ nat (nn x) * (real_of_int (a x) / real_of_int (a (Suc x)))
[PROOF STEP]
using a[rule_format,of x] a[rule_format,of "Suc x"] d[rule_format,of "Suc x"] nn_pos[of x]
[PROOF STATE]
proof (prove)
using this:
0 < a x
0 < a (Suc x)
1 < d (Suc x)
0 < nn x

goal (1 subgoal):
 1. ((real_of_int (a x) / real_of_int (a (Suc x))) powr (1 / real_of_int (nn x)) * d (Suc x)) powr real_of_int (nn x) = d (Suc x) ^ nat (nn x) * (real_of_int (a x) / real_of_int (a (Suc x)))
[PROOF STEP]
apply (auto simp add:field_simps powr_divide powr_powr powr_mult )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < a x; 0 < a (Suc x); 1 < d (Suc x); 0 < nn x\<rbrakk> \<Longrightarrow> d (Suc x) powr real_of_int (nn x) = d (Suc x) ^ nat (nn x)
[PROOF STEP]
by (simp add: powr_int)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in sequentially. ff x powr real_of_int (nn x) = d (Suc x) ^ nat (nn x) * (real_of_int (a x) / real_of_int (a (Suc x)))

goal (2 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(\<lambda>n. d (Suc n) ^ nat (nn n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<lambda>n. d (Suc n) ^ nat (nn n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. b (Suc n) / (d (Suc n))^(nat (nn n))) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b (Suc n)) / d (Suc n) ^ nat (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
using tendsto_inverse_0_at_top[OF assu3,THEN LIMSEQ_ignore_initial_segment[where k=1]]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. inverse (d (n + 1) ^ 2 ^ (n + 1) / real_of_int (b (n + 1)))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b (Suc n)) / d (Suc n) ^ nat (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
unfolding nn_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. inverse (d (n + 1) ^ 2 ^ (n + 1) / real_of_int (b (n + 1)))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b (Suc n)) / d (Suc n) ^ nat (2 ^ Suc n)) \<longlonglongrightarrow> 0
[PROOF STEP]
by (auto simp add:field_simps nat_mult_distrib nat_power_eq)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real_of_int (b (Suc n)) / d (Suc n) ^ nat (nn n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. d (Suc n) ^ nat (nn n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
(\<lambda>n. real_of_int (b (Suc n)) / d (Suc n) ^ nat (nn n)) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. b (Suc n) * (a n / a (Suc n))) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. d (Suc n) ^ nat (nn n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
(\<lambda>n. real_of_int (b (Suc n)) / d (Suc n) ^ nat (nn n)) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b (Suc n)) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>n. d (Suc n) ^ nat (nn n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0; (\<lambda>n. real_of_int (b (Suc n)) / d (Suc n) ^ nat (nn n)) \<longlonglongrightarrow> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. real_of_int (b (Suc n)) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
[PROOF STEP]
subgoal premises asm
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b (Suc n)) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
[PROOF STEP]
using tendsto_mult[OF asm,simplified]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. if d (Suc x) = 0 \<and> 0 < nn x then 0 else real_of_int (a x) * real_of_int (b (Suc x)) / real_of_int (a (Suc x))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b (Suc n)) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (elim filterlim_mono_eventually)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. (if d (Suc x) = 0 \<and> 0 < nn x then 0 else real_of_int (a x) * real_of_int (b (Suc x)) / real_of_int (a (Suc x))) = real_of_int (b (Suc x)) * (real_of_int (a x) / real_of_int (a (Suc x)))
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 1 < d n

goal (3 subgoals):
 1. nhds 0 \<le> nhds 0
 2. sequentially \<le> sequentially
 3. \<forall>\<^sub>F x in sequentially. (if d (Suc x) = 0 \<and> 0 < nn x then 0 else real_of_int (a x) * real_of_int (b (Suc x)) / real_of_int (a (Suc x))) = real_of_int (b (Suc x)) * (real_of_int (a x) / real_of_int (a (Suc x)))
[PROOF STEP]
by (auto simp add:algebra_simps,metis (mono_tags, lifting) always_eventually
            not_one_less_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real_of_int (b (Suc n)) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. real_of_int (b (Suc n)) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. (b (Suc n) / b n) * (a n / a (Suc n))) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (Suc n)) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b (Suc n)) / real_of_int (b n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0
[PROOF STEP]
apply (elim Lim_transform_bound[rotated])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (real_of_int (b (Suc n)) / real_of_int (b n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<le> norm (real_of_int (b (Suc n)) * (real_of_int (a n) / real_of_int (a (Suc n))))
[PROOF STEP]
apply (rule eventuallyI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. norm (real_of_int (b (Suc x)) / real_of_int (b x) * (real_of_int (a x) / real_of_int (a (Suc x)))) \<le> norm (real_of_int (b (Suc x)) * (real_of_int (a x) / real_of_int (a (Suc x))))
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (real_of_int (b (Suc x)) / real_of_int (b x) * (real_of_int (a x) / real_of_int (a (Suc x)))) \<le> norm (real_of_int (b (Suc x)) * (real_of_int (a x) / real_of_int (a (Suc x))))
[PROOF STEP]
using a[rule_format, of x] a[rule_format, of "Suc x"]
          b[rule_format, of x] b[rule_format, of "Suc x"]
[PROOF STATE]
proof (prove)
using this:
0 < a x
0 < a (Suc x)
0 < b x
0 < b (Suc x)

goal (1 subgoal):
 1. norm (real_of_int (b (Suc x)) / real_of_int (b x) * (real_of_int (a x) / real_of_int (a (Suc x)))) \<le> norm (real_of_int (b (Suc x)) * (real_of_int (a x) / real_of_int (a (Suc x))))
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>n. real_of_int (b (Suc n)) / real_of_int (b n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0

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

goal (1 subgoal):
 1. (\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (Suc n)) / real_of_int (b n) * (real_of_int (a n) / real_of_int (a (Suc n)))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)) / (real_of_int (b n) / real_of_int (a n))) \<longlonglongrightarrow> 0
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0

goal (2 subgoals):
 1. summable (\<lambda>j. real_of_int (b j) / real_of_int (a j))
 2. \<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)
[PROOF STEP]
from c_ratio_tendsto
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0
[PROOF STEP]
have "(\<lambda>n. norm (b (Suc n) / a (Suc n)) / norm (b n / a n)) \<longlonglongrightarrow> 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. c (n + 1) / c n) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. norm (real_of_int (b (Suc n)) / real_of_int (a (Suc n))) / norm (real_of_int (b n) / real_of_int (a n))) \<longlonglongrightarrow> 0
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)) / (real_of_int (b n) / real_of_int (a n))) \<longlonglongrightarrow> 0

goal (1 subgoal):
 1. (\<lambda>n. norm (real_of_int (b (Suc n)) / real_of_int (a (Suc n))) / norm (real_of_int (b n) / real_of_int (a n))) \<longlonglongrightarrow> 0
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)) / (real_of_int (b n) / real_of_int (a n))) \<longlonglongrightarrow> 0
\<forall>n. 0 < a n
\<forall>n. 0 < b n

goal (1 subgoal):
 1. (\<lambda>n. norm (real_of_int (b (Suc n)) / real_of_int (a (Suc n))) / norm (real_of_int (b n) / real_of_int (a n))) \<longlonglongrightarrow> 0
[PROOF STEP]
by (force simp add:divide_simps abs_of_pos intro: Lim_transform_eventually)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. norm (real_of_int (b (Suc n)) / real_of_int (a (Suc n))) / norm (real_of_int (b n) / real_of_int (a n))) \<longlonglongrightarrow> 0

goal (2 subgoals):
 1. summable (\<lambda>j. real_of_int (b j) / real_of_int (a j))
 2. \<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)
[PROOF STEP]
from summable_ratio_test_tendsto[OF _ _ this] a b
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 < 1; \<forall>n. real_of_int (b n) / real_of_int (a n) \<noteq> 0\<rbrakk> \<Longrightarrow> summable (\<lambda>n. real_of_int (b n) / real_of_int (a n))
\<forall>n. 0 < a n
\<forall>n. 0 < b n
[PROOF STEP]
show "summable c"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < 1; \<forall>n. real_of_int (b n) / real_of_int (a n) \<noteq> 0\<rbrakk> \<Longrightarrow> summable (\<lambda>n. real_of_int (b n) / real_of_int (a n))
\<forall>n. 0 < a n
\<forall>n. 0 < b n

goal (1 subgoal):
 1. summable c
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < 1; \<forall>n. real_of_int (b n) / real_of_int (a n) \<noteq> 0\<rbrakk> \<Longrightarrow> summable (\<lambda>n. real_of_int (b n) / real_of_int (a n))
\<forall>n. 0 < a n
\<forall>n. 0 < b n

goal (1 subgoal):
 1. summable (\<lambda>j. real_of_int (b j) / real_of_int (a j))
[PROOF STEP]
by (metis c_def c_pos less_irrefl zero_less_one)
[PROOF STATE]
proof (state)
this:
summable c

goal (1 subgoal):
 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)
[PROOF STEP]
have "\<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n
[PROOF STEP]
obtain N where N_ratio:"\<forall>n\<ge>N. c (n + 1) / c n < 1 / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. c (n + 1) / c n < 1 / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. c (n + 1) / c n < 1 / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "eventually (\<lambda>n. c (n+1) / c n < 1/2) sequentially"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. c (n + 1) / c n < 1 / 2
[PROOF STEP]
using c_ratio_tendsto[unfolded tendsto_iff,rule_format, of "1/2",simplified]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in sequentially. \<bar>c (Suc x)\<bar> * 2 / \<bar>c x\<bar> < 1

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. c (n + 1) / c n < 1 / 2
[PROOF STEP]
apply eventually_elim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<bar>c (Suc n)\<bar> * 2 / \<bar>c n\<bar> < 1 \<Longrightarrow> c (n + 1) / c n < 1 / 2
[PROOF STEP]
subgoal for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>c (Suc n)\<bar> * 2 / \<bar>c n\<bar> < 1 \<Longrightarrow> c (n + 1) / c n < 1 / 2
[PROOF STEP]
using c_pos[of n] c_pos[of "Suc n"]
[PROOF STATE]
proof (prove)
using this:
0 < c n
0 < c (Suc n)

goal (1 subgoal):
 1. \<bar>c (Suc n)\<bar> * 2 / \<bar>c n\<bar> < 1 \<Longrightarrow> c (n + 1) / c n < 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. c (n + 1) / c n < 1 / 2

goal (1 subgoal):
 1. (\<And>N. \<forall>n\<ge>N. c (n + 1) / c n < 1 / 2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. c (n + 1) / c n < 1 / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. c (n + 1) / c n < 1 / 2

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. c (n + 1) / c n < 1 / 2
\<forall>n\<ge>?N. c (n + 1) / c n < 1 / 2 \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
\<exists>N. \<forall>n\<ge>N. c (n + 1) / c n < 1 / 2
\<forall>n\<ge>?N. c (n + 1) / c n < 1 / 2 \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>N. c (n + 1) / c n < 1 / 2

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n
[PROOF STEP]
have "(\<Sum>j. c (j + n)) \<le> 2 * c n" when "n\<ge>N" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j. c (j + n)) \<le> 2 * c n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>j. c (j + n)) \<le> 2 * c n
[PROOF STEP]
have "(\<Sum>j<m. c (j + n)) \<le> 2*c n * (1 - 1 / 2^(m+1))" for m
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1))
[PROOF STEP]
proof (induct m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>j<0. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (0 + 1))
 2. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<Sum>j<0. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (0 + 1))
 2. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<0. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (0 + 1))
[PROOF STEP]
using c_pos[of n]
[PROOF STATE]
proof (prove)
using this:
0 < c n

goal (1 subgoal):
 1. (\<Sum>j<0. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (0 + 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j<0. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (0 + 1))

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
(\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1))

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
have "(\<Sum>j<Suc m. c (j + n)) = c n + (\<Sum>i<m. c (Suc i + n)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<Suc m. c (j + n)) = c n + (\<Sum>i<m. c (Suc i + n))
[PROOF STEP]
unfolding sum.lessThan_Suc_shift
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c (0 + n) + (\<Sum>i<m. c (Suc i + n)) = c n + (\<Sum>i<m. c (Suc i + n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j<Suc m. c (j + n)) = c n + (\<Sum>i<m. c (Suc i + n))

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j<Suc m. c (j + n)) = c n + (\<Sum>i<m. c (Suc i + n))

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
have "... \<le> c n + (\<Sum>i<m. c (i + n) / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c n + (\<Sum>i<m. c (Suc i + n)) \<le> c n + (\<Sum>i<m. c (i + n) / 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c n + (\<Sum>i<m. c (Suc i + n)) \<le> c n + (\<Sum>i<m. c (i + n) / 2)
[PROOF STEP]
have "c (Suc i + n) \<le> c (i + n) / 2" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c (Suc i + n) \<le> c (i + n) / 2
[PROOF STEP]
using N_ratio[rule_format,of "i+n"] \<open>n\<ge>N\<close> c_pos[of "i+n"]
[PROOF STATE]
proof (prove)
using this:
N \<le> i + n \<Longrightarrow> c (i + n + 1) / c (i + n) < 1 / 2
N \<le> n
0 < c (i + n)

goal (1 subgoal):
 1. c (Suc i + n) \<le> c (i + n) / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c (Suc ?i + n) \<le> c (?i + n) / 2

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

goal (1 subgoal):
 1. c n + (\<Sum>i<m. c (Suc i + n)) \<le> c n + (\<Sum>i<m. c (i + n) / 2)
[PROOF STEP]
by (auto intro:sum_mono)
[PROOF STATE]
proof (state)
this:
c n + (\<Sum>i<m. c (Suc i + n)) \<le> c n + (\<Sum>i<m. c (i + n) / 2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c n + (\<Sum>i<m. c (Suc i + n)) \<le> c n + (\<Sum>i<m. c (i + n) / 2)

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c n + (\<Sum>i<m. c (Suc i + n)) \<le> c n + (\<Sum>i<m. c (i + n) / 2)

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
have "... = c n + (\<Sum>i<m. c (i + n)) / 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c n + (\<Sum>i<m. c (i + n) / 2) = c n + (\<Sum>i<m. c (i + n)) / 2
[PROOF STEP]
unfolding sum_divide_distrib
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c n + (\<Sum>i<m. c (i + n) / 2) = c n + (\<Sum>na<m. c (na + n) / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c n + (\<Sum>i<m. c (i + n) / 2) = c n + (\<Sum>i<m. c (i + n)) / 2

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c n + (\<Sum>i<m. c (i + n) / 2) = c n + (\<Sum>i<m. c (i + n)) / 2

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
have "... \<le> c n + c n * (1 - 1 / 2 ^ (m + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c n + (\<Sum>i<m. c (i + n)) / 2 \<le> c n + c n * (1 - 1 / 2 ^ (m + 1))
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1))

goal (1 subgoal):
 1. c n + (\<Sum>i<m. c (i + n)) / 2 \<le> c n + c n * (1 - 1 / 2 ^ (m + 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c n + (\<Sum>i<m. c (i + n)) / 2 \<le> c n + c n * (1 - 1 / 2 ^ (m + 1))

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c n + (\<Sum>i<m. c (i + n)) / 2 \<le> c n + c n * (1 - 1 / 2 ^ (m + 1))

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
have "... = 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c n + c n * (1 - 1 / 2 ^ (m + 1)) = 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
by (auto simp add:field_simps)
[PROOF STATE]
proof (state)
this:
c n + c n * (1 - 1 / 2 ^ (m + 1)) = 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))

goal (1 subgoal):
 1. \<And>m. (\<Sum>j<m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (m + 1)) \<Longrightarrow> (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))

goal (1 subgoal):
 1. (\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>j<Suc m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (?m + 1))

goal (1 subgoal):
 1. (\<Sum>j. c (j + n)) \<le> 2 * c n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (?m + 1))
[PROOF STEP]
have "(\<Sum>j<m. c (j + n)) \<le> 2*c n" for m
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (?m + 1))

goal (1 subgoal):
 1. (\<Sum>j<m. c (j + n)) \<le> 2 * c n
[PROOF STEP]
using c_pos[of n]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n * (1 - 1 / 2 ^ (?m + 1))
0 < c n

goal (1 subgoal):
 1. (\<Sum>j<m. c (j + n)) \<le> 2 * c n
[PROOF STEP]
by (smt divide_le_eq_1_pos divide_pos_pos nonzero_mult_div_cancel_left zero_less_power)
[PROOF STATE]
proof (state)
this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n

goal (1 subgoal):
 1. (\<Sum>j. c (j + n)) \<le> 2 * c n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n

goal (1 subgoal):
 1. (\<Sum>j. c (j + n)) \<le> 2 * c n
[PROOF STEP]
have "summable (\<lambda>j. c (j + n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>j. c (j + n))
[PROOF STEP]
using \<open>summable c\<close>
[PROOF STATE]
proof (prove)
using this:
summable c

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

goal (1 subgoal):
 1. (\<Sum>j. c (j + n)) \<le> 2 * c n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n
summable (\<lambda>j. c (j + n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n
summable (\<lambda>j. c (j + n))

goal (1 subgoal):
 1. (\<Sum>j. c (j + n)) \<le> 2 * c n
[PROOF STEP]
using suminf_le_const[of "\<lambda>j. c (j+n)" "2*c n"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j<?m. c (j + n)) \<le> 2 * c n
summable (\<lambda>j. c (j + n))
\<lbrakk>summable (\<lambda>j. c (j + n)); \<And>na. (\<Sum>j<na. c (j + n)) \<le> 2 * c n\<rbrakk> \<Longrightarrow> (\<Sum>j. c (j + n)) \<le> 2 * c n

goal (1 subgoal):
 1. (\<Sum>j. c (j + n)) \<le> 2 * c n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>j. c (j + n)) \<le> 2 * c n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> (\<Sum>j. c (j + ?n)) \<le> 2 * c ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<le> ?n \<Longrightarrow> (\<Sum>j. c (j + ?n)) \<le> 2 * c ?n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n \<Longrightarrow> (\<Sum>j. c (j + ?n)) \<le> 2 * c ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n
[PROOF STEP]
unfolding eventually_sequentially
[PROOF STATE]
proof (prove)
using this:
N \<le> ?n \<Longrightarrow> (\<Sum>j. c (j + ?n)) \<le> 2 * c ?n

goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. (\<Sum>j. c (n + j)) \<le> 2 * c n
[PROOF STEP]
by (auto simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n

goal (1 subgoal):
 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)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n
[PROOF STEP]
show "\<forall>\<^sub>F n in sequentially. (\<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. (\<Sum>j. c (n + j)) \<le> 2 * c n

goal (1 subgoal):
 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)
[PROOF STEP]
unfolding c_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. (\<Sum>j. real_of_int (b (n + j)) / real_of_int (a (n + j))) \<le> 2 * (real_of_int (b n) / real_of_int (a n))

goal (1 subgoal):
 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)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<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:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Hancl3:
  fixes d ::"nat\<Rightarrow>real" and  a b :: "nat\<Rightarrow>int"
  assumes "A > 1" and d: "\<forall>n. d n > 1" and a: "\<forall>n. a n>0" and b: "\<forall>n. b n > 0" and "s>0"
    and assu1: "(\<lambda>n. (a n) powr(1 / of_int(2^n))) \<longlonglongrightarrow> A"
    and assu2: "\<forall>n \<ge> s. A / (a n) powr (1 / of_int(2^n)) > (\<Prod>j. d (n+j))"
    and assu3: "LIM n sequentially. d n ^ 2 ^ n / b n :> at_top"
    and "convergent_prod d"
  shows "(\<Sum>n. b n / a n) \<notin> \<rat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat>
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat> \<Longrightarrow> False
[PROOF STEP]
assume asm: "\<not> ((\<Sum>n. b n / a n) \<notin> \<rat>)"
[PROOF STATE]
proof (state)
this:
\<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat>

goal (1 subgoal):
 1. \<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat> \<Longrightarrow> False
[PROOF STEP]
have ab_sum: "summable (\<lambda>j. b j / a j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>j. real_of_int (b j) / real_of_int (a j))
[PROOF STEP]
using issummable[OF \<open>A>1\<close> d a b assu1 assu3 \<open>convergent_prod d\<close>]
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>j. real_of_int (b j) / real_of_int (a j))

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

goal (1 subgoal):
 1. \<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat> \<Longrightarrow> False
[PROOF STEP]
obtain p q ::int where "q>0" and pq_def: "(\<lambda>n. b (n+1) / a (n+1)) sums (p/q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q p. \<lbrakk>0 < q; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>q p. \<lbrakk>0 < q; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from asm
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat>
[PROOF STEP]
have "(\<Sum>n. b n / a n) \<in> \<rat>"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat>

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<in> \<rat>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<in> \<rat>

goal (1 subgoal):
 1. (\<And>q p. \<lbrakk>0 < q; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<in> \<rat>
[PROOF STEP]
have "(\<Sum>n. b (n+1) / a (n+1)) \<in> \<rat>"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<in> \<rat>

goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) \<in> \<rat>
[PROOF STEP]
apply (subst suminf_minus_initial_segment[OF ab_sum,of 1])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<in> \<rat> \<Longrightarrow> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) - (\<Sum>i<1. real_of_int (b i) / real_of_int (a i)) \<in> \<rat>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) \<in> \<rat>

goal (1 subgoal):
 1. (\<And>q p. \<lbrakk>0 < q; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) \<in> \<rat>
[PROOF STEP]
obtain p' q' ::int where "q'\<noteq>0" and pq_def: "(\<lambda> n. b (n+1) / a (n+1) ) sums (p'/q')"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) \<in> \<rat>

goal (1 subgoal):
 1. (\<And>q' p'. \<lbrakk>q' \<noteq> 0; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Rats_eq_int_div_int
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) \<in> {real_of_int i / real_of_int j |i j. j \<noteq> 0}

goal (1 subgoal):
 1. (\<And>q' p'. \<lbrakk>q' \<noteq> 0; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using summable_ignore_initial_segment[OF ab_sum,of 1,THEN summable_sums]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) \<in> {real_of_int i / real_of_int j |i j. j \<noteq> 0}
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))

goal (1 subgoal):
 1. (\<And>q' p'. \<lbrakk>q' \<noteq> 0; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
q' \<noteq> 0
(\<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. (\<And>q p. \<lbrakk>0 < q; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define p q where "p \<equiv> (if q'<0 then -p' else p')" and "q \<equiv> (if q'<0 then -q' else q')"
[PROOF STATE]
proof (state)
this:
p \<equiv> if q' < 0 then - p' else p'
q \<equiv> if q' < 0 then - q' else q'

goal (1 subgoal):
 1. (\<And>q p. \<lbrakk>0 < q; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "p'/q' = p/q" "q>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_int p' / real_of_int q' = real_of_int p / real_of_int q &&& 0 < q
[PROOF STEP]
using \<open>q'\<noteq>0\<close>
[PROOF STATE]
proof (prove)
using this:
q' \<noteq> 0

goal (1 subgoal):
 1. real_of_int p' / real_of_int q' = real_of_int p / real_of_int q &&& 0 < q
[PROOF STEP]
unfolding p_def q_def
[PROOF STATE]
proof (prove)
using this:
q' \<noteq> 0

goal (1 subgoal):
 1. real_of_int p' / real_of_int q' = real_of_int (if q' < 0 then - p' else p') / real_of_int (if q' < 0 then - q' else q') &&& 0 < (if q' < 0 then - q' else q')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real_of_int p' / real_of_int q' = real_of_int p / real_of_int q
0 < q

goal (1 subgoal):
 1. (\<And>q p. \<lbrakk>0 < q; (\<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> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int p' / real_of_int q' = real_of_int p / real_of_int q
0 < q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int p' / real_of_int q' = real_of_int p / real_of_int q
0 < q

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that[of q p] pq_def
[PROOF STATE]
proof (prove)
using this:
real_of_int p' / real_of_int q' = real_of_int p / real_of_int q
0 < q
\<lbrakk>0 < q; (\<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> thesis
(\<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. thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < q
(\<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. \<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat> \<Longrightarrow> False
[PROOF STEP]
define ALPHA where
    "ALPHA = (\<lambda>n. of_int q * (\<Prod>j=1..n. of_int(a j)) * (\<Sum>j. (b (j+n+1)/a (j+n+1))))"
[PROOF STATE]
proof (state)
this:
ALPHA = (\<lambda>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))))

goal (1 subgoal):
 1. \<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat> \<Longrightarrow> False
[PROOF STEP]
have "ALPHA n \<ge> 1" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> ALPHA n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> ALPHA n
[PROOF STEP]
have "(\<Sum>n. b (n+1) / a (n+1)) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < (\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))
[PROOF STEP]
proof (rule suminf_pos)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. summable (\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))
 2. \<And>n. 0 < real_of_int (b (n + 1)) / real_of_int (a (n + 1))
[PROOF STEP]
show "summable (\<lambda>n. b (n + 1) / real_of_int (a (n + 1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable (\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))
[PROOF STEP]
using summable_ignore_initial_segment[OF ab_sum,of 1]
[PROOF STATE]
proof (prove)
using this:
summable (\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))

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

goal (1 subgoal):
 1. \<And>n. 0 < real_of_int (b (n + 1)) / real_of_int (a (n + 1))
[PROOF STEP]
show "\<And>n. 0 < b (n + 1) / a (n + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. 0 < real_of_int (b (n + 1)) / real_of_int (a (n + 1))
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n
\<forall>n. 0 < b n

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

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

goal (1 subgoal):
 1. 1 \<le> ALPHA n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < (\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))
[PROOF STEP]
have "p/q > 0"
[PROOF STATE]
proof (prove)
using this:
0 < (\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))

goal (1 subgoal):
 1. 0 < real_of_int p / real_of_int q
[PROOF STEP]
using pq_def sums_unique
[PROOF STATE]
proof (prove)
using this:
0 < (\<Sum>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1)))
(\<lambda>n. real_of_int (b (n + 1)) / real_of_int (a (n + 1))) sums (real_of_int p / real_of_int q)
?f sums ?s \<Longrightarrow> ?s = suminf ?f

goal (1 subgoal):
 1. 0 < real_of_int p / real_of_int q
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 < real_of_int p / real_of_int q

goal (1 subgoal):
 1. 1 \<le> ALPHA n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < real_of_int p / real_of_int q
[PROOF STEP]
have "q\<ge>1" "p\<ge>1"
[PROOF STATE]
proof (prove)
using this:
0 < real_of_int p / real_of_int q

goal (1 subgoal):
 1. 1 \<le> q &&& 1 \<le> p
[PROOF STEP]
using \<open>q>0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < real_of_int p / real_of_int q
0 < q

goal (1 subgoal):
 1. 1 \<le> q &&& 1 \<le> p
[PROOF STEP]
by (auto simp add:divide_simps)
[PROOF STATE]
proof (state)
this:
1 \<le> q
1 \<le> p

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

goal (1 subgoal):
 1. 1 \<le> ALPHA n
[PROOF STEP]
have "\<forall>n. 1 \<le> a n" "\<forall>n. 1 \<le> b n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. 1 \<le> a n &&& \<forall>n. 1 \<le> b n
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
\<forall>n. 0 < a n
\<forall>n. 0 < b n

goal (1 subgoal):
 1. \<forall>n. 1 \<le> a n &&& \<forall>n. 1 \<le> b n
[PROOF STEP]
by (auto simp add: int_one_le_iff_zero_less)
[PROOF STATE]
proof (state)
this:
\<forall>n. 1 \<le> a n
\<forall>n. 1 \<le> b n

goal (1 subgoal):
 1. 1 \<le> ALPHA n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 \<le> q
1 \<le> p
\<forall>n. 1 \<le> a n
\<forall>n. 1 \<le> b n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> q
1 \<le> p
\<forall>n. 1 \<le> a n
\<forall>n. 1 \<le> b n

goal (1 subgoal):
 1. 1 \<le> ALPHA n
[PROOF STEP]
unfolding ALPHA_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> q
1 \<le> p
\<forall>n. 1 \<le> a n
\<forall>n. 1 \<le> b n

goal (1 subgoal):
 1. 1 \<le> 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)))
[PROOF STEP]
using show7[OF _ _ _ _ pq_def]
[PROOF STATE]
proof (prove)
using this:
1 \<le> q
1 \<le> p
\<forall>n. 1 \<le> a n
\<forall>n. 1 \<le> b n
\<lbrakk>1 \<le> q; 1 \<le> p; \<forall>n. 1 \<le> a n; \<forall>n. 1 \<le> b n\<rbrakk> \<Longrightarrow> 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 (1 subgoal):
 1. 1 \<le> 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)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
1 \<le> ALPHA n

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

goal (1 subgoal):
 1. \<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> ALPHA ?n

goal (1 subgoal):
 1. \<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat> \<Longrightarrow> False
[PROOF STEP]
have "\<exists>n. ALPHA n < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. ALPHA n < 1
[PROOF STEP]
unfolding ALPHA_def
[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 (rule lasttoshow[OF d a \<open>s>0\<close> \<open>q>0\<close> \<open>A>1\<close> b _ assu3])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 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)))
 2. \<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)
[PROOF STEP]
show "\<forall>\<^sub>F n in sequentially. (\<Sum>j. b (n+j) / a (n+j)) \<le> (2 * b n) / a n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 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)
[PROOF STEP]
using show5[OF \<open>A>1\<close> d a b assu1 assu3 \<open>convergent_prod d\<close>]
[PROOF STATE]
proof (prove)
using this:
\<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. (\<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 simp
[PROOF STATE]
proof (state)
this:
\<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>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]
show "\<forall>m\<ge>s. \<exists>n\<ge>m. d (n+1) * (MAX j\<in>{s..n}. a j powr (1 / of_int (2 ^ j)))
                    \<le> a (n+1) powr (1 / of_int (2 ^ (n+1)))"
[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]
apply (rule show9[OF \<open>A>1\<close> d a \<open>s>0\<close> assu1 \<open>convergent_prod d\<close>])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<ge>s. (\<Prod>j. d (n + j)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
using show8[OF \<open>A>1\<close> d a \<open>s>0\<close> \<open>convergent_prod d\<close> assu2]
[PROOF STATE]
proof (prove)
using this:
\<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)))

goal (1 subgoal):
 1. \<forall>n\<ge>s. (\<Prod>j. d (n + j)) < A / (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))
[PROOF STEP]
by (simp add:algebra_simps)
[PROOF STATE]
proof (state)
this:
\<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)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>n. ALPHA n < 1

goal (1 subgoal):
 1. \<not> (\<Sum>n. real_of_int (b n) / real_of_int (a n)) \<notin> \<rat> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 \<le> ALPHA ?n
\<exists>n. ALPHA n < 1
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
1 \<le> ALPHA ?n
\<exists>n. ALPHA n < 1

goal (1 subgoal):
 1. False
[PROOF STEP]
using not_le
[PROOF STATE]
proof (prove)
using this:
1 \<le> ALPHA ?n
\<exists>n. ALPHA n < 1
(\<not> ?x \<le> ?y) = (?y < ?x)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cons_chainp:
  assumes "P x (S 0)" and "chainp P S"
  shows "chainp P (case_nat x S)" (is "chainp P ?S")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. P (case i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x) (case Suc i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. P (case i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x) (case Suc i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. P (case i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x) (case Suc i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x)
[PROOF STEP]
show "P (?S i) (?S (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (case i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x) (case Suc i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P x (S 0)
\<forall>i. P (S i) (S (Suc i))

goal (1 subgoal):
 1. P (case i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x) (case Suc i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x)
[PROOF STEP]
by (cases i) simp_all
[PROOF STATE]
proof (state)
this:
P (case i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x) (case Suc i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cons_chain:
  assumes "(x, S 0) \<in> r" and "chain r S" shows "chain r (case_nat x S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. (case i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x, case Suc i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x) \<in> r
[PROOF STEP]
using cons_chainp[of "\<lambda>x y. (x, y) \<in> r", OF assms]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. (case i of 0 \<Rightarrow> x | Suc i \<Rightarrow> S i, case Suc i of 0 \<Rightarrow> x | Suc i \<Rightarrow> S i) \<in> r

goal (1 subgoal):
 1. \<forall>i. (case i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x, case Suc i of 0 \<Rightarrow> x | Suc x \<Rightarrow> S x) \<in> r
[PROOF STEP]
.


[STATEMENT]
lemma chainp_imp_relpowp:
  assumes "chainp P S" shows "(P^^j) (S i) (S (i + j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P ^^ j) (S i) (S (i + j))
[PROOF STEP]
proof (induct "i + j" arbitrary: j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. 0 = i + j \<Longrightarrow> (P ^^ j) (S i) (S (i + j))
 2. \<And>x j. \<lbrakk>\<And>j. x = i + j \<Longrightarrow> (P ^^ j) (S i) (S (i + j)); Suc x = i + j\<rbrakk> \<Longrightarrow> (P ^^ j) (S i) (S (i + j))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n = i + ?j \<Longrightarrow> (P ^^ ?j) (S i) (S (i + ?j))
Suc n = i + j

goal (2 subgoals):
 1. \<And>j. 0 = i + j \<Longrightarrow> (P ^^ j) (S i) (S (i + j))
 2. \<And>x j. \<lbrakk>\<And>j. x = i + j \<Longrightarrow> (P ^^ j) (S i) (S (i + j)); Suc x = i + j\<rbrakk> \<Longrightarrow> (P ^^ j) (S i) (S (i + j))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n = i + ?j \<Longrightarrow> (P ^^ ?j) (S i) (S (i + ?j))
Suc n = i + j

goal (1 subgoal):
 1. (P ^^ j) (S i) (S (i + j))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n = i + ?j \<Longrightarrow> (P ^^ ?j) (S i) (S (i + ?j))
Suc n = i + j
\<forall>i. P (S i) (S (Suc i))

goal (1 subgoal):
 1. (P ^^ j) (S i) (S (i + j))
[PROOF STEP]
by (cases j) auto
[PROOF STATE]
proof (state)
this:
(P ^^ j) (S i) (S (i + j))

goal (1 subgoal):
 1. \<And>j. 0 = i + j \<Longrightarrow> (P ^^ j) (S i) (S (i + j))
[PROOF STEP]
qed simp


[STATEMENT]
lemma chain_imp_relpow:
  assumes "chain r S" shows "(S i, S (i + j)) \<in> r^^j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S i, S (i + j)) \<in> r ^^ j
[PROOF STEP]
proof (induct "i + j" arbitrary: j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. 0 = i + j \<Longrightarrow> (S i, S (i + j)) \<in> r ^^ j
 2. \<And>x j. \<lbrakk>\<And>j. x = i + j \<Longrightarrow> (S i, S (i + j)) \<in> r ^^ j; Suc x = i + j\<rbrakk> \<Longrightarrow> (S i, S (i + j)) \<in> r ^^ j
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n = i + ?j \<Longrightarrow> (S i, S (i + ?j)) \<in> r ^^ ?j
Suc n = i + j

goal (2 subgoals):
 1. \<And>j. 0 = i + j \<Longrightarrow> (S i, S (i + j)) \<in> r ^^ j
 2. \<And>x j. \<lbrakk>\<And>j. x = i + j \<Longrightarrow> (S i, S (i + j)) \<in> r ^^ j; Suc x = i + j\<rbrakk> \<Longrightarrow> (S i, S (i + j)) \<in> r ^^ j
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n = i + ?j \<Longrightarrow> (S i, S (i + ?j)) \<in> r ^^ ?j
Suc n = i + j

goal (1 subgoal):
 1. (S i, S (i + j)) \<in> r ^^ j
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n = i + ?j \<Longrightarrow> (S i, S (i + ?j)) \<in> r ^^ ?j
Suc n = i + j
\<forall>i. (S i, S (Suc i)) \<in> r

goal (1 subgoal):
 1. (S i, S (i + j)) \<in> r ^^ j
[PROOF STEP]
by (cases j) auto
[PROOF STATE]
proof (state)
this:
(S i, S (i + j)) \<in> r ^^ j

goal (1 subgoal):
 1. \<And>j. 0 = i + j \<Longrightarrow> (S i, S (i + j)) \<in> r ^^ j
[PROOF STEP]
qed simp


[STATEMENT]
lemma chainp_imp_tranclp:
  assumes "chainp P S" and "i < j" shows "P^++ (S i) (S j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>+\<^sup>+ (S i) (S j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P\<^sup>+\<^sup>+ (S i) (S j)
[PROOF STEP]
from less_imp_Suc_add[OF assms(2)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. j = Suc (i + k)
[PROOF STEP]
obtain n where "j = i + Suc n"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. j = Suc (i + k)

goal (1 subgoal):
 1. (\<And>n. j = i + Suc n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j = i + Suc n

goal (1 subgoal):
 1. P\<^sup>+\<^sup>+ (S i) (S j)
[PROOF STEP]
with chainp_imp_relpowp[of P S "Suc n" i, OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
(P ^^ Suc n) (S i) (S (i + Suc n))
j = i + Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(P ^^ Suc n) (S i) (S (i + Suc n))
j = i + Suc n

goal (1 subgoal):
 1. P\<^sup>+\<^sup>+ (S i) (S j)
[PROOF STEP]
unfolding trancl_power[of "(S i, S j)", to_pred]
[PROOF STATE]
proof (prove)
using this:
(P ^^ Suc n) (S i) (S (i + Suc n))
j = i + Suc n

goal (1 subgoal):
 1. \<exists>n>0. (P ^^ n) (S i) (S j)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
P\<^sup>+\<^sup>+ (S i) (S j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_imp_trancl:
  assumes "chain r S" and "i < j" shows "(S i, S j) \<in> r^+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S i, S j) \<in> r\<^sup>+
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (S i, S j) \<in> r\<^sup>+
[PROOF STEP]
from less_imp_Suc_add[OF assms(2)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. j = Suc (i + k)
[PROOF STEP]
obtain n where "j = i + Suc n"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. j = Suc (i + k)

goal (1 subgoal):
 1. (\<And>n. j = i + Suc n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j = i + Suc n

goal (1 subgoal):
 1. (S i, S j) \<in> r\<^sup>+
[PROOF STEP]
with chain_imp_relpow[OF assms(1), of i "Suc n"]
[PROOF STATE]
proof (chain)
picking this:
(S i, S (i + Suc n)) \<in> r ^^ Suc n
j = i + Suc n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(S i, S (i + Suc n)) \<in> r ^^ Suc n
j = i + Suc n

goal (1 subgoal):
 1. (S i, S j) \<in> r\<^sup>+
[PROOF STEP]
unfolding trancl_power
[PROOF STATE]
proof (prove)
using this:
(S i, S (i + Suc n)) \<in> r ^^ Suc n
j = i + Suc n

goal (1 subgoal):
 1. \<exists>n>0. (S i, S j) \<in> r ^^ n
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(S i, S j) \<in> r\<^sup>+

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chainp_imp_rtranclp:
  assumes "chainp P S" and "i \<le> j" shows "P^** (S i) (S j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>*\<^sup>* (S i) (S j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P\<^sup>*\<^sup>* (S i) (S j)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
[PROOF STEP]
obtain n where "j = i + n"
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. (\<And>n. j = i + n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (induct "j - i" arbitrary: j) force+
[PROOF STATE]
proof (state)
this:
j = i + n

goal (1 subgoal):
 1. P\<^sup>*\<^sup>* (S i) (S j)
[PROOF STEP]
with chainp_imp_relpowp[of P S, OF assms(1), of n i]
[PROOF STATE]
proof (chain)
picking this:
(P ^^ n) (S i) (S (i + n))
j = i + n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(P ^^ n) (S i) (S (i + n))
j = i + n

goal (1 subgoal):
 1. P\<^sup>*\<^sup>* (S i) (S j)
[PROOF STEP]
by (simp add: relpow_imp_rtrancl[of "(S i, S (i + n))", to_pred])
[PROOF STATE]
proof (state)
this:
P\<^sup>*\<^sup>* (S i) (S j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chain_imp_rtrancl:
  assumes "chain r S" and "i \<le> j" shows "(S i, S j) \<in> r^*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S i, S j) \<in> r\<^sup>*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (S i, S j) \<in> r\<^sup>*
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
[PROOF STEP]
obtain n where "j = i + n"
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. (\<And>n. j = i + n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (induct "j - i" arbitrary: j) force+
[PROOF STATE]
proof (state)
this:
j = i + n

goal (1 subgoal):
 1. (S i, S j) \<in> r\<^sup>*
[PROOF STEP]
with chain_imp_relpow[OF assms(1), of i n]
[PROOF STATE]
proof (chain)
picking this:
(S i, S (i + n)) \<in> r ^^ n
j = i + n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(S i, S (i + n)) \<in> r ^^ n
j = i + n

goal (1 subgoal):
 1. (S i, S j) \<in> r\<^sup>*
[PROOF STEP]
by (simp add: relpow_imp_rtrancl)
[PROOF STATE]
proof (state)
this:
(S i, S j) \<in> r\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stepfun_imp_chainp':
  assumes "\<forall>i\<ge>n::nat. f i \<ge> i \<and> P (S i) (S (f i))"
  shows "chainp P (\<lambda>i. S ((f ^^ i) n))" (is "chainp P ?T")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<ge>n. i \<le> f i \<and> P (S i) (S (f i))
[PROOF STEP]
have "(f ^^ i) n \<ge> n"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<ge>n. i \<le> f i \<and> P (S i) (S (f i))

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

goal (1 subgoal):
 1. \<And>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
[PROOF STEP]
with assms[THEN spec[of _ "(f ^^ i) n"]]
[PROOF STATE]
proof (chain)
picking this:
n \<le> (f ^^ i) n \<longrightarrow> (f ^^ i) n \<le> f ((f ^^ i) n) \<and> P (S ((f ^^ i) n)) (S (f ((f ^^ i) n)))
n \<le> (f ^^ i) n
[PROOF STEP]
show "P (?T i) (?T (Suc i))"
[PROOF STATE]
proof (prove)
using this:
n \<le> (f ^^ i) n \<longrightarrow> (f ^^ i) n \<le> f ((f ^^ i) n) \<and> P (S ((f ^^ i) n)) (S (f ((f ^^ i) n)))
n \<le> (f ^^ i) n

goal (1 subgoal):
 1. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stepfun_imp_chainp:
  assumes "\<forall>i\<ge>n::nat. f i > i \<and> P (S i) (S (f i))"
  shows "chainp P (\<lambda>i. S ((f ^^ i) n))" (is "chainp P ?T")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
[PROOF STEP]
using stepfun_imp_chainp'[of n f P S] and assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<ge>n. i \<le> f i \<and> P (S i) (S (f i)) \<Longrightarrow> \<forall>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
\<forall>i\<ge>n. i < f i \<and> P (S i) (S (f i))

goal (1 subgoal):
 1. \<forall>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
[PROOF STEP]
by force


[STATEMENT]
lemma subchain:
  assumes "\<forall>i::nat>n. \<exists>j>i. P (f i) (f j)"
  shows "\<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>i>n. \<exists>j>i. P (f i) (f j)
[PROOF STEP]
have "\<forall>i\<in>{i. i > n}. \<exists>j>i. P (f i) (f j)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i>n. \<exists>j>i. P (f i) (f j)

goal (1 subgoal):
 1. \<forall>i\<in>{i. n < i}. \<exists>j>i. P (f i) (f j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{i. n < i}. \<exists>j>i. P (f i) (f j)

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
from bchoice [OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>fa. \<forall>x\<in>{i. n < i}. x < fa x \<and> P (f x) (f (fa x))
[PROOF STEP]
obtain g
    where *: "\<forall>i>n. g i > i"
    and **: "\<forall>i>n. P (f i) (f (g i))"
[PROOF STATE]
proof (prove)
using this:
\<exists>fa. \<forall>x\<in>{i. n < i}. x < fa x \<and> P (f x) (f (fa x))

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>\<forall>i>n. i < g i; \<forall>i>n. P (f i) (f (g i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i>n. i < g i
\<forall>i>n. P (f i) (f (g i))

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
define \<phi> where [simp]: "\<phi> i = (g ^^ i) (Suc n)" for i
[PROOF STATE]
proof (state)
this:
\<phi> ?i = (g ^^ ?i) (Suc n)

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
\<forall>i>n. i < g i
[PROOF STEP]
have ***: "\<And>i. \<phi> i > n"
[PROOF STATE]
proof (prove)
using this:
\<forall>i>n. i < g i

goal (1 subgoal):
 1. \<And>i. n < \<phi> i
[PROOF STEP]
by (induct_tac i) auto
[PROOF STATE]
proof (state)
this:
n < \<phi> ?i

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n < \<phi> ?i
[PROOF STEP]
have "\<And>i. \<phi> i < \<phi> (Suc i)"
[PROOF STATE]
proof (prove)
using this:
n < \<phi> ?i

goal (1 subgoal):
 1. \<And>i. \<phi> i < \<phi> (Suc i)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
n < \<phi> ?i
\<forall>i>n. i < g i

goal (1 subgoal):
 1. \<And>i. \<phi> i < \<phi> (Suc i)
[PROOF STEP]
by (induct_tac i) auto
[PROOF STATE]
proof (state)
this:
\<phi> ?i < \<phi> (Suc ?i)

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<phi> ?i < \<phi> (Suc ?i)
[PROOF STEP]
have "\<And>i j. i < j \<Longrightarrow> \<phi> i < \<phi> j"
[PROOF STATE]
proof (prove)
using this:
\<phi> ?i < \<phi> (Suc ?i)

goal (1 subgoal):
 1. \<And>i j. i < j \<Longrightarrow> \<phi> i < \<phi> j
[PROOF STEP]
by (rule lift_Suc_mono_less)
[PROOF STATE]
proof (state)
this:
?i < ?j \<Longrightarrow> \<phi> ?i < \<phi> ?j

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?i < ?j \<Longrightarrow> \<phi> ?i < \<phi> ?j

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
have "\<And>i. P (f (\<phi> i)) (f (\<phi> (Suc i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. P (f (\<phi> i)) (f (\<phi> (Suc i)))
[PROOF STEP]
using ** and ***
[PROOF STATE]
proof (prove)
using this:
\<forall>i>n. P (f i) (f (g i))
n < \<phi> ?i

goal (1 subgoal):
 1. \<And>i. P (f (\<phi> i)) (f (\<phi> (Suc i)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P (f (\<phi> ?i)) (f (\<phi> (Suc ?i)))

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?i < ?j \<Longrightarrow> \<phi> ?i < \<phi> ?j
P (f (\<phi> ?i)) (f (\<phi> (Suc ?i)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?i < ?j \<Longrightarrow> \<phi> ?i < \<phi> ?j
P (f (\<phi> ?i)) (f (\<phi> (Suc ?i)))

goal (1 subgoal):
 1. \<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<phi>. (\<forall>i j. i < j \<longrightarrow> \<phi> i < \<phi> j) \<and> (\<forall>i. P (f (\<phi> i)) (f (\<phi> (Suc i))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma steps_imp_chainp':
  assumes "\<forall>i\<ge>n::nat. \<exists>j\<ge>i. P (S i) (S j)" shows "\<exists>T. chainp P T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T. \<forall>i. P (T i) (T (Suc i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>T. \<forall>i. P (T i) (T (Suc i))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<ge>n. \<exists>j\<ge>i. P (S i) (S j)
[PROOF STEP]
have "\<forall>i\<in>{i. i \<ge> n}. \<exists>j\<ge>i. P (S i) (S j)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<ge>n. \<exists>j\<ge>i. P (S i) (S j)

goal (1 subgoal):
 1. \<forall>i\<in>{i. n \<le> i}. \<exists>j\<ge>i. P (S i) (S j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>{i. n \<le> i}. \<exists>j\<ge>i. P (S i) (S j)

goal (1 subgoal):
 1. \<exists>T. \<forall>i. P (T i) (T (Suc i))
[PROOF STEP]
from bchoice [OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x\<in>{i. n \<le> i}. x \<le> f x \<and> P (S x) (S (f x))
[PROOF STEP]
(*choice could be replaced by an application of Least_Enum.infinitely_many2*)
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x\<in>{i. n \<le> i}. x \<le> f x \<and> P (S x) (S (f x))
[PROOF STEP]
obtain f where "\<forall>i\<ge>n. f i \<ge> i \<and> P (S i) (S (f i))"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x\<in>{i. n \<le> i}. x \<le> f x \<and> P (S x) (S (f x))

goal (1 subgoal):
 1. (\<And>f. \<forall>i\<ge>n. i \<le> f i \<and> P (S i) (S (f i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i\<ge>n. i \<le> f i \<and> P (S i) (S (f i))

goal (1 subgoal):
 1. \<exists>T. \<forall>i. P (T i) (T (Suc i))
[PROOF STEP]
from stepfun_imp_chainp'[of n f P S, OF this]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i. P (S ((f ^^ i) n)) (S ((f ^^ Suc i) n))

goal (1 subgoal):
 1. \<exists>T. \<forall>i. P (T i) (T (Suc i))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<exists>T. \<forall>i. P (T i) (T (Suc i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma steps_imp_chainp:
  assumes "\<forall>i\<ge>n::nat. \<exists>j>i. P (S i) (S j)" shows "\<exists>T. chainp P T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T. \<forall>i. P (T i) (T (Suc i))
[PROOF STEP]
using steps_imp_chainp' [of n P S] and assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<ge>n. \<exists>j\<ge>i. P (S i) (S j) \<Longrightarrow> \<exists>T. \<forall>i. P (T i) (T (Suc i))
\<forall>i\<ge>n. \<exists>j>i. P (S i) (S j)

goal (1 subgoal):
 1. \<exists>T. \<forall>i. P (T i) (T (Suc i))
[PROOF STEP]
by force


[STATEMENT]
lemma inf: "\<exists>j\<ge>i. p j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j\<ge>i. p j
[PROOF STEP]
using infinite[unfolded INFM_nat_le]
[PROOF STATE]
proof (prove)
using this:
\<forall>m. \<exists>n\<ge>m. p n

goal (1 subgoal):
 1. \<exists>j\<ge>i. p j
[PROOF STEP]
by auto


[STATEMENT]
lemma index_p: "p (index n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p (index n)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p (index 0)
 2. \<And>n. p (index n) \<Longrightarrow> p (index (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. p (index 0)
 2. \<And>n. p (index n) \<Longrightarrow> p (index (Suc n))
[PROOF STEP]
from inf
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<ge>?i. p j
[PROOF STEP]
obtain j where "p j"
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>?i. p j

goal (1 subgoal):
 1. (\<And>j. p j \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p j

goal (2 subgoals):
 1. p (index 0)
 2. \<And>n. p (index n) \<Longrightarrow> p (index (Suc n))
[PROOF STEP]
with LeastI[of p j]
[PROOF STATE]
proof (chain)
picking this:
p j \<Longrightarrow> p (LEAST x. p x)
p j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p j \<Longrightarrow> p (LEAST x. p x)
p j

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

goal (1 subgoal):
 1. \<And>n. p (index n) \<Longrightarrow> p (index (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. p (index n) \<Longrightarrow> p (index (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
p (index n)

goal (1 subgoal):
 1. \<And>n. p (index n) \<Longrightarrow> p (index (Suc n))
[PROOF STEP]
from inf
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<ge>?i. p j
[PROOF STEP]
obtain k where "k \<ge> Suc (index n) \<and> p k"
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>?i. p j

goal (1 subgoal):
 1. (\<And>k. Suc (index n) \<le> k \<and> p k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (index n) \<le> k \<and> p k

goal (1 subgoal):
 1. \<And>n. p (index n) \<Longrightarrow> p (index (Suc n))
[PROOF STEP]
with LeastI[of "\<lambda> k. p k \<and> k > index n" k]
[PROOF STATE]
proof (chain)
picking this:
p k \<and> index n < k \<Longrightarrow> p (LEAST x. p x \<and> index n < x) \<and> index n < (LEAST x. p x \<and> index n < x)
Suc (index n) \<le> k \<and> p k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p k \<and> index n < k \<Longrightarrow> p (LEAST x. p x \<and> index n < x) \<and> index n < (LEAST x. p x \<and> index n < x)
Suc (index n) \<le> k \<and> p k

goal (1 subgoal):
 1. p (index (Suc n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p (index (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_ordered: "index n < index (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index n < index (Suc n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. index n < index (Suc n)
[PROOF STEP]
from inf
[PROOF STATE]
proof (chain)
picking this:
\<exists>j\<ge>?i. p j
[PROOF STEP]
obtain k where "k \<ge> Suc (index n) \<and> p k"
[PROOF STATE]
proof (prove)
using this:
\<exists>j\<ge>?i. p j

goal (1 subgoal):
 1. (\<And>k. Suc (index n) \<le> k \<and> p k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (index n) \<le> k \<and> p k

goal (1 subgoal):
 1. index n < index (Suc n)
[PROOF STEP]
with LeastI[of "\<lambda> k. p k \<and> k > index n" k]
[PROOF STATE]
proof (chain)
picking this:
p k \<and> index n < k \<Longrightarrow> p (LEAST x. p x \<and> index n < x) \<and> index n < (LEAST x. p x \<and> index n < x)
Suc (index n) \<le> k \<and> p k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p k \<and> index n < k \<Longrightarrow> p (LEAST x. p x \<and> index n < x) \<and> index n < (LEAST x. p x \<and> index n < x)
Suc (index n) \<le> k \<and> p k

goal (1 subgoal):
 1. index n < index (Suc n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index n < index (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_not_p_between:
  assumes i1: "index n < i"
    and i2: "i < index (Suc n)"
  shows "\<not> p i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> p i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> p i
[PROOF STEP]
from not_less_Least[OF i2[simplified]] i1
[PROOF STATE]
proof (chain)
picking this:
\<not> (p i \<and> index n < i)
index n < i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (p i \<and> index n < i)
index n < i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_ordered_le:
  assumes "i \<le> j" shows "index i \<le> index j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index i \<le> index j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. index i \<le> index j
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i \<le> j
[PROOF STEP]
have "j = i + (j - i)"
[PROOF STATE]
proof (prove)
using this:
i \<le> j

goal (1 subgoal):
 1. j = i + (j - i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j = i + (j - i)

goal (1 subgoal):
 1. index i \<le> index j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j = i + (j - i)
[PROOF STEP]
obtain k where j: "j = i + k"
[PROOF STATE]
proof (prove)
using this:
j = i + (j - i)

goal (1 subgoal):
 1. (\<And>k. j = i + k \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j = i + k

goal (1 subgoal):
 1. index i \<le> index j
[PROOF STEP]
have "index i \<le> index (i + k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index i \<le> index (i + k)
[PROOF STEP]
proof (induct k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. index i \<le> index (i + 0)
 2. \<And>k. index i \<le> index (i + k) \<Longrightarrow> index i \<le> index (i + Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
index i \<le> index (i + k)

goal (2 subgoals):
 1. index i \<le> index (i + 0)
 2. \<And>k. index i \<le> index (i + k) \<Longrightarrow> index i \<le> index (i + Suc k)
[PROOF STEP]
with index_ordered[of "i + k"]
[PROOF STATE]
proof (chain)
picking this:
index (i + k) < index (Suc (i + k))
index i \<le> index (i + k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
index (i + k) < index (Suc (i + k))
index i \<le> index (i + k)

goal (1 subgoal):
 1. index i \<le> index (i + Suc k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index i \<le> index (i + Suc k)

goal (1 subgoal):
 1. index i \<le> index (i + 0)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
index i \<le> index (i + k)

goal (1 subgoal):
 1. index i \<le> index j
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
index i \<le> index (i + k)

goal (1 subgoal):
 1. index i \<le> index j
[PROOF STEP]
unfolding j
[PROOF STATE]
proof (prove)
using this:
index i \<le> index (i + k)

goal (1 subgoal):
 1. index i \<le> index (i + k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
index i \<le> index j

goal:
No subgoals!
[PROOF STEP]
qed