proposition: Lemma Log_Exp_inv : Feq realline (Logarithm[o]Expon) FId.
proof: Proof. apply Feq_criterium with I (Fconst (S:=IR) [1]) ZeroR. cut (Derivative realline I Expon Expon); [ intro H | apply Derivative_Exp ]. cut (Derivative (openl [0]) I Logarithm {1/}FId); [ intro H0 | apply Derivative_Log ]. Derivative_Help. apply eq_imp_Feq. split; auto. exists I. split; auto. intro; simpl in |- *; apply Greater_imp_ap. apply less_wdr with (Exp x); [ apply Exp_pos | simpl in |- *; algebra ]. Included. intros; simpl in |- *; rational. apply Derivative_comp with (openl [0]) I; Deriv. red in |- *; intros a b Hab H1. exists (Exp a); exists (Exp b[+][1]); exists (leEq_less_trans _ _ _ _ (Exp_resp_leEq _ _ Hab) (less_plusOne _ _)). split. red in |- *; intros x H2. elim H2; intros H3 H4. simpl in |- *. apply less_leEq_trans with (Exp a); auto. apply Exp_pos. intros x Hx H2; elim H2; intros H3 H4; split. apply leEq_wdr with (Exp x). apply Exp_resp_leEq; auto. simpl in |- *; algebra. apply less_leEq; apply leEq_less_trans with (Exp b). apply leEq_wdl with (Exp x). apply Exp_resp_leEq; auto. simpl in |- *; algebra. apply less_plusOne. Deriv. split. intros; simpl in |- *. astepr (Log [1] (pos_one _)). unfold Log in |- *; apply pfwdef. astepr (Exp [0]). simpl in |- *; algebra. Qed.
imports: CoRN.transc.TaylorSeries