[STATEMENT]
lemma asymptotics1':
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "(bs!i*x) powr p * (1 + ln x powr (-e/2)) \<le>
           (bs!i*x + (hs!i) x) powr p * (1 + ln (bs!i*x + (hs!i) x) powr (-e/2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have x: "x \<ge> x\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
from b_pos[of "bs!i"] assms
[PROOF STATE]
proof (chain)
picking this:
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have b_pos: "bs!i > 0" "bs!i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. 0 < bs ! i &&& bs ! i \<noteq> 0
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < bs ! i
bs ! i \<noteq> 0

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
from b_less_1[of "bs!i"] assms
[PROOF STATE]
proof (chain)
picking this:
bs ! i \<in> set bs \<Longrightarrow> bs ! i < 1
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have b_less_1: "bs!i < 1"
[PROOF STATE]
proof (prove)
using this:
bs ! i \<in> set bs \<Longrightarrow> bs ! i < 1
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. bs ! i < 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i < 1

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
from x1_gt_1 assms
[PROOF STATE]
proof (chain)
picking this:
1 < x\<^sub>1
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have ln_x_pos: "ln x > 0"
[PROOF STATE]
proof (prove)
using this:
1 < x\<^sub>1
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. 0 < ln x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < ln x

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
have mono: "\<And>a b. a \<le> b \<Longrightarrow> (bs!i*x) powr p * a \<le> (bs!i*x) powr p * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. a \<le> b \<Longrightarrow> (bs ! i * x) powr p * a \<le> (bs ! i * x) powr p * b
[PROOF STEP]
by (rule mult_left_mono) simp_all
[PROOF STATE]
proof (state)
this:
?a \<le> ?b \<Longrightarrow> (bs ! i * x) powr p * ?a \<le> (bs ! i * x) powr p * ?b

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
define s :: real where [abs_def]: "s = (if p \<ge> 0 then 1 else -1)"
[PROOF STATE]
proof (state)
this:
s \<equiv> if 0 \<le> p then 1 else - 1

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
have "1 + ln x powr (-e/2) \<le>
          (1 - s*hb*inverse(bs!i)*ln x powr -(1+e)) powr p *
          (1 + ln (bs!i*x + hb * x / ln x powr (1+e)) powr (-e/2))" (is "_ \<le> ?A * ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + ln x powr (- e / 2) \<le> (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))
[PROOF STEP]
using assms x
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. 1 + ln x powr (- e / 2) \<le> (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))
[PROOF STEP]
unfolding s_def
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. 1 + ln x powr (- e / 2) \<le> (1 - (if 0 \<le> p then 1 else - 1) * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))
[PROOF STEP]
using asymptotics1[OF x assms(2)] asymptotics1'[OF x assms(2)]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x
1 + ln x powr (- e / 2) \<le> (1 - hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))
1 + ln x powr (- e / 2) \<le> (1 + hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))

goal (1 subgoal):
 1. 1 + ln x powr (- e / 2) \<le> (1 - (if 0 \<le> p then 1 else - 1) * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 + ln x powr (- e / 2) \<le> (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + ln x powr (- e / 2) \<le> (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
have "(bs!i*x) powr p * ... = (bs!i*x) powr p * ?A * ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i * x) powr p * ((1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))) = (bs ! i * x) powr p * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(bs ! i * x) powr p * ((1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))) = (bs ! i * x) powr p * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i * x) powr p * ((1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))) = (bs ! i * x) powr p * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
from x0_hb_bound0'[OF x, of "bs!i"] hb_nonneg x ln_x_pos assms
[PROOF STATE]
proof (chain)
picking this:
bs ! i \<in> set bs \<Longrightarrow> hb / ln x powr (1 + e) < bs ! i
0 \<le> hb
x\<^sub>0 \<le> x
0 < ln x
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "s*hb * ln x powr -(1 + e) < bs ! i"
[PROOF STATE]
proof (prove)
using this:
bs ! i \<in> set bs \<Longrightarrow> hb / ln x powr (1 + e) < bs ! i
0 \<le> hb
x\<^sub>0 \<le> x
0 < ln x
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. s * hb * ln x powr - (1 + e) < bs ! i
[PROOF STEP]
by (subst powr_minus) (simp_all add: field_simps s_def)
[PROOF STATE]
proof (state)
this:
s * hb * ln x powr - (1 + e) < bs ! i

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
hence "(bs!i*x) powr p * ?A = (bs!i*x*(1 - s*hb*inverse (bs!i)*ln x powr -(1+e))) powr p"
[PROOF STATE]
proof (prove)
using this:
s * hb * ln x powr - (1 + e) < bs ! i

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p = (bs ! i * x * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e))) powr p
[PROOF STEP]
using b_pos assms x x0_pos b_less_1 ln_x_pos
[PROOF STATE]
proof (prove)
using this:
s * hb * ln x powr - (1 + e) < bs ! i
0 < bs ! i
bs ! i \<noteq> 0
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x
0 < x\<^sub>0
bs ! i < 1
0 < ln x

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p = (bs ! i * x * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e))) powr p
[PROOF STEP]
by (subst powr_mult[symmetric]) (simp_all add: s_def field_simps)
[PROOF STATE]
proof (state)
this:
(bs ! i * x) powr p * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p = (bs ! i * x * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e))) powr p

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i * x) powr p * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p = (bs ! i * x * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e))) powr p

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
have "bs!i*x*(1 - s*hb*inverse (bs!i)*ln x powr -(1+e)) = bs!i*x - s*hb*x*ln x powr -(1+e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs ! i * x * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) = bs ! i * x - s * hb * x * ln x powr - (1 + e)
[PROOF STEP]
using b_pos assms
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i
bs ! i \<noteq> 0
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. bs ! i * x * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) = bs ! i * x - s * hb * x * ln x powr - (1 + e)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
bs ! i * x * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) = bs ! i * x - s * hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bs ! i * x * (1 - s * hb * inverse (bs ! i) * ln x powr - (1 + e)) = bs ! i * x - s * hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
have "?B = 1 + ln (bs!i*x + hb*x*ln x powr -(1+e)) powr (-e/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2) = 1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2)
[PROOF STEP]
by (subst powr_minus) (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2) = 1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2) = 1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
1 + ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2) = 1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
from x assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "(bs!i*x - s*hb*x*ln x powr -(1+e)) powr p \<le> (bs!i*x + (hs!i) x) powr p"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
[PROOF STEP]
using asymptotics_aux(1)[OF assms(1,2) s_def]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
x\<^sub>1 \<le> x
i < k
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p

goal (1 subgoal):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
have "(hs!i) x \<le> \<bar>(hs!i) x\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hs ! i) x \<le> \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have "\<bar>(hs!i) x\<bar> \<le> hb * x / ln x powr (1+e)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. \<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)
[PROOF STEP]
by (intro h_bounds) simp_all
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(hs ! i) x \<le> hb * x / ln x powr (1 + e)
[PROOF STEP]
have "(hs ! i) x \<le> hb * x * ln x powr -(1 + e)"
[PROOF STATE]
proof (prove)
using this:
(hs ! i) x \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. (hs ! i) x \<le> hb * x * ln x powr - (1 + e)
[PROOF STEP]
by (subst powr_minus) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
from x hb_nonneg x0_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x
0 \<le> hb
0 < x\<^sub>0
[PROOF STEP]
have "hb * x * ln x powr -(1+e) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x
0 \<le> hb
0 < x\<^sub>0

goal (1 subgoal):
 1. 0 \<le> hb * x * ln x powr - (1 + e)
[PROOF STEP]
by (intro mult_nonneg_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(hs ! i) x \<le> hb * x * ln x powr - (1 + e)
0 \<le> hb * x * ln x powr - (1 + e)
[PROOF STEP]
have "1 + ln (bs!i*x + hb * x * ln x powr -(1+e)) powr (-e/2) \<le>
                       1 + ln (bs!i*x + (hs!i) x) powr (-e/2)"
[PROOF STATE]
proof (prove)
using this:
(hs ! i) x \<le> hb * x * ln x powr - (1 + e)
0 \<le> hb * x * ln x powr - (1 + e)

goal (1 subgoal):
 1. 1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2) \<le> 1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)
[PROOF STEP]
using assms x e_pos b_pos x0_pos
[PROOF STATE]
proof (prove)
using this:
(hs ! i) x \<le> hb * x * ln x powr - (1 + e)
0 \<le> hb * x * ln x powr - (1 + e)
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x
0 < e
0 < bs ! i
bs ! i \<noteq> 0
0 < x\<^sub>0

goal (1 subgoal):
 1. 1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2) \<le> 1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)
[PROOF STEP]
by (intro add_left_mono powr_mono2' ln_mono ln_gt_zero step_pos x0_hb_bound7'
                add_pos_nonneg mult_pos_pos) simp_all
[PROOF STATE]
proof (state)
this:
1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2) \<le> 1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2) \<le> 1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2) \<le> 1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)
[PROOF STEP]
have "(bs!i*x - s*hb*x*ln x powr -(1+e)) powr p *
                         (1 + ln (bs!i*x + hb * x * ln x powr -(1+e)) powr (-e/2))
                     \<le> (bs!i*x + (hs!i) x) powr p * (1 + ln (bs!i*x + (hs!i) x) powr (-e/2))"
[PROOF STATE]
proof (prove)
using this:
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p \<le> (bs ! i * x + (hs ! i) x) powr p
1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2) \<le> 1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
by (rule mult_mono) simp_all
[PROOF STATE]
proof (state)
this:
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(bs ! i * x - s * hb * x * ln x powr - (1 + e)) powr p * (1 + ln (bs ! i * x + hb * x * ln x powr - (1 + e)) powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> (bs ! i * x) powr p * xa \<le> (bs ! i * x) powr p * y) \<Longrightarrow> (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> (bs ! i * x) powr p * xa \<le> (bs ! i * x) powr p * y) \<Longrightarrow> (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
by (simp_all add: mono)
[PROOF STATE]
proof (state)
this:
(bs ! i * x) powr p * (1 + ln x powr (- e / 2)) \<le> (bs ! i * x + (hs ! i) x) powr p * (1 + ln (bs ! i * x + (hs ! i) x) powr (- e / 2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma asymptotics2':
  assumes "x \<ge> x\<^sub>1" "i < k"
  shows   "(bs!i*x + (hs!i) x) powr p * (1 - ln (bs!i*x + (hs!i) x) powr (-e/2)) \<le>
           (bs!i*x) powr p * (1 - ln x powr (-e/2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
define s :: real where "s = (if p \<ge> 0 then 1 else -1)"
[PROOF STATE]
proof (state)
this:
s = (if 0 \<le> p then 1 else - 1)

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have x: "x \<ge> x\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. x\<^sub>0 \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
from assms x1_gt_1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
1 < x\<^sub>1
[PROOF STEP]
have ln_x_pos: "ln x > 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
1 < x\<^sub>1

goal (1 subgoal):
 1. 0 < ln x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < ln x

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
from b_pos[of "bs!i"] assms
[PROOF STATE]
proof (chain)
picking this:
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have b_pos: "bs!i > 0" "bs!i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. 0 < bs ! i &&& bs ! i \<noteq> 0
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
0 < bs ! i
bs ! i \<noteq> 0

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
from b_pos hb_nonneg
[PROOF STATE]
proof (chain)
picking this:
0 < bs ! i
bs ! i \<noteq> 0
0 \<le> hb
[PROOF STEP]
have pos: "1 + s * hb * (inverse (bs!i) * ln x powr -(1+e)) > 0"
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i
bs ! i \<noteq> 0
0 \<le> hb

goal (1 subgoal):
 1. 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))
[PROOF STEP]
using x0_hb_bound0'[OF x, of "bs!i"] b_pos assms ln_x_pos
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i
bs ! i \<noteq> 0
0 \<le> hb
bs ! i \<in> set bs \<Longrightarrow> hb / ln x powr (1 + e) < bs ! i
0 < bs ! i
bs ! i \<noteq> 0
x\<^sub>1 \<le> x
i < k
0 < ln x

goal (1 subgoal):
 1. 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))
[PROOF STEP]
by (subst powr_minus) (simp add: field_simps s_def)
[PROOF STATE]
proof (state)
this:
0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
have mono: "\<And>a b. a \<le> b \<Longrightarrow> (bs!i*x) powr p * a \<le> (bs!i*x) powr p * b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. a \<le> b \<Longrightarrow> (bs ! i * x) powr p * a \<le> (bs ! i * x) powr p * b
[PROOF STEP]
by (rule mult_left_mono) simp_all
[PROOF STATE]
proof (state)
this:
?a \<le> ?b \<Longrightarrow> (bs ! i * x) powr p * ?a \<le> (bs ! i * x) powr p * ?b

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
let ?A = "(1 + s*hb*inverse(bs!i)*ln x powr -(1+e)) powr p"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
let ?B = "1 - ln (bs!i*x + (hs!i) x) powr (-e/2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
let ?B' = "1 - ln (bs!i*x + hb * x / ln x powr (1+e)) powr (-e/2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
from assms x
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x
[PROOF STEP]
have "(bs!i*x + (hs!i) x) powr p \<le> (bs!i*x + s*hb*x*ln x powr -(1+e)) powr p"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
[PROOF STEP]
by (intro asymptotics_aux(2)) (simp_all add: s_def)
[PROOF STATE]
proof (state)
this:
(bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
from x0_hb_bound9[OF assms(1,2)]
[PROOF STATE]
proof (chain)
picking this:
ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1
[PROOF STEP]
have "?B \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
ln (bs ! i * x + (hs ! i) x) powr - (e / 2) < 1

goal (1 subgoal):
 1. 0 \<le> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
0 \<le> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
0 \<le> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)
[PROOF STEP]
have "(bs!i*x + (hs!i) x) powr p * ?B \<le>
                   (bs!i*x + s*hb*x*ln x powr -(1+e)) powr p * ?B"
[PROOF STATE]
proof (prove)
using this:
(bs ! i * x + (hs ! i) x) powr p \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p
0 \<le> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2))
[PROOF STEP]
by (rule mult_right_mono)
[PROOF STATE]
proof (state)
this:
(bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
from assms e_pos pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
0 < e
0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))
[PROOF STEP]
have "?B \<le> ?B'"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
0 < e
0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))

goal (1 subgoal):
 1. 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
from x0_hb_bound8'[OF assms(1,2)] x0_hb_bound8[OF assms(1,2)] x0_ge_1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
1 \<le> x\<^sub>0
[PROOF STEP]
have *: "bs ! i * x + s*hb * x / ln x powr (1 + e) > 1"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 < bs ! i * x + hb * x / ln x powr (1 + e)
x\<^sub>0 < bs ! i * x - hb * x / ln x powr (1 + e)
1 \<le> x\<^sub>0

goal (1 subgoal):
 1. 1 < bs ! i * x + s * hb * x / ln x powr (1 + e)
[PROOF STEP]
by (simp add: s_def)
[PROOF STATE]
proof (state)
this:
1 < bs ! i * x + s * hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 < bs ! i * x + s * hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
1 < bs ! i * x + s * hb * x / ln x powr (1 + e)
[PROOF STEP]
have "... > 0"
[PROOF STATE]
proof (prove)
using this:
1 < bs ! i * x + s * hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. 0 < bs ! i * x + s * hb * x / ln x powr (1 + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < bs ! i * x + s * hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < bs ! i * x + s * hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
from x0_hb_bound7[OF assms(1,2)] x0_ge_1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 < bs ! i * x + (hs ! i) x
1 \<le> x\<^sub>0
[PROOF STEP]
have "bs ! i * x + (hs ! i) x > 1"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 < bs ! i * x + (hs ! i) x
1 \<le> x\<^sub>0

goal (1 subgoal):
 1. 1 < bs ! i * x + (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
1 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
have "(hs!i) x \<le> \<bar>(hs!i) x\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (hs ! i) x \<le> \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(hs ! i) x \<le> \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
from assms x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "... \<le> hb*x/ln x powr (1+e)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. \<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)
[PROOF STEP]
by (intro h_bounds) simp_all
[PROOF STATE]
proof (state)
this:
\<bar>(hs ! i) x\<bar> \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(hs ! i) x \<le> hb * x / ln x powr (1 + e)
[PROOF STEP]
have "bs!i*x + (hs!i) x \<le> bs!i*x + hb*x/ln x powr (1+e)"
[PROOF STATE]
proof (prove)
using this:
(hs ! i) x \<le> hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; 0 < e; 0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))\<rbrakk> \<Longrightarrow> 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 < bs ! i * x + s * hb * x / ln x powr (1 + e)
0 < bs ! i * x + s * hb * x / ln x powr (1 + e)
1 < bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x / ln x powr (1 + e)
[PROOF STEP]
show "?B \<le> ?B'"
[PROOF STATE]
proof (prove)
using this:
1 < bs ! i * x + s * hb * x / ln x powr (1 + e)
0 < bs ! i * x + s * hb * x / ln x powr (1 + e)
1 < bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
using assms e_pos x step_pos
[PROOF STATE]
proof (prove)
using this:
1 < bs ! i * x + s * hb * x / ln x powr (1 + e)
0 < bs ! i * x + s * hb * x / ln x powr (1 + e)
1 < bs ! i * x + (hs ! i) x
bs ! i * x + (hs ! i) x \<le> bs ! i * x + hb * x / ln x powr (1 + e)
x\<^sub>1 \<le> x
i < k
0 < e
x\<^sub>0 \<le> x
\<lbrakk>?i < k; x\<^sub>1 \<le> ?x\<rbrakk> \<Longrightarrow> 0 < bs ! ?i * ?x + (hs ! ?i) ?x

goal (1 subgoal):
 1. 1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)
[PROOF STEP]
by (intro diff_left_mono powr_mono2' ln_mono ln_gt_zero) simp_all
[PROOF STATE]
proof (state)
this:
1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
hence "(bs!i*x + s*hb*x*ln x powr -(1+e)) powr p * ?B \<le>
             (bs!i*x + s*hb*x*ln x powr -(1+e)) powr p * ?B'"
[PROOF STATE]
proof (prove)
using this:
1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2) \<le> 1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))
[PROOF STEP]
by (intro mult_left_mono) simp_all
[PROOF STATE]
proof (state)
this:
(bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x + s * hb * x * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
have "bs!i*x + s*hb*x*ln x powr -(1+e) = bs!i*x*(1 + s*hb*inverse (bs!i)*ln x powr -(1+e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bs ! i * x + s * hb * x * ln x powr - (1 + e) = bs ! i * x * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e))
[PROOF STEP]
using b_pos
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i
bs ! i \<noteq> 0

goal (1 subgoal):
 1. bs ! i * x + s * hb * x * ln x powr - (1 + e) = bs ! i * x * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e))
[PROOF STEP]
by (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
bs ! i * x + s * hb * x * ln x powr - (1 + e) = bs ! i * x * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bs ! i * x + s * hb * x * ln x powr - (1 + e) = bs ! i * x * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
have "... powr p = (bs!i*x) powr p * ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i * x * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e))) powr p = (bs ! i * x) powr p * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p
[PROOF STEP]
using b_pos x x0_pos pos
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i
bs ! i \<noteq> 0
x\<^sub>0 \<le> x
0 < x\<^sub>0
0 < 1 + s * hb * (inverse (bs ! i) * ln x powr - (1 + e))

goal (1 subgoal):
 1. (bs ! i * x * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e))) powr p = (bs ! i * x) powr p * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p
[PROOF STEP]
by (intro powr_mult) simp_all
[PROOF STATE]
proof (state)
this:
(bs ! i * x * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e))) powr p = (bs ! i * x) powr p * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i * x * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e))) powr p = (bs ! i * x) powr p * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
have "(bs!i*x) powr p * ?A * ?B' = (bs!i*x) powr p * (?A * ?B')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i * x) powr p * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) = (bs ! i * x) powr p * ((1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(bs ! i * x) powr p * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) = (bs ! i * x) powr p * ((1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i * x) powr p * (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) = (bs ! i * x) powr p * ((1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
have "?A * ?B' \<le> 1 - ln x powr (-e/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) \<le> 1 - ln x powr (- e / 2)
[PROOF STEP]
using assms x
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x

goal (1 subgoal):
 1. (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) \<le> 1 - ln x powr (- e / 2)
[PROOF STEP]
using asymptotics2[OF x assms(2)] asymptotics2'[OF x assms(2)]
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x
(1 + hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) \<le> 1 - ln x powr (- e / 2)
(1 - hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) \<le> 1 - ln x powr (- e / 2)

goal (1 subgoal):
 1. (1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) \<le> 1 - ln x powr (- e / 2)
[PROOF STEP]
by (simp add: s_def)
[PROOF STATE]
proof (state)
this:
(1 + s * hb * inverse (bs ! i) * ln x powr - (1 + e)) powr p * (1 - ln (bs ! i * x + hb * x / ln x powr (1 + e)) powr (- e / 2)) \<le> 1 - ln x powr (- e / 2)

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> (bs ! i * x) powr p * xa \<le> (bs ! i * x) powr p * y) \<Longrightarrow> (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> (bs ! i * x) powr p * xa \<le> (bs ! i * x) powr p * y) \<Longrightarrow> (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))
[PROOF STEP]
by (simp_all add: mono)
[PROOF STATE]
proof (state)
this:
(bs ! i * x + (hs ! i) x) powr p * (1 - ln (bs ! i * x + (hs ! i) x) powr (- e / 2)) \<le> (bs ! i * x) powr p * (1 - ln x powr (- e / 2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Cx_le_step:
  assumes "i < k" "x \<ge> x\<^sub>1"
  shows   "C*x \<le> bs!i*x + (hs!i) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
[PROOF STEP]
have "C*x \<le> bs!i*x - hb*x/ln x powr (1+e)"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. C * x \<le> bs ! i * x - hb * x / ln x powr (1 + e)
[PROOF STEP]
by (intro C_bound) simp_all
[PROOF STATE]
proof (state)
this:
C * x \<le> bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
C * x \<le> bs ! i * x - hb * x / ln x powr (1 + e)

goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
[PROOF STEP]
have "-(hb*x/ln x powr (1+e)) \<le> -\<bar>(hs!i) x\<bar>"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. - (hb * x / ln x powr (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by (subst neg_le_iff_le, intro h_bounds) simp_all
[PROOF STATE]
proof (state)
this:
- (hb * x / ln x powr (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
hence "bs!i*x - hb*x/ln x powr (1+e) \<le> bs!i*x + -\<bar>(hs!i) x\<bar>"
[PROOF STATE]
proof (prove)
using this:
- (hb * x / ln x powr (1 + e)) \<le> - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + - \<bar>(hs ! i) x\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bs ! i * x - hb * x / ln x powr (1 + e) \<le> bs ! i * x + - \<bar>(hs ! i) x\<bar>

goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
have "-\<bar>(hs!i) x\<bar> \<le> (hs!i) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- \<bar>(hs ! i) x\<bar> \<le> (hs ! i) x

goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> bs ! i * x + xa \<le> bs ! i * x + y) \<Longrightarrow> C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> bs ! i * x + xa \<le> bs ! i * x + y) \<Longrightarrow> C * x \<le> bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C * x \<le> bs ! i * x + (hs ! i) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f'_base: "x \<ge> x\<^sub>0 \<Longrightarrow> x \<le> x\<^sub>1 \<Longrightarrow> f' x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 0 \<le> f' x
[PROOF STEP]
apply (subst f'.simps(1), assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> 0 \<le> f (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
apply (rule f_base)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> x\<^sub>0 \<le> real (nat \<lfloor>x\<rfloor>)
 2. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> real (nat \<lfloor>x\<rfloor>) \<le> x\<^sub>1
[PROOF STEP]
apply (rule order.trans[of _ "real (nat \<lfloor>x\<^sub>0\<rfloor>)"], simp add: x0_int)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> real (nat \<lfloor>x\<^sub>0\<rfloor>) \<le> real (nat \<lfloor>x\<rfloor>)
 2. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> real (nat \<lfloor>x\<rfloor>) \<le> x\<^sub>1
[PROOF STEP]
apply (subst of_nat_le_iff, intro nat_mono floor_mono, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> real (nat \<lfloor>x\<rfloor>) \<le> x\<^sub>1
[PROOF STEP]
using x0_pos
[PROOF STATE]
proof (prove)
using this:
0 < x\<^sub>0

goal (1 subgoal):
 1. \<lbrakk>x\<^sub>0 \<le> x; x \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> real (nat \<lfloor>x\<rfloor>) \<le> x\<^sub>1
[PROOF STEP]
apply linarith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gb2_nonneg: "gb2 \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> gb2
[PROOF STEP]
using g_bounded[of x\<^sub>0] x0_le_x1 x0_pos g_nonneg[of x\<^sub>0]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>0 \<le> x\<^sub>0; x\<^sub>0 \<le> x\<^sub>1\<rbrakk> \<Longrightarrow> g x\<^sub>0 \<le> gb2
x\<^sub>0 \<le> x\<^sub>1
0 < x\<^sub>0
x\<^sub>0 \<le> x\<^sub>0 \<Longrightarrow> 0 \<le> g x\<^sub>0

goal (1 subgoal):
 1. 0 \<le> gb2
[PROOF STEP]
by simp


[STATEMENT]
lemma g_growth2':
  assumes "x \<ge> x\<^sub>1" "i < k" "u \<in> {bs!i*x+(hs!i) x..x}"
  shows   "c2 * g x \<ge> g u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g u \<le> c2 * g x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g u \<le> c2 * g x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
[PROOF STEP]
have "C*x \<le> bs!i*x+(hs!i) x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}

goal (1 subgoal):
 1. C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
by (intro Cx_le_step)
[PROOF STATE]
proof (state)
this:
C * x \<le> bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. g u \<le> c2 * g x
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
C * x \<le> bs ! i * x + (hs ! i) x
[PROOF STEP]
have "u \<in> {C*x..x}"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
C * x \<le> bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. u \<in> {C * x..x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<in> {C * x..x}

goal (1 subgoal):
 1. g u \<le> c2 * g x
[PROOF STEP]
with assms g_growth2
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
\<forall>x\<ge>x\<^sub>1. \<forall>u\<in>{C * x..x}. g u \<le> c2 * g x
u \<in> {C * x..x}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
u \<in> {bs ! i * x + (hs ! i) x..x}
\<forall>x\<ge>x\<^sub>1. \<forall>u\<in>{C * x..x}. g u \<le> c2 * g x
u \<in> {C * x..x}

goal (1 subgoal):
 1. g u \<le> c2 * g x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g u \<le> c2 * g x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma g_bounds2:
  obtains c4 where "\<And>x i. x \<ge> x\<^sub>1 \<Longrightarrow> i < k \<Longrightarrow> g_approx i x \<le> c4 * g x" "c4 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define c4
    where "c4 = Max {c2 / min 1 (min ((b/2) powr (p+1)) ((b*3/2) powr (p+1))) |b. b \<in> set bs}"
[PROOF STATE]
proof (state)
this:
c4 = Max {c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1))) |b. b \<in> set bs}

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
c4 = Max {c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1))) |b. b \<in> set bs}

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from bs_nonempty
[PROOF STATE]
proof (chain)
picking this:
bs \<noteq> []
[PROOF STEP]
obtain b where b: "b \<in> set bs"
[PROOF STATE]
proof (prove)
using this:
bs \<noteq> []

goal (1 subgoal):
 1. (\<And>b. b \<in> set bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases bs) auto
[PROOF STATE]
proof (state)
this:
b \<in> set bs

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m = "min 1 (min ((b/2) powr (p+1)) ((b*3/2) powr (p+1)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from b b_pos
[PROOF STATE]
proof (chain)
picking this:
b \<in> set bs
?b \<in> set bs \<Longrightarrow> 0 < ?b
[PROOF STEP]
have "?m > 0"
[PROOF STATE]
proof (prove)
using this:
b \<in> set bs
?b \<in> set bs \<Longrightarrow> 0 < ?b

goal (1 subgoal):
 1. 0 < min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))
[PROOF STEP]
unfolding min_def
[PROOF STATE]
proof (prove)
using this:
b \<in> set bs
?b \<in> set bs \<Longrightarrow> 0 < ?b

goal (1 subgoal):
 1. 0 < (if 1 \<le> (if (b / 2) powr (p + 1) \<le> (b * 3 / 2) powr (p + 1) then (b / 2) powr (p + 1) else (b * 3 / 2) powr (p + 1)) then 1 else if (b / 2) powr (p + 1) \<le> (b * 3 / 2) powr (p + 1) then (b / 2) powr (p + 1) else (b * 3 / 2) powr (p + 1))
[PROOF STEP]
by (auto simp: not_le)
[PROOF STATE]
proof (state)
this:
0 < min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with b b_pos c2_pos
[PROOF STATE]
proof (chain)
picking this:
b \<in> set bs
?b \<in> set bs \<Longrightarrow> 0 < ?b
0 < c2
0 < min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))
[PROOF STEP]
have "c2 / ?m > 0"
[PROOF STATE]
proof (prove)
using this:
b \<in> set bs
?b \<in> set bs \<Longrightarrow> 0 < ?b
0 < c2
0 < min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. 0 < c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))
[PROOF STEP]
by (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
0 < c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
b \<in> set bs
0 < c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))
[PROOF STEP]
have "c4 > 0"
[PROOF STATE]
proof (prove)
using this:
b \<in> set bs
0 < c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. 0 < c4
[PROOF STEP]
unfolding c4_def
[PROOF STATE]
proof (prove)
using this:
b \<in> set bs
0 < c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. 0 < Max {c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1))) |b. b \<in> set bs}
[PROOF STEP]
by (subst Max_gr_iff) (simp, simp, blast)
[PROOF STATE]
proof (state)
this:
0 < c4

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
0 < c4

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < c4

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume i: "i < k" and x: "x \<ge> x\<^sub>1"
[PROOF STATE]
proof (state)
this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have powr_negD: "a powr b \<le> 0 \<Longrightarrow> a = 0"
      for a b :: real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a powr b \<le> 0 \<Longrightarrow> a = 0
[PROOF STEP]
unfolding powr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a = 0 then 0 else exp (b * ln a)) \<le> 0 \<Longrightarrow> a = 0
[PROOF STEP]
by (simp split: if_split_asm)
[PROOF STATE]
proof (state)
this:
?a powr ?b \<le> 0 \<Longrightarrow> ?a = 0

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m = "min 1 (min ((bs!i/2) powr (p+1)) ((bs!i*3/2) powr (p+1)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "min 1 ((bs!i + (hs ! i) x / x) powr (p+1)) \<ge> min 1 (min ((bs!i/2) powr (p+1)) ((bs!i*3/2) powr (p+1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))
[PROOF STEP]
apply (insert x i x0_le_x1 x1_pos step_pos b_pos[OF b_in_bs[OF i]],
             rule min.mono, simp, cases "p + 1 \<ge> 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; x\<^sub>0 \<le> x\<^sub>1; 0 < x\<^sub>1; \<And>i x. \<lbrakk>i < k; x\<^sub>1 \<le> x\<rbrakk> \<Longrightarrow> 0 < bs ! i * x + (hs ! i) x; 0 < bs ! i; 0 \<le> p + 1\<rbrakk> \<Longrightarrow> min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)) \<le> (bs ! i + (hs ! i) x / x) powr (p + 1)
 2. \<lbrakk>x\<^sub>1 \<le> x; i < k; x\<^sub>0 \<le> x\<^sub>1; 0 < x\<^sub>1; \<And>i x. \<lbrakk>i < k; x\<^sub>1 \<le> x\<rbrakk> \<Longrightarrow> 0 < bs ! i * x + (hs ! i) x; 0 < bs ! i; \<not> 0 \<le> p + 1\<rbrakk> \<Longrightarrow> min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)) \<le> (bs ! i + (hs ! i) x / x) powr (p + 1)
[PROOF STEP]
apply (rule order.trans[OF min.cobounded1 powr_mono2[OF _ _ x0_hb_bound4']], simp_all add: field_simps) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x\<^sub>1 \<le> x; i < k; x\<^sub>0 \<le> x\<^sub>1; 0 < x\<^sub>1; \<And>i x. \<lbrakk>i < k; x\<^sub>1 \<le> x\<rbrakk> \<Longrightarrow> 0 < bs ! i * x + (hs ! i) x; 0 < bs ! i; \<not> 0 \<le> p + 1\<rbrakk> \<Longrightarrow> min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)) \<le> (bs ! i + (hs ! i) x / x) powr (p + 1)
[PROOF STEP]
apply (rule order.trans[OF min.cobounded2 powr_mono2'[OF _ _ x0_hb_bound5]], simp_all add: field_simps) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with i b_pos[of "bs!i"]
[PROOF STATE]
proof (chain)
picking this:
i < k
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))
[PROOF STEP]
have "c2 / min 1 ((bs!i + (hs ! i) x / x) powr (p+1)) \<le> c2 / ?m"
[PROOF STATE]
proof (prove)
using this:
i < k
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))

goal (1 subgoal):
 1. c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c2 / min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))
[PROOF STEP]
using c2_pos
[PROOF STATE]
proof (prove)
using this:
i < k
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))
0 < c2

goal (1 subgoal):
 1. c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c2 / min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))
[PROOF STEP]
unfolding min_def
[PROOF STATE]
proof (prove)
using this:
i < k
bs ! i \<in> set bs \<Longrightarrow> 0 < bs ! i
(if 1 \<le> (if (bs ! i / 2) powr (p + 1) \<le> (bs ! i * 3 / 2) powr (p + 1) then (bs ! i / 2) powr (p + 1) else (bs ! i * 3 / 2) powr (p + 1)) then 1 else if (bs ! i / 2) powr (p + 1) \<le> (bs ! i * 3 / 2) powr (p + 1) then (bs ! i / 2) powr (p + 1) else (bs ! i * 3 / 2) powr (p + 1)) \<le> (if 1 \<le> (bs ! i + (hs ! i) x / x) powr (p + 1) then 1 else (bs ! i + (hs ! i) x / x) powr (p + 1))
0 < c2

goal (1 subgoal):
 1. c2 / (if 1 \<le> (bs ! i + (hs ! i) x / x) powr (p + 1) then 1 else (bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c2 / (if 1 \<le> (if (bs ! i / 2) powr (p + 1) \<le> (bs ! i * 3 / 2) powr (p + 1) then (bs ! i / 2) powr (p + 1) else (bs ! i * 3 / 2) powr (p + 1)) then 1 else if (bs ! i / 2) powr (p + 1) \<le> (bs ! i * 3 / 2) powr (p + 1) then (bs ! i / 2) powr (p + 1) else (bs ! i * 3 / 2) powr (p + 1))
[PROOF STEP]
by (intro divide_left_mono) (auto intro!: mult_pos_pos dest!: powr_negD)
[PROOF STATE]
proof (state)
this:
c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c2 / min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c2 / min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from i x
[PROOF STATE]
proof (chain)
picking this:
i < k
x\<^sub>1 \<le> x
[PROOF STEP]
have "... \<le> c4"
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. c2 / min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> c4
[PROOF STEP]
unfolding c4_def
[PROOF STATE]
proof (prove)
using this:
i < k
x\<^sub>1 \<le> x

goal (1 subgoal):
 1. c2 / min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> Max {c2 / min 1 (min ((b / 2) powr (p + 1)) ((b * 3 / 2) powr (p + 1))) |b. b \<in> set bs}
[PROOF STEP]
by (intro Max.coboundedI) auto
[PROOF STATE]
proof (state)
this:
c2 / min 1 (min ((bs ! i / 2) powr (p + 1)) ((bs ! i * 3 / 2) powr (p + 1))) \<le> c4

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c4
[PROOF STEP]
have "c2 / min 1 ((bs!i + (hs ! i) x / x) powr (p+1)) \<le> c4"
[PROOF STATE]
proof (prove)
using this:
c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c4

goal (1 subgoal):
 1. c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c4
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) \<le> c4

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < k; x\<^sub>1 \<le> ?x2\<rbrakk> \<Longrightarrow> c2 / min 1 ((bs ! ?i2 + (hs ! ?i2) ?x2 / ?x2) powr (p + 1)) \<le> c4

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
note c4 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < k; x\<^sub>1 \<le> ?x2\<rbrakk> \<Longrightarrow> c2 / min 1 ((bs ! ?i2 + (hs ! ?i2) ?x2 / ?x2) powr (p + 1)) \<le> c4

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i2 < k; x\<^sub>1 \<le> ?x2\<rbrakk> \<Longrightarrow> c2 / min 1 ((bs ! ?i2 + (hs ! ?i2) ?x2 / ?x2) powr (p + 1)) \<le> c4

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix x :: real and i :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume x: "x \<ge> x\<^sub>1" and i: "i < k"
[PROOF STATE]
proof (state)
this:
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
0 < x\<^sub>1
[PROOF STEP]
have x_pos: "x > 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
0 < x\<^sub>1

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

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?x' = "bs ! i * x + (hs ! i) x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?x'' = "bs ! i + (hs ! i) x / x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x x1_ge_1 i g_growth2' x0_le_x1 c2_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
1 \<le> x\<^sub>1
i < k
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k; ?u \<in> {bs ! ?i * ?x + (hs ! ?i) ?x..?x}\<rbrakk> \<Longrightarrow> g ?u \<le> c2 * g ?x
x\<^sub>0 \<le> x\<^sub>1
0 < c2
[PROOF STEP]
have c2: "c2 > 0" "\<forall>u\<in>{?x'..x}. g u \<le> c2 * g x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
1 \<le> x\<^sub>1
i < k
\<lbrakk>x\<^sub>1 \<le> ?x; ?i < k; ?u \<in> {bs ! ?i * ?x + (hs ! ?i) ?x..?x}\<rbrakk> \<Longrightarrow> g ?u \<le> c2 * g ?x
x\<^sub>0 \<le> x\<^sub>1
0 < c2

goal (1 subgoal):
 1. 0 < c2 &&& \<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x0_le_x1 x i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x\<^sub>1
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have x'_le_x: "?x' \<le> x"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x\<^sub>1
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. bs ! i * x + (hs ! i) x \<le> x
[PROOF STEP]
by (intro step_le_x) simp_all
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x \<le> x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?m = "min (?x' powr (p + 1)) (x powr (p + 1))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define m' where "m' = min 1 (?x'' powr (p + 1))"
[PROOF STATE]
proof (state)
this:
m' = min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have [simp]: "bs ! i > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < bs ! i
[PROOF STEP]
by (intro b_pos nth_mem) (simp add: i length_bs)
[PROOF STATE]
proof (state)
this:
0 < bs ! i

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x0_le_x1 x i
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>0 \<le> x\<^sub>1
x\<^sub>1 \<le> x
i < k
[PROOF STEP]
have [simp]: "?x' > 0"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>0 \<le> x\<^sub>1
x\<^sub>1 \<le> x
i < k

goal (1 subgoal):
 1. 0 < bs ! i * x + (hs ! i) x
[PROOF STEP]
by (intro step_pos) simp_all
[PROOF STATE]
proof (state)
this:
0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
0 < bs ! i * x + (hs ! i) x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume u: "u \<ge> ?x'" "u \<le> x"
[PROOF STATE]
proof (state)
this:
bs ! i * x + (hs ! i) x \<le> u
u \<le> x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "?m \<le> u powr (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> u powr (p + 1)
[PROOF STEP]
using x u
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
bs ! i * x + (hs ! i) x \<le> u
u \<le> x

goal (1 subgoal):
 1. min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> u powr (p + 1)
[PROOF STEP]
by (intro powr_lower_bound mult_pos_pos) simp_all
[PROOF STATE]
proof (state)
this:
min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> u powr (p + 1)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> u powr (p + 1)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from c2 and u
[PROOF STATE]
proof (chain)
picking this:
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x
bs ! i * x + (hs ! i) x \<le> u
u \<le> x
[PROOF STEP]
have "g u \<le> c2 * g x"
[PROOF STATE]
proof (prove)
using this:
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x
bs ! i * x + (hs ! i) x \<le> u
u \<le> x

goal (1 subgoal):
 1. g u \<le> c2 * g x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g u \<le> c2 * g x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> u powr (p + 1)
g u \<le> c2 * g x
[PROOF STEP]
have "g u * ?m \<le> c2 * g x * u powr (p + 1)"
[PROOF STATE]
proof (prove)
using this:
min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> u powr (p + 1)
g u \<le> c2 * g x

goal (1 subgoal):
 1. g u * min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> c2 * g x * u powr (p + 1)
[PROOF STEP]
using c2 x x1_pos x0_le_x1
[PROOF STATE]
proof (prove)
using this:
min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> u powr (p + 1)
g u \<le> c2 * g x
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x
x\<^sub>1 \<le> x
0 < x\<^sub>1
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. g u * min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> c2 * g x * u powr (p + 1)
[PROOF STEP]
by (intro mult_mono mult_nonneg_nonneg g_nonneg) auto
[PROOF STATE]
proof (state)
this:
g u * min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> c2 * g x * u powr (p + 1)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>bs ! i * x + (hs ! i) x \<le> ?u2; ?u2 \<le> x\<rbrakk> \<Longrightarrow> g ?u2 * min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> c2 * g x * ?u2 powr (p + 1)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence "integral (\<lambda>u. g u / u powr (p+1)) ?x' x \<le> integral (\<lambda>u. c2 * g x / ?m) ?x' x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bs ! i * x + (hs ! i) x \<le> ?u2; ?u2 \<le> x\<rbrakk> \<Longrightarrow> g ?u2 * min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> c2 * g x * ?u2 powr (p + 1)

goal (1 subgoal):
 1. integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> integral (\<lambda>u. c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
using x_pos step_pos[OF i x] x0_hb_bound7[OF x i] c2 x x0_le_x1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>bs ! i * x + (hs ! i) x \<le> ?u2; ?u2 \<le> x\<rbrakk> \<Longrightarrow> g ?u2 * min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)) \<le> c2 * g x * ?u2 powr (p + 1)
0 < x
0 < bs ! i * x + (hs ! i) x
x\<^sub>0 < bs ! i * x + (hs ! i) x
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> integral (\<lambda>u. c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x
[PROOF STEP]
by (intro integral_le x'_le_x akra_bazzi_integrable ballI integrable_const)
         (auto simp: field_simps intro!: mult_nonneg_nonneg g_nonneg)
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> integral (\<lambda>u. c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> integral (\<lambda>u. c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x0_pos x x0_le_x1 x'_le_x c2
[PROOF STATE]
proof (chain)
picking this:
0 < x\<^sub>0
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
bs ! i * x + (hs ! i) x \<le> x
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x
[PROOF STEP]
have "... = (x - ?x') * (c2 * g x / ?m)"
[PROOF STATE]
proof (prove)
using this:
0 < x\<^sub>0
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
bs ! i * x + (hs ! i) x \<le> x
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x

goal (1 subgoal):
 1. integral (\<lambda>u. c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x = (x - (bs ! i * x + (hs ! i) x)) * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)))
[PROOF STEP]
by (subst integral_const) (simp_all add: g_nonneg)
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x = (x - (bs ! i * x + (hs ! i) x)) * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral (\<lambda>u. c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) (bs ! i * x + (hs ! i) x) x = (x - (bs ! i * x + (hs ! i) x)) * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from c2 x_pos x x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x
0 < x
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1
[PROOF STEP]
have "c2 * g x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
0 < c2
\<forall>u\<in>{bs ! i * x + (hs ! i) x..x}. g u \<le> c2 * g x
0 < x
x\<^sub>1 \<le> x
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. 0 \<le> c2 * g x
[PROOF STEP]
by (intro mult_nonneg_nonneg g_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> c2 * g x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with x i x0_le_x1
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
0 \<le> c2 * g x
[PROOF STEP]
have "(x - ?x') * (c2 * g x / ?m) \<le> x * (c2 * g x / ?m)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> x\<^sub>1
0 \<le> c2 * g x

goal (1 subgoal):
 1. (x - (bs ! i * x + (hs ! i) x)) * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) \<le> x * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)))
[PROOF STEP]
by (intro x0_hb_bound3 mult_right_mono) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
(x - (bs ! i * x + (hs ! i) x)) * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) \<le> x * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x - (bs ! i * x + (hs ! i) x)) * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1))) \<le> x * (c2 * g x / min ((bs ! i * x + (hs ! i) x) powr (p + 1)) (x powr (p + 1)))

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "x powr (p + 1) = x powr (p + 1) * 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr (p + 1) = x powr (p + 1) * 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x powr (p + 1) = x powr (p + 1) * 1

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x powr (p + 1) = x powr (p + 1) * 1

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "(bs ! i * x + (hs ! i) x) powr (p + 1) =
               (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr (p + 1) = (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)
[PROOF STEP]
using x x1_pos step_pos[OF i x] x_pos i x0_le_x1
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
0 < x\<^sub>1
0 < bs ! i * x + (hs ! i) x
0 < x
i < k
x\<^sub>0 \<le> x\<^sub>1

goal (1 subgoal):
 1. (bs ! i * x + (hs ! i) x) powr (p + 1) = (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)
[PROOF STEP]
by (subst powr_mult[symmetric]) (simp add: field_simps, simp, simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
(bs ! i * x + (hs ! i) x) powr (p + 1) = (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i * x + (hs ! i) x) powr (p + 1) = (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "... = x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1) = x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1) = x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(bs ! i + (hs ! i) x / x) powr (p + 1) * x powr (p + 1) = x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have "min ... (x powr (p + 1) * 1) = x powr (p + 1) * m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1) = x powr (p + 1) * m'
[PROOF STEP]
unfolding m'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1) = x powr (p + 1) * min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))
[PROOF STEP]
using x_pos
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. min (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1) = x powr (p + 1) * min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1))
[PROOF STEP]
by (subst min.commute, intro min_mult_left[symmetric]) simp
[PROOF STATE]
proof (state)
this:
min (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1) = x powr (p + 1) * m'

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
min (x powr (p + 1) * (bs ! i + (hs ! i) x / x) powr (p + 1)) (x powr (p + 1) * 1) = x powr (p + 1) * m'

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x_pos
[PROOF STATE]
proof (chain)
picking this:
0 < x
[PROOF STEP]
have "x * (c2 * g x / (x powr (p + 1) * m')) = (c2/m') * (g x / x powr p)"
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. x * (c2 * g x / (x powr (p + 1) * m')) = c2 / m' * (g x / x powr p)
[PROOF STEP]
by (simp add: field_simps powr_add)
[PROOF STATE]
proof (state)
this:
x * (c2 * g x / (x powr (p + 1) * m')) = c2 / m' * (g x / x powr p)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x * (c2 * g x / (x powr (p + 1) * m')) = c2 / m' * (g x / x powr p)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x i g_nonneg x0_le_x1 x1_pos
[PROOF STATE]
proof (chain)
picking this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> g ?x
x\<^sub>0 \<le> x\<^sub>1
0 < x\<^sub>1
[PROOF STEP]
have "... \<le> c4 * (g x / x powr p)"
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> g ?x
x\<^sub>0 \<le> x\<^sub>1
0 < x\<^sub>1

goal (1 subgoal):
 1. c2 / m' * (g x / x powr p) \<le> c4 * (g x / x powr p)
[PROOF STEP]
unfolding m'_def
[PROOF STATE]
proof (prove)
using this:
x\<^sub>1 \<le> x
i < k
x\<^sub>0 \<le> ?x \<Longrightarrow> 0 \<le> g ?x
x\<^sub>0 \<le> x\<^sub>1
0 < x\<^sub>1

goal (1 subgoal):
 1. c2 / min 1 ((bs ! i + (hs ! i) x / x) powr (p + 1)) * (g x / x powr p) \<le> c4 * (g x / x powr p)
[PROOF STEP]
by (intro mult_right_mono c4) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
c2 / m' * (g x / x powr p) \<le> c4 * (g x / x powr p)

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> c4 * (g x / x powr p)
[PROOF STEP]
have "g_approx i x \<le> c4 * g x"
[PROOF STATE]
proof (prove)
using this:
integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> c4 * (g x / x powr p)

goal (1 subgoal):
 1. g_approx i x \<le> c4 * g x
[PROOF STEP]
unfolding g_approx_def
[PROOF STATE]
proof (prove)
using this:
integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> c4 * (g x / x powr p)

goal (1 subgoal):
 1. x powr p * integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> c4 * g x
[PROOF STEP]
using x_pos
[PROOF STATE]
proof (prove)
using this:
integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> c4 * (g x / x powr p)
0 < x

goal (1 subgoal):
 1. x powr p * integral (\<lambda>u. g u / u powr (p + 1)) (bs ! i * x + (hs ! i) x) x \<le> c4 * g x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
g_approx i x \<le> c4 * g x

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>x\<^sub>1 \<le> ?x2; ?i2 < k\<rbrakk> \<Longrightarrow> g_approx ?i2 ?x2 \<le> c4 * g ?x2

goal (1 subgoal):
 1. (\<And>c4. \<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> c4 * g x; 0 < c4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>1 \<le> ?x2; ?i2 < k\<rbrakk> \<Longrightarrow> g_approx ?i2 ?x2 \<le> c4 * g ?x2

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using that \<open>c4 > 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x\<^sub>1 \<le> ?x2; ?i2 < k\<rbrakk> \<Longrightarrow> g_approx ?i2 ?x2 \<le> c4 * g ?x2
\<lbrakk>\<And>x i. \<lbrakk>x\<^sub>1 \<le> x; i < k\<rbrakk> \<Longrightarrow> g_approx i x \<le> ?c4.0 * g x; 0 < ?c4.0\<rbrakk> \<Longrightarrow> thesis
0 < c4

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

goal:
No subgoals!
[PROOF STEP]
qed