equal
deleted
inserted
replaced
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 |