proposition: Lemma ExpCC_equation_aid_3 : forall z1 z2 : CC, cc_IR (Exp (Re z1) [*]Exp (Re z2)) [*] ((Cos (Im z1) [*]Cos (Im z2) [-]Sin (Im z1) [*]Sin (Im z2)) [+I*] (Sin (Im z1) [*]Cos (Im z2) [+]Cos (Im z1) [*]Sin (Im z2))) [=] cc_IR (Exp (Re z1) [*]Exp (Re z2)) [*] ((Cos (Im z1) [+I*]Sin (Im z1)) [*] (Cos (Im z2) [+I*]Sin (Im z2))).
proof: Proof. intros z1 z2. apply bin_op_wd_unfolded. apply eq_reflexive. set (c1 := Cos (Im z1)) in *. set (c2 := Cos (Im z2)) in *. set (s1 := Sin (Im z1)) in *. set (s2 := Sin (Im z2)) in *. split; simpl in |- *; algebra. Qed.
imports: CoRN.complex.AbsCC CoRN.transc.Exponential CoRN.transc.Pi