diff --git a/thys/Irrational_Series_Erdos_Straus/Irrational_Series_Erdos_Straus.thy b/thys/Irrational_Series_Erdos_Straus/Irrational_Series_Erdos_Straus.thy
--- a/thys/Irrational_Series_Erdos_Straus/Irrational_Series_Erdos_Straus.thy
+++ b/thys/Irrational_Series_Erdos_Straus/Irrational_Series_Erdos_Straus.thy
@@ -1,2008 +1,2003 @@
 (* Title:      Irrational_Series_Erdos_Straus.thy
    Author:     Angeliki Koutsoukou-Argyraki and Wenda Li, University of Cambridge, UK.
 
 We formalise certain irrationality criteria for infinite series by P. Erdos and E.G. Straus.
 In particular, we formalise Theorem 2.1, Corollary 2.10 and Theorem 3.1 in [1]. The latter is an 
 application of Theorem 2.1 involving the prime numbers.
 
 References:
 [1]  P. Erdos and E.G. Straus, On the irrationality of certain series, Pacific Journal of 
 Mathematics, Vol. 55, No 1, 1974  https://projecteuclid.org/euclid.pjm/1102911140
 *)
 
 theory "Irrational_Series_Erdos_Straus" imports
   Prime_Number_Theorem.Prime_Number_Theorem
   Prime_Distribution_Elementary.PNT_Consequences
 begin
 
 section \<open>Miscellaneous\<close>
 
 lemma suminf_comparison:
   assumes "summable f" and gf: "\<And>n. norm (g n) \<le> f n"
   shows "suminf g \<le> suminf f"
 proof (rule suminf_le)
   show "g n \<le> f n" for n
     using gf[of n] by auto
   show "summable g"
     using assms summable_comparison_test' by blast 
   show "summable f" using assms(1) .
 qed
 
 lemma tendsto_of_int_diff_0:
   assumes "(\<lambda>n. f n - of_int(g n)) \<longlonglongrightarrow> (0::real)" "\<forall>\<^sub>F n in sequentially. f n > 0"
   shows "\<forall>\<^sub>F n in sequentially. 0 \<le> g n"
 proof -
   have "\<forall>\<^sub>F n in sequentially. \<bar>f n - of_int(g n)\<bar> < 1 / 2" 
     using assms(1)[unfolded tendsto_iff,rule_format,of "1/2"] by auto
   then show ?thesis using assms(2)
     apply eventually_elim
     by linarith
 qed
 
 lemma eventually_mono_sequentially:
   assumes "eventually P sequentially"
   assumes "\<And>x. P (x+k) \<Longrightarrow> Q (x+k)"
   shows "eventually Q sequentially"
   using sequentially_offset[OF assms(1),of k]
   apply (subst eventually_sequentially_seg[symmetric,of _ k])
   apply (elim eventually_mono)
   by fact
 
 lemma frequently_eventually_at_top:
   fixes P Q::"'a::linorder \<Rightarrow> bool"
   assumes "frequently P at_top" "eventually Q at_top"
   shows "frequently (\<lambda>x. P x \<and> (\<forall>y\<ge>x. Q y) ) at_top"
   using assms
   unfolding frequently_def eventually_at_top_linorder 
   by (metis (mono_tags, hide_lams) le_cases order_trans)
 
 lemma eventually_at_top_mono:
   fixes P Q::"'a::linorder \<Rightarrow> bool"
   assumes event_P:"eventually P at_top"
   assumes PQ_imp:"\<And>x. x\<ge>z \<Longrightarrow> \<forall>y\<ge>x. P y \<Longrightarrow> Q x"
   shows "eventually Q at_top"
 proof -
   obtain N where N_P:"\<forall>n\<ge>N. P n"
     using event_P[unfolded eventually_at_top_linorder] by auto
   define N' where "N' = max N z"
   have "Q x" when "x\<ge>N'" for x 
     apply (rule PQ_imp)
     using N_P that unfolding N'_def by auto
   then show ?thesis unfolding eventually_at_top_linorder
     by auto
 qed
 
 lemma frequently_at_top_elim:
   fixes P Q::"'a::linorder \<Rightarrow> bool"
   assumes "\<exists>\<^sub>Fx in at_top. P x"
   assumes "\<And>i. P i \<Longrightarrow> \<exists>j>i. Q j"
   shows "\<exists>\<^sub>Fx in at_top. Q x"
   using assms unfolding frequently_def eventually_at_top_linorder 
   by (meson leD le_cases less_le_trans)
 
 lemma less_Liminf_iff:
   fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
   shows "Liminf F X < C \<longleftrightarrow> (\<exists>y<C. frequently (\<lambda>x. y \<ge> X x) F)"
   apply (subst Not_eq_iff[symmetric])
   apply (simp add:not_less not_frequently not_le le_Liminf_iff)
   by force
 
 lemma sequentially_even_odd_imp:
   assumes "\<forall>\<^sub>F N in sequentially. P (2*N)" "\<forall>\<^sub>F N in sequentially. P (2*N+1)"
   shows "\<forall>\<^sub>F n in sequentially. P n"
 proof -
   obtain N where N_P:"\<forall>x\<ge>N.  P (2 * x) \<and> P (2 * x + 1)"
     using eventually_conj[OF assms] 
     unfolding eventually_at_top_linorder by auto
   define N' where "N'=2*N "
   have "P n" when "n\<ge>2*N" for n
   proof -
     define n' where "n'= n div 2"
     then have "n'\<ge>N" using that by auto
     then have "P (2 * n') \<and> P (2 * n' + 1)"
       using N_P by auto
     then show ?thesis unfolding n'_def
       apply (cases "even n")
       by auto
   qed
   then show ?thesis unfolding eventually_at_top_linorder by auto
 qed
 
 
 section \<open>Theorem 2.1 and Corollary 2.10\<close>
 
 context
   fixes a b ::"nat\<Rightarrow>int "
   assumes a_pos:"\<forall> n. a n >0 " and a_large:"\<forall>\<^sub>F n in sequentially. a n > 1" 
     and ab_tendsto: "(\<lambda>n. \<bar>b n\<bar> / (a (n-1)*a n)) \<longlonglongrightarrow> 0"
 begin
 
 private lemma aux_series_summable: "summable (\<lambda>n. b n / (\<Prod>k\<le>n. a k))" 
 proof -
   have "\<forall>e>0. \<forall>\<^sub>F x in sequentially. \<bar>b x\<bar> / (a (x-1) * a x) < e"
     using ab_tendsto[unfolded tendsto_iff] 
     apply (simp add:of_int_abs[symmetric] abs_mult del:of_int_abs)
     by (subst (asm) (2) abs_of_pos,use \<open>\<forall> n. a n > 0\<close> in auto)+                 
   from this[rule_format,of 1]
   have "\<forall>\<^sub>F x in sequentially. \<bar>real_of_int(b x)\<bar> < (a (x-1) * a x)"
     using \<open>\<forall> n. a n >0\<close> by auto
   moreover have "\<forall>n. (\<Prod>k\<le>n. real_of_int (a k)) > 0" 
     using a_pos by (auto intro!:linordered_semidom_class.prod_pos)
   ultimately have "\<forall>\<^sub>F n in sequentially. \<bar>b n\<bar> / (\<Prod>k\<le>n. a k) 
                         < (a (n-1) * a n) / (\<Prod>k\<le>n. a k)"
     apply (elim eventually_mono)
     by (auto simp add:field_simps)
   moreover have "\<bar>b n\<bar> / (\<Prod>k\<le>n. a k) = norm (b n / (\<Prod>k\<le>n. a k))" for n 
     using \<open>\<forall>n. (\<Prod>k\<le>n. real_of_int (a k)) > 0\<close>[rule_format,of n] by auto
   ultimately have "\<forall>\<^sub>F n in sequentially. norm (b n / (\<Prod>k\<le>n. a k)) 
                         < (a (n-1) * a n) / (\<Prod>k\<le>n. a k)"
     by algebra
   moreover have "summable (\<lambda>n. (a (n-1) * a n) / (\<Prod>k\<le>n. a k))" 
   proof -
     obtain s where a_gt_1:"\<forall> n\<ge>s. a n >1"
       using a_large[unfolded eventually_at_top_linorder] by auto
     define cc where "cc= (\<Prod>k<s. a k)"
     have "cc>0" 
       unfolding cc_def
       apply (rule linordered_semidom_class.prod_pos)
       using a_pos by auto
     have "(\<Prod>k\<le>n+s. a k) \<ge> cc * 2^n" for n
     proof -
       have "prod a {s..<Suc (s + n)} \<ge> 2^n"
       proof (induct n)
         case 0
         then show ?case using a_gt_1 by auto
       next
         case (Suc n)
         moreover have "a (s + Suc n) \<ge> 2" 
           using a_gt_1 by (smt le_add1)
         ultimately show ?case 
           apply (subst prod.atLeastLessThan_Suc,simp)
           using mult_mono'[of 2 "a (Suc (s + n))" " 2 ^ n" "prod a {s..<Suc (s + n)}",simplified] 
           by (simp add: mult.commute)
       qed
       moreover have "prod a {0..(n + s)} =
             prod a {..<s} * prod a {s..<Suc (s + n)} "
         using prod.atLeastLessThan_concat[of 0 s "s+n+1" a,simplified]
         apply (simp add: atLeastLessThanSuc_atLeastAtMost algebra_simps
             atLeast0LessThan)
         by (smt a_gt_1 le_add2 lessThan_atLeast0 mult.left_commute prod.last_plus zero_le)
       ultimately show ?thesis
         using \<open>cc>0\<close> unfolding cc_def by (simp add: atLeast0AtMost)
     qed
     then have "1/(\<Prod>k\<le>n+s. a k) \<le> 1/(cc * 2^n)" for n
     proof -
       assume asm:"\<And>n. cc * 2 ^ n \<le> prod a {..n + s}"
       then have "real_of_int (cc * 2 ^ n) \<le> prod a {..n + s}" using of_int_le_iff by blast
       moreover have "prod a {..n + s} >0" using \<open>cc>0\<close> by (simp add: a_pos prod_pos)
       ultimately show ?thesis using \<open>cc>0\<close> 
         by (auto simp:field_simps simp del:of_int_prod)
     qed
     moreover have "summable (\<lambda>n. 1/(cc * 2^n))"
     proof -
       have "summable (\<lambda>n. 1/(2::int)^n)"
         using summable_geometric[of "1/(2::int)"] by (simp add:power_one_over)
       from summable_mult[OF this,of "1/cc"] show ?thesis by auto
     qed
     ultimately have "summable (\<lambda>n. 1 / (\<Prod>k\<le>n+s. a k))"
       apply (elim summable_comparison_test'[where N=0])
       apply (unfold real_norm_def, subst abs_of_pos)
       by (auto simp add: \<open>\<forall>n. 0 < (\<Prod>k\<le>n. real_of_int (a k))\<close>)
     then have "summable (\<lambda>n. 1 / (\<Prod>k\<le>n. a k))"
       apply (subst summable_iff_shift[where k=s,symmetric])
       by simp
     then have "summable (\<lambda>n. (a (n+1) * a (n+2)) / (\<Prod>k\<le>n+2. a k))"
     proof -
       assume asm:"summable (\<lambda>n. 1 / real_of_int (prod a {..n}))"
       have "1 / real_of_int (prod a {..n}) = (a (n+1) * a (n+2)) / (\<Prod>k\<le>n+2. a k)" for n 
       proof -
         have "a (Suc (Suc n)) \<noteq> 0" "a (Suc n) \<noteq>0" 
           using a_pos by (metis less_irrefl)+
         then show ?thesis 
           by (simp add: atLeast0_atMost_Suc atMost_atLeast0)
       qed
       then show ?thesis using asm by auto
     qed
     then show "summable (\<lambda>n. (a (n-1) * a n) / (\<Prod>k\<le>n. a k))"
       apply (subst summable_iff_shift[symmetric,of _ 2])
       by auto
   qed
   ultimately show ?thesis 
     apply (elim summable_comparison_test_ev[rotated])
     by (simp add: eventually_mono)
 qed
 
 private fun get_c::"(nat \<Rightarrow> int) \<Rightarrow> (nat \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> int)" where
   "get_c a' b' B N 0 = round (B * b' N / a' N)"|
   "get_c a' b' B N (Suc n) = get_c a' b' B N n * a' (n+N) - B * b' (n+N)"
 
 lemma ab_rationality_imp:
   assumes ab_rational:"(\<Sum>n. (b n / (\<Prod>i \<le> n. a i))) \<in> \<rat>"
   shows "\<exists> (B::int)>0. \<exists> c::nat\<Rightarrow> int.
             (\<forall>\<^sub>F n in sequentially. B*b n = c n * a n - c(n+1) \<and> \<bar>c(n+1)\<bar><a n/2)
             \<and> (\<lambda>n. c (Suc n) / a n) \<longlonglongrightarrow> 0"
 proof -
   have [simp]:"a n \<noteq> 0" for n using a_pos by (metis less_numeral_extra(3))
   obtain A::int and B::int where 
     AB_eq:"(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = A / B" and "B>0"
   proof -
     obtain q::rat where "(\<Sum>n. real_of_int (b n) / real_of_int (prod a {..n})) = real_of_rat q"
       using ab_rational by (rule Rats_cases) simp
     moreover obtain A::int and B::int where "q = Rat.Fract A B" "B > 0" "coprime A B"
       by (rule Rat_cases) auto
     ultimately show ?thesis by (auto intro!: that[of A B] simp:of_rat_rat)
   qed  
   define f where "f = (\<lambda>n.  b n / real_of_int (prod a {..n}))"
   define R where "R = (\<lambda>N. (\<Sum>n. B*b (n+N+1) / prod a {N..n+N+1}))"
   have all_e_ubound:"\<forall>e>0. \<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>B*b (n+M+1) / prod a {M..n+M+1}\<bar> < e/4 * 1/2^n"
   proof safe
     fix e::real assume "e>0"
     obtain N where N_a2: "\<forall>n \<ge> N. a n \<ge> 2" 
       and N_ba: "\<forall>n \<ge> N. \<bar>b n\<bar> / (a (n-1) * a n)  < e/(4*B)"
     proof -
       have "\<forall>\<^sub>F n in sequentially. \<bar>b n\<bar> / (a (n - 1) * a n) < e/(4*B)" 
         using order_topology_class.order_tendstoD[OF ab_tendsto,of "e/(4*B)"] \<open>B>0\<close> \<open>e>0\<close>
         by auto
       moreover have "\<forall>\<^sub>F n in sequentially. a n \<ge> 2"
         using a_large by (auto elim: eventually_mono)
       ultimately have "\<forall>\<^sub>F n in sequentially. \<bar>b n\<bar> / (a (n - 1) * a n) < e/(4*B) \<and> a n \<ge> 2" 
         by eventually_elim auto
       then show ?thesis unfolding eventually_at_top_linorder using that
         by auto
     qed
     have geq_N_bound:"\<bar>B*b (n+M+1) / prod a {M..n+M+1}\<bar> < e/4 * 1/2^n" when "M\<ge>N" for n M   
     proof -
       define D where "D = B*b (n+M+1)/ (a (n+M) * a (n+M+1))"
       have "\<bar>B*b (n+M+1) / prod a {M..n+M+1}\<bar> = \<bar>D / prod a {M..<n+M}\<bar>"
       proof -
         have "{M..n+M+1} = {M..<n+M} \<union> {n+M,n+M+1}" by auto
         then have "prod a {M..n+M+1} = a (n+M) * a (n+M+1)* prod a {M..<n+M}" by simp
         then show ?thesis unfolding D_def by (simp add:algebra_simps)
       qed
       also have "... <  \<bar>e/4 * (1/prod a {M..<n+M})\<bar>"
       proof -
         have "\<bar>D\<bar> < e/ 4" 
           unfolding D_def using N_ba[rule_format, of "n+M+1"] \<open>B>0\<close> \<open>M \<ge> N\<close> \<open>e>0\<close> a_pos
           by (auto simp:field_simps abs_mult abs_of_pos)
         from mult_strict_right_mono[OF this,of "1/prod a {M..<n+M}"] a_pos \<open>e>0\<close>
         show ?thesis 
           apply (auto simp:abs_prod abs_mult prod_pos)
           by (subst (2) abs_of_pos,auto)+
       qed
       also have "... \<le> e/4 * 1/2^n"
       proof -
         have "prod a {M..<n+M} \<ge> 2^n"
         proof (induct n)
           case 0
           then show ?case by simp
         next
           case (Suc n)
           then show ?case 
             using \<open>M\<ge>N\<close> by (simp add: N_a2 mult.commute mult_mono' prod.atLeastLessThan_Suc)
         qed
         then have "real_of_int (prod a {M..<n+M}) \<ge> 2^n" 
           using numeral_power_le_of_int_cancel_iff by blast
         then show ?thesis using \<open>e>0\<close> by (auto simp add:divide_simps)
       qed
       finally show ?thesis .
     qed
     show "\<forall>\<^sub>F M in sequentially. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) 
                 / real_of_int (prod a {M..n + M + 1})\<bar> < e / 4 * 1 / 2 ^ n"
       apply (rule eventually_sequentiallyI[of N])
       using geq_N_bound by blast
   qed
   have R_tendsto_0:"R \<longlonglongrightarrow> 0"
   proof (rule tendstoI)
     fix e::real assume "e>0"
     show "\<forall>\<^sub>F x in sequentially. dist (R x) 0 < e" using all_e_ubound[rule_format,OF \<open>e>0\<close>]
     proof eventually_elim
       case (elim M)
       define g where "g = (\<lambda>n. B*b (n+M+1) / prod a {M..n+M+1})"
       have g_lt:"\<bar>g n\<bar> < e/4 * 1/2^n" for n
         using elim unfolding g_def by auto
-      have g_abs_summable:"summable (\<lambda>n. \<bar>g n\<bar>)"
-      proof -
-        have "summable (\<lambda>n. e/4 * 1/2^n)" 
-          using summable_geometric[of "1/2",THEN summable_mult,of "e/4",simplified]
-          by (auto simp add:algebra_simps power_divide)
-        then show ?thesis 
-          apply (elim summable_comparison_test')
-          using g_lt less_eq_real_def by auto
-      qed
+      have \<section>: "summable (\<lambda>n. (e/4) * (1/2)^n)"
+        by simp 
+      then have g_abs_summable:"summable (\<lambda>n. \<bar>g n\<bar>)"
+        apply (elim summable_comparison_test')
+        by (metis abs_idempotent g_lt less_eq_real_def power_one_over real_norm_def times_divide_eq_right)
       have "\<bar>\<Sum>n. g n\<bar> \<le> (\<Sum>n. \<bar>g n\<bar>)" by (rule summable_rabs[OF g_abs_summable])
       also have "... \<le>(\<Sum>n. e/4 * 1/2^n)"
       proof (rule suminf_comparison)
         show "summable (\<lambda>n. e/4 * 1/2^n)" 
-          using summable_geometric[of "1/2",THEN summable_mult,of "e/4",simplified]
-          by (auto simp add:algebra_simps power_divide)
+          using \<section> unfolding power_divide by simp
         show "\<And>n. norm \<bar>g n\<bar> \<le> e / 4 * 1 / 2 ^ n" using g_lt less_eq_real_def by auto
       qed
       also have "... = (e/4) * (\<Sum>n. (1/2)^n)"
         apply (subst suminf_mult[symmetric])
         subgoal 
           apply (rule complete_algebra_summable_geometric)
           by simp
         subgoal by (auto simp:algebra_simps power_divide)
         done
       also have "... = e/2" by (simp add:suminf_geometric[of "1/2"])
       finally have "\<bar>\<Sum>n. g n\<bar> \<le> e / 2" .
       then show "dist (R M) 0 < e" unfolding R_def g_def using \<open>e>0\<close> by auto
     qed
   qed
 
   obtain N where R_N_bound:"\<forall>M \<ge> N. \<bar>R M\<bar> \<le>  1 / 4"
     and N_geometric:"\<forall>M\<ge>N. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) / (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n"
   proof -
     obtain N1 where N1:"\<forall>M \<ge> N1. \<bar>R M\<bar> \<le>  1 / 4"
       using metric_LIMSEQ_D[OF R_tendsto_0,of "1/4"] all_e_ubound[rule_format,of 4,unfolded eventually_sequentially]
       by (auto simp:less_eq_real_def)
     obtain N2 where N2:"\<forall>M\<ge>N2. \<forall>n. \<bar>real_of_int (B * b (n + M + 1)) 
                           / (prod a {M..n + M + 1})\<bar> < 1 / 2 ^ n"
       using all_e_ubound[rule_format,of 4,unfolded eventually_sequentially]
       by (auto simp:less_eq_real_def)
     define N where "N=max N1 N2"
     show ?thesis using that[of N] N1 N2 unfolding N_def by simp
   qed
 
   define C where "C = B * prod a {..<N} * (\<Sum>n<N. f n)"
   have "summable f"
     unfolding f_def using aux_series_summable .
   have "A * prod a {..<N} = C + B * b N / a N  + R N" 
   proof -
     have "A * prod a {..<N} = B * prod a {..<N} * (\<Sum>n. f n)"
       unfolding AB_eq f_def using \<open>B>0\<close> by auto
     also have "... = B * prod a {..<N} * ((\<Sum>n<N+1. f n) + (\<Sum>n. f (n+N+1)))"
       using suminf_split_initial_segment[OF \<open>summable f\<close>, of "N+1"] by auto
     also have "... = B * prod a {..<N} * ((\<Sum>n<N. f n) + f N + (\<Sum>n. f (n+N+1)))"
       using sum.atLeast0_lessThan_Suc by simp
     also have "... = C + B * b N / a N + (\<Sum>n. B*b (n+N+1) / prod a {N..n+N+1})"
     proof -
       have "B * prod a {..<N} * f N = B * b N / a N" 
       proof -
         have "{..N} =  {..<N} \<union> {N}" using ivl_disj_un_singleton(2) by blast
         then show ?thesis unfolding f_def by auto
       qed
       moreover have "B * prod a {..<N} * (\<Sum>n. f (n+N+1)) = (\<Sum>n. B*b (n+N+1) / prod a {N..n+N+1})"
       proof -
         have "summable (\<lambda>n. f (n + N + 1))" 
           using \<open>summable f\<close> summable_iff_shift[of f "N+1"] by auto
         moreover have "prod a {..<N} * f (n + N + 1) = b (n + N + 1) / prod a {N..n + N + 1}" for n
         proof -
           have "{..n + N + 1} = {..<N} \<union> {N..n + N + 1}" by auto
           then show ?thesis 
             unfolding f_def
             apply simp
             apply (subst prod.union_disjoint)
             by auto
         qed
         ultimately show ?thesis 
           apply (subst suminf_mult[symmetric])
           by (auto simp add: mult.commute mult.left_commute)
       qed
       ultimately show ?thesis unfolding C_def by (auto simp:algebra_simps)
     qed
     also have "... = C +B * b N / a N  + R N"
       unfolding R_def by simp
     finally show ?thesis .
   qed
   have R_bound:"\<bar>R M\<bar> \<le> 1 / 4" and R_Suc:"R (Suc M) = a M * R M - B * b (Suc M) / a (Suc M)" 
     when "M \<ge> N" for M
   proof -
     define g where "g = (\<lambda>n. B*b (n+M+1) / prod a {M..n+M+1})"
     have g_abs_summable:"summable (\<lambda>n. \<bar>g n\<bar>)"
     proof -
       have "summable (\<lambda>n. (1/2::real) ^ n)" 
         by simp
       moreover have "\<bar>g n\<bar> < 1/2^n" for n
         using N_geometric[rule_format,OF that] unfolding g_def by simp
       ultimately show ?thesis 
         apply (elim summable_comparison_test')
         by (simp add: less_eq_real_def power_one_over)
     qed
     show "\<bar>R M\<bar> \<le> 1 / 4" using R_N_bound[rule_format,OF that] .
     have "R M = (\<Sum>n. g n)" unfolding R_def g_def by simp
     also have "... = g 0 + (\<Sum>n. g (Suc n))"
       apply (subst suminf_split_head)
       using summable_rabs_cancel[OF g_abs_summable] by auto
     also have "... = g 0 + 1/a M * (\<Sum>n. a M * g (Suc n))"
       apply (subst suminf_mult)
       by (auto simp add: g_abs_summable summable_Suc_iff summable_rabs_cancel)
     also have "... = g 0 + 1/a M * R (Suc M)"
     proof -
       have "a M * g (Suc n) = B * b (n + M + 2) / prod a {Suc M..n + M + 2}" for n
       proof -
         have "{M..Suc (Suc (M + n))} = {M} \<union> {Suc M..Suc (Suc (M + n))}" by auto
         then show ?thesis 
           unfolding g_def using \<open>B>0\<close> by (auto simp add:algebra_simps)
       qed
       then have "(\<Sum>n. a M * g (Suc n)) = R (Suc M)"
         unfolding R_def by auto
       then show ?thesis by auto
     qed
     finally have "R M = g 0 + 1 / a M * R (Suc M)" .
     then have "R (Suc M) = a M * R M - g 0 * a M" 
       by (auto simp add:algebra_simps)
     moreover have "{M..Suc M} = {M,Suc M}" by auto
     ultimately show "R (Suc M) = a M * R M - B * b (Suc M) / a (Suc M)" 
       unfolding g_def by auto
   qed
 
   define c where "c = (\<lambda>n. if n\<ge>N then get_c a b B N (n-N) else undefined)"
   have c_rec:"c (n+1) = c n * a n -  B * b n" when "n \<ge> N" for n
     unfolding c_def using that by (auto simp:Suc_diff_le)
   have c_R:"c (Suc n) / a n = R n" when "n \<ge> N" for n
     using that
   proof (induct rule:nat_induct_at_least)
     case base
     have "\<bar> c (N+1) / a N \<bar> \<le> 1/2" 
     proof -
       have "c N = round (B * b N / a N)" unfolding c_def by simp
       moreover have "c (N+1) / a N = c N - B * b N / a N"
         using a_pos[rule_format,of N]
         by (auto simp add:c_rec[of N,simplified] divide_simps)
       ultimately show ?thesis using of_int_round_abs_le by auto
     qed        
     moreover have "\<bar>R N\<bar> \<le> 1 / 4" using R_bound[of N] by simp
     ultimately have "\<bar>c (N+1) / a N - R N \<bar> < 1" by linarith
     moreover have "c (N+1) / a N - R N \<in> \<int>"
     proof -
       have "c (N+1) / a N = c N - B * b N / a N"
         using a_pos[rule_format,of N]
         by (auto simp add:c_rec[of N,simplified] divide_simps)
       moreover have " B * b N / a N + R N \<in> \<int>" 
       proof -
         have "C = B * (\<Sum>n<N. prod a {..<N} * (b n / prod a {..n}))"
           unfolding C_def f_def by (simp add:sum_distrib_left algebra_simps)
         also have "... = B * (\<Sum>n<N. prod a {n<..<N} * b n)"
         proof -
           have "{..<N} = {n<..<N} \<union> {..n}" if "n<N" for n 
             by (simp add: ivl_disj_un_one(1) sup_commute that)
           then show ?thesis
             using \<open>B>0\<close> 
             apply simp
             apply (subst prod.union_disjoint)
             by auto
         qed
         finally have "C = real_of_int (B * (\<Sum>n<N. prod a {n<..<N} * b n))" .
         then have "C \<in> \<int>" using Ints_of_int by blast
         moreover note \<open>A * prod a {..<N} = C + B * b N / a N  + R N\<close>
         ultimately show ?thesis 
           by (metis Ints_diff Ints_of_int add.assoc add_diff_cancel_left')
       qed
       ultimately show ?thesis by (simp add: diff_diff_add)
     qed
     ultimately have "c (N+1) / a N - R N = 0"
       by (metis Ints_cases less_irrefl of_int_0 of_int_lessD)
     then show ?case by simp
   next
     case (Suc n)
     have "c (Suc (Suc n)) / a (Suc n) = c (Suc n) - B * b (Suc n) / a (Suc n)"
       apply (subst c_rec[of "Suc n",simplified])
       using \<open>N \<le> n\<close> by (auto simp add: divide_simps)
     also have "... = a n * R n - B * b (Suc n) / a (Suc n)"  
       using Suc by (auto simp: divide_simps)
     also have "... = R (Suc n)"
       using R_Suc[OF \<open>N \<le> n\<close>] by simp
     finally  show ?case .
   qed
   have ca_tendsto_zero:"(\<lambda>n. c (Suc n) / a n) \<longlonglongrightarrow> 0"
     using R_tendsto_0 
     apply (elim filterlim_mono_eventually)
     using c_R by (auto intro!:eventually_sequentiallyI[of N])
   have ca_bound:"\<bar>c (n + 1)\<bar> < a n / 2" when "n \<ge> N" for n
   proof -
     have "\<bar>c (Suc n)\<bar> / a n  = \<bar>c (Suc n) / a n\<bar>" using a_pos[rule_format,of n] by auto
     also have "... = \<bar>R n\<bar>" using c_R[OF that] by auto
     also have "... < 1/2" using R_bound[OF that] by auto
     finally have "\<bar>c (Suc n)\<bar> / a n < 1/2" .
     then show ?thesis using a_pos[rule_format,of n] by auto
   qed
 
 (* (* the following part corresponds to (2.7) (2.8) in the original paper, but turns out to be
         not necessary. *)
   have c_round:"c n = round (B * b n / a n)" when "n \<ge> N" for n
   proof (cases "n=N")
     case True
     then show ?thesis unfolding c_def by simp
   next
     case False
     with \<open>n\<ge>N\<close> obtain n' where n_Suc:"n=Suc n'" and "n' \<ge> N" 
       by (metis le_eq_less_or_eq lessE less_imp_le_nat)
     have "B * b n / a n = c n - R n"
     proof -
       have "R n = c n - B * b n / a n"
         using c_R[OF \<open>n'\<ge>N\<close>,symmetric,folded n_Suc] R_Suc[OF \<open>n'\<ge>N\<close>,folded n_Suc]
         by (auto simp:field_simps)
       then show ?thesis by (auto simp:field_simps)
     qed
     then have "\<bar>B * b n / a n - c n\<bar> = \<bar>R n\<bar>" by auto
     then have "\<bar>B * b n / a n - c n\<bar> < 1/2" using R_bound[OF \<open>n \<ge> N\<close>] by auto
     from round_unique'[OF this] show ?thesis by auto
   qed
   *)
   show "\<exists>B>0. \<exists>c. (\<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) 
             \<and> real_of_int \<bar>c (n + 1)\<bar> < a n / 2) \<and> (\<lambda>n. c (Suc n) / a n) \<longlonglongrightarrow> 0"
     unfolding eventually_at_top_linorder
     apply (rule exI[of _ B],use \<open>B>0\<close> in simp)
     apply (intro exI[of _c] exI[of _ N])
     using c_rec ca_bound ca_tendsto_zero 
     by fastforce
 qed
 
 private lemma imp_ab_rational:
   assumes "\<exists> (B::int)>0. \<exists> c::nat\<Rightarrow> int.
               (\<forall>\<^sub>F n in sequentially. B*b n = c n * a n - c(n+1) \<and> \<bar>c(n+1)\<bar><a n/2)"
   shows "(\<Sum>n. (b n / (\<Prod>i \<le> n. a i))) \<in> \<rat>"
 proof -
   obtain B::int and c::"nat\<Rightarrow>int" and N::nat where "B>0" and  
     large_n:"\<forall>n\<ge>N. B * b n = c n * a n - c (n + 1) \<and> real_of_int \<bar>c (n + 1)\<bar> < a n / 2
                       \<and> a n\<ge>2"
   proof -
     obtain B c where "B>0" and event1:"\<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) 
               \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2"
       using assms by auto
     from eventually_conj[OF event1 a_large,unfolded eventually_at_top_linorder]
     obtain N where "\<forall>n\<ge>N. (B * b n = c n * a n - c (n + 1) 
                         \<and> real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and> 2 \<le> a n"
       by fastforce
     then show ?thesis using that[of B N c] \<open>B>0\<close> by auto
   qed
   define f where "f=(\<lambda>n. real_of_int (b n) / real_of_int (prod a {..n}))"
   define S where "S = (\<Sum>n. f n)"
   have "summable f"
     unfolding f_def by (rule aux_series_summable)
   define C where "C=B*prod a {..<N} * (\<Sum>n<N. f n)"
   have "B*prod a {..<N} * S = C + real_of_int (c N)" 
   proof -
     define h1 where "h1= (\<lambda>n. (c (n+N) * a (n+N)) / prod a {N..n+N})"
     define h2 where "h2 = (\<lambda>n. c (n+N+1) / prod a {N..n+N})"
     have f_h12:"B*prod a {..<N}*f (n+N) = h1 n - h2 n" for n 
     proof -
       define g1 where "g1 = (\<lambda>n. B * b (n+N))"
       define g2 where "g2 = (\<lambda>n. prod a {..<N} / prod a {..n + N})"
       have "B*prod a {..<N}*f (n+N) = (g1 n * g2 n)"
         unfolding f_def g1_def g2_def by (auto simp:algebra_simps)
       moreover have "g1 n = c (n+N) * a (n+N) - c (n+N+1)" 
         using large_n[rule_format,of "n+N"] unfolding g1_def by auto
       moreover have "g2 n = (1/prod a {N..n+N})" 
       proof -
         have "prod a ({..<N} \<union> {N..n + N}) = prod a {..<N} * prod a {N..n + N}"
           apply (rule prod.union_disjoint[of "{..<N}" "{N..n+N}" a])
           by auto
         moreover have "prod a ({..<N} \<union> {N..n + N}) = prod a {..n+N}"
           by (simp add: ivl_disj_un_one(4))
         ultimately show ?thesis 
           unfolding g2_def
           apply simp
           using a_pos by (metis less_irrefl)
       qed
       ultimately have "B*prod a {..<N}*f (n+N) = (c (n+N) * a (n+N) - c (n+N+1)) / prod a {N..n+N}"
         by auto
       also have "... = h1 n - h2 n"
         unfolding h1_def h2_def by (auto simp:algebra_simps diff_divide_distrib)
       finally show ?thesis by simp
     qed
     have "B*prod a {..<N} * S = B*prod a {..<N} * ((\<Sum>n<N. f n) + (\<Sum>n. f (n+N)))"
       using suminf_split_initial_segment[OF \<open>summable f\<close>,of N] 
       unfolding S_def by (auto simp:algebra_simps)
     also have "... = C + B*prod a {..<N}*(\<Sum>n. f (n+N))"
       unfolding C_def by (auto simp:algebra_simps)
     also have "... = C + (\<Sum>n. h1 n - h2 n)"
       apply (subst suminf_mult[symmetric])
       subgoal using \<open>summable f\<close> by (simp add: summable_iff_shift)
       subgoal using f_h12 by auto
       done
     also have "... = C + h1 0"
     proof -
       have "(\<lambda>n. \<Sum>i\<le>n. h1 i - h2 i) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)"
       proof (rule summable_LIMSEQ')
         have "(\<lambda>i. h1 i - h2 i) = (\<lambda>i.  real_of_int (B * prod a {..<N}) * f (i + N))"
           using f_h12 by auto
         then show "summable (\<lambda>i. h1 i - h2 i)"
           using \<open>summable f\<close> by (simp add: summable_iff_shift summable_mult)
       qed
       moreover have "(\<Sum>i\<le>n. h1 i - h2 i)  = h1 0 - h2 n" for n
       proof (induct n)
         case 0
         then show ?case by simp
       next
         case (Suc n)
         have "(\<Sum>i\<le>Suc n. h1 i - h2 i) = (\<Sum>i\<le>n. h1 i - h2 i) + h1 (n+1) - h2 (n+1)"
           by auto
         also have "... =  h1 0 - h2 n + h1 (n+1) - h2 (n+1)" using Suc by auto
         also have "... = h1 0 - h2 (n+1)"
         proof -
           have "h2 n = h1 (n+1)"
             unfolding h2_def h1_def 
             apply (auto simp:prod.nat_ivl_Suc')
             using a_pos by (metis less_numeral_extra(3))
           then show ?thesis by auto
         qed
         finally show ?case by simp
       qed
       ultimately have "(\<lambda>n. h1 0 - h2 n) \<longlonglongrightarrow> (\<Sum>i. h1 i - h2 i)" by simp
       then have "h2 \<longlonglongrightarrow> (h1 0 -  (\<Sum>i. h1 i - h2 i))"
         apply (elim metric_tendsto_imp_tendsto)
         by (auto intro!:eventuallyI simp add:dist_real_def)
       moreover have "h2 \<longlonglongrightarrow> 0"
       proof -
         have h2_n:"\<bar>h2 n\<bar> < (1 / 2)^(n+1)" for n 
         proof -
           have "\<bar>h2 n\<bar> = \<bar>c (n + N + 1)\<bar> / prod a {N..n + N}"
             unfolding h2_def abs_divide
             using a_pos by (simp add: abs_of_pos prod_pos)
           also have "... < (a (N+n) / 2) / prod a {N..n + N}"
             unfolding h2_def
             apply (rule divide_strict_right_mono)
             subgoal using large_n[rule_format,of "N+n"] by (auto simp add:algebra_simps)
             subgoal using a_pos by (simp add: prod_pos)
             done
           also have "... = 1 / (2*prod a {N..<n + N})"
             apply (subst ivl_disj_un(6)[of N "n+N",symmetric])
             using a_pos[rule_format,of "N+n"] by (auto simp add:algebra_simps)
           also have "... \<le> (1/2)^(n+1)"
           proof (induct n)
             case 0
             then show ?case by auto
           next
             case (Suc n)
             define P where "P=1 / real_of_int (2 * prod a {N..<n + N})"
             have "1 / real_of_int (2 * prod a {N..<Suc n + N}) = P / a (n+N)"
               unfolding P_def by (auto simp add: prod.atLeastLessThan_Suc)
             also have "... \<le>  ( (1 / 2) ^ (n + 1) ) / a (n+N) "
               apply (rule divide_right_mono)
               subgoal unfolding P_def using Suc by auto
               subgoal by (simp add: a_pos less_imp_le)
               done
             also have "... \<le> ( (1 / 2) ^ (n + 1) ) / 2 "
               apply (rule divide_left_mono)
               using large_n[rule_format,of "n+N",simplified] by auto
             also have "... = (1 / 2) ^ (n + 2)" by auto
             finally show ?case by simp
           qed
           finally show ?thesis .
         qed
         have "(\<lambda>n. (1 / 2)^(n+1)) \<longlonglongrightarrow> (0::real)" 
           using tendsto_mult_right_zero[OF LIMSEQ_abs_realpow_zero2[of "1/2",simplified],of "1/2"]
           by auto
         then show ?thesis 
           apply (elim Lim_null_comparison[rotated])
           using h2_n less_eq_real_def by (auto intro!:eventuallyI)
       qed
       ultimately have "(\<Sum>i. h1 i - h2 i) = h1 0"
         using LIMSEQ_unique by fastforce
       then show ?thesis by simp
     qed
     also have "... = C + c N"
       unfolding h1_def using a_pos 
       by auto (metis less_irrefl)
     finally show ?thesis . 
   qed
   then have "S = (C + real_of_int (c N)) / (B*prod a {..<N})" 
     by (metis \<open>0 < B\<close> a_pos less_irrefl mult.commute mult_pos_pos 
         nonzero_mult_div_cancel_right of_int_eq_0_iff prod_pos)
   moreover have "... \<in> \<rat>"
     unfolding C_def f_def by (intro Rats_divide Rats_add Rats_mult Rats_of_int Rats_sum)
   ultimately show "S \<in> \<rat>" by auto
 qed
 
 theorem theorem_2_1_Erdos_Straus :
   "(\<Sum>n. (b n / (\<Prod>i \<le> n. a i))) \<in> \<rat> \<longleftrightarrow> (\<exists> (B::int)>0. \<exists> c::nat\<Rightarrow> int.
             (\<forall>\<^sub>F n in sequentially. B*b n = c n * a n - c(n+1) \<and> \<bar>c(n+1)\<bar><a n/2))"
   using ab_rationality_imp imp_ab_rational by auto
 
 text\<open>The following is a Corollary to Theorem 2.1.  \<close>
 
 corollary corollary_2_10_Erdos_Straus:
   assumes ab_event:"\<forall>\<^sub>F n in sequentially. b n > 0 \<and> a (n+1) \<ge> a n" 
     and ba_lim_leq:"lim (\<lambda>n. (b(n+1) - b n )/a n) \<le> 0" 
     and ba_lim_exist:"convergent (\<lambda>n. (b(n+1) - b n )/a n)"
     and "liminf (\<lambda>n. a n / b n) = 0 "
   shows "(\<Sum>n. (b n / (\<Prod>i \<le> n. a i))) \<notin> \<rat>"
 proof 
   assume "(\<Sum>n. (b n / (\<Prod>i \<le> n. a i))) \<in> \<rat>"
   then obtain B c where "B>0" and abc_event:"\<forall>\<^sub>F n in sequentially. B * b n = c n * a n - c (n + 1) 
           \<and> \<bar>c (n + 1)\<bar> < a n / 2" and ca_vanish: "(\<lambda>n. c (Suc n) / a n) \<longlonglongrightarrow> 0"
     using ab_rationality_imp by auto
 
   have bac_close:"(\<lambda>n. B * b n / a n - c n) \<longlonglongrightarrow> 0"
   proof -
     have "\<forall>\<^sub>F n in sequentially. B * b n - c n * a n + c (n + 1) = 0"
       using abc_event by (auto elim!:eventually_mono)
     then have "\<forall>\<^sub>F n in sequentially. (B * b n - c n * a n + c (n+1)) / a n = 0 "
       apply eventually_elim
       by auto
     then have "\<forall>\<^sub>F n in sequentially. B * b n / a n - c n  + c (n + 1) / a n = 0"
       apply eventually_elim
       using a_pos by (auto simp:divide_simps) (metis less_irrefl)
     then have "(\<lambda>n. B * b n / a n - c n  + c (n + 1) / a n) \<longlonglongrightarrow> 0"
       by (simp add: eventually_mono tendsto_iff)
     from tendsto_diff[OF this ca_vanish]  
     show ?thesis by auto
   qed
 
   have c_pos:"\<forall>\<^sub>F n in sequentially. c n > 0" 
   proof -
     from bac_close have *:"\<forall>\<^sub>F n in sequentially. c n \<ge> 0"
       apply (elim tendsto_of_int_diff_0)
       using ab_event a_large apply (eventually_elim) 
       using \<open>B>0\<close> by auto 
     show ?thesis
     proof (rule ccontr)
       assume "\<not> (\<forall>\<^sub>F n in sequentially. c n > 0)"
       moreover have "\<forall>\<^sub>F n in sequentially. c (Suc n) \<ge> 0 \<and> c n\<ge>0"
         using * eventually_sequentially_Suc[of "\<lambda>n. c n\<ge>0"] 
         by (metis (mono_tags, lifting) eventually_at_top_linorder le_Suc_eq)
       ultimately have "\<exists>\<^sub>F n in sequentially. c n = 0 \<and> c (Suc n) \<ge> 0"
         using eventually_elim2 frequently_def by fastforce
       moreover have "\<forall>\<^sub>F n in sequentially. b n > 0 \<and> B * b n = c n * a n - c (n + 1)"
         using ab_event abc_event by eventually_elim auto
       ultimately have "\<exists>\<^sub>F n in sequentially. c n = 0 \<and> c (Suc n) \<ge> 0 \<and> b n > 0 
                           \<and> B * b n = c n * a n - c (n + 1)"
         using frequently_eventually_frequently by fastforce
       from frequently_ex[OF this] 
       obtain n where "c n = 0" "c (Suc n) \<ge> 0" "b n > 0" 
         "B * b n = c n * a n - c (n + 1)"
         by auto
       then have "B * b n \<le> 0" by auto
       then show False using \<open>b n>0\<close> \<open>B > 0\<close> using mult_pos_pos not_le by blast
     qed
   qed
 
   have bc_epsilon:"\<forall>\<^sub>F n in sequentially. b (n+1) / b n >  (c (n+1) - \<epsilon>) / c n" when "\<epsilon>>0" "\<epsilon><1" for \<epsilon>::real
   proof -
     have "\<forall>\<^sub>F x in sequentially. \<bar>c (Suc x) / a x\<bar> < \<epsilon> / 2"
       using ca_vanish[unfolded tendsto_iff,rule_format, of "\<epsilon>/2"] \<open>\<epsilon>>0\<close> by auto
     moreover then have "\<forall>\<^sub>F x in sequentially. \<bar>c (x+2) / a (x+1)\<bar> < \<epsilon> / 2"
       apply (subst (asm) eventually_sequentially_Suc[symmetric])
       by simp
     moreover have "\<forall>\<^sub>F n in sequentially. B * b (n+1) = c (n+1) * a (n+1) - c (n + 2)"
       using abc_event
       apply (subst (asm) eventually_sequentially_Suc[symmetric])
       by (auto elim:eventually_mono)
     moreover have "\<forall>\<^sub>F n in sequentially. c n > 0 \<and> c (n+1) > 0 \<and> c (n+2) > 0"
     proof -
       have "\<forall>\<^sub>F n in sequentially. 0 < c (Suc n)"
         using c_pos by (subst eventually_sequentially_Suc) simp
       moreover then have "\<forall>\<^sub>F n in sequentially. 0 < c (Suc (Suc n))"
         using c_pos by (subst eventually_sequentially_Suc) simp
       ultimately show ?thesis using c_pos by eventually_elim auto
     qed
     ultimately show ?thesis using ab_event abc_event 
     proof eventually_elim
       case (elim n)
       define \<epsilon>\<^sub>0 \<epsilon>\<^sub>1 where "\<epsilon>\<^sub>0 = c (n+1) / a n" and "\<epsilon>\<^sub>1 = c (n+2) / a (n+1)"
       have "\<epsilon>\<^sub>0 > 0" "\<epsilon>\<^sub>1 > 0" "\<epsilon>\<^sub>0 < \<epsilon>/2" "\<epsilon>\<^sub>1 < \<epsilon>/2" using a_pos elim by (auto simp add: \<epsilon>\<^sub>0_def \<epsilon>\<^sub>1_def)
       have "(\<epsilon> - \<epsilon>\<^sub>1) * c n > 0"
         apply (rule mult_pos_pos)
         using \<open>\<epsilon>\<^sub>1 > 0\<close> \<open>\<epsilon>\<^sub>1 < \<epsilon>/2\<close> \<open>\<epsilon>>0\<close> elim by auto
       moreover have "\<epsilon>\<^sub>0 * (c (n+1) - \<epsilon>) > 0"
         apply (rule mult_pos_pos[OF \<open>\<epsilon>\<^sub>0 > 0\<close>])
         using elim(4) that(2) by linarith
       ultimately have "(\<epsilon> - \<epsilon>\<^sub>1) * c n + \<epsilon>\<^sub>0 * (c (n+1) - \<epsilon>) > 0" by auto
       moreover have "c n - \<epsilon>\<^sub>0 > 0" using \<open>\<epsilon>\<^sub>0 < \<epsilon> / 2\<close> elim(4) that(2) by linarith
       moreover have "c n > 0" by (simp add: elim(4))
       ultimately have "(c (n+1) - \<epsilon>) / c n < (c (n+1) - \<epsilon>\<^sub>1) / (c n -  \<epsilon>\<^sub>0)"
         by (auto simp add: field_simps)
       also have "... \<le> (c (n+1) - \<epsilon>\<^sub>1) / (c n -  \<epsilon>\<^sub>0) * (a (n+1) / a n)"
       proof -
         have "(c (n+1) - \<epsilon>\<^sub>1) / (c n -  \<epsilon>\<^sub>0) > 0" 
           by (smt \<open>0 < (\<epsilon> - \<epsilon>\<^sub>1) * real_of_int (c n)\<close> \<open>0 < real_of_int (c n) - \<epsilon>\<^sub>0\<close> 
               divide_pos_pos elim(4) mult_le_0_iff of_int_less_1_iff that(2))
         moreover have "(a (n+1) / a n) \<ge> 1" 
           using a_pos elim(5) by auto
         ultimately show ?thesis by (metis mult_cancel_left1 mult_le_cancel_iff2)
       qed
       also have "... = (B * b (n+1)) / (B * b n)"
       proof -
         have "B * b n = c n * a n - c (n + 1)"
           using elim by auto
         also have "... = a n * (c n - \<epsilon>\<^sub>0)"
           using a_pos[rule_format,of n] unfolding \<epsilon>\<^sub>0_def by (auto simp:field_simps)
         finally have "B * b n = a n * (c n - \<epsilon>\<^sub>0)" .
         moreover have "B * b (n+1) = a (n+1) * (c (n+1) - \<epsilon>\<^sub>1)" 
           unfolding \<epsilon>\<^sub>1_def 
           using a_pos[rule_format,of "n+1"] 
           apply (subst \<open>B * b (n + 1) = c (n + 1) * a (n + 1) - c (n + 2)\<close>)
           by (auto simp:field_simps)
         ultimately show ?thesis by (simp add: mult.commute)
       qed
       also have "... = b (n+1) / b n" 
         using \<open>B>0\<close> by auto
       finally show ?case .
     qed
   qed
 
   have eq_2_11:"\<exists>\<^sub>F n in sequentially. b (n+1) > b n + (1 - \<epsilon>)^2 * a n / B" 
     when "\<epsilon>>0" "\<epsilon><1" "\<not> (\<forall>\<^sub>F n in sequentially. c (n+1) \<le> c n)"  for \<epsilon>::real
   proof -
     have "\<exists>\<^sub>F x in sequentially. c x < c (Suc x) " using that(3) 
       by (simp add:not_eventually frequently_elim1)
     moreover have "\<forall>\<^sub>F x in sequentially. \<bar>c (Suc x) / a x\<bar> < \<epsilon>"
       using ca_vanish[unfolded tendsto_iff,rule_format, of \<epsilon>] \<open>\<epsilon>>0\<close> by auto
     moreover have "\<forall>\<^sub>F n in sequentially. c n > 0 \<and> c (n+1) > 0"
     proof -
       have "\<forall>\<^sub>F n in sequentially. 0 < c (Suc n)"
         using c_pos by (subst eventually_sequentially_Suc) simp
       then show ?thesis using c_pos by eventually_elim auto
     qed
     ultimately show ?thesis  using ab_event abc_event bc_epsilon[OF \<open>\<epsilon>>0\<close> \<open>\<epsilon><1\<close>] 
     proof (elim frequently_rev_mp,eventually_elim)
       case (elim n)
       then have "c (n+1) / a n < \<epsilon>" 
         using a_pos[rule_format,of n] by auto
       also have "... \<le> \<epsilon> * c n" using elim(7) that(1) by auto
       finally have "c (n+1) / a n < \<epsilon> * c n" .
       then have "c (n+1) / c n < \<epsilon> * a n" 
         using a_pos[rule_format,of n] elim by (auto simp:field_simps)
       then have "(1 - \<epsilon>) * a n < a n - c (n+1) / c n"
         by (auto simp:algebra_simps)
       then have "(1 - \<epsilon>)^2 * a n / B < (1 - \<epsilon>) * (a n - c (n+1) / c n) / B"
         apply (subst (asm) mult_less_iff1[symmetric, of "(1-\<epsilon>)/B"])
         using \<open>\<epsilon><1\<close> \<open>B>0\<close> by (auto simp: divide_simps power2_eq_square mult_less_iff1)
       then have "b n + (1 - \<epsilon>)^2 * a n / B < b n + (1 - \<epsilon>) * (a n - c (n+1) / c n) / B"
         using \<open>B>0\<close> by auto
       also have "... = b n + (1 - \<epsilon>) * ((c n *a n - c (n+1)) / c n) / B"
         using elim by (auto simp:field_simps)
       also have "... = b n + (1 - \<epsilon>) * (b n / c n)"
       proof -
         have "B * b n = c n * a n - c (n + 1)" using elim by auto
         from this[symmetric] show ?thesis
           using \<open>B>0\<close> by simp
       qed
       also have "... = (1+(1-\<epsilon>)/c n) * b n"
         by (auto simp:algebra_simps)
       also have "... = ((c n+1-\<epsilon>)/c n) * b n"
         using elim by (auto simp:divide_simps)
       also have "... \<le> ((c (n+1) -\<epsilon>)/c n) * b n"
       proof -
         define cp where "cp = c n+1"
         have "c (n+1) \<ge> cp" unfolding cp_def using \<open>c n < c (Suc n)\<close> by auto
         moreover have "c n>0" "b n>0" using elim by auto
         ultimately show ?thesis 
           apply (fold cp_def)
           by (auto simp:divide_simps)
       qed
       also have "... < b (n+1)"
         using elim by (auto simp:divide_simps)
       finally show ?case .
     qed
   qed
 
   have "\<forall>\<^sub>F n in sequentially. c (n+1) \<le> c n"
   proof (rule ccontr)
     assume "\<not> (\<forall>\<^sub>F n in sequentially. c (n + 1) \<le> c n)"
     from eq_2_11[OF _ _ this,of "1/2"]
     have "\<exists>\<^sub>F n in sequentially. b (n+1) > b n + 1/4 * a n / B" 
       by (auto simp:algebra_simps power2_eq_square)
     then have *:"\<exists>\<^sub>F n in sequentially. (b (n+1) - b n) / a n > 1 / (B * 4)" 
       apply (elim frequently_elim1)
       subgoal for n
         using a_pos[rule_format,of n] by (auto simp:field_simps)
       done
     define f where "f = (\<lambda>n. (b (n+1) - b n) / a n)"
     have "f \<longlonglongrightarrow> lim f"
       using convergent_LIMSEQ_iff ba_lim_exist unfolding f_def by auto
     from this[unfolded tendsto_iff,rule_format, of "1 / (B*4)"] 
     have "\<forall>\<^sub>F x in sequentially. \<bar>f x - lim f\<bar> < 1 / (B * 4)"
       using \<open>B>0\<close> by (auto simp:dist_real_def)
     moreover have "\<exists>\<^sub>F n in sequentially. f n > 1 / (B * 4)" 
       using * unfolding f_def by auto
     ultimately have "\<exists>\<^sub>F n in sequentially. f n > 1 / (B * 4) \<and> \<bar>f n - lim f\<bar> < 1 / (B * 4)"
       by (auto elim:frequently_eventually_frequently[rotated])
     from frequently_ex[OF this] 
     obtain n where "f n > 1 / (B * 4)" "\<bar>f n - lim f\<bar> < 1 / (B * 4)"
       by auto
     moreover have "lim f \<le> 0" using ba_lim_leq unfolding f_def by auto
     ultimately show False by linarith
   qed
   then obtain N where N_dec:"\<forall>n\<ge>N. c (n+1) \<le> c n" by (meson eventually_at_top_linorder)
   define max_c where "max_c = (MAX n \<in> {..N}. c n)"
   have max_c:"c n \<le> max_c" for n
   proof (cases "n\<le>N")
     case True
     then show ?thesis unfolding max_c_def by simp
   next
     case False
     then have "n\<ge>N" by auto
     then have "c n\<le>c N" 
     proof (induct rule:nat_induct_at_least)
       case base
       then show ?case by simp
     next
       case (Suc n)
       then have "c (n+1) \<le> c n" using N_dec by auto
       then show ?case using \<open>c n \<le> c N\<close> by auto
     qed
     moreover have "c N \<le> max_c" unfolding max_c_def by auto
     ultimately show ?thesis by auto
   qed
   have "max_c > 0 " 
   proof -
     obtain N where "\<forall>n\<ge>N. 0 < c n" 
       using c_pos[unfolded eventually_at_top_linorder] by auto
     then have "c N > 0" by auto
     then show ?thesis using max_c[of N] by simp
   qed
   have ba_limsup_bound:"1/(B*(B+1)) \<le> limsup (\<lambda>n. b n/a n)" 
     "limsup (\<lambda>n. b n/a n) \<le> max_c / B + 1 / (B+1)"
   proof -
     define f where "f = (\<lambda>n. b n/a n)"
     from tendsto_mult_right_zero[OF bac_close,of "1/B"] 
     have "(\<lambda>n. f n - c n / B) \<longlonglongrightarrow> 0"
       unfolding f_def using  \<open>B>0\<close> by (auto simp:algebra_simps)
     from this[unfolded tendsto_iff,rule_format,of "1/(B+1)"]
     have "\<forall>\<^sub>F x in sequentially. \<bar>f x - c x / B\<bar> < 1 / (B+1)"
       using \<open>B>0\<close> by auto
     then have *:"\<forall>\<^sub>F n in sequentially. 1/(B*(B+1)) \<le> ereal (f n) \<and> ereal (f n) \<le> max_c / B + 1 / (B+1)" 
       using c_pos
     proof eventually_elim
       case (elim n)
       then have "f n - c n / B < 1 / (B+1)" by auto
       then have "f n < c n / B + 1 / (B+1)" by simp
       also have "... \<le> max_c / B + 1 / (B+1)"
         using max_c[of n] using \<open>B>0\<close> by (auto simp:divide_simps)
       finally have *:"f n < max_c / B + 1 / (B+1)" .
 
       have "1/(B*(B+1)) = 1/B - 1 / (B+1)" 
         using \<open>B>0\<close> by (auto simp:divide_simps)
       also have "... \<le> c n/B - 1 / (B+1)" 
         using \<open>0 < c n\<close> \<open>B>0\<close> by (auto,auto simp:divide_simps)
       also have "... < f n" using elim by auto
       finally have "1/(B*(B+1)) < f n" .
       with * show ?case by simp
     qed
     show "limsup f \<le> max_c / B + 1 / (B+1)"
       apply (rule Limsup_bounded)
       using * by (auto elim:eventually_mono)
     have "1/(B*(B+1)) \<le> liminf f"
       apply (rule Liminf_bounded)
       using * by (auto elim:eventually_mono)
     also have "liminf f \<le> limsup f" by (simp add: Liminf_le_Limsup)
     finally show "1/(B*(B+1)) \<le> limsup f" .
   qed
 
   have "0 < inverse (ereal (max_c / B + 1 / (B+1)))"
     using \<open>max_c > 0\<close> \<open>B>0\<close> 
     by (simp add: pos_add_strict)
   also have "... \<le> inverse (limsup (\<lambda>n. b n/a n))"
   proof (rule ereal_inverse_antimono[OF _ ba_limsup_bound(2)])
     have "0<1/(B*(B+1))" using \<open>B>0\<close> by auto
     also have "... \<le> limsup (\<lambda>n. b n/a n)" using ba_limsup_bound(1) .
     finally show "0\<le>limsup (\<lambda>n. b n/a n)" using zero_ereal_def by auto
   qed 
   also have "... = liminf (\<lambda>n. inverse (ereal ( b n/a n)))"
     apply (subst Liminf_inverse_ereal[symmetric])
     using a_pos ab_event by (auto elim!:eventually_mono simp:divide_simps)
   also have "... = liminf (\<lambda>n. ( a n/b n))"
     apply (rule Liminf_eq)
     using a_pos ab_event 
     apply (auto elim!:eventually_mono) 
     by (metis less_int_code(1))
   finally have "liminf (\<lambda>n. ( a n/b n)) > 0" .
   then show False using \<open>liminf (\<lambda>n. a n / b n) = 0\<close> by simp
 qed
 
 end
 
 section\<open>Some auxiliary results on the prime numbers. \<close>
 
 lemma nth_prime_nonzero[simp]:"nth_prime n \<noteq> 0"
   by (simp add: prime_gt_0_nat prime_nth_prime)
 
 lemma nth_prime_gt_zero[simp]:"nth_prime n >0"
   by (simp add: prime_gt_0_nat prime_nth_prime)
 
 lemma ratio_of_consecutive_primes:
   "(\<lambda>n. nth_prime (n+1)/nth_prime n) \<longlonglongrightarrow>1"
 proof -
   define f where "f=(\<lambda>x. real (nth_prime (Suc x)) /real (nth_prime x))"
   define g where "g=(\<lambda>x. (real x * ln (real x)) 
                               / (real (Suc x) * ln (real (Suc x))))"
   have p_n:"(\<lambda>x. real (nth_prime x) / (real x * ln (real x))) \<longlonglongrightarrow> 1"
     using nth_prime_asymptotics[unfolded asymp_equiv_def,simplified] .
   moreover have p_sn:"(\<lambda>n. real (nth_prime (Suc n)) 
                         / (real (Suc n) * ln (real (Suc n)))) \<longlonglongrightarrow> 1"
     using nth_prime_asymptotics[unfolded asymp_equiv_def,simplified
         ,THEN LIMSEQ_Suc] .
   ultimately have "(\<lambda>x. f x * g x) \<longlonglongrightarrow> 1"
     using tendsto_divide[OF p_sn p_n] 
     unfolding f_def g_def by (auto simp:algebra_simps)
   moreover have "g \<longlonglongrightarrow> 1" unfolding g_def
     by real_asymp
   ultimately have "(\<lambda>x. if g x = 0 then 0 else f x) \<longlonglongrightarrow> 1"
     apply (drule_tac tendsto_divide[OF _ \<open>g \<longlonglongrightarrow> 1\<close>])
     by auto
   then have "f \<longlonglongrightarrow> 1"
   proof (elim filterlim_mono_eventually)
     have "\<forall>\<^sub>F x in sequentially. (if g (x+3) = 0 then 0 
                 else f (x+3)) = f (x+3)" 
       unfolding g_def by auto
     then show "\<forall>\<^sub>F x in sequentially. (if g x = 0 then 0 else f x) = f x"
       apply (subst (asm) eventually_sequentially_seg)
       by simp
   qed auto
   then show ?thesis unfolding f_def by auto
 qed
 
 lemma nth_prime_double_sqrt_less:
   assumes "\<epsilon> > 0"
   shows "\<forall>\<^sub>F n in sequentially. (nth_prime (2*n) - nth_prime n) 
             / sqrt (nth_prime n) < n powr (1/2+\<epsilon>)"
 proof -
   define pp ll where 
     "pp=(\<lambda>n. (nth_prime (2*n) - nth_prime n) / sqrt (nth_prime n))" and
     "ll=(\<lambda>x::nat. x * ln x)"
   have pp_pos:"pp (n+1) > 0" for n
     unfolding pp_def by simp
 
   have "(\<lambda>x. nth_prime (2 * x)) \<sim>[sequentially] (\<lambda>x. (2 * x) * ln (2 * x))"
     using nth_prime_asymptotics[THEN asymp_equiv_compose
         ,of "(*) 2" sequentially,unfolded comp_def]
     using mult_nat_left_at_top pos2 by blast
   also have "... \<sim>[sequentially] (\<lambda>x. 2 *x * ln x)"
     by real_asymp
   finally have "(\<lambda>x. nth_prime (2 * x)) \<sim>[sequentially] (\<lambda>x. 2 *x * ln x)" .
   from this[unfolded asymp_equiv_def, THEN tendsto_mult_left,of 2]
   have "(\<lambda>x. nth_prime (2 * x) / (x * ln x)) \<longlonglongrightarrow> 2"
     unfolding asymp_equiv_def by auto
   moreover have *:"(\<lambda>x. nth_prime x / (x * ln x)) \<longlonglongrightarrow> 1"
     using nth_prime_asymptotics unfolding asymp_equiv_def by auto
   ultimately    
   have "(\<lambda>x. (nth_prime (2 * x) - nth_prime x) / ll x) \<longlonglongrightarrow> 1"
     unfolding ll_def
     apply -
     apply (drule (1) tendsto_diff)
     apply (subst of_nat_diff,simp)
     by (subst diff_divide_distrib,simp)
   moreover have "(\<lambda>x. sqrt (nth_prime x) / sqrt (ll x)) \<longlonglongrightarrow> 1"
     unfolding ll_def
     using tendsto_real_sqrt[OF *] 
     by (auto simp: real_sqrt_divide)
   ultimately have "(\<lambda>x. pp x * (sqrt (ll x) / (ll x))) \<longlonglongrightarrow> 1"
     apply -
     apply (drule (1) tendsto_divide,simp)
     by (auto simp:field_simps of_nat_diff pp_def)
   moreover have "\<forall>\<^sub>F x in sequentially. sqrt (ll x) / ll x = 1/sqrt (ll x)"
     apply (subst eventually_sequentially_Suc[symmetric])
     by (auto intro!:eventuallyI simp:ll_def divide_simps)
   ultimately have "(\<lambda>x. pp x / sqrt (ll x)) \<longlonglongrightarrow> 1"
     apply (elim filterlim_mono_eventually)
     by (auto elim!:eventually_mono) (metis mult.right_neutral times_divide_eq_right)
   moreover have "(\<lambda>x. sqrt (ll x) / x powr (1/2+\<epsilon>)) \<longlonglongrightarrow> 0"
     unfolding ll_def using \<open>\<epsilon>>0\<close> by real_asymp
   ultimately have "(\<lambda>x. pp x / x powr (1/2+\<epsilon>) * 
                       (sqrt (ll x) / sqrt (ll x))) \<longlonglongrightarrow> 0"
     apply -
     apply (drule (1) tendsto_mult)
     by (auto elim:filterlim_mono_eventually)
   moreover have "\<forall>\<^sub>F x in sequentially. sqrt (ll x) / sqrt (ll x) = 1"
     apply (subst eventually_sequentially_Suc[symmetric])
     by (auto intro!:eventuallyI simp:ll_def )
   ultimately have "(\<lambda>x. pp x / x powr (1/2+\<epsilon>)) \<longlonglongrightarrow> 0"
     apply (elim filterlim_mono_eventually)
     by (auto elim:eventually_mono)
   from tendstoD[OF this, of 1,simplified]
   show "\<forall>\<^sub>F x in sequentially. pp x < x powr (1 / 2 + \<epsilon>)"
     apply (elim eventually_mono_sequentially[of _ 1])
     using pp_pos by auto
 qed
 
 
 section \<open>Theorem 3.1\<close>
 
 text\<open>Theorem 3.1 is an application of Theorem 2.1 with the sequences considered involving 
 the prime numbers.\<close>
 
 theorem theorem_3_10_Erdos_Straus:
   fixes a::"nat \<Rightarrow> int"
   assumes a_pos:"\<forall> n. a n >0" and "mono a"
     and nth_1:"(\<lambda>n. nth_prime n / (a n)^2) \<longlonglongrightarrow> 0"
     and nth_2:"liminf (\<lambda>n. a n / nth_prime n) = 0"
   shows "(\<Sum>n. (nth_prime n / (\<Prod>i \<le> n. a i))) \<notin> \<rat>"
 proof
   assume asm:"(\<Sum>n. (nth_prime n / (\<Prod>i \<le> n. a i))) \<in> \<rat>"
 
   have a2_omega:"(\<lambda>n. (a n)^2) \<in> \<omega>(\<lambda>x. x * ln x)"
   proof -
     have "(\<lambda>n. real (nth_prime n)) \<in> o(\<lambda>n. real_of_int ((a n)\<^sup>2))"
       apply (rule smalloI_tendsto[OF nth_1])
       using a_pos by (metis (mono_tags, lifting) less_int_code(1) 
           not_eventuallyD of_int_0_eq_iff zero_eq_power2)
     moreover have "(\<lambda>x. real (nth_prime x)) \<in> \<Omega>(\<lambda>x. real x * ln (real x))"
       using nth_prime_bigtheta
       by blast
     ultimately show ?thesis 
       using landau_omega.small_big_trans smallo_imp_smallomega by blast
   qed
 
   have a_gt_1:"\<forall>\<^sub>F n in sequentially. 1 < a n" 
   proof -
     have "\<forall>\<^sub>F x in sequentially. \<bar>x * ln x\<bar> \<le> (a x)\<^sup>2"
       using a2_omega[unfolded smallomega_def,simplified,rule_format,of 1]
       by auto
     then have "\<forall>\<^sub>F x in sequentially. \<bar>(x+3) * ln (x+3)\<bar> \<le> (a (x+3))\<^sup>2" 
       apply (subst (asm) eventually_sequentially_seg[symmetric, of _ 3])
       by simp
     then have "\<forall>\<^sub>F n in sequentially. 1 < a ( n+3)" 
     proof (elim eventually_mono)
       fix x
       assume "\<bar>real (x + 3) * ln (real (x + 3))\<bar> \<le> real_of_int ((a (x + 3))\<^sup>2)"
       moreover have "\<bar>real (x + 3) * ln (real (x + 3))\<bar> > 3"
       proof -
         have "ln (real (x + 3)) > 1"
           apply simp using ln3_gt_1 ln_gt_1 by force
         moreover have "real(x+3) \<ge> 3" by simp
         ultimately have "(x+3)*ln (real (x + 3)) > 3*1 "
           apply (rule_tac mult_le_less_imp_less)
           by auto
         then show ?thesis by auto
       qed
       ultimately have "real_of_int ((a (x + 3))\<^sup>2) > 3"
         by auto
       then show "1 < a (x + 3)" 
         by (smt Suc3_eq_add_3 a_pos add.commute of_int_1 one_power2)
     qed
     then show ?thesis 
       apply (subst eventually_sequentially_seg[symmetric, of _ 3])
       by auto
   qed
 
   obtain B::int and c where 
     "B>0" and Bc_large:"\<forall>\<^sub>F n in sequentially. B * nth_prime n 
                 = c n * a n - c (n + 1) \<and> \<bar>c (n + 1)\<bar> <  a n / 2"
     and ca_vanish: "(\<lambda>n. c (Suc n) / real_of_int (a n)) \<longlonglongrightarrow> 0"
   proof -
     note a_gt_1
     moreover have "(\<lambda>n. real_of_int \<bar>int (nth_prime n)\<bar> 
                     / real_of_int (a (n - 1) * a n)) \<longlonglongrightarrow> 0" 
     proof -
       define f where "f=(\<lambda>n. nth_prime (n+1) / (a n * a (n+1)))"
       define g where "g=(\<lambda>n. 2*nth_prime n / (a n)^2)"
       have "\<forall>\<^sub>F x in sequentially. norm (f x) \<le> g x"
       proof -
         have "\<forall>\<^sub>F n in sequentially. nth_prime (n+1) < 2*nth_prime n" 
           using ratio_of_consecutive_primes[unfolded tendsto_iff
               ,rule_format,of 1,simplified]
           apply (elim eventually_mono)
           by (auto simp :divide_simps dist_norm)
         moreover have "\<forall>\<^sub>F n in sequentially. real_of_int (a n * a (n+1))
                            \<ge> (a n)^2"
           apply (rule eventuallyI)
           using \<open>mono a\<close> by (auto simp:power2_eq_square a_pos incseq_SucD)
         ultimately show ?thesis unfolding f_def g_def
           apply eventually_elim
           apply (subst norm_divide)
           apply (rule_tac linordered_field_class.frac_le)
           using a_pos[rule_format, THEN order.strict_implies_not_eq ]
           by auto
       qed
       moreover have "g \<longlonglongrightarrow> 0 " 
         using nth_1[THEN tendsto_mult_right_zero,of 2] unfolding g_def 
         by auto
       ultimately have "f \<longlonglongrightarrow> 0" 
         using Lim_null_comparison[of f g sequentially]
         by auto
       then show ?thesis
         unfolding f_def
         by (rule_tac LIMSEQ_imp_Suc) auto
     qed
     moreover have "(\<Sum>n. real_of_int (int (nth_prime n)) 
                     / real_of_int (prod a {..n})) \<in> \<rat>" 
       using asm by simp
     ultimately have "\<exists>B>0. \<exists>c. (\<forall>\<^sub>F n in sequentially.
               B * int (nth_prime n) = c n * a n - c (n + 1) \<and>
               real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2) \<and>
           (\<lambda>n. real_of_int (c (Suc n)) / real_of_int (a n)) \<longlonglongrightarrow> 0"
       using ab_rationality_imp[OF a_pos,of nth_prime] by fast
     then show thesis 
       apply clarify
       apply (rule_tac c=c and B=B in that)
       by auto
   qed
 
   have bac_close:"(\<lambda>n. B * nth_prime n / a n - c n) \<longlonglongrightarrow> 0"
   proof -
     have "\<forall>\<^sub>F n in sequentially. B * nth_prime n - c n * a n + c (n + 1) = 0"
       using Bc_large by (auto elim!:eventually_mono)
     then have "\<forall>\<^sub>F n in sequentially. (B * nth_prime n - c n * a n + c (n+1)) / a n = 0 "
       by eventually_elim auto
     then have "\<forall>\<^sub>F n in sequentially. B * nth_prime n / a n - c n  + c (n + 1) / a n = 0"
       apply eventually_elim
       using a_pos by (auto simp:divide_simps) (metis less_irrefl)
     then have "(\<lambda>n. B * nth_prime n / a n - c n  + c (n + 1) / a n) \<longlonglongrightarrow> 0"
       by (simp add: eventually_mono tendsto_iff)
     from tendsto_diff[OF this ca_vanish]  
     show ?thesis by auto
   qed
 
   have c_pos:"\<forall>\<^sub>F n in sequentially. c n > 0" 
   proof -
     from bac_close have *:"\<forall>\<^sub>F n in sequentially. c n \<ge> 0"
       apply (elim tendsto_of_int_diff_0)
       using a_gt_1 apply (eventually_elim) 
       using \<open>B>0\<close> by auto 
     show ?thesis
     proof (rule ccontr)
       assume "\<not> (\<forall>\<^sub>F n in sequentially. c n > 0)"
       moreover have "\<forall>\<^sub>F n in sequentially. c (Suc n) \<ge> 0 \<and> c n\<ge>0"
         using * eventually_sequentially_Suc[of "\<lambda>n. c n\<ge>0"] 
         by (metis (mono_tags, lifting) eventually_at_top_linorder le_Suc_eq)
       ultimately have "\<exists>\<^sub>F n in sequentially. c n = 0 \<and> c (Suc n) \<ge> 0"
         using eventually_elim2 frequently_def by fastforce
       moreover have "\<forall>\<^sub>F n in sequentially. nth_prime n > 0 
                         \<and> B * nth_prime n = c n * a n - c (n + 1)"
         using Bc_large by eventually_elim auto
       ultimately have "\<exists>\<^sub>F n in sequentially. c n = 0 \<and> c (Suc n) \<ge> 0 
           \<and> B * nth_prime n = c n * a n - c (n + 1)"
         using frequently_eventually_frequently by fastforce
       from frequently_ex[OF this] 
       obtain n where "c n = 0" "c (Suc n) \<ge> 0"
         "B * nth_prime n = c n * a n - c (n + 1)"
         by auto
       then have "B * nth_prime n \<le> 0" by auto
       then show False using \<open>B > 0\<close> 
         by (simp add: mult_le_0_iff)
     qed
   qed
 
   have B_nth_prime:"\<forall>\<^sub>F n in sequentially. nth_prime n > B" 
   proof -
     have "\<forall>\<^sub>F x in sequentially. B+1 \<le> nth_prime x"
       using nth_prime_at_top[unfolded filterlim_at_top_ge[where c="nat B+1"]
           ,rule_format,of "nat B + 1",simplified] 
 
       apply (elim eventually_mono)
       using \<open>B>0\<close> by auto
     then show ?thesis 
       by (auto elim: eventually_mono)
   qed
 
   have bc_epsilon:"\<forall>\<^sub>F n in sequentially. nth_prime (n+1) 
             / nth_prime n >  (c (n+1) - \<epsilon>) / c n" when "\<epsilon>>0" "\<epsilon><1" for \<epsilon>::real
   proof -
     have "\<forall>\<^sub>F x in sequentially. \<bar>c (Suc x) / a x\<bar> < \<epsilon> / 2"
       using ca_vanish[unfolded tendsto_iff,rule_format, of "\<epsilon>/2"] \<open>\<epsilon>>0\<close> by auto
     moreover then have "\<forall>\<^sub>F x in sequentially. \<bar>c (x+2) / a (x+1)\<bar> < \<epsilon> / 2"
       apply (subst (asm) eventually_sequentially_Suc[symmetric])
       by simp
     moreover have "\<forall>\<^sub>F n in sequentially. B * nth_prime (n+1) = c (n+1) * a (n+1) - c (n + 2)"
       using Bc_large
       apply (subst (asm) eventually_sequentially_Suc[symmetric])
       by (auto elim:eventually_mono)
     moreover have "\<forall>\<^sub>F n in sequentially. c n > 0 \<and> c (n+1) > 0 \<and> c (n+2) > 0"
     proof -
       have "\<forall>\<^sub>F n in sequentially. 0 < c (Suc n)"
         using c_pos by (subst eventually_sequentially_Suc) simp
       moreover then have "\<forall>\<^sub>F n in sequentially. 0 < c (Suc (Suc n))"
         using c_pos by (subst eventually_sequentially_Suc) simp
       ultimately show ?thesis using c_pos by eventually_elim auto
     qed
     ultimately show ?thesis using Bc_large
     proof eventually_elim
       case (elim n)
       define \<epsilon>\<^sub>0 \<epsilon>\<^sub>1 where "\<epsilon>\<^sub>0 = c (n+1) / a n" and "\<epsilon>\<^sub>1 = c (n+2) / a (n+1)"
       have "\<epsilon>\<^sub>0 > 0" "\<epsilon>\<^sub>1 > 0" "\<epsilon>\<^sub>0 < \<epsilon>/2" "\<epsilon>\<^sub>1 < \<epsilon>/2" 
         using a_pos elim \<open>mono a\<close>
         by (auto simp add: \<epsilon>\<^sub>0_def \<epsilon>\<^sub>1_def abs_of_pos)
       have "(\<epsilon> - \<epsilon>\<^sub>1) * c n > 0"
         using \<open>\<epsilon>\<^sub>1 > 0\<close> \<open>\<epsilon>\<^sub>1 < \<epsilon>/2\<close> \<open>\<epsilon>>0\<close> elim by auto
       moreover have "\<epsilon>\<^sub>0 * (c (n+1) - \<epsilon>) > 0"
         using \<open>\<epsilon>\<^sub>0 > 0\<close> elim(4) that(2) by force
       ultimately have "(\<epsilon> - \<epsilon>\<^sub>1) * c n + \<epsilon>\<^sub>0 * (c (n+1) - \<epsilon>) > 0" by auto
       moreover have "c n - \<epsilon>\<^sub>0 > 0" using \<open>\<epsilon>\<^sub>0 < \<epsilon> / 2\<close> elim(4) that(2) by linarith
       moreover have "c n > 0" by (simp add: elim(4))
       ultimately have "(c (n+1) - \<epsilon>) / c n < (c (n+1) - \<epsilon>\<^sub>1) / (c n -  \<epsilon>\<^sub>0)"
         by (auto simp add:field_simps)
       also have "... \<le> (c (n+1) - \<epsilon>\<^sub>1) / (c n -  \<epsilon>\<^sub>0) * (a (n+1) / a n)"
       proof -
         have "(c (n+1) - \<epsilon>\<^sub>1) / (c n -  \<epsilon>\<^sub>0) > 0" 
           by (smt \<open>0 < (\<epsilon> - \<epsilon>\<^sub>1) * real_of_int (c n)\<close> \<open>0 < real_of_int (c n) - \<epsilon>\<^sub>0\<close> 
               divide_pos_pos elim(4) mult_le_0_iff of_int_less_1_iff that(2))
         moreover have "(a (n+1) / a n) \<ge> 1" 
           using a_pos \<open>mono a\<close> by (simp add: mono_def)
         ultimately show ?thesis by (metis mult_cancel_left1 mult_le_cancel_iff2)
       qed
       also have "... = (B * nth_prime (n+1)) / (B * nth_prime n)"
       proof -
         have "B * nth_prime n = c n * a n - c (n + 1)"
           using elim by auto
         also have "... = a n * (c n - \<epsilon>\<^sub>0)"
           using a_pos[rule_format,of n] unfolding \<epsilon>\<^sub>0_def by (auto simp:field_simps)
         finally have "B * nth_prime n = a n * (c n - \<epsilon>\<^sub>0)" .
         moreover have "B * nth_prime (n+1) = a (n+1) * (c (n+1) - \<epsilon>\<^sub>1)" 
           unfolding \<epsilon>\<^sub>1_def 
           using a_pos[rule_format,of "n+1"] 
           apply (subst \<open>B * nth_prime (n + 1) = c (n + 1) * a (n + 1) - c (n + 2)\<close>)
           by (auto simp:field_simps)
         ultimately show ?thesis by (simp add: mult.commute)
       qed
       also have "... = nth_prime (n+1) / nth_prime n" 
         using \<open>B>0\<close> by auto
       finally show ?case .
     qed
   qed
 
 
   have c_ubound:"\<forall>x. \<exists>n. c n > x"
   proof (rule ccontr)
     assume " \<not> (\<forall>x. \<exists>n. x < c n)"
     then obtain ub where "\<forall>n. c n \<le> ub" "ub > 0"
       by (meson dual_order.trans int_one_le_iff_zero_less le_cases not_le)
     define pa where "pa = (\<lambda>n. nth_prime n / a n)"
     have pa_pos:"\<And>n. pa n > 0" unfolding pa_def by (simp add: a_pos)
     have "liminf (\<lambda>n. 1 / pa n) = 0"
       using nth_2 unfolding pa_def by auto
     then have "(\<exists>y<ereal (real_of_int B / real_of_int (ub + 1)). 
       \<exists>\<^sub>F x in sequentially. ereal (1 / pa x) \<le> y)"
       apply (subst less_Liminf_iff[symmetric])
       using \<open>0 < B\<close> \<open>0 < ub\<close> by auto
     then have "\<exists>\<^sub>F x in sequentially. 1 / pa x < B/(ub+1)"
       by (meson frequently_mono le_less_trans less_ereal.simps(1))
     then have "\<exists>\<^sub>F x in sequentially. B*pa x > (ub+1)"
       apply (elim frequently_elim1)
       by (metis \<open>0 < ub\<close> mult.left_neutral of_int_0_less_iff pa_pos pos_divide_less_eq 
           pos_less_divide_eq times_divide_eq_left zless_add1_eq)
     moreover have "\<forall>\<^sub>F x in sequentially. c x \<le> ub"
       using \<open>\<forall>n. c n \<le> ub\<close> by simp
     ultimately have "\<exists>\<^sub>F x in sequentially. B*pa x - c x > 1"
       by (elim frequently_rev_mp eventually_mono) linarith
     moreover have "(\<lambda>n. B * pa n - c n) \<longlonglongrightarrow>0" 
       unfolding pa_def using bac_close by auto
     from tendstoD[OF this,of 1] 
     have "\<forall>\<^sub>F n in sequentially.  \<bar>B * pa n - c n\<bar> < 1"
       by auto
     ultimately have "\<exists>\<^sub>F x in sequentially. B*pa x - c x > 1 \<and> \<bar>B * pa x - c x\<bar> < 1"
       using frequently_eventually_frequently by blast
     then show False 
       by (simp add: frequently_def)
   qed
 
   have eq_2_11:"\<forall>\<^sub>F n in sequentially. c (n+1)>c n \<longrightarrow> 
                   nth_prime (n+1) > nth_prime n + (1 - \<epsilon>)^2 * a n / B" 
     when "\<epsilon>>0" "\<epsilon><1" for \<epsilon>::real
   proof -
     have "\<forall>\<^sub>F x in sequentially. \<bar>c (Suc x) / a x\<bar> < \<epsilon>"
       using ca_vanish[unfolded tendsto_iff,rule_format, of \<epsilon>] \<open>\<epsilon>>0\<close> by auto
     moreover have "\<forall>\<^sub>F n in sequentially. c n > 0 \<and> c (n+1) > 0"
     proof -
       have "\<forall>\<^sub>F n in sequentially. 0 < c (Suc n)"
         using c_pos by (subst eventually_sequentially_Suc) simp
       then show ?thesis using c_pos by eventually_elim auto
     qed
     ultimately show ?thesis  using Bc_large bc_epsilon[OF \<open>\<epsilon>>0\<close> \<open>\<epsilon><1\<close>] 
     proof (eventually_elim, rule_tac impI)
       case (elim n)
       assume "c n < c (n + 1)"
       have "c (n+1) / a n < \<epsilon>" 
         using a_pos[rule_format,of n] using elim(1,2) by auto
       also have "... \<le> \<epsilon> * c n" using elim(2) that(1) by auto
       finally have "c (n+1) / a n < \<epsilon> * c n" .
       then have "c (n+1) / c n < \<epsilon> * a n" 
         using a_pos[rule_format,of n] elim by (auto simp:field_simps)
       then have "(1 - \<epsilon>) * a n < a n - c (n+1) / c n"
         by (auto simp:algebra_simps)
       then have "(1 - \<epsilon>)^2 * a n / B < (1 - \<epsilon>) * (a n - c (n+1) / c n) / B"
         apply (subst (asm) mult_less_iff1[symmetric, of "(1-\<epsilon>)/B"])
         using \<open>\<epsilon><1\<close> \<open>B>0\<close> by (auto simp: divide_simps power2_eq_square mult_less_iff1)
       then have "nth_prime n + (1 - \<epsilon>)^2 * a n / B < nth_prime n + (1 - \<epsilon>) * (a n - c (n+1) / c n) / B"
         using \<open>B>0\<close> by auto
       also have "... = nth_prime n + (1 - \<epsilon>) * ((c n *a n - c (n+1)) / c n) / B"
         using elim by (auto simp:field_simps)
       also have "... = nth_prime n + (1 - \<epsilon>) * (nth_prime n / c n)"
       proof -
         have "B * nth_prime n = c n * a n - c (n + 1)" using elim by auto
         from this[symmetric] show ?thesis
           using \<open>B>0\<close> by simp
       qed
       also have "... = (1+(1-\<epsilon>)/c n) * nth_prime n"
         by (auto simp:algebra_simps)
       also have "... = ((c n+1-\<epsilon>)/c n) * nth_prime n"
         using elim by (auto simp:divide_simps)
       also have "... \<le> ((c (n+1) -\<epsilon>)/c n) * nth_prime n"
       proof -
         define cp where "cp = c n+1"
         have "c (n+1) \<ge> cp" unfolding cp_def using \<open>c n < c (n + 1)\<close> by auto
         moreover have "c n>0" "nth_prime n>0" using elim by auto
         ultimately show ?thesis 
           apply (fold cp_def)
           by (auto simp:divide_simps)
       qed
       also have "... < nth_prime (n+1)"
         using elim by (auto simp:divide_simps)
       finally show "real (nth_prime n) + (1 - \<epsilon>)\<^sup>2 * real_of_int (a n) 
           / real_of_int B < real (nth_prime (n + 1))" .
     qed
   qed
 
   have c_neq_large:"\<forall>\<^sub>F n in sequentially. c (n+1) \<noteq> c n"
   proof (rule ccontr)
     assume "\<not> (\<forall>\<^sub>F n in sequentially. c (n + 1) \<noteq> c n)"
     then have that:"\<exists>\<^sub>F n in sequentially. c (n + 1) = c n"
       unfolding frequently_def .
     have "\<forall>\<^sub>F x in sequentially. (B * int (nth_prime x) = c x * a x - c (x + 1) 
         \<and> \<bar>real_of_int (c (x + 1))\<bar> < real_of_int (a x) / 2) \<and> 0 < c x \<and> B < int (nth_prime x)
         \<and> (c (x+1)>c x \<longrightarrow> nth_prime (x+1) > nth_prime x +  a x / (2* B))"
       using Bc_large c_pos B_nth_prime eq_2_11[of "1-1/ sqrt 2",simplified]
       by eventually_elim (auto simp:divide_simps)
     then have "\<exists>\<^sub>F m in sequentially. nth_prime (m+1) > (1+1/(2*B))*nth_prime m"
     proof (elim frequently_eventually_at_top[OF that, THEN frequently_at_top_elim])
       fix n
       assume "c (n + 1) = c n \<and>
            (\<forall>y\<ge>n. (B * int (nth_prime y) = c y * a y - c (y + 1) \<and>
                     \<bar>real_of_int (c (y + 1))\<bar> < real_of_int (a y) / 2) \<and>
                    0 < c y \<and> B < int (nth_prime y) \<and> (c y < c (y + 1) \<longrightarrow>
                    real (nth_prime y) + real_of_int (a y) / real_of_int (2 * B)
                    < real (nth_prime (y + 1))))"
       then have "c (n + 1) = c n" 
         and Bc_eq:"\<forall>y\<ge>n. B * int (nth_prime y) = c y * a y - c (y + 1) \<and> 0 < c y 
                             \<and> \<bar>real_of_int (c (y + 1))\<bar> < real_of_int (a y) / 2 
                             \<and> B < int (nth_prime y)
                             \<and> (c y < c (y + 1) \<longrightarrow>
                    real (nth_prime y) + real_of_int (a y) / real_of_int (2 * B)
                    < real (nth_prime (y + 1)))"
         by auto
       obtain m where "n<m" "c m \<le> c n" "c n<c (m+1)" 
       proof -
         have "\<exists>N. N > n \<and> c N > c n"
           using c_ubound[rule_format, of "MAX x\<in>{..n}. c x"] 
           by (metis Max_ge atMost_iff dual_order.trans finite_atMost finite_imageI image_eqI 
               linorder_not_le order_refl)
         then obtain N where "N>n" "c N>c n" by auto
         define A m where "A={m. n<m \<and> (m+1)\<le>N \<and> c (m+1) > c n}" and "m = Min A"
         have "finite A" unfolding A_def
           by (metis (no_types, lifting) A_def add_leE finite_nat_set_iff_bounded_le mem_Collect_eq)
         moreover have "N-1\<in>A" unfolding A_def 
           using \<open>c n < c N\<close> \<open>n < N\<close> \<open>c (n + 1) = c n\<close>
           by (smt Suc_diff_Suc Suc_eq_plus1 Suc_leI Suc_pred  add.commute 
               add_diff_inverse_nat add_leD1 diff_is_0_eq' mem_Collect_eq nat_add_left_cancel_less
               zero_less_one)
         ultimately have "m\<in>A"
           using Min_in unfolding m_def by auto
         then have "n<m"  "c n<c (m+1)" "m>0"
           unfolding m_def A_def by auto
         moreover have "c m \<le> c n"
         proof (rule ccontr)
           assume " \<not> c m \<le> c n"
           then have "m-1\<in>A" using \<open>m\<in>A\<close> \<open>c (n + 1) = c n\<close>
             unfolding A_def 
             by auto (smt One_nat_def Suc_eq_plus1 Suc_lessI less_diff_conv)
           from  Min_le[OF \<open>finite A\<close> this,folded m_def] \<open>m>0\<close> show False by auto
         qed
         ultimately show ?thesis using that[of m] by auto
       qed
       have "(1 + 1 / (2 * B)) * nth_prime m < nth_prime m + a m / (2*B)"
       proof -
         have "nth_prime m < a m"
         proof -
           have "B * int (nth_prime m) < c m * (a m - 1)"
             using Bc_eq[rule_format,of m] \<open>c m \<le> c n\<close> \<open>c n < c (m + 1)\<close> \<open>n < m\<close> 
             by (auto simp:algebra_simps)
           also have "... \<le> c n * (a m - 1)"
             by (simp add: \<open>c m \<le> c n\<close> a_pos mult_right_mono)
           finally have "B * int (nth_prime m) < c n * (a m - 1)" .
           moreover have "c n\<le>B" 
           proof -
             have " B * int (nth_prime n) = c n * (a n - 1)" "B < int (nth_prime n)"
               and c_a:"\<bar>real_of_int (c (n + 1))\<bar> < real_of_int (a n) / 2"
               using Bc_eq[rule_format,of n] \<open>c (n + 1) = c n\<close> by (auto simp:algebra_simps)
             from this(1) have " c n dvd (B * int (nth_prime n))"
               by simp
             moreover have "coprime (c n) (int (nth_prime n))"
             proof -
               have "c n < int (nth_prime n)" 
               proof (rule ccontr)
                 assume "\<not> c n < int (nth_prime n)"
                 then have asm:"c n \<ge> int (nth_prime n)" by auto
                 then have "a n > 2 * nth_prime n"
                   using c_a \<open>c (n + 1) = c n\<close> by auto
                 then have "a n -1 \<ge> 2 * nth_prime n"
                   by simp
                 then have "a n - 1 > 2 * B"
                   using \<open>B < int (nth_prime n)\<close> by auto
                 from mult_le_less_imp_less[OF asm this] \<open>B>0\<close>
                 have "int (nth_prime n) * (2 * B) < c n * (a n - 1)"
                   by auto
                 then show False using \<open>B * int (nth_prime n) = c n * (a n - 1)\<close>
                   by (smt \<open>0 < B\<close> \<open>B < int (nth_prime n)\<close> combine_common_factor 
                       mult.commute mult_pos_pos)
               qed
               then have "\<not> nth_prime n dvd c n" 
                 by (simp add: Bc_eq zdvd_not_zless)
               then have "coprime (int (nth_prime n)) (c n)" 
                 by (auto intro!:prime_imp_coprime_int)
               then show ?thesis using coprime_commute by blast
             qed
             ultimately have "c n dvd B"
               using coprime_dvd_mult_left_iff by auto
             then show ?thesis using \<open>0 < B\<close> zdvd_imp_le by blast
           qed
           moreover have "c n > 0 " using Bc_eq by blast
           ultimately show ?thesis
             using \<open>B>0\<close> by (smt a_pos mult_mono)
         qed
         then show ?thesis using \<open>B>0\<close> by (auto simp:field_simps)
       qed
       also have "... < nth_prime (m+1)"
         using Bc_eq[rule_format, of m] \<open>n<m\<close> \<open>c m \<le> c n\<close> \<open>c n < c (m+1)\<close>
         by linarith
       finally show "\<exists>j>n. (1 + 1 / real_of_int (2 * B)) * real (nth_prime j)
                        < real (nth_prime (j + 1))" using \<open>m>n\<close> by auto
     qed
     then have "\<exists>\<^sub>F m in sequentially. nth_prime (m+1)/nth_prime m > (1+1/(2*B))"
       by (auto elim:frequently_elim1 simp:field_simps)
     moreover have "\<forall>\<^sub>F m in sequentially. nth_prime (m+1)/nth_prime m < (1+1/(2*B))"
       using ratio_of_consecutive_primes[unfolded tendsto_iff,rule_format,of "1/(2*B)"]
         \<open>B>0\<close>
       unfolding dist_real_def
       by (auto elim!:eventually_mono simp:algebra_simps)
     ultimately show False by (simp add: eventually_mono frequently_def)
   qed
 
   have c_gt_half:"\<forall>\<^sub>F N in sequentially. card {n\<in>{N..<2*N}.  c n > c (n+1)} > N / 2"
   proof -
     define h where "h=(\<lambda>n. (nth_prime (2*n) - nth_prime n) 
                               /  sqrt (nth_prime n))"
     have "\<forall>\<^sub>F n in sequentially. h n < n / 2"
     proof -
       have "\<forall>\<^sub>F n in sequentially. h n < n powr (5/6)"
         using nth_prime_double_sqrt_less[of "1/3"]
         unfolding h_def by auto
       moreover have "\<forall>\<^sub>F n in sequentially. n powr (5/6) < (n /2)"
         by real_asymp
       ultimately show ?thesis 
         by eventually_elim auto 
     qed
     moreover have "\<forall>\<^sub>F n in sequentially. sqrt (nth_prime n) / a n < 1 / (2*B)"
       using nth_1[THEN tendsto_real_sqrt,unfolded tendsto_iff
           ,rule_format,of "1/(2*B)"] \<open>B>0\<close> a_pos
       by (auto simp:real_sqrt_divide abs_of_pos)
     ultimately have "\<forall>\<^sub>F x in sequentially. c (x+1) \<noteq> c x
         \<and> sqrt (nth_prime x) / a x < 1 / (2*B)
         \<and>  h x < x / 2
         \<and> (c (x+1)>c x \<longrightarrow> nth_prime (x+1) > nth_prime x +  a x / (2* B))"
       using c_neq_large B_nth_prime eq_2_11[of "1-1/ sqrt 2",simplified]
       by eventually_elim (auto simp:divide_simps)
     then show ?thesis
     proof (elim eventually_at_top_mono)
       fix N assume "N\<ge>1" and N_asm:"\<forall>y\<ge>N. c (y + 1) \<noteq> c y \<and>
                sqrt (real (nth_prime y)) / real_of_int (a y)
                < 1 / real_of_int (2 * B) \<and>  h y < y / 2 \<and>
                (c y < c (y + 1) \<longrightarrow>
                 real (nth_prime y) + real_of_int (a y) / real_of_int (2 * B)
                 < real (nth_prime (y + 1)))"
 
       define S where "S={n \<in> {N..<2 * N}. c n < c (n + 1)}"
       define g where "g=(\<lambda>n. (nth_prime (n+1) - nth_prime n) 
                               /  sqrt (nth_prime n))"
       define f where "f=(\<lambda>n. nth_prime (n+1) - nth_prime n)"
       have g_gt_1:"g n>1" when "n\<ge>N" "c n < c (n + 1)" for n
       proof -
         have "nth_prime n + sqrt (nth_prime n) < nth_prime (n+1)"
         proof -
           have "nth_prime n + sqrt (nth_prime n) < nth_prime n + a n / (2*B)"
             using N_asm[rule_format,OF \<open>n\<ge>N\<close>] a_pos
             by (auto simp:field_simps)
           also have "... < nth_prime (n+1)"
             using N_asm[rule_format,OF \<open>n\<ge>N\<close>] \<open>c n < c (n + 1)\<close> by auto
           finally show ?thesis .
         qed
         then show ?thesis unfolding g_def 
           using \<open>c n < c (n + 1)\<close> by auto
       qed
       have g_geq_0:"g n \<ge> 0" for n 
         unfolding g_def  by auto
 
       have "finite S" "\<forall>x\<in>S. x\<ge>N \<and> c x<c (x+1)"
         unfolding S_def by auto
       then have "card S \<le> sum g S" 
       proof (induct S)
         case empty
         then show ?case by auto
       next
         case (insert x F)
         moreover have "g x>1" 
         proof -
           have "c x < c (x+1)" "x\<ge>N" using insert(4) by auto
           then show ?thesis using g_gt_1 by auto
         qed
         ultimately show ?case by simp
       qed
       also have "... \<le> sum g {N..<2*N}"
         apply (rule sum_mono2)
         unfolding S_def using g_geq_0 by auto
       also have "... \<le> sum (\<lambda>n. f n/sqrt (nth_prime N)) {N..<2*N}"
         unfolding f_def g_def by (auto intro!:sum_mono divide_left_mono)
       also have "... = sum f {N..<2*N} / sqrt (nth_prime N)"
         unfolding sum_divide_distrib[symmetric] by auto
       also have "... = (nth_prime (2*N) - nth_prime N) / sqrt (nth_prime N)"
       proof -
         have "sum f {N..<2 * N} = nth_prime (2 * N) - nth_prime N"   
         proof (induct N)
           case 0
           then show ?case by simp
         next
           case (Suc N)
           have ?case if "N=0"
           proof -
             have "sum f {Suc N..<2 * Suc N} = sum f {1}"
               using that by (simp add: numeral_2_eq_2)
             also have "... = nth_prime 2 - nth_prime 1"
               unfolding f_def by (simp add:numeral_2_eq_2)
             also have "... = nth_prime (2 * Suc N) - nth_prime (Suc N)"
               using that by auto
             finally show ?thesis .
           qed
           moreover have ?case if "N\<noteq>0"
           proof -
             have "sum f {Suc N..<2 * Suc N} = sum f {N..<2 * Suc N} - f N"
               apply (subst (2) sum.atLeast_Suc_lessThan)
               using that by auto
             also have "... = sum f {N..<2 * N}+ f (2*N) + f(2*N+1) - f N"
               by auto
             also have "... = nth_prime (2 * Suc N) - nth_prime (Suc N)"
               using Suc unfolding f_def by auto
             finally show ?thesis .
           qed
           ultimately show ?case by blast
         qed
         then show ?thesis by auto
       qed
       also have "... = h N"
         unfolding h_def by auto
       also have "... < N/2"
         using N_asm by auto
       finally have "card S < N/2" .
 
       define T where "T={n \<in> {N..<2 * N}. c n > c (n + 1)}"
       have "T \<union> S = {N..<2 * N}" "T \<inter> S = {}" "finite T"
         unfolding T_def S_def using N_asm by fastforce+
 
       then have "card T + card S = card {N..<2 * N}"
         using card_Un_disjoint \<open>finite S\<close> by metis
       also have "... = N"
         by simp
       finally have "card T + card S = N" .
       with \<open>card S < N/2\<close> 
       show "card T > N/2" by linarith
     qed
   qed
 
   text\<open>Inequality (3.5) in the original paper required a slight modification: \<close>
 
   have a_gt_plus:"\<forall>\<^sub>F n in sequentially. c n > c (n+1) \<longrightarrow>a (n+1) > a n + (a n - c(n+1) - 1) / c (n+1)"
   proof -
     note a_gt_1[THEN eventually_all_ge_at_top] c_pos[THEN eventually_all_ge_at_top]
     moreover have "\<forall>\<^sub>F n in sequentially. 
               B * int (nth_prime (n+1)) = c (n+1) * a (n+1) - c (n + 2)"
       using Bc_large 
       apply (subst (asm) eventually_sequentially_Suc[symmetric])
       by (auto elim:eventually_mono)
     moreover have "\<forall>\<^sub>F n in sequentially. 
                         B * int (nth_prime n) = c n * a n - c (n + 1) \<and> \<bar>c (n + 1)\<bar> <  a n / 2"
       using Bc_large by (auto elim:eventually_mono)
     ultimately show ?thesis 
       apply (eventually_elim)
     proof (rule impI)
       fix n 
       assume "\<forall>y\<ge>n. 1 < a y" "\<forall>y\<ge>n. 0 < c y"
         and
         Suc_n_eq:"B * int (nth_prime (n + 1)) = c (n + 1) * a (n + 1) - c (n + 2)" and
         "B * int (nth_prime n) = c n * a n - c (n + 1) \<and>
                 real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2" 
         and "c (n + 1) < c n"
       then have n_eq:"B * int (nth_prime n) = c n * a n - c (n + 1)" and 
         c_less_a: "real_of_int \<bar>c (n + 1)\<bar> < real_of_int (a n) / 2" 
         by auto
       from \<open>\<forall>y\<ge>n. 1 < a y\<close> \<open>\<forall>y\<ge>n. 0 < c y\<close> 
       have *:"a n>1" "a (n+1) > 1" "c n > 0" 
         "c (n+1) > 0"  "c (n+2) > 0"
         by auto
       then have "(1+1/c (n+1))* (a n - 1)/a (n+1) = (c (n+1)+1) * ((a n - 1) / (c (n+1) * a (n+1)))"
         by (auto simp:field_simps)
       also have "... \<le> c n * ((a n - 1) / (c (n+1) * a (n+1)))"
         apply (rule mult_right_mono)
         subgoal using \<open>c (n + 1) < c n\<close> by auto
         subgoal by (smt \<open>0 < c (n + 1)\<close> a_pos divide_nonneg_pos mult_pos_pos of_int_0_le_iff 
               of_int_0_less_iff)
         done
       also have "... = (c n * (a n - 1)) / (c (n+1) * a (n+1))" by auto
       also have "... < (c n * (a n - 1)) / (c (n+1) * a (n+1)  - c (n+2))"
         apply (rule divide_strict_left_mono)
         subgoal using \<open>c (n+2) > 0\<close> by auto
         unfolding Suc_n_eq[symmetric] using * \<open>B>0\<close> by auto
       also have "... < (c n * a n - c (n+1)) / (c (n+1) * a (n+1)  - c (n+2))"
         apply (rule frac_less)
         unfolding Suc_n_eq[symmetric] using * \<open>B>0\<close> \<open>c (n + 1) < c n\<close> 
         by (auto simp:algebra_simps)
       also have "... = nth_prime n / nth_prime (n+1)"
         unfolding Suc_n_eq[symmetric] n_eq[symmetric] using \<open>B>0\<close> by auto
       also have "... < 1" by auto
       finally have "(1 + 1 / real_of_int (c (n + 1))) * real_of_int (a n - 1) 
         / real_of_int (a (n + 1)) < 1 " .
       then show "a n + (a n - c (n + 1) - 1) /  (c (n + 1)) < (a (n + 1))"
         using * by (auto simp:field_simps)
     qed
   qed
   have a_gt_1:"\<forall>\<^sub>F n in sequentially. c n > c (n+1) \<longrightarrow> a (n+1) > a n + 1"
     using Bc_large a_gt_plus c_pos[THEN eventually_all_ge_at_top]
     apply eventually_elim
   proof (rule impI)
     fix n assume  
       "c (n + 1) < c n \<longrightarrow> a n +  (a n - c (n + 1) - 1) / c (n + 1) <  a (n + 1)" 
       "c (n + 1) < c n" and B_eq:"B * int (nth_prime n) = c n * a n - c (n + 1) \<and>
          \<bar>real_of_int (c (n + 1))\<bar> < real_of_int (a n) / 2" and c_pos:"\<forall>y\<ge>n. 0 < c y"
     from this(1,2) 
     have "a n +  (a n - c (n + 1) - 1) / c (n + 1) <  a (n + 1)" by auto
     moreover have "a n - 2 * c (n+1) > 0"
       using B_eq c_pos[rule_format,of "n+1"] by auto
     then have "a n - 2 * c (n+1) \<ge> 1" by simp
     then have "(a n - c (n + 1) - 1) / c (n + 1) \<ge> 1"
       using c_pos[rule_format,of "n+1"] by (auto simp:field_simps)
     ultimately show "a n + 1 < a (n + 1)" by auto
   qed
 
   text\<open>The following corresponds to inequality (3.6) in the paper, which had to be
         slightly corrected:  \<close>
 
   have a_gt_sqrt:"\<forall>\<^sub>F n in sequentially. c n > c (n+1) \<longrightarrow> a (n+1) > a n + (sqrt n - 2)"
   proof -
     have a_2N:"\<forall>\<^sub>F N in sequentially. a (2*N) \<ge> N /2 +1" 
       using c_gt_half a_gt_1[THEN eventually_all_ge_at_top] 
     proof eventually_elim
       case (elim N)
       define S where "S={n \<in> {N..<2 * N}. c (n + 1) < c n}"
       define f where "f = (\<lambda>n. a (Suc n) - a n)"
 
       have f_1:"\<forall>x\<in>S. f x\<ge>1" and f_0:"\<forall>x. f x\<ge>0"
         subgoal using elim unfolding S_def f_def by auto
         subgoal using \<open>mono a\<close>[THEN incseq_SucD] unfolding f_def by auto
         done
       have "N / 2 < card S" 
         using elim unfolding S_def by auto
       also have "... \<le> sum f S" 
         unfolding of_int_sum
         apply (rule sum_bounded_below[of _ 1,simplified])
         using f_1 by auto
       also have "... \<le> sum f {N..<2 * N}" 
         unfolding of_int_sum
         apply (rule sum_mono2)
         unfolding S_def using f_0 by auto
       also have "... = a (2*N) - a N" 
         unfolding of_int_sum f_def of_int_diff
         apply (rule sum_Suc_diff')
         by auto
       finally have "N / 2 < a (2*N) - a N" .
       then show ?case using a_pos[rule_format,of N] by linarith
     qed
 
     have a_n4:"\<forall>\<^sub>F n in sequentially. a n > n/4" 
     proof -
       obtain N where a_N:"\<forall>n\<ge>N. a (2*n) \<ge> n /2+1"
         using a_2N unfolding eventually_at_top_linorder by auto
       have "a n>n/4" when "n\<ge>2*N" for n 
       proof -
         define n' where "n'=n div 2"
         have "n'\<ge>N" unfolding n'_def using that by auto
         have "n/4 < n' /2+1"
           unfolding n'_def by auto
         also have "... \<le> a (2*n')"
           using a_N \<open>n'\<ge>N\<close> by auto
         also have "... \<le>a n" unfolding n'_def
           apply (cases "even n")
           subgoal by simp
           subgoal by (simp add: assms(2) incseqD)
           done
         finally show ?thesis .
       qed
       then show ?thesis
         unfolding eventually_at_top_linorder by auto
     qed
 
     have c_sqrt:"\<forall>\<^sub>F n in sequentially. c n < sqrt n / 4"
     proof -
       have "\<forall>\<^sub>F x in sequentially. x>1" by simp
       moreover have "\<forall>\<^sub>F x in sequentially. real (nth_prime x) / (real x * ln (real x)) < 2"
         using nth_prime_asymptotics[unfolded asymp_equiv_def,THEN order_tendstoD(2),of 2]
         by simp
       ultimately have "\<forall>\<^sub>F n in sequentially. c n < B*8 *ln n + 1" using a_n4 Bc_large
       proof eventually_elim
         case (elim n)
         from this(4) have "c n=(B*nth_prime n+c (n+1))/a n"
           using a_pos[rule_format,of n] 
           by (auto simp:divide_simps)
         also have "... = (B*nth_prime n)/a n+c (n+1)/a n"
           by (auto simp:divide_simps)
         also have "... < (B*nth_prime n)/a n + 1"
         proof -
           have "c (n+1)/a n < 1" using elim(4) by auto
           then show ?thesis by auto
         qed
         also have "... < B*8 * ln n + 1"
         proof -
           have "B*nth_prime n < 2*B*n*ln n"
             using \<open>real (nth_prime n) / (real n * ln (real n)) < 2\<close> \<open>B>0\<close> \<open> 1 < n\<close> 
             by (auto simp:divide_simps)
           moreover have "real n / 4 < real_of_int (a n)" by fact
           ultimately have "(B*nth_prime n) / a n < (2*B*n*ln n) / (n/4)"
             apply (rule_tac frac_less)
             using \<open>B>0\<close> \<open> 1 < n\<close>  by auto
           also have "... = B*8 * ln n"
             using \<open> 1 < n\<close> by auto
           finally show ?thesis by auto
         qed
         finally show ?case .
       qed
       moreover have "\<forall>\<^sub>F n in sequentially. B*8 *ln n + 1 < sqrt n / 4"
         by real_asymp
       ultimately show ?thesis 
         by eventually_elim auto
     qed
 
     have 
       "\<forall>\<^sub>F n in sequentially. 0 < c (n+1)"
       "\<forall>\<^sub>F n in sequentially. c (n+1) < sqrt (n+1) / 4"
       "\<forall>\<^sub>F n in sequentially. n > 4"
       "\<forall>\<^sub>F n in sequentially. (n - 4) / sqrt (n + 1) + 1 > sqrt n"
       subgoal using c_pos[THEN eventually_all_ge_at_top]    
         by eventually_elim auto
       subgoal using  c_sqrt[THEN eventually_all_ge_at_top] 
         by eventually_elim (use le_add1 in blast)
       subgoal by simp
       subgoal 
         by real_asymp
       done
     then show ?thesis using a_gt_plus a_n4
       apply eventually_elim
     proof (rule impI)
       fix n assume asm:"0 < c (n + 1)" "c (n + 1) < sqrt (real (n + 1)) / 4" and
         a_ineq:"c (n + 1) < c n \<longrightarrow> a n +  (a n - c (n + 1) - 1) /  c (n + 1) < a (n + 1)" 
         "c (n + 1) < c n"  and "n / 4 < a n" "n > 4" 
         and n_neq:" sqrt (real n) < real (n - 4) / sqrt (real (n + 1)) + 1"
 
       have "(n-4) / sqrt(n+1) = (n/4 - 1)/ (sqrt (real (n + 1)) / 4)"
         using \<open>n>4\<close> by (auto simp:divide_simps)
       also have "... < (a n - 1) /  c (n + 1)" 
         apply (rule frac_less)
         using \<open>n > 4\<close> \<open>n / 4 < a n\<close> \<open>0 < c (n + 1)\<close> \<open>c (n + 1) < sqrt (real (n + 1)) / 4\<close>
         by auto
       also have "... - 1 = (a n - c (n + 1) - 1) /  c (n + 1)"
         using \<open>0 < c (n + 1)\<close> by (auto simp:field_simps)
       also have "a n + ... < a (n+1)"
         using a_ineq by auto
       finally have "a n + ((n - 4) / sqrt (n + 1) - 1) < a (n + 1)" by simp
       moreover have "(n - 4) / sqrt (n + 1) - 1 > sqrt n - 2"
         using n_neq[THEN diff_strict_right_mono,of 2] \<open>n>4\<close> 
         by (auto simp:algebra_simps of_nat_diff) 
       ultimately show "real_of_int (a n) + (sqrt (real n) - 2) < real_of_int (a (n + 1))"
         by argo
     qed
   qed
 
   text\<open>The following corresponds to inequality $ a_{2N} > N^{3/2}/2$ in the paper,
  which had to be slightly corrected: \<close>
 
   have a_2N_sqrt:"\<forall>\<^sub>F N in sequentially. a (2*N) >  real N * (sqrt (real N)/2 - 1)"
     using c_gt_half a_gt_sqrt[THEN eventually_all_ge_at_top] eventually_gt_at_top[of 4]
   proof eventually_elim
     case (elim N)
     define S where "S={n \<in> {N..<2 * N}. c (n + 1) < c n}"
     define f where "f = (\<lambda>n. a (Suc n) - a n)"
 
     have f_N:"\<forall>x\<in>S. f x\<ge>sqrt N - 2"
     proof 
       fix x assume "x\<in>S"
       then have "sqrt (real x) - 2 < f x" "x\<ge>N"
         using elim unfolding S_def f_def by auto
       moreover have "sqrt x - 2 \<ge> sqrt N - 2"
         using \<open>x\<ge>N\<close> by simp
       ultimately show  "sqrt (real N) - 2 \<le> real_of_int (f x)" by argo
     qed
     have f_0:"\<forall>x. f x\<ge>0"
       using \<open>mono a\<close>[THEN incseq_SucD] unfolding f_def by auto
 
     have "(N / 2)  * (sqrt N - 2) < card S * (sqrt N - 2)" 
       apply (rule mult_strict_right_mono)
       subgoal using elim unfolding S_def by auto
       subgoal using \<open>N>4\<close> 
         by (metis diff_gt_0_iff_gt numeral_less_real_of_nat_iff real_sqrt_four real_sqrt_less_iff)
       done
     also have "...  \<le> sum f S" 
       unfolding of_int_sum
       apply (rule sum_bounded_below)
       using f_N by auto
     also have "... \<le> sum f {N..<2 * N}" 
       unfolding of_int_sum
       apply (rule sum_mono2)
       unfolding S_def using f_0 by auto
     also have "... = a (2*N) - a N" 
       unfolding of_int_sum f_def of_int_diff
       apply (rule sum_Suc_diff')
       by auto
     finally have "real N / 2 * (sqrt (real N) - 2) < real_of_int (a (2 * N) - a N)" 
       .              
     then have "real N / 2 * (sqrt (real N) - 2) < a (2 * N)"
       using a_pos[rule_format,of N] by linarith
     then show ?case by (auto simp:field_simps)
   qed
 
   text\<open>The following part is required to derive the final contradiction of the proof.\<close>
 
   have a_n_sqrt:"\<forall>\<^sub>F n in sequentially. a n > (((n-1)/2) powr (3/2) - (n-1)) /2"
   proof (rule sequentially_even_odd_imp)
     define f where "f=(\<lambda>N. ((real (2 * N - 1) / 2) powr (3 / 2) - real (2 * N - 1)) / 2)"
     define g where "g=(\<lambda>N. real N * (sqrt (real N) / 2 - 1))"
     have "\<forall>\<^sub>F N in sequentially. g N > f N"
       unfolding f_def g_def
       by real_asymp
     moreover have "\<forall>\<^sub>F N in sequentially. a (2 * N) > g N"
       unfolding g_def using a_2N_sqrt .
     ultimately show "\<forall>\<^sub>F N in sequentially. f N < a (2 * N)"
       by eventually_elim auto
   next
     define f where "f=(\<lambda>N. ((real (2 * N + 1 - 1) / 2) powr (3 / 2) 
                                   - real (2 * N + 1 - 1)) / 2)"
     define g where "g=(\<lambda>N. real N * (sqrt (real N) / 2 - 1))"
     have "\<forall>\<^sub>F N in sequentially. g N = f N"
       using eventually_gt_at_top[of 0]
       apply eventually_elim
       unfolding f_def g_def
       by (auto simp:algebra_simps powr_half_sqrt[symmetric] powr_mult_base)
     moreover have "\<forall>\<^sub>F N in sequentially. a (2 * N) > g N"
       unfolding g_def using a_2N_sqrt .
     moreover have "\<forall>\<^sub>F N in sequentially. a (2 * N + 1) \<ge> a (2*N)"
       apply (rule eventuallyI)
       using \<open>mono a\<close> by (simp add: incseqD)
     ultimately show "\<forall>\<^sub>F N in sequentially. f N < (a (2 * N + 1))"
       by eventually_elim auto
   qed
 
   have a_nth_prime_gt:"\<forall>\<^sub>F n in sequentially. a n / nth_prime n > 1"
   proof -
     define f where "f=(\<lambda>n::nat. (((n-1)/2) powr (3/2) - (n-1)) /2)"
     have "\<forall>\<^sub>F x in sequentially. real (nth_prime x) / (real x * ln (real x)) < 2"
       using nth_prime_asymptotics[unfolded asymp_equiv_def,THEN order_tendstoD(2),of 2]
       by simp
     from this eventually_gt_at_top[of 1]
     have "\<forall>\<^sub>F n in sequentially. real (nth_prime n)   < 2*(real n * ln n)"
       by eventually_elim (auto simp:field_simps)
     moreover have *:"\<forall>\<^sub>F N in sequentially. f N >0 "
       unfolding f_def
       by real_asymp
     moreover have " \<forall>\<^sub>F n in sequentially. f n < a n"
       using a_n_sqrt unfolding f_def .
     ultimately have "\<forall>\<^sub>F n in sequentially. a n / nth_prime n 
                     > f n / (2*(real n * ln n))"
       apply eventually_elim
       apply (rule frac_less2)
       by auto
     moreover have "\<forall>\<^sub>F n in sequentially.
         (f n)/ (2*(real n * ln n)) > 1"
       unfolding f_def 
       by real_asymp
     ultimately show ?thesis 
       by eventually_elim argo
   qed
 
   have a_nth_prime_lt:"\<exists>\<^sub>F n in sequentially. a n / nth_prime n < 1"
   proof -
     have "liminf (\<lambda>x. a x / nth_prime x) < 1"
       using nth_2 by auto
     from this[unfolded less_Liminf_iff]
     show ?thesis
       apply (auto elim!:frequently_elim1)
       by (meson divide_less_eq_1 ereal_less_eq(7) leD leI 
           nth_prime_nonzero of_nat_eq_0_iff of_nat_less_0_iff order.trans)
   qed
 
   from a_nth_prime_gt a_nth_prime_lt show False 
     by (simp add: eventually_mono frequently_def) 
 qed
 
 section\<open>Acknowledgements\<close>
 
 text\<open>A.K.-A. and W.L. were supported by the ERC Advanced Grant ALEXANDRIA (Project 742178)
  funded by the European Research Council and led by Professor Lawrence Paulson
  at the University of Cambridge, UK.\<close>
 
 end
\ No newline at end of file
diff --git a/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy b/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy
--- a/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy
+++ b/thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy
@@ -1,1066 +1,1062 @@
 (*
   File: Irrationality_J_Hancl.thy
   Authors:  Angeliki Koutsoukou-Argyraki and Wenda Li,
             Computer Laboratory, University of Cambridge, UK.
   Email: ak2110@cam.ac.uk, wl302@cam.ac.uk  
 *)
 
 section \<open>Irrational Rapidly Convergent Series\<close>
 theory Irrationality_J_Hancl
   imports "HOL-Analysis.Analysis" "HOL-Decision_Procs.Approximation"
 begin
 
 text \<open>This is the formalisation of a proof by J. Hancl, in particular of the proof of his Theorem 3 in
 the paper: Irrational Rapidly Convergent Series, Rend. Sem. Mat. Univ. Padova, Vol 107 (2002).
 
 The statement asserts the irrationality of the sum of a series consisting of rational numbers
 defined using sequences that fulfill certain properties. Even though the statement
 is number-theoretic, the proof uses only arguments from introductory Analysis.\<close>
 
 text \<open>We show the central result (theorem Hancl3) by proof by contradiction, by making use of some of 
  the auxiliary lemmas. To this end, assuming that the sum is a rational number, for a quantity 
  $\textrm{ALPHA}(n)$ we show that $\textrm{ALPHA}(n) \geq 1$ for all $n \in \mathbb{N}$. After that we show that we can find an 
   $n \in \mathbb{N}$ for which $\textrm{ALPHA}(n) < 1$ which yields a contradiction and we thus conclude that the 
   sum of the series is a rational number. We finally give an immediate application of theorem Hancl3
  for a specific series (corollary Hancl3corollary, requiring lemma
  summable\_ln\_plus) which corresponds to Corollary 2 in the original
 paper by J. Hancl. 
 \<close>
 
 hide_const floatarith.Max
 
 subsection \<open>Misc\<close>
 
 lemma filterlim_sequentially_iff:
   "filterlim f F1 sequentially \<longleftrightarrow> filterlim (\<lambda>x. f (x+k)) F1 sequentially"
   unfolding filterlim_iff
   apply (subst eventually_sequentially_seg)
   by auto
 
 lemma filterlim_realpow_sequentially_at_top:
   "(x::real) > 1 \<Longrightarrow> filterlim ((^) x) at_top sequentially"
   apply (rule LIMSEQ_divide_realpow_zero[THEN filterlim_inverse_at_top,of _ 1,simplified])
   by auto
 
 lemma filterlim_at_top_powr_real:
   fixes g::"'b \<Rightarrow> real"
   assumes "filterlim f at_top F" "(g \<longlongrightarrow> g') F" "g'>1"
   shows "filterlim (\<lambda>x. g x powr f x) at_top F"
 proof -
   have "filterlim (\<lambda>x. ((g'+1)/2) powr f x) at_top F" 
   proof (subst filterlim_at_top_gt[of _ _ 1],rule+)
     fix Z assume "Z>(1::real)"
     have "\<forall>\<^sub>F x in F. ln Z \<le> ln (((g' + 1) / 2) powr f x)"
       using assms(1)[unfolded filterlim_at_top,rule_format,of "ln Z / ln ((g' + 1) / 2)"]
       apply (eventually_elim)
       using \<open>g'>1\<close> by (auto simp:ln_powr divide_simps)
     then show "\<forall>\<^sub>F x in F. Z \<le> ((g' + 1) / 2) powr f x"
       apply (eventually_elim)
       apply (subst (asm) ln_le_cancel_iff)
       using \<open>Z>1\<close> \<open>g'>1\<close> by auto
   qed
   moreover have "\<forall>\<^sub>F x in F. ((g'+1)/2) powr f x \<le> g x powr f x" 
   proof -
     have "\<forall>\<^sub>F x in F. g x > (g'+1)/2"
       apply (rule order_tendstoD[OF assms(2)])
       using \<open>g'>1\<close> by auto
     moreover have "\<forall>\<^sub>F x in F. f x>0" 
       using assms(1)[unfolded filterlim_at_top_dense,rule_format,of 0] .
     ultimately show ?thesis
       apply eventually_elim
       using \<open>g'>1\<close> by (auto intro!: powr_mono2)
   qed
   ultimately show ?thesis using filterlim_at_top_mono by fast
 qed
 
 lemma powrfinitesum:
   fixes a::real and s::nat assumes  "s \<le> n"
   shows " (\<Prod>j=s..(n::nat).(a powr (2^j)))  = a powr (\<Sum>j=s..(n::nat).(2^j)) "
   using \<open>s \<le> n\<close> 
 proof(induct n)
   case 0
   then show ?case by auto
 next
   case (Suc n)
   have ?case when "s\<le>n" using Suc.hyps 
     by (metis Suc.prems add.commute linorder_not_le powr_add prod.nat_ivl_Suc' sum.cl_ivl_Suc that)
   moreover have ?case when "s=Suc n"   
   proof-
     have "(\<Prod>j = s..Suc n. a powr 2 ^ j) =(a powr 2 ^(Suc n))  " 
       using \<open>s=Suc n\<close> by simp
     also have "(a powr 2 ^(Suc n) ) =  a powr sum ((^) 2) {s..Suc n}   " using that by auto
     ultimately show " (\<Prod>j = s..Suc n. a powr 2 ^ j) = a powr sum ((^) 2) {s..Suc n}"
       using \<open>s\<le>Suc n\<close> by linarith
   qed
   ultimately show ?case using \<open>s\<le>Suc n\<close> by linarith
 qed
 
 lemma summable_ratio_test_tendsto:
   fixes f :: "nat \<Rightarrow> 'a::banach"
   assumes "c < 1" and "\<forall>n. f n\<noteq>0" and "(\<lambda>n. norm (f (Suc n)) / norm (f n)) \<longlonglongrightarrow> c"
   shows "summable f"
 proof -
   obtain N where N_dist:"\<forall>n\<ge>N. dist (norm (f (Suc n)) / norm (f n)) c < (1-c)/2"
     using assms unfolding tendsto_iff eventually_sequentially 
     by (meson diff_gt_0_iff_gt zero_less_divide_iff zero_less_numeral)
   have "norm (f (Suc n)) / norm (f n) \<le> (1+c)/2" when "n\<ge>N" for n
     using N_dist[rule_format,OF that] \<open>c<1\<close> 
     apply (auto simp add:field_simps dist_norm)
     by argo
   then have "norm (f (Suc n))  \<le> (1+c)/2 * norm (f n)" when "n\<ge>N" for n
     using that assms(2)[rule_format, of n] by (auto simp add:divide_simps)
   moreover have "(1+c)/2 < 1" using \<open>c<1\<close> by auto 
   ultimately show ?thesis
     using summable_ratio_test[of _ N f] by blast
 qed
 
 lemma summable_ln_plus:
   fixes f::"nat \<Rightarrow> real" 
   assumes "summable f" "\<forall>n. f n>0"
   shows "summable (\<lambda>n. ln (1+f n))"
 proof (rule summable_comparison_test_ev[OF _ assms(1)])
   have "ln (1 + f n) > 0" for n by (simp add: assms(2) ln_gt_zero)
   moreover have "ln (1 + f n) \<le> f n" for n 
     apply (rule ln_add_one_self_le_self2)
     using assms(2)[rule_format,of n] by auto 
   ultimately show "\<forall>\<^sub>F n in sequentially. norm (ln (1 + f n)) \<le> f n"
     by (auto intro!: eventuallyI simp add:less_imp_le) 
 qed
 
 lemma suminf_real_offset_le:
   fixes f :: "nat \<Rightarrow> real"
   assumes f: "\<And>i. 0 \<le> f i" and "summable f"
   shows "(\<Sum>i. f (i + k)) \<le> suminf f"
 proof -
   have "(\<lambda>n. \<Sum>i<n. f (i + k)) \<longlonglongrightarrow> (\<Sum>i. f (i + k))"
     using summable_sums[OF \<open>summable f\<close>] 
     by (simp add: assms(2) summable_LIMSEQ summable_ignore_initial_segment)
   moreover have "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
     using summable_sums[OF \<open>summable f\<close>] by (simp add: sums_def atLeast0LessThan f)
   then have "(\<lambda>n. \<Sum>i<n + k. f i) \<longlonglongrightarrow> (\<Sum>i. f i)"
     by (rule LIMSEQ_ignore_initial_segment)
   ultimately show ?thesis
   proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
     fix n assume "k \<le> n"
     have "(\<Sum>i<n. f (i + k)) = (\<Sum>i<n. (f \<circ> (\<lambda>i. i + k)) i)"
       by simp
     also have "\<dots> = (\<Sum>i\<in>(\<lambda>i. i + k) ` {..<n}. f i)"
       by (subst sum.reindex) auto
     also have "\<dots> \<le> sum f {..<n + k}"
       by (intro sum_mono2) (auto simp: f)
     finally show "(\<Sum>i<n. f (i + k)) \<le> sum f {..<n + k}" .
   qed
 qed
 
 
 
 lemma factt:
   fixes s n ::nat assumes "s \<le> n" 
   shows " (\<Sum>i=s..n. 2^i) < (2^(n+1) :: real) " using assms
 proof (induct n)
   case 0
   show ?case by  auto 
 next
   case (Suc n)
   have ?case when  "s=n+1" using that by auto
   moreover have ?case when  "s \<noteq> n+1" 
   proof -
     have"(\<Sum>i=s..(n+1). 2^i ) = (\<Sum>i=s..n. 2^i ) + (2::real)^(n+1) "
       using sum.cl_ivl_Suc \<open>s \<le> Suc n \<close>
       by (auto simp add:add.commute)
     also have "... < (2) ^ (n +1) + (2)^(n+1)" 
     proof -
       have "s \<le>n" using that  \<open>s \<le> Suc n \<close> by auto
       then show ?thesis
         using Suc.hyps \<open>s \<le> n\<close> by linarith
     qed
     also have "... = 2^(n+2)" by simp
     finally show "(\<Sum>i=s..(Suc n). 2^i )< (2::real)^(Suc n+1)" by auto
   qed
   ultimately show ?case by blast
 qed
 
 subsection \<open>Auxiliary lemmas and the main proof\<close>
 
 lemma showpre7:
   fixes a b ::"nat\<Rightarrow>int " and q p::int
   assumes "q>0" and "p>0"and a: "\<forall>n. a n>0" and "\<forall>n. b n>0" and 
     assumerational:"(\<lambda> n. b (n+1) / a (n+1) )  sums (p/q)"
   shows "q*((\<Prod>j=1..n. of_int( a j)))*(suminf (\<lambda>(j::nat). (b (j+n+1)/ a (j+n+1 )))) 
         = ((\<Prod>j=1..n. of_int( a j)))*(p -q* (\<Sum>j=1..n. b j / a j))       " 
 proof -
   define aa where "aa=(\<Prod>j = 1..n. real_of_int (a j))"
   define ff where "ff=(\<lambda>i. real_of_int (b (i+1)) / real_of_int (a (i+1)))"
 
   have "(\<Sum>j. ff (j+n)) =  (\<Sum>n. ff n) - sum ff {..<n}"
     apply (rule suminf_minus_initial_segment)
     using assumerational unfolding ff_def by (simp add: sums_summable)
   also have "... = p/q - sum ff {..<n}"
     using assumerational unfolding ff_def by (simp add: sums_iff)
   also have "... = p/q - (\<Sum>j=1..n. ff (j-1))"
   proof -
     have "sum ff {..<n} = (\<Sum>j=1..n. ff (j-1))"
       apply (subst sum_bounds_lt_plus1[symmetric])
       by simp
     then show ?thesis unfolding ff_def by auto
   qed
   finally have "(\<Sum>j. ff (j + n)) = p / q - (\<Sum>j = 1..n. ff (j - 1))" .
   then have "q*(\<Sum>j. ff (j + n)) = p - q*(\<Sum>j = 1..n. ff (j - 1))"
     using \<open>q>0\<close> by (auto simp add:field_simps)
   then have "aa*q*(\<Sum>j. ff (j + n)) = aa*(p - q*(\<Sum>j = 1..n. ff (j - 1)))" 
     by auto
   then show ?thesis unfolding aa_def ff_def by auto
 qed
 
 lemma show7:
   fixes d::"nat\<Rightarrow>real" and a b::"nat\<Rightarrow>int " and q p::int
   assumes "q \<ge>1" and "p \<ge> 1" and a: "\<forall>n. a n \<ge> 1" and "\<forall>n. b n \<ge> 1"
     and assumerational:"(\<lambda> n. b (n+1) / a (n+1) ) sums (p/q)"
   shows "q*((\<Prod>j=1..n. of_int( a j)))*( suminf (\<lambda> (j::nat). (b (j+n+1)/ a (j+n+1 )))) \<ge> 1 "
     (is "?L \<ge> _")
 proof-
   define LL where "LL=?L"
   define aa where "aa=(\<Prod>j = 1..n. real_of_int (a j))"
   define ff where "ff=(\<lambda>i. real_of_int (b (i+1)) / real_of_int (a (i+1)))"
 
   have "?L > 0"
   proof -
     have "aa > 0"
       unfolding aa_def using a
       apply (induct n,auto)
       by (simp add: int_one_le_iff_zero_less prod_pos)
     moreover have "(\<Sum>j. ff (j + n)) > 0"
     proof (rule suminf_pos)
       have "summable ff" unfolding ff_def using assumerational
         using summable_def by blast
       then show " summable (\<lambda>j. ff (j + n))" using summable_iff_shift[of ff n] by auto
       show "\<And>i. 0 < ff (i + n)" unfolding ff_def using a assms(4) int_one_le_iff_zero_less by auto
     qed
     ultimately show ?thesis unfolding aa_def ff_def using \<open>q\<ge>1\<close> by auto
   qed
   moreover have "?L \<in> \<int>"
   proof -
     have "?L = aa *(p -q* ( \<Sum>j=1..n. b j / a j))"
       unfolding aa_def
       apply (rule showpre7)
       using assms int_one_le_iff_zero_less by auto
     also have "... = aa * p - q * (\<Sum>j=1..n. aa * b j / a j)"
       by (auto simp add:algebra_simps sum_distrib_left)
     also have "... = prod a {1..n} * p - q * (\<Sum>j = 1..n. b j * prod a ({1..n} - {j}))"
     proof -
       have "(\<Sum>j=1..n. aa * b j / a j) = (\<Sum>j=1..n. b j * prod a ({1..n} - {j}))"
         unfolding of_int_sum
       proof (rule sum.cong)
         fix x assume "x \<in> {1..n}"
         then have "(\<Prod>i = 1..n. real_of_int (a i)) = a x * (\<Prod>i\<in>{1..n} - {x}. real_of_int (a i))"
           apply (rule_tac prod.remove)
           by auto
         then have "aa / real_of_int (a x) = prod a ({1..n} - {x})"
           unfolding aa_def using a[rule_format,of x] by (auto simp add:field_simps)
         then show "aa * b x / a x = b x * prod a ({1..n} - {x})"
           by (metis mult.commute of_int_mult times_divide_eq_right)
       qed simp
       moreover have "aa * p = (\<Prod>j = 1..n.  (a j)) *  p"
         unfolding aa_def by auto
       ultimately show ?thesis by force
     qed
     also have "... \<in> \<int>" using Ints_of_int by blast
     finally show ?thesis .
   qed
   ultimately show ?thesis 
     apply (fold LL_def)
     by (metis Ints_cases int_one_le_iff_zero_less not_less of_int_0_less_iff of_int_less_1_iff)
 qed
 
 lemma show8:
   fixes d ::"nat\<Rightarrow>real " and a :: "nat\<Rightarrow>int" and s k::nat 
   assumes "A > 1" and d: "\<forall>n. d n> 1"  and a:"\<forall>n. a n>0" and "s>0"
     and "convergent_prod d"
     and assu2: "\<forall>n \<ge> s. ( A/ (of_int (a n)) powr(1/of_int (2^n)))> prodinf (\<lambda>j. d(n +j))"
   shows "\<forall>n\<ge>s. prodinf (\<lambda>j. d(j+n)) < A/(Max ((\<lambda>(j::nat). 
                   (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n}))"
 proof (intro strip)
   fix n assume "s \<le> n"
   define sp where "sp = (\<lambda>n. prodinf (\<lambda>j. d(j+n)))"
   define ff where "ff = (\<lambda>(j::nat). (real_of_int (a j)) powr(1 /of_int (2^j)))"
   have "sp i \<ge> sp n" when "i\<le>n" for i
   proof -
     have "(\<Prod>j. d (j + i)) = (\<Prod>ia. d (ia + (n - i) + i)) * (\<Prod>ia<n - i. d (ia + i))"
     proof (rule prodinf_split_initial_segment) 
       show "convergent_prod (\<lambda>j. d (j + i))"
         using \<open>convergent_prod d\<close> convergent_prod_iff_shift[of d i] by simp
       show "\<And>j. j < n - i \<Longrightarrow> d (j + i) \<noteq> 0"
         by (metis d not_one_less_zero)
     qed
     then have "sp i = sp n * (\<Prod>j<n - i. d (i + j))"
       unfolding sp_def using \<open>n\<ge>i\<close> by (auto simp:algebra_simps)
     moreover have "sp i>1" "sp n>1" 
       unfolding sp_def using convergent_prod_iff_shift \<open>convergent_prod d\<close> d 
       by (auto intro!:less_1_prodinf)
     moreover have "(\<Prod>j<n - i. d (i + j)) \<ge> 1" 
       using d less_imp_le by (auto intro: prod_ge_1)
     ultimately show ?thesis by auto
   qed
   moreover have "\<forall>j\<ge>s. A / ff j > sp j" 
     unfolding ff_def sp_def using assu2 by (auto simp:algebra_simps)
   ultimately have "\<forall>j. s\<le>j \<and> j\<le>n \<longrightarrow> A / ff j > sp n" by force
   then show "sp n< A / Max (ff ` {s..n})" 
     by (metis (mono_tags, hide_lams) Max_in \<open>n\<ge>s\<close> atLeastAtMost_iff empty_iff 
         finite_atLeastAtMost finite_imageI imageE image_is_empty order_refl)
 qed
 
 lemma auxiliary1_9:
   fixes d ::"nat\<Rightarrow>real" and a::"nat\<Rightarrow>int " and s m::nat 
   assumes d: "\<forall>n. d n> 1"  and a: "\<forall>n. a n>0" and "s>0" and "n \<ge> m" and " m \<ge> s"
     and auxifalse_assu: "\<forall>n\<ge>m. (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) <
               (d (n+1))* (Max ((\<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} ))"
   shows "(of_int (a (n+1))) powr(1 /of_int (2^(n+1))) <
     (\<Prod>j=(m+1)..(n+1). d j) * (Max ((\<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..m}))"
 proof-
   define ff where "ff = (\<lambda>(j::nat). (real_of_int (a j)) powr(1 /of_int (2^j)))"
   have [simp]:"ff j > 0" for j
     unfolding ff_def by (metis a less_numeral_extra(3) of_int_0_less_iff powr_gt_zero)
 
   have ff_asm:"ff (n+1) < d (n+1) * Max (ff ` {s..n})" when "n\<ge>m" for n
     using auxifalse_assu that unfolding ff_def by simp
   from \<open>n\<ge>m\<close>
   have Q: "(Max( ff ` {s..n} )) \<le> (\<Prod>j=(m+1)..n. d j)* (Max (ff ` {s..m}))"
   proof(induct n)
     case 0
     then show ?case using \<open>m\<ge>s\<close> by simp 
   next
     case (Suc n)
     have ?case when "m=Suc n"
       using that by auto
     moreover have ?case when "m\<noteq>Suc n" 
     proof -
       have "m \<le> n" using that Suc(2) by simp
       then have IH:"Max (ff ` {s..n}) \<le> prod d {m + 1..n} * Max (ff ` {s..m})"
         using Suc(1) by linarith
       have "Max (ff ` {s..Suc n}) = Max (ff ` {s..n} \<union> {ff (Suc n)})"
         using Suc.prems assms(5) atLeastAtMostSuc_conv by auto
       also have "... = max (Max (ff ` {s..n})) (ff (Suc n))"
         using Suc.prems assms(5) max_def sup_assoc that by auto
       also have "... \<le> max (Max (ff ` {s..n})) (d (n+1) * Max (ff ` {s..n}))"
         using \<open>m \<le> n\<close> ff_asm by fastforce
       also have "... \<le> Max (ff ` {s..n}) * max 1 (d (n+1))"
       proof -
         have "Max (ff ` {s..n}) \<ge> 0" 
           by (metis (mono_tags, hide_lams) Max_in \<open>\<And>j. 0 < ff j\<close> \<open>m \<le> n\<close> assms(5) 
               atLeastAtMost_iff empty_iff finite_atLeastAtMost finite_imageI imageE 
               image_is_empty less_eq_real_def)
         then show ?thesis using max_mult_distrib_right 
           by (simp add: max_mult_distrib_right mult.commute)
       qed
       also have "... = Max (ff ` {s..n}) * d (n+1)"
         using d[rule_format, of "n+1"] by auto
       also have "... \<le>  prod d {m + 1..n} * Max (ff ` {s..m}) * d (n+1)"
         using IH d[rule_format, of "n+1"] by auto
       also have "... = prod d {m + 1..n+1} * Max (ff ` {s..m})"
         using \<open>n\<ge>m\<close> by (simp add:prod.nat_ivl_Suc' algebra_simps)
       finally show ?case by simp
     qed
     ultimately show ?case by blast
   qed
   then have "d (n+1) * Max (ff ` {s..n} ) \<le> (\<Prod>j=(m+1)..(n+1). d j)* (Max (ff ` {s..m}))"
     using \<open>m\<le>n\<close> d[rule_format,of "Suc n"] by (simp add:prod.nat_ivl_Suc')
   then show ?thesis using ff_asm[of n] \<open>s\<le>m\<close> \<open>m\<le>n\<close> unfolding ff_def by auto
 qed
 
 lemma show9:
   fixes d ::"nat\<Rightarrow>real " and a :: "nat\<Rightarrow>int " and s ::nat and A::real
   assumes   "A > 1" and  d: "\<forall>n. d n> 1"  and a: "\<forall>n. a n>0" and "s>0"  
     and assu1: "(( \<lambda> n. (of_int (a n)) powr(1 /of_int (2^n)))\<longlongrightarrow> A) sequentially "
     and "convergent_prod d"
     and 8: "\<forall>n\<ge>s. prodinf (\<lambda>j. d( n+j)) 
                   < A/(Max ((\<lambda>(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n})) "
   shows "\<forall>m \<ge>s. \<exists>n\<ge>m.  ( (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
           (d (n+1))* (Max ( ( \<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
 proof (rule ccontr)
   define ff where "ff = (\<lambda>(j::nat). (real_of_int (a j)) powr(1 /of_int (2^j)))"
   assume assumptioncontra: " \<not> (\<forall>m \<ge>s. \<exists>n\<ge>m.  ( (ff (n+1)) \<ge> (d (n+1))* (Max ( ff  ` {s..n}))))"
 
   then obtain  t where "t\<ge>s" and
     ttt: "  \<forall>n\<ge>t.  ( (ff (n+1)) < (d (n+1))* (Max ( ff ` {s..n} ) ))"               
     by fastforce
   define B where "B=prodinf (\<lambda>j. d(t+1+j))"
   have "B>0" unfolding B_def 
   proof (rule less_0_prodinf)
     show "convergent_prod (\<lambda>j. d (t + 1 + j))"
       using convergent_prod_iff_shift[of d "t+1"] \<open>convergent_prod d\<close> 
       by (auto simp: algebra_simps)
     show "\<And>i. 0 < d (t + 1 + i)"
       using d le_less_trans zero_le_one by blast
   qed
   have "A \<le> B * Max ( ff ` {s..t})"
   proof (rule tendsto_le[of sequentially "\<lambda>n. (\<Prod>j=(t+1)..(n+1). d j) * Max ( ff ` {s..t})" _ 
         "\<lambda>n. ff (n+1)"])
     show "(\<lambda>n. ff (n + 1)) \<longlonglongrightarrow> A"
       using assu1[folded ff_def] LIMSEQ_ignore_initial_segment by blast
     have "(\<lambda>n. prod d {t + 1..n + 1}) \<longlonglongrightarrow> B"
     proof -
       have "convergent_prod (\<lambda>j. d (t + 1 + j))"
         using \<open>convergent_prod d\<close> convergent_prod_iff_shift[of d "t+1"] by (simp add:algebra_simps)
       then have "(\<lambda>n. \<Prod>i\<le>n. d (t + 1 + i)) \<longlonglongrightarrow> B"
         using B_def convergent_prod_LIMSEQ by blast
       then have "(\<lambda>n. \<Prod>i\<in>{0..n}. d (i+(t + 1))) \<longlonglongrightarrow> B"
         using atLeast0AtMost by (auto simp:algebra_simps)
       then have "(\<lambda>n. prod d {(t + 1)..n + (t + 1)}) \<longlonglongrightarrow> B" 
         apply (subst (asm) prod.shift_bounds_cl_nat_ivl[symmetric])
         by simp
       from seq_offset_neg[OF this,of "t"]
       show "(\<lambda>n. prod d {t + 1..n+1}) \<longlonglongrightarrow> B"
         apply (elim Lim_transform)
         apply (rule LIMSEQ_I)
         apply (rule exI[where x="t+1"])
         by auto
     qed
     then show "(\<lambda>n. prod d {t + 1..n + 1} * Max (ff ` {s..t})) \<longlonglongrightarrow> B * Max (ff ` {s..t})" 
       by (auto intro:tendsto_eq_intros)
     have "\<forall>\<^sub>F n in sequentially. (ff (n+1)) < (\<Prod>j=(t+1)..(n+1). d j) * (Max ( ff ` {s..t}))"
       unfolding eventually_sequentially ff_def
       using auxiliary1_9[OF d a \<open>s>0\<close> _ \<open>t\<ge>s\<close> ttt[unfolded ff_def]]
       by blast
     then show "\<forall>\<^sub>F n in sequentially. (ff (n+1)) \<le> (\<Prod>j=(t+1)..(n+1). d j) * (Max ( ff ` {s..t}))"
       by (eventually_elim,simp)
   qed simp
   also have "... \<le> B * Max ( ff ` {s..t+1})"
   proof -
     have "Max (ff ` {s..t}) \<le> Max (ff ` {s..t + 1})"
       apply (rule Max_mono)
       using \<open>t\<ge>s\<close> by auto
     then show ?thesis using \<open>B>0\<close> by auto
   qed
   finally have "A \<le> B * Max (ff ` {s..t + 1})" 
     unfolding B_def .
   moreover have "B < A / Max (ff ` {s..t + 1})"
     using 8[rule_format, of "t+1",folded ff_def B_def] \<open>s\<le>t\<close> by auto
   moreover have "Max (ff ` {s..t+1})>0"
     using \<open>A \<le> B * Max (ff ` {s..t + 1})\<close> \<open>B>0\<close> \<open>A>1\<close>
       zero_less_mult_pos [of B "Max (ff ` {s..Suc t})"]
     by simp
   ultimately show False by (auto simp add:field_simps)
 qed
 
 lemma show10:
   fixes d ::"nat\<Rightarrow>real " and  a ::"nat\<Rightarrow>int " and s::nat
   assumes d: "\<forall>n. d n> 1" and a: "\<forall>n. a n>0"  and " s>0"
     and 9: "\<forall>m \<ge>s. \<exists>n\<ge>m.  ((of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
           (d (n+1))* (Max ((\<lambda>(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
   shows "\<forall>m\<ge>s. \<exists>n\<ge>m. (((d (n+1))powr(2^(n+1))) * (\<Prod>j=1..n. of_int( a j)) * 
             (1/ (\<Prod>j=1..s-1. (of_int( a j) )))) \<le> (a (n+1)) "
 proof (rule,rule)
   fix m assume "s \<le> m" 
   from 9[rule_format,OF this]
   obtain n where "n\<ge>m" and asm_9:"( (of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
           (d (n+1))* (Max ( ( \<lambda> (j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
     by auto
   with \<open>s\<le>m\<close> have "s\<le>n" by auto
 
   have prod:"(\<Prod>j=1..n. real_of_int( a j)) * ( 1/ (\<Prod>j=1..s-1. (of_int( a j) )))
           = (\<Prod>j=s..n. of_int( a j))"
   proof -
     define f where "f= (\<lambda>j. real_of_int( a j))"
     have "{Suc 0..n}= {Suc 0..s - Suc 0} \<union> {s..n}" using \<open>n\<ge>s\<close>  \<open>s >0\<close>
       by auto
     then have "(\<Prod>j=1..n. f j) = (\<Prod>j=1..s-1. f j) * (\<Prod>j=s..n. f j)"
       apply (subst prod.union_disjoint[symmetric])
       by auto
     moreover have "(\<Prod>j=1..s-1. f j) > 0 "
       by (metis a f_def of_int_0_less_iff prod_pos)
     then have "(\<Prod>j=1..s-1. f j) \<noteq> 0" by argo
     ultimately show ?thesis unfolding f_def by auto 
   qed
   then have "d (n+1) powr 2 ^ (n+1) * (\<Prod>j = 1..n. of_int (a j)) * (1 / (\<Prod>j = 1..s - 1. of_int (a j))) =
              d (n+1) powr 2 ^ (n+1) * (\<Prod>j = s..n. of_int (a j))" 
      by (metis mult.assoc prod)
   also have
     "... \<le> ((d (n+1))powr(2^(n+1) ) * (\<Prod>i=s..n. (Max(( \<lambda> (j::nat). ( of_int( a j) powr(1 /real_of_int (2^j)) )) ` {s..n  } ))   powr(2^i)) )"
   proof (rule mult_left_mono)
     show "0 \<le> (d (n + 1)) powr 2 ^ (n + 1)"
       by auto
     show "(\<Prod>j = s..n. real_of_int (a j))
     \<le> (\<Prod>i = s..n.
            Max ((\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) `
                 {s..n}) powr
            2 ^ i)"
     proof (rule prod_mono)
       fix i assume i: "i \<in> {s..n}"
       have "real_of_int (a i) = (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i"
         unfolding powr_powr by (simp add: a less_eq_real_def)
       also have  "\<dots> \<le>  (Max(( \<lambda> (j::nat). ( real_of_int( a j) powr(1 /real_of_int (2^j)))) ` {s..n}))powr(2^i)" 
       proof (rule powr_mono2)
         show "real_of_int (a i) powr (1 / real_of_int (2 ^ i))
                   \<le> Max ((\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n})" 
           using i by force
       qed simp_all
       finally have "real_of_int (a i) \<le> Max ((\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}) powr 2 ^ i" .
       then show "0 \<le> real_of_int (a i) \<and>
                  real_of_int (a i) \<le> (MAX j\<in>{s..n}. of_int (a j) powr (1 / of_int (2 ^ j))) powr 2 ^ i"
         using a i
         by (metis \<open>real_of_int (a i) = (real_of_int (a i) powr (1 / real_of_int (2 ^ i))) powr 2 ^ i\<close> 
             powr_ge_pzero)
     qed
   qed
   also have "... = ((d (n+1))powr(2^(n+1) )) * (Max(( \<lambda> (j::nat). ( of_int( a j) powr 
                       (1 /of_int (2^j)) )) ` {s..n  } )) powr (\<Sum>i=s..n. 2^i ) "
   proof-
     have  "((d (n+1))powr(2^(n+1) ))\<ge>1  "
       by (metis Transcendental.log_one  d le_powr_iff zero_le_numeral zero_le_power zero_less_one)
     moreover have "(\<Prod>i=s..n. (Max(( \<lambda> (j::nat). ( of_int( a j) powr(1 /real_of_int (2^j)) )) ` {s..n  } ) )   powr(2^i))     = (Max(( \<lambda> (j::nat). ( of_int( a j) powr(1 /of_int (2^j)) )) ` {s..n  } )) powr (\<Sum>i=s..n. 2^i )  "
       using \<open>s\<le>n\<close>  powrfinitesum by auto
     ultimately show ?thesis by auto
   qed
   also have "... \<le>   ((d (n+1))powr(2^(n+1) )) * 
                 (Max(( \<lambda> (j::nat).( of_int( a j) powr(1 /of_int (2^j)) )) ` {s..n  })) powr(2^(n+1))   "
 
   proof -
     define ff where "ff \<equiv> (MAX j\<in>{s..n}. real_of_int (a j) powr (1 / real_of_int (2 ^ j)))"
     have " sum ((^) 2) {s..n} < (2::real) ^ (n + 1)" using factt \<open>s\<le>n\<close> by auto
     moreover have "1 \<le> ff" 
     proof -
       define S where "S=(\<lambda>(j::nat). ( of_int( a j) powr(1 /real_of_int (2^j)) )) ` {s..n  }"
       have "finite S" unfolding S_def by auto
       moreover have "S\<noteq>{}" unfolding S_def using \<open>s\<le>n\<close>  by auto
       moreover have "\<exists>x\<in>S. x\<ge>1"
       proof-
         have "a s powr (1 / (2^s)) \<ge> 1"  
         proof (rule ge_one_powr_ge_zero)
           show "1 \<le> real_of_int (a s)"
             by (simp add: a int_one_le_iff_zero_less)
         qed auto
         moreover have "of_int( a s) powr(1 /real_of_int (2^s)) \<in> S" 
           unfolding S_def
           using \<open>s\<le>n\<close> by auto
         ultimately show ?thesis by auto
       qed
       ultimately show ?thesis 
         using Max_ge_iff[of S 1] unfolding S_def ff_def by blast
     qed
     moreover have "0 \<le> (d (n + 1)) powr 2 ^ (n + 1)" by auto
     ultimately show ?thesis
       by (simp add: mult_left_mono powr_mono ff_def)
   qed
 
   also have "... =  ((d (n+1)) * 
                       (Max((\<lambda>j. (of_int( a j) powr(1 /of_int (2^j)))) ` {s..n}))) powr(2^(n+1))"
   proof -
     define ss where "ss = (\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}"
     have "d (n + 1) \<ge>0" using d[rule_format,of "n+1"] by argo
     moreover have "Max ss \<ge>0" 
     proof -
       have "(a s) powr (1 /  (2 ^ s)) \<ge> 0" by auto
       moreover have "(a s) powr (1 /  (2 ^ s)) \<in> ss" unfolding ss_def 
         using \<open>s\<le>n\<close> by auto
       moreover have "finite ss" "ss \<noteq> {}" unfolding ss_def using \<open>s\<le>n\<close> by auto
       ultimately show ?thesis using Max_ge_iff[of ss 0] by blast
     qed
     ultimately show ?thesis 
       unfolding ss_def
       using powr_mult by auto
   qed
   also have "... \<le> (real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))) powr 2 ^ (n + 1)"
   proof - 
     define ss where "ss = (\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n}"
     show ?thesis 
     proof (fold ss_def,rule powr_mono2)
       have "Max ss \<ge>0" \<comment> \<open>NOTE: we are repeating the same proof, so it may be a good idea to put 
                             this conclusion in an outer block so that it can be reused 
                             (without reproving).\<close>
       proof -
         have "(a s) powr (1 /  (2 ^ s)) \<ge> 0" by auto
         moreover have "(a s) powr (1 /  (2 ^ s)) \<in> ss" unfolding ss_def 
           using \<open>s\<le>n\<close> by auto
         moreover have "finite ss" "ss \<noteq> {}" unfolding ss_def using \<open>s\<le>n\<close> by auto
         ultimately show ?thesis using Max_ge_iff[of ss 0] by blast
       qed
       moreover have "d (n + 1) \<ge>0" 
         using d[rule_format,of "n+1"] by argo
       ultimately show "0 \<le> (d (n + 1)) * Max ss" by auto
       show "(d (n + 1)) * Max ss \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))"
         using asm_9[folded ss_def] .
     qed simp    
   qed
   also have "... =  (of_int (a (n+1)))" 
     by (simp add: a less_eq_real_def pos_add_strict powr_powr)
   finally show "\<exists>n\<ge>m. d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) *
                 (1 / (\<Prod>j = 1..s - 1. real_of_int (a j)))
                 \<le> real_of_int (a (n + 1))" using \<open>n\<ge>m\<close> \<open>m\<ge>s\<close> 
     by force
 qed
 
 lemma lasttoshow:
   fixes d ::"nat\<Rightarrow>real " and a b ::"nat\<Rightarrow>int " and q::int and s::nat
   assumes d: "\<forall>n. d n> 1" and a:"\<forall>n. a n>0" and "s>0" and "q>0"  
     and "A > 1" and b:"\<forall>n. b n>0" and 9:
     "\<forall>m\<ge>s. \<exists>n\<ge>m. ((of_int (a (n+1))) powr(1 /of_int (2^(n+1))) \<ge>
           (d (n+1))* (Max ((\<lambda>(j::nat). (of_int (a j)) powr(1 /of_int (2^j))) ` {s..n} )))"
     and assu3: "filterlim( \<lambda> n. (d n)^(2^n)/ b n) at_top sequentially "
     and 5: "\<forall>\<^sub>F n in sequentially. (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
   shows "\<exists>n. q*((\<Prod>j=1..n. real_of_int(a j))) * suminf (\<lambda>(j::nat). (b (j+n+1)/ a (j+n+1)))<1"
 proof-
   define as where "as=(\<Prod>j = 1..s - 1. real_of_int (a j))"
   obtain n where "n\<ge>s" and n_def1:"real_of_int q * as * 2 
       * real_of_int (b (n + 1)) / d (n + 1) powr 2 ^ (n + 1) < 1"
     and n_def2:"d (n + 1) powr 2 ^ (n + 1) * (\<Prod>j = 1..n. real_of_int (a j)) * (1 / as) 
           \<le> real_of_int (a (n + 1))"
     and n_def3:"(\<Sum>j. (b (n+1 + j)) /  (a (n+1 + j))) \<le> 2 * b (n+1) / a (n+1)"
   proof -
     have *:"(\<lambda>n. real_of_int (b n) / d n ^ 2 ^ n) \<longlonglongrightarrow> 0"
       using tendsto_inverse_0_at_top[OF assu3] by auto
     then have "(\<lambda>n. real_of_int (b n) / d n powr 2 ^ n) \<longlonglongrightarrow> 0"
     proof -
       have "d n ^ 2 ^ n = d n powr (of_nat (2 ^ n))" for n 
         apply (subst powr_realpow)
         using d[rule_format, of n] by auto
       then show ?thesis using * by auto
     qed
     from tendsto_mult_right_zero[OF this,of "q * as * 2"] 
     have "(\<lambda>n. q * as * 2 * b n / d n powr 2 ^ n) \<longlonglongrightarrow> 0"
       by auto
     then have "\<forall>\<^sub>F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1"
       by (elim order_tendstoD) simp
     then have "\<forall>\<^sub>F n in sequentially. q * as * 2 * b n / d n powr 2 ^ n < 1 
                   \<and> (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
       using 5 by eventually_elim auto
     then obtain N where N_def:"\<forall>n\<ge>N. q * as * 2 * b n / d n powr 2 ^ n < 1 
             \<and> (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
       unfolding eventually_sequentially by auto
     obtain n where "n\<ge>s" and "n\<ge>N" and n_def:"d (n + 1) powr 2 ^ (n + 1) 
                 * (\<Prod>j = 1..n. of_int (a j)) * (1 / as) \<le> real_of_int (a (n + 1))"
       using show10[OF d a \<open>s>0\<close> 9,folded as_def,rule_format,of "max s N"] by auto
     with N_def[rule_format, of "n+1"] that[of n]  show ?thesis by auto
   qed
 
   define pa where "pa = (\<Prod>j = 1..n. real_of_int (a j))"
   define dn where "dn = d (n + 1) powr 2 ^ (n + 1)"
   have [simp]:"dn >0" "as > 0" 
     subgoal unfolding dn_def by (metis d not_le numeral_One powr_gt_zero zero_le_numeral)
     subgoal unfolding as_def by (simp add: a prod_pos)
     done
   have [simp]:"pa>0"
     unfolding pa_def using a by (simp add: prod_pos)
 
   have K: "q* (\<Prod>j=1..n. real_of_int (a j)) * suminf (\<lambda> (j::nat). (b (j+n+1)/ a (j+n+1)))
               \<le>q* (\<Prod>j=1..n. real_of_int (a j)) *2* (b (n+1))/(a( n+1))"
     apply (fold pa_def)
     using mult_left_mono[OF n_def3,of "real_of_int q * pa"] 
       \<open>n\<ge>s\<close> \<open>pa>0\<close> \<open>q>0\<close> by (auto simp add:algebra_simps) 
   also have KK:"... \<le> 2*q* (\<Prod>j=1..n. real_of_int (a j)) * (b(n+1))*
       ((\<Prod>j=1..s-1. real_of_int( a j))/((d (n+1))powr(2^(n+1)) * (\<Prod>j=1..n. real_of_int ( a j))))" 
   proof -
     have " dn * pa * (1 / as) \<le> real_of_int (a (n + 1))"
       using n_def2 unfolding dn_def pa_def .
     then show ?thesis 
       apply (fold pa_def dn_def as_def)
       using \<open>pa>0\<close> \<open>q>0\<close> a[rule_format, of "Suc n"] b[rule_format, of "Suc n"]
       by (auto simp add:divide_simps algebra_simps)
   qed
   also have KKK: "... = (q* ((\<Prod>j=1..(s-1). real_of_int( a j)))*2
                                 * (b (n+1)))/ ((d (n+1))powr(2^(n+1)))"
     apply (fold as_def pa_def dn_def)
     apply simp
     using \<open>0 < pa\<close> by blast
   also have KKKK: "... < 1" using n_def1 unfolding as_def by simp
   finally show ?thesis by auto
 qed
 
 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-
   define c where "c = (\<lambda>j. b j / a j)"
   have c_pos:"c j>0" for j 
     using a b unfolding c_def by simp
   have c_ratio_tendsto:"(\<lambda>n. c (n+1) / c n ) \<longlonglongrightarrow> 0"
   proof -
     define nn where "nn=(\<lambda>n. (2::int)^ (Suc n))"
     define ff where "ff=(\<lambda> n. (a n / a (Suc n)) powr(1 /nn n)*(d(Suc n)))"
     have nn_pos:"nn n>0" and ff_pos:"ff n>0" for n
       subgoal unfolding nn_def by simp
       subgoal unfolding ff_def
         using d[rule_format, of "Suc n"] a[rule_format, of n] a[rule_format, of "Suc n"]
         by auto
       done
     have ff_tendsto:"ff \<longlonglongrightarrow> 1/ sqrt A" 
     proof -
       have "(of_int (a n)) powr(1 / (nn n)) = sqrt(of_int (a n) powr(1 /of_int (2^n)))" for n
         unfolding nn_def using a
         by (simp add: powr_half_sqrt [symmetric] powr_powr ac_simps)
       moreover have "(( \<lambda> n. sqrt(of_int (a n) powr(1 /of_int (2^n))))\<longlongrightarrow> sqrt A) sequentially " 
         using assu1 tendsto_real_sqrt by blast
       ultimately have "(( \<lambda> n. (of_int (a n)) powr(1 /of_int (nn n)))\<longlongrightarrow> sqrt A) sequentially " 
         by auto
       from tendsto_divide[OF this assu1[THEN LIMSEQ_ignore_initial_segment[where k=1]]] 
       have "(\<lambda>n. (a n / a (Suc n)) powr(1 /nn n)) \<longlonglongrightarrow> 1/sqrt A"
         using \<open>A>1\<close> a unfolding nn_def
         by (auto simp add:powr_divide less_imp_le inverse_eq_divide sqrt_divide_self_eq)
       moreover have "(\<lambda>n. d (Suc n))\<longlonglongrightarrow> 1" 
         apply (rule convergent_prod_imp_LIMSEQ)
         using convergent_prod_iff_shift[of d 1] \<open>convergent_prod d\<close> by auto
       ultimately show ?thesis
         unfolding ff_def by (auto intro:tendsto_eq_intros)
     qed
     have "(\<lambda>n. (ff n) powr nn n) \<longlonglongrightarrow> 0" 
     proof -
       define aa where "aa=(1+1/sqrt A) / 2"
       have "eventually (\<lambda>n. ff n<aa) sequentially"
         apply (rule order_tendstoD[OF ff_tendsto])
         unfolding aa_def using \<open>A>1\<close> by (auto simp add:field_simps)
       moreover have "(\<lambda>n. aa powr nn n) \<longlonglongrightarrow> 0" 
       proof -
         have "(\<lambda>y. aa ^ (nat \<circ> nn) y) \<longlonglongrightarrow> 0"
           apply (rule tendsto_power_zero)
           subgoal unfolding nn_def comp_def
             apply (rule filterlim_subseq)
             by (auto intro:strict_monoI)
           subgoal unfolding aa_def using \<open>A>1\<close> by auto
           done
         then show ?thesis
         proof (elim filterlim_mono_eventually)
           have "aa>0" unfolding aa_def using \<open>A>1\<close> 
             by  (auto simp add:field_simps pos_add_strict)
           then show " \<forall>\<^sub>F x in sequentially. aa ^ (nat \<circ> nn) x = aa powr real_of_int (nn x)"
             by (auto simp: powr_int order.strict_implies_order[OF nn_pos])
         qed auto
       qed
       ultimately show ?thesis
         apply (elim metric_tendsto_imp_tendsto)
         apply (auto intro!:powr_mono2 elim!:eventually_mono)
         using nn_pos ff_pos by (meson le_cases not_le)+
     qed
     then have "(\<lambda>n. (d (Suc n))^(nat (nn n)) * (a n / a (Suc n))) \<longlonglongrightarrow> 0" 
     proof (elim filterlim_mono_eventually)
       show "\<forall>\<^sub>F x in sequentially. ff x powr  (nn x) = d (Suc x) ^ nat (nn x) * (a x / a (Suc x))" 
         apply (rule eventuallyI)
         subgoal for x
           unfolding ff_def
           using a[rule_format,of x] a[rule_format,of "Suc x"] d[rule_format,of "Suc x"] nn_pos[of x]
           apply (auto simp add:field_simps powr_divide powr_powr powr_mult )
           by (simp add: powr_int)
         done
     qed auto 
     moreover have "(\<lambda>n. b (Suc n) / (d (Suc n))^(nat (nn n))) \<longlonglongrightarrow> 0"
       using tendsto_inverse_0_at_top[OF assu3,THEN LIMSEQ_ignore_initial_segment[where k=1]]
       unfolding nn_def by (auto simp add:field_simps nat_mult_distrib nat_power_eq)
     ultimately have "(\<lambda>n. b (Suc n) * (a n / a (Suc n))) \<longlonglongrightarrow> 0" 
       apply -
       subgoal premises asm
         using tendsto_mult[OF asm,simplified]
         apply (elim filterlim_mono_eventually)
         using d by (auto simp add:algebra_simps,metis (mono_tags, lifting) always_eventually 
             not_one_less_zero)
       done
     then have "(\<lambda>n. (b (Suc n) / b n) * (a n / a (Suc n))) \<longlonglongrightarrow> 0" 
       apply (elim Lim_transform_bound[rotated])
       apply (rule eventuallyI)
       subgoal for x using a[rule_format, of x] a[rule_format, of "Suc x"] 
           b[rule_format, of x] b[rule_format, of "Suc x"]
         by (auto simp add:field_simps)
       done
     then show ?thesis unfolding c_def by (auto simp add:algebra_simps)
   qed
   from c_ratio_tendsto
   have "(\<lambda>n. norm (b (Suc n) / a (Suc n)) / norm (b n / a n)) \<longlonglongrightarrow> 0" 
     unfolding c_def
     using a b by (force simp add:divide_simps abs_of_pos intro: Lim_transform_eventually)
   from summable_ratio_test_tendsto[OF _ _ this] a b 
   show "summable c" unfolding c_def
     by (metis c_def c_pos less_irrefl zero_less_one)
   have "\<forall>\<^sub>F n in sequentially. (\<Sum>j. c (n + j)) \<le> 2 * c n"
   proof -
     obtain N where N_ratio:"\<forall>n\<ge>N. c (n + 1) / c n < 1 / 2" 
     proof -
       have "eventually (\<lambda>n. c (n+1) / c n < 1/2) sequentially" 
         using c_ratio_tendsto[unfolded tendsto_iff,rule_format, of "1/2",simplified]
         apply eventually_elim
         subgoal for n using c_pos[of n] c_pos[of "Suc n"] by auto
         done
       then show ?thesis using that unfolding eventually_sequentially by auto
     qed
     have "(\<Sum>j. c (j + n)) \<le> 2 * c n" when "n\<ge>N" for n
     proof -
       have "(\<Sum>j<m. c (j + n)) \<le> 2*c n * (1 - 1 / 2^(m+1))" for m
       proof (induct m)
         case 0
         then show ?case using c_pos[of n] by simp
       next
         case (Suc m)
         have "(\<Sum>j<Suc m. c (j + n)) = c n + (\<Sum>i<m. c (Suc i + n)) "
           unfolding sum.lessThan_Suc_shift by simp
         also have "... \<le> c n + (\<Sum>i<m. c (i + n) / 2)"
         proof -
           have "c (Suc i + n) \<le> c (i + n) / 2" for i
             using N_ratio[rule_format,of "i+n"] \<open>n\<ge>N\<close> c_pos[of "i+n"]  by simp
           then show ?thesis by (auto intro:sum_mono)
         qed
         also have "... = c n + (\<Sum>i<m. c (i + n)) / 2"
           unfolding sum_divide_distrib by simp
         also have "... \<le> c n + c n * (1 - 1 / 2 ^ (m + 1))"
           using Suc by auto
         also have "... = 2 * c n * (1 - 1 / 2 ^ (Suc m + 1))"
           by (auto simp add:field_simps)
         finally show ?case .
       qed
       then have "(\<Sum>j<m. c (j + n)) \<le> 2*c n" for m
         using c_pos[of n] 
         by (smt divide_le_eq_1_pos divide_pos_pos nonzero_mult_div_cancel_left zero_less_power)
       moreover have "summable (\<lambda>j. c (j + n))" 
         using \<open>summable c\<close> by (simp add: summable_iff_shift)
       ultimately show ?thesis using suminf_le_const[of "\<lambda>j. c (j+n)" "2*c n"] by auto
     qed
     then show ?thesis unfolding eventually_sequentially by (auto simp add:algebra_simps)
   qed
   then show "\<forall>\<^sub>F n in sequentially. (\<Sum>j. (b (n + j)) /  (a (n + j))) \<le> 2 * b n / a n"
     unfolding c_def by simp
 qed
 
 
 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. (of_int (a n)) powr(1 /of_int (2^n)))\<longlongrightarrow> A) sequentially "
     and assu2: "\<forall>n \<ge> s. (A/ (of_int (a n)) powr(1 /of_int (2^n)))> prodinf (\<lambda>j. d(n +j))"
     and assu3: "filterlim (\<lambda> n. (d n)^(2^n)/ b n) at_top sequentially"
     and "convergent_prod d" 
   shows "suminf(\<lambda> n. b n / a n ) \<notin> Rats"
 proof(rule ccontr)
   assume asm:"\<not> (suminf(\<lambda> n. b n / a n ) \<notin> Rats)"
   have ab_sum:"summable (\<lambda>j. b j / a j)"
     using issummable[OF \<open>A>1\<close> d a b assu1 assu3 \<open>convergent_prod d\<close>] .
   obtain p q ::int where "q>0" and pq_def:"(\<lambda> n. b (n+1) / a (n+1) ) sums (p/q)"
   proof -
     from asm have "suminf(\<lambda> n. b n / a n ) \<in> Rats" by auto
     then have "suminf(\<lambda> n. b (n+1) / a (n+1)) \<in> Rats" 
       apply (subst suminf_minus_initial_segment[OF ab_sum,of 1])
       by auto   
     then obtain p' q' ::int where "q'\<noteq>0" and pq_def:"(\<lambda> n. b (n+1) / a (n+1) ) sums (p'/q')"
       unfolding Rats_eq_int_div_int
       using summable_ignore_initial_segment[OF ab_sum,of 1,THEN summable_sums]
       by force
     define p q where "p=(if q'<0 then - p' else p')" and "q=(if q'<0 then - q' else q')"
     have "p'/q'=p/q" "q>0" using \<open>q'\<noteq>0\<close> unfolding p_def q_def by auto
     then show ?thesis using that[of q p] pq_def by auto
   qed
 
   define ALPHA where 
     "ALPHA = (\<lambda>n. (of_int q)*((\<Prod>j=1..n. of_int(a j)))*(suminf (\<lambda> (j::nat). 
                       (b (j+n+1)/a (j+n+1)))))"
   have "ALPHA n \<ge> 1" for n 
   proof -
     have "suminf(\<lambda> n. b (n+1) / a (n+1)) > 0"
       apply (rule suminf_pos)
       subgoal using summable_ignore_initial_segment[OF ab_sum,of 1] by auto
       subgoal using a b by simp
       done
     then have "p/q > 0" using sums_unique[OF pq_def,symmetric] by auto
     then have "q\<ge>1" "p\<ge>1" using \<open>q>0\<close> by (auto simp add:divide_simps)
     moreover have "\<forall>n. 1 \<le> a n" "\<forall>n. 1 \<le> b n" using a b 
       by (auto simp add: int_one_le_iff_zero_less)
     ultimately show ?thesis unfolding ALPHA_def
       using show7[OF _ _ _ _ pq_def] by auto
   qed
   moreover have "\<exists>n. ALPHA n < 1" unfolding ALPHA_def
   proof (rule lasttoshow[OF d a \<open>s>0\<close> \<open>q>0\<close> \<open>A>1\<close> b _ assu3])
     show "\<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)"
       using show5[OF \<open>A>1\<close> d a b assu1 assu3 \<open>convergent_prod d\<close>] by simp
     show "\<forall>m\<ge>s. \<exists>n\<ge>m. d (n + 1) * Max ((\<lambda>j. real_of_int (a j) powr (1 / real_of_int (2 ^ j))) ` {s..n})
                  \<le> real_of_int (a (n + 1)) powr (1 / real_of_int (2 ^ (n + 1)))"
       apply (rule show9[OF \<open>A>1\<close> d a \<open>s>0\<close> assu1 \<open>convergent_prod d\<close>])
       using show8[OF \<open>A>1\<close> d a \<open>s>0\<close> \<open>convergent_prod d\<close> assu2] by (simp add:algebra_simps)
   qed
   ultimately show False using not_le by blast
 qed
 
 corollary Hancl3corollary:
   fixes A::real and  a b ::"nat\<Rightarrow>int "
   assumes "A > 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 asscor2: "\<forall>n \<ge>6. (of_int (a n)) powr(1 /of_int (2^n ))*(1+ 4*(2/3)^n) \<le> A
                     \<and> (b n \<le>2 powr((4/3)^(n-1)) )   "
   shows "suminf(\<lambda> n. b n / a n ) \<notin> Rats"
 proof-
   define d::"nat\<Rightarrow>real" where "d= (\<lambda> n. 1+(2/3)^(n+1))" 
 
   have dgt1:"\<forall>n. 1 < d n " unfolding d_def by auto
   moreover have "convergent_prod d"
     unfolding d_def
     apply (rule abs_convergent_prod_imp_convergent_prod)
     apply (rule summable_imp_abs_convergent_prod)
-    using summable_ignore_initial_segment[OF complete_algebra_summable_geometric
-          [of "2/3::real",simplified],of 1] by simp
+    by simp
   moreover have "\<forall>n\<ge>6. (\<Prod>j. d (n + j)) 
                     < A / real_of_int (a n) powr (1 / real_of_int (2 ^ n))"
-  proof rule+
+  proof (intro strip)
     fix n::nat assume "6 \<le> n"
     have d_sum:"summable (\<lambda>j. ln (d j))" unfolding d_def
-      apply (rule summable_ln_plus)
-      apply (rule summable_ignore_initial_segment[OF complete_algebra_summable_geometric
-          [of "2/3::real",simplified],of 1])
-      by simp 
+      by (auto intro: summable_ln_plus)
 
     have "(\<Sum>j. ln (d (n + j))) < ln (1+4 * (2 / 3) ^ n)"
     proof -
       define c::real where "c=(2 / 3) ^ n"
       have "0<c" "c<1/8" 
       proof -
         have "c=(2 / 3)^6 * (2 / 3)  ^ (n-6)"
           unfolding c_def using \<open>n\<ge>6\<close>
           apply (subst power_add[symmetric])
           by auto
         also have "... \<le> (2 / 3)^6" by (auto intro:power_le_one)
         also have "... < 1/8" by (auto simp add:field_simps)
         finally show "c<1/8" .
       qed (simp add:c_def)
 
       have "(\<Sum>j. ln (d (n + j))) \<le> (\<Sum>j. (2 / 3) ^ (n + j + 1))"
       proof (rule suminf_le)
         show "\<And>j. ln (d (n + j)) \<le> (2 / 3) ^ (n + j + 1)"
           unfolding d_def
           by (metis divide_pos_pos less_eq_real_def ln_add_one_self_le_self zero_less_numeral zero_less_power)
         show "summable (\<lambda>j. ln (d (n + j)))"
           using summable_ignore_initial_segment[OF d_sum] 
           by (force simp add: algebra_simps)
         show "summable (\<lambda>j. (2 / 3::real) ^ (n + j + 1))"
           using summable_geometric[THEN summable_ignore_initial_segment,of "2/3" "n+1"]
           by (auto simp add:algebra_simps)
       qed
       also have "... = (\<Sum>j. (2 / 3)^(n+1)*(2 / 3) ^ j)"
         by (auto simp add:algebra_simps power_add)
       also have "... = (2 / 3)^(n+1) * (\<Sum>j. (2 / 3) ^ j)"
         by (force intro!: summable_geometric suminf_mult)
       also have "... = 2 * c"
         unfolding c_def
         apply (subst suminf_geometric)
         by auto
       also have "... <  4 * c - (4 * c)\<^sup>2"
         using \<open>0<c\<close> \<open>c<1/8\<close>
         by (sos "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1/16 * [1]^2))))")
       also have "... \<le> ln (1 + 4 * c)"
         apply (rule ln_one_plus_pos_lower_bound)
         using \<open>0<c\<close> \<open>c<1/8\<close> by auto
       finally show ?thesis unfolding c_def by simp
     qed
     then have "exp (\<Sum>j. ln (d (n + j))) < 1 + 4 * (2 / 3) ^ n"
       by (metis Groups.mult_ac(2) add.right_neutral add_mono_thms_linordered_field(5) 
           divide_inverse divide_less_eq_numeral1(1) divide_pos_pos exp_gt_zero less_eq_real_def
           ln_exp ln_less_cancel_iff mult_zero_left rel_simps(27) rel_simps(76) zero_less_one
           zero_less_power)
     moreover have "exp (\<Sum>j. ln (d (n + j))) = (\<Prod>j. d (n + j))"
     proof (subst exp_suminf_prodinf_real [symmetric])
       show "\<And>k. 0 \<le> ln (d (n + k))" 
         using dgt1 by (simp add: less_imp_le)
       show "abs_convergent_prod (\<lambda>na. exp (ln (d (n + na))))"
         apply (subst exp_ln)
         subgoal for j using dgt1[rule_format,of "n+j"] by auto
         subgoal unfolding abs_convergent_prod_def real_norm_def
           apply (subst abs_of_nonneg)
           using convergent_prod_iff_shift[of d n] \<open>convergent_prod d\<close> 
           by (auto simp add: dgt1 less_imp_le algebra_simps)
         done
       show "(\<Prod>na. exp (ln (d (n + na)))) = (\<Prod>j. d (n + j))"
         apply (subst exp_ln)
         subgoal using dgt1 le_less_trans zero_le_one by blast
         subgoal by simp
         done
     qed
     ultimately have "(\<Prod>j. d (n + j))  < 1 + 4 * (2 / 3) ^ n"
       by simp
     also have "... \<le> A / (a n) powr (1 / of_int (2 ^ n))" 
     proof -
       have "a n powr (1 / real_of_int (2 ^ n)) > 0"
         using a[rule_format,of n] by auto
       then show ?thesis using asscor2[rule_format,OF \<open>6\<le>n\<close>] 
         by (auto simp add:field_simps)
     qed
     finally show "(\<Prod>j. d (n + j)) < A / real_of_int (a n) powr (1 / of_int (2 ^ n))" .
   qed
   moreover have "LIM n sequentially. d n ^ 2 ^ n / real_of_int (b n) :> at_top" 
   proof -
     have "LIM n sequentially. d n ^ 2 ^ n / 2 powr((4/3)^(n-1)) :> at_top"
     proof -
       define n1 where "n1=(\<lambda>n. (2::real)* (3/2)^(n-1))"
       define n2 where "n2=(\<lambda>n. ((4::real)/3)^(n-1))"
       have "LIM n sequentially. (((1+(8/9)/(n1 n)) powr (n1 n))/2) powr (n2 n) :> at_top" 
       proof (rule filterlim_at_top_powr_real[where g'="exp (8/9) / (2::real)"])
         define e1 where "e1=exp (8/9) / (2::real)"
         show "e1>1" unfolding e1_def by (approximation 4)
         show "(\<lambda>n. ((1+(8/9)/(n1 n)) powr (n1 n))/2) \<longlonglongrightarrow> e1"
         proof -
           have "(\<lambda>n. (1+(8/9)/(n1 n)) powr (n1 n)) \<longlonglongrightarrow> exp (8/9)"
             apply (rule filterlim_compose[OF tendsto_exp_limit_at_top])
             unfolding n1_def
             by (auto intro!: filterlim_tendsto_pos_mult_at_top 
                 filterlim_realpow_sequentially_at_top
                 simp:filterlim_sequentially_iff[of "\<lambda>x. (3 / 2) ^ (x - Suc 0)" _ 1])
           then show ?thesis unfolding e1_def
             by (intro tendsto_intros,auto)
         qed
         show "filterlim n2 at_top sequentially"
           unfolding n2_def
           apply (subst filterlim_sequentially_iff[of "\<lambda>n. (4 / 3) ^ (n - 1)" _ 1])
           by (auto intro:filterlim_realpow_sequentially_at_top)
       qed
       moreover have "\<forall>\<^sub>F n in sequentially. (((1+(8/9)/(n1 n)) powr (n1 n))/2) powr (n2 n)
         = d n ^ 2 ^ n / 2 powr((4/3)^(n-1))"
       proof (rule eventually_sequentiallyI[of 1])
         fix x assume "x\<ge>(1::nat)"
         have " ((1 + 8 / 9 / n1 x) powr n1 x / 2) powr n2 x 
                     = (((1 + 8 / 9 / n1 x) powr n1 x) powr n2 x) / 2 powr (4 / 3) ^ (x - 1)"
           by (simp add:n1_def n2_def powr_divide)
         also have "... = (1 + 8 / 9 / n1 x) powr (n1 x * n2 x) / 2 powr (4 / 3) ^ (x - 1)"
           by (simp add: powr_powr)
         also have "... = (1 + 8 / 9 / n1 x) powr (2 ^ x) / 2 powr (4 / 3) ^ (x - 1)"
         proof -
           have "n1 x * n2 x = 2 ^ x" 
             unfolding n1_def n2_def
             apply (subst mult.assoc)
             apply (subst power_mult_distrib[symmetric])
             using \<open>x\<ge>1\<close> by (auto simp flip:power_Suc)
           then show ?thesis by simp
         qed
         also have "... = (1 + 8 / 9 / n1 x) ^ (2 ^ x) / 2 powr (4 / 3) ^ (x - 1)"
           apply (subst (3) powr_realpow[symmetric])
            apply (simp_all add: n1_def)
           by (smt zero_le_divide_iff zero_le_power)
         also have "... = d x ^ 2 ^ x / 2 powr (4 / 3) ^ (x - 1)"
         proof -
           define x1 where "x1=x-1"
           have *:"x=x1+1" unfolding x1_def using \<open>x\<ge>1\<close> by simp
           have **: "8 / 9 / n1 x = (2 / 3) ^ (x + 1)" 
             unfolding n1_def using \<open>x\<ge>1\<close>
             apply (fold x1_def *[symmetric])
             by (auto simp add:divide_simps)
           then show ?thesis 
             unfolding d_def 
             apply (subst **)
             by auto
         qed
         finally show "((1 + 8 / 9 / n1 x) powr n1 x / 2) powr n2 x 
                         = d x ^ 2 ^ x / 2 powr (4 / 3) ^ (x - 1) " .
       qed
       ultimately show ?thesis using filterlim_cong by fast
     qed
     moreover have "\<forall>\<^sub>F n in sequentially. d n ^ 2 ^ n / 2 powr((4/3)^(n-1)) 
         \<le> d n ^ 2 ^ n / real_of_int (b n)"
       apply (rule eventually_sequentiallyI[of 6])
       apply (rule divide_left_mono)
       subgoal for x
         using asscor2[rule_format,of x] by auto
       subgoal for x
         using \<open>\<forall>n. 1 < d n\<close>[rule_format, of x] by auto
       subgoal for x
         using b by auto
       done
     ultimately show ?thesis by (auto elim: filterlim_at_top_mono)
   qed
   ultimately show ?thesis using Hancl3[OF \<open>A>1\<close> _ a b _ assu1,of d 6] by force
 qed
 
 end