[STATEMENT]
lemma 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