proposition: Lemma AbsCC_ExpCC : forall z : CC, AbsCC (ExpCC z) [=] Exp (Re z).
proof: Proof. intro z. unfold ExpCC in |- *. astepl (AbsCC (cc_IR (Exp (Re z))) [*]AbsCC (Cos (Im z) [+I*]Sin (Im z))). astepr (Exp (Re z) [*][1]). apply bin_op_wd_unfolded. assert (H : AbsCC (cc_IR (Exp (Re z))) [=] Exp (Re z)). apply AbsCC_IR. apply less_leEq. apply Exp_pos. astepl (Exp (Re z)). apply eq_reflexive. cut (AbsCC (Cos (Im z) [+I*]Sin (Im z)) [^]2 [=] [1]). set (x := AbsCC (Cos (Im z) [+I*]Sin (Im z))) in *. intro H0. assert (H1 : x[+][1][~=][0]). apply ap_imp_neq. apply Greater_imp_ap. apply leEq_less_trans with (y := x). unfold x in |- *. apply AbsCC_nonneg. apply less_plusOne. assert (H2 : (x[+][1]) [*] (x[-][1]) [=] [0]). cut (x[^]2[-][1][^]2 [=] [0]). intro H'. astepl (x[^]2[-][1][^]2). assumption. astepl (x[^]2[-][1]). astepr (OneR[-]OneR). apply cg_minus_wd; [ assumption | apply eq_reflexive ]. assert (H3 : x[-][1] [=] [0]). apply (mult_eq_zero _ _ _ H1 H2). rstepl ([1][+] (x[-][1])). astepr (OneR[+]ZeroR). apply plus_resp_eq. assumption. astepl (Cos (Im z) [^]2[+]Sin (Im z) [^]2). astepl OneR. apply eq_reflexive. apply AbsCC_square_Re_Im. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi