src/HOL/Hyperreal/Deriv.thy
 changeset 21785 885667874dfc parent 21784 e76faa6e65fd child 21810 b2d23672b003
equal inserted replaced
21784:e76faa6e65fd 21785:885667874dfc
697        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
697        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
698 by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
698 by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc)
699
699
700 lemma NSDERIV_quotient:
700 lemma NSDERIV_quotient:
701   fixes x :: "'a::{real_normed_field,recpower}"
701   fixes x :: "'a::{real_normed_field,recpower}"
702   shows "[| NSDERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 |]
702   shows "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> 0 |]
703        ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
703        ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x)
704                             - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
704                             - (e*f(x))) / (g(x) ^ Suc (Suc 0))"
705 by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
705 by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc)
706
706
707 lemma CARAT_NSDERIV: "NSDERIV f x :> l ==>
707 lemma CARAT_NSDERIV: "NSDERIV f x :> l ==>