[STATEMENT]
lemma bv_to_nat_emsapss_smaller_pq: assumes a: "prime p" and b: "prime q" and pneq: "p ~= q" and c: "emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []" shows "bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p*q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
from a and b and c
[PROOF STATE]
proof (chain)
picking this:
prime p
prime q
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime p
prime q
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []

goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
proof (cases "8 dvd ((length (nat_to_bv (p * q))) - Suc 0)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
 2. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
assume d: "8 dvd ((length (nat_to_bv (p * q))) - Suc 0)"
[PROOF STATE]
proof (state)
this:
8 dvd length (nat_to_bv (p * q)) - Suc 0

goal (2 subgoals):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
 2. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
8 dvd length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
have "2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p*q"
[PROOF STATE]
proof (prove)
using this:
8 dvd length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 8 dvd length (nat_to_bv (p * q)) - Suc 0 \<Longrightarrow> 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
[PROOF STEP]
from d
[PROOF STATE]
proof (chain)
picking this:
8 dvd length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
have e: "roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 = length (nat_to_bv (p * q)) - Suc 0"
[PROOF STATE]
proof (prove)
using this:
8 dvd length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 = length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
using rnddvd
[PROOF STATE]
proof (prove)
using this:
8 dvd length (nat_to_bv (p * q)) - Suc 0
?b dvd ?a \<Longrightarrow> roundup ?a ?b * ?b = ?a

goal (1 subgoal):
 1. roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 = length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 = length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. 8 dvd length (nat_to_bv (p * q)) - Suc 0 \<Longrightarrow> 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
[PROOF STEP]
have "p*q = bv_to_nat (nat_to_bv (p*q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * q = bv_to_nat (nat_to_bv (p * q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p * q = bv_to_nat (nat_to_bv (p * q))

goal (1 subgoal):
 1. 8 dvd length (nat_to_bv (p * q)) - Suc 0 \<Longrightarrow> 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p * q = bv_to_nat (nat_to_bv (p * q))
[PROOF STEP]
have "2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p*q"
[PROOF STATE]
proof (prove)
using this:
p * q = bv_to_nat (nat_to_bv (p * q))

goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p * q = bv_to_nat (nat_to_bv (p * q)) \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
[PROOF STEP]
have "0<p*q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < p * q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < p * q
[PROOF STEP]
have "0<p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < p
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
prime p

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

goal (1 subgoal):
 1. 0 < p * q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < p

goal (1 subgoal):
 1. 0 < p * q
[PROOF STEP]
have "0<q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < q
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
prime q

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

goal (1 subgoal):
 1. 0 < p * q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < p
0 < q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < p
0 < q

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

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

goal (1 subgoal):
 1. p * q = bv_to_nat (nat_to_bv (p * q)) \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < p * q

goal (1 subgoal):
 1. p * q = bv_to_nat (nat_to_bv (p * q)) \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
[PROOF STEP]
have "2^(length (nat_to_bv (p*q)) - Suc 0) ~= p*q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
proof (cases "2^(length (nat_to_bv (p*q)) - Suc 0) = p*q")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) = p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
 2. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
assume "2^(length (nat_to_bv (p*q)) - Suc 0) = p*q"
[PROOF STATE]
proof (state)
this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) = p * q

goal (2 subgoals):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) = p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
 2. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) = p * q
[PROOF STEP]
have "p=q"
[PROOF STATE]
proof (prove)
using this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) = p * q

goal (1 subgoal):
 1. p = q
[PROOF STEP]
using a and b and prime_equal
[PROOF STATE]
proof (prove)
using this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) = p * q
prime p
prime q
\<lbrakk>prime ?p; prime ?q; 2 ^ ?x = ?p * ?q\<rbrakk> \<Longrightarrow> ?p = ?q

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p = q

goal (2 subgoals):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) = p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
 2. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p = q

goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
using pneq
[PROOF STATE]
proof (prove)
using this:
p = q
p \<noteq> q

goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q

goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
assume "2^(length (nat_to_bv (p*q)) - Suc 0) ~= p*q"
[PROOF STATE]
proof (state)
this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q

goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q

goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q

goal (1 subgoal):
 1. p * q = bv_to_nat (nat_to_bv (p * q)) \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < p * q
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < p * q
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q

goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
[PROOF STEP]
using len_lower_bound[of "p*q"]
[PROOF STATE]
proof (prove)
using this:
0 < p * q
2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<noteq> p * q
0 < p * q \<Longrightarrow> 2 ^ (length (nat_to_bv (p * q)) - Suc 0) \<le> p * q

goal (1 subgoal):
 1. 2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q

goal (1 subgoal):
 1. 8 dvd length (nat_to_bv (p * q)) - Suc 0 \<Longrightarrow> 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q

goal (1 subgoal):
 1. 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
2 ^ (length (nat_to_bv (p * q)) - Suc 0) < p * q
roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8 = length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q

goal (2 subgoals):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
 2. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q

goal (2 subgoals):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
 2. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
[PROOF STEP]
have "bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0)8 * 8 )"
[PROOF STATE]
proof (prove)
using this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []

goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)
[PROOF STEP]
using bv_to_nat_emsapss_encode_le [of m "(length (nat_to_bv (p * q)) - Suc 0)"]
[PROOF STATE]
proof (prove)
using this:
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> [] \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)

goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)

goal (2 subgoals):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
 2. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) < p * q
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < 2 ^ (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)

goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q

goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
assume y: "~(8 dvd (length (nat_to_bv (p*q)) - Suc 0))"
[PROOF STATE]
proof (state)
this:
\<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0 \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
from y
[PROOF STATE]
proof (chain)
picking this:
\<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0
[PROOF STEP]
have x: "~((length (nat_to_bv (p * q)) - Suc 0) mod 8 = 0)"
[PROOF STATE]
proof (prove)
using this:
\<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0

goal (1 subgoal):
 1. (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
[PROOF STEP]
by (simp add: dvd_eq_mod_eq_0)
[PROOF STATE]
proof (state)
this:
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0

goal (1 subgoal):
 1. \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0 \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
from remzeroeq
[PROOF STATE]
proof (chain)
picking this:
bv_to_nat ?a = bv_to_nat (remzero ?a)
[PROOF STEP]
have d: "bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)))"
[PROOF STATE]
proof (prove)
using this:
bv_to_nat ?a = bv_to_nat (remzero ?a)

goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)))

goal (1 subgoal):
 1. \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0 \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
from a and b and c and x and length_emsapss_smaller_pq[of p q m]
[PROOF STATE]
proof (chain)
picking this:
prime p
prime q
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
\<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
[PROOF STEP]
have "bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p*q))"
[PROOF STATE]
proof (prove)
using this:
prime p
prime q
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
\<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))

goal (1 subgoal):
 1. bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p * q))
[PROOF STEP]
using length_lower[of "remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))" "nat_to_bv (p * q)"] and prime_hd_non_zero[of p q]
[PROOF STATE]
proof (prove)
using this:
prime p
prime q
emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []
(length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0
\<lbrakk>prime p; prime q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; (length (nat_to_bv (p * q)) - Suc 0) mod 8 \<noteq> 0\<rbrakk> \<Longrightarrow> length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q))
\<lbrakk>length (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < length (nat_to_bv (p * q)); hd (nat_to_bv (p * q)) \<noteq> \<zero>\<rbrakk> \<Longrightarrow> bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p * q))
\<lbrakk>prime p; prime q\<rbrakk> \<Longrightarrow> hd (nat_to_bv (p * q)) \<noteq> \<zero>

goal (1 subgoal):
 1. bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p * q))
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p * q))

goal (1 subgoal):
 1. \<not> 8 dvd length (nat_to_bv (p * q)) - Suc 0 \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p * q))
[PROOF STEP]
show "bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q"
[PROOF STATE]
proof (prove)
using this:
bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p * q))

goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
using d and bv_nat_bv
[PROOF STATE]
proof (prove)
using this:
bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) < bv_to_nat (nat_to_bv (p * q))
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = bv_to_nat (remzero (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)))
bv_to_nat (nat_to_bv ?n) = ?n

goal (1 subgoal):
 1. bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rsa_pss_verify: "\<lbrakk> prime p; prime q; p \<noteq> q; n = p*q; e*d mod ((pred p)*(pred q)) = 1; rsapss_sign m e n \<noteq> []; s = rsapss_sign m e n \<rbrakk> \<Longrightarrow> rsapss_verify m s d n = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = 1; rsapss_sign m e n \<noteq> []; s = rsapss_sign m e n\<rbrakk> \<Longrightarrow> rsapss_verify m s d n = True
[PROOF STEP]
apply (simp only: rsapss_sign_def rsapss_verify_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = 1; (if emsapss_encode m (length (nat_to_bv (p * q)) - 1) = [] then [] else rsapss_sign_help1 (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - 1))) e (p * q)) \<noteq> []; s = (if emsapss_encode m (length (nat_to_bv (p * q)) - 1) = [] then [] else rsapss_sign_help1 (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - 1))) e (p * q))\<rbrakk> \<Longrightarrow> (if length (if emsapss_encode m (length (nat_to_bv (p * q)) - 1) = [] then [] else rsapss_sign_help1 (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - 1))) e (p * q)) \<noteq> length (nat_to_bv (p * q)) then False else let em = nat_to_bv_length (rsa_crypt (bv_to_nat (if emsapss_encode m (length (nat_to_bv (p * q)) - 1) = [] then [] else rsapss_sign_help1 (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - 1))) e (p * q))) d (p * q)) (roundup (length (nat_to_bv (p * q)) - 1) 8 * 8) in emsapss_decode m em (length (nat_to_bv (p * q)) - 1)) = True
[PROOF STEP]
apply (simp only: rsapss_sign_help1_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = 1; (if emsapss_encode m (length (nat_to_bv (p * q)) - 1) = [] then [] else nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - 1))) e (p * q)) (length (nat_to_bv (p * q)))) \<noteq> []; s = (if emsapss_encode m (length (nat_to_bv (p * q)) - 1) = [] then [] else nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - 1))) e (p * q)) (length (nat_to_bv (p * q))))\<rbrakk> \<Longrightarrow> (if length (if emsapss_encode m (length (nat_to_bv (p * q)) - 1) = [] then [] else nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - 1))) e (p * q)) (length (nat_to_bv (p * q)))) \<noteq> length (nat_to_bv (p * q)) then False else let em = nat_to_bv_length (rsa_crypt (bv_to_nat (if emsapss_encode m (length (nat_to_bv (p * q)) - 1) = [] then [] else nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - 1))) e (p * q)) (length (nat_to_bv (p * q))))) d (p * q)) (roundup (length (nat_to_bv (p * q)) - 1) 8 * 8) in emsapss_decode m em (length (nat_to_bv (p * q)) - 1)) = True
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []\<rbrakk> \<Longrightarrow> length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q))
 2. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q))\<rbrakk> \<Longrightarrow> emsapss_decode m (nat_to_bv_length (rsa_crypt (bv_to_nat (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))))) d (p * q)) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
apply (simp add: length_nat_to_bv_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q))\<rbrakk> \<Longrightarrow> emsapss_decode m (nat_to_bv_length (rsa_crypt (bv_to_nat (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))))) d (p * q)) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
apply (simp add: bv_to_nat_nat_to_bv_length)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q))\<rbrakk> \<Longrightarrow> emsapss_decode m (nat_to_bv_length (rsa_crypt (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) d (p * q)) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
apply (insert length_emsapss_encode [of m "(length (nat_to_bv (p * q)) - Suc 0)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q)); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> [] \<Longrightarrow> length (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8\<rbrakk> \<Longrightarrow> emsapss_decode m (nat_to_bv_length (rsa_crypt (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) d (p * q)) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
apply (insert bv_to_nat_emsapss_smaller_pq [of p q m])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q)); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> [] \<Longrightarrow> length (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8; \<lbrakk>prime p; prime q; p \<noteq> q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []\<rbrakk> \<Longrightarrow> bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q\<rbrakk> \<Longrightarrow> emsapss_decode m (nat_to_bv_length (rsa_crypt (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) d (p * q)) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
apply (simp add: cryptinverts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q)); length (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8; bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q\<rbrakk> \<Longrightarrow> emsapss_decode m (nat_to_bv_length (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
apply (insert length_emsapss_encode [of m "(length (nat_to_bv (p * q)) - Suc 0)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q)); length (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8; bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> [] \<Longrightarrow> length (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8\<rbrakk> \<Longrightarrow> emsapss_decode m (nat_to_bv_length (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
apply (insert nat_to_bv_length_bv_to_nat [of "emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)" "roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime p; prime q; p \<noteq> q; n = p * q; e * d mod (pred p * pred q) = Suc 0; nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))) \<noteq> []; s = nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q))); emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []; length (nat_to_bv_length (rsa_crypt (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) e (p * q)) (length (nat_to_bv (p * q)))) = length (nat_to_bv (p * q)); length (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8; bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) < p * q; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> [] \<Longrightarrow> length (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8; \<lbrakk>length (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)) = roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8; emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0) \<noteq> []\<rbrakk> \<Longrightarrow> nat_to_bv_length (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8) = emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0)\<rbrakk> \<Longrightarrow> emsapss_decode m (nat_to_bv_length (bv_to_nat (emsapss_encode m (length (nat_to_bv (p * q)) - Suc 0))) (roundup (length (nat_to_bv (p * q)) - Suc 0) 8 * 8)) (length (nat_to_bv (p * q)) - Suc 0)
[PROOF STEP]
apply (simp add: verify)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma case_val'_cert:
  fixes bool word' b w
  assumes "CASE \<equiv> case_val' bool word'"
  shows "(CASE (Bool b) \<equiv> bool b) &&& (CASE (Word' w) \<equiv> word' w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (CASE (Bool b) \<equiv> bool b) &&& CASE (Word' w) \<equiv> word' w
[PROOF STEP]
by (simp_all add: assms)


[STATEMENT]
lemma double_code [code]: "double n = n + n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. double n = n + n
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma src_port: "src_port (a,x::adr\<^sub>i\<^sub>p,d,e) = snd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. src_port (a, x, d, e) = snd x
[PROOF STEP]
by (simp add: src_port_int_def in_subnet)


[STATEMENT]
lemma dest_port: "dest_port (a,d,x::adr\<^sub>i\<^sub>p,e) = snd x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dest_port (a, d, x, e) = snd x
[PROOF STEP]
by (simp add: dest_port_int_def in_subnet)


[STATEMENT]
lemma ln_mono: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x \<le> y \<Longrightarrow> ln (x::real) \<le> ln y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < x; 0 < y; x \<le> y\<rbrakk> \<Longrightarrow> ln x \<le> ln y
[PROOF STEP]
by (subst ln_le_cancel_iff) simp_all


[STATEMENT]
lemma ln_mono_strict: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> x < y \<Longrightarrow> ln (x::real) < ln y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < x; 0 < y; x < y\<rbrakk> \<Longrightarrow> ln x < ln y
[PROOF STEP]
by (subst ln_less_cancel_iff) simp_all


[STATEMENT]
lemma sum_pos':
  assumes "finite I"
  assumes "\<exists>x\<in>I. f x > (0 :: _ :: linordered_ab_group_add)"
  assumes "\<And>x. x \<in> I \<Longrightarrow> f x \<ge> 0"
  shows   "sum f I > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<exists>x\<in>I. (0::'b) < f x
[PROOF STEP]
guess x
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>I. (0::'b) < f x

goal (1 subgoal):
 1. thesis
goal instantiation:
PROP ?guess \<leadsto> thesis
[PROOF STEP]
by (elim bexE)
[PROOF STATE]
proof (state)
this:
x \<in> I
(0::'b) < f x

goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
note x = this
[PROOF STATE]
proof (state)
this:
x \<in> I
(0::'b) < f x

goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> I
(0::'b) < f x
[PROOF STEP]
have "I = insert x I"
[PROOF STATE]
proof (prove)
using this:
x \<in> I
(0::'b) < f x

goal (1 subgoal):
 1. I = insert x I
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
I = insert x I

goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
I = insert x I

goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
finite I
[PROOF STEP]
have "sum f ... = f x + sum f (I - {x})"
[PROOF STATE]
proof (prove)
using this:
finite I

goal (1 subgoal):
 1. sum f (insert x I) = f x + sum f (I - {x})
[PROOF STEP]
by (rule sum.insert_remove)
[PROOF STATE]
proof (state)
this:
sum f (insert x I) = f x + sum f (I - {x})

goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f (insert x I) = f x + sum f (I - {x})

goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
from x assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> I
(0::'b) < f x
finite I
\<exists>x\<in>I. (0::'b) < f x
?x \<in> I \<Longrightarrow> (0::'b) \<le> f ?x
[PROOF STEP]
have "... > 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> I
(0::'b) < f x
finite I
\<exists>x\<in>I. (0::'b) < f x
?x \<in> I \<Longrightarrow> (0::'b) \<le> f ?x

goal (1 subgoal):
 1. (0::'b) < f x + sum f (I - {x})
[PROOF STEP]
by (intro add_pos_nonneg sum_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
(0::'b) < f x + sum f (I - {x})

goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'b) < sum f I
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'b) < sum f I

goal (1 subgoal):
 1. (0::'b) < sum f I
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(0::'b) < sum f I

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_mult_left:
  assumes "(x::real) > 0"
  shows   "x * min y z = min (x*y) (x*z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * min y z = min (x * y) (x * z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. x * min y z = min (x * y) (x * z)
[PROOF STEP]
by (auto simp add: min_def algebra_simps)


[STATEMENT]
lemma max_mult_left:
  assumes "(x::real) > 0"
  shows   "x * max y z = max (x*y) (x*z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * max y z = max (x * y) (x * z)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < x

goal (1 subgoal):
 1. x * max y z = max (x * y) (x * z)
[PROOF STEP]
by (auto simp add: max_def algebra_simps)


[STATEMENT]
lemma DERIV_nonneg_imp_mono:
  assumes "\<And>t. t\<in>{x..y} \<Longrightarrow> (f has_field_derivative f' t) (at t)"
  assumes "\<And>t. t\<in>{x..y} \<Longrightarrow> f' t \<ge> 0"
  assumes "(x::real) \<le> y"
  shows   "(f x :: real) \<le> f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<le> f y
[PROOF STEP]
proof (cases x y rule: linorder_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x < y \<Longrightarrow> f x \<le> f y
 2. x = y \<Longrightarrow> f x \<le> f y
 3. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
assume xy: "x < y"
[PROOF STATE]
proof (state)
this:
x < y

goal (3 subgoals):
 1. x < y \<Longrightarrow> f x \<le> f y
 2. x = y \<Longrightarrow> f x \<le> f y
 3. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
hence "\<exists>z. x < z \<and> z < y \<and> f y - f x = (y - x) * f' z"
[PROOF STATE]
proof (prove)
using this:
x < y

goal (1 subgoal):
 1. \<exists>z>x. z < y \<and> f y - f x = (y - x) * f' z
[PROOF STEP]
by (rule MVT2) (insert assms(1), simp)
[PROOF STATE]
proof (state)
this:
\<exists>z>x. z < y \<and> f y - f x = (y - x) * f' z

goal (3 subgoals):
 1. x < y \<Longrightarrow> f x \<le> f y
 2. x = y \<Longrightarrow> f x \<le> f y
 3. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z>x. z < y \<and> f y - f x = (y - x) * f' z
[PROOF STEP]
guess z
[PROOF STATE]
proof (prove)
using this:
\<exists>z>x. z < y \<and> f y - f x = (y - x) * f' z

goal (1 subgoal):
 1. thesis
goal instantiation:
PROP ?guess \<leadsto> thesis
[PROOF STEP]
by (elim exE conjE)
[PROOF STATE]
proof (state)
this:
x < z
z < y
f y - f x = (y - x) * f' z

goal (3 subgoals):
 1. x < y \<Longrightarrow> f x \<le> f y
 2. x = y \<Longrightarrow> f x \<le> f y
 3. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
note z = this
[PROOF STATE]
proof (state)
this:
x < z
z < y
f y - f x = (y - x) * f' z

goal (3 subgoals):
 1. x < y \<Longrightarrow> f x \<le> f y
 2. x = y \<Longrightarrow> f x \<le> f y
 3. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
from z(1,2) assms(2) xy
[PROOF STATE]
proof (chain)
picking this:
x < z
z < y
?t \<in> {x..y} \<Longrightarrow> 0 \<le> f' ?t
x < y
[PROOF STEP]
have "0 \<le> (y - x) * f' z"
[PROOF STATE]
proof (prove)
using this:
x < z
z < y
?t \<in> {x..y} \<Longrightarrow> 0 \<le> f' ?t
x < y

goal (1 subgoal):
 1. 0 \<le> (y - x) * f' z
[PROOF STEP]
by (intro mult_nonneg_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> (y - x) * f' z

goal (3 subgoals):
 1. x < y \<Longrightarrow> f x \<le> f y
 2. x = y \<Longrightarrow> f x \<le> f y
 3. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> (y - x) * f' z

goal (3 subgoals):
 1. x < y \<Longrightarrow> f x \<le> f y
 2. x = y \<Longrightarrow> f x \<le> f y
 3. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
note z(3)[symmetric]
[PROOF STATE]
proof (state)
this:
(y - x) * f' z = f y - f x

goal (3 subgoals):
 1. x < y \<Longrightarrow> f x \<le> f y
 2. x = y \<Longrightarrow> f x \<le> f y
 3. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 \<le> f y - f x
[PROOF STEP]
show "f x \<le> f y"
[PROOF STATE]
proof (prove)
using this:
0 \<le> f y - f x

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

goal (2 subgoals):
 1. x = y \<Longrightarrow> f x \<le> f y
 2. y < x \<Longrightarrow> f x \<le> f y
[PROOF STEP]
qed (insert assms(3), simp_all)


[STATEMENT]
lemma eventually_conjE: "eventually (\<lambda>x. P x \<and> Q x) F \<Longrightarrow> (eventually P F \<Longrightarrow> eventually Q F \<Longrightarrow> R) \<Longrightarrow> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<^sub>F x in F. P x \<and> Q x; \<lbrakk>eventually P F; eventually Q F\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
apply (frule eventually_rev_mp[of _ _ P], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>\<^sub>F x in F. P x \<and> Q x; \<lbrakk>eventually P F; eventually Q F\<rbrakk> \<Longrightarrow> R; eventually P F\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
apply (drule eventually_rev_mp[of _ _ Q], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>eventually P F; eventually Q F\<rbrakk> \<Longrightarrow> R; eventually P F; eventually Q F\<rbrakk> \<Longrightarrow> R
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma real_natfloor_nat: "x \<in> \<nat> \<Longrightarrow> real (nat \<lfloor>x\<rfloor>) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<nat> \<Longrightarrow> real (nat \<lfloor>x\<rfloor>) = x
[PROOF STEP]
by (elim Nats_cases) simp


[STATEMENT]
lemma eventually_natfloor:
  assumes "eventually P (at_top :: nat filter)"
  shows   "eventually (\<lambda>x. P (nat \<lfloor>x\<rfloor>)) (at_top :: real filter)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
eventually P sequentially
[PROOF STEP]
obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> P n"
[PROOF STATE]
proof (prove)
using this:
eventually P sequentially

goal (1 subgoal):
 1. (\<And>N. (\<And>n. N \<le> n \<Longrightarrow> P n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
eventually P sequentially
eventually ?P at_top = (\<exists>N. \<forall>n\<ge>N. ?P n)

goal (1 subgoal):
 1. (\<And>N. (\<And>n. N \<le> n \<Longrightarrow> P n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
N \<le> ?n \<Longrightarrow> P ?n

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
have "\<forall>n\<ge>real N. P (nat \<lfloor>n\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n\<ge>real N. P (nat \<lfloor>n\<rfloor>)
[PROOF STEP]
by (intro allI impI N le_nat_floor) simp_all
[PROOF STATE]
proof (state)
this:
\<forall>n\<ge>real N. P (nat \<lfloor>n\<rfloor>)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>real N. P (nat \<lfloor>n\<rfloor>)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
using eventually_at_top_linorder
[PROOF STATE]
proof (prove)
using this:
\<forall>n\<ge>real N. P (nat \<lfloor>n\<rfloor>)
eventually ?P at_top = (\<exists>N. \<forall>n\<ge>N. ?P n)

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. P (nat \<lfloor>x\<rfloor>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_top. P (nat \<lfloor>x\<rfloor>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tendsto_0_smallo_1: "f \<in> o(\<lambda>x. 1 :: real) \<Longrightarrow> (f \<longlongrightarrow> 0) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> o(\<lambda>x. 1) \<Longrightarrow> (f \<longlongrightarrow> 0) at_top
[PROOF STEP]
by (drule smalloD_tendsto) simp


[STATEMENT]
lemma filterlim_at_top_smallomega_1:
  assumes "f \<in> \<omega>[F](\<lambda>x. 1 :: real)" "eventually (\<lambda>x. f x > 0) F"
  shows   "filterlim f at_top F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterlim f at_top F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. filterlim f at_top F
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
f \<in> \<omega>[F](\<lambda>x. 1)
\<forall>\<^sub>F x in F. 0 < f x
[PROOF STEP]
have "filterlim (\<lambda>x. norm (f x / 1)) at_top F"
[PROOF STATE]
proof (prove)
using this:
f \<in> \<omega>[F](\<lambda>x. 1)
\<forall>\<^sub>F x in F. 0 < f x

goal (1 subgoal):
 1. LIM x F. norm (f x / 1) :> at_top
[PROOF STEP]
by (intro smallomegaD_filterlim_at_top_norm) (auto elim: eventually_mono)
[PROOF STATE]
proof (state)
this:
LIM x F. norm (f x / 1) :> at_top

goal (1 subgoal):
 1. filterlim f at_top F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LIM x F. norm (f x / 1) :> at_top

goal (1 subgoal):
 1. filterlim f at_top F
[PROOF STEP]
have "?this \<longleftrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LIM x F. norm (f x / 1) :> at_top) = filterlim f at_top F
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> \<omega>[F](\<lambda>x. 1)
\<forall>\<^sub>F x in F. 0 < f x

goal (1 subgoal):
 1. (LIM x F. norm (f x / 1) :> at_top) = filterlim f at_top F
[PROOF STEP]
by (intro filterlim_cong refl) (auto elim!: eventually_mono)
[PROOF STATE]
proof (state)
this:
(LIM x F. norm (f x / 1) :> at_top) = filterlim f at_top F

goal (1 subgoal):
 1. filterlim f at_top F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
filterlim f at_top F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
filterlim f at_top F

goal (1 subgoal):
 1. filterlim f at_top F
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
filterlim f at_top F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smallo_imp_abs_less_real:
  assumes "f \<in> o[F](g)" "eventually (\<lambda>x. g x > (0::real)) F"
  shows   "eventually (\<lambda>x. \<bar>f x\<bar> < g x) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. \<bar>f x\<bar> < g x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. \<bar>f x\<bar> < g x
[PROOF STEP]
have "1/2 > (0::real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 1 / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < 1 / 2

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. \<bar>f x\<bar> < g x
[PROOF STEP]
from landau_o.smallD[OF assms(1) this] assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in F. norm (f x) \<le> 1 / 2 * norm (g x)
\<forall>\<^sub>F x in F. 0 < g x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. norm (f x) \<le> 1 / 2 * norm (g x)
\<forall>\<^sub>F x in F. 0 < g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. \<bar>f x\<bar> < g x
[PROOF STEP]
by eventually_elim auto
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. \<bar>f x\<bar> < g x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smallo_imp_less_real:
  assumes "f \<in> o[F](g)" "eventually (\<lambda>x. g x > (0::real)) F"
  shows   "eventually (\<lambda>x. f x < g x) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. f x < g x
[PROOF STEP]
using smallo_imp_abs_less_real[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. \<bar>f x\<bar> < g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. f x < g x
[PROOF STEP]
by eventually_elim simp


[STATEMENT]
lemma smallo_imp_le_real:
  assumes "f \<in> o[F](g)" "eventually (\<lambda>x. g x \<ge> (0::real)) F"
  shows   "eventually (\<lambda>x. f x \<le> g x) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. f x \<le> g x
[PROOF STEP]
using landau_o.smallD[OF assms(1) zero_less_one] assms(2)
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. norm (f x) \<le> 1 * norm (g x)
\<forall>\<^sub>F x in F. 0 \<le> g x

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. f x \<le> g x
[PROOF STEP]
by eventually_elim simp


[STATEMENT]
lemma filterlim_at_right:
  "filterlim f (at_right a) F \<longleftrightarrow> eventually (\<lambda>x. f x > a) F \<and> filterlim f (nhds a) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterlim f (at_right a) F = ((\<forall>\<^sub>F x in F. a < f x) \<and> (f \<longlongrightarrow> a) F)
[PROOF STEP]
by (subst filterlim_at) (auto elim!: eventually_mono)


[STATEMENT]
lemma one_plus_x_powr_approx_ex:
  assumes x: "abs (x::real) \<le> 1/2"
  obtains t where "abs t < 1/2" "(1 + x) powr p =
    1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x ^ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume x': "x \<noteq> 0"
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?f = "\<lambda>x. (1 + x) powr p"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?f' = "\<lambda>x. p * (1 + x) powr (p - 1)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?f'' = "\<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
let ?fs = "(!) [?f, ?f', ?f'']"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have A: "\<forall>m t. m < 2 \<and> t \<ge> -0.5 \<and> t \<le> 0.5 \<longrightarrow> (?fs m has_real_derivative ?fs (Suc m) t) (at t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m t. m < 2 \<and> - (5 / 10) \<le> t \<and> t \<le> 5 / 10 \<longrightarrow> ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m has_real_derivative ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! Suc m) t) (at t)
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m t. \<lbrakk>m < 2; - (5 / 10) \<le> t; t \<le> 5 / 10\<rbrakk> \<Longrightarrow> ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m has_real_derivative ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! Suc m) t) (at t)
[PROOF STEP]
fix m :: nat and t :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m t. \<lbrakk>m < 2; - (5 / 10) \<le> t; t \<le> 5 / 10\<rbrakk> \<Longrightarrow> ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m has_real_derivative ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! Suc m) t) (at t)
[PROOF STEP]
assume m: "m < 2" and t: "t \<ge> -0.5" "t \<le> 0.5"
[PROOF STATE]
proof (state)
this:
m < 2
- (5 / 10) \<le> t
t \<le> 5 / 10

goal (1 subgoal):
 1. \<And>m t. \<lbrakk>m < 2; - (5 / 10) \<le> t; t \<le> 5 / 10\<rbrakk> \<Longrightarrow> ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m has_real_derivative ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! Suc m) t) (at t)
[PROOF STEP]
thus "(?fs m has_real_derivative ?fs (Suc m) t) (at t)"
[PROOF STATE]
proof (prove)
using this:
m < 2
- (5 / 10) \<le> t
t \<le> 5 / 10

goal (1 subgoal):
 1. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m has_real_derivative ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! Suc m) t) (at t)
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
m < 2
- (5 / 10) \<le> t
t \<le> 5 / 10
m < 2

goal (1 subgoal):
 1. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m has_real_derivative ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! Suc m) t) (at t)
[PROOF STEP]
by (cases m) (force intro: derivative_eq_intros algebra_simps)+
[PROOF STATE]
proof (state)
this:
([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m has_real_derivative ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! Suc m) t) (at t)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m t. m < 2 \<and> - (5 / 10) \<le> t \<and> t \<le> 5 / 10 \<longrightarrow> ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m has_real_derivative ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! Suc m) t) (at t)

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "\<exists>t. (if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x) \<and>
              (1 + x) powr p = (\<Sum>m<2. ?fs m 0 / (fact m) * (x - 0)^m) +
              ?fs 2 t / (fact 2) * (x - 0)\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. (if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x) \<and> (1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2
[PROOF STEP]
using assms x'
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> \<le> 1 / 2
x \<noteq> 0

goal (1 subgoal):
 1. \<exists>t. (if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x) \<and> (1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2
[PROOF STEP]
by (intro Taylor[OF _ _ A]) simp_all
[PROOF STATE]
proof (state)
this:
\<exists>t. (if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x) \<and> (1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>t. (if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x) \<and> (1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2
[PROOF STEP]
guess t
[PROOF STATE]
proof (prove)
using this:
\<exists>t. (if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x) \<and> (1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2

goal (1 subgoal):
 1. thesis
goal instantiation:
PROP ?guess \<leadsto> thesis
[PROOF STEP]
by (elim exE conjE)
[PROOF STATE]
proof (state)
this:
if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x
(1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
note t = this
[PROOF STATE]
proof (state)
this:
if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x
(1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<bar>x\<bar> \<le> 1 / 2
if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x
(1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2
[PROOF STEP]
have "abs t < 1/2"
[PROOF STATE]
proof (prove)
using this:
\<bar>x\<bar> \<le> 1 / 2
if x < 0 then x < t \<and> t < 0 else 0 < t \<and> t < x
(1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2

goal (1 subgoal):
 1. \<bar>t\<bar> < 1 / 2
[PROOF STEP]
by (auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
\<bar>t\<bar> < 1 / 2

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>t\<bar> < 1 / 2

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from t(2)
[PROOF STATE]
proof (chain)
picking this:
(1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2
[PROOF STEP]
have "(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x ^ 2"
[PROOF STATE]
proof (prove)
using this:
(1 + x) powr p = (\<Sum>m<2. ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! m) 0 / fact m * (x - 0) ^ m) + ([\<lambda>x. (1 + x) powr p, \<lambda>x. p * (1 + x) powr (p - 1), \<lambda>x. p * (p - 1) * (1 + x) powr (p - 2)] ! 2) t / fact 2 * (x - 0)\<^sup>2

goal (1 subgoal):
 1. (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2
[PROOF STEP]
by (simp add: numeral_2_eq_2 of_nat_Suc)
[PROOF STATE]
proof (state)
this:
(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2

goal (2 subgoals):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x \<noteq> 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>t\<bar> < 1 / 2
(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<bar>t\<bar> < 1 / 2
(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2

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

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
assume "x = 0"
[PROOF STATE]
proof (state)
this:
x = 0

goal (1 subgoal):
 1. \<lbrakk>\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis; x = 0\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
with that[of 0]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<bar>0\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + 0) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<bar>0\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + 0) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> thesis
x = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma powr_lower_bound: "\<lbrakk>(l::real) > 0; l \<le> x; x \<le> u\<rbrakk> \<Longrightarrow> min (l powr z) (u powr z) \<le> x powr z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> x; x \<le> u\<rbrakk> \<Longrightarrow> min (l powr z) (u powr z) \<le> x powr z
[PROOF STEP]
apply (cases "z \<ge> 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < l; l \<le> x; x \<le> u; 0 \<le> z\<rbrakk> \<Longrightarrow> min (l powr z) (u powr z) \<le> x powr z
 2. \<lbrakk>0 < l; l \<le> x; x \<le> u; \<not> 0 \<le> z\<rbrakk> \<Longrightarrow> min (l powr z) (u powr z) \<le> x powr z
[PROOF STEP]
apply (rule order.trans[OF min.cobounded1 powr_mono2], simp_all) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> x; x \<le> u; \<not> 0 \<le> z\<rbrakk> \<Longrightarrow> min (l powr z) (u powr z) \<le> x powr z
[PROOF STEP]
apply (rule order.trans[OF min.cobounded2 powr_mono2'], simp_all) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma powr_upper_bound: "\<lbrakk>(l::real) > 0; l \<le> x; x \<le> u\<rbrakk> \<Longrightarrow> max (l powr z) (u powr z) \<ge> x powr z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> x; x \<le> u\<rbrakk> \<Longrightarrow> x powr z \<le> max (l powr z) (u powr z)
[PROOF STEP]
apply (cases "z \<ge> 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < l; l \<le> x; x \<le> u; 0 \<le> z\<rbrakk> \<Longrightarrow> x powr z \<le> max (l powr z) (u powr z)
 2. \<lbrakk>0 < l; l \<le> x; x \<le> u; \<not> 0 \<le> z\<rbrakk> \<Longrightarrow> x powr z \<le> max (l powr z) (u powr z)
[PROOF STEP]
apply (rule order.trans[OF powr_mono2 max.cobounded2], simp_all) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> x; x \<le> u; \<not> 0 \<le> z\<rbrakk> \<Longrightarrow> x powr z \<le> max (l powr z) (u powr z)
[PROOF STEP]
apply (rule order.trans[OF powr_mono2' max.cobounded1], simp_all) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma one_plus_x_powr_Taylor2:
  obtains k where "\<And>x. abs (x::real) \<le> 1/2 \<Longrightarrow> abs ((1 + x) powr p - 1 - p*x) \<le> k*x^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. (\<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>k. (\<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
define k where "k = \<bar>p*(p - 1)\<bar> * max ((1/2) powr (p - 2)) ((3/2) powr (p - 2)) / 2"
[PROOF STATE]
proof (state)
this:
k = \<bar>p * (p - 1)\<bar> * max ((1 / 2) powr (p - 2)) ((3 / 2) powr (p - 2)) / 2

goal (1 subgoal):
 1. (\<And>k. (\<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof (rule that[of k])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
fix x :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
assume "abs x \<le> 1/2"
[PROOF STATE]
proof (state)
this:
\<bar>x\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. \<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
from one_plus_x_powr_approx_ex[OF this, of p]
[PROOF STATE]
proof (chain)
picking this:
(\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
guess t
[PROOF STATE]
proof (prove)
using this:
(\<And>t. \<lbrakk>\<bar>t\<bar> < 1 / 2; (1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. thesis
goal instantiation:
PROP ?guess \<leadsto> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>t\<bar> < 1 / 2
(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2

goal (1 subgoal):
 1. \<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
note t = this
[PROOF STATE]
proof (state)
this:
\<bar>t\<bar> < 1 / 2
(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2

goal (1 subgoal):
 1. \<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
from t
[PROOF STATE]
proof (chain)
picking this:
\<bar>t\<bar> < 1 / 2
(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2
[PROOF STEP]
have "abs ((1 + x) powr p - 1 - p*x) = \<bar>p*(p - 1)\<bar> * (1 + t) powr (p - 2)/2 * x\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
\<bar>t\<bar> < 1 / 2
(1 + x) powr p = 1 + p * x + p * (p - 1) * (1 + t) powr (p - 2) / 2 * x\<^sup>2

goal (1 subgoal):
 1. \<bar>(1 + x) powr p - 1 - p * x\<bar> = \<bar>p * (p - 1)\<bar> * (1 + t) powr (p - 2) / 2 * x\<^sup>2
[PROOF STEP]
by (simp add: abs_mult)
[PROOF STATE]
proof (state)
this:
\<bar>(1 + x) powr p - 1 - p * x\<bar> = \<bar>p * (p - 1)\<bar> * (1 + t) powr (p - 2) / 2 * x\<^sup>2

goal (1 subgoal):
 1. \<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>(1 + x) powr p - 1 - p * x\<bar> = \<bar>p * (p - 1)\<bar> * (1 + t) powr (p - 2) / 2 * x\<^sup>2

goal (1 subgoal):
 1. \<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
from t(1)
[PROOF STATE]
proof (chain)
picking this:
\<bar>t\<bar> < 1 / 2
[PROOF STEP]
have "(1 + t) powr (p - 2) \<le> max ((1/2) powr (p - 2)) ((3/2) powr (p - 2))"
[PROOF STATE]
proof (prove)
using this:
\<bar>t\<bar> < 1 / 2

goal (1 subgoal):
 1. (1 + t) powr (p - 2) \<le> max ((1 / 2) powr (p - 2)) ((3 / 2) powr (p - 2))
[PROOF STEP]
by (intro powr_upper_bound) simp_all
[PROOF STATE]
proof (state)
this:
(1 + t) powr (p - 2) \<le> max ((1 / 2) powr (p - 2)) ((3 / 2) powr (p - 2))

goal (1 subgoal):
 1. \<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> \<bar>p * (p - 1)\<bar> * xa / 2 * x\<^sup>2 \<le> \<bar>p * (p - 1)\<bar> * y / 2 * x\<^sup>2) \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> \<bar>p * (p - 1)\<bar> * max ((1 / 2) powr (p - 2)) ((3 / 2) powr (p - 2)) / 2 * x\<^sup>2
[PROOF STEP]
show "abs ((1 + x) powr p - 1 - p*x) \<le> k*x^2"
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> \<bar>p * (p - 1)\<bar> * xa / 2 * x\<^sup>2 \<le> \<bar>p * (p - 1)\<bar> * y / 2 * x\<^sup>2) \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> \<bar>p * (p - 1)\<bar> * max ((1 / 2) powr (p - 2)) ((3 / 2) powr (p - 2)) / 2 * x\<^sup>2

goal (1 subgoal):
 1. \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2
[PROOF STEP]
by (simp add: mult_left_mono mult_right_mono k_def)
[PROOF STATE]
proof (state)
this:
\<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_plus_x_powr_Taylor2_bigo:
  assumes lim: "(f \<longlongrightarrow> 0) F"
  shows   "(\<lambda>x. (1 + f x) powr (p::real) - 1 - p * f x) \<in> O[F](\<lambda>x. f x ^ 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)
[PROOF STEP]
from one_plus_x_powr_Taylor2[of p]
[PROOF STATE]
proof (chain)
picking this:
(\<And>k. (\<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
guess k
[PROOF STATE]
proof (prove)
using this:
(\<And>k. (\<And>x. \<bar>x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + x) powr p - 1 - p * x\<bar> \<le> k * x\<^sup>2) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. thesis
goal instantiation:
PROP ?guess \<leadsto> thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>?x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + ?x) powr p - 1 - p * ?x\<bar> \<le> k * ?x\<^sup>2

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<bar>?x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + ?x) powr p - 1 - p * ?x\<bar> \<le> k * ?x\<^sup>2

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)
[PROOF STEP]
from tendstoD[OF lim, of "1/2"]
[PROOF STATE]
proof (chain)
picking this:
0 < 1 / 2 \<Longrightarrow> \<forall>\<^sub>F x in F. dist (f x) 0 < 1 / 2
[PROOF STEP]
have "eventually (\<lambda>x. abs (f x) < 1/2) F"
[PROOF STATE]
proof (prove)
using this:
0 < 1 / 2 \<Longrightarrow> \<forall>\<^sub>F x in F. dist (f x) 0 < 1 / 2

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. \<bar>f x\<bar> < 1 / 2
[PROOF STEP]
by (simp add: dist_real_def)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. \<bar>f x\<bar> < 1 / 2

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<bar>?x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + ?x) powr p - 1 - p * ?x\<bar> \<le> k * ?x\<^sup>2
\<forall>\<^sub>F x in F. \<bar>f x\<bar> < 1 / 2
[PROOF STEP]
have "eventually (\<lambda>x. norm ((1 + f x) powr p - 1 - p * f x) \<le> k * norm (f x ^ 2)) F"
[PROOF STATE]
proof (prove)
using this:
\<bar>?x\<bar> \<le> 1 / 2 \<Longrightarrow> \<bar>(1 + ?x) powr p - 1 - p * ?x\<bar> \<le> k * ?x\<^sup>2
\<forall>\<^sub>F x in F. \<bar>f x\<bar> < 1 / 2

goal (1 subgoal):
 1. \<forall>\<^sub>F x in F. norm ((1 + f x) powr p - 1 - p * f x) \<le> k * norm ((f x)\<^sup>2)
[PROOF STEP]
by (auto elim!: eventually_mono)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in F. norm ((1 + f x) powr p - 1 - p * f x) \<le> k * norm ((f x)\<^sup>2)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in F. norm ((1 + f x) powr p - 1 - p * f x) \<le> k * norm ((f x)\<^sup>2)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)
[PROOF STEP]
by (rule bigoI)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_plus_x_powr_Taylor1_bigo:
  assumes lim: "(f \<longlongrightarrow> 0) F"
  shows   "(\<lambda>x. (1 + f x) powr (p::real) - 1) \<in> O[F](\<lambda>x. f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(f \<longlongrightarrow> 0) F
[PROOF STEP]
have "(\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
(f \<longlongrightarrow> 0) F

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)
[PROOF STEP]
by (rule one_plus_x_powr_Taylor2_bigo)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](\<lambda>x. (f x)\<^sup>2)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(f \<longlongrightarrow> 0) F
[PROOF STEP]
have "f \<in> O[F](\<lambda>_. 1)"
[PROOF STATE]
proof (prove)
using this:
(f \<longlongrightarrow> 0) F

goal (1 subgoal):
 1. f \<in> O[F](\<lambda>_. 1)
[PROOF STEP]
by (intro bigoI_tendsto) simp_all
[PROOF STATE]
proof (state)
this:
f \<in> O[F](\<lambda>_. 1)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
from landau_o.big.mult[of f F f, OF _ this]
[PROOF STATE]
proof (chain)
picking this:
f \<in> O[F](f) \<Longrightarrow> (\<lambda>x. f x * f x) \<in> O[F](\<lambda>x. f x * 1)
[PROOF STEP]
have "(\<lambda>x. (f x)^2) \<in> O[F](\<lambda>x. f x)"
[PROOF STATE]
proof (prove)
using this:
f \<in> O[F](f) \<Longrightarrow> (\<lambda>x. f x * f x) \<in> O[F](\<lambda>x. f x * 1)

goal (1 subgoal):
 1. (\<lambda>x. (f x)\<^sup>2) \<in> O[F](f)
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f x)\<^sup>2) \<in> O[F](f)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](f)
[PROOF STEP]
have A: "(\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](f)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](f)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 + f x) powr p - 1 - p * f x) \<in> O[F](f)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
have B: "(\<lambda>x. p * f x) \<in> O[F](f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. p * f x) \<in> O[F](f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. p * f x) \<in> O[F](f)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
from sum_in_bigo(1)[OF A B]
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (1 + f x) powr p - 1 - p * f x + p * f x) \<in> O[F](f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (1 + f x) powr p - 1 - p * f x + p * f x) \<in> O[F](f)

goal (1 subgoal):
 1. (\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (1 + f x) powr p - 1) \<in> O[F](f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x_times_x_minus_1_nonneg: "x \<le> 0 \<or> x \<ge> 1 \<Longrightarrow> (x::_::linordered_idom) * (x - 1) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> (0::'a) \<or> (1::'a) \<le> x \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
[PROOF STEP]
proof (elim disjE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<le> (0::'a) \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
 2. (1::'a) \<le> x \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
[PROOF STEP]
assume x: "x \<le> 0"
[PROOF STATE]
proof (state)
this:
x \<le> (0::'a)

goal (2 subgoals):
 1. x \<le> (0::'a) \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
 2. (1::'a) \<le> x \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<le> (0::'a)

goal (2 subgoals):
 1. x \<le> (0::'a) \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
 2. (1::'a) \<le> x \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
[PROOF STEP]
have "0 \<le> x^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> x\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> x\<^sup>2

goal (2 subgoals):
 1. x \<le> (0::'a) \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
 2. (1::'a) \<le> x \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<le> x\<^sup>2
[PROOF STEP]
show "x * (x - 1) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
x \<le> x\<^sup>2

goal (1 subgoal):
 1. (0::'a) \<le> x * (x - (1::'a))
[PROOF STEP]
by (simp add: power2_eq_square algebra_simps)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> x * (x - (1::'a))

goal (1 subgoal):
 1. (1::'a) \<le> x \<Longrightarrow> (0::'a) \<le> x * (x - (1::'a))
[PROOF STEP]
qed simp


[STATEMENT]
lemma x_times_x_minus_1_nonpos: "x \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> (x::_::linordered_idom) * (x - 1) \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'a) \<le> x; x \<le> (1::'a)\<rbrakk> \<Longrightarrow> x * (x - (1::'a)) \<le> (0::'a)
[PROOF STEP]
by (intro mult_nonneg_nonpos) simp_all


[STATEMENT]
lemma powr_mono':
  assumes "(x::real) > 0" "x \<le> 1" "a \<le> b"
  shows   "x powr b \<le> x powr a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr b \<le> x powr a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x powr b \<le> x powr a
[PROOF STEP]
have "inverse x powr a \<le> inverse x powr b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse x powr a \<le> inverse x powr b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < x
x \<le> 1
a \<le> b

goal (1 subgoal):
 1. inverse x powr a \<le> inverse x powr b
[PROOF STEP]
by (intro powr_mono) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
inverse x powr a \<le> inverse x powr b

goal (1 subgoal):
 1. x powr b \<le> x powr a
[PROOF STEP]
hence "inverse (x powr a) \<le> inverse (x powr b)"
[PROOF STATE]
proof (prove)
using this:
inverse x powr a \<le> inverse x powr b

goal (1 subgoal):
 1. inverse (x powr a) \<le> inverse (x powr b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inverse x powr a \<le> inverse x powr b
0 < x
x \<le> 1
a \<le> b

goal (1 subgoal):
 1. inverse (x powr a) \<le> inverse (x powr b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inverse (x powr a) \<le> inverse (x powr b)

goal (1 subgoal):
 1. x powr b \<le> x powr a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < x
x \<le> 1
a \<le> b
inverse (x powr a) \<le> inverse (x powr b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x
x \<le> 1
a \<le> b
inverse (x powr a) \<le> inverse (x powr b)

goal (1 subgoal):
 1. x powr b \<le> x powr a
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x powr b \<le> x powr a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma powr_less_mono':
  assumes "(x::real) > 0" "x < 1" "a < b"
  shows   "x powr b < x powr a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr b < x powr a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x powr b < x powr a
[PROOF STEP]
have "inverse x powr a < inverse x powr b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse x powr a < inverse x powr b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < x
x < 1
a < b

goal (1 subgoal):
 1. inverse x powr a < inverse x powr b
[PROOF STEP]
by (intro powr_less_mono) (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
inverse x powr a < inverse x powr b

goal (1 subgoal):
 1. x powr b < x powr a
[PROOF STEP]
hence "inverse (x powr a) < inverse (x powr b)"
[PROOF STATE]
proof (prove)
using this:
inverse x powr a < inverse x powr b

goal (1 subgoal):
 1. inverse (x powr a) < inverse (x powr b)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
inverse x powr a < inverse x powr b
0 < x
x < 1
a < b

goal (1 subgoal):
 1. inverse (x powr a) < inverse (x powr b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
inverse (x powr a) < inverse (x powr b)

goal (1 subgoal):
 1. x powr b < x powr a
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < x
x < 1
a < b
inverse (x powr a) < inverse (x powr b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < x
x < 1
a < b
inverse (x powr a) < inverse (x powr b)

goal (1 subgoal):
 1. x powr b < x powr a
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
x powr b < x powr a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_powr_at_bot:
  assumes "(a::real) > 1"
  shows   "((\<lambda>x. a powr x) \<longlongrightarrow> 0) at_bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_bot
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_bot
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
1 < a
[PROOF STEP]
have "filterlim (\<lambda>x. ln a * x) at_bot at_bot"
[PROOF STATE]
proof (prove)
using this:
1 < a

goal (1 subgoal):
 1. filterlim ((*) (ln a)) at_bot at_bot
[PROOF STEP]
by (intro filterlim_tendsto_pos_mult_at_bot[OF tendsto_const _ filterlim_ident]) auto
[PROOF STATE]
proof (state)
this:
filterlim ((*) (ln a)) at_bot at_bot

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_bot
[PROOF STEP]
hence "((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_bot"
[PROOF STATE]
proof (prove)
using this:
filterlim ((*) (ln a)) at_bot at_bot

goal (1 subgoal):
 1. ((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_bot
[PROOF STEP]
by (intro filterlim_compose[OF exp_at_bot]) (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_bot

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_bot
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_bot

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_bot
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_bot
1 < a

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_bot
[PROOF STEP]
unfolding powr_def
[PROOF STATE]
proof (prove)
using this:
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_bot
1 < a

goal (1 subgoal):
 1. ((\<lambda>x. if a = 0 then 0 else exp (x * ln a)) \<longlongrightarrow> 0) at_bot
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((powr) a \<longlongrightarrow> 0) at_bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_powr_at_bot_neg:
  assumes "(a::real) > 0" "a < 1"
  shows   "filterlim (\<lambda>x. a powr x) at_top at_bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterlim ((powr) a) at_top at_bot
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. filterlim ((powr) a) at_top at_bot
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < a
a < 1
[PROOF STEP]
have "LIM x at_bot. ln (inverse a) * -x :> at_top"
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1

goal (1 subgoal):
 1. LIM x at_bot. ln (inverse a) * - x :> at_top
[PROOF STEP]
by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] filterlim_uminus_at_top_at_bot)
       (simp_all add: ln_inverse)
[PROOF STATE]
proof (state)
this:
LIM x at_bot. ln (inverse a) * - x :> at_top

goal (1 subgoal):
 1. filterlim ((powr) a) at_top at_bot
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < a
a < 1
LIM x at_bot. ln (inverse a) * - x :> at_top
[PROOF STEP]
have "LIM x at_bot. x * ln a :> at_top"
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1
LIM x at_bot. ln (inverse a) * - x :> at_top

goal (1 subgoal):
 1. LIM x at_bot. x * ln a :> at_top
[PROOF STEP]
by (subst (asm) ln_inverse) (simp_all add: mult.commute)
[PROOF STATE]
proof (state)
this:
LIM x at_bot. x * ln a :> at_top

goal (1 subgoal):
 1. filterlim ((powr) a) at_top at_bot
[PROOF STEP]
hence "LIM x at_bot. exp (x * ln a) :> at_top"
[PROOF STATE]
proof (prove)
using this:
LIM x at_bot. x * ln a :> at_top

goal (1 subgoal):
 1. LIM x at_bot. exp (x * ln a) :> at_top
[PROOF STEP]
by (intro filterlim_compose[OF exp_at_top]) simp
[PROOF STATE]
proof (state)
this:
LIM x at_bot. exp (x * ln a) :> at_top

goal (1 subgoal):
 1. filterlim ((powr) a) at_top at_bot
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
LIM x at_bot. exp (x * ln a) :> at_top

goal (1 subgoal):
 1. filterlim ((powr) a) at_top at_bot
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
LIM x at_bot. exp (x * ln a) :> at_top
0 < a
a < 1

goal (1 subgoal):
 1. filterlim ((powr) a) at_top at_bot
[PROOF STEP]
unfolding powr_def
[PROOF STATE]
proof (prove)
using this:
LIM x at_bot. exp (x * ln a) :> at_top
0 < a
a < 1

goal (1 subgoal):
 1. LIM x at_bot. if a = 0 then 0 else exp (x * ln a) :> at_top
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
filterlim ((powr) a) at_top at_bot

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma real_powr_at_top_neg:
  assumes "(a::real) > 0" "a < 1"
  shows   "((\<lambda>x. a powr x) \<longlongrightarrow> 0) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < a
a < 1
[PROOF STEP]
have "LIM x at_top. ln (inverse a) * x :> at_top"
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1

goal (1 subgoal):
 1. filterlim ((*) (ln (inverse a))) at_top at_top
[PROOF STEP]
by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const])
       (simp_all add: filterlim_ident field_simps)
[PROOF STATE]
proof (state)
this:
filterlim ((*) (ln (inverse a))) at_top at_top

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < a
a < 1
filterlim ((*) (ln (inverse a))) at_top at_top
[PROOF STEP]
have "LIM x at_top. ln a * x :> at_bot"
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1
filterlim ((*) (ln (inverse a))) at_top at_top

goal (1 subgoal):
 1. filterlim ((*) (ln a)) at_bot at_top
[PROOF STEP]
by (subst filterlim_uminus_at_bot) (simp add: ln_inverse)
[PROOF STATE]
proof (state)
this:
filterlim ((*) (ln a)) at_bot at_top

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
hence "((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top"
[PROOF STATE]
proof (prove)
using this:
filterlim ((*) (ln a)) at_bot at_top

goal (1 subgoal):
 1. ((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top
[PROOF STEP]
by (intro filterlim_compose[OF exp_at_bot]) (simp_all add: mult.commute)
[PROOF STATE]
proof (state)
this:
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < a
a < 1
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top

goal (1 subgoal):
 1. ((powr) a \<longlongrightarrow> 0) at_top
[PROOF STEP]
unfolding powr_def
[PROOF STATE]
proof (prove)
using this:
0 < a
a < 1
((\<lambda>x. exp (x * ln a)) \<longlongrightarrow> 0) at_top

goal (1 subgoal):
 1. ((\<lambda>x. if a = 0 then 0 else exp (x * ln a)) \<longlongrightarrow> 0) at_top
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((powr) a \<longlongrightarrow> 0) at_top

goal:
No subgoals!
[PROOF STEP]
qed