src/HOL/NthRoot.thy
changeset 49753 a344f1a21211
parent 44349 f057535311c5
child 49962 a8cc904a6820
equal deleted inserted replaced
49752:2bbb0013ff82 49753:a344f1a21211
   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])