src/HOL/Transcendental.thy
changeset 52139 40fe6b80b481
parent 51641 cd05e9fcc63d
child 53015 a1119cf551e8
equal deleted inserted replaced
52138:e21426f244aa 52139:40fe6b80b481
  1817   apply (subgoal_tac "real(Suc n) = real n + 1")
  1817   apply (subgoal_tac "real(Suc n) = real n + 1")
  1818   apply (erule ssubst)
  1818   apply (erule ssubst)
  1819   apply (subst powr_add, simp, simp)
  1819   apply (subst powr_add, simp, simp)
  1820 done
  1820 done
  1821 
  1821 
       
  1822 lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x^(numeral n)"
       
  1823   unfolding real_of_nat_numeral[symmetric] by (rule powr_realpow)
       
  1824 
  1822 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
  1825 lemma powr_realpow2: "0 <= x ==> 0 < n ==> x^n = (if (x = 0) then 0 else x powr (real n))"
  1823   apply (case_tac "x = 0", simp, simp)
  1826   apply (case_tac "x = 0", simp, simp)
  1824   apply (rule powr_realpow [THEN sym], simp)
  1827   apply (rule powr_realpow [THEN sym], simp)
  1825 done
  1828 done
  1826 
  1829