[STATEMENT]
lemma filterlim_pow_at_bot_even:
  fixes f :: "real \<Rightarrow> real"
  shows "0 < n \<Longrightarrow> LIM x F. f x :> at_bot \<Longrightarrow> even n \<Longrightarrow> LIM x F. (f x)^n :> at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; filterlim f at_bot F; even n\<rbrakk> \<Longrightarrow> LIM x F. f x ^ n :> at_top
[PROOF STEP]
using filterlim_pow_at_top[of n "\<lambda>x. - f x" F]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 < n; LIM x F. - f x :> at_top\<rbrakk> \<Longrightarrow> LIM x F. (- f x) ^ n :> at_top

goal (1 subgoal):
 1. \<lbrakk>0 < n; filterlim f at_bot F; even n\<rbrakk> \<Longrightarrow> LIM x F. f x ^ n :> at_top
[PROOF STEP]
by (simp add: filterlim_uminus_at_top)