proposition: Lemma sqrt_continuity_pt : forall x:R, 0 < x -> continuity_pt sqrt x.
proof: Proof. intros; generalize sqrt_continuity_pt_R1. unfold continuity_pt; unfold continue_in; unfold limit1_in; unfold limit_in; unfold dist; simpl; unfold Rdist; intros. assert (0 < eps / sqrt x). { unfold Rdiv; apply Rmult_lt_0_compat. - apply H1. - apply Rinv_0_lt_compat; apply sqrt_lt_R0; apply H. } elim (H0 _ H2); intros alp_1 H3. elim H3; intros. set (alpha := alp_1 * x). exists (Rmin alpha x); intros. split. { change (0 < Rmin alpha x); unfold Rmin; case (Rle_dec alpha x); intro. - unfold alpha; apply Rmult_lt_0_compat; assumption. - apply H. } intros; replace x0 with (x + (x0 - x)); [ idtac | ring ]; replace (sqrt (x + (x0 - x)) - sqrt x) with (sqrt x * (sqrt (1 + (x0 - x) / x) - sqrt 1)). 2:{ unfold Rminus; rewrite Rmult_plus_distr_l; rewrite Ropp_mult_distr_r_reverse; repeat rewrite <- sqrt_mult. - rewrite Rmult_1_r; rewrite Rmult_plus_distr_l; rewrite Rmult_1_r; unfold Rdiv; rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l. + rewrite Rmult_1_r; reflexivity. + red; intro; rewrite H7 in H; elim (Rlt_irrefl _ H). - left; apply H. - left; apply Rlt_0_1. - left; apply H. - elim H6; intros. destruct (Rcase_abs (x0 - x)) as [Hlt|Hgt]. + rewrite (Rabs_left (x0 - x) Hlt) in H8. rewrite Rplus_comm. apply Rplus_le_reg_l with (- ((x0 - x) / x)). rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; unfold Rdiv; rewrite <- Ropp_mult_distr_l_reverse. apply Rmult_le_reg_l with x. * apply H. * rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc; rewrite Rinv_l. -- rewrite Rmult_1_r; left; apply Rlt_le_trans with (Rmin alpha x). ++ apply H8. ++ apply Rmin_r. -- lra. + apply Rplus_le_le_0_compat. * lra. * unfold Rdiv; apply Rmult_le_pos. -- lra. -- left; apply Rinv_0_lt_compat; apply H. } rewrite Rabs_mult; rewrite (Rabs_right (sqrt x)). 2:{ apply Rle_ge; apply sqrt_positivity. left; apply H. } apply Rmult_lt_reg_l with (/ sqrt x). { apply Rinv_0_lt_compat; apply sqrt_lt_R0; assumption. } rewrite <- Rmult_assoc; rewrite Rinv_l. 2:{ assert (H7 := sqrt_lt_R0 x H). lra. } rewrite Rmult_1_l; rewrite Rmult_comm. unfold Rdiv in H5. case (Req_dec x x0); intro. { rewrite H7; unfold Rminus, Rdiv; rewrite Rplus_opp_r; rewrite Rmult_0_l; rewrite Rplus_0_r; rewrite Rplus_opp_r; rewrite Rabs_R0. apply Rmult_lt_0_compat. - assumption. - apply Rinv_0_lt_compat; rewrite <- H7; apply sqrt_lt_R0; assumption. } apply H5. split. - unfold D_x, no_cond. split. + trivial. + red; intro. assert ((x0 - x) * / x = 0) by lra. elim (Rmult_integral _ _ H9); intro. { lra. } assert (H11 := Rmult_eq_0_compat_r _ x H10). rewrite Rinv_l in H11;lra. - unfold Rminus; rewrite Rplus_comm; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; elim H6; intros. unfold Rdiv; rewrite Rabs_mult. rewrite Rabs_inv. rewrite (Rabs_right x). + rewrite Rmult_comm; apply Rmult_lt_reg_l with x. { apply H. } rewrite <- Rmult_assoc; rewrite Rinv_r. 2:{ lra. } rewrite Rmult_1_l; rewrite Rmult_comm; fold alpha. apply Rlt_le_trans with (Rmin alpha x). * apply H9. * apply Rmin_l. + apply Rle_ge; left; apply H. Qed.
imports: Rbase Rfunctions Ranalysis1 R_sqrt Lra