equal
deleted
inserted
replaced
396 using n by (rule isCont_real_root) |
396 using n by (rule isCont_real_root) |
397 qed |
397 qed |
398 |
398 |
399 lemma DERIV_real_root_generic: |
399 lemma DERIV_real_root_generic: |
400 assumes "0 < n" and "x \<noteq> 0" |
400 assumes "0 < n" and "x \<noteq> 0" |
401 and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" |
401 and "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" |
402 and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))" |
402 and "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))" |
403 and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" |
403 and "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))" |
404 shows "DERIV (root n) x :> D" |
404 shows "DERIV (root n) x :> D" |
405 using assms by (cases "even n", cases "0 < x", |
405 using assms by (cases "even n", cases "0 < x", |
406 auto intro: DERIV_real_root[THEN DERIV_cong] |
406 auto intro: DERIV_real_root[THEN DERIV_cong] |
407 DERIV_odd_real_root[THEN DERIV_cong] |
407 DERIV_odd_real_root[THEN DERIV_cong] |
408 DERIV_even_real_root[THEN DERIV_cong]) |
408 DERIV_even_real_root[THEN DERIV_cong]) |