proposition: Lemma ExpCC_equation_aid_4 : forall z1 z2 : CC, cc_IR (Exp (Re z1) [*]Exp (Re z2)) [*] ((Cos (Im z1) [+I*]Sin (Im z1)) [*] (Cos (Im z2) [+I*]Sin (Im z2))) [=] ExpCC z1[*]ExpCC z2.
proof: Proof. intros z1 z2. unfold ExpCC in |- *. set (c := Cos (Im z1) [+I*]Sin (Im z1)) in *. set (d := Cos (Im z2) [+I*]Sin (Im z2)) in *. astepl (cc_IR (Exp (Re z1)) [*]cc_IR (Exp (Re z2)) [*] (c[*]d)). rational. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi