proposition: Lemma CRmorph_mult_pos_pos : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), CRlt R1 0 y -> CRmorph f (CRmult R1 x y) == CRmult R2 (CRmorph f x) (CRmorph f y).
proof: Proof. split. { apply CRmorph_mult_pos_pos_le. exact H. } intro abs. destruct (CR_Q_dense R2 _ _ abs) as [q [H1 H2]]. destruct (CRmorph_rat f q) as [_ H3]. apply (CRle_lt_trans _ _ _ H3) in H2. clear H3. apply CRmorph_increasing_inv in H2. apply (CRlt_asym _ _ H2). clear H2. destruct (CR_Q_dense R2 _ _ H1) as [r [H2 H3]]. apply lt_CR_of_Q in H3. destruct (CR_archimedean R1 y) as [A Amaj]. destruct (CR_Q_dense R1 x (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A))))) as [s [H4 H5]]. - apply (CRle_lt_trans _ (CRplus R1 x 0)). + apply CRplus_0_r. + apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (CR_of_Q R1 0)). * apply CRle_refl. * apply CR_of_Q_lt. rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l. -- apply Qlt_minus_iff in H3. exact H3. -- reflexivity. - apply (CRmorph_increasing f) in H5. destruct (CRmorph_plus f x (CR_of_Q R1 ((q-r) * (1#A)))) as [_ H6]. apply (CRlt_le_trans _ _ _ H5) in H6. clear H5. destruct (CRmorph_rat f s) as [H5 _ ]. apply (CRle_lt_trans _ _ _ H5) in H6. clear H5. apply (CRmult_lt_compat_r (CRmorph f y)) in H6. 2:{ apply (CRle_lt_trans _ (CRmorph f 0)). - apply CRmorph_zero. - apply CRmorph_increasing. exact H. } apply (CRlt_le_trans _ (CRmult R1 (CR_of_Q R1 s) y)). { apply CRmult_lt_compat_r. - exact H. - exact H4. } clear H4. apply (CRmorph_le_inv f). apply (CRle_trans _ (CR_of_Q R2 q)). 2: destruct (CRmorph_rat f q); exact H0. apply (CRle_trans _ (CRmult R2 (CR_of_Q R2 s) (CRmorph f y))). 1:apply (CRle_trans _ (CRmorph f (CRmult R1 y (CR_of_Q R1 s)))). + destruct (CRmorph_proper f (CRmult R1 (CR_of_Q R1 s) y) (CRmult R1 y (CR_of_Q R1 s))). * apply (Rmul_comm (CRisRing R1)). * exact H4. + apply (CRle_trans _ (CRmult R2 (CRmorph f y) (CR_of_Q R2 s))). * exact (proj2 (CRmorph_mult_rat f y s)). * destruct (Rmul_comm (CRisRing R2) (CR_of_Q R2 s) (CRmorph f y)). exact H0. + intro H5. apply (CRlt_asym _ _ H5). clear H5. apply (CRlt_trans _ _ _ H6). clear H6. apply (CRle_lt_trans _ (CRplus R2 (CRmult R2 (CRmorph f x) (CRmorph f y)) (CRmult R2 (CRmorph f (CR_of_Q R1 ((q - r) * (1 # A)))) (CRmorph f y)))). { apply (Rdistr_l (CRisRing R2)). } apply (CRle_lt_trans _ (CRplus R2 (CR_of_Q R2 r) (CRmult R2 (CRmorph f (CR_of_Q R1 ((q - r) * (1 # A)))) (CRmorph f y)))). { apply CRplus_le_compat_r. intro H5. apply (CRlt_asym _ _ H5 H2). } clear H2. apply (CRle_lt_trans _ (CRplus R2 (CR_of_Q R2 r) (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y)))). { apply CRplus_le_compat_l, CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f 0)). + apply CRmorph_zero. + apply CRmorph_increasing. exact H. - destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H2. } apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 r) (CR_of_Q R2 ((q - r))))). * apply CRplus_lt_compat_l. apply (CRmult_lt_reg_l (CR_of_Q R2 (/((q - r) * (1 # A))))). { apply (CRle_lt_trans _ (CR_of_Q R2 0)). { apply CRle_refl. } apply CR_of_Q_lt, Qinv_lt_0_compat. rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l. - apply Qlt_minus_iff in H3. exact H3. - reflexivity. } apply (CRle_lt_trans _ (CRmorph f y)). -- apply (CRle_trans _ (CRmult R2 (CRmult R2 (CR_of_Q R2 (/ ((q - r) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A)))) (CRmorph f y))). { exact (proj2 (Rmul_assoc (CRisRing R2) (CR_of_Q R2 (/ ((q - r) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))). } apply (CRle_trans _ (CRmult R2 1 (CRmorph f y))). ++ apply CRmult_le_compat_r_half. { apply (CRle_lt_trans _ (CRmorph f 0)). { apply CRmorph_zero. } apply CRmorph_increasing. exact H. } apply (CRle_trans _ (CR_of_Q R2 ((/ ((q - r) * (1 # A))) * ((q - r) * (1 # A))))). { exact (proj1 (CR_of_Q_mult R2 (/ ((q - r) * (1 # A))) ((q - r) * (1 # A)))). } apply (CRle_trans _ (CR_of_Q R2 1)). { destruct (CR_of_Q_morph R2 (/ ((q - r) * (1 # A)) * ((q - r) * (1 # A))) 1). - field_simplify. { reflexivity. } split. { intro H5. inversion H5. } intro H5. apply Qlt_minus_iff in H3. rewrite H5 in H3. inversion H3. - exact H2. } apply CRle_refl. ++ destruct (Rmul_1_l (CRisRing R2) (CRmorph f y)). intro H5. contradiction. -- apply (CRlt_le_trans _ (CR_of_Q R2 (Z.pos A # 1))). 1:apply (CRlt_le_trans _ (CRmorph f (CR_of_Q R1 (Z.pos A # 1)))). { apply CRmorph_increasing. exact Amaj. } { exact (proj2 (CRmorph_rat f (Z.pos A # 1))). } apply (CRle_trans _ (CR_of_Q R2 ((/ ((q - r) * (1 # A))) * (q - r)))). 2: exact (proj2 (CR_of_Q_mult R2 (/ ((q - r) * (1 # A))) (q - r))). destruct (CR_of_Q_morph R2 (Z.pos A # 1) (/ ((q - r) * (1 # A)) * (q - r))). { field_simplify. { reflexivity. } split. - intro H5. inversion H5. - intro H5. apply Qlt_minus_iff in H3. rewrite H5 in H3. inversion H3. } exact H2. * apply (CRle_trans _ (CR_of_Q R2 (r + (q-r)))). -- exact (proj1 (CR_of_Q_plus R2 r (q-r))). -- destruct (CR_of_Q_morph R2 (r + (q-r)) q). ++ ring. ++ exact H2. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs