add powr_inj
authorhoelzl
Wed Apr 18 14:29:18 2012 +0200 (2012-04-18)
changeset 47595836b4c4d7c86
parent 47594 be2ac449488c
child 47596 c031e65c8ddc
add powr_inj
src/HOL/Log.thy
     1.1 --- a/src/HOL/Log.thy	Wed Apr 18 14:29:17 2012 +0200
     1.2 +++ b/src/HOL/Log.thy	Wed Apr 18 14:29:18 2012 +0200
     1.3 @@ -285,6 +285,10 @@
     1.4    apply (rule powr_less_mono2, auto)
     1.5  done
     1.6  
     1.7 +lemma powr_inj:
     1.8 +  "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
     1.9 +  unfolding powr_def exp_inj_iff by simp
    1.10 +
    1.11  lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
    1.12    apply (rule mult_imp_le_div_pos)
    1.13    apply (assumption)