proposition: Theorem R_is_complete : forall a : CauchySeq R_COrdField', SeqLimit (R:=R_COrdField') a (LimR_CauchySeq a).
proof: Proof. intros. simpl in |- *. red in |- *. case a. intros a_ pa. intros e H. simpl in |- *. set (He := pos_ap_zero _ _ H) in *. elim (Q_dense_in_R (e [/]ThreeNZ)); [ intros q Hq Hinj | apply pos_div_three; auto ]. set (Hq' := pos_ap_zero _ _ Hq) in *. elim (F_is_archemaedian ((Four[/] q[//]Hq') [-][1])); intros M HM. unfold Cauchy_prop in pa. elim (pa (e [/]SixNZ)); [ intros N2 HN2 | apply pos_div_six; auto ]. elim (CS_seq_diagonal (Build_CauchySeq R_COrdField' a_ pa) (q [/]EightNZ)); [ intros N1 HN1 | apply pos_div_eight; auto ]. exists (Nat.max M (Nat.max N1 N2)). intros. rstepl (e [/]ThreeNZ[+]e [/]ThreeNZ[+]e [/]ThreeNZ). rstepr (a_ m[-]a_ (Nat.max M (Nat.max N1 N2)) [+] (a_ (Nat.max M (Nat.max N1 N2)) [-] inject_Q (CS_seq F (LimR_CauchySeq (Build_CauchySeq R_COrdField' a_ pa)) (Nat.max M (Nat.max N1 N2)))) [+] (inject_Q (CS_seq F (LimR_CauchySeq (Build_CauchySeq R_COrdField' a_ pa)) (Nat.max M (Nat.max N1 N2))) [-] LimR_CauchySeq (Build_CauchySeq R_COrdField' a_ pa))). apply AbsSmall_plus. apply AbsSmall_plus. rstepl (e [/]SixNZ[+]e [/]SixNZ). rstepr (a_ m[-]a_ N2[+] (a_ N2[-]a_ (Nat.max M (Nat.max N1 N2)))). apply AbsSmall_plus. apply HN2; eauto with arith. apply AbsSmall_minus; apply HN2; eauto with arith. apply AbsSmall_leEq_trans with (R := R_COrdField') (e1 := inject_Q q). apply less_leEq; assumption. apply AbsSmall_minus. simpl in |- *. apply AbsSmall_leEq_trans with (R := R_COrdField') (e1 := Four[*] (one_div_succ (Nat.max M (Nat.max N1 N2)):R_COrdField')). apply less_leEq. apply leEq_less_trans with (R := R_COrdField') (y := Four[*]one_div_succ (R:=R_COrdField') M). apply mult_resp_leEq_lft. apply one_div_succ_resp_leEq. auto with arith. apply less_leEq; apply pos_four. apply mult_cancel_less with (R := R_COrdField') (z := nring M[+][1]:R_COrdField'). apply less_transitive_unfolded with (F := R_COrdField') (y := inject_Q (Four[/] q[//]Hq')). change (inject_Q ([0]:F) [<] inject_Q (Four[/] q[//]Hq')) in |- *. apply ing_lt. apply mult_cancel_less with (R := F) (z := q). assumption. rstepl ([0]:F). rstepr (Four:F). apply pos_four. apply shift_less_plus. astepl (inject_Q ((Four[/] q[//]Hq') [+][--][1])). astepr (inject_Q (nring M)). apply ing_lt. rstepl ((Four[/] q[//]Hq') [-][1]). exact HM. apply eq_symmetric_unfolded. apply ing_nring. unfold cg_minus in |- *. apply eq_transitive_unfolded with (inject_Q (Four[/] q[//]Hq') [+]inject_Q ( [--][1]:F)). apply ing_plus. apply plus_resp_eq. apply eq_transitive_unfolded with ( [--] (inject_Q ([1]:F))). apply ing_min. astepl ([0][-]inject_Q ([1]:F)). Step_final ([0][-] ([1]:R_COrdField')). unfold one_div_succ in |- *. unfold Snring in |- *. change (Four[*] ([1][/] nring M[+][1][//]nringS_ap_zero R_COrdField' M) [*] (nring M[+][1]) [<] inject_Q q[*] (nring M[+][1])) in |- *. rstepl (Four:R_COrdField'). astepr (inject_Q q[*]inject_Q (nring M[+][1])). astepl (inject_Q (Four:F)). astepr (inject_Q (q[*] (nring M[+][1]))). apply ing_lt. apply mult_cancel_less with (R := F) (z := [1][/] q[//]Hq'). apply recip_resp_pos. assumption. rstepl (Four[/] q[//]Hq'). rstepr (nring (R:=F) M[+][1]). apply plus_cancel_less with (R := F) (z := [--] ([1]:F)). rstepl ((Four[/] q[//]Hq') [-][1]). rstepr (nring (R:=F) M). exact HM. apply ing_mult. apply eq_symmetric_unfolded. apply ing_nring. apply mult_wd. apply ing_eq. apply eq_reflexive_unfolded. apply eq_transitive_unfolded with (inject_Q (nring M) [+]inject_Q ([1]:F)). apply ing_plus. astepl (inject_Q (nring M) [+][1]). astepl ([1][+]inject_Q (nring M)). astepr ([1][+]nring (R:=R_COrdField') M). apply plus_resp_eq. apply eq_symmetric_unfolded. apply ing_nring. astepl (inject_Q (Four[*]one_div_succ (R:=F) (Nat.max M (Nat.max N1 N2)))). apply expand_Q_R_2 with (x := a_ (Nat.max M (Nat.max N1 N2))) (e := Four[*]one_div_succ (R:=F) (Nat.max M (Nat.max N1 N2))) (N := T (a_ (Nat.max M (Nat.max N1 N2))) (Nat.max M (Nat.max N1 N2))). apply mult_resp_pos. apply pos_four. apply one_div_succ_pos. intros. rstepl (one_div_succ (R:=F) (Nat.max M (Nat.max N1 N2))). apply modulus_property_2. assumption. apply eq_transitive_unfolded with (inject_Q (Four:F) [*]inject_Q (one_div_succ (Nat.max M (Nat.max N1 N2)))). apply ing_mult. apply eq_transitive_unfolded with (Four[*]inject_Q (one_div_succ (Nat.max M (Nat.max N1 N2)))). apply mult_wd. apply eq_symmetric_unfolded. apply ing_nring. apply eq_reflexive_unfolded. apply mult_wd. apply eq_reflexive_unfolded. unfold one_div_succ in |- *. unfold Snring in |- *. astepl (inject_Q ([1][/] _[//]nringS_ap_zero _ (Nat.max M (Nat.max N1 N2)))). Step_final ([1][/] _[//]nringS_ap_zero R_COrdField' (Nat.max M (Nat.max N1 N2))). apply eq_transitive_unfolded with (inject_Q ([1]:F) [/] _[//]nringS_ap_zero _ (Nat.max M (Nat.max N1 N2))). apply eq_symmetric_unfolded. apply ing_n. apply div_wd. exact ing_One. apply eq_reflexive_unfolded. apply AbsSmall_leEq_trans with (R := R_COrdField') (e1 := inject_Q q). apply less_leEq; assumption. apply expand_Q_R_2 with (x := LimR_CauchySeq (Build_CauchySeq R_COrdField' a_ pa)) (e := q) (N := Nat.max M (Nat.max N1 N2)). assumption. intros. rstepl (q [/]EightNZ[+]q [/]EightNZ). rstepr (CS_seq F (LimR_CauchySeq (Build_CauchySeq R_COrdField' a_ pa)) m0[-] CS_seq F (LimR_CauchySeq (Build_CauchySeq R_COrdField' a_ pa)) N1[+] (CS_seq F (LimR_CauchySeq (Build_CauchySeq R_COrdField' a_ pa)) N1[-] CS_seq F (LimR_CauchySeq (Build_CauchySeq R_COrdField' a_ pa)) (Nat.max M (Nat.max N1 N2)))). apply AbsSmall_plus. unfold LimR_CauchySeq in |- *; simpl in |- *; apply HN1; eauto with arith. apply AbsSmall_minus. unfold LimR_CauchySeq in |- *; simpl in |- *; apply HN1; eauto with arith. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals