850 NSCDERIV_CDERIV_iff RS sym]) 1); |
850 NSCDERIV_CDERIV_iff RS sym]) 1); |
851 qed "CDERIV_mult"; |
851 qed "CDERIV_mult"; |
852 |
852 |
853 Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"; |
853 Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"; |
854 by (asm_full_simp_tac |
854 by (asm_full_simp_tac |
855 (simpset() addsimps [complex_times_divide1_eq RS sym, NSCDERIV_NSCLIM_iff, |
855 (simpset() addsimps [times_divide_eq_right RS sym, NSCDERIV_NSCLIM_iff, |
856 complex_minus_mult_eq2, complex_add_mult_distrib2 RS sym, |
856 minus_mult_right, complex_add_mult_distrib2 RS sym, |
857 complex_diff_def] |
857 complex_diff_def] |
858 delsimps [complex_times_divide1_eq, complex_minus_mult_eq2 RS sym] |
858 delsimps [times_divide_eq_right, minus_mult_right RS sym]) 1); |
859 delsimps [times_divide_eq_right, minus_mult_right RS sym] |
|
860 |
|
861 ) 1); |
|
862 by (etac (NSCLIM_const RS NSCLIM_mult) 1); |
859 by (etac (NSCLIM_const RS NSCLIM_mult) 1); |
863 qed "NSCDERIV_cmult"; |
860 qed "NSCDERIV_cmult"; |
864 |
861 |
865 Goal "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D"; |
862 Goal "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D"; |
866 by (auto_tac (claset(),simpset() addsimps [NSCDERIV_cmult,NSCDERIV_CDERIV_iff |
863 by (auto_tac (claset(),simpset() addsimps [NSCDERIV_cmult,NSCDERIV_CDERIV_iff |