equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 section \<open>Nth Roots of Real Numbers\<close> |
6 section \<open>Nth Roots of Real Numbers\<close> |
7 |
7 |
8 theory NthRoot |
8 theory NthRoot |
9 imports Deriv Binomial |
9 imports Deriv |
10 begin |
10 begin |
11 |
11 |
12 |
12 |
13 subsection \<open>Existence of Nth Root\<close> |
13 subsection \<open>Existence of Nth Root\<close> |
14 |
14 |
467 using real_sqrt_le_mono[of "x\<^sup>2" y] by simp |
467 using real_sqrt_le_mono[of "x\<^sup>2" y] by simp |
468 |
468 |
469 lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y" |
469 lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y" |
470 using real_sqrt_less_mono[of "x\<^sup>2" y] by simp |
470 using real_sqrt_less_mono[of "x\<^sup>2" y] by simp |
471 |
471 |
472 lemma real_sqrt_power_even: |
472 lemma real_sqrt_power_even: |
473 assumes "even n" "x \<ge> 0" |
473 assumes "even n" "x \<ge> 0" |
474 shows "sqrt x ^ n = x ^ (n div 2)" |
474 shows "sqrt x ^ n = x ^ (n div 2)" |
475 proof - |
475 proof - |
476 from assms obtain k where "n = 2*k" by (auto elim!: evenE) |
476 from assms obtain k where "n = 2*k" by (auto elim!: evenE) |
477 with assms show ?thesis by (simp add: power_mult) |
477 with assms show ?thesis by (simp add: power_mult) |