proposition: Lemma Log_mult : forall x y Hx Hy Hxy, Log (x[*]y) Hxy [=] Log x Hx[+]Log y Hy.
proof: Proof. intros x y Hx Hy Hxy. set (G := (Logarithm[o]y{**}FId) {-}[-C-] (Log y Hy)) in *. cut (proper (openl [0])); [ intro H | simpl in |- *; auto ]. cut (Derivative (openl [0]) H G {1/}FId). intro H0. cut (Derivative (openl [0]) H Logarithm {1/}FId); [ intro H1 | Deriv ]. elim (FTC2 (openl [0]) {1/}FId log_defn_lemma [1] (pos_one IR) H G H0); intros c Hc. fold Logarithm in Hc. elim Hc; intros H2' H2''. elim H2''; intros H2 H5. clear Hc H2 H2' H2''. cut (c [=] [0]). intro H2. cut (forall z w t : IR, w[-] (z[-]t) [=] [0] -> z [=] w[+]t). intro H3. apply H3; clear H3. astepr c; clear H2. cut (Dom (Logarithm{-}G) x); [ intro H2 | repeat split; simpl in |- *; auto ]. eapply eq_transitive_unfolded. 2: apply (H5 x Hx H2 I). Opaque Logarithm. simpl in |- *; algebra. clear H5. exists (I, I); apply mult_resp_pos; auto. intros z w t H3. rstepl (z[-]t[+]t). apply bin_op_wd_unfolded. 2: algebra. apply cg_inv_unique_2. astepr ( [--]ZeroR). rstepl ( [--] (w[-] (z[-]t))). apply un_op_wd_unfolded; auto. cut (Dom (Logarithm{-}G) [1]); [ intro H2 | repeat split; simpl in |- *; auto ]. apply eq_symmetric_unfolded; eapply eq_transitive_unfolded. 2: apply (H5 [1] (pos_one IR) H2 I). simpl in |- *. rstepl ([0][-] (Log y Hy[-]Log y Hy)). algebra. Transparent Logarithm. simpl in |- *; apply pos_one. exists (I, I); simpl in |- *; apply mult_resp_pos; auto; apply pos_one. unfold G in |- *. cut (Derivative (openl [0]) H Logarithm {1/}FId); [ intro H0 | unfold Logarithm in |- *; apply FTC1 ]. Derivative_Help. apply eq_imp_Feq. repeat split. exists (I, I); simpl in |- *. repeat split. intros; apply Greater_imp_ap; apply mult_resp_pos; auto. Included. intros; simpl in |- *; rational. apply Derivative_minus. apply Derivative_comp with (openl [0]) H; Deriv. clear H0; red in |- *; intros a b Hab H0. simpl in |- *; exists (y[*]a); exists (y[*]b[+][1]). cut (y[*]a [<] y[*]b[+][1]). intro H1; exists H1; split. intros x0 H2. elim H2; intros H3 H4; simpl in |- *. apply less_leEq_trans with (y[*]a). apply mult_resp_pos; auto. apply H0; apply compact_inc_lft. auto. intros x0 Hx0 H2; elim H2; intros H3 H4; split. apply mult_resp_leEq_lft; auto. apply less_leEq; auto. apply leEq_transitive with (y[*]b). apply mult_resp_leEq_lft; auto. apply less_leEq; auto. apply less_leEq; apply less_plusOne. apply leEq_less_trans with (y[*]b). apply mult_resp_leEq_lft; auto. apply less_leEq; auto. apply less_plusOne. Deriv. Qed.
imports: CoRN.transc.TaylorSeries