proposition: Theorem R_complete : forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } .
proof: Proof. intros. set (Vn := sequence_minorant Un (cauchy_min Un H)). set (Wn := sequence_majorant Un (cauchy_maj Un H)). pose proof (maj_cv Un H) as (x,p). fold Wn in p. pose proof (min_cv Un H) as (x0,p0). fold Vn in p0. cut (x = x0). - intros H2. exists x. rewrite <- H2 in p0. unfold Un_cv. intros. unfold Un_cv in p; unfold Un_cv in p0. cut (0 < eps / 3). + intro H4. elim (p (eps / 3) H4); intros. elim (p0 (eps / 3) H4); intros. exists (max x1 x2). intros. unfold Rdist. apply Rle_lt_trans with (Rabs (Un n - Vn n) + Rabs (Vn n - x)). { replace (Un n - x) with (Un n - Vn n + (Vn n - x)); [ apply Rabs_triang | ring ]. } apply Rle_lt_trans with (Rabs (Wn n - Vn n) + Rabs (Vn n - x)). * do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))). apply Rplus_le_compat_l. repeat rewrite Rabs_right. -- unfold Rminus; do 2 rewrite <- (Rplus_comm (- Vn n)); apply Rplus_le_compat_l. assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). fold Vn Wn in H8. elim (H8 n); intros. assumption. -- apply Rle_ge. unfold Rminus; apply Rplus_le_reg_l with (Vn n). rewrite Rplus_0_r. replace (Vn n + (Wn n + - Vn n)) with (Wn n); [ idtac | ring ]. assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). fold Vn Wn in H8. elim (H8 n); intros. apply Rle_trans with (Un n); assumption. -- apply Rle_ge. unfold Rminus; apply Rplus_le_reg_l with (Vn n). rewrite Rplus_0_r. replace (Vn n + (Un n + - Vn n)) with (Un n); [ idtac | ring ]. assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)). fold Vn Wn in H8. elim (H8 n); intros. assumption. * apply Rle_lt_trans with (Rabs (Wn n - x) + Rabs (x - Vn n) + Rabs (Vn n - x)). -- do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))). apply Rplus_le_compat_l. replace (Wn n - Vn n) with (Wn n - x + (x - Vn n)); [ apply Rabs_triang | ring ]. -- apply Rlt_le_trans with (eps / 3 + eps / 3 + eps / 3). 1:repeat apply Rplus_lt_compat. ++ unfold Rdist in H1. apply H1. unfold ge; apply Nat.le_trans with (max x1 x2). ** apply Nat.le_max_l. ** assumption. ++ rewrite <- Rabs_Ropp. replace (- (x - Vn n)) with (Vn n - x); [ idtac | ring ]. unfold Rdist in H3. apply H3. unfold ge; apply Nat.le_trans with (max x1 x2). ** apply Nat.le_max_r. ** assumption. ++ unfold Rdist in H3. apply H3. unfold ge; apply Nat.le_trans with (max x1 x2). ** apply Nat.le_max_r. ** assumption. ++ right. pattern eps at 4; replace eps with (3 * (eps / 3)). ** ring. ** unfold Rdiv; rewrite <- Rmult_assoc; apply Rmult_inv_r_id_m; discrR. + unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. - apply cond_eq. intros. cut (0 < eps / 5). + intro. unfold Un_cv in p; unfold Un_cv in p0. unfold Rdist in p; unfold Rdist in p0. elim (p (eps / 5) H1); intros N1 H4. elim (p0 (eps / 5) H1); intros N2 H5. unfold Cauchy_crit in H. unfold Rdist in H. elim (H (eps / 5) H1); intros N3 H6. set (N := max (max N1 N2) N3). apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - x0)). { replace (x - x0) with (x - Wn N + (Wn N - x0)); [ apply Rabs_triang | ring ]. } apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - Vn N) + Rabs (Vn N - x0)). * rewrite Rplus_assoc. apply Rplus_le_compat_l. replace (Wn N - x0) with (Wn N - Vn N + (Vn N - x0)); [ apply Rabs_triang | ring ]. * replace eps with (eps / 5 + 3 * (eps / 5) + eps / 5). -- repeat apply Rplus_lt_compat. ++ rewrite <- Rabs_Ropp. replace (- (x - Wn N)) with (Wn N - x); [ apply H4 | ring ]. unfold ge, N. apply Nat.le_trans with (max N1 N2); apply Nat.le_max_l. ++ unfold Wn, Vn. unfold sequence_majorant, sequence_minorant. assert (H7 := approx_maj (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))). assert (H8 := approx_min (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))). assert (H10 :Wn N = majorant (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))) by reflexivity. assert (H9:Vn N = minorant (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))) by reflexivity. rewrite <- H9 in H8 |- *. rewrite <- H10 in H7 |- *. elim (H7 (eps / 5) H1); intros k2 H11. elim (H8 (eps / 5) H1); intros k1 H12. apply Rle_lt_trans with (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Vn N)). { replace (Wn N - Vn N) with (Wn N - Un (N + k2)%nat + (Un (N + k2)%nat - Vn N)); [ apply Rabs_triang | ring ]. } apply Rle_lt_trans with (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Un (N + k1)%nat) + Rabs (Un (N + k1)%nat - Vn N)). { rewrite Rplus_assoc. apply Rplus_le_compat_l. replace (Un (N + k2)%nat - Vn N) with (Un (N + k2)%nat - Un (N + k1)%nat + (Un (N + k1)%nat - Vn N)); [ apply Rabs_triang | ring ]. } replace (3 * (eps / 5)) with (eps / 5 + eps / 5 + eps / 5); [ repeat apply Rplus_lt_compat | ring ]. ** assumption. ** { apply H6. - unfold ge. apply Nat.le_trans with N. + unfold N; apply Nat.le_max_r. + apply Nat.le_add_r. - unfold ge. apply Nat.le_trans with N. + unfold N; apply Nat.le_max_r. + apply Nat.le_add_r. } ** rewrite <- Rabs_Ropp. replace (- (Un (N + k1)%nat - Vn N)) with (Vn N - Un (N + k1)%nat); [ assumption | ring ]. ++ apply H5. unfold ge; apply Nat.le_trans with (max N1 N2). ** apply Nat.le_max_r. ** unfold N; apply Nat.le_max_l. -- pattern eps at 4; replace eps with (5 * (eps / 5)). ++ ring. ++ unfold Rdiv; rewrite <- Rmult_assoc; apply Rmult_inv_r_id_m. discrR. + unfold Rdiv; apply Rmult_lt_0_compat. * assumption. * apply Rinv_0_lt_compat. prove_sup0. Qed.
imports: Rbase Rfunctions Rseries SeqProp