proposition: Lemma CRmorph_mult_pos_pos_le : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), CRlt R1 0 y -> CRmult R2 (CRmorph f x) (CRmorph f y) <= CRmorph f (CRmult R1 x y).
proof: Proof. intros. intro abs. destruct (CR_Q_dense R2 _ _ abs) as [q [H1 H2]]. destruct (CRmorph_rat f q) as [H3 _]. apply (CRlt_le_trans _ _ _ H1) in H3. clear H1. apply CRmorph_increasing_inv in H3. apply (CRlt_asym _ _ H3). clear H3. destruct (CR_Q_dense R2 _ _ H2) as [r [H1 H3]]. apply lt_CR_of_Q in H1. destruct (CR_archimedean R1 y) as [A Amaj]. assert (/ ((r - q) * (1 # A)) * (q - r) == - (Z.pos A # 1))%Q as diveq. { rewrite Qinv_mult_distr. setoid_replace (q-r)%Q with (-1*(r-q))%Q. 2:field. field_simplify. - reflexivity. - split. + intro H4. inversion H4. + intro H4. apply Qlt_minus_iff in H1. rewrite H4 in H1. inversion H1. } destruct (CR_Q_dense R1 (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A)))) x) as [s [H4 H5]]. - apply (CRlt_le_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l R1 (CR_of_Q R1 ((r-q) * (1#A)))). apply (CRle_lt_trans _ 0). 1:apply (CRle_trans _ (CR_of_Q R1 ((r-q)*(1#A) + (q-r)*(1#A)))). + destruct (CR_of_Q_plus R1 ((r-q)*(1#A)) ((q-r)*(1#A))). exact H0. + apply (CRle_trans _ (CR_of_Q R1 0)). 2: apply CRle_refl. intro H4. apply lt_CR_of_Q in H4. ring_simplify in H4. inversion H4. + apply (CRlt_le_trans _ (CR_of_Q R1 ((r - q) * (1 # A)))). 2: apply CRplus_0_r. apply (CRle_lt_trans _ (CR_of_Q R1 0)). 1:apply CRle_refl. apply CR_of_Q_lt. rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l. * apply Qlt_minus_iff in H1. exact H1. * reflexivity. - apply (CRmorph_increasing f) in H4. destruct (CRmorph_plus f x (CR_of_Q R1 ((q-r) * (1#A)))) as [H6 _]. apply (CRle_lt_trans _ _ _ H6) in H4. clear H6. destruct (CRmorph_rat f s) as [_ H6]. apply (CRlt_le_trans _ _ _ H4) in H6. clear H4. apply (CRmult_lt_compat_r (CRmorph f y)) in H6. + destruct (Rdistr_l (CRisRing R2) (CRmorph f x) (CRmorph f (CR_of_Q R1 ((q-r) * (1#A)))) (CRmorph f y)) as [H4 _]. apply (CRle_lt_trans _ _ _ H4) in H6. clear H4. apply (CRle_lt_trans _ (CRmult R1 (CR_of_Q R1 s) y)). 2:{ apply CRmult_lt_compat_r. - exact H. - exact H5. } apply (CRmorph_le_inv f). apply (CRle_trans _ (CR_of_Q R2 q)). { destruct (CRmorph_rat f q). exact H4. } apply (CRle_trans _ (CRmult R2 (CR_of_Q R2 s) (CRmorph f y))). 1:apply (CRle_trans _ (CRplus R2 (CRmult R2 (CRmorph f x) (CRmorph f y)) (CR_of_Q R2 (q-r)))). 1:apply (CRle_trans _ (CRplus R2 (CR_of_Q R2 r) (CR_of_Q R2 (q - r)))). * apply (CRle_trans _ (CR_of_Q R2 (r + (q-r)))). -- intro H4. apply lt_CR_of_Q in H4. ring_simplify in H4. exact (Qlt_not_le q q H4 (Qle_refl q)). -- destruct (CR_of_Q_plus R2 r (q-r)). exact H4. * apply CRplus_le_compat_r. intro H4. apply (CRlt_asym _ _ H3). exact H4. * intro H4. apply (CRlt_asym _ _ H4). clear H4. apply (CRlt_trans_flip _ _ _ H6). clear H6. apply CRplus_lt_compat_l. apply (CRlt_le_trans _ (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))). { apply (CRmult_lt_reg_l (CR_of_Q R2 (/((r-q)*(1#A))))). 1: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 (r-q)). apply Qmult_lt_l. + apply Qlt_minus_iff in H1. exact H1. + reflexivity. - apply (CRle_lt_trans _ (CRopp R2 (CR_of_Q R2 (Z.pos A # 1)))). 1:apply (CRle_trans _ (CR_of_Q R2 (-(Z.pos A # 1)))). 1:apply (CRle_trans _ (CR_of_Q R2 ((/ ((r - q) * (1 # A))) * (q - r)))). + destruct (CR_of_Q_mult R2 (/ ((r - q) * (1 # A))) (q - r)). exact H0. + destruct (CR_of_Q_morph R2 (/ ((r - q) * (1 # A)) * (q - r)) (-(Z.pos A # 1))). * exact diveq. * intro H7. apply lt_CR_of_Q in H7. rewrite diveq in H7. exact (Qlt_not_le _ _ H7 (Qle_refl _)). + destruct (@CR_of_Q_opp R2 (Z.pos A # 1)). exact H4. + apply (CRlt_le_trans _ (CRopp R2 (CRmorph f y))). { apply CRopp_gt_lt_contravar. apply (CRlt_le_trans _ (CRmorph f (CR_of_Q R1 (Z.pos A # 1)))). { apply CRmorph_increasing. exact Amaj. } destruct (CRmorph_rat f (Z.pos A # 1)). exact H4. } apply (CRle_trans _ (CRmult R2 (CRopp R2 1) (CRmorph f y))). 1:apply (CRle_trans _ (CRopp R2 (CRmult R2 1 (CRmorph f y)))). * destruct (Ropp_ext (CRisRingExt R2) (CRmorph f y) (CRmult R2 1 (CRmorph f y))). -- apply CReq_sym, (Rmul_1_l (CRisRing R2)). -- exact H4. * destruct (CRopp_mult_distr_l 1 (CRmorph f y)). exact H4. * apply (CRle_trans _ (CRmult R2 (CRmult R2 (CR_of_Q R2 (/ ((r - q) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A)))) (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 ((/ ((r - q) * (1 # A))) * ((q - r) * (1 # A))))). 1:apply (CRle_trans _ (CR_of_Q R2 (-1))). 1:apply (CRle_trans _ (CRopp R2 (CR_of_Q R2 1))). + destruct (Ropp_ext (CRisRingExt R2) 1 (CR_of_Q R2 1)). * reflexivity. * exact H4. + destruct (@CR_of_Q_opp R2 1). exact H0. + destruct (CR_of_Q_morph R2 (-1) (/ ((r - q) * (1 # A)) * ((q - r) * (1 # A)))). * field. split. -- intro H4. inversion H4. -- intro H4. apply Qlt_minus_iff in H1. rewrite H4 in H1. inversion H1. * exact H4. + destruct (CR_of_Q_mult R2 (/ ((r - q) * (1 # A))) ((q - r) * (1 # A))). exact H4. } destruct (Rmul_assoc (CRisRing R2) (CR_of_Q R2 (/ ((r - q) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y)). exact H0. } apply 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 H0. * apply (CRle_trans _ (CRmorph f (CRmult R1 y (CR_of_Q R1 s)))). 1:apply (CRle_trans _ (CRmult R2 (CRmorph f y) (CR_of_Q R2 s))). -- destruct (Rmul_comm (CRisRing R2) (CRmorph f y) (CR_of_Q R2 s)). exact H0. -- destruct (CRmorph_mult_rat f y s). exact H0. -- destruct (CRmorph_proper f (CRmult R1 y (CR_of_Q R1 s)) (CRmult R1 (CR_of_Q R1 s) y)). ++ apply (Rmul_comm (CRisRing R1)). ++ exact H4. + apply (CRle_lt_trans _ (CRmorph f 0)). * apply CRmorph_zero. * apply CRmorph_increasing. exact H. Qed.
imports: QArith Qabs ConstructiveReals ConstructiveLimits ConstructiveAbs