src/HOL/NthRoot.thy
 changeset 49753 a344f1a21211 parent 44349 f057535311c5 child 49962 a8cc904a6820
equal 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])`