proposition: Lemma G_pres_mult : forall (IR : CReals) (x y : IR), (Build_CauchySeq Q_as_COrdField (fun m : nat => G IR (x[*]y) m) (CS_seq_G IR (x[*]y)) :R_COrdField Q_as_COrdField)[=] Build_CauchySeq Q_as_COrdField (fun m : nat => G IR x m[*]G IR y m) (CS_seq_mult Q_as_COrdField _ _ (CS_proof _ (G_as_CauchySeq IR x)) (CS_proof _ (G_as_CauchySeq IR y))).
proof: Proof. intros. apply not_ap_imp_eq. simpl in |- *. apply Eq_alt_2_2. intros. unfold CS_seq at 1 in |- *. unfold CS_seq in |- *. cut (SeqLimit (inj_Q_G_as_CauchySeq IR x) x). intro H0. cut (SeqLimit (inj_Q_G_as_CauchySeq IR y) y). intro H1. cut (SeqLimit (inj_Q_G_as_CauchySeq IR (x[*]y)) (x[*]y)). intro H2. case (CS_seq_bounded Q_as_COrdField (G IR y) (CS_seq_G IR y)). intro K. set (H3 := True) in *. intros H4 H5. case H5. intro M1. intro H6. case (nonarchemaedian_bound_for_Lim _ (inj_Q_G_as_CauchySeq IR x)). intro L. set (H7 := True) in *. intros H8 H9. cut (Twelve[*]inj_Q IR K[#][0]). intro H10. cut (Twelve[*]L[#][0]). intro H11. red in H0. case (H0 (inj_Q IR e[/] Twelve[*]inj_Q IR K[//]H10)). apply div_resp_pos. apply mult_resp_pos. apply pos_nring_S. apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. apply leEq_not_eq. apply (AbsSmall_nonneg Q_as_COrdField K (G IR y M1)). apply H6. constructor. apply less_imp_ap; auto. simpl in |- *. rational. apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. assumption. simpl in |- *. rational. intro N1. intro H12. red in H1. case (H1 (inj_Q IR e[/] Twelve[*]L[//]H11)). apply div_resp_pos. apply mult_resp_pos. apply pos_nring_S. assumption. apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. assumption. simpl in |- *. rational. intro N2. intro H13. red in H2. case (H2 (inj_Q IR e [/]TwoNZ)). apply div_resp_pos. apply pos_two. apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. assumption. simpl in |- *. rational. intro N3. intro H14. exists (N1 + (N2 + (N3 + M1))). intros. apply (AbsSmall_inj_Q IR). apply AbsSmall_wdr_unfolded with (y := inj_Q IR (G IR (x[*]y) m)[-] inj_Q IR (G IR x m)[*]inj_Q IR (G IR y m)). rstepr (inj_Q IR (G IR (x[*]y) m)[-]x[*]y[+]x[*](y[-]inj_Q IR (G IR y m))[+] inj_Q IR (G IR y m)[*](x[-]inj_Q IR (G IR x m))). rstepl (inj_Q IR e [/]TwoNZ[+]Three[*](L[*](inj_Q IR e[/] Twelve[*]L[//]H11))[+] Three[*](inj_Q IR K[*](inj_Q IR e[/] Twelve[*]inj_Q IR K[//]H10))). apply AbsSmall_plus. apply AbsSmall_plus. unfold inj_Q_G_as_CauchySeq in H14. unfold CS_seq at 1 in H14. apply H14. apply Nat.le_trans with (m := N1 + (N2 + (N3 + M1))). rewrite -> Nat.add_shuffle3 with (m := N3). rewrite -> Nat.add_shuffle3 with (m := N3). apply Nat.le_add_r. assumption. apply AbsSmall_mult. apply AbsSmall_wdr_unfolded with (y := Lim (inj_Q_G_as_CauchySeq IR x)). assumption. apply eq_symmetric_unfolded. apply SeqLimit_unique. apply x_is_SeqLimit_G. apply AbsSmall_minus. unfold inj_Q_G_as_CauchySeq in H13. unfold CS_seq at 1 in H13. apply H13. apply Nat.le_trans with (m := N1 + (N2 + (N3 + M1))). rewrite -> Nat.add_shuffle3 with (m := N2). apply Nat.le_add_r. assumption. apply AbsSmall_mult. apply inj_Q_AbsSmall. apply H6. apply Nat.le_trans with (m := N1 + (N2 + (N3 + M1))). rewrite -> Nat.add_comm with (m := M1). rewrite -> Nat.add_shuffle3 with (m := M1). rewrite -> Nat.add_shuffle3 with (m := M1). apply Nat.le_add_r. assumption. apply AbsSmall_minus. unfold inj_Q_G_as_CauchySeq in H12. unfold CS_seq at 1 in H12. apply H12. apply Nat.le_trans with (m := N1 + (N2 + (N3 + M1))). apply Nat.le_add_r. assumption. apply eq_transitive_unfolded with (y := inj_Q IR (G IR (x[*]y) m)[-]inj_Q IR (G IR x m[*]G IR y m)). apply cg_minus_wd. apply eq_reflexive_unfolded. apply eq_symmetric_unfolded. apply inj_Q_mult. apply eq_symmetric_unfolded. apply inj_Q_minus. apply Greater_imp_ap. apply mult_resp_pos. apply pos_nring_S. assumption. apply Greater_imp_ap. apply mult_resp_pos. apply pos_nring_S. apply less_wdl with (x := inj_Q IR [0]). apply inj_Q_less. apply leEq_not_eq. apply (AbsSmall_nonneg Q_as_COrdField K (G IR y M1)). apply H6. constructor. apply less_imp_ap; auto. simpl in |- *. rational. apply x_is_SeqLimit_G. apply x_is_SeqLimit_G. apply x_is_SeqLimit_G. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism