equal
deleted
inserted
replaced
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 ==> |