Definition ExpCC (z : C) := cc_IR (Exp (ℜ z)) [*] (Cos (ℑ z) [+I*]Sin (ℑ z)).

Lemma ExpCC_wd : forall z1 z2 : C, z1 [=] z2 -> ExpCC z1 [=] ExpCC z2.







Lemma ExpCC_plus : forall z1 z2 : C, ExpCC (z1[+]z2) [=] ExpCC z1[*]ExpCC z2.




Lemma ExpCC_Zero : ExpCC 0 [=] 1.



Lemma ExpCC_inv_aid : forall z : C, ExpCC z[*]ExpCC [--]z [=] 1.


Lemma ExpCC_ap_zero : forall z : C, ExpCC z [#] 0.

Lemma ExpCC_inv : forall z z_, (1[/] (ExpCC z) [//]z_) [=] ExpCC [--]z.



Lemma ExpCC_pow : forall z n, ExpCC z[^]n [=] ExpCC (nring n[*]z).




Lemma AbsCC_ExpCC : forall z : C, AbsCC (ExpCC z) [=] Exp (ℜ z).





Lemma ExpCC_Periodic : forall z, ExpCC (z[+]i[*]2[*]cc_IR π) [=] ExpCC z.




Lemma ExpCC_Exp : forall x : IR, ExpCC (cc_IR x) [=] cc_IR (Exp x).



Theorem Euler : (ExpCC (i[*] (cc_IR π))) [+]1 [=] 0.