equal
deleted
inserted
replaced
974 "[| CDERIV f x :> d; CDERIV g x :> e; g(x) \<noteq> 0 |] |
974 "[| CDERIV f x :> d; CDERIV g x :> e; g(x) \<noteq> 0 |] |
975 ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)" |
975 ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)" |
976 apply (simp add: diff_minus) |
976 apply (simp add: diff_minus) |
977 apply (drule_tac f = g in CDERIV_inverse_fun) |
977 apply (drule_tac f = g in CDERIV_inverse_fun) |
978 apply (drule_tac [2] CDERIV_mult, assumption+) |
978 apply (drule_tac [2] CDERIV_mult, assumption+) |
979 apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left |
979 apply (simp add: divide_inverse left_distrib power_inverse minus_mult_left |
980 mult_ac |
980 mult_ac |
981 del: minus_mult_right [symmetric] minus_mult_left [symmetric] |
981 del: minus_mult_right [symmetric] minus_mult_left [symmetric] |
982 complexpow_Suc) |
982 complexpow_Suc) |
983 done |
983 done |
984 |
984 |