proposition: Theorem derivable_pt_lim_sin : forall x:R, derivable_pt_lim sin x (cos x).
proof: Proof. intro; assert (H0 := derivable_pt_lim_sin_0). assert (H := derivable_pt_lim_cos_0). unfold derivable_pt_lim in H0, H. unfold derivable_pt_lim; intros. cut (0 < eps / 2); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ apply H1 | apply Rinv_0_lt_compat; prove_sup0 ] ]. elim (H0 _ H2); intros alp1 H3. elim (H _ H2); intros alp2 H4. set (alp := Rmin alp1 alp2). assert (0 < alp). { unfold alp; unfold Rmin; case (Rle_dec alp1 alp2); intro. - apply (cond_pos alp1). - apply (cond_pos alp2). } exists (mkposreal _ H5); intros. replace ((sin (x + h) - sin x) / h - cos x) with (sin x * ((cos h - 1) / h) + cos x * (sin h / h - 1)). 2:{ rewrite sin_plus; now field. } eapply Rle_lt_trans. { apply Rabs_triang. } rewrite <-(Rplus_half_diag eps); apply Rplus_lt_compat. - apply Rle_lt_trans with (Rabs ((cos h - 1) / h)). + rewrite Rabs_mult; rewrite Rmult_comm; pattern (Rabs ((cos h - 1) / h)) at 2; rewrite <- Rmult_1_r; apply Rmult_le_compat_l. { apply Rabs_pos. } pose proof (SIN_bound x). unfold Rabs; case (Rcase_abs (sin x)); lra. + assert (Rabs h < alp2). { apply Rlt_le_trans with alp. - apply H7. - unfold alp; apply Rmin_r. } assert (H9 := H4 _ H6 H8). rewrite cos_0 in H9; rewrite Rplus_0_l in H9; rewrite Rminus_0_r in H9; apply H9. - apply Rle_lt_trans with (Rabs (sin h / h - 1)). + rewrite Rabs_mult; rewrite Rmult_comm; pattern (Rabs (sin h / h - 1)) at 2; rewrite <- Rmult_1_r; apply Rmult_le_compat_l. { apply Rabs_pos. } pose proof (COS_bound x). unfold Rabs; case (Rcase_abs (cos x)); lra. + assert (Rabs h < alp1). { apply Rlt_le_trans with alp. - apply H7. - unfold alp; apply Rmin_l. } assert (H9 := H3 _ H6 H8). rewrite sin_0 in H9; rewrite Rplus_0_l in H9; rewrite Rminus_0_r in H9; apply H9. Qed.
imports: Rbase Rfunctions SeqSeries Rtrigo1 Ranalysis1 PSeries_reg Lra